Fix #14880.

Authored by goldfire on Oct 5 2018, 9:34 PM.



The real change that fixes the ticket is described in
Note [Naughty quantification candidates] in TcMType.

Fixing this required reworking candidateQTyVarsOfType, the function
that extracts free variables as candidates for quantification.
One consequence is that we now must be more careful when quantifying:
any skolems around must be quantified manually, and quantifyTyVars
will now only quantify over metavariables. This makes good sense,
as skolems are generally user-written and are listed in the AST.

As a bonus, we now have more control over the ordering of such

Along the way, this commit fixes Trac #15711 and refines the fix
to Trac #14552 (by accepted a program that was previously rejected,
as we can now accept that program by zapping variables to Any).

Test cases: dependent/should_fail/T14880{,-2}

Test Plan


goldfire created this revision.Oct 5 2018, 9:34 PM
RyanGlScott requested changes to this revision.Oct 6 2018, 10:11 AM
RyanGlScott added a subscriber: RyanGlScott.
RyanGlScott added inline comments.

This should be traceRn instead of traceTc, no?


There are a lot of traceTcs in this Diff with the comment RAE, which isn't terribly informative. Can these be combined with existing traceRns/traceTcs, or be given more descriptive comments?


The order of type variables here is now incorrect.

This revision now requires changes to proceed.Oct 6 2018, 10:11 AM

And I'll look into your comment about variable ordering. Thanks for pointing this out.


That was on purpose. But of course it shouldn't be merged!

goldfire updated this revision to Diff 18270.Oct 8 2018, 10:33 PM

A little more bugfixing.

RyanGlScott added inline comments.Oct 9 2018, 1:08 PM

I might be missing something obvious, but why is b inferred here? The type variable is certainly specified in C (it's required in C, in fact), so I would have expected F1 to inherit b's visibility from C.


Wow, impressive! Does this fully fix the remaining issues in Trac #15592, then?

I'm also curious to know how this patch works on the following program from :

class C a where
  type T (x :: (f :: k -> Type) a)

That's accepted in GHC 8.6 but currently rejected in HEAD. Does this patch change that story?

Started review; but ran out of time. Will try to do more shortly


I think we *only* collect meta-tyvars, correct? So dv_kvs, dv_tvs are all meta-tyvars. Any skolems are simply ignored. Right? Please so so in the data type decl, and mention this when discarding skolems


This "We identify the naughty..." is a tricky point, and is rather buried in this para. Could you support it with a concrete example?


Really funny name. Maybe cand_qtvs or collect_cand_qtvs?


So this warning is just for info -- it's not actually warning about anything wrong? I suggest deleting before committing.


Not just then --we can get skolems from enclosing scopes, and we don't want to quantify over them. Nothing naughty there.


Is that specified in the docs for extendDVarSet? If not, it should be.


This closeOverKinds covars is new. Explain it? (I think it is right.)

Maybe that affects/simplifies Note [Emitting the residual implication in simplifyInfer] in TsSimplify? Maybe not.. have not thought this through.


This is a tricky function! Make it top level, so that you can refer to it *by name* from the appropriate place in the (long) Note.



bgamari abandoned this revision.Oct 15 2018, 12:04 PM

Bumping out of the review queue. This has been broken up into several pieces. See Trac #14880 for details.

Oh dear, I was a bit hasty in concluding that this was stale; it looks like I was wrong.

@goldfire, feel free to request review on this again. Sorry about that!

goldfire added inline comments.Oct 15 2018, 12:11 PM

This is really just a judgment call. b isn't included in the type family definition, and so I would call it Inferred. Maybe that's silly, though, because we always do know where it will end up (if it ends up in the TF's kind at all) -- its order is determined by the class variable order.

What's weird about ATs is that, unlike normal methods, an AT kind doesn't necessarily mention all the class variables; only those that are mentioned in the AT LHS (or LHS variable kinds).

OK. You've convinced me. It should be Specified.

goldfire reclaimed this revision.Oct 15 2018, 12:12 PM

This is still under active work. I understand parts of Trac #14880 have been merged and will deal with that in due course.

goldfire marked 5 inline comments as done.Oct 15 2018, 4:53 PM
goldfire added inline comments.

Naughty quantification is exceedingly rare -- and almost always an error. If we hit this block of code, it's much more likely that GHC has gone off its rails than that the user has intended this. I think the warning is useful. Ask again and I'll remove it.


No. Those skolems are in the bound set, so will be caught by the first guard. (This is a change from previous versions, where bound contained only local tyvars. Now, it contains all in-scope tyvars.)


I don't really understand that Note.

  • decideMonoTyVars already pulls out the covars. We won't quantify over them or any tyvar free in their kinds. So the qtvs and the theta returned from decideQuantification won't have any covars.
  • mkResidualConstraints doesn't close over kinds. It seems to assume that co_vars will already be closed over kinds. But I don't see where this happens anywhere. (And if it does, then the type of co_vars, [EvVar] is a white lie.)
  • I don't see why any of this is necessary. Instead of separating out the outer simples from the inner ones, why not just put everything as an inner wanted? solveImplication will, in due course, float out the ones you promote in mkResidualConstraint, but that's much simpler than doing this all manually here.

So, this plan isn't working out. Here's the test case:

class C a where
  type F (x :: f a)
  1. No CUSK. So all those user-written variables are TyVarTvs.
  2. Kind inference tells us a :: kappa, f :: kappa -> Type, and, of course x :: f a.
  3. We generalize C in this generalise function. This skolemizes kappa to become k and also skolemizes a. We get C :: forall k. k -> Constraint.
  4. We generalize F:

    a. If we blithely called kindGeneralize on f a -> Type, we'd go wrong, because candidateQTyVarsOfType doesn't want to find skolems. It wants to generalize over metavars. So, instead, we look at F's ungeneralized (but zonked) type, find some skolems in there, and pull them out as the surprise_skolems. This will be a and k.

    b. Then, we generalize forall (k :: Type) (a :: k). f a -> Type. But that fails because f depends on k, and it looks like a naughty quantification candidate. This is caught in checkNaughtyQuantification.

The problem is that there's nothing wrong about putting f after k in the telescope. Indeed, I'd want k and a to come first, as their class variables. I don't know how to arrange for this.

I'm musing about the meaning of TyVarTvs here. We use them as described in this Note:

Note [Kind generalisation and TyVarTvs]
  data T (a :: k1) x = MkT (S a ())
  data S (b :: k2) y = MkS (T b ())

While we are doing kind inference for the mutually-recursive S,T,
we will end up unifying k1 and k2 together. So they can't be skolems.
We therefore make them TyVarTvs, which can unify with type variables,
but not with general types.  All this is very similar at the level
of terms: see Note [Quantified variables in partial type signatures]
in TcBinds.

There are some wrinkles

* We always want to kind-generalise over TyVarTvs, and /not/ default
  them to Type.  Another way to say this is: a SigTV should /never/
  stand for a type, even via defaulting. Hence the check in
  TcSimplify.defaultTyVarTcS, and TcMType.defaultTyVar.  Here's
  another example (Trac #14555):
     data Exp :: [TYPE rep] -> TYPE rep -> Type where
        Lam :: Exp (a:xs) b -> Exp xs (a -> b)
  We want to kind-generalise over the 'rep' variable.
  Trac #14563 is another example.

* Consider Trac #11203
    data SameKind :: k -> k -> *
    data Q (a :: k1) (b :: k2) c = MkQ (SameKind a b)
  Here we will unify k1 with k2, but this time doing so is an error,
  because k1 and k2 are bound in the same declaration.

  We sort this out using findDupTyVarTvs, in TcTyClTyVars; very much
  as we do with partial type signatures in mk_psig_qtvs in

It's gotten me thinking. What we really want to do is to allow unification of these TyVarTvs during constraint generation/solving, but (assuming the solver succeeds) we want to treat them as skolems during generalization.

So, new plan here: At the beginning of generalise, before any zonking, we go through and skolemize all TyVarTvs. This means filling the metavar IORefs with fresh skolem variables -- even if an IORef is already filled. (Alternatively, we could just use a substitution.) Now, zonk and manually quantify over those skolems. By "manually" here, I mean not to use quantifyTyVars; instead, just make TyConBinders and prepend to tc_binders. Then, after all that, call kindGeneralize to find any unconstrained metavars left in a kind.

This new approach avoids the two wrinkles in the Note above and it accepts the example at the top of this comment. (The second wrinkle is avoided because the "type-checking" pass will error if the first pass unified two TyVarTvs.) The cost is that it bizarrely re-fills filled-in metavars. One worry here is that there may have been zonking that happened before the re-fill. Here, that won't happen because we've just pulled the tycon's kind from the TcTyCon generated in getInitialKinds.

I think the strangeness here is with good reason: the user really meant these variables to be skolems; we just couldn't be clever enough during kind inference to use skolems the first time, instead relying on TyVarTvs.

I'd love some feedback before plowing ahead.

goldfire updated this revision to Diff 18319.Oct 15 2018, 4:54 PM
goldfire marked an inline comment as done.
  • Wibbles suggested by Simon
goldfire updated this revision to Diff 18509.Oct 28 2018, 2:27 PM

Get quantification right, for once.

See Note [Required, Specified, and Inferred for types] in TcTyClsDecls
and the new, shiny implementation of the generalise function
in kcTyClGroup.

Also, lots of user's manual updates.

goldfire added inline comments.Oct 28 2018, 2:46 PM

I gave up on this plan entirely. It was never going to work. The new one, skolemising all the declarations at once, then sorting out the quantified variables one-at-a-time, works very well.