(posted on behalf of Simon PJ)
My original goal was (Trac Trac #15809) to move towards using level numbers
as the basis for deciding which type variables to generalise, rather
than searching for the free varaibles of the environment.
And indeed this patch does make such a step:
- Augment quantifyTyVars to calculate the type variables to quantify using level numbers, and compare the result with the existing approach. That is; no change in behaviour, just a WARNing if the two approaches give different answers.
- To do this I had to get the level number right when calling quantifyTyVars, and this entailed a bit of care, especially in the code for kind-checking type declarations.
- However, on the way I was able to eliminate or simplify a number of calls to solveEqualities.
Similarly I curbed the excessive use of scopeTyVars, which also invokes solveEqualities. There is only one left, in tcFamTyPats -- a gruesome function that is next on my target list.
This led me into deep dive into kind inference for type and class
declarations, which has been a soggy part of GHC for a long time.
Richard already did some good work recently in
commit 5e45ad10ffca1ad175b10f6ef3327e1ed8ba25f3 Date: Thu Sep 13 09:56:02 2018 +0200 Finish fix for #14880. The real change that fixes the ticket is described in Note [Naughty quantification candidates] in TcMType.
but I kept turning over stones. So this patch has ended up
with a pretty significant refactoring of that code too.
- Major refactoring in the way we generalise the inferred kind of a TyCon, in kcTyClGroup. Indeed, I made it into a new top-level function, generaliseTcTyCon. Plus a new Note to explain it Note [Inferring kinds for type declarations].
- We decided (Trac Trac #15592) not to treat class type variables specially when dealing with Inferred/Specified/Required for associated types. That simplifies things quite a bit. I also rewrote Note [Required, Specified, and Inferred for types]
- Some refactoring in kcLHsQTyVarBndrs (the CUSK case); it is easier because of our new decision not to treat the class variables specially
- I now deal with the "naughty quantification candidates" of the previous patch in candidateQTyVars, rather than in quantifyTyVars; see Note [Naughty quantification candidates] in TcMType.
I also killed off closeOverKindsCQTvs in favour of the same strategy that we use for tyCoVarsOfType: namely, close over kinds at the occurrences.
And candidateQTyVars no longer needs a gbl_tvs argument.
- Passing the ContextKind, rather than the expected kind itself, to tc_hs_sig_type_and_gen makes it easy to allocate the expected result kind (when we are in inference mode) at the right level.
- I moved all the error checks from tcTyClTyVars (which was a bizarre place for it) into generaliseTcTyCon and/or the CUSK case of kcLHsQTyVars. Now tcTyClTyVars is extremely simple.
- kcLHsQTYVarBndrs had strange stuff about "bind unless scoped". I could not see any justification for this, so I simply removed it all. Much simpler now.
- I rejigged the error message in checkValidTelescope; I think it's quite a bit better now.
- checkValidType was not rejecting constraints in a kind signature forall (a :: Eq b => blah). blah2 That led to further errors when we then do an ambiguity check. So I make checkValidType reject it more aggressively.
- I killed off quantifyConDecl, instead calling kindGeneralize directly.
- I fixed an outright bug in tyCoVarsOfImplic, where we were not colleting the tyvar of the kind of the skolems
Some other oddments
- Refactoring around the trace messages from reportUnsolved.
- A bit of extra tc-tracing in TcHsSyn.commitFlexi