Dear GHC devs, and typechecker plugin authors in particular,
In GHC ticket #26935 <https://gitlab.haskell.org/ghc/ghc/-/issues/26395>, 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
<https://gitlab.haskell.org/ghc/ghc/-/merge_requests/14797> (only present
in GHC HEAD at the moment), but, as noted in GHC ticket #26839
<https://gitlab.haskell.org/ghc/ghc/-/issues/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
<https://github.com/ArturGajowy/ghc-clippy-plugin/blob/0f97274f238b78e1117b751fdd3f39e210841864/src/Clippy.hs#L33>).
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
_______________________________________________
ghc-devs mailing list -- [email protected]
To unsubscribe send an email to [email protected]
