5a6f60d40b36d953f2917417add155c652fb2373
[ghc.git] / testsuite / tests / dependent / should_compile / KindEqualities2.hs
1 {-# LANGUAGE DataKinds, GADTs, PolyKinds, TypeFamilies, ExplicitForAll,
2 TemplateHaskell, UndecidableInstances, ScopedTypeVariables,
3 TypeInType #-}
4
5 module KindEqualities2 where
6
7 import Data.Kind
8 import GHC.Exts ( Any )
9
10 data Kind = Star | Arr Kind Kind
11
12 data Ty :: Kind -> * where
13 TInt :: Ty Star
14 TBool :: Ty Star
15 TMaybe :: Ty (Arr Star Star)
16 TApp :: Ty (Arr k1 k2) -> Ty k1 -> Ty k2
17
18
19 data TyRep (k :: Kind) (t :: Ty k) where
20 TyInt :: TyRep Star TInt
21 TyBool :: TyRep Star TBool
22 TyMaybe :: TyRep (Arr Star Star) TMaybe
23 TyApp :: TyRep (Arr k1 k2) a -> TyRep k1 b -> TyRep k2 (TApp a b)
24
25 type family IK (k :: Kind)
26 type instance IK Star = *
27 type instance IK (Arr k1 k2) = IK k1 -> IK k2
28
29 $(return []) -- necessary because the following instances depend on the
30 -- previous ones.
31
32 type family I (t :: Ty k) :: IK k
33 type instance I TInt = Int
34 type instance I TBool = Bool
35 type instance I TMaybe = Maybe
36 type instance I (TApp a b) = (I a) (I b)
37
38 zero :: forall (a :: Ty 'Star). TyRep Star a -> I a
39 zero TyInt = 0
40 zero TyBool = False
41 zero (TyApp TyMaybe TyInt) = Nothing
42
43 main = print $ zero (TyApp TyMaybe TyInt)