[GHC] #13822: GHC not using injectivity?

[GHC]

#13822: GHC not using injectivity?
-------------------------------------+-------------------------------------
           Reporter:  Iceland_jack   |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.0.1
           Keywords:                 |  Operating System:  Unknown/Multiple
  InjectiveFamilies, TypeInType      |
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 This may be normal behavior but.. (Example from
 [http://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1014&context=compsci_pubs
 System FC with Explicit Kind Equality])

 {{{#!hs
 {-# LANGUAGE GADTs, TypeOperators, PolyKinds, DataKinds,
 TypeFamilyDependencies, TypeInType, RankNTypes, LambdaCase, EmptyCase #-}

 import Data.Kind

 data KIND = STAR | KIND :> KIND

 data Ty :: KIND -> Type where
   TInt   :: Ty STAR
   TBool  :: Ty STAR
   TMaybe :: Ty (STAR :> STAR)
   TApp   :: Ty (a :> b) -> (Ty a -> Ty b)

 type family
   IK (k :: KIND) = (res :: Type) | res -> k where
   IK STAR   = Type
   IK (a:>b) = IK a -> IK b

 type family
   I (t :: Ty k) = (res :: IK k) | res -> t where
   I TInt       = Int
   I TBool      = Bool
   I TMaybe     = Maybe
   I (TApp f a) = (I f) (I a)

 data TyRep (k :: KIND) (t :: Ty k) where
   TyInt   :: TyRep STAR         TInt
   TyBool  :: TyRep STAR         TBool
   TyMaybe :: TyRep (STAR:>STAR) TMaybe
   TyApp   :: TyRep (a:>b) f -> TyRep a x -> TyRep b (TApp f x)

 zero :: TyRep STAR a -> I a
 zero = \case
   TyInt           -> 0
   TyBool          -> False
   TyApp TyMaybe _ -> Nothing
 }}}

 When I ask it to infer the representation for `Int` and `Bool` it does so
 with no surprises

 {{{#!hs
 -- Inferred type:
 --
 -- int :: TyRep STAR TInt -> Int
 int rep = zero rep :: Int


 -- bool:: TyRep STAR TBool -> Bool
 bool rep = zero rep :: Bool
 }}}

 but inferring the representation for `Maybe Int` fails

 {{{#!hs
 -- v.hs:43:16: error:
 --     • Couldn't match kind ‘k’ with ‘'STAR’
 --       ‘k’ is a rigid type variable bound by
 --         the inferred type of
 --         maybeInt :: (I 'TInt ~ Int, I 'TMaybe ~ Maybe) =>
 --                     TyRep 'STAR ('TApp 'TMaybe 'TInt) -> Maybe Int
 --         at v.hs:25:3
 --       When matching the kind of ‘'TMaybe’
 --       Expected type: Maybe Int
 --         Actual type: I ('TApp 'TMaybe 'TInt)
 --     • In the expression: zero rep :: Maybe Int
 --       In an equation for ‘maybeInt’: maybeInt rep = zero rep :: Maybe
 Int
 --     • Relevant bindings include
 --         rep :: TyRep 'STAR ('TApp 'TMaybe 'TInt) (bound at v.hs:43:10)
 --         maybeInt :: TyRep 'STAR ('TApp 'TMaybe 'TInt) -> Maybe Int
 --           (bound at v.hs:43:1)
 -- Failed, modules loaded: none.
 maybeInt rep = zero rep :: Maybe Int
 }}}

 even though `I` is injective and GHC knows that `I (TMaybe `TApp` TMaybe)
 = Maybe Int`

 {{{
 >>> :kind! I (TMaybe `TApp` TInt)
 I (TMaybe `TApp` TInt) :: IK 'STAR
 = Maybe Int
 }}}

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