Test Trac #7224 and #7230

5 files changed, 89 insertions, 1 deletions

diff --git a/testsuite/tests/polykinds/T7224.hs b/testsuite/tests/polykinds/T7224.hs
new file mode 100644
index 0000000000..a065bc8494
--- /dev/null
+++ b/testsuite/tests/polykinds/T7224.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE PolyKinds #-}
+
+module T7224 where
+
+class PMonad' (m :: i -> i -> * -> *) where
+  ret'  :: a -> m i i a
+  bind' :: m i j a -> (a -> m j k b) -> m i k b
diff --git a/testsuite/tests/polykinds/T7224.stderr b/testsuite/tests/polykinds/T7224.stderr
new file mode 100644
index 0000000000..c1508e9b7d
--- /dev/null
+++ b/testsuite/tests/polykinds/T7224.stderr
@@ -0,0 +1,5 @@
+
+T7224.hs:6:19:
+    Kind variable `i' used as a type
+    In the type `a -> m i i a'
+    In the class declaration for PMonad'
diff --git a/testsuite/tests/polykinds/T7230.hs b/testsuite/tests/polykinds/T7230.hs
new file mode 100644
index 0000000000..d3c6a51ae5
--- /dev/null
+++ b/testsuite/tests/polykinds/T7230.hs
@@ -0,0 +1,49 @@
+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
+{-# LANGUAGE DataKinds, PolyKinds, GADTs, TypeFamilies #-}
+{-# LANGUAGE TypeOperators, UndecidableInstances #-}
+module T7230 where
+
+data Nat = Zero | Succ Nat deriving (Show, Eq, Ord)
+
+data family Sing (x :: k)
+
+data instance Sing (n :: Nat) where
+  SZero :: Sing Zero
+  SSucc :: Sing n -> Sing (Succ n)
+
+type SNat (n :: Nat) = Sing n
+
+data instance Sing (b :: Bool) where
+  STrue  :: Sing True
+  SFalse :: Sing False
+
+type SBool (b :: Bool) = Sing b
+
+data instance Sing (xs :: [k]) where
+  SNil  :: Sing ('[] :: [k])
+  SCons :: Sing x -> Sing xs -> Sing (x ': xs)
+
+type SList (xs :: [k]) = Sing (xs :: [k])
+
+type family (:<<=) (n :: Nat) (m :: Nat) :: Bool
+type instance Zero   :<<= n      = True
+type instance Succ n :<<= Zero   = False
+type instance Succ n :<<= Succ m = n :<<= m
+
+(%:<<=) :: SNat n -> SNat m -> SBool (n :<<= m)
+SZero   %:<<= _       = STrue
+SSucc _ %:<<= SZero   = SFalse
+SSucc n %:<<= SSucc m = n %:<<= m
+
+type family   (b :: Bool) :&& (b' :: Bool) :: Bool
+type instance True  :&& b = b
+type instance False :&& b = False
+
+type family   Increasing (xs :: [Nat]) :: Bool
+type instance Increasing '[]  = True
+type instance Increasing '[n] = True
+type instance Increasing (n ': m ': ns) = n :<<= m :&& Increasing (m ': ns)
+
+crash :: (Increasing xs) ~ True => SList xs -> SBool (Increasing xs)
+crash (SCons x (SCons y xs)) = x %:<<= y
+crash _                      = STrue
diff --git a/testsuite/tests/polykinds/T7230.stderr b/testsuite/tests/polykinds/T7230.stderr
new file mode 100644
index 0000000000..ee82a2bb19
--- /dev/null
+++ b/testsuite/tests/polykinds/T7230.stderr
@@ -0,0 +1,25 @@
+
+T7230.hs:48:32:
+    Could not deduce ((x :<<= x1) ~ 'True)
+    from the context (Increasing xs ~ 'True)
+      bound by the type signature for
+                 crash :: Increasing xs ~ 'True =>
+                          SList Nat xs -> SBool (Increasing xs)
+      at T7230.hs:47:10-68
+    or from (xs ~ (':) Nat x xs1)
+      bound by a pattern with constructor
+                 SCons :: forall (k :: BOX) (x :: k) (xs :: [k]).
+                          Sing k x -> Sing [k] xs -> Sing [k] ((':) k x xs),
+               in an equation for `crash'
+      at T7230.hs:48:8-27
+    or from (xs1 ~ (':) Nat x1 xs2)
+      bound by a pattern with constructor
+                 SCons :: forall (k :: BOX) (x :: k) (xs :: [k]).
+                          Sing k x -> Sing [k] xs -> Sing [k] ((':) k x xs),
+               in an equation for `crash'
+      at T7230.hs:48:17-26
+    Expected type: SBool (Increasing xs)
+      Actual type: SBool (x :<<= x1)
+    In the expression: x %:<<= y
+    In an equation for `crash':
+        crash (SCons x (SCons y xs)) = x %:<<= y
diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index f2d2532b8d..1ad1b31d63 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -63,6 +63,8 @@ test('T7128', normal, compile,[''])
 test('T7151', normal, compile_fail,[''])
 test('T7095', normal, compile,[''])
 test('T7090', normal, compile,[''])
-test('T7176', expect_broken(7176), compile,[''])
+test('T7176', normal, compile,[''])
+test('T7224', normal, compile_fail,[''])
+test('T7230', normal, compile_fail,[''])