Rewriting plugins: request for feedback

[Sam Derbyshire]

Hi again everyone,


I've been making some more adjustments to the API of type-checking plugins.
Following a suggestion by Richard, the mechanism for reporting errors while
rewriting type family applications now consists of emitting a wanted
constraint with a custom type error message. There are several technical
reasons for this, which I will not get into.
This means there are now only two constructors of TcPluginRewriteResult:
TcPluginNoRewrite and TcPluginRewriteTo. Both of these now take an extra
argument: additional wanted constraints, which will be processed and
emitted by GHC.


Coming back to the type-checking plugin API as a whole (not just the
rewriting of type family applications), I've come to the realisation that
it is probably best to keep GHC's interface as simple as possible, to allow
library authors to write their own APIs.
After all, most of the API doesn't need to live within the GHC codebase,
and instead (in my opinion) belongs in libraries that simply import the ghc
package (which thankfully doesn't hide any exports one might want to use).
This means we don't have to tie any experimentation with type-checking
plugin APIs to the GHC release schedule.

To that end, I have concluded that one single non-backwards-compatible
change seems important: changing the TcPluginM monad from being isomorphic
to "ReaderT EvBindsVar TcM" to simply being a newtype around TcM. Then, we
instead pass an EvBindsVar as an extra argument to tcPluginSolve.
This avoids all the silly business with functions whose documentation said
"only call this within tcPluginSolve or it will cause a crash" (a situation
which was only made worse by the addition of rewriting plugins). It's also
less opinionated: library authors can use a ReaderT wrapper in their API if
they desire, but are not forced to do so.
Please note that I don't make this change lightly, as I know it is already
time-consuming enough to maintain type-checking plugins, especially as much
more significant changes abound (removal of flattening variables in GHC
9.2, removal of derived constraints (possibly in GHC 9.4)). I hope
nevertheless that you might find this acceptable.


Finally, facilitated by the above, I have started implementing a library
providing a simple API for type-checking plugins; see here
https://github.com/sheaf/ghc-tcplugin-api.
An example of a not-totally-trivial rewriting plugin is given here:
https://github.com/sheaf/ghc-tcplugin-api/blob/ad6ca964c3b27c28bb27392d7ba406cfac82176d/examples/RewriterPlugin/plugin/RewriterPlugin.hs
.
Note that I barely had to import anything from the ghc package; I hope this
can remain true for more involved plugins (up to a point).
Please let me know what you think, in particular if you think certain
important functions are missing from the API.

For this library specifically, I have added back ReaderT layers (but only
in the appropriate situations, to avoid reintroducing the aforementioned
problem with "only call this in tcPluginSolve"), and provided MTL-style
typeclasses for operations that work with multiple different phases of the
plugin.
Other design options are of course possible; at any rate, I think it is
preferable to be making these API choices outside of GHC itself whenever
possible.
I've also included helpers for creating custom type errors within
type-checking plugins, as that was unnecessarily cumbersome. (One still
needs to provide a CtLoc to inform GHC of the source location of the error;
one can get this from a constraint fed to the plugin in a solver plugin, or
from the rewriting environment in a rewriter plugin).


Note that this all still depends on the WIP GHC MR 5909, available at
https://gitlab.haskell.org/ghc/ghc/-/merge_requests/5909.


I look forward to your feedback,

Thanks,

Sam
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20210615/e76e5d12/attachment.html>