Iavor, Adam, Eric I’m happy with the general direction of the plugins stuff, so I’m mostly going to leave it to you guys to plough ahead; but I am happy to respond to questions. * I still think it would be better to provide an escape hatch to the TcS, not merely the TcM, alongside the nice TcPluginM wrapper. Notably, Simon's new TcFlatten.unflatten needs TcS... It think the only reason for this is that ‘unflatten’ needs to set evidence bindings, which in turn requires access to tcs_ev_binds. I think that everything else is in TcM. So I suppose you could carry around the EvBindsVar if you really didn’t want TcS. (And I can see why you wouldn’t; TcS has a lot of stuff you don’t need.) Simon From: Iavor Diatchki [mailto:iavor.diatchki@gmail.com] Sent: 10 November 2014 19:15 To: Adam Gundry Cc: ghc-devs@haskell.org; Simon Peyton Jones Subject: Re: Typechecker plugins: request for review and another workflow question Hi, On Mon, Nov 10, 2014 at 1:31 AM, Adam Gundry mailto:adam@well-typed.com> wrote: On the subject of that "nearly", I'm interested to learn whether you have a suggestion to deal with unflattening, because the interface still works with flat constraints only. Simon's changes should make it more practical to unflatten inside the plugin, but it would be far easier (at least for my purposes) if it was simply given unflattened constraints. I realise that this would require the plugin loop to be pushed further out, however, which has other difficulties. Not sure what to do about this. With the current setup, I think either way, the plugin would have to do some extract work. Perhaps we should run the plugins on the unflattened constraints, and leave to the plugins to manually temporarily "flatten" terms from external theories? For example, if the type-nat plugin saw `2 * F a ~ 4`, it could temporarily work with `2 * x ~ 4`, and then when it figures out that `x ~ 2`, it could emit `F a ~ 2` (non-canonical), which would go around again, and hopefully get fully simplified. A few other issues, of lesser importance: * I still think it would be better to provide an escape hatch to the TcS, not merely the TcM, alongside the nice TcPluginM wrapper. Notably, Simon's new TcFlatten.unflatten needs TcS... I don't mind that but, if I recall correctly, to do this without more recursive modules, we had to split `TCSMonad` in two parts, one with the types, and one with other stuff. Eric and I did this once, but we didn't commit it, because it seemed like an orthogonal change. * Is there a way for my plugin to "solve" a given constraint (e.g. to discard the uninformative "a * 1 ~ a")? Yes, you'd say something like: `TcPluginOK [(evidence, "a * 1 ~ a")] []` The first field of `TcPluginOK` are things that are solved, the second one is new work. * It is unfortunately easy to create infinite loops by writing plugins that emit wanteds but make no useful progress. Perhaps there should be a limit on the number of times round the loop (like SubGoalDepth but for all constraints)? Indeed, if a plugin keeps generating new work, we could go in a loop, so maybe a limit of some sort is useful. However, note that if the plugin generates things that are already in the inert set, GHC should notice this and filter them, so we won't keep going. * Perhaps runTcPlugin should skip invoking the plugin if there are no wanteds? Oh, there is an important detail here that needs documentation! GHC will call the plugin twice: once to improve the givens, and once to solve the wanteds. The way to distinguish the two is exactly by the presence of the wanteds. Why might you want to improve the givens? Suppose you had something like `x * 2 ~ 4` as a given: then you'd really want the plugin to generate another given: `x ~ 2`, as this is likely to help the rest of the constraint solving process. * The use of ctev_evar in runTcPlugin is partial, and fails with a nasty error if the plugin returns a non-wanted in the solved constraints list. Would it be worth catching this error and issuing a sensible message that chastises the plugin author appropriately? Aha, good idea. Bad plugin! :-) * Finally, I presume the comment on runTcPlugin that "The plugin is provided only with CTyEq and CFunEq constraints" is simply outdated and should be removed? Yep, thanks! Apologies for the deluge of questions - please take them as evidence of my eagerness to use this feature! Thanks for your feedback! Also, if you feel like doing some hacking please do so---I am quite busy at the moment so I don't have a ton of time to work on it, so any help you be most appreciated. I know Eric is also quite keen on helping out so we can just coordinate over e-mail. -Iavor

For what it's worth, I'd be very excited to have that feature in 7.10. Iavor, is there anywhere I can read on how to try your solver for type-level naturals? Francesco On 14 November 2014 18:14, Adam Gundry wrote:

Thanks, Simon! I've been convinced that TcS is more than we need, and I think the right thing to do is to (optionally) invoke the plugin after the constraints have been unflattened anyway. I've just pushed a commit to wip/tc-plugins-amg that does this. Iavor, Eric, your views on how convenient this alternative is would be most welcome. I'm also wondering if the plugin should be told how many times it has been called, to make it easier to prevent infinite loops.

I'm very keen to get this into 7.10, appropriately branded as a very experimental feature. Austin, have I sufficiently addressed your concerns about the hs-boot file and multiple flags? Is there anything else we need, apart perhaps from tests and documentation, which I'll put together next week?

Thanks,

Adam

On 12/11/14 11:16, Simon Peyton Jones wrote:

...

Iavor, Adam, Eric

I’m happy with the general direction of the plugins stuff, so I’m mostly going to leave it to you guys to plough ahead; but I am happy to respond to questions.

* I still think it would be better to provide an escape hatch to the TcS, not merely the TcM, alongside the nice TcPluginM wrapper. Notably, Simon's new TcFlatten.unflatten needs TcS...

It think the only reason for this is that ‘unflatten’ needs to set evidence bindings, which in turn requires access to tcs_ev_binds. I think that everything else is in TcM. So I suppose you could carry around the EvBindsVar if you really didn’t want TcS. (And I can see why you wouldn’t; TcS has a lot of stuff you don’t need.)

Simon

*From:*Iavor Diatchki [mailto:iavor.diatchki@gmail.com] *Sent:* 10 November 2014 19:15 *To:* Adam Gundry *Cc:* ghc-devs@haskell.org; Simon Peyton Jones *Subject:* Re: Typechecker plugins: request for review and another workflow question

Hi,

On Mon, Nov 10, 2014 at 1:31 AM, Adam Gundry mailto:adam@well-typed.com> wrote:

On the subject of that "nearly", I'm interested to learn whether you have a suggestion to deal with unflattening, because the interface still works with flat constraints only. Simon's changes should make it more practical to unflatten inside the plugin, but it would be far easier (at least for my purposes) if it was simply given unflattened constraints. I realise that this would require the plugin loop to be pushed further out, however, which has other difficulties.

Not sure what to do about this. With the current setup, I think either way, the plugin would have to do some extract work. Perhaps we should run the plugins on the unflattened constraints, and leave to the plugins to manually temporarily "flatten" terms from external theories? For example, if the type-nat plugin saw `2 * F a ~ 4`, it could temporarily work with `2 * x ~ 4`, and then when it figures out that `x ~ 2`, it could emit `F a ~ 2` (non-canonical), which would go around again, and hopefully get fully simplified.

A few other issues, of lesser importance:

* I still think it would be better to provide an escape hatch to the TcS, not merely the TcM, alongside the nice TcPluginM wrapper. Notably, Simon's new TcFlatten.unflatten needs TcS...

I don't mind that but, if I recall correctly, to do this without more recursive modules, we had to split `TCSMonad` in two parts, one with the types, and one with other stuff. Eric and I did this once, but we didn't commit it, because it seemed like an orthogonal change.

* Is there a way for my plugin to "solve" a given constraint (e.g. to discard the uninformative "a * 1 ~ a")?

Yes, you'd say something like: `TcPluginOK [(evidence, "a * 1 ~ a")] []`

The first field of `TcPluginOK` are things that are solved, the second one is new work.

* It is unfortunately easy to create infinite loops by writing plugins that emit wanteds but make no useful progress. Perhaps there should be a limit on the number of times round the loop (like SubGoalDepth but for all constraints)?

Indeed, if a plugin keeps generating new work, we could go in a loop, so maybe a limit of some sort is useful. However, note that if the plugin generates things that are already in the inert set, GHC should notice this and filter them, so we won't keep going.

* Perhaps runTcPlugin should skip invoking the plugin if there are no wanteds?

Oh, there is an important detail here that needs documentation! GHC will call the plugin twice: once to improve the givens, and once to solve the wanteds. The way to distinguish the two is exactly by the presence of the wanteds.

Why might you want to improve the givens? Suppose you had something like `x * 2 ~ 4` as a given: then you'd really want the plugin to generate another given: `x ~ 2`, as this is likely to help the rest of the constraint solving process.

* The use of ctev_evar in runTcPlugin is partial, and fails with a nasty error if the plugin returns a non-wanted in the solved constraints list. Would it be worth catching this error and issuing a sensible message that chastises the plugin author appropriately?

Aha, good idea. Bad plugin! :-)

* Finally, I presume the comment on runTcPlugin that "The plugin is provided only with CTyEq and CFunEq constraints" is simply outdated and should be removed?

Yep, thanks!

Apologies for the deluge of questions - please take them as evidence of my eagerness to use this feature!

Thanks for your feedback! Also, if you feel like doing some hacking please do so---I am quite busy at the moment so I don't have a ton of time to work on it, so any help you be most appreciated. I know Eric is also quite keen on helping out so we can just coordinate over e-mail.

-Iavor

-- Adam Gundry, Haskell Consultant Well-Typed LLP, http://www.well-typed.com/ _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs

On Nov 14, 2014, at 09:14, Adam Gundry wrote:

Thanks, Simon! I've been convinced that TcS is more than we need, and I think the right thing to do is to (optionally) invoke the plugin after the constraints have been unflattened anyway. I've just pushed a commit to wip/tc-plugins-amg that does this. Iavor, Eric, your views on how convenient this alternative is would be most welcome. I'm also wondering if the plugin should be told how many times it has been called, to make it easier to prevent infinite loops.

Thanks, I was just sitting down to figure out how to call the plugins with the unflattened constraints. Is there really a point though in calling the plugins with flattened and unflattened versions of the same constraints? Perhaps we should just settle on one or the other? I think Iavor and I are fine with only passing unflattened constraints to the plugins. It means a bit more work for the type-nat plugin, but shouldn't be a huge issue (I'll confirm this before next week). I don't think the plugins should be told how often they're being called, I'd prefer for GHC to track that and break the loop, if anything. I'm generally unconvinced that tracking the invocations is necessary at all though. The only way I can see an infinite loop occurring is if the plugins keep emitting *new* facts. Disregarding the possibility of a malicious plugin, that should mean that we're making progress towards a solution, right? Eric

Indeed, I spoke too soon. The type-nat plugin in fact causes an infinite loop when run on the unflattened constraints for one of our examples.. I think it would be reasonable for TcM to track how many times it has called the plugins and disable them after N iterations. But I don't know what would be a sensible default for N :/

On Nov 14, 2014, at 10:50, Iavor Diatchki wrote:

Hi,

depending on what the plugin does, it is not too hard to get into a loop. For example, the plugin could keep generating things like: x > 5, x + 1 > 5, x + 2 > 5, x + 3 > 5. Of course, this is not a good plan, but one has to be careful to avoid doing it accidentally. I think that a good general guideline for plugin behavior is like this:

- Avoid generating new variables - Only generate constrains of the form: `x = y` or `x = K`: these always make things more defined and could help another solver to make progress - These two ensure that eventually you will run out of new things to generate. - It is occasionally useful to also generate more complex equations: (e.g. x = y + 1), but then one needs to be careful to ensure progress.

Despite this, I also don't think that plugins need to be told how many times they've been called: it seems hard for a plugin author to know what to do with this number. Besides, a buggy plugin could also get stuck in loops in other ways (e.g., get stuck in some internal loop, without going back to GHC).

-Iavor

On Fri, Nov 14, 2014 at 10:09 AM, Eric Seidel wrote:

...

On Nov 14, 2014, at 09:14, Adam Gundry wrote:

Thanks, Simon! I've been convinced that TcS is more than we need, and I think the right thing to do is to (optionally) invoke the plugin after the constraints have been unflattened anyway. I've just pushed a commit to wip/tc-plugins-amg that does this. Iavor, Eric, your views on how convenient this alternative is would be most welcome. I'm also wondering if the plugin should be told how many times it has been called, to make it easier to prevent infinite loops.

Thanks, I was just sitting down to figure out how to call the plugins with the unflattened constraints. Is there really a point though in calling the plugins with flattened and unflattened versions of the same constraints? Perhaps we should just settle on one or the other? I think Iavor and I are fine with only passing unflattened constraints to the plugins. It means a bit more work for the type-nat plugin, but shouldn't be a huge issue (I'll confirm this before next week).

I don't think the plugins should be told how often they're being called, I'd prefer for GHC to track that and break the loop, if anything. I'm generally unconvinced that tracking the invocations is necessary at all though. The only way I can see an infinite loop occurring is if the plugins keep emitting *new* facts. Disregarding the possibility of a malicious plugin, that should mean that we're making progress towards a solution, right?

Eric

This looks excellent! Thank you Adam and Eric for helping Iavor with this. But I'm slightly confused by the git history since it seems to be cluttered with a few merges, and it seems like Eric has pushed the latest changes to all this. The branch is also a little bit behind master too. Iavor, would you like to: 1) Incorporate all of the changes from Eric and Adam, 2) Rebase your work on HEAD so we can read it in a digestible way? I still need to read over all the changes since my first review, since Adam addressed them. The 7.10 branch is at the end of this week, but this would be a really cool feature to have. Thanks! The branch for 7.10 is now the end of this week! It would be nice to get this in On Sun, Nov 16, 2014 at 1:33 PM, Eric Seidel wrote:

Hi Adam,

I've made a few changes based on your branch. Specifically I've removed the call to runTcPlugins inside solveFlats, and have replaced it with a specific runTcPluginsGiven that runs in a loop inside solveFlatsGiven much like your runTcPluginsFinal runs inside solveFlatsWanted. I think this is a bit cleaner given that you've split the wanteds-solving out already.

The changes are at https://github.com/gridaphobe/ghc/tree/wip/tc-plugins-els since I don't have commit access to GHC :)

Iavor and I also have a question about your change to the last statement in solveFlatWanteds. You're putting the unsolved wanteds in a field called wc_flat, which suggests that they ought to be flattened. But the unsolved wanteds were just unflattened a few lines above! Is this a problem, or is the wc_flat field in need of a new name? :)

Eric

...

On Nov 14, 2014, at 09:14, Adam Gundry wrote:

Thanks, Simon! I've been convinced that TcS is more than we need, and I think the right thing to do is to (optionally) invoke the plugin after the constraints have been unflattened anyway. I've just pushed a commit to wip/tc-plugins-amg that does this. Iavor, Eric, your views on how convenient this alternative is would be most welcome. I'm also wondering if the plugin should be told how many times it has been called, to make it easier to prevent infinite loops.

I'm very keen to get this into 7.10, appropriately branded as a very experimental feature. Austin, have I sufficiently addressed your concerns about the hs-boot file and multiple flags? Is there anything else we need, apart perhaps from tests and documentation, which I'll put together next week?

Thanks,

Adam

On 12/11/14 11:16, Simon Peyton Jones wrote:

...

Iavor, Adam, Eric

I’m happy with the general direction of the plugins stuff, so I’m mostly going to leave it to you guys to plough ahead; but I am happy to respond to questions.

* I still think it would be better to provide an escape hatch to the TcS, not merely the TcM, alongside the nice TcPluginM wrapper. Notably, Simon's new TcFlatten.unflatten needs TcS...

It think the only reason for this is that ‘unflatten’ needs to set evidence bindings, which in turn requires access to tcs_ev_binds. I think that everything else is in TcM. So I suppose you could carry around the EvBindsVar if you really didn’t want TcS. (And I can see why you wouldn’t; TcS has a lot of stuff you don’t need.)

Simon

*From:*Iavor Diatchki [mailto:iavor.diatchki@gmail.com] *Sent:* 10 November 2014 19:15 *To:* Adam Gundry *Cc:* ghc-devs@haskell.org; Simon Peyton Jones *Subject:* Re: Typechecker plugins: request for review and another workflow question

Hi,

On Mon, Nov 10, 2014 at 1:31 AM, Adam Gundry mailto:adam@well-typed.com> wrote:

On the subject of that "nearly", I'm interested to learn whether you have a suggestion to deal with unflattening, because the interface still works with flat constraints only. Simon's changes should make it more practical to unflatten inside the plugin, but it would be far easier (at least for my purposes) if it was simply given unflattened constraints. I realise that this would require the plugin loop to be pushed further out, however, which has other difficulties.

Not sure what to do about this. With the current setup, I think either way, the plugin would have to do some extract work. Perhaps we should run the plugins on the unflattened constraints, and leave to the plugins to manually temporarily "flatten" terms from external theories? For example, if the type-nat plugin saw `2 * F a ~ 4`, it could temporarily work with `2 * x ~ 4`, and then when it figures out that `x ~ 2`, it could emit `F a ~ 2` (non-canonical), which would go around again, and hopefully get fully simplified.

A few other issues, of lesser importance:

* I still think it would be better to provide an escape hatch to the TcS, not merely the TcM, alongside the nice TcPluginM wrapper. Notably, Simon's new TcFlatten.unflatten needs TcS...

I don't mind that but, if I recall correctly, to do this without more recursive modules, we had to split `TCSMonad` in two parts, one with the types, and one with other stuff. Eric and I did this once, but we didn't commit it, because it seemed like an orthogonal change.

* Is there a way for my plugin to "solve" a given constraint (e.g. to discard the uninformative "a * 1 ~ a")?

Yes, you'd say something like: `TcPluginOK [(evidence, "a * 1 ~ a")] []`

The first field of `TcPluginOK` are things that are solved, the second one is new work.

* It is unfortunately easy to create infinite loops by writing plugins that emit wanteds but make no useful progress. Perhaps there should be a limit on the number of times round the loop (like SubGoalDepth but for all constraints)?

Indeed, if a plugin keeps generating new work, we could go in a loop, so maybe a limit of some sort is useful. However, note that if the plugin generates things that are already in the inert set, GHC should notice this and filter them, so we won't keep going.

* Perhaps runTcPlugin should skip invoking the plugin if there are no wanteds?

Oh, there is an important detail here that needs documentation! GHC will call the plugin twice: once to improve the givens, and once to solve the wanteds. The way to distinguish the two is exactly by the presence of the wanteds.

Why might you want to improve the givens? Suppose you had something like `x * 2 ~ 4` as a given: then you'd really want the plugin to generate another given: `x ~ 2`, as this is likely to help the rest of the constraint solving process.

* The use of ctev_evar in runTcPlugin is partial, and fails with a nasty error if the plugin returns a non-wanted in the solved constraints list. Would it be worth catching this error and issuing a sensible message that chastises the plugin author appropriately?

Aha, good idea. Bad plugin! :-)

* Finally, I presume the comment on runTcPlugin that "The plugin is provided only with CTyEq and CFunEq constraints" is simply outdated and should be removed?

Yep, thanks!

Apologies for the deluge of questions - please take them as evidence of my eagerness to use this feature!

Thanks for your feedback! Also, if you feel like doing some hacking please do so---I am quite busy at the moment so I don't have a ton of time to work on it, so any help you be most appreciated. I know Eric is also quite keen on helping out so we can just coordinate over e-mail.

-Iavor

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

-- Regards, Austin Seipp, Haskell Consultant Well-Typed LLP, http://www.well-typed.com/

Yes, that would be ideal, and it can built/test it for you. This is all enough for one patch I imagine, which should be pretty easy to rebase locally, then submit with `arc diff`. On Mon, Nov 17, 2014 at 9:54 AM, Eric Seidel wrote:

Would it easier to send the diff to Phab? I don't think the git history will be particularly illuminating.

On Mon, Nov 17, 2014, at 07:45, Austin Seipp wrote:

...

This looks excellent! Thank you Adam and Eric for helping Iavor with this.

But I'm slightly confused by the git history since it seems to be cluttered with a few merges, and it seems like Eric has pushed the latest changes to all this. The branch is also a little bit behind master too.

Iavor, would you like to:

1) Incorporate all of the changes from Eric and Adam, 2) Rebase your work on HEAD so we can read it in a digestible way?

I still need to read over all the changes since my first review, since Adam addressed them. The 7.10 branch is at the end of this week, but this would be a really cool feature to have.

Thanks!

The branch for 7.10 is now the end of this week! It would be nice to get this in

On Sun, Nov 16, 2014 at 1:33 PM, Eric Seidel wrote:

...

Hi Adam,

I've made a few changes based on your branch. Specifically I've removed the call to runTcPlugins inside solveFlats, and have replaced it with a specific runTcPluginsGiven that runs in a loop inside solveFlatsGiven much like your runTcPluginsFinal runs inside solveFlatsWanted. I think this is a bit cleaner given that you've split the wanteds-solving out already.

The changes are at https://github.com/gridaphobe/ghc/tree/wip/tc-plugins-els since I don't have commit access to GHC :)

Iavor and I also have a question about your change to the last statement in solveFlatWanteds. You're putting the unsolved wanteds in a field called wc_flat, which suggests that they ought to be flattened. But the unsolved wanteds were just unflattened a few lines above! Is this a problem, or is the wc_flat field in need of a new name? :)

Eric

...

On Nov 14, 2014, at 09:14, Adam Gundry wrote:

Thanks, Simon! I've been convinced that TcS is more than we need, and I think the right thing to do is to (optionally) invoke the plugin after the constraints have been unflattened anyway. I've just pushed a commit to wip/tc-plugins-amg that does this. Iavor, Eric, your views on how convenient this alternative is would be most welcome. I'm also wondering if the plugin should be told how many times it has been called, to make it easier to prevent infinite loops.

I'm very keen to get this into 7.10, appropriately branded as a very experimental feature. Austin, have I sufficiently addressed your concerns about the hs-boot file and multiple flags? Is there anything else we need, apart perhaps from tests and documentation, which I'll put together next week?

Thanks,

Adam

On 12/11/14 11:16, Simon Peyton Jones wrote:

...

Iavor, Adam, Eric

I’m happy with the general direction of the plugins stuff, so I’m mostly going to leave it to you guys to plough ahead; but I am happy to respond to questions.

* I still think it would be better to provide an escape hatch to the TcS, not merely the TcM, alongside the nice TcPluginM wrapper. Notably, Simon's new TcFlatten.unflatten needs TcS...

It think the only reason for this is that ‘unflatten’ needs to set evidence bindings, which in turn requires access to tcs_ev_binds. I think that everything else is in TcM. So I suppose you could carry around the EvBindsVar if you really didn’t want TcS. (And I can see why you wouldn’t; TcS has a lot of stuff you don’t need.)

Simon

*From:*Iavor Diatchki [mailto:iavor.diatchki@gmail.com] *Sent:* 10 November 2014 19:15 *To:* Adam Gundry *Cc:* ghc-devs@haskell.org; Simon Peyton Jones *Subject:* Re: Typechecker plugins: request for review and another workflow question

Hi,

On Mon, Nov 10, 2014 at 1:31 AM, Adam Gundry mailto:adam@well-typed.com> wrote:

On the subject of that "nearly", I'm interested to learn whether you have a suggestion to deal with unflattening, because the interface still works with flat constraints only. Simon's changes should make it more practical to unflatten inside the plugin, but it would be far easier (at least for my purposes) if it was simply given unflattened constraints. I realise that this would require the plugin loop to be pushed further out, however, which has other difficulties.

Not sure what to do about this. With the current setup, I think either way, the plugin would have to do some extract work. Perhaps we should run the plugins on the unflattened constraints, and leave to the plugins to manually temporarily "flatten" terms from external theories? For example, if the type-nat plugin saw `2 * F a ~ 4`, it could temporarily work with `2 * x ~ 4`, and then when it figures out that `x ~ 2`, it could emit `F a ~ 2` (non-canonical), which would go around again, and hopefully get fully simplified.

A few other issues, of lesser importance:

* I still think it would be better to provide an escape hatch to the TcS, not merely the TcM, alongside the nice TcPluginM wrapper. Notably, Simon's new TcFlatten.unflatten needs TcS...

I don't mind that but, if I recall correctly, to do this without more recursive modules, we had to split `TCSMonad` in two parts, one with the types, and one with other stuff. Eric and I did this once, but we didn't commit it, because it seemed like an orthogonal change.

* Is there a way for my plugin to "solve" a given constraint (e.g. to discard the uninformative "a * 1 ~ a")?

Yes, you'd say something like: `TcPluginOK [(evidence, "a * 1 ~ a")] []`

The first field of `TcPluginOK` are things that are solved, the second one is new work.

* It is unfortunately easy to create infinite loops by writing plugins that emit wanteds but make no useful progress. Perhaps there should be a limit on the number of times round the loop (like SubGoalDepth but for all constraints)?

Indeed, if a plugin keeps generating new work, we could go in a loop, so maybe a limit of some sort is useful. However, note that if the plugin generates things that are already in the inert set, GHC should notice this and filter them, so we won't keep going.

* Perhaps runTcPlugin should skip invoking the plugin if there are no wanteds?

Oh, there is an important detail here that needs documentation! GHC will call the plugin twice: once to improve the givens, and once to solve the wanteds. The way to distinguish the two is exactly by the presence of the wanteds.

Why might you want to improve the givens? Suppose you had something like `x * 2 ~ 4` as a given: then you'd really want the plugin to generate another given: `x ~ 2`, as this is likely to help the rest of the constraint solving process.

* The use of ctev_evar in runTcPlugin is partial, and fails with a nasty error if the plugin returns a non-wanted in the solved constraints list. Would it be worth catching this error and issuing a sensible message that chastises the plugin author appropriately?

Aha, good idea. Bad plugin! :-)

* Finally, I presume the comment on runTcPlugin that "The plugin is provided only with CTyEq and CFunEq constraints" is simply outdated and should be removed?

Yep, thanks!

Apologies for the deluge of questions - please take them as evidence of my eagerness to use this feature!

Thanks for your feedback! Also, if you feel like doing some hacking please do so---I am quite busy at the moment so I don't have a ton of time to work on it, so any help you be most appreciated. I know Eric is also quite keen on helping out so we can just coordinate over e-mail.

-Iavor

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

-- Regards,

Austin Seipp, Haskell Consultant Well-Typed LLP, http://www.well-typed.com/

-- Regards, Austin Seipp, Haskell Consultant Well-Typed LLP, http://www.well-typed.com/

Thanks Eric! On 16/11/14 19:33, Eric Seidel wrote:

I've made a few changes based on your branch. Specifically I've removed the call to runTcPlugins inside solveFlats, and have replaced it with a specific runTcPluginsGiven that runs in a loop inside solveFlatsGiven much like your runTcPluginsFinal runs inside solveFlatsWanted. I think this is a bit cleaner given that you've split the wanteds-solving out already.

The changes are at https://github.com/gridaphobe/ghc/tree/wip/tc-plugins-els since I don't have commit access to GHC

I agree that it's better to split these out separately, if you and Iavor are happy to work with only the unflattened constraints. I'm not completely convinced by how solveFlatGivens/runTcPluginsGiven work now though. It seems slightly odd that solveFlatGivens calls solveFlats and runTcPluginsGiven with the same set of givens, even though solveFlats might have simplified/discarded some. Also, if I understand correctly, when a plugin generates new facts, those will be added to the worklist directly, but also passed back in the result Cts to be added to the worklist again. In the solveFlatWanteds case, new facts are added to the worklist but not the result Cts, which is fine. Finally, I think the plugin should be allowed to "solve" given constraints, just by discarding them (e.g. if the constraint is something like "1 * x ~ x"). It's slightly odd that the interface requires the plugin to provide an evidence term in this case, but the evidence associated with the CtGiven (ctev_evtm) will do. I'll put some commits together shortly to address these fine details.

Iavor and I also have a question about your change to the last statement in solveFlatWanteds. You're putting the unsolved wanteds in a field called wc_flat, which suggests that they ought to be flattened. But the unsolved wanteds were just unflattened a few lines above! Is this a problem, or is the wc_flat field in need of a new name? :)

This is a slightly unfortunate clash of terminology. I believe wc_flat is so named because the constraints are flat in the sense of "not implications" rather than "contain no type family applications". This is also the reason for the name "solveFlats". Adam -- Adam Gundry, Haskell Consultant Well-Typed LLP, http://www.well-typed.com/

I think we're converging on a reasonable story about the way to call plugins for givens and for wanteds; it's a shame they don't quite match up, but I think that is probably unavoidable and relatively harmless. On 17/11/14 17:11, Eric Seidel wrote:

Ah, good catch on both accounts, thanks!

Re "solving" givens: although the interface requires the plugins to provide an evidence term, the end result would be that the given is discarded entirely, correct? If so, we should probably caution plugin authors not to solve any givens they can't easily re-derive later, but perhaps this is obvious.. Apart from that concern, it seems reasonable, and could potentially reduce the amount of work GHC has to do.

Yes, that's right, it makes sense to discard a given only if it can be re-derived (and hence is providing no new information). This happens in the vanilla constraint solver, for example reflexive given equations are discarded. When reporting errors, it's nice to omit obviously boring constraints!

Ping me if you want to offload any work, I'm also very keen to get this landed before the 7.10 branch!

I'd be very grateful if you could try out my latest commit to wip/tc-plugins-amg and tell me if it makes sense or if I'm doing something silly. The code could do with a bit of tidying up, including cleaning up the diff to master, which I'll try to get done tomorrow, unless you want to jump in first. ;-) Cheers, Adam

On Mon, Nov 17, 2014, at 08:36, Adam Gundry wrote:

...

Thanks Eric!

On 16/11/14 19:33, Eric Seidel wrote:

...

I've made a few changes based on your branch. Specifically I've removed the call to runTcPlugins inside solveFlats, and have replaced it with a specific runTcPluginsGiven that runs in a loop inside solveFlatsGiven much like your runTcPluginsFinal runs inside solveFlatsWanted. I think this is a bit cleaner given that you've split the wanteds-solving out already.

The changes are at https://github.com/gridaphobe/ghc/tree/wip/tc-plugins-els since I don't have commit access to GHC

I agree that it's better to split these out separately, if you and Iavor are happy to work with only the unflattened constraints. I'm not completely convinced by how solveFlatGivens/runTcPluginsGiven work now though. It seems slightly odd that solveFlatGivens calls solveFlats and runTcPluginsGiven with the same set of givens, even though solveFlats might have simplified/discarded some.

Also, if I understand correctly, when a plugin generates new facts, those will be added to the worklist directly, but also passed back in the result Cts to be added to the worklist again. In the solveFlatWanteds case, new facts are added to the worklist but not the result Cts, which is fine.

Finally, I think the plugin should be allowed to "solve" given constraints, just by discarding them (e.g. if the constraint is something like "1 * x ~ x"). It's slightly odd that the interface requires the plugin to provide an evidence term in this case, but the evidence associated with the CtGiven (ctev_evtm) will do.

I'll put some commits together shortly to address these fine details.

...

Iavor and I also have a question about your change to the last statement in solveFlatWanteds. You're putting the unsolved wanteds in a field called wc_flat, which suggests that they ought to be flattened. But the unsolved wanteds were just unflattened a few lines above! Is this a problem, or is the wc_flat field in need of a new name? :)

This is a slightly unfortunate clash of terminology. I believe wc_flat is so named because the constraints are flat in the sense of "not implications" rather than "contain no type family applications". This is also the reason for the name "solveFlats".

Adam

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

On Nov 10, 2014, at 09:46, Adam Gundry wrote:

On 10/11/14 15:58, Austin Seipp wrote:

...

- 2) I am kind of not a fan of having separate 'plugins for core2core' and 'plugins for typechecking' flags, AKA -ftc-plugin and -fplugin. Ideally I would think all plugins could be uniformly specified by simply saying '-fplugin'. This mostly avoids the need for duplication and a naming convention/slew of flags for each case (which we have to catalog and document). There may be an easy way to make this the case; I haven't looked closely yet (it has been some time since I starred at the plugin code, even though Max wrote it and I helped get it merged!)

FWIW, I originally envisaged reusing the existing plugins machinery, and I don't think there are any great problems in doing so (see https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker). In fact, I had an early implementation of typechecker plugins that did exactly this.

I have been wondering, however, about another possible approach. We could:

1. make the constraint solver changes use a *hook*, instead of the plugins directly, and

2. make it possible for plugins to install/modify hooks at some suitable point in the compilation pipeline.

I don't know the hooks machinery very well, but if this is feasible it seems like it would provide more power (plugins could modify any part of GHC for which a hook is available) and avoid having multiple overlapping ways of extending GHC. In the future, I can imagine wanting plugins to hook into other parts of GHC (e.g. error message postprocessing for domain-specific error reporting), and this seems like a good way to achieve that.

I think we could merge the TcPlugin type into the existing Plugin type without much difficulty, but I also agree that combining both plugin types with Hooks to present a more uniform interface would be nice. Eric

I've just pushed wip/tc-plugins-amg, in which I remove the hs-boot file and unify the core2core and typechecker plugins under a single -fplugin flag. This did involve making a separate module for plugins, which I think is probably a good thing. I looked at using a hook instead, with a plugin to modify hooks, but I'm not sure exactly where such a plugin should be invoked. Ideally we want the typechecker modifications to work on a per-module basis, but most of the hooks seem to have a wider scope than that. Adam On 11/11/14 03:08, Eric Seidel wrote:

...

On Nov 10, 2014, at 07:58, Austin Seipp wrote:

Hi Iavor;

I took a very, very cursory glance. Naturally I am not a typechecker guru, but I did look over the mechanical changes/extensions to thread things around. Two things popped out to me:

- 1) Ugh, a new .hs-boot file. I assume this wasn't added without good reason, but ideally we would be eliminating them quicker than we add them. :) I want to take a closer look at this; perhaps we can refactor something for you to remove the need for this.

- 2) I am kind of not a fan of having separate 'plugins for core2core' and 'plugins for typechecking' flags, AKA -ftc-plugin and -fplugin. Ideally I would think all plugins could be uniformly specified by simply saying '-fplugin'. This mostly avoids the need for duplication and a naming convention/slew of flags for each case (which we have to catalog and document). There may be an easy way to make this the case; I haven't looked closely yet (it has been some time since I starred at the plugin code, even though Max wrote it and I helped get it merged!)

I looked into this again a bit today and recall now why we made a separate Plugin type and flag; adding the TcPlugin to the existing Plugin type defined in CoreMonad creates a circular dependency between CoreMonad and TcRnTypes.

We could (and perhaps should) move all of the plugin types into a separate module, but that would require pulling other types (e.g. CoreToDo) out of CoreMonad to break the circularity.

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

Hi, thanks Adam! I merged your changes into `wip/tc-plugin` and updated the type-nats plugin to work with the new plugin interface. -Iavor PS: It looks like `Plugins` was already in ghc.cabal.in and things worked form me. Maybe the problem was a stale ghc.cabal? On Tue, Nov 11, 2014 at 9:49 AM, Eric Seidel wrote:

...

On Nov 11, 2014, at 04:19, Adam Gundry wrote:

I've just pushed wip/tc-plugins-amg, in which I remove the hs-boot file and unify the core2core and typechecker plugins under a single -fplugin flag. This did involve making a separate module for plugins, which I think is probably a good thing.

Thanks! I just checked out your branch, but had to add `Plugins` to the list of exposed modules in ghc.cabal in order to actually use a plugin though. Otherwise I get a horrible

Symbol not found: _ghc_Plugins_Plugin_con_info

error from the linker when I try to compile a module with -fplugin=MyPlugin.

...

I looked at using a hook instead, with a plugin to modify hooks, but I'm not sure exactly where such a plugin should be invoked. Ideally we want the typechecker modifications to work on a per-module basis, but most of the hooks seem to have a wider scope than that.

Well, I think we want the option to decide between per-module and global invocation of plugins, e.g. if I pass -fplugin on the command-line then I would expect ghc to use the plugin for *any* module it ends up compiling.

The list of plugins to enable is in the DynFlags, which suggests to me that GHC must compile each module with a specific set of DynFlags, based on the LANGUAGE and OPTIONS_GHC pragmas. The Hooks are also in the DynFlags, so perhaps all we need to do is make -fplugin add a Hook, and let GHC's existing machinery take care of the rest?

Eric