<div dir="ltr"><div>Hi all,</div><div><br></div><div>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.</div><div><br></div><div>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`.</div><div><br></div><div>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 <i>not</i> 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.<br></div><div><br></div><div>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 <i>not</i> 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.</div><div><br></div><div>Does this all sound right to people? If so, I will update the Note with the modified invariant and update the code to match.</div><div><br></div><div>Alexis<br></div></div>