content: {-# LANGUAGE DataKinds, GADTs, PolyKinds, TypeFamilies, ExplicitForAll,
               TemplateHaskell, UndecidableInstances, ScopedTypeVariables #-}
  
  module KindEqualities2 where
  
  import Data.Kind
  import GHC.Exts ( Any )
  
  data Kind = Star | Arr Kind Kind
  
  data Ty :: Kind -> Type where
    TInt :: Ty Star
    TBool :: Ty Star
    TMaybe :: Ty (Arr Star Star)
    TApp :: Ty (Arr k1 k2) -> Ty k1 -> Ty k2
  
  
  type TyRep :: forall (k :: Kind) -> Ty k -> Type
  data TyRep k t where
    TyInt :: TyRep Star TInt
    TyBool :: TyRep Star TBool
    TyMaybe :: TyRep (Arr Star Star) TMaybe
    TyApp :: TyRep (Arr k1 k2) a -> TyRep k1 b -> TyRep k2 (TApp a b)
  
  type family IK (k :: Kind)
  type instance IK Star = Type
  type instance IK (Arr k1 k2) = IK k1 -> IK k2
  
  $(return [])  -- necessary because the following instances depend on the
                -- previous ones.
  
  type family I (t :: Ty k) :: IK k
  type instance I TInt = Int
  type instance I TBool = Bool
  type instance I TMaybe = Maybe
  type instance I (TApp a b) = (I a) (I b)
  
  zero :: forall (a :: Ty 'Star). TyRep Star a -> I a
  zero TyInt = 0
  zero TyBool = False
  zero (TyApp TyMaybe TyInt) = Nothing
  
  main = print $ zero (TyApp TyMaybe TyInt)
  