... | @@ -169,9 +169,20 @@ for units of measure) it should be possible for the solver to encode |
... | @@ -169,9 +169,20 @@ for units of measure) it should be possible for the solver to encode |
|
the axioms of the equational theory and build proofs from them.
|
|
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 [ this ghc-devs thread](https://www.haskell.org/pipermail/ghc-devs/2014-December/007626.html) for discussion of the problem and a potential solution.
|
|
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.
|
|
|
|
|
|
## Open questions and future directions
|
|
|
|
|
|
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`.
|
|
|
|
|
|
|
|
## Outstanding issues
|
|
|
|
|
|
|
|
- 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`).
|
|
|
|
|
|
|
|
- Plugins that define type families often need to ensure that those type families have no normal instances, to avoid inconsistency, but empty closed type families are currently rejected ([\#9840](https://gitlab.haskell.org//ghc/ghc/issues/9840)).
|
|
|
|
|
|
|
|
- Defining type families is more work than it needs to be, because the current interface forces the plugin to search the unsolved constraints for the type family in question (which might be anywhere within the types), then emit a new given constraint to reduce the type family. Instead, it should be possible to plug in to `matchFam` directly.
|
|
|
|
|
|
- For units of measure, it would be nice to be able to extend the
|
|
- 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
|
|
pretty-printer for types (so we could get a nicely formatted
|
... | @@ -184,6 +195,8 @@ At present, plugins can produce blatant assertions using a `UnivCo` inside a `Tc |
... | @@ -184,6 +195,8 @@ At present, plugins can produce blatant assertions using a `UnivCo` inside a `Tc |
|
messages that result from type checking, along the lines of error
|
|
messages that result from type checking, along the lines of error
|
|
reflection in Idris.
|
|
reflection in Idris.
|
|
|
|
|
|
|
|
- Would it be useful if plugins could generate code on a per-module basis, depending on the contents of the module (e.g. generating instances of a class like `Typeable` uniformly for every datatype)?
|
|
|
|
|
|
- At the moment there is not a very clear relationship between plugins and [hooks](ghc/hooks). It might be nice to unify the two approaches, but they have quite different design goals.
|
|
- At the moment there is not a very clear relationship between plugins and [hooks](ghc/hooks). It might be nice to unify the two approaches, but they have quite different design goals.
|
|
|
|
|
|
## Reactions from community
|
|
## Reactions from community
|
... | | ... | |