plugins/type-checker.md

@@ -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 theory-specific axioms in the form of `CoAxiomRule`, but this is limited to built-in 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 ghc-devs](https://mail.haskell.org/pipermail/ghc-devs/2014-December/007626.html) for discussion of the problem and a potential solution.
-
 ## Post-7.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 pre-zonked expression?
 
+### Evidence for axioms
+
+
+At present, plugins can produce blatant assertions using a `UnivCo` inside a `TcCoercion`. GHC has limited support for theory-specific axioms in the form of `CoAxiomRule`, but this is limited to built-in 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 ghc-devs](https://mail.haskell.org/pipermail/ghc-devs/2014-December/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 built-in notion of apartness written `#`). We sometimes need to observe the branch structure, for example when reifying the type family for TH.
+
+- `CoAxiomRule` describes a potentially-infinite 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/clash-lang/ghc-typelits-natnormalise/issues/1#issuecomment-106748739) 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/clash-lang/ghc-typelits-natnormalise/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
   pretty-printer for types (so we could get a nicely formatted
   inferred type like `m/s^2` rather than a nested type family