... | ... | @@ -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
|
... | ... | |