<div dir="ltr"><div>I actually have conflicting needs:</div><div>1. ghc-typelits-natnormalise, a solver for type-level Nat equations, would benefits from both unflattened givens and unflattened wanteds!</div><div>Why unflattened givens? because from `[G] 2*x + a ~ 2*x + b` I can derive `a ~ b`</div><div>Which I could then use to solve: [W] 3*y + a ~ 3*y + b</div><div><br></div><div>So for both givens and wanteds I want unflattened constraints, because my simplifier "simplifies" by eliminating equal terms on either side of the '~'</div><div>I actually had to write my own unflattening function for givens.</div><div><br></div><div>Now, if flattened wanteds would mean that a single unflattened `
[W] 3*y + a ~ 3*y + b` is split up into multiple flattened wanteds, that could complicate ghc-typelits-natnormalise, although I cannot be sure.</div><div>So if I could be kept in the loop, and test an API with flattened wanteds early, I could give more feedback on that.</div><div><br></div><div>2. ghc-typelits-knownnat, this solves complicated knownnat constraints from simpler ones.</div><div>e.g. given [G] KnownNat a, [G] KnownNat b, and a [W] KnownNat (a + b), it can create that dictionary using some "magic" dictionary functions.</div><div>Again, here I benifit from unflattened wanteds because I see [W] KnownNat (a + b), instead of [W] KnownNat fmv</div><div><br></div><div>3. ghc-typelits-extra, adds additional operations on types of kind Nat, e.g. LogBase.</div><div>This one probably benifits from flattened wanteds, so I can solve one "magic" type family at a time.</div><div><br></div><div>So if I'd had to hazard a guess, I think I'd want to receive my wanteds as an "Either [flattened] [unflattened]" and then return a "Solved (Either [flattened] [unflattened])" as well.<br></div><div><br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Mon, 2 Mar 2020 at 21:20, Nicolas Frisby <<a href="mailto:nicolas.frisby@gmail.com">nicolas.frisby@gmail.com</a>> wrote:<br></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="auto"><div dir="auto">If you know of any typechecker plugin authors I've missed, please add them to the thread.</div><div dir="auto"><br></div>In the comments of ticket <a href="https://gitlab.haskell.org/ghc/ghc/issues/15147" target="_blank">https://gitlab.haskell.org/ghc/ghc/issues/15147</a> several of us agreed that the behavior of the typechecker plugin interface should change: GHC should no longer unflatten the fmvs in the Wanteds before passing them to the plugin.<div dir="auto"><br></div><div dir="auto">This is presumably a breaking change to plugins. We might be able to get by with some sort of flag indicating if the plugin expects the Wanteds flattened or not, but ideally GHC would just always pass them flattened. I'm unaware of any established policy about interface changes at this level, whether we've somehow committed to backwards-compatibility here or not. Anyone know?</div><div dir="auto"><br></div><div dir="auto">Plugin authors: would you look over the ticket comments and share your thoughts here? We're looking to build some sort of consensus about how to proceed without shocking the API users.</div><div dir="auto"><br></div><div dir="auto">Thank you for your time. -Nick</div></div>
</blockquote></div>