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

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
8 messages Options
Reply | Threaded
Open this post in threaded view
|

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

Richard Eisenberg-5
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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

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

Ben Gamari-3
Iavor and Christiaan are two plugin authors that come to mind.

Ideally the patch would also include some migration documentation in the release notes.

Cheers,

- Ben

On November 18, 2020 11:20:40 PM EST, Richard Eisenberg <[hidden email]> 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

--
Sent from my Android device with K-9 Mail. Please excuse my brevity.
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

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

Adam Gundry-2
Thanks Richard!

I'm happy to see this as I've always felt the flattening story to be
unnecessarily complex for type-checker plugins, and in fact uom-plugin
has been broken for a long time because of a previous GHC change to
flattening skolems.[1,2] I haven't checked but I am moderately hopeful
your work will at least make it easier to fix, if not fix it outright.

As part of removing Deriveds, do you plan to change the type-checker
plugin interface to drop the redundant argument? Although I suppose GHC
could simply pass an empty list to the plugin.

Ideally we would have a spec (or at least some tests!) for what
constraints get presented to plugins. The current implementation is
rather dependent on whatever GHC's solver happens to produce. In my
paper [3] I tried to specify plugins based on the published description
of OutsideIn(X), but that's far enough from the reality of GHC that it
isn't much help in practice. (One point it lacks is any treatment of
Deriveds, so I'm happy to see them go!)

Cheers,

Adam

[1] https://github.com/adamgundry/uom-plugin/issues/43
[2] https://gitlab.haskell.org/ghc/ghc/-/issues/15147
[3] https://adam.gundry.co.uk/pub/typechecker-plugins/




On 19/11/2020 04:45, Ben Gamari wrote:

> Iavor and Christiaan are two plugin authors that come to mind.
>
> Ideally the patch would also include some migration documentation in the
> release notes.
>
> Cheers,
>
> - Ben
>
> On November 18, 2020 11:20:40 PM EST, Richard Eisenberg
> <[hidden email]> 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



--
Adam Gundry, Haskell Consultant
Well-Typed LLP, https://www.well-typed.com/

Registered in England & Wales, OC335890
118 Wymering Mansions, Wymering Road, London W9 2NF, England
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

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

Christiaan Baaij
In reply to this post by Richard Eisenberg-5
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 <[hidden email]> 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

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

Iavor Diatchki
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?

-Iavor


On Thu, Nov 19, 2020 at 2:21 AM Christiaan Baaij <[hidden email]> 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 <[hidden email]> 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

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

Richard Eisenberg-5
In reply to this post by Adam Gundry-2


On Nov 19, 2020, at 4:14 AM, Adam Gundry <[hidden email]> wrote:

As part of removing Deriveds, do you plan to change the type-checker
plugin interface to drop the redundant argument? Although I suppose GHC
could simply pass an empty list to the plugin.

No -- I think we'll just remove the unused parameter. So much is changing in this space that the tiny bit of back-compat leaving that parameter would grant is a false promise.


Ideally we would have a spec (or at least some tests!) for what
constraints get presented to plugins. The current implementation is
rather dependent on whatever GHC's solver happens to produce. In my
paper [3] I tried to specify plugins based on the published description
of OutsideIn(X), but that's far enough from the reality of GHC that it
isn't much help in practice. (One point it lacks is any treatment of
Deriveds, so I'm happy to see them go!)

Yes. But this is really hard, and it would likely make e.g. my simplifications harder to execute on. (That is, it would be nice, but it wouldn't be free.) I think that maintaining this would require the extra labor of someone more familiar with the world of plugins... :)

Richard

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

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

Richard Eisenberg-5
In reply to this post by Christiaan Baaij


On Nov 19, 2020, at 5:20 AM, Christiaan Baaij <[hidden email]> 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

?

Yes, but it's worse. It would actually leave us with

G y ~ p
H z ~ q
F p q ~ r
r ~ 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).

Yes, this would be unflattening.

Glad to know this would work well with your plugins. :)

Richard


On Thu, 19 Nov 2020 at 05:20, Richard Eisenberg <[hidden email]> 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

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

Richard Eisenberg-5
In reply to this post by Iavor Diatchki


On Nov 19, 2020, at 12:40 PM, Iavor Diatchki <[hidden email]> 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 <[hidden email]> 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 <[hidden email]> 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs