Changes between Version 19 and Version 20 of Plugins/TypeChecker

Jun 1, 2015 1:30:58 PM (2 years ago)

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


  • 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.
    167 === Empty closed type families ===
     167=== Implemented: Empty closed type families ===
    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.
    171 === Creating constraints ===
     171=== Implemented: Creating constraints ===
    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 [ 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.)
    183 This is being reviewed. See Phab:D909.
    185 === Defining type families ===
     183These are now in HEAD, along with `newUnique :: TcPluginM Unique`. See Phab:D909.
     185=== Under discussion: Defining type families ===
    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'''
    199 === Embedding CoreExpr in EvTerm ===
     199=== Under discussion: Embedding CoreExpr in EvTerm ===
    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 [ "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?
    213 === Evidence for axioms ===
     213=== Under discussion: Evidence for axioms ===
    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 [ "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.