Skip to content

Fix #16517 by bumping the TcLevel for method sigs

Richard Eisenberg requested to merge rae/ghc:wip/t16517 into master

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.

  1. GHC assigns f :: kappa1[1], where the [1] means that we're at TcLevel 1.

  2. GHC assigns a :: kappa2[2]. The level is higher here because we're inside a signature. This bump is new in this patch.

  3. We get the following constraints, while at TcLevel 2:

    [WD] kappa1[1] ~ (kappa2[2] -> *)
    [WD] kappa1[1] ~ *

    I've simplified slightly by writing * instead of TYPE rho[2], because levity polymorphism is not the issue here.

  4. 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.

  5. This set of constraints, rightly, is labeled as insoluble, and so we fail in the check at the end of tc_hs_sig_type.

  6. 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.

  7. captureTopConstraints ends up in its Nothing case, where it calls simplifyTop, which should report errors.

  8. Then, simplifyTop ends up eventually calling setImplicationStatus (the constraints above end up, rightly, in an implication constraint, because the a is local in the type of x), which ends up dropping Derived constraints (see pruned_simples in setImplicationStatus).

  9. 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.)

Edited by Richard Eisenberg

Merge request reports