summaryrefslogtreecommitdiff
path: root/tests/examples/pre-ghc86/RaeBlogPost.hs
diff options
context:
space:
mode:
Diffstat (limited to 'tests/examples/pre-ghc86/RaeBlogPost.hs')
-rw-r--r--tests/examples/pre-ghc86/RaeBlogPost.hs63
1 files changed, 63 insertions, 0 deletions
diff --git a/tests/examples/pre-ghc86/RaeBlogPost.hs b/tests/examples/pre-ghc86/RaeBlogPost.hs
new file mode 100644
index 0000000..e99c7b5
--- /dev/null
+++ b/tests/examples/pre-ghc86/RaeBlogPost.hs
@@ -0,0 +1,63 @@
+{-# LANGUAGE DataKinds, PolyKinds, GADTs, TypeOperators, TypeFamilies,
+ TypeInType #-}
+{-# OPTIONS_GHC -fwarn-unticked-promoted-constructors #-}
+
+module RaeBlogPost where
+
+import Data.Kind
+
+-- a Proxy type with an explicit kind
+data Proxy k (a :: k) = P
+prox :: Proxy * Bool
+prox = P
+
+prox2 :: Proxy Bool 'True
+prox2 = P
+
+-- implicit kinds still work
+data A
+data B :: A -> *
+data C :: B a -> *
+data D :: C b -> *
+data E :: D c -> *
+-- note that E :: forall (a :: A) (b :: B a) (c :: C b). D c -> *
+
+-- a kind-indexed GADT
+data TypeRep (a :: k) where
+ TInt :: TypeRep Int
+ TMaybe :: TypeRep Maybe
+ TApp :: TypeRep a -> TypeRep b -> TypeRep (a b)
+
+zero :: TypeRep a -> a
+zero TInt = 0
+zero (TApp TMaybe _) = Nothing
+
+data Nat = Zero | Succ Nat
+type family a + b where
+ 'Zero + b = b
+ ('Succ a) + b = 'Succ (a + b)
+
+data Vec :: * -> Nat -> * where
+ Nil :: Vec a 'Zero
+ (:>) :: a -> Vec a n -> Vec a ('Succ n)
+infixr 5 :>
+
+-- promoted GADT, and using + as a "kind family":
+type family (x :: Vec a n) ++ (y :: Vec a m) :: Vec a (n + m) where
+ 'Nil ++ y = y
+ (h ':> t) ++ y = h ':> (t ++ y)
+
+-- datatype that mentions *
+data U = Star (*)
+ | Bool Bool
+
+-- kind synonym
+type Monadish = * -> *
+class MonadTrans (t :: Monadish -> Monadish) where
+ lift :: Monad m => m a -> t m a
+data Free :: Monadish where
+ Return :: a -> Free a
+ Bind :: Free a -> (a -> Free b) -> Free b
+
+-- yes, * really does have type *.
+type Star = (* :: (* :: (* :: *)))