Serialising evidence generated by typechecker plugins

[Richard Eisenberg]

I've been following the plugins stuff at a small distance. I'vm very interested as a user, but don't have the bandwidth to think deeply as an implementor. With that caveat, I have a proposal:

Suppose plugin P is responsible for producing CoAxiomRule R while compiling module M. I think it's reasonable to require any module N that imports M to have access to plugin P. (And, perhaps, to specify the use of P in GHC options while compiling N.) With this requirement, rule R could be serialized with its name, as is done now, but with an enhanced name that includes all the info about P, including versioning/checksum. Then, we can keep a nice higher-order representation of CoAxiomRules, and still get serialization.

Or is there a basic assumption about plugins that I'm missing here?

Richard

On Dec 11, 2014, at 7:22 AM, Adam Gundry <adam at well-typed.com> wrote:

> Hi folks,
> 
> I've just discovered tcIfaceCoAxiomRule, which is used when typechecking
> a coercion from an interface file. It turns out that CoAxiomRules are
> represented in interface files by their names, so tcIfaceCoAxiomRule
> looks up this name in a map containing all the built-in typeNatCoAxiomRules.
> 
> Unfortunately, this lookup fails when a plugin has defined its own
> CoAxiomRule (as both uom-plugin and type-nat-solver do)! This means that
> if a module uses a plugin and exports some of the evidence generated via
> an unfolding, importing the module may result in a tcIfaceCoAxiomRule panic.
> 
> At the moment, both plugins generate fake CoAxiomRules that can prove
> the equality of any types, so one workaround would be to expose this
> ability in the TcCoercion type (i.e. add the equivalent of UnivCo). In
> the future, however, it would be nice if plugins could actually generate
> bona fide evidence based on their own axioms (e.g. the abelian group
> laws, for uom-plugin).
> 
> We can't currently serialise CoAxiomRule directly, because it contains a
> function in the coaxrProves field. Could we support an alternative
> first-order representation that could be serialised? This probably
> wouldn't be as expressive, in particular it might not cover the built-in
> axioms that define type-level comparison functions and arithmetic
> operators, but it would allow plugins to axiomatize algebraic theories.
> 
> Any thoughts?
> 
> Adam
> 
> P.S. I've updated https://phabricator.haskell.org/D553 with the
> TcPluginM changes we discussed.
> 
> 
> -- 
> Adam Gundry, Haskell Consultant
> Well-Typed LLP, http://www.well-typed.com/