Type equality in constraint not used?
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
import Data.Kind
data TyRep :: forall k. k -> Type where
TyInt :: TyRep Int
TyBool :: TyRep Bool
TyMaybe :: TyRep Maybe
TyApp :: TyRep f -> TyRep x -> TyRep (f x)
zero :: Type ~ k => TyRep (a :: k) -> a
zero = undefine
fails with the error
ttest.hs:13:39: error:
• Expected a type, but ‘a’ has kind ‘k’
• In the type signature: zero :: Type ~ k => TyRep (a :: k) -> a
But if you replace zero
with
zero :: TypeRep (a :: Type) -> a
zero = undefined
then the program compiles.