Dear GHC devs, and typechecker plugin authors in particular,
In
GHC ticket #26935, I noticed that typechecker plugins were not getting run when doing pattern match checking, which was a long standing source of frustration. I fixed this in
GHC MR !14797 (only present in GHC HEAD at the moment), but, as noted in
GHC ticket #26839, this meant that GHC is repeatedly initialising typechecker plugins for a single module (starting and stopping the plugins for each call of
initTcDsForSolver by the pattern-match checker).
I am proposing to change the TcPlugin datatype to split the existing "stop" action into two separate actions, "end of typechecking" and "plugin shutdown". This would allow typechecker plugins to be kept running after typechecking (for the benefit of the pattern-match checker) while upholding the invariant that typechecker plugins are initialised once per module being typechecked (modulo small caveats about certain one-off runs of the typechecker by e.g. Backpack).
The current TcPlugin data type is as follows:
data TcPlugin = forall s. TcPlugin
{ tcPluginInit :: TcPluginM s
, tcPluginSolve :: s -> TcPluginSolver
, tcPluginRewrite :: s -> UniqFM TyCon TcPluginRewriter
, tcPluginStop :: s -> TcPluginM ()
-- ^ Clean up after the plugin, when exiting the type-checker.
}
To allow typechecker plugins to be run by the pattern-match checker, I propose to change this to:
data TcPlugin = forall s. TcPlugin
{ tcPluginInit :: TcPluginM s
, tcPluginSolve :: s -> TcPluginSolver
, tcPluginRewrite :: s -> UniqFM TyCon TcPluginRewriter
, tcPluginPostTc :: s -> TcPluginM ()
-- ^ Action to run at the end of type-checking.
, tcPluginShutdown :: s -> IO ()
-- ^ Clean up after the plugin, after desugaring is finished.
}
tcPluginPostTc would run at the end of typechecking. This gives plugins a final opportunity to modify the typechecker environment before it is finalised (as e.g.
the clippy plugin does). If the plugin relies on an active session (e.g. with
Z3), the post-tc action should not end the session, because the plugin might still be invoked by
the pattern match checker, later, during desugaring.
Some remarks:
- I changed tcPluginStop to tcPluginPostTc, because it now serves a different function (an action at the end of typechecking that should not shut down the plugin). Keeping the same name would be confusing, I think.
- The tcPluginShutdown action runs in IO only, as running in TcPluginM would require holding on to a typechecker environment during desugaring, which can cause memory leaks.
- This same change would also be carried over to defaulting plugins, but not to hole fit plugins – the latter cannot affect pattern match checking.
- A better solution to all of this would be to run the pattern match checker during typechecking, but that would be a significant infrastructural change to GHC.
I would like feedback from authors of typechecker plugins on this proposed change.
Thanks,
Sam