Fix #16517 by bumping the TcLevel for method sigs
Fix #16517 by bumping the TcLevel for method sigs There were actually two bugs fixed here: 1. candidateQTyVarsOfType really needs to know what tvs are in scope, so that it doesn't think that an in-scope tv is "naughty". Not doing this led to the reported error in #16517. This is easy to fix, by passing in the set of in-scope variables. (Indeed, the comments suggested we were already doing this, but we weren't.) 2. We weren't bumping the TcLevel in kcHsKindSig, which was used only for class method sigs. This mistake led to the acceptance of class C a where meth :: forall k. Proxy (a :: k) -> () Note that k is *locally* quantified. This patch fixes the problem by using tcClassSigType, which correctly bumps the level. It's a bit inefficient because tcClassSigType does other work, too, but it would be tedious to repeat much of the code there with only a few changes. This version works well and is simple.
OLD TEXT -- FIXED NOW:
Sadly, this doesn't quite work yet. The failing case is deceptively simple:
class Foo f where x :: f a -> f
That's clearly very bogus. This patch suppresses GHC's error reporting. Here is why.
f :: kappa1, where the
means that we're at TcLevel 1.
a :: kappa2. The level is higher here because we're inside a signature. This bump is new in this patch.
We get the following constraints, while at TcLevel 2:
[WD] kappa1 ~ (kappa2 -> *) [WD] kappa1 ~ *
I've simplified slightly by writing
TYPE rho, because levity polymorphism is not the issue here.
We can't simplify these Wanteds because
kappa1is untouchable, and wanteds don't rewrite wanteds. But we can simplify the associated Deriveds, yielding:
[W] kappa1 ~ (kappa2 -> *) [W] kappa1 ~ * [D] * ~ (kappa2 -> *) (insol)
Note that only the Derived is insoluble.
This set of constraints, rightly, is labeled as insoluble, and so we fail in the check at the end of
Failing kicks us up to
tryCaptureConstraints(as called from
captureTopConstraints), where we filter out anything that isn't insoluble, according to Note [Constraints and errors] in TcRnMonad. So, now we're just left the Derived constraint.
captureTopConstraintsends up in its
Nothingcase, where it calls
simplifyTop, which should report errors.
simplifyTopends up eventually calling
setImplicationStatus(the constraints above end up, rightly, in an implication constraint, because the
ais local in the type of
x), which ends up dropping Derived constraints (see
Now we're left with no constraints at all! And so GHC reports no errors and just stops, silently and disconcertingly.
I can think of various knobs to turn to stop this chain of events, but these knobs will all have knock-on effects, and I'd like advice before I start spinning knobs. (In particular, I'm curious why we always drop Deriveds in