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/