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

[Richard Eisenberg]

> On Nov 30, 2020, at 3:50 PM, Christiaan Baaij  
> wrote:
> 
> It seems like a function like `rewritePlugin` is something we could/should 
> just build on top of the existing plugin mechanism, and have something along 
> the line of:
> 
> > -- | Create a 'TcPluginSolver' from the provided rewrite function
> > rewritePluginSolver ::
> >   (s -> TyCon -> [TcType] -> TcPluginM (Maybe TcType)) -> 
> >   (s -> TcPluginSolver) <>
> 
> where `rewritePlugin` just traverses constraints with the given rewrite and 
> creates the evidence, emits new wanteds, etc.
> (We could develop such a function outside of the `ghc` package, and only once 
> we have a satisfactory solution, perhaps consider it for inclusion in the 
> `ghc` package.)
> This way, we won't have to make the common case of simplifying type families 
> slow, and still provide a straightforward API.

Ooh. I like that idea. Much more orthogonal than mine. It would mean, though, 
that a plugin that needs to reduce lots of type families is slower than it 
needs to be. (That is, my idea is slower in the common case of doing most type 
family reduction within GHC, but faster in the case where more type family 
reduction is done by plugin.) In any case, it would make a nice stepping stone 
for the future.

If you (for any value of you) get all the infrastructure settled, I'll happily 
contribute the implementation of that particular function. It would be nice if 
the infrastructure allows me to test, as I'll surely get it wrong a few times 
before getting it right.

Richard

___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

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

[Christiaan Baaij]

Sorry for my mistakes. It is as you said, I changed the example, but didn't
properly follow through in the rest of the email.

I'm glad I've understood the intended interaction with the constraint
solver correctly then.
(With regard to the coercion... I usually just end up using UnivCo...)

It seems like a function like `rewritePlugin` is something we could/should
just build on top of the existing plugin mechanism, and have something
along the line of:

> -- | Create a 'TcPluginSolver' from the provided rewrite function
> rewritePluginSolver ::
>   (s -> TyCon -> [TcType] -> TcPluginM (Maybe TcType)) ->
>   (s -> TcPluginSolver)

where `rewritePlugin` just traverses constraints with the given rewrite and
creates the evidence, emits new wanteds, etc.
(We could develop such a function outside of the `ghc` package, and only
once we have a satisfactory solution, perhaps consider it for inclusion in
the `ghc` package.)
This way, we won't have to make the common case of simplifying type
families slow, and still provide a straightforward API.



On Mon, 30 Nov 2020 at 20:03, Richard Eisenberg  wrote:

>
>
> On Nov 30, 2020, at 11:41 AM, Christiaan Baaij 
> wrote:
>
> 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.
>
>
> Yes, that's true.
>
>
> 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?
>
>
> I get
>
> [W] Magic 8 ~ fmv1
> [W] Foo fmv1 ~ fmv2
> [W] Bar 42 ~ fmv3
> [W] fmv2 ~ fmv3
>
>
> 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.
>
>
> 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.
>
>
> But in a version without flattening, all we would see is:
> [W] Foo (Magic 8) ~ Foo 42
>
>
> Did you mean [W] Foo (Magic 8) ~ Bar 42? Then, yes.
>
>
> 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"
>
>
> Yes, that's what you would do. Indeed, it's what GHC does whenever
> simplifying part of a Wanted.
>
> 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)
>
>
> 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):
>
> import GHC.Plugins
> import GHC.Tc.Utils.TcType
> import GHC.Tc.Types.Evidence
> import GHC.Tc.Types.Constraint
> import GHC.Tc.Plugin
>
> updateWantedType :: Ct-- initial constraint; always unsolved
> equality wanted
>   --   t1 ~N t2
>  -> TcPredType-- desired new constraint: s1 ~N s2
>  -> CoercionN -- lhs_co :: t1 ~N s1
>  -> CoercionN -- rhs_co :: t2 ~N s2
>  -> TcPluginM (Ct, EvTerm)  -- new constraint, evidence
> for *old* constraint
> -- NB: the *old* constraint is solved by the returned EvTerm;
> -- return the EvTerm with the *old* constraint in TcPluginOk
> updateWantedType old_ct new_pred lhs_co rhs_co = do
>   new_w <- newWanted (ctLoc old_ct) new_pred
>   let new_co = ctEvCoercion new_w-- :: s1 ~N s2
>   old_co = lhs_co `mkTransCo` new_co `mkTransCo` mkSymCo rhs_co
>   old_ev = evCoercion old_co
>   return (mkNonCanonical new_w, old_ev)
>
>
> That would seem to do the trick. This function is essentially 

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

[Richard Eisenberg]

> On Nov 30, 2020, at 11:41 AM, Christiaan Baaij  
> wrote:
> 
> 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.

Yes, that's true.

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

I get

[W] Magic 8 ~ fmv1
[W] Foo fmv1 ~ fmv2
[W] Bar 42 ~ fmv3
[W] fmv2 ~ fmv3

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

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.

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

Did you mean [W] Foo (Magic 8) ~ Bar 42? Then, yes.

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

Yes, that's what you would do. Indeed, it's what GHC does whenever simplifying 
part of a Wanted.

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

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

> import GHC.Plugins
> import GHC.Tc.Utils.TcType
> import GHC.Tc.Types.Evidence
> import GHC.Tc.Types.Constraint
> import GHC.Tc.Plugin
> 
> updateWantedType :: Ct-- initial constraint; always unsolved 
> equality wanted
>   --   t1 ~N t2
>  -> TcPredType-- desired new constraint: s1 ~N s2
>  -> CoercionN -- lhs_co :: t1 ~N s1
>  -> CoercionN -- rhs_co :: t2 ~N s2
>  -> TcPluginM (Ct, EvTerm)  -- new constraint, evidence for 
> *old* constraint
> -- NB: the *old* constraint is solved by the returned EvTerm;
> -- return the EvTerm with the *old* constraint in TcPluginOk
> updateWantedType old_ct new_pred lhs_co rhs_co = do
>   new_w <- newWanted (ctLoc old_ct) new_pred
>   let new_co = ctEvCoercion new_w-- :: s1 ~N s2
>   old_co = lhs_co `mkTransCo` new_co `mkTransCo` mkSymCo rhs_co
>   old_ev = evCoercion old_co
>   return (mkNonCanonical new_w, old_ev)

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.

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

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.

> If that's the case, how do you envision plugin writers interacting with the 
> solver?

As you've outlined above.

> 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 

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

[Christiaan Baaij]

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  wrote:

>
>
> On Nov 19, 2020, at 12:40 PM, Iavor Diatchki 
> 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.ba...@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  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 

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

[Richard Eisenberg]

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

___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

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

[Richard Eisenberg]

> On Nov 19, 2020, at 5:20 AM, Christiaan Baaij  
> 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  > 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@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

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

[Richard Eisenberg]

> On Nov 19, 2020, at 4:14 AM, Adam Gundry  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
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

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 
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  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@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

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

[Christiaan Baaij]

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  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@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

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

[Adam Gundry]

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
>  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
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

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

[Ben Gamari]

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  
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@haskell.org
>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
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs