diff options
Diffstat (limited to 'testsuite/tests/dependent/should_compile/KindEqualities2.hs')
-rw-r--r-- | testsuite/tests/dependent/should_compile/KindEqualities2.hs | 43 |
1 files changed, 43 insertions, 0 deletions
diff --git a/testsuite/tests/dependent/should_compile/KindEqualities2.hs b/testsuite/tests/dependent/should_compile/KindEqualities2.hs new file mode 100644 index 0000000000..5a6f60d40b --- /dev/null +++ b/testsuite/tests/dependent/should_compile/KindEqualities2.hs @@ -0,0 +1,43 @@ +{-# LANGUAGE DataKinds, GADTs, PolyKinds, TypeFamilies, ExplicitForAll, + TemplateHaskell, UndecidableInstances, ScopedTypeVariables, + TypeInType #-} + +module KindEqualities2 where + +import Data.Kind +import GHC.Exts ( Any ) + +data Kind = Star | Arr Kind Kind + +data Ty :: Kind -> * where + TInt :: Ty Star + TBool :: Ty Star + TMaybe :: Ty (Arr Star Star) + TApp :: Ty (Arr k1 k2) -> Ty k1 -> Ty k2 + + +data TyRep (k :: Kind) (t :: Ty k) 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 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) |