
<html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">Good point.<div class=""><br class=""></div><div class="">The Note is wrong.</div><div class=""><br class=""></div><div class="">But I don't like an invariant on a data structure about zonkedness: the zonkedness of a type can change whenever we fill in a unification variable, possibly very far away. (On the other hand, it does make sense for functions to talk about zonkedness in preconditions and postconditions, because function calls happen at a certain instant of time.)</div><div class=""><br class=""></div><div class="">Instead, I think the invariant is good as it is except for CSpecialPreds. Which are special. :)</div><div class=""><br class=""></div><div class="">And, you're right that a CoVar should never have a type of Concrete# blah. Find that code and kill it.</div><div class=""><br class=""></div><div class="">Does this help?</div><div class=""><br class=""></div><div class="">Richard</div><div class=""><div><br class=""><blockquote type="cite" class=""><div class="">On Dec 8, 2021, at 2:40 PM, Alexis King <<a href="mailto:lexi.lambda@gmail.com" class="">lexi.lambda@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div dir="ltr" class=""><div class="">Hi all,</div><div class=""><br class=""></div><div class="">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 class=""><br class=""></div><div class="">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 class=""><br class=""></div><div class="">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 class="">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 class=""></div><div class=""><br class=""></div><div class="">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 class="">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 class=""><br class=""></div><div class="">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 class=""><br class=""></div><div class="">Alexis<br class=""></div></div>

</div></blockquote></div><br class=""></div></body></html>