blob: 1caa46f7c3fbc1adecfa214be14d2b41ea69eaf2 (
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
|
{-# LANGUAGE PolyKinds, GADTs, ExplicitForAll #-}
{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
module KindEqualities where
import Data.Kind
data TyRep1 :: * -> * where
TyInt1 :: TyRep1 Int
TyBool1 :: TyRep1 Bool
zero1 :: forall a. TyRep1 a -> a
zero1 TyInt1 = 0
zero1 TyBool1 = False
data Proxy (a :: k) = P
data TyRep :: forall k. k -> * where
TyInt :: TyRep Int
TyBool :: TyRep Bool
TyMaybe :: TyRep Maybe
TyApp :: TyRep a -> TyRep b -> TyRep (a b)
zero :: forall (a :: *). TyRep a -> a
zero TyInt = 0
zero TyBool = False
zero (TyApp TyMaybe _) = Nothing
|
