<html><head><meta http-equiv="Content-Type" content="text/html; charset=us-ascii"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><br class=""><div><br class=""><blockquote type="cite" class=""><div class="">On Nov 30, 2020, at 11:41 AM, Christiaan Baaij <<a href="mailto:christiaan.baaij@gmail.com" class="">christiaan.baaij@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div dir="ltr" class=""><div class="">Richard, I just watched your talk about simplifying the constraint solver: <a href="https://www.youtube.com/watch?v=flwz6V5Ps8w" class="">https://www.youtube.com/watch?v=flwz6V5Ps8w</a></div><div class="">and then realised that no flattening at all means also no flattening of [W]anteds.</div></div></div></blockquote><div><br class=""></div><div>Yes, that's true.</div><br class=""><blockquote type="cite" class=""><div class=""><div dir="ltr" class=""><div class=""><br class=""></div><div class="">Now, let's say I have a type family called "Magic" for which I want to write a constraint solver plugin; and some type family "Foo" and "Bar"<br class=""></div><div class="">And then lets say we start out with an original [W]anted: Foo (Magic 8) ~ Bar 42</div><div class=""><br class=""></div><div class="">Then if I understand flattening correctly, that would get flattened to:</div><div class="">[w] Magic 8 ~ fmv1</div><div class="">[w] fmv1 ~ 42</div><div class="">[w] Foo fmv1 ~ fmv2</div><div class="">[w] fmv2 ~ Bar fmv1</div><div class=""><br class=""></div><div class="">Correct?</div></div></div></blockquote><div><br class=""></div><div>I get</div><div><br class=""></div><div>[W] Magic 8 ~ fmv1</div><div>[W] Foo fmv1 ~ fmv2</div><div>[W] Bar 42 ~ fmv3</div><div>[W] fmv2 ~ fmv3</div><div><br class=""></div><blockquote type="cite" class=""><div class=""><div dir="ltr" class=""><div class=""><br class=""></div><div class="">So currently, with flattened wanted, all a constraint solver plugin has to do is look for [w]anted where the head of the type family application is "Magic", [w] Magic 8 ~ fmv1.</div><div class="">Then perhaps do some substitution for fmv1 to get back [w] Magic 8 ~ 42, use its internal solving rules to reduce Magic 8 to 42, and conclude what "[w] 42 ~ 42" can be solved by reflexivity.</div></div></div></blockquote><div><br class=""></div><div>It looks like maybe you edited your example afterwards? This doesn't quite line up, because we don't have [W] Magic 8 ~ 42 anywhere. But I see your point, in that flattening brings the type family out to the top level.</div><br class=""><blockquote type="cite" class=""><div class=""><div dir="ltr" class=""><div class=""><br class=""></div><div class="">But in a version without flattening, all we would see is:</div><div class="">[W]
Foo (Magic 8) ~ Foo 42 <br class=""></div></div></div></blockquote><div><br class=""></div><div>Did you mean [W] Foo (Magic 8) ~ Bar 42? Then, yes.</div><br class=""><blockquote type="cite" class=""><div class=""><div dir="ltr" class=""><div class=""><br class=""></div><div class="">And all I can do is to traverse the entire [W]anted, look for type family applications of "Magic" an then improve to:</div><div class="">[W] Foo 42 ~ Bar 42</div><div class=""><br class=""></div><div class="">Now... I can't declare that [W]anted solved, because i have no idea what Foo and Bar do (they might also be type families that can only be solved through constraint solver plugins).</div><div class="">Currently, the API for constraint solving plugins allows me to return _either_: <a href="http://hackage.haskell.org/package/ghc-8.10.1/docs/TcRnTypes.html#t:TcPluginResult" class="">http://hackage.haskell.org/package/ghc-8.10.1/docs/TcRnTypes.html#t:TcPluginResult</a></div><div class="">A) A set of contradictions</div><div class="">B) A set of solved [W] constraints + A set of new [W] constraints</div><div class=""><br class=""></div><div class="">With the above API, the only way to move forward is to: 1) declare "[w] Foo (Magic 8) ~ Bar 42" solved, while at the same time emitting a new wanted "[w] Foo 42 ~ Bar 42"</div></div></div></blockquote><div><br class=""></div><div>Yes, that's what you would do. Indeed, it's what GHC does whenever simplifying part of a Wanted.</div><br class=""><blockquote type="cite" class=""><div class=""><div dir="ltr" class=""><div class="">But it's basically the same wanted... so I would like a function of type "updateWantedType :: Ct -> TcPredType -> Ct" (which I don't think exists in the current GHC API)</div></div></div></blockquote><div><br class=""></div><div>This would not be hard to write, though you'd also need evidence relating the old type and the new one. Here's an attempt (that I have not tested, beyond the ability to compile it):</div><div><br class=""></div><div><div></div><blockquote type="cite" class=""><div>import GHC.Plugins</div><div>import GHC.Tc.Utils.TcType</div><div>import GHC.Tc.Types.Evidence</div><div>import GHC.Tc.Types.Constraint</div><div>import GHC.Tc.Plugin</div><div><br class=""></div><div>updateWantedType :: Ct -- initial constraint; always unsolved equality wanted</div><div> -- t1 ~N t2</div><div> -> TcPredType -- desired new constraint: s1 ~N s2</div><div> -> CoercionN -- lhs_co :: t1 ~N s1</div><div> -> CoercionN -- rhs_co :: t2 ~N s2</div><div> -> TcPluginM (Ct, EvTerm) -- new constraint, evidence for *old* constraint</div><div>-- NB: the *old* constraint is solved by the returned EvTerm;</div><div>-- return the EvTerm with the *old* constraint in TcPluginOk</div><div>updateWantedType old_ct new_pred lhs_co rhs_co = do</div><div> new_w <- newWanted (ctLoc old_ct) new_pred</div><div> let new_co = ctEvCoercion new_w -- :: s1 ~N s2</div><div> old_co = lhs_co `mkTransCo` new_co `mkTransCo` mkSymCo rhs_co</div><div> old_ev = evCoercion old_co</div><div> return (mkNonCanonical new_w, old_ev)</div></blockquote><div class=""><br class=""></div></div><div>That would seem to do the trick. This function is essentially extracted from GHC.Tc.Solver.Canonical.rewriteEqEvidence, and GHC does it many many times while working with equalities.</div><br class=""><blockquote type="cite" class=""><div class=""><div dir="ltr" class=""><div class=""><br class=""></div><div class="">But you might think the above way of working with the constraint solver as a plugin write, where we "solve" a wanted, only to emit an "improved" wanted, is _not_ the way things should work.</div></div></div></blockquote><div><br class=""></div><div>I don't quite know how to interpret this statement. This way of working is commonplace. For example, it's what we do when trying to prove a goal by hand when working backwards: we simplify the goal Wanted by rewriting it to another (presumably simpler) Wanted -- as long as the new Wanted can prove the old one.</div><br class=""><blockquote type="cite" class=""><div class=""><div dir="ltr" class=""><div class="">If that's the case, how do you envision plugin writers interacting with the solver?</div></div></div></blockquote><div><br class=""></div><div>As you've outlined above.</div><br class=""><blockquote type="cite" class=""><div class=""><div dir="ltr" class=""><div class="">Note that the above way of interacting with the constraint solver, "solving" + emitting "improved", is something I already sorta do, but in a different context:</div><div class="">In "ghc-typelits-natnormalise", when asked to solve [w] "a + Foo b ~ Foo b + c", I solve it, but then immediately emitting "[w] a ~ c".<br class=""></div></div></div></blockquote><div><br class=""></div><div>And that's really the way to do it.</div><div><br class=""></div><div>A slightly different problem than the one you've outlined here is that generating the coercions to pass to updatedWantedType might be challenging. So I wonder about a new kind of plugin, called a "rewriter plugin", that looks like</div><div><br class=""></div><div>> rewriterPlugin :: TyCon -> [TcType] -> TcPluginM (Maybe TcType)</div><div><br class=""></div><div>possibly with some other state passed in (including other constraints, if there is demand). The tycon would always be a type family, and the types would always exactly saturate the type family. Then, the plugin could reduce the type family if it knows how to do so. This seems to be a fairly simple interface and would be very, very easy to insert into the new infrastructure. (I'm a little worried about performance, because simplifying type families is code that's hammered on. But one step at a time.) Would that satisfy your need?</div><div><br class=""></div><div>Richard</div><br class=""><blockquote type="cite" class=""><div class=""><div dir="ltr" class=""><div class=""><br class=""></div><div class="">-- Christiaan<br class=""></div><div class=""><br class=""></div><div class=""><br class=""></div><div class=""><br class=""></div><div class=""><br class=""></div><div class=""><br class=""></div></div><br class=""><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Fri, 20 Nov 2020 at 20:43, Richard Eisenberg <<a href="mailto:rae@richarde.dev" class="">rae@richarde.dev</a>> wrote:<br class=""></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div style="overflow-wrap: break-word;" class=""><br class=""><div class=""><br class=""><blockquote type="cite" class=""><div class="">On Nov 19, 2020, at 12:40 PM, Iavor Diatchki <<a href="mailto:iavor.diatchki@gmail.com" target="_blank" class="">iavor.diatchki@gmail.com</a>> wrote:</div><br class=""><div class=""><div dir="ltr" class="">Hello,<div class=""><br class=""></div><div class="">I haven't worked on that stuff in Haskell for a long time, but here are some thoughts:</div><div class=""> - I think plugins should generally be agnostic to the form of the constraints they are given, thus flattening or not should not affect them---after all, the user might have written the constraints in the "flattened" form in the first place. So I think a plugin needs to convert the constraints to whatever form it assumes anyways.</div><div class=""> - I always thought that derived constraints were a pretty clever way for disseminating information in the constraint solver, is there a note somewhere on what's going to be the new mechanism?</div></div></div></blockquote><div class=""><br class=""></div><div class="">This Note (<a href="https://gitlab.haskell.org/ghc/ghc/-/blob/wip/derived-refactor/compiler/GHC/Tc/Types/Constraint.hs#L1678" target="_blank" class="">https://gitlab.haskell.org/ghc/ghc/-/blob/wip/derived-refactor/compiler/GHC/Tc/Types/Constraint.hs#L1678</a>) is the best I can offer, though it may be out of date. In the final version of the patch, that Note will naturally be updated. Essentially, the new plan is just to use Wanteds instead of Deriveds, which will achieve the same goal (but do not need to be distinct from Deriveds).</div><div class=""><br class=""></div><div class="">Richard</div><br class=""><blockquote type="cite" class=""><div class=""><div dir="ltr" class=""><div class=""><br class=""></div><div class="">-Iavor</div><div class=""><br class=""></div></div><br class=""><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, Nov 19, 2020 at 2:21 AM Christiaan Baaij <<a href="mailto:christiaan.baaij@gmail.com" target="_blank" class="">christiaan.baaij@gmail.com</a>> wrote:<br class=""></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr" class=""><div class="">I always forget what flattening did/does. Is it the thing where it turns a "complex" type family application:<br class=""><br class=""></div><div class="">F (G y) (H z) ~ a<br class=""></div><div class=""><br class=""></div><div class="">into:<br class=""><br class=""></div><div class="">G y ~ p</div><div class="">H z ~ q</div><div class="">F p q ~ a</div><div class=""><br class=""></div><div class="">?</div><div class=""><br class=""></div><div class="">If so, then I'm all for removing that. Since I actually wrote/hacked a function that "reverts" that process (for [G]ivens only): <a href="https://hackage.haskell.org/package/ghc-tcplugins-extra-0.4/docs/src/GHC.TcPluginM.Extra.html#flattenGivens" target="_blank" class="">https://hackage.haskell.org/package/ghc-tcplugins-extra-0.4/docs/src/GHC.TcPluginM.Extra.html#flattenGivens</a><br class=""></div><div class="">Which I use in all of my plugins. (PS it should perhaps be called "unflattenGiven"? like I said, I always get confused about flatten vs unflatten).</div></div><br class=""><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, 19 Nov 2020 at 05:20, Richard Eisenberg <<a href="mailto:rae@richarde.dev" target="_blank" class="">rae@richarde.dev</a>> wrote:<br class=""></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Hi all,<br class="">
<br class="">
I'm hard at work on two significant refactorings within GHC's constraint solver. The first is at <a href="https://gitlab.haskell.org/ghc/ghc/-/merge_requests/4149" rel="noreferrer" target="_blank" class="">https://gitlab.haskell.org/ghc/ghc/-/merge_requests/4149</a>. It removes flattening meta-variables and flattening skolems. This is a very nice simplification. Instead, it just reduces type families directly. My other patch (held up by the first) is at <a href="https://gitlab.haskell.org/ghc/ghc/-/tree/wip/derived-refactor" rel="noreferrer" target="_blank" class="">https://gitlab.haskell.org/ghc/ghc/-/tree/wip/derived-refactor</a> and will remove Derived constraints, to be replaced by a little bit of cleverness in suppressing certain confusing error messages. My guess is that either or both of these will invalidate the current behavior of type-checker plugins. Sadly, this is not just a case of finding a new function that replicates the old behavior -- enough is changing under the hood that you might actually have to rewrite chunks of your code.<br class="">
<br class="">
I have never written a type-checker plugin, and so I don't currently have advice for you. But if you are a plugin author affected by this change and want help, please reach out -- I would be happy to walk you through the changes, and then hopefully make a little video explaining the process to other plugin authors.<br class="">
<br class="">
Neither patch will make it for 9.0, but I expect both to be in 9.2. There may be more where this came from (<a href="https://gitlab.haskell.org/ghc/ghc/-/issues/18965" rel="noreferrer" target="_blank" class="">https://gitlab.haskell.org/ghc/ghc/-/issues/18965</a>) in the future, but it's all for a good cause.<br class="">
<br class="">
(I have bcc'd plugin authors that I'm aware of. Just adding this in case you're surprised at receiving this email.)<br class="">
<br class="">
Thanks,<br class="">
Richard</blockquote></div>
_______________________________________________<br class="">
ghc-devs mailing list<br class="">
<a href="mailto:ghc-devs@haskell.org" target="_blank" class="">ghc-devs@haskell.org</a><br class="">
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs" rel="noreferrer" target="_blank" class="">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs</a><br class="">
</blockquote></div>
</div></blockquote></div><br class=""></div></blockquote></div>
</div></blockquote></div><br class=""></body></html>