Bump TcLevel of failing kind equality implication

  Not bumping the TcLevel meant that we could end up
  trying to add evidence terms for the implication constraint
  created to wrap failing kind equalities (to avoid their deferral).

fixes #20043

4 files changed, 56 insertions, 8 deletions

diff --git a/compiler/GHC/Tc/Solver.hs b/compiler/GHC/Tc/Solver.hs
index 7836c4a1b4..6d9770adbf 100644
--- a/compiler/GHC/Tc/Solver.hs
+++ b/compiler/GHC/Tc/Solver.hs
@@ -222,9 +222,11 @@ simplifyAndEmitFlatConstraints wanted
                          -- Emit the bad constraints, wrapped in an implication
                          -- See Note [Wrapping failing kind equalities]
                          ; tclvl  <- TcM.getTcLevel
-                         ; implic <- buildTvImplication UnkSkol [] tclvl wanted
-                                     -- UnkSkol: doesn't matter, because
-                                     -- we bind no skolem variables here
+                         ; implic <- buildTvImplication UnkSkol [] (pushTcLevel tclvl) wanted
+                                    --                  ^^^^^^   |  ^^^^^^^^^^^^^^^^^
+                                    -- it's OK to use UnkSkol    |  we must increase the TcLevel,
+                                    -- because we don't bind     |  as explained in
+                                    -- any skolem variables here |  Note [Wrapping failing kind equalities]
                          ; emitImplication implic
                          ; failM }
            Just (simples, holes)
@@ -403,12 +405,30 @@ Our solution is this:
 
 * Right here in simplifyAndEmitFlatConstraints, use buildTvImplication
   to wrap the failing constraint in a degenerate implication (no
-  skolems, no theta, no bumped TcLevel), with ic_binds = CoEvBindsVar.
-  That way any failing equalities will lead to an error not a warning,
-  irrespective of -fdefer-type-errors.
+  skolems, no theta), with ic_binds = CoEvBindsVar.  This setting of
+  `ic_binds` means that any failing equalities will lead to an
+  error not a warning, irrespective of -fdefer-type-errors: see
+  Note [Failing equalities with no evidence bindings] in GHC.Tc.Errors,
+  and `maybeSwitchOffDefer` in that module.
+
+  We still take care to bump the TcLevel of the implication.  Partly,
+  that ensures that nested implications have increasing level numbers
+  which seems nice.  But more specifically, suppose the outer level
+  has a Given `(C ty)`, which has pending (not-yet-expanded)
+  superclasses. Consider what happens when we process this implication
+  constraint (which we have re-emitted) in that context:
+    - in the inner implication we'll call `getPendingGivenScs`,
+    - we /do not/ want to get the `(C ty)` from the outer level,
+    lest we try to add an evidence term for the superclass,
+    which we can't do because we have specifically set
+    `ic_binds` = `CoEvBindsVar`.
+    - as `getPendingGivenSCcs is careful to only get Givens from
+    the /current/ level, and we bumped the `TcLevel` of the implication,
+    we're OK.
+
+  TL;DR: bump the `TcLevel` when creating the nested implication.
+  If we don't we get a panic in `GHC.Tc.Utils.Monad.addTcEvBind` (#20043).
 
-  This is a slight hack, because the implication doesn't have a bumped
-  TcLevel, but that doesn't matter.
 
 We re-emit the implication rather than reporting the errors right now,
 so that the error mesages are improved by other solving and defaulting.
diff --git a/testsuite/tests/typecheck/should_fail/T20043.hs b/testsuite/tests/typecheck/should_fail/T20043.hs
new file mode 100644
index 0000000000..8494537c7c
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T20043.hs
@@ -0,0 +1,21 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE MonoLocalBinds #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE UndecidableSuperClasses #-}
+
+module T20043 where
+import Data.Kind
+data T1
+data T2
+
+type All :: Type -> Type -> Constraint
+class All T1 xs => All c xs
+repo :: forall (a :: Type). All T2 a => a -> a
+repo x =
+    let y = undefined @a
+    in x
diff --git a/testsuite/tests/typecheck/should_fail/T20043.stderr b/testsuite/tests/typecheck/should_fail/T20043.stderr
new file mode 100644
index 0000000000..cafb93bd04
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T20043.stderr
@@ -0,0 +1,6 @@
+
+T20043.hs:20:24: error:
+    • Expected kind ‘GHC.Types.RuntimeRep’, but ‘a’ has kind ‘*’
+    • In the type ‘a’
+      In the expression: undefined @a
+      In an equation for ‘y’: y = undefined @a
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 20b30d3deb..34ab2f2f7a 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -634,6 +634,7 @@ test('T19615', normal, compile_fail, [''])
 test('T17817', normal, compile_fail, [''])
 test('T17817_elab', normal, compile_fail, ['-fprint-typechecker-elaboration'])
 test('T19978', normal, compile_fail, [''])
+test('T20043', normal, compile_fail, [''])
 test('T20122', normal, compile_fail, [''])
 test('T20241b', normal, compile_fail, [''])
 test('OrdErr', normal, compile_fail, [''])