Add regression tests for #13601, #13780, #13877

Summary:
Some recent commits happened to fix other issues:

* c2417b87ff59c92fbfa8eceeff2a0d6152b11a47 fixed #13601 and #13780
* 8e15e3d370e9c253ae0dbb330e25b72cb00cdb76 fixed the original program in #13877

Let's add regression tests for each of these to ensure they stay fixed.

Test Plan: make test TEST="T13601 T13780a T13780c T13877"

Reviewers: goldfire, bgamari, austin

Reviewed By: bgamari

Subscribers: rwbarton, thomie

GHC Trac Issues: #13601, #13780, #13877

Differential Revision: https://phabricator.haskell.org/D3794

8 files changed, 106 insertions, 0 deletions

diff --git a/testsuite/tests/dependent/should_fail/T13601.hs b/testsuite/tests/dependent/should_fail/T13601.hs
new file mode 100644
index 0000000000..5e98c7a657
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T13601.hs
@@ -0,0 +1,47 @@
+{-# LANGUAGE TypeFamilies, DataKinds, TypeInType #-}
+
+import GHC.Exts
+import Prelude (Bool(True,False),Integer,Ordering,undefined)
+import qualified Prelude
+import Data.Kind
+
+--------------------
+-- class hierarchy
+
+type family
+  Rep (rep :: RuntimeRep) :: RuntimeRep where
+  -- Rep IntRep         = IntRep
+  -- Rep DoubleRep      = IntRep
+  -- Rep PtrRepUnlifted = IntRep
+  -- Rep PtrRepLifted   = PtrRepLifted
+
+class Boolean (Logic a) => Eq (a :: TYPE rep) where
+  type Logic (a :: TYPE rep) :: TYPE (Rep rep)
+  (==) :: a -> a -> Logic a
+
+class Eq a => POrd (a :: TYPE rep) where
+  inf :: a -> a -> a
+
+class POrd a => MinBound (a :: TYPE rep) where
+  minBound :: () -> a
+
+class POrd a => Lattice (a :: TYPE rep) where
+  sup :: a -> a -> a
+
+class (Lattice a, MinBound a) => Bounded (a :: TYPE rep) where
+  maxBound :: () -> a
+
+class Bounded a => Complemented (a :: TYPE rep) where
+  not :: a -> a
+
+class Bounded a => Heyting (a :: TYPE rep) where
+  infixr 3 ==>
+  (==>) :: a -> a -> a
+
+class (Complemented a, Heyting a) => Boolean a
+
+(||) :: Boolean a => a -> a -> a
+(||) = sup
+
+(&&) :: Boolean a => a -> a -> a
+(&&) = inf
diff --git a/testsuite/tests/dependent/should_fail/T13601.stderr b/testsuite/tests/dependent/should_fail/T13601.stderr
new file mode 100644
index 0000000000..c1c9803e5a
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T13601.stderr
@@ -0,0 +1,6 @@
+
+T13601.hs:18:16: error:
+    • Expected kind ‘TYPE (Rep 'LiftedRep)’,
+        but ‘Logic a’ has kind ‘TYPE (Rep rep)’
+    • In the first argument of ‘Boolean’, namely ‘(Logic a)’
+      In the class declaration for ‘Eq’
diff --git a/testsuite/tests/dependent/should_fail/T13780a.hs b/testsuite/tests/dependent/should_fail/T13780a.hs
new file mode 100644
index 0000000000..1f7c95c40a
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T13780a.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+module T13780a where
+
+data family Sing (a :: k)
+
+data Foo a = a ~ Bool => MkFoo
+data instance Sing (z :: Foo a) = (z ~ MkFoo) => SMkFoo
diff --git a/testsuite/tests/dependent/should_fail/T13780a.stderr b/testsuite/tests/dependent/should_fail/T13780a.stderr
new file mode 100644
index 0000000000..3b113bd89e
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T13780a.stderr
@@ -0,0 +1,6 @@
+
+T13780a.hs:9:40: error:
+    • Expected kind ‘Foo a’, but ‘MkFoo’ has kind ‘Foo Bool’
+    • In the second argument of ‘(~)’, namely ‘MkFoo’
+      In the definition of data constructor ‘SMkFoo’
+      In the data instance declaration for ‘Sing’
diff --git a/testsuite/tests/dependent/should_fail/T13780b.hs b/testsuite/tests/dependent/should_fail/T13780b.hs
new file mode 100644
index 0000000000..238e7a1af9
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T13780b.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+module T13780b where
+
+data family Sing (a :: k)
+
+data instance Sing (z :: Bool) =
+    z ~ False => SFalse
+  | z ~ True  => STrue
diff --git a/testsuite/tests/dependent/should_fail/T13780c.hs b/testsuite/tests/dependent/should_fail/T13780c.hs
new file mode 100644
index 0000000000..eee6436237
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T13780c.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+module T13780c where
+
+import Data.Kind
+import T13780b
+
+type family ElimBool (p :: Bool -> Type) (b :: Bool) (s :: Sing b)
+                     (pFalse :: p False) (pTrue :: p True) :: p b where
+  ElimBool _ _ SFalse pFalse _ = pFalse
+  ElimBool _ _ STrue  _ pTrue  = pTrue
diff --git a/testsuite/tests/dependent/should_fail/T13780c.stderr b/testsuite/tests/dependent/should_fail/T13780c.stderr
new file mode 100644
index 0000000000..f91d7a3236
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T13780c.stderr
@@ -0,0 +1,12 @@
+[1 of 2] Compiling T13780b          ( T13780b.hs, T13780b.o )
+[2 of 2] Compiling T13780c          ( T13780c.hs, T13780c.o )
+
+T13780c.hs:11:16: error:
+    • Expected kind ‘Sing _’, but ‘SFalse’ has kind ‘Sing 'False’
+    • In the third argument of ‘ElimBool’, namely ‘SFalse’
+      In the type family declaration for ‘ElimBool’
+
+T13780c.hs:12:16: error:
+    • Expected kind ‘Sing _1’, but ‘STrue’ has kind ‘Sing 'True’
+    • In the third argument of ‘ElimBool’, namely ‘STrue’
+      In the type family declaration for ‘ElimBool’
diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T
index af3efc6716..4eb426419d 100644
--- a/testsuite/tests/dependent/should_fail/all.T
+++ b/testsuite/tests/dependent/should_fail/all.T
@@ -17,3 +17,7 @@ test('T11471', normal, compile_fail, [''])
 test('T12174', normal, compile_fail, [''])
 test('T12081', normal, compile_fail, [''])
 test('T13135', normal, compile_fail, [''])
+test('T13601', normal, compile_fail, [''])
+test('T13780a', normal, compile_fail, [''])
+test('T13780c', [extra_files(['T13780b.hs'])],
+                multimod_compile_fail, ['T13780c', ''])