Opened 3 years ago

Last modified 3 years ago

## #13621 new feature request

# Problems with injective type families

Reported by: | Iceland_jack | Owned by: | |
---|---|---|---|

Priority: | normal | Milestone: | |

Component: | Compiler | Version: | 8.0.1 |

Keywords: | InjectiveFamilies | Cc: | |

Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |

Type of failure: | None/Unknown | Test Case: | |

Blocked By: | Blocking: | ||

Related Tickets: | Differential Rev(s): | ||

Wiki Page: |

### 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) -- Failed, modules loaded: none.

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`

?

### Change History (4)

### comment:1 Changed 3 years ago by

### comment:3 Changed 3 years ago by

Type: | bug → feature request |
---|

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

**Note:**See TracTickets for help on using tickets.

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.