implement proposal 106 (Define Kinds Without Promotion) (fixes #6024)

includes corresponding changes to haddock submodule

35 files changed, 198 insertions, 0 deletions

diff --git a/testsuite/tests/type-data/Makefile b/testsuite/tests/type-data/Makefile
new file mode 100644
index 0000000000..9a36a1c5fe
--- /dev/null
+++ b/testsuite/tests/type-data/Makefile
@@ -0,0 +1,3 @@
+TOP=../..
+include $(TOP)/mk/boilerplate.mk
+include $(TOP)/mk/test.mk
diff --git a/testsuite/tests/type-data/should_compile/Makefile b/testsuite/tests/type-data/should_compile/Makefile
new file mode 100644
index 0000000000..9101fbd40a
--- /dev/null
+++ b/testsuite/tests/type-data/should_compile/Makefile
@@ -0,0 +1,3 @@
+TOP=../../..
+include $(TOP)/mk/boilerplate.mk
+include $(TOP)/mk/test.mk
diff --git a/testsuite/tests/type-data/should_compile/TDDataConstructor.hs b/testsuite/tests/type-data/should_compile/TDDataConstructor.hs
new file mode 100644
index 0000000000..8474ec25eb
--- /dev/null
+++ b/testsuite/tests/type-data/should_compile/TDDataConstructor.hs
@@ -0,0 +1,5 @@
+{-# LANGUAGE TypeData #-}
+module TDDataConstructor where
+
+type data P = MkP
+data Prom = P
diff --git a/testsuite/tests/type-data/should_compile/TDExistential.hs b/testsuite/tests/type-data/should_compile/TDExistential.hs
new file mode 100644
index 0000000000..0e9bb04014
--- /dev/null
+++ b/testsuite/tests/type-data/should_compile/TDExistential.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE TypeData #-}
+{-# LANGUAGE TypeFamilies #-}
+module TDExistential where
+
+import Data.Kind (Type)
+
+-- example from GHC User's Guide 6.4.10.6
+
+type data Ex :: Type where
+  MkEx :: forall a. a -> Ex
+
+type family UnEx (ex :: Ex) :: k
+type instance UnEx (MkEx x) = x
diff --git a/testsuite/tests/type-data/should_compile/TDGoodConsConstraints.hs b/testsuite/tests/type-data/should_compile/TDGoodConsConstraints.hs
new file mode 100644
index 0000000000..0b4e006184
--- /dev/null
+++ b/testsuite/tests/type-data/should_compile/TDGoodConsConstraints.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE TypeData #-}
+{-# LANGUAGE GADTs #-}
+module TDGoodConsConstraints where
+
+import Data.Kind (Type)
+import Data.Type.Equality
+
+type data Foo :: Type -> Type where
+  MkFoo1 :: a ~ Int         => Foo a
+  MkFoo2 :: a ~~ Int        => Foo a
diff --git a/testsuite/tests/type-data/should_compile/TDVector.hs b/testsuite/tests/type-data/should_compile/TDVector.hs
new file mode 100644
index 0000000000..753cd97375
--- /dev/null
+++ b/testsuite/tests/type-data/should_compile/TDVector.hs
@@ -0,0 +1,21 @@
+{-# LANGUAGE TypeData #-}
+{-# LANGUAGE MonoLocalBinds #-}
+module TDVector where
+
+import Data.Kind (Type)
+
+type data Nat = Zero | Succ Nat
+
+type data List a = Nil | Cons a (List a)
+
+type data Pair a b = MkPair a b
+
+type data Sum a b = L a | R b
+
+data Vec :: Nat -> Type -> Type where
+    VNil :: Vec Zero a
+    VCons :: a -> Vec n a -> Vec (Succ n) a
+
+instance Functor (Vec n) where
+    fmap _ VNil = VNil
+    fmap f (VCons x xs) = VCons (f x) (fmap f xs)
diff --git a/testsuite/tests/type-data/should_compile/all.T b/testsuite/tests/type-data/should_compile/all.T
new file mode 100644
index 0000000000..0f8294bee7
--- /dev/null
+++ b/testsuite/tests/type-data/should_compile/all.T
@@ -0,0 +1,4 @@
+test('TDDataConstructor', normal, compile, [''])
+test('TDExistential', normal, compile, [''])
+test('TDGoodConsConstraints', normal, compile, [''])
+test('TDVector', normal, compile, [''])
diff --git a/testsuite/tests/type-data/should_fail/Makefile b/testsuite/tests/type-data/should_fail/Makefile
new file mode 100644
index 0000000000..9101fbd40a
--- /dev/null
+++ b/testsuite/tests/type-data/should_fail/Makefile
@@ -0,0 +1,3 @@
+TOP=../../..
+include $(TOP)/mk/boilerplate.mk
+include $(TOP)/mk/test.mk
diff --git a/testsuite/tests/type-data/should_fail/TDBadConsConstraint.hs b/testsuite/tests/type-data/should_fail/TDBadConsConstraint.hs
new file mode 100644
index 0000000000..43a709f516
--- /dev/null
+++ b/testsuite/tests/type-data/should_fail/TDBadConsConstraint.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE TypeData #-}
+{-# LANGUAGE GADTs #-}
+module TDConsConstraints where
+
+import Data.Kind (Type)
+
+type data Foo :: Type -> Type where
+  MkFoo3 :: Show a          => Foo a
diff --git a/testsuite/tests/type-data/should_fail/TDBadConsConstraint.stderr b/testsuite/tests/type-data/should_fail/TDBadConsConstraint.stderr
new file mode 100644
index 0000000000..1e2eddc456
--- /dev/null
+++ b/testsuite/tests/type-data/should_fail/TDBadConsConstraint.stderr
@@ -0,0 +1,5 @@
+
+TDBadConsConstraint.hs:8:3: [GHC-01259]
+     Illegal constraint in a kind: forall a. Show a => Foo a
+     In the definition of data constructor ‘MkFoo3’
+      In the data type declaration for ‘Foo’
diff --git a/testsuite/tests/type-data/should_fail/TDDeriving.hs b/testsuite/tests/type-data/should_fail/TDDeriving.hs
new file mode 100644
index 0000000000..dc804fc532
--- /dev/null
+++ b/testsuite/tests/type-data/should_fail/TDDeriving.hs
@@ -0,0 +1,5 @@
+{-# LANGUAGE TypeData #-}
+module TDDeriving where
+
+type data Nat = Zero | Succ Nat
+    deriving (Eq)
diff --git a/testsuite/tests/type-data/should_fail/TDDeriving.stderr b/testsuite/tests/type-data/should_fail/TDDeriving.stderr
new file mode 100644
index 0000000000..231f2c7df7
--- /dev/null
+++ b/testsuite/tests/type-data/should_fail/TDDeriving.stderr
@@ -0,0 +1,3 @@
+
+TDDeriving.hs:4:1: [GHC-67297]
+    Deriving clauses are not allowed in type data declarations.
diff --git a/testsuite/tests/type-data/should_fail/TDExpression.hs b/testsuite/tests/type-data/should_fail/TDExpression.hs
new file mode 100644
index 0000000000..4f04993459
--- /dev/null
+++ b/testsuite/tests/type-data/should_fail/TDExpression.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE TypeData #-}
+module TDExpression where
+
+type data Nat = Zero | Succ Nat
+
+-- Not in scope: data constructor ‘Zero’
+z = Zero
diff --git a/testsuite/tests/type-data/should_fail/TDExpression.stderr b/testsuite/tests/type-data/should_fail/TDExpression.stderr
new file mode 100644
index 0000000000..354dac183f
--- /dev/null
+++ b/testsuite/tests/type-data/should_fail/TDExpression.stderr
@@ -0,0 +1,6 @@
+
+TDExpression.hs:7:5: [GHC-31891]
+     Illegal term-level use of the type constructor or class ‘Zero’
+     defined at TDExpression.hs:4:17
+     In the expression: Zero
+      In an equation for ‘z’: z = Zero
diff --git a/testsuite/tests/type-data/should_fail/TDMultiple01.hs b/testsuite/tests/type-data/should_fail/TDMultiple01.hs
new file mode 100644
index 0000000000..ead94c4d1d
--- /dev/null
+++ b/testsuite/tests/type-data/should_fail/TDMultiple01.hs
@@ -0,0 +1,5 @@
+{-# LANGUAGE TypeData #-}
+module TDMultiple01 where
+
+data P = MkP
+type data Prom = P -- P is multiply defined
diff --git a/testsuite/tests/type-data/should_fail/TDMultiple01.stderr b/testsuite/tests/type-data/should_fail/TDMultiple01.stderr
new file mode 100644
index 0000000000..5b3abe33ed
--- /dev/null
+++ b/testsuite/tests/type-data/should_fail/TDMultiple01.stderr
@@ -0,0 +1,5 @@
+
+TDMultiple01.hs:5:18:
+    Multiple declarations of ‘P’
+    Declared at: TDMultiple01.hs:4:1
+                 TDMultiple01.hs:5:18
diff --git a/testsuite/tests/type-data/should_fail/TDMultiple02.hs b/testsuite/tests/type-data/should_fail/TDMultiple02.hs
new file mode 100644
index 0000000000..91dcf565f7
--- /dev/null
+++ b/testsuite/tests/type-data/should_fail/TDMultiple02.hs
@@ -0,0 +1,5 @@
+{-# LANGUAGE TypeData #-}
+module TDMultiple02 where
+
+type data P = MkP
+type data Prom = P -- type P is multiply defined
diff --git a/testsuite/tests/type-data/should_fail/TDMultiple02.stderr b/testsuite/tests/type-data/should_fail/TDMultiple02.stderr
new file mode 100644
index 0000000000..c08709fa8c
--- /dev/null
+++ b/testsuite/tests/type-data/should_fail/TDMultiple02.stderr
@@ -0,0 +1,5 @@
+
+TDMultiple02.hs:5:18:
+    Multiple declarations of ‘P’
+    Declared at: TDMultiple02.hs:4:1
+                 TDMultiple02.hs:5:18
diff --git a/testsuite/tests/type-data/should_fail/TDNoPragma.hs b/testsuite/tests/type-data/should_fail/TDNoPragma.hs
new file mode 100644
index 0000000000..a1b5386f62
--- /dev/null
+++ b/testsuite/tests/type-data/should_fail/TDNoPragma.hs
@@ -0,0 +1,4 @@
+module TDNoPragma where
+
+-- requires LANGUAGE TypeData
+type data Nat = Zero | Succ Nat
diff --git a/testsuite/tests/type-data/should_fail/TDNoPragma.stderr b/testsuite/tests/type-data/should_fail/TDNoPragma.stderr
new file mode 100644
index 0000000000..62b47da4d1
--- /dev/null
+++ b/testsuite/tests/type-data/should_fail/TDNoPragma.stderr
@@ -0,0 +1,4 @@
+
+TDNoPragma.hs:4:1: [GHC-15013]
+    Illegal type-level data declaration
+    Suggested fix: Perhaps you intended to use TypeData
diff --git a/testsuite/tests/type-data/should_fail/TDPattern.hs b/testsuite/tests/type-data/should_fail/TDPattern.hs
new file mode 100644
index 0000000000..abcf65de24
--- /dev/null
+++ b/testsuite/tests/type-data/should_fail/TDPattern.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE TypeData #-}
+module TDPattern where
+
+type data Nat = Zero | Succ Nat
+
+-- Zero is not a data constructor
+f Zero = 0
diff --git a/testsuite/tests/type-data/should_fail/TDPattern.stderr b/testsuite/tests/type-data/should_fail/TDPattern.stderr
new file mode 100644
index 0000000000..3fecbb1f6b
--- /dev/null
+++ b/testsuite/tests/type-data/should_fail/TDPattern.stderr
@@ -0,0 +1,3 @@
+
+TDPattern.hs:7:3: [GHC-76037]
+    Not in scope: data constructor ‘Zero’
diff --git a/testsuite/tests/type-data/should_fail/TDPunning.hs b/testsuite/tests/type-data/should_fail/TDPunning.hs
new file mode 100644
index 0000000000..0560009ce8
--- /dev/null
+++ b/testsuite/tests/type-data/should_fail/TDPunning.hs
@@ -0,0 +1,4 @@
+{-# LANGUAGE TypeData #-}
+module TDPunning where
+
+type data T = T -- type T is multiply defined
diff --git a/testsuite/tests/type-data/should_fail/TDPunning.stderr b/testsuite/tests/type-data/should_fail/TDPunning.stderr
new file mode 100644
index 0000000000..95ddbf51d3
--- /dev/null
+++ b/testsuite/tests/type-data/should_fail/TDPunning.stderr
@@ -0,0 +1,5 @@
+
+TDPunning.hs:4:15:
+    Multiple declarations of ‘T’
+    Declared at: TDPunning.hs:4:1
+                 TDPunning.hs:4:15
diff --git a/testsuite/tests/type-data/should_fail/TDRecordsGADT.hs b/testsuite/tests/type-data/should_fail/TDRecordsGADT.hs
new file mode 100644
index 0000000000..0d9e6536c3
--- /dev/null
+++ b/testsuite/tests/type-data/should_fail/TDRecordsGADT.hs
@@ -0,0 +1,6 @@
+{-# LANGUAGE TypeData #-}
+{-# LANGUAGE GADTs #-}
+module TDRecordsGADT where
+
+type data Record a where
+    Cons :: { field :: a } -> Record a
diff --git a/testsuite/tests/type-data/should_fail/TDRecordsGADT.stderr b/testsuite/tests/type-data/should_fail/TDRecordsGADT.stderr
new file mode 100644
index 0000000000..8695163190
--- /dev/null
+++ b/testsuite/tests/type-data/should_fail/TDRecordsGADT.stderr
@@ -0,0 +1,3 @@
+
+TDRecordsGADT.hs:6:5: [GHC-67297]
+    Labelled fields are not allowed in type data declarations.
diff --git a/testsuite/tests/type-data/should_fail/TDRecordsH98.hs b/testsuite/tests/type-data/should_fail/TDRecordsH98.hs
new file mode 100644
index 0000000000..d6d805532f
--- /dev/null
+++ b/testsuite/tests/type-data/should_fail/TDRecordsH98.hs
@@ -0,0 +1,4 @@
+{-# LANGUAGE TypeData #-}
+module TDRecordsH98 where
+
+type data Record a = Cons { field :: a }
diff --git a/testsuite/tests/type-data/should_fail/TDRecordsH98.stderr b/testsuite/tests/type-data/should_fail/TDRecordsH98.stderr
new file mode 100644
index 0000000000..c20a83dc73
--- /dev/null
+++ b/testsuite/tests/type-data/should_fail/TDRecordsH98.stderr
@@ -0,0 +1,3 @@
+
+TDRecordsH98.hs:4:22: [GHC-67297]
+    Labelled fields are not allowed in type data declarations.
diff --git a/testsuite/tests/type-data/should_fail/TDRecursive.hs b/testsuite/tests/type-data/should_fail/TDRecursive.hs
new file mode 100644
index 0000000000..b4a09c165e
--- /dev/null
+++ b/testsuite/tests/type-data/should_fail/TDRecursive.hs
@@ -0,0 +1,4 @@
+{-# LANGUAGE TypeData #-}
+module TDRecursive where
+
+type data T f = K (f (K Int))
diff --git a/testsuite/tests/type-data/should_fail/TDRecursive.stderr b/testsuite/tests/type-data/should_fail/TDRecursive.stderr
new file mode 100644
index 0000000000..8225bd1790
--- /dev/null
+++ b/testsuite/tests/type-data/should_fail/TDRecursive.stderr
@@ -0,0 +1,7 @@
+
+TDRecursive.hs:4:23: [GHC-88634]
+     Type constructor ‘K’ cannot be used here
+        (it is defined and used in the same recursive group)
+     In the first argument of ‘f’, namely ‘(K Int)’
+      In the type ‘(f (K Int))’
+      In the definition of data constructor ‘K’
diff --git a/testsuite/tests/type-data/should_fail/TDStrictnessGADT.hs b/testsuite/tests/type-data/should_fail/TDStrictnessGADT.hs
new file mode 100644
index 0000000000..774c560e30
--- /dev/null
+++ b/testsuite/tests/type-data/should_fail/TDStrictnessGADT.hs
@@ -0,0 +1,5 @@
+{-# LANGUAGE TypeData #-}
+module TDStrictnessGADT where
+
+type data T a where
+     Cons :: !a -> T a
diff --git a/testsuite/tests/type-data/should_fail/TDStrictnessGADT.stderr b/testsuite/tests/type-data/should_fail/TDStrictnessGADT.stderr
new file mode 100644
index 0000000000..db235cd048
--- /dev/null
+++ b/testsuite/tests/type-data/should_fail/TDStrictnessGADT.stderr
@@ -0,0 +1,3 @@
+
+TDStrictnessGADT.hs:5:6: [GHC-67297]
+    Strictness flags are not allowed in type data declarations.
diff --git a/testsuite/tests/type-data/should_fail/TDStrictnessH98.hs b/testsuite/tests/type-data/should_fail/TDStrictnessH98.hs
new file mode 100644
index 0000000000..062df5bd02
--- /dev/null
+++ b/testsuite/tests/type-data/should_fail/TDStrictnessH98.hs
@@ -0,0 +1,4 @@
+{-# LANGUAGE TypeData #-}
+module TDStrictnessH98 where
+
+type data T a = Cons !a
diff --git a/testsuite/tests/type-data/should_fail/TDStrictnessH98.stderr b/testsuite/tests/type-data/should_fail/TDStrictnessH98.stderr
new file mode 100644
index 0000000000..e0ccd5e456
--- /dev/null
+++ b/testsuite/tests/type-data/should_fail/TDStrictnessH98.stderr
@@ -0,0 +1,3 @@
+
+TDStrictnessH98.hs:4:17: [GHC-67297]
+    Strictness flags are not allowed in type data declarations.
diff --git a/testsuite/tests/type-data/should_fail/all.T b/testsuite/tests/type-data/should_fail/all.T
new file mode 100644
index 0000000000..ddf7bd86bd
--- /dev/null
+++ b/testsuite/tests/type-data/should_fail/all.T
@@ -0,0 +1,13 @@
+test('TDNoPragma', normal, compile_fail, [''])
+test('TDBadConsConstraint', normal, compile_fail, [''])
+test('TDDeriving', normal, compile_fail, [''])
+test('TDExpression', normal, compile_fail, [''])
+test('TDMultiple01', normal, compile_fail, [''])
+test('TDMultiple02', normal, compile_fail, [''])
+test('TDPattern', normal, compile_fail, [''])
+test('TDPunning', normal, compile_fail, [''])
+test('TDRecordsGADT', normal, compile_fail, [''])
+test('TDRecordsH98', normal, compile_fail, [''])
+test('TDRecursive', normal, compile_fail, [''])
+test('TDStrictnessGADT', normal, compile_fail, [''])
+test('TDStrictnessH98', normal, compile_fail, [''])