...  ...  @@ 173,9 +173,6 @@ way. However, in some cases (such as an abelian group unifier used 


for units of measure) it should be possible for the solver to encode



the axioms of the equational theory and build proofs from them.









At present, plugins can produce blatant assertions using a `UnivCo` inside a `TcCoercion`. GHC has limited support for theoryspecific axioms in the form of `CoAxiomRule`, but this is limited to builtin axioms relating to type literals. A plugin that creates its own `CoAxiomRule` may at first appear to work fine, but if such an axiom is exposed in an interface file (e.g. via an unfolding) then GHC will crash with a `tcIfaceCoAxiomRule` panic when importing it. See [ "Serialising evidence generated by typechecker plugins" on ghcdevs](https://mail.haskell.org/pipermail/ghcdevs/2014December/007626.html) for discussion of the problem and a potential solution.






## Post7.10 changes to TcPluginM API







...  ...  @@ 237,12 +234,31 @@ dsEvTerm (EvCoreExpr e) = return e 





I'm not very clear on whether we need to extend zonking to work on `CoreExpr`? Or should `EvCoreExpr` take a prezonked expression?






### Evidence for axioms









At present, plugins can produce blatant assertions using a `UnivCo` inside a `TcCoercion`. GHC has limited support for theoryspecific axioms in the form of `CoAxiomRule`, but this is limited to builtin axioms relating to type literals. A plugin that creates its own `CoAxiomRule` may at first appear to work fine, but if such an axiom is exposed in an interface file (e.g. via an unfolding) then GHC will crash with a `tcIfaceCoAxiomRule` panic when importing it. See [ "Serialising evidence generated by typechecker plugins" on ghcdevs](https://mail.haskell.org/pipermail/ghcdevs/2014December/007626.html) for discussion of the problem and a potential solution, namely making plugins able to create their own `CoAxiomRule`s and serialise them in interface files.






**Richard:** While we're at it, we should probably merge `CoAxiomRule` with `CoAxiom` somehow. I believe `CoAxiomRule` is just a generalization of `CoAxiom`. **End Richard**






**Adam:** I'm not convinced this is true. It seems to me that `CoAxiom` and `CoAxiomRule` encode two different forms of axiom families:






 `CoAxiom` describes a finite collection of branches for a closed type family, for example `forall a . Equal a a ~ True` and `forall a b . a # b => Equal a b ~ False` (where I pretend we have a builtin notion of apartness written `#`). We sometimes need to observe the branch structure, for example when reifying the type family for TH.






 `CoAxiomRule` describes a potentiallyinfinite family of axioms that have the form `forall as . cs => coaxrProves(as, cs)` for some arbitrary metalevel function `coaxrProves` that generates an equation. For example, the definition for (+) generates `2 + 2 ~ 4` and infinitely many other axioms. `CoAxiomRule` doesn't give a way to describe apartness requirements.









It may be possible to generalize both of these into a single form of evidence, but it'll take a bit of thought. I wonder if the real distinction should be between single axioms (with a type that can be expressed in FC) and infinite families of axioms (which are not directly expressible in FC, e.g. arithmetic operators). In particular, I think it may be worth representing apartness evidence more explicitly, so that a `CoAxiom` can correspond directly to a set of single axioms. **End Adam**









Iavor notes out that it would be useful to be able to express evidence for functional dependencies using axioms like `forall a b c. (C a b, C a c) => (b ~ c)`.






[ Christiaan points out](https://github.com/clashlang/ghctypelitsnatnormalise/issues/1#issuecomment106748739) that the evidence we can generate constrains the way multiple plugins can interact sensibly.






## Outstanding issues






 Dynamic loading seems to be subtly broken on Windows or when using multiple plugins (see [\#10301](https://gitlab.haskell.org//ghc/ghc/issues/10301)). There is a [ workaround](https://github.com/clashlang/ghctypelitsnatnormalise/commit/afc4f2538081b46439e26e1a2bc6b7a5c3751781).






 As discussed above, plugins should be able to create their own `CoAxiomRule`s, but this requires some way of serialising them in interface files. **Richard:** While we're at it, we should probably merge `CoAxiomRule` with `CoAxiom` somehow. I believe `CoAxiomRule` is just a generalization of `CoAxiom`. **End Richard**






 For units of measure, it would be nice to be able to extend the



prettyprinter for types (so we could get a nicely formatted



inferred type like `m/s^2` rather than a nested type family

...  ...  