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