summaryrefslogtreecommitdiff
path: root/tests/examples/ghc80/KindEqualities2.hs
blob: 5a6f60d40b36d953f2917417add155c652fb2373 (plain)
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)