Test Trac #6049, #6093, #6129, #6137

6 files changed, 69 insertions, 0 deletions

diff --git a/testsuite/tests/polykinds/T6049.hs b/testsuite/tests/polykinds/T6049.hs
new file mode 100644
index 0000000000..51e5958fa9
--- /dev/null
+++ b/testsuite/tests/polykinds/T6049.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE DataKinds, KindSignatures, PolyKinds, GADTs,  ExistentialQuantification #-}
+
+module T6049 where
+
+data SMaybe :: (k -> *) -> Maybe k -> * where
+   SNothing :: forall (s :: k -> *). SMaybe s Nothing
+   SJust :: forall (s :: k -> *) (a :: k). SMaybe s (Just a)
+
diff --git a/testsuite/tests/polykinds/T6093.hs b/testsuite/tests/polykinds/T6093.hs
new file mode 100644
index 0000000000..3fdeb207f8
--- /dev/null
+++ b/testsuite/tests/polykinds/T6093.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE GADTs, PolyKinds #-}
+module T6093 where
+
+-- Polymorphic kind recursion
+data R :: k -> * where
+    MkR :: R f -> R (f ())
+
+
+data IOWitness (a :: k) = IOW
+
+data Type :: k -> * where
+  SimpleType :: IOWitness a -> Type a
+  ConstructedType :: Type f -> Type a -> Type (f a)
diff --git a/testsuite/tests/polykinds/T6129.hs b/testsuite/tests/polykinds/T6129.hs
new file mode 100644
index 0000000000..2f163de192
--- /dev/null
+++ b/testsuite/tests/polykinds/T6129.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE GADTs        #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE PolyKinds    #-}
+{-# LANGUAGE DataKinds    #-}
+
+module T6129 where
+
+data family D a
+data instance D a = DInt
+
+data X a where
+  X1 :: X DInt
diff --git a/testsuite/tests/polykinds/T6129.stderr b/testsuite/tests/polykinds/T6129.stderr
new file mode 100644
index 0000000000..0a27e0e4d3
--- /dev/null
+++ b/testsuite/tests/polykinds/T6129.stderr
@@ -0,0 +1,7 @@
+
+T6129.hs:12:11:
+    You can't use data constructor `DInt' here
+      (it comes from a data family instance)
+    In the type `X DInt'
+    In the definition of data constructor `X1'
+    In the data declaration for `X'
diff --git a/testsuite/tests/polykinds/T6137.hs b/testsuite/tests/polykinds/T6137.hs
new file mode 100644
index 0000000000..dafe9a21e9
--- /dev/null
+++ b/testsuite/tests/polykinds/T6137.hs
@@ -0,0 +1,25 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE GADTs #-}
+
+module T6137 where
+
+data Sum a b = L a | R b
+
+data Sum1 (a :: k1 -> *) (b :: k2 -> *) :: Sum k1 k2 -> * where
+  LL :: a i -> Sum1 a b (L i)
+  RR :: b i -> Sum1 a b (R i)
+
+data Code i o = F (Code (Sum i o) o)
+
+-- An interpretation for `Code` using a data family works:
+data family In (f :: Code i o) :: (i -> *) -> (o -> *)
+
+data instance In (F f) r o where
+  MkIn :: In f (Sum1 r (In (F f) r)) o -> In (F f) r o
+
+-- Requires polymorphic recursion
+data In' (f :: Code i o) :: (i -> *) -> o -> * where
+  MkIn' :: In' g (Sum1 r (In' (F g) r)) t -> In' (F g) r t
diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index 2261fdacff..bec2cc11c5 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -50,3 +50,7 @@ test('T6015a', normal, compile, [''])
 test('T6068', normal, ghci_script, ['T6068.script'])
 test('RedBlack', normal, compile, [''])
 test('T6118', normal, compile,[''])
+test('T6137', normal, compile,[''])
+test('T6093', normal, compile,[''])
+test('T6049', normal, compile,[''])
+test('T6129', normal, compile_fail,[''])