diff options
| -rw-r--r-- | compiler/GHC/Tc/Solver.hs | 36 | ||||
| -rw-r--r-- | testsuite/tests/typecheck/should_fail/T20043.hs | 21 | ||||
| -rw-r--r-- | testsuite/tests/typecheck/should_fail/T20043.stderr | 6 | ||||
| -rw-r--r-- | testsuite/tests/typecheck/should_fail/all.T | 1 |
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, ['']) |