Fix and simplify DeriveAnyClass's context inference using SubTypePredSpec
As explained in Note [Gathering and simplifying constraints for DeriveAnyClass]
in GHC.Tc.Deriv.Infer
, DeriveAnyClass
infers instance contexts by emitting
implication constraints. Previously, these implication constraints were
constructed by hand. This is a terribly trick thing to get right, as it
involves a delicate interplay of skolemisation, metavariable instantiation, and
TcLevel
bumping. Despite much effort, we discovered in #20719 (closed) that the
implementation was subtly incorrect, leading to valid programs being rejected.
While we could scrutinize the code that manually constructs implication
constraints and repair it, there is a better, less error-prone way to do
things. After all, the heart of DeriveAnyClass
is generating code which
fills in each class method with defaults, e.g., foo = $gdm_foo
. Typechecking
this sort of code is tantamount to calling tcSubTypeSigma
, as we much ensure
that the type of $gdm_foo
is a subtype of (i.e., more polymorphic than) the
type of foo
. As an added bonus, tcSubTypeSigma
is a battle-tested function
that handles skolemisation, metvariable instantiation, TcLevel
bumping, and
all other means of tricky bookkeeping correctly.
With this insight, the solution to the problems uncovered in #20719 (closed) is simple:
use tcSubTypeSigma
to check if $gdm_foo
's type is a subtype of foo
's
type. As a side effect, tcSubTypeSigma
will emit exactly the implication
constraint that we were attempting to construct by hand previously. Moreover,
it does so correctly, fixing #20719 (closed) as a consequence.
This patch implements the solution thusly:
- The
PredSpec
data type (previously namedPredOrigin
) is now split intoSimplePredSpec
, which directly stores aPredType
, andSubTypePredSpec
, which stores the actual and expected types in a subtype check.SubTypePredSpec
is only used forDeriveAnyClass
; all other deriving strategies useSimplePredSpec
. - Because
tcSubTypeSigma
manages the finer details of type variable instantiation and constraint solving under the hood, there is no longer any need to delicately split apart the method type signatures ininferConstraintsAnyclass
. This greatly simplifies the implementation ofinferConstraintsAnyclass
and obviates the need to store skolems, metavariables, or given constraints in aThetaSpec
(previously namedThetaOrigin
). As a bonus, this means thatThetaSpec
now simply becomes a synonym for a list ofPredSpec
s, which is conceptually much simpler than it was before. - In
simplifyDeriv
, eachSubTypePredSpec
results in a call totcSubTypeSigma
. This is only performed for its side effect of emitting an implication constraint, which is fed to the rest of the constraint solving machinery insimplifyDeriv
. I have updatedNote [Gathering and simplifying constraints for DeriveAnyClass]
to explain this in more detail.
To make the changes in simplifyDeriv
more manageable, I also performed some
auxiliary refactoring:
- Previously, every iteration of
simplifyDeriv
was skolemising the type variables at the start, simplifying, and then performing a reverse substitution at the end to un-skolemise the type variables. This is not necessary, however, since we can just as well skolemise once at the beginning of thederiving
pipeline and zonk theTcTyVar
s aftersimplifyDeriv
is finished. This patch does just that, having been made possible by prior work in !7613 (closed). I have updatedNote [Overlap and deriving]
inGHC.Tc.Deriv.Infer
to explain this, and I have also left comments on the relevant data structures (e.g.,DerivEnv
andDerivSpec
) to explain when things might beTcTyVar
s orTyVar
s. - All of the aforementioned cleanup allowed me to remove an ad hoc
deriving-related in
checkImplicationInvariants
, as all of the skolems in atcSubTypeSigma
–produced implication constraint should now beTcTyVar
at the time the implication is created. - Since
simplifyDeriv
now needs aSkolemInfo
andUserTypeCtxt
, I have addedds_skol_info
andds_user_ctxt
fields toDerivSpec
to store these. Similarly, I have also added adenv_skol_info
field toDerivEnv
, which ultimately gets used to initialize theds_skol_info
in aDerivSpec
.
Fixes #20719 (closed).