[commit: testsuite] master: Test Trac #6049, #6093, #6129, #6137 (f7a5b4c)

[Simon Peyton Jones]

Repository : ssh://darcs.haskell.org//srv/darcs/testsuite

On branch  : master

http://hackage.haskell.org/trac/ghc/changeset/f7a5b4ce9ab3efced15f374cd7a97eba4a9ab53b

>---------------------------------------------------------------

commit f7a5b4ce9ab3efced15f374cd7a97eba4a9ab53b
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date:   Thu Jun 7 14:07:56 2012 +0100

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

>---------------------------------------------------------------

 tests/polykinds/T6049.hs     |    8 ++++++++
 tests/polykinds/T6093.hs     |   13 +++++++++++++
 tests/polykinds/T6129.hs     |   12 ++++++++++++
 tests/polykinds/T6129.stderr |    7 +++++++
 tests/polykinds/T6137.hs     |   25 +++++++++++++++++++++++++
 tests/polykinds/all.T        |    4 ++++
 6 files changed, 69 insertions(+), 0 deletions(-)

diff --git a/tests/polykinds/T6049.hs b/tests/polykinds/T6049.hs
new file mode 100644
index 0000000..51e5958
--- /dev/null
+++ b/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/tests/polykinds/T6093.hs b/tests/polykinds/T6093.hs
new file mode 100644
index 0000000..3fdeb20
--- /dev/null
+++ b/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/tests/polykinds/T6129.hs b/tests/polykinds/T6129.hs
new file mode 100644
index 0000000..2f163de
--- /dev/null
+++ b/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/tests/polykinds/T6129.stderr b/tests/polykinds/T6129.stderr
new file mode 100644
index 0000000..0a27e0e
--- /dev/null
+++ b/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/tests/polykinds/T6137.hs b/tests/polykinds/T6137.hs
new file mode 100644
index 0000000..dafe9a2
--- /dev/null
+++ b/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/tests/polykinds/all.T b/tests/polykinds/all.T
index 2261fda..bec2cc1 100644
--- a/tests/polykinds/all.T
+++ b/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,[''])