Fix over-eager implication constraint discard

Ticket #16247 showed that we were discarding an implication
constraint that had empty ic_wanted, when we still needed to
keep it so we could check whether it had a bad telescope.

Happily it's a one line fix.  All the rest is comments!

5 files changed, 50 insertions, 0 deletions

diff --git a/testsuite/tests/polykinds/T16247.hs b/testsuite/tests/polykinds/T16247.hs
new file mode 100644
index 0000000000..617f3c4aca
--- /dev/null
+++ b/testsuite/tests/polykinds/T16247.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeInType #-}
+module Bug where
+
+import Data.Kind
+
+data SameKind :: forall k. k -> k -> Type
+data Foo :: forall a k (b :: k). SameKind a b -> Type where
+  MkFoo :: Foo sameKind
diff --git a/testsuite/tests/polykinds/T16247.stderr b/testsuite/tests/polykinds/T16247.stderr
new file mode 100644
index 0000000000..34a1319996
--- /dev/null
+++ b/testsuite/tests/polykinds/T16247.stderr
@@ -0,0 +1,7 @@
+
+T16247.hs:9:13: error:
+    • These kind and type variables: a k (b :: k)
+      are out of dependency order. Perhaps try this ordering:
+        k (a :: k) (b :: k)
+    • In the kind ‘forall a k (b :: k). SameKind a b -> Type’
+      In the data type declaration for ‘Foo’
diff --git a/testsuite/tests/polykinds/T16247a.hs b/testsuite/tests/polykinds/T16247a.hs
new file mode 100644
index 0000000000..60a98d6c8f
--- /dev/null
+++ b/testsuite/tests/polykinds/T16247a.hs
@@ -0,0 +1,23 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+module Bug where
+
+import Data.Kind (Constraint, Type)
+import GHC.Generics (Rep1, U1(..))
+
+data TyFun :: Type -> Type -> Type
+type a ~> b = TyFun a b -> Type
+infixr 0 ~>
+type family Apply (f :: a ~> b) (x :: a) :: b
+type SameKind (a :: k) (b :: k) = (() :: Constraint)
+
+type family From1 (z :: (f :: Type -> Type) a) :: Rep1 f a
+
+type family From1U1 (x :: U1 (p :: k)) :: Rep1 U1 p where {}
+data From1U1Sym0 :: forall p k. (U1 :: k -> Type) p ~> Rep1 (U1 :: k -> Type) p where
+  From1Sym0KindInference :: forall z arg. SameKind (Apply From1U1Sym0 arg) (From1U1 arg)
+                         => From1U1Sym0 z
diff --git a/testsuite/tests/polykinds/T16247a.stderr b/testsuite/tests/polykinds/T16247a.stderr
new file mode 100644
index 0000000000..ce75878f38
--- /dev/null
+++ b/testsuite/tests/polykinds/T16247a.stderr
@@ -0,0 +1,8 @@
+
+T16247a.hs:21:21: error:
+    • These kind and type variables: p k
+      are out of dependency order. Perhaps try this ordering:
+        k (p :: k)
+    • In the kind ‘forall p k.
+                   (U1 :: k -> Type) p ~> Rep1 (U1 :: k -> Type) p’
+      In the data type declaration for ‘From1U1Sym0’
diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index c67d80d621..6238fbe770 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -206,6 +206,8 @@ test('T14887a', normal, compile, [''])
 test('T14847', normal, compile, [''])
 test('T15795', normal, compile, [''])
 test('T15795a', normal, compile, [''])
+test('T16247', normal, compile_fail, [''])
+test('T16247a', normal, compile_fail, [''])
 test('KindVarOrder', normal, ghci_script, ['KindVarOrder.script'])
 test('T16221', normal, compile, [''])
 test('T16221a', normal, compile_fail, [''])