[GHC] #13621: Problems with injective type families

[GHC]

#13621: Problems with injective type families
-------------------------------------+-------------------------------------
           Reporter:  Iceland_jack   |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.0.1
           Keywords:                 |  Operating System:  Unknown/Multiple
  InjectiveFamilies                  |
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 {{{#!hs
 {-# 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:

 {{{#!hs
 data F :: Cat Type where
   F :: (IB a -> a) -> F (IB a) a
 }}}

 but it gives

 {{{#!hs
 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`?

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13621>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler