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.lam...@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
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
