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 <a...@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/ _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs
