Fix #16517 by bumping the TcLevel for method sigs
Commit message:
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.
-
GHC assigns
f :: kappa1[1]
, where the[1]
means that we're at TcLevel 1. -
GHC assigns
a :: kappa2[2]
. 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[1] ~ (kappa2[2] -> *) [WD] kappa1[1] ~ *
I've simplified slightly by writing
*
instead ofTYPE rho[2]
, because levity polymorphism is not the issue here. -
We can't simplify these Wanteds because
kappa1[1]
is untouchable, and wanteds don't rewrite wanteds. But we can simplify the associated Deriveds, yielding:[W] kappa1[1] ~ (kappa2[2] -> *) [W] kappa1[1] ~ * [D] * ~ (kappa2[2] -> *) (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
tc_hs_sig_type
. -
Failing kicks us up to
tryCaptureConstraints
(as called fromcaptureTopConstraints
), 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. -
captureTopConstraints
ends up in itsNothing
case, where it callssimplifyTop
, which should report errors. -
Then,
simplifyTop
ends up eventually callingsetImplicationStatus
(the constraints above end up, rightly, in an implication constraint, because thea
is local in the type ofx
), which ends up dropping Derived constraints (seepruned_simples
insetImplicationStatus
). -
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 setImplicationStatus
.)