... | ... | @@ -178,12 +178,12 @@ the axioms of the equational theory and build proofs from them. |
|
|
|
|
|
In the light of experience with GHC 7.10.1, we are considering some changes to the typechecker plugins API for the next release.
|
|
|
|
|
|
### Empty closed type families
|
|
|
### Implemented: Empty closed type families
|
|
|
|
|
|
|
|
|
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 were previously rejected ([\#9840](https://gitlab.haskell.org//ghc/ghc/issues/9840)). They are now permitted in HEAD. See [ Phab:D841](https://phabricator.haskell.org/D841).
|
|
|
|
|
|
### Creating constraints
|
|
|
### Implemented: Creating constraints
|
|
|
|
|
|
|
|
|
The existing API does not offer a very direct way for plugins to create new constraints. In particular, creating new givens is problematic now that [ givens contain EvVars rather than EvTerms](https://github.com/ghc/ghc/commit/fa46c597db9939de1de4bc9b917c8dc1d9e2093a). I propose that we add new functions to `TcPluginM`:
|
... | ... | @@ -198,9 +198,9 @@ newGiven :: CtLoc -> PredType -> EvTerm -> TcPluginM CtEvidence |
|
|
The implementation of `newGiven` will require `TcPluginM` to pass around an `EvBindsVar`, so that it can bind a new evidence variable. This is not available in `tcPluginInit` and `tcPluginStop`, so using `newGiven` there will result in a crash. (I previously considered making `TcPluginM` wrap `TcS` directly, but that turns out to require a lot of rearrangement and probably hs-boot files.)
|
|
|
|
|
|
|
|
|
This is being reviewed. See [ Phab:D909](https://phabricator.haskell.org/D909).
|
|
|
These are now in HEAD, along with `newUnique :: TcPluginM Unique`. See [ Phab:D909](https://phabricator.haskell.org/D909).
|
|
|
|
|
|
### Defining type families
|
|
|
### Under discussion: Defining type families
|
|
|
|
|
|
|
|
|
Defining type families in plugins 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.
|
... | ... | @@ -217,7 +217,7 @@ This is similar to `sfMatchFam`, which gives the definition of built-in type fam |
|
|
|
|
|
**Richard:** This makes me uncomfortable, in exactly the same way that I was made to feel uncomfortable in the comments starting with [comment:4:ticket:9840](https://gitlab.haskell.org//ghc/ghc/issues/9840). The fact that the new, (what I will call) *external* type families will behave differently than internal type families is further evidence that something is amiss. (The difference in behavior I'm referring to is the difference between `matchFam` and `reduceTyFamApp_maybe`.) This, of course, ties into [\#9636](https://gitlab.haskell.org//ghc/ghc/issues/9636) as well and to some of the more esoteric issues that cropped up while working on [\#6018](https://gitlab.haskell.org//ghc/ghc/issues/6018)/[ Phab:D202](https://phabricator.haskell.org/D202) and perhaps even [\#10327](https://gitlab.haskell.org//ghc/ghc/issues/10327). I would love to approach this problem with the idea of making broader changes instead of looking for a minimal change just to support typechecker plugins better. **End Richard**
|
|
|
|
|
|
### Embedding CoreExpr in EvTerm
|
|
|
### Under discussion: 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.
|
... | ... | @@ -234,7 +234,7 @@ 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
|
|
|
### Under discussion: 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.
|
... | ... | |