summaryrefslogtreecommitdiff
path: root/testsuite/tests/dependent/should_compile/KindEqualities2.hs
diff options
context:
space:
mode:
Diffstat (limited to 'testsuite/tests/dependent/should_compile/KindEqualities2.hs')
-rw-r--r--testsuite/tests/dependent/should_compile/KindEqualities2.hs43
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)