PSA: type checker plugins to be affected by upcoming changes to GHC

Mon Nov 30 16:41:54 UTC 2020

Richard, I just watched your talk about simplifying the constraint solver:
https://www.youtube.com/watch?v=flwz6V5Ps8w
and then realised that no flattening at all means also no flattening of
[W]anteds.

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"
And then lets say we start out with an original [W]anted: Foo (Magic 8) ~
Bar 42

Then if I understand flattening correctly, that would get flattened to:
[w] Magic 8 ~ fmv1
[w] fmv1 ~ 42
[w] Foo fmv1 ~ fmv2
[w] fmv2 ~ Bar fmv1

Correct?

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

But in a version without flattening, all we would see is:
[W] Foo (Magic 8) ~ Foo 42

And all I can do is to traverse the entire [W]anted, look for type family
applications of "Magic" an then improve to:
[W] Foo 42 ~ Bar 42

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).
Currently, the API for constraint solving plugins allows me to return
_either_:
http://hackage.haskell.org/package/ghc-8.10.1/docs/TcRnTypes.html#t:TcPluginResult
A) A set of contradictions
B) A set of solved [W] constraints + A set of new [W] constraints

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

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.
If that's the case, how do you envision plugin writers interacting with the
solver?
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:
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".

-- Christiaan

On Fri, 20 Nov 2020 at 20:43, Richard Eisenberg <rae at richarde.dev> wrote:

>
>
> On Nov 19, 2020, at 12:40 PM, Iavor Diatchki <iavor.diatchki at gmail.com>
> wrote:
>
> Hello,
>
> I haven't worked on that stuff in Haskell for a long time, but here are
> some thoughts:
>   - 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.
>   - 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?
>
>
> This Note (
> https://gitlab.haskell.org/ghc/ghc/-/blob/wip/derived-refactor/compiler/GHC/Tc/Types/Constraint.hs#L1678)
> 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).
>
> Richard
>
>
> -Iavor
>
>
> On Thu, Nov 19, 2020 at 2:21 AM Christiaan Baaij <
> christiaan.baaij at gmail.com> wrote:
>
>> I always forget what flattening did/does. Is it the thing where it turns
>> a "complex" type family application:
>>
>> F (G y) (H z) ~ a
>>
>> into:
>>
>> G y ~ p
>> H z ~ q
>> F p q ~ a
>>
>> ?
>>
>> If so, then I'm all for removing that. Since I actually wrote/hacked a
>> function that "reverts" that process (for [G]ivens only):
>> https://hackage.haskell.org/package/ghc-tcplugins-extra-0.4/docs/src/GHC.TcPluginM.Extra.html#flattenGivens
>> 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).
>>
>> On Thu, 19 Nov 2020 at 05:20, Richard Eisenberg <rae at richarde.dev> wrote:
>>
>>> Hi all,
>>>
>>> I'm hard at work on two significant refactorings within GHC's constraint
>>> solver. The first is at
>>> https://gitlab.haskell.org/ghc/ghc/-/merge_requests/4149. 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
>>> https://gitlab.haskell.org/ghc/ghc/-/tree/wip/derived-refactor 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.
>>>
>>> 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.
>>>
>>> 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 (
>>> https://gitlab.haskell.org/ghc/ghc/-/issues/18965) in the future, but
>>> it's all for a good cause.
>>>
>>> (I have bcc'd plugin authors that I'm aware of. Just adding this in case
>>> you're surprised at receiving this email.)
>>>
>>> Thanks,
>>> Richard
>>
>> _______________________________________________
>> ghc-devs mailing list
>> ghc-devs at haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20201130/a2c664aa/attachment.html>