Serialising evidence generated by typechecker plugins

[Simon Peyton Jones]

Go ahead and make suggestions here.  Since a CoAxiomRule embodies essentially arbitrary computation, it's hardly surprising that there's a fixed range of possibilities.

I suppose that for extensibilty, any particular plugin could say "TypeNats:Rule1", "TypeNats:Rule" etc, and recognise that at the other end.  We'd just need generic way to identify a plugin, plus an Int to say which axiom from that plugin.

Anyway, it's all to play for.

Simon

| -----Original Message-----
| From: ghc-devs [mailto:ghc-devs-bounces at haskell.org] On Behalf Of Adam
| Gundry
| Sent: 11 December 2014 12:23
| To: Iavor Diatchki; Eric Seidel
| Cc: ghc-devs at haskell.org
| Subject: Serialising evidence generated by typechecker plugins
| 
| 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 at haskell.org
| http://www.haskell.org/mailman/listinfo/ghc-devs