Opened 3 years ago

# Problems with injective type families

Reported by: Owned by: Iceland_jack normal Compiler 8.0.1 InjectiveFamilies Unknown/Multiple Unknown/Multiple None/Unknown

### Description

```{-# LANGUAGE GADTs, TypeInType, DataKinds, TypeFamilyDependencies #-}

import Data.Kind

type family
IB a = res | res -> a where
IB Int  = Bool
IB Bool = Int

type Cat k = k -> k -> Type

data F :: Cat Type where
F :: (a -> IB a) -> F a (IB a)

data Exp :: Type -> Type where
I :: Int  -> Exp Int
B :: Bool -> Exp Bool

fmap' :: F a b -> (Exp a -> Exp b)
fmap' (F f) = \case
B b -> I (f b)
I i -> B (f i)
```

I would have thought this should work as well, given that `IB` is injective:

```data F :: Cat Type where
F :: (IB a -> a) -> F (IB a) a
```

but it gives

```fmap' :: F a b -> (Exp a -> Exp b)
fmap' (F f) = \case
B b -> I (f b)

-- c.hs:33:13: error:
--     • Could not deduce: b ~ Int
--       from the context: a ~ IB b
--         bound by a pattern with constructor:
--                    F :: forall a. (IB a -> a) -> F (IB a) a,
--                  in an equation for ‘fmap'’
--         at c.hs:32:8-10
--       or from: a ~ Bool
--         bound by a pattern with constructor: B :: Bool -> Exp Bool,
--                  in a case alternative
--         at c.hs:33:3-5
--       ‘b’ is a rigid type variable bound by
--         the type signature for:
--           fmap' :: forall a b. F a b -> Exp a -> Exp b
--         at c.hs:31:10
--     • In the first argument of ‘I’, namely ‘(f b)’
--       In the expression: I (f b)
--       In a case alternative: B b -> I (f b)
--     • Relevant bindings include
--         f :: IB b -> b (bound at c.hs:32:10)
--         fmap' :: F a b -> Exp a -> Exp b (bound at c.hs:32:1)
```

But if we know that `a ~ Bool` (as we do from matching on `B`), and we know that `a ~ IB b` then by injectivity it should figure that `b ~ Int`?

### comment:1 Changed 3 years ago by goldfire

No, injectivity can't yet do this. Injectivity annotations are very much like functional dependencies, working only to do type inference. They have no representation in Core. Why not, you ask? Because I was unable to prove the soundness of doing so. But perhaps Constrained Type Families gives us a way forward here. I have yet to attempt the injectivity proof in the context of that paper, but my hunch is that it will succeed.

### comment:2 Changed 3 years ago by Iceland_jack

Sounds promising, should the ticket be kept open?

### comment:3 Changed 3 years ago by goldfire

Type: bug → feature request

As a feature request, sure. But don't hold your breath! :)

### comment:4 Changed 3 years ago by Iceland_jack

Too late!

Note: See TracTickets for help on using tickets.