Typechecker plugin proposal, ticket #15147

[Christiaan Baaij]

I actually have conflicting needs:
1. ghc-typelits-natnormalise, a solver for type-level Nat equations, would
benefits from both unflattened givens and unflattened wanteds!
Why unflattened givens? because from `[G] 2*x + a ~ 2*x + b` I can derive
`a ~ b`
Which I could then use to solve: [W] 3*y + a ~ 3*y + b

So for both givens and wanteds I want unflattened constraints, because my
simplifier "simplifies" by eliminating equal terms on either side of the '~'
I actually had to write my own unflattening function for givens.

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.
So if I could be kept in the loop, and test an API with flattened wanteds
early, I could give more feedback on that.

2. ghc-typelits-knownnat, this solves complicated knownnat constraints from
simpler ones.
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.
Again, here I benifit from unflattened wanteds because I see [W] KnownNat
(a + b), instead of [W] KnownNat fmv

3. ghc-typelits-extra, adds additional operations on types of kind Nat,
e.g. LogBase.
This one probably benifits from flattened wanteds, so I can solve one
"magic" type family at a time.

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.


On Mon, 2 Mar 2020 at 21:20, Nicolas Frisby <nicolas.frisby at gmail.com>
wrote:

> If you know of any typechecker plugin authors I've missed, please add them
> to the thread.
>
> In the comments of ticket https://gitlab.haskell.org/ghc/ghc/issues/15147
> 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.
>
> 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?
>
> 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.
>
> Thank you for your time. -Nick
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20200306/614433a6/attachment.html>