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!

8 files changed, 98 insertions, 5 deletions

diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index fac6f2e31c..a7e3cf7945 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -1652,6 +1652,8 @@ is correct, choosing ImplicationStatus IC_BadTelescope if they aren't.
 Then, in TcErrors, we report if there is a bad telescope. This way,
 we can report a suggested ordering to the user if there is a problem.
 
+See also Note [Checking telescopes] in TcRnTypes
+
 Note [Keeping scoped variables in order: Implicit]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 When the user implicitly quantifies over variables (say, in a type
diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs
index c8d83215fd..8882bbc6c7 100644
--- a/compiler/typecheck/TcRnTypes.hs
+++ b/compiler/typecheck/TcRnTypes.hs
@@ -2587,11 +2587,9 @@ data Implication
       ic_skols :: [TcTyVar],     -- Introduced skolems
       ic_info  :: SkolemInfo,    -- See Note [Skolems in an implication]
                                  -- See Note [Shadowing in a constraint]
+
       ic_telescope :: Maybe SDoc,  -- User-written telescope, if there is one
-                                   -- The list of skolems is order-checked
-                                   -- if and only if this is a Just.
-                                   -- See Note [Keeping scoped variables in order: Explicit]
-                                   -- in TcHsType
+                                   -- See Note [Checking telescopes]
 
       ic_given  :: [EvVar],      -- Given evidence variables
                                  --   (order does not matter)
@@ -2708,7 +2706,43 @@ instance Outputable ImplicStatus where
   ppr (IC_Solved { ics_dead = dead })
     = text "Solved" <+> (braces (text "Dead givens =" <+> ppr dead))
 
-{-
+{- Note [Checking telescopes]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When kind-checking a /user-written/ type, we might have a "bad telescope"
+like this one:
+  data SameKind :: forall k. k -> k -> Type
+  type Foo :: forall a k (b :: k). SameKind a b -> Type
+
+The kind of 'a' mentions 'k' which is bound after 'a'.  Oops.
+
+Knowing this means that unification etc must have happened, so it's
+convenient to detect it in the constraint solver:
+
+* We make a single implication constraint when kind-checking
+  the 'forall' in Foo's kind, something like
+      forall a k (b::k). { wanted constraints }
+
+* Having solved {wanted}, before discarding the now-solved implication,
+  the costraint solver checks the dependency order of the skolem
+  variables (ic_skols).  This is done in setImplicationStatus.
+
+* This check is only necessary if the implication was born from a
+  user-written signature.  If, say, it comes from checking a pattern
+  match that binds existentials, where the type of the data constructor
+  is known to be valid (it in tcConPat), no need for the check.
+
+  So the check is done if and only if ic_telescope is (Just blah).
+
+* If ic_telesope is (Just d), the d::SDoc displays the original,
+  user-written type variables.
+
+* Be careful /NOT/ to discard an implication with non-Nothing
+  ic_telescope, even if ic_wanted is empty.  We must give the
+  constraint solver a chance to make that bad-telesope test!  Hence
+  the extra guard in emitResidualTvConstraint; see #16247
+
+See also TcHsTYpe Note [Keeping scoped variables in order: Explicit]
+
 Note [Needed evidence variables]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Th ic_need_evs field holds the free vars of ic_binds, and all the
diff --git a/compiler/typecheck/TcUnify.hs b/compiler/typecheck/TcUnify.hs
index 35f4d00f39..45cc3f9168 100644
--- a/compiler/typecheck/TcUnify.hs
+++ b/compiler/typecheck/TcUnify.hs
@@ -64,6 +64,7 @@ import Util
 import qualified GHC.LanguageExtensions as LangExt
 import Outputable
 
+import Data.Maybe( isNothing )
 import Control.Monad
 import Control.Arrow ( second )
 
@@ -1176,7 +1177,13 @@ emitResidualTvConstraint :: SkolemInfo -> Maybe SDoc -> [TcTyVar]
                          -> TcLevel -> WantedConstraints -> TcM ()
 emitResidualTvConstraint skol_info m_telescope skol_tvs tclvl wanted
   | isEmptyWC wanted
+  , isNothing m_telescope || skol_tvs `lengthAtMost` 1
+    -- If m_telescope is (Just d), we must do the bad-telescope check,
+    -- so we must /not/ discard the implication even if there are no
+    -- wanted constraints. See Note [Checking telescopes] in TcRnTypes.
+    -- Lacking this check led to #16247
   = return ()
+
   | otherwise
   = do { ev_binds <- newNoTcEvBinds
        ; implic   <- newImplication
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, [''])