Implement typechecker plugins
ClosedPublic

Authored by adamgundry on Nov 18 2014, 6:55 AM.

Details

Summary

See https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker

This is based on work by Iavor Diatchki and Eric Seidel.

Test Plan

validate

Diff Detail

Repository
rGHC Glasgow Haskell Compiler
Lint
Automatic diff as part of commit; lint not applicable.
Unit
Automatic diff as part of commit; unit tests not applicable.
adamgundry retitled this revision from to Implement typechecker plugins.Nov 18 2014, 6:55 AM
adamgundry updated this object.
adamgundry edited the test plan for this revision. (Show Details)
adamgundry added reviewers: austin, simonpj.

The build passes apart from one failing test, which is broken on master (see 2a6f193).

yav added a subscriber: yav.EditedNov 18 2014, 10:20 AM

Hello,

Here are some things we may want to change:

  1. I think the changes in PrelNames are not needed anymore, now that Adam refactored things to use the common plugin architecture
  2. runTcPluginsGiven and runtcPluginsWanted look quite similar---perhaps we can combine them into a single function with a parameter?
  3. I think we should add some more functionality to TcPluginM. One function I think would be useful is a way to get the touchable unification variables. (e.g. tcPluginBindableVars :: TcPluginM (Bag TyVar)` or something)
  4. It looks like the changes to TcSMonad are not really needed anymore?

Thanks Iavor!

In D489#12594, @yav wrote:

Here are some things we may want to change:

  1. I think the changes in PrelNames are not needed anymore, now that Adam refactored things to use the common plugin architecture

You're right, some of the PrelNames additions are now redundant, and can be removed.

  1. runTcPluginsGiven and runtcPluginsWanted look quite similar---perhaps we can combine them into a single function with a parameter?

True; it is unfortunate that there are quite subtle differences between them (e.g. runTcPluginsWanted has to return the insolubles whereas runTcPluginsGiven can just emit them). I'll see what I can come up with, but suggestions are welcome.

  1. I think we should add some more functionality to TcPluginM. One function I think would be useful is a way to get the touchable unification variables. (e.g. tcPluginBindableVars :: TcPluginM (Bag TyVar)` or something)

Does such a function exist already? I'd rather stick to wrapping existing TcM functionality, rather than writing much brand new code, at least to begin with.

You're right that we ought to have some more functionality in TcPluginM, though. I've used the following in my units of measure plugin: isTouchableTcM, tclookupTyCon, newFlexiTyVar, zonkCt, lookupRdrNameInModuleForPlugins, getTopEnv. Obviously this list is incomplete, but Is there any category that I'm obviously missing? Also, matchFam is useful, but will need to be tweaked to work in TcM instead of TcS (which is easy enough, I think).

  1. It looks like the changes to TcSMonad are not really needed anymore?

Good point, some of them are unnecessary. Perhaps we should move splitInertCans and removeInertCts to TcSMonad, because it feels like they belong there, and then lots of the new TcSMonad exports go away?

austin requested changes to this revision.Nov 18 2014, 11:57 AM

Nice, all the changes to remove the boot files, etc look great. Thank you Adam!

I think Iavor may have some more requests first before accepting it. But I also have requests:

  • We need a release note in the manual about this, in docs/users_guide/7.10.1-notes.xml, under the "Compiler" section (I'll add the highlights later so don't worry about that).
  • This needs to be added to the users manual; we already have documentation about plugins in docs/users_guide/extending_ghc.xml, which is where this would go.
  • We're trying to keep 80 column violations under control, so if you can reasonably fix them, please do so!

I think those are my main concerns - thanks!

This revision now requires changes to proceed.Nov 18 2014, 11:57 AM

@adamgundry thanks for pulling this together! Looks good to me.

@yav I spent some time looking at the two plugin-runners this morning, but couldn't quite see a way to cleanly generalize them either. I agree that it would be nice though.

adamgundry updated this revision to Diff 1511.Nov 18 2014, 1:43 PM

Address some of Iavor's feedback

  • Remove unnecessary PrelNames exports
  • Move splitInertCans/removeInertCts to TcSMonad, where they belong
  • Thou shalt not have more than 80 columns
  • Expose new module TcPluginM wrapping more TcM functionality
adamgundry updated this revision to Diff 1543.Nov 19 2014, 4:23 AM

Address feedback from Austin and Harbormaster

  • Fix redundant import warnings
  • Update user manual for typechecker plugins
adamgundry updated this revision to Diff 1547.Nov 19 2014, 6:15 AM
  • Tidy up runTcPluginsGiven/runTcPluginsWanted

I think I've now addressed everything. @yav, @gridaphobe, how does the new common runTcPlugins look?

In the docstring for SolvedCts, I believe you mean that the wanteds will have evidence :)

I'm not a huge fan of the giant tuple that runTcPlugins returns, I'd generally prefer a record in that case. On the other hand, runTcPlugins only has two call-sites, so it's probably not that big a deal.

yav added a comment.EditedNov 19 2014, 11:22 AM

Hello,

I am not convinced that requiring the plugins to check for duplicate work on their own will avoid getting stuck in a loop. I am thinking of a situation like this:

  1. The inert set has some unsolved wanted, say C
  2. We run the plugin on it, it fails to solve it C, but it generates some new work D
  3. D is not an exact copy of anything in the inert set.
  4. We go again, and it turns out that D is discharged by solveFlats (i.e., it was already implied by the inert set).
  5. Now the remaining unsolved flats are C, so we run the plugin again...

To work around this situation, in the version that Eric and I implemented, we modified solveFlats to return a boolean flag indicating if there were any modifications to the inert set after the solving. We only re-run the plugins, if there were changes to the inert set.

I guess another way to do the same would be to remember the previous inputs to the plugin, and only re-run them if the inputs have changed.

austin accepted this revision.Nov 19 2014, 4:14 PM

Awesome, LGTM!

This revision is now accepted and ready to land.Nov 19 2014, 4:14 PM

In the docstring for SolvedCts, I believe you mean that the wanteds will have evidence :)

Thanks @gridaphobe, good catch!

I'm not a huge fan of the giant tuple that runTcPlugins returns, I'd generally prefer a record in that case. On the other hand, runTcPlugins only has two call-sites, so it's probably not that big a deal.

Fair point, I'll stop being lazy and make a proper record.

In D489#13013, @yav wrote:

I am not convinced that requiring the plugins to check for duplicate work on their own will avoid getting stuck in a loop.

We know that plugins can cause loops if they generate new work without making progress; there are a number of heuristics we could apply to try to prevent this, but ultimately it is the responsibility of the plugin not to do this. I'm not convinced there is much benefit in implementing such heuristics before we get more experience of actually writing plugins, because the possible ways to cause loops are many and various.

To work around this situation, in the version that Eric and I implemented, we modified solveFlats to return a boolean flag indicating if there were any modifications to the inert set after the solving. We only re-run the plugins, if there were changes to the inert set.

Yes, this is a nice rule, but unfortunately I can't see how to make it work now that plugins are being run on the wanteds after unflattening. When we go round the loop, we will be changing the inert set to flatten the constraints again, regardless of new constraints from the plugin. Suggestions are welcome...

I guess another way to do the same would be to remember the previous inputs to the plugin, and only re-run them if the inputs have changed.

This is possible, but (to begin with at least) could be implemented by a plugin itself, using an IORef to store its previous inputs. Similarly, I think my previous worries about a plugin needing to know how many times it has been invoked (motivated by similar loop-avoidance concerns) are unfounded: the plugin can just stick the count in an IORef!

TL;DR: I'd like to land this essentially as is, and revisit the question of loop-avoidance heuristics in the future if necessary.

adamgundry updated this revision to Diff 1584.Nov 20 2014, 3:26 AM

Final polishing

  • Use a record to make clearer the structure of runTcPlugins; fix comment
  • Tiny cleanup in solveFlatGivens
  • Do not invoke plugins if there are no constraints of the appropriate type
This revision was automatically updated to reflect the committed changes.