Typechecker plugins and BuiltInSynFamily

[Alexis King]

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:

AxiomRuleCo provides significantly more safety from -dcore-lint than UnivCo, but UnivCo is currently the only way to provide evidence for plugin-solved families.

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:

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).

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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20190820/07d8f8f9/attachment.html>