Concrete#, SpecialPred, and CtEvidence invariants

[Alexis King]

Hi all,

After a recent off-list conversation, I’ve been exploring using the new
SpecialPred mechanism to implement a custom constraint, but I’ve run into
some questions regarding evidence for CSpecialCan constraints.
Specifically, I’m uncertain about how to use them while satisfying Note
[CtEvidence invariants] in GHC.Tc.Types.Constraint.

Specifically, the Note in question states that ctev_pred must always be
kept in sync with the type of the evidence. For example, if ctev_dest for a
wanted constraint is a coercion hole, ctev_pred must be `varType
(coHoleCoVar hole)`. However, this seems rather odd in the case of
Concrete# constraints, since the evidence for a `Concrete# (ty :: ki)`
constraint is a coercion of type `ty ~# alpha`.

In canNonDecomposableConcretePrim in GHC.Tc.Solver.Canonical,
setCtEvPredType is used to update the type of a CSpecialCan constraint, and
setCtEvPredType automatically maintains the CtEvidence invariant mentioned
above. But this results in setCoHoleType being used to modify the type of
the CoVar from `ty ~# alpha` to `Concrete# (ty :: ki)`, which does not make
much sense, since that is definitely *not* the type of the CoVar. As far as
I can tell, the only reason that doesn’t cause Core Lint errors is that the
modified CoVar is never actually used, only the original one is.

This suggests to me that the invariant is not actually the right one. The
Note suggests that the reason the invariant exists is that the type must be
kept fully-zonked… which in turn suggests that perhaps fully-zonkedness is
the invariant that’s actually desired. In that case, ctev_pred would *not*
necessarily always be a cache for the type of the evidence, since in the
case of Concrete#, the evidence has a different type (though for other
types of constraints the old invariant would still coincidentally hold).
Rather, it would be the responsibility of canNonDecomposableConcretePrim to
merely ensure the evidence’s type is appropriately zonked.

Does this all sound right to people? If so, I will update the Note with the
modified invariant and update the code to match.

Alexis
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20211208/a8a93ade/attachment.html>