GHC not using injectivity?

This may be normal behavior but.. (Example from System FC with Explicit Kind Equality)

{-# 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

-- 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

-- 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

Trac metadata

Trac field	Value
Version	8.0.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture