| ... | ... | @@ -176,9 +176,6 @@ 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.
|
|
|
|
|
|
|
|
|
|
|
|
See also [ "EvTerms and how they are used" on ghc-devs](https://mail.haskell.org/pipermail/ghc-devs/2015-February/008414.html) for details on constructing evidence for typeclass constraints using `EvDFunApp`.
|
|
|
|
|
|
|
|
## Post-7.10 changes to TcPluginM API
|
|
|
|
|
|
|
|
|
| ... | ... | @@ -221,14 +218,29 @@ tcPluginMatchFam :: s -> TyCon -> [Type] -> TcPluginM (Maybe (TcCoercion, TcType |
|
|
|
|
|
|
|
This is similar to `sfMatchFam`, which gives the definition of built-in type families like `(+)`. However, it would be invoked only in `matchFam`, rather than `reduceTyFamApp_maybe`, to save having to load plugins at all the call sites of the latter. Thus plugin-defined type families would reduce in the constraint solver, but not necessarily elsewhere.
|
|
|
|
|
|
|
|
### Embedding CoreExpr in EvTerm
|
|
|
|
|
|
|
|
|
|
|
|
At the moment, the `EvTerm` type used to represent evidence for constraints is quite restricted. In particular, it permits a selection of special cases (e.g. `EvLit`, `EvCallStack`, `EvTypeable`) but does not permit general `CoreExpr`s. This makes it difficult to constraint evidence for typeclass constraints, because they must use `EvDFunApp` with an existing dfun, rather than generating a dictionary directly. See [ "EvTerms and how they are used" on ghc-devs](https://mail.haskell.org/pipermail/ghc-devs/2015-February/008414.html) for discussion of this.
|
|
|
|
|
|
|
|
|
|
|
|
The plan is to add a constructor `EvCoreExpr CoreExpr` to `EvTerm`, with
|
|
|
|
|
|
|
|
```wiki
|
|
|
|
dsEvTerm :: EvTerm -> DsM CoreExpr
|
|
|
|
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?
|
|
|
|
|
|
|
|
## 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.
|
|
|
|
|
|
|
|
- Generating instances for typeclass constraints would be easier if `EvTerm` could contain Core expressions directly, rather than having a selection of special cases (e.g. `EvLit`).
|
|
|
|
|
|
|
|
- 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
|
| ... | ... | |
