plugins/type-checker.md

@@ -260,7 +260,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**
 
-### Under discussion: Embedding CoreExpr in EvTerm
+### Implemented: 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.
@@ -277,6 +277,9 @@ 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?
 
+
+This is now implemented; see [\#14691](https://gitlab.haskell.org//ghc/ghc/issues/14691).
+
 ### Under discussion: Evidence for axioms
 
 
@@ -300,7 +303,7 @@ Iavor notes out that it would be useful to be able to express evidence for funct
 
 ## 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).
+- The current API does not make it possible to express the fact that a plugin solved some constraints but discovered others were impossible to solve. The only option is to solve the valid constraints and leave the others as unsolved, rather than identifying the contradiction.
 
 - 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