Rewriting plugins: request for feedback

[Sam Derbyshire]

Hi everyone,

Recent refactors to the constraint solver have complicated the story for
authors of type-checking plugins. Following a suggestion by Christiaan
Baaij, and aided by Richard Eisenberg, I'm working on adding the ability
for type-checking plugins to rewrite type family applications directly
(hooking straight into GHC's type-family rewriting code). The goal is to
ease migration for the plugin authors, hopefully simplifying the common
operation of rewriting type family applications.


Let me now describe the current API for this new functionality, for which I
would like feedback.

--------------------------------------------------------------------------

A new field is added to the TcPlugin data type, namely

tcPluginRewrite :: s -> UniqFM TyCon TcPluginRewriter

Here s is the existential plugin state that users can choose as they wish
for their own plugin.
Plugins thus register which type family TyCons they are interested in
rewriting, like so:

myTcPluginRewrite :: MyPluginState -> UniqFM TyCon TcPluginRewriter
myTcPluginRewrite s@(MyPluginState {myFam1TyCon, myFam2TyCon}) =
  listToUFM [ (myFam1TyCon, myFam1Rewriter s), (myFam2TyCon, myFam2Rewriter
s) ]

For each type family TyCon, the plugin should provide a rewriting function
(corresponding to myFam1Rewriter and myFam2Rewriter above), of type

type TcPluginRewriter = [Ct] -> [TcType] -> TcPluginM TcPluginRewriteResult

This means that a rewriting function is supplied with the current Given
constraints and the arguments of the (guaranteed to be saturated)
type-family application, and should return a result of type:

data TcPluginRewriteResult where
  TcPluginRewriteError
    :: (Diagnostic a, Typeable a) => a -> TcPluginRewriteResult
  TcPluginNoRewrite
    :: TcPluginRewriteResult
  TcPluginRewriteTo
    :: { rewriteTo :: TcType
       , rewriteEvidence :: TcCoercion }
    -> TcPluginRewriteResult

That is, the plugin can specify what the type-family application should be
rewritten to, throw an error, or do nothing.

--------------------------------------------------------------------------

I'm hoping that the components of existing type-checking plugins concerned
with type-family applications can instead use this mechanism and achieve
more robust results by doing so, with less effort.

I would like to hear from plugin authors whether this API suits their
needs. If you know of someone not on this list that might be interested,
please invite them to join the conversation.

The current state of this patch can be found in the GHC MR 5909:
https://gitlab.haskell.org/ghc/ghc/-/merge_requests/5909

Thanks,

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