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 <ghc-devs-bounces@haskell.org> On Behalf Of Alexis King
Sent: 20 August 2019 09:17
To: ghc-devs@haskell.org
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