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
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/