Alexis
What you suggest sounds like an excellent idea. For some plugins, being able
to extend the range of “built in” families might be all the plugin needs to do!
(For others it might need to do some solving too.)
I’ve thought a bit about how to achieve this:
* The most direct thing would be for the solver, when initialised (via
tcPluginInit), to return a [(Name, BuiltinSynFamily)] pairs as well as the
solver and plugin-stop action. See Note 1 below.
* Then the typechecker can keep (in tcg_plugins) a little (NameEnv
BuiltinSynFamily), gotten by accumulating all the lists from all the plugins.
* Now, in three places we need to look up in that env:
* TcInteract.improveLocalFunEqs – see the use of sfInteractInert
* TcInteract.improve_top_fun_eqs – see the use of sfInteractTop
* FamInstEnv.reduceTyFamApp_maybe – see the use of
isBuildintSynFamTyCon_maybe
The easiest thing might be to extend the type FamInstEnvs to be a triple, with
the (NameEnv BuiltinSymFamily) as one of the components.
That would make it possible for a plugin to “register” any number of type
families as having a BuiltinSynFamily, which allows all the type-family
matching and reduction to be done by code written by the plugin author.
(Maybe “built in” is a misnomer... perhaps “magic” or something would be less
misleading.)
I don’t think this would be hard, and for the things it worked for it’d be much
much better, I think.
If anyone wants to have a go, I’m happy to advise.
NB: if we do this for type families, we should probably do it for
* Type classes (so the a plugin could implement new class-instance
behaviour that needs code; c.f. the current ClsInst.matchGlobalInst which
dispatches off to functions that handle the current built-in cases: Typeable,
Coercible, HasField, etc.
* CoreRules (so that a plugin could could add new BuitinRules)
Simon
Note 1.
TcPlugin is defined oddly:
data TcPlugin = forall s. TcPlugin
{ tcPluginInit :: TcPluginM s
-- ^ Initialize plugin, when entering type-checker.
, tcPluginSolve :: s -> TcPluginSolver
-- ^ Solve some constraints.
-- TODO: WRITE MORE DETAILS ON HOW THIS WORKS.
, tcPluginStop :: s -> TcPluginM ()
-- ^ Clean up after the plugin, when exiting the type-checker.
}
What is that bizarre existential ‘s’? All we can do is to apply tcPluginSolve
and tcPluginStop to it, which happens immediately, in TcRnDriver.withTcPlugins.
So I think it’d make more sense and simpler thus
type TcPlugin = TcM (TcPluginSolver, TcM ())
So, run that TcM action to initialise it; the action returns a solver, and a
stop action. Neither initialisation nor stop action need to access that
EvBindsVar.
You could make that tuple into a record with named fields.
From: ghc-devs <[email protected]> On Behalf Of Alexis King
Sent: 20 August 2019 09:17
To: [email protected]
Subject: Typechecker plugins and BuiltInSynFamily
Hello all,
As I’ve been dabbling with typechecker plugins, I’ve found myself primarily
using them to define new “magic” type families, and I don’t think I’m
alone—Sandy Maguire recently released the magic-tyfams package for precisely
that purpose. However, I can’t help but notice that GHC already has good
internal support for such type families via BuiltInSynFamily and CoAxiomRule,
which are mostly used to implement operations on Nats. As a plugin author, I
would love to be able to use that functionality directly instead of being
forced to reimplement it myself, for two big reasons:
1. AxiomRuleCo provides significantly more safety from -dcore-lint than
UnivCo, but UnivCo is currently the only way to provide evidence for
plugin-solved families.
2. The sfInteractTop and sfInteractInert fields of BuiltInSynFamily make it
easy to support improvement for custom type families, which I believe would
take a non-trivial amount of tricky code to get right using the current
typechecker plugin API.
Given the above, I started wondering if it is possible to define a
BuiltInSynFamily from inside a plugin or, failing that, to modify GHC to expose
that functionality to typechecker plugin authors. I am not familiar with GHC’s
internals, but in my brief reading of the source code, the following two things
seem like the trickiest obstacles:
1. BuiltInSynFamily TyCons need to be injected into the initial name cache,
since otherwise those names will get resolved to their ordinary, non-built-in
counterparts (e.g. the ordinary open type families defined in GHC.TypeLits).
2. Since CoAxiomRule values actually have functions inside them, they can’t
be serialized into interface files. Therefore, it looks like GHC currently
maintains a hardcoded list of all the known CoAxiomRules, and
tcIfaceCoAxiomRule just searches for a value in that list using a well-known
(i.e. not in any way namespaced!) string.
I am not knowledgable enough about GHC to say how hard overcoming either of
those issues would be. Point 1 seems possible to achieve by arranging for
plugins to export the built-in names they want to define and propagating those
to the initial name cache, but I don’t know enough about how plugins are loaded
to know if that would create any possible circular dependencies (i.e. does the
name cache need to already exist in order to load a plugin in the first place?).
Point 2 seems harder. My gut instinct is that it could probably be overcome by
somehow storing a reference to the plugin that defined the CoAxiomRule in the
interface file (by, for example, storing its package-qualified module name),
but I’m not immediately certain when that reference should be resolved to the
actual CoAxiomRule value. It also presumably needs to complain if the necessary
plugin is not actually loaded when the CoAxiomRule needs to be resolved!
I’m willing to try my hand at experimenting with an implementation of this if
someone can give me a couple pointers on where to start on the above two issues
(assuming people don’t think it’s a bad idea to do it at all). Any advice would
be appreciated!
Thanks,
Alexis
_______________________________________________
ghc-devs mailing list
[email protected]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
