Changes between Version 19 and Version 20 of Plugins/TypeChecker


Ignore:
Timestamp:
Jun 1, 2015 1:30:58 PM (2 years ago)
Author:
adamgundry
Comment:

update status of Phab:D909 and make clear which changes have been implemented

Legend:

Unmodified
Added
Removed
Modified
  • Plugins/TypeChecker

    v19 v20  
    165165In the light of experience with GHC 7.10.1, we are considering some changes to the typechecker plugins API for the next release.
    166166
    167 === Empty closed type families ===
     167=== Implemented: Empty closed type families ===
    168168
    169169Plugins 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). They are now permitted in HEAD. See Phab:D841.
    170170
    171 === Creating constraints ===
     171=== Implemented: Creating constraints ===
    172172
    173173The existing API does not offer a very direct way for plugins to create new constraints. In particular, creating new givens is problematic now that [https://github.com/ghc/ghc/commit/fa46c597db9939de1de4bc9b917c8dc1d9e2093a givens contain EvVars rather than EvTerms]. I propose that we add new functions to `TcPluginM`:
     
    181181The 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.)
    182182
    183 This is being reviewed. See Phab:D909.
    184 
    185 === Defining type families ===
     183These are now in HEAD, along with `newUnique :: TcPluginM Unique`. See Phab:D909.
     184
     185=== Under discussion: Defining type families ===
    186186
    187187Defining 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.
     
    197197'''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. 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 as well and to some of the more esoteric issues that cropped up while working on #6018/Phab:D202 and perhaps even #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'''
    198198
    199 === Embedding CoreExpr in EvTerm ===
     199=== Under discussion: Embedding CoreExpr in EvTerm ===
    200200
    201201At 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 [https://mail.haskell.org/pipermail/ghc-devs/2015-February/008414.html "EvTerms and how they are used" on ghc-devs] for discussion of this.
     
    211211I'm not very clear on whether we need to extend zonking to work on `CoreExpr`? Or should `EvCoreExpr` take a pre-zonked expression?
    212212
    213 === Evidence for axioms ===
     213=== Under discussion: Evidence for axioms ===
    214214
    215215At 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 [https://mail.haskell.org/pipermail/ghc-devs/2014-December/007626.html "Serialising evidence generated by typechecker plugins" on ghc-devs] 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.