Serialising evidence generated by typechecker plugins

[Adam Gundry]

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/