1 files changed, 63 insertions, 0 deletions
diff --git a/testsuite/tests/dependent/should_compile/RaeBlogPost.hs b/testsuite/tests/dependent/should_compile/RaeBlogPost.hs
new file mode 100644
index 0000000000..e99c7b5dd5
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/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 = (* :: (* :: (* :: *)))