Concrete#, SpecialPred, and CtEvidence invariants

[Richard Eisenberg]

Good point.

The Note is wrong.

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.)

Instead, I think the invariant is good as it is except for CSpecialPreds. Which are special. :)

And, you're right that a CoVar should never have a type of Concrete# blah. Find that code and kill it.

Does this help?

Richard

> On Dec 8, 2021, at 2:40 PM, Alexis King <lexi.lambda at gmail.com> wrote:
> 
> 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/d4cba8f3/attachment.html>