e99c7b5dd58e8fe4dd06cb350f2b9827138a40e6
[ghc.git] / testsuite / tests / dependent / should_compile / RaeBlogPost.hs
1 {-# LANGUAGE DataKinds, PolyKinds, GADTs, TypeOperators, TypeFamilies,
2 TypeInType #-}
3 {-# OPTIONS_GHC -fwarn-unticked-promoted-constructors #-}
4
5 module RaeBlogPost where
6
7 import Data.Kind
8
9 -- a Proxy type with an explicit kind
10 data Proxy k (a :: k) = P
11 prox :: Proxy * Bool
12 prox = P
13
14 prox2 :: Proxy Bool 'True
15 prox2 = P
16
17 -- implicit kinds still work
18 data A
19 data B :: A -> *
20 data C :: B a -> *
21 data D :: C b -> *
22 data E :: D c -> *
23 -- note that E :: forall (a :: A) (b :: B a) (c :: C b). D c -> *
24
25 -- a kind-indexed GADT
26 data TypeRep (a :: k) where
27 TInt :: TypeRep Int
28 TMaybe :: TypeRep Maybe
29 TApp :: TypeRep a -> TypeRep b -> TypeRep (a b)
30
31 zero :: TypeRep a -> a
32 zero TInt = 0
33 zero (TApp TMaybe _) = Nothing
34
35 data Nat = Zero | Succ Nat
36 type family a + b where
37 'Zero + b = b
38 ('Succ a) + b = 'Succ (a + b)
39
40 data Vec :: * -> Nat -> * where
41 Nil :: Vec a 'Zero
42 (:>) :: a -> Vec a n -> Vec a ('Succ n)
43 infixr 5 :>
44
45 -- promoted GADT, and using + as a "kind family":
46 type family (x :: Vec a n) ++ (y :: Vec a m) :: Vec a (n + m) where
47 'Nil ++ y = y
48 (h ':> t) ++ y = h ':> (t ++ y)
49
50 -- datatype that mentions *
51 data U = Star (*)
52 | Bool Bool
53
54 -- kind synonym
55 type Monadish = * -> *
56 class MonadTrans (t :: Monadish -> Monadish) where
57 lift :: Monad m => m a -> t m a
58 data Free :: Monadish where
59 Return :: a -> Free a
60 Bind :: Free a -> (a -> Free b) -> Free b
61
62 -- yes, * really does have type *.
63 type Star = (* :: (* :: (* :: *)))