1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
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)
|
