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

11 files changed, 212 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', ''])
diff --git a/testsuite/tests/indexed-types/should_fail/T13877.hs b/testsuite/tests/indexed-types/should_fail/T13877.hs
new file mode 100644
index 0000000000..ee5f16b1f3
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T13877.hs
@@ -0,0 +1,74 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE Trustworthy #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+module T13877 where
+
+import Data.Kind
+
+data family Sing (a :: k)
+data instance Sing (z :: [a]) where
+  SNil  :: Sing '[]
+  SCons :: Sing x -> Sing xs -> Sing (x:xs)
+
+data TyFun :: * -> * -> *
+type a ~> b = TyFun a b -> *
+infixr 0 ~>
+
+type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
+type a @@ b = Apply a b
+infixl 9 @@
+
+data FunArrow = (:->) | (:~>)
+
+class FunType (arr :: FunArrow) where
+  type Fun (k1 :: Type) arr (k2 :: Type) :: Type
+
+class FunType arr => AppType (arr :: FunArrow) where
+  type App k1 arr k2 (f :: Fun k1 arr k2) (x :: k1) :: k2
+
+type FunApp arr = (FunType arr, AppType arr)
+
+instance FunType (:->) where
+  type Fun k1 (:->) k2 = k1 -> k2
+
+instance AppType (:->) where
+  type App k1 (:->) k2 (f :: k1 -> k2) x = f x
+
+instance FunType (:~>) where
+  type Fun k1 (:~>) k2 = k1 ~> k2
+
+instance AppType (:~>) where
+  type App k1 (:~>) k2 (f :: k1 ~> k2) x = f @@ x
+
+infixr 0 -?>
+type (-?>) (k1 :: Type) (k2 :: Type) (arr :: FunArrow) = Fun k1 arr k2
+
+listElim :: forall (a :: Type) (p :: [a] -> Type) (l :: [a]).
+            Sing l
+         -> p '[]
+         -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p xs -> p (x:xs))
+         -> p l
+listElim = listElimPoly @(:->) @a @p @l
+
+listElimTyFun :: forall (a :: Type) (p :: [a] ~> Type) (l :: [a]).
+                 Sing l
+              -> p @@ '[]
+              -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p @@ xs -> p @@ (x:xs))
+              -> p @@ l
+listElimTyFun = listElimPoly @(:->) @a @p @l
+
+listElimPoly :: forall (arr :: FunArrow) (a :: Type) (p :: ([a] -?> Type) arr) (l :: [a]).
+                FunApp arr
+             => Sing l
+             -> App [a] arr Type p '[]
+             -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> App [a] arr Type p xs -> App [a] arr Type p (x:xs))
+             -> App [a] arr Type p l
+listElimPoly SNil                      pNil _     = pNil
+listElimPoly (SCons x (xs :: Sing xs)) pNil pCons = pCons x xs (listElimPoly @arr @a @p @xs xs pNil pCons)
diff --git a/testsuite/tests/indexed-types/should_fail/T13877.stderr b/testsuite/tests/indexed-types/should_fail/T13877.stderr
new file mode 100644
index 0000000000..4498d97a41
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T13877.stderr
@@ -0,0 +1,31 @@
+
+T13877.hs:65:17: error:
+    • Couldn't match type ‘p xs’ with ‘Apply p xs’
+      Expected type: Sing x
+                     -> Sing xs -> App [a] (':->) * p xs -> App [a] (':->) * p (x : xs)
+        Actual type: Sing x -> Sing xs -> (p @@ xs) -> p @@ (x : xs)
+    • In the expression: listElimPoly @(:->) @a @p @l
+      In an equation for ‘listElimTyFun’:
+          listElimTyFun = listElimPoly @(:->) @a @p @l
+    • Relevant bindings include
+        listElimTyFun :: Sing l
+                         -> (p @@ '[])
+                         -> (forall (x :: a) (xs :: [a]).
+                             Sing x -> Sing xs -> (p @@ xs) -> p @@ (x : xs))
+                         -> p @@ l
+          (bound at T13877.hs:65:1)
+
+T13877.hs:65:41: error:
+    • Expecting one more argument to ‘p’
+      Expected kind ‘(-?>) [a] * (':->)’, but ‘p’ has kind ‘[a] ~> *’
+    • In the type ‘p’
+      In the expression: listElimPoly @(:->) @a @p @l
+      In an equation for ‘listElimTyFun’:
+          listElimTyFun = listElimPoly @(:->) @a @p @l
+    • Relevant bindings include
+        listElimTyFun :: Sing l
+                         -> (p @@ '[])
+                         -> (forall (x :: a) (xs :: [a]).
+                             Sing x -> Sing xs -> (p @@ xs) -> p @@ (x : xs))
+                         -> p @@ l
+          (bound at T13877.hs:65:1)
diff --git a/testsuite/tests/indexed-types/should_fail/all.T b/testsuite/tests/indexed-types/should_fail/all.T
index 88859338d1..c1d308fbe4 100644
--- a/testsuite/tests/indexed-types/should_fail/all.T
+++ b/testsuite/tests/indexed-types/should_fail/all.T
@@ -135,4 +135,5 @@ test('T7102a', normal, ghci_script, ['T7102a.script'])
 test('T13271', normal, compile_fail, [''])
 test('T13674', normal, compile_fail, [''])
 test('T13784', normal, compile_fail, [''])
+test('T13877', normal, compile_fail, [''])
 test('T14033', normal, compile_fail, [''])