Add rewriting to typechecking plugins

Type-checking plugins can now directly rewrite type-families.
The TcPlugin record is given a new field, tcPluginRewrite.
The plugin specifies how to rewrite certain type-families with a value
of type `UniqFM TyCon TcPluginRewriter`, where:

type TcPluginRewriter
  =  RewriteEnv -- Rewriter environment
  -> [Ct]       -- Givens
  -> [TcType]   -- type family arguments
  -> TcPluginM TcPluginRewriteResult

data TcPluginRewriteResult
  = TcPluginNoRewrite
  | TcPluginRewriteTo
      { tcPluginRewriteTo    :: Reduction
      , tcRewriterNewWanteds :: [Ct]
      }

When rewriting an exactly-saturated type-family application,
GHC will first query type-checking plugins for possible rewritings
before proceeding.

Includes some changes to the TcPlugin API, e.g. removal
of the EvBindsVar parameter to the TcPluginM monad.

24 files changed, 851 insertions, 195 deletions

diff --git a/compiler/GHC/Tc/Module.hs b/compiler/GHC/Tc/Module.hs
index e0a4f58d39..bf190f059c 100644
--- a/compiler/GHC/Tc/Module.hs
+++ b/compiler/GHC/Tc/Module.hs
@@ -3088,19 +3088,24 @@ withTcPlugins hsc_env m =
        []      -> m  -- Common fast case
        plugins -> do
                 ev_binds_var <- newTcEvBinds
-                (solvers,stops) <- unzip `fmap` mapM (startPlugin ev_binds_var) plugins
-                -- This ensures that tcPluginStop is called even if a type
+                (solvers, rewriters, stops) <-
+                  unzip3 `fmap` mapM (startPlugin ev_binds_var) plugins
+                let
+                  rewritersUniqFM :: UniqFM TyCon [TcPluginRewriter]
+                  !rewritersUniqFM = sequenceUFMList rewriters
+                -- The following ensures that tcPluginStop is called even if a type
                 -- error occurs during compilation (Fix of #10078)
                 eitherRes <- tryM $
-                  updGblEnv (\e -> e { tcg_tc_plugins = solvers }) m
-                mapM_ (flip runTcPluginM ev_binds_var) stops
+                  updGblEnv (\e -> e { tcg_tc_plugin_solvers   = solvers
+                                     , tcg_tc_plugin_rewriters = rewritersUniqFM }) m
+                mapM_ runTcPluginM stops
                 case eitherRes of
                   Left _ -> failM
                   Right res -> return res
   where
-  startPlugin ev_binds_var (TcPlugin start solve stop) =
-    do s <- runTcPluginM start ev_binds_var
-       return (solve s, stop s)
+  startPlugin ev_binds_var (TcPlugin start solve rewrite stop) =
+    do s <- runTcPluginM start
+       return (solve s ev_binds_var, rewrite s, stop s)
 
 getTcPlugins :: HscEnv -> [GHC.Tc.Utils.Monad.TcPlugin]
 getTcPlugins hsc_env = catMaybes $ mapPlugins hsc_env (\p args -> tcPlugin p args)
diff --git a/compiler/GHC/Tc/Plugin.hs b/compiler/GHC/Tc/Plugin.hs
index 78a0ebd16a..a62ac86734 100644
--- a/compiler/GHC/Tc/Plugin.hs
+++ b/compiler/GHC/Tc/Plugin.hs
@@ -47,7 +47,6 @@ module GHC.Tc.Plugin (
         -- * Manipulating evidence bindings
         newEvVar,
         setEvBind,
-        getEvBindsTcPluginM
     ) where
 
 import GHC.Prelude
@@ -62,30 +61,30 @@ import qualified GHC.Unit.Finder        as Finder
 
 import GHC.Core.FamInstEnv     ( FamInstEnv )
 import GHC.Tc.Utils.Monad      ( TcGblEnv, TcLclEnv, TcPluginM
-                               , unsafeTcPluginTcM, getEvBindsTcPluginM
+                               , unsafeTcPluginTcM
                                , liftIO, traceTc )
 import GHC.Tc.Types.Constraint ( Ct, CtLoc, CtEvidence(..), ctLocOrigin )
 import GHC.Tc.Utils.TcMType    ( TcTyVar, TcType )
 import GHC.Tc.Utils.Env        ( TcTyThing )
 import GHC.Tc.Types.Evidence   ( CoercionHole, EvTerm(..)
-                               , EvExpr, EvBind, mkGivenEvBind )
+                               , EvExpr, EvBindsVar, EvBind, mkGivenEvBind )
 import GHC.Types.Var           ( EvVar )
 
-import GHC.Unit.Module
-import GHC.Types.Name
-import GHC.Types.TyThing
+import GHC.Unit.Module    ( ModuleName, Module )
+import GHC.Types.Name     ( OccName, Name )
+import GHC.Types.TyThing  ( TyThing )
 import GHC.Core.Reduction ( Reduction )
-import GHC.Core.TyCon
-import GHC.Core.DataCon
-import GHC.Core.Class
-import GHC.Driver.Config.Finder
-import GHC.Driver.Env
-import GHC.Utils.Outputable
-import GHC.Core.Type
-import GHC.Types.Id
-import GHC.Core.InstEnv
-import GHC.Data.FastString
-import GHC.Types.Unique
+import GHC.Core.TyCon     ( TyCon )
+import GHC.Core.DataCon   ( DataCon )
+import GHC.Core.Class     ( Class )
+import GHC.Driver.Config.Finder ( initFinderOpts )
+import GHC.Driver.Env       ( HscEnv(..), hsc_home_unit, hsc_units )
+import GHC.Utils.Outputable ( SDoc )
+import GHC.Core.Type        ( Kind, Type, PredType )
+import GHC.Types.Id         ( Id )
+import GHC.Core.InstEnv     ( InstEnvs )
+import GHC.Data.FastString  ( FastString )
+import GHC.Types.Unique     ( Unique )
 
 
 -- | Perform some IO, typically to interact with an external tool.
@@ -162,9 +161,8 @@ zonkTcType = unsafeTcPluginTcM . TcM.zonkTcType
 zonkCt :: Ct -> TcPluginM Ct
 zonkCt = unsafeTcPluginTcM . TcM.zonkCt
 
-
 -- | Create a new wanted constraint.
-newWanted  :: CtLoc -> PredType -> TcPluginM CtEvidence
+newWanted :: CtLoc -> PredType -> TcPluginM CtEvidence
 newWanted loc pty
   = unsafeTcPluginTcM (TcM.newWanted (ctLocOrigin loc) Nothing pty)
 
@@ -172,26 +170,29 @@ newWanted loc pty
 newDerived :: CtLoc -> PredType -> TcPluginM CtEvidence
 newDerived loc pty = return CtDerived { ctev_pred = pty, ctev_loc = loc }
 
--- | Create a new given constraint, with the supplied evidence.  This
--- must not be invoked from 'tcPluginInit' or 'tcPluginStop', or it
--- will panic.
-newGiven :: CtLoc -> PredType -> EvExpr -> TcPluginM CtEvidence
-newGiven loc pty evtm = do
+-- | Create a new given constraint, with the supplied evidence.
+--
+-- This should only be invoked within 'tcPluginSolve'.
+newGiven :: EvBindsVar -> CtLoc -> PredType -> EvExpr -> TcPluginM CtEvidence
+newGiven tc_evbinds loc pty evtm = do
    new_ev <- newEvVar pty
-   setEvBind $ mkGivenEvBind new_ev (EvExpr evtm)
+   setEvBind tc_evbinds $ mkGivenEvBind new_ev (EvExpr evtm)
    return CtGiven { ctev_pred = pty, ctev_evar = new_ev, ctev_loc = loc }
 
 -- | Create a fresh evidence variable.
+--
+-- This should only be invoked within 'tcPluginSolve'.
 newEvVar :: PredType -> TcPluginM EvVar
 newEvVar = unsafeTcPluginTcM . TcM.newEvVar
 
 -- | Create a fresh coercion hole.
+-- This should only be invoked within 'tcPluginSolve'.
 newCoercionHole :: PredType -> TcPluginM CoercionHole
 newCoercionHole = unsafeTcPluginTcM . TcM.newCoercionHole
 
--- | Bind an evidence variable.  This must not be invoked from
--- 'tcPluginInit' or 'tcPluginStop', or it will panic.
-setEvBind :: EvBind -> TcPluginM ()
-setEvBind ev_bind = do
-    tc_evbinds <- getEvBindsTcPluginM
+-- | Bind an evidence variable.
+--
+-- This should only be invoked within 'tcPluginSolve'.
+setEvBind :: EvBindsVar -> EvBind -> TcPluginM ()
+setEvBind tc_evbinds ev_bind = do
     unsafeTcPluginTcM $ TcM.addTcEvBind tc_evbinds ev_bind
diff --git a/compiler/GHC/Tc/Solver/Interact.hs b/compiler/GHC/Tc/Solver/Interact.hs
index 171cb958f2..98824022cd 100644
--- a/compiler/GHC/Tc/Solver/Interact.hs
+++ b/compiler/GHC/Tc/Solver/Interact.hs
@@ -192,11 +192,11 @@ solveSimples cts
 -- into the main solver.
 runTcPluginsGiven :: TcS [Ct]
 runTcPluginsGiven
-  = do { plugins <- getTcPlugins
-       ; if null plugins then return [] else
+  = do { solvers <- getTcPluginSolvers
+       ; if null solvers then return [] else
     do { givens <- getInertGivens
        ; if null givens then return [] else
-    do { p <- runTcPlugins plugins (givens,[],[])
+    do { p <- runTcPluginSolvers solvers (givens,[],[])
        ; let (solved_givens, _, _) = pluginSolvedCts p
              insols                = pluginBadCts p
        ; updInertCans (removeInertCts solved_givens)
@@ -213,13 +213,13 @@ runTcPluginsWanted wc@(WC { wc_simple = simples1 })
   | isEmptyBag simples1
   = return (False, wc)
   | otherwise
-  = do { plugins <- getTcPlugins
-       ; if null plugins then return (False, wc) else
+  = do { solvers <- getTcPluginSolvers
+       ; if null solvers then return (False, wc) else
 
     do { given <- getInertGivens
        ; simples1 <- zonkSimples simples1    -- Plugin requires zonked inputs
        ; let (wanted, derived) = partition isWantedCt (bagToList simples1)
-       ; p <- runTcPlugins plugins (given, derived, wanted)
+       ; p <- runTcPluginSolvers solvers (given, derived, wanted)
        ; let (_, _,                solved_wanted)   = pluginSolvedCts p
              (_, unsolved_derived, unsolved_wanted) = pluginInputCts p
              new_wanted                             = pluginNewCts p
@@ -260,11 +260,12 @@ data TcPluginProgress = TcPluginProgress
       -- ^ New constraints emitted by plugins
     }
 
-getTcPlugins :: TcS [TcPluginSolver]
-getTcPlugins = do { tcg_env <- getGblEnv; return (tcg_tc_plugins tcg_env) }
+getTcPluginSolvers :: TcS [TcPluginSolver]
+getTcPluginSolvers
+  = do { tcg_env <- getGblEnv; return (tcg_tc_plugin_solvers tcg_env) }
 
 -- | Starting from a triple of (given, derived, wanted) constraints,
--- invoke each of the typechecker plugins in turn and return
+-- invoke each of the typechecker constraint-solving plugins in turn and return
 --
 --  * the remaining unmodified constraints,
 --  * constraints that have been solved,
@@ -276,16 +277,16 @@ getTcPlugins = do { tcg_env <- getGblEnv; return (tcg_tc_plugins tcg_env) }
 -- re-invoked and they will see it later).  There is no check that new
 -- work differs from the original constraints supplied to the plugin:
 -- the plugin itself should perform this check if necessary.
-runTcPlugins :: [TcPluginSolver] -> SplitCts -> TcS TcPluginProgress
-runTcPlugins plugins all_cts
-  = foldM do_plugin initialProgress plugins
+runTcPluginSolvers :: [TcPluginSolver] -> SplitCts -> TcS TcPluginProgress
+runTcPluginSolvers solvers all_cts
+  = foldM do_plugin initialProgress solvers
   where
     do_plugin :: TcPluginProgress -> TcPluginSolver -> TcS TcPluginProgress
     do_plugin p solver = do
         result <- runTcPluginTcS (uncurry3 solver (pluginInputCts p))
         return $ progress p result
 
-    progress :: TcPluginProgress -> TcPluginResult -> TcPluginProgress
+    progress :: TcPluginProgress -> TcPluginSolveResult -> TcPluginProgress
     progress p (TcPluginContradiction bad_cts) =
        p { pluginInputCts = discard bad_cts (pluginInputCts p)
          , pluginBadCts   = bad_cts ++ pluginBadCts p
diff --git a/compiler/GHC/Tc/Solver/Monad.hs b/compiler/GHC/Tc/Solver/Monad.hs
index 750b21f9c5..5796e2bd6a 100644
--- a/compiler/GHC/Tc/Solver/Monad.hs
+++ b/compiler/GHC/Tc/Solver/Monad.hs
@@ -1255,7 +1255,7 @@ traceTcS herald doc = wrapTcS (TcM.traceTc herald doc)
 {-# INLINE traceTcS #-}  -- see Note [INLINE conditional tracing utilities]
 
 runTcPluginTcS :: TcPluginM a -> TcS a
-runTcPluginTcS m = wrapTcS . runTcPluginM m =<< getTcEvBindsVar
+runTcPluginTcS = wrapTcS . runTcPluginM
 
 instance HasDynFlags TcS where
     getDynFlags = wrapTcS getDynFlags
diff --git a/compiler/GHC/Tc/Solver/Rewrite.hs b/compiler/GHC/Tc/Solver/Rewrite.hs
index cf95fd8b3a..82c6c580a4 100644
--- a/compiler/GHC/Tc/Solver/Rewrite.hs
+++ b/compiler/GHC/Tc/Solver/Rewrite.hs
@@ -12,6 +12,10 @@ module GHC.Tc.Solver.Rewrite(
 import GHC.Prelude
 
 import GHC.Core.TyCo.Ppr ( pprTyVar )
+import GHC.Tc.Types ( TcGblEnv(tcg_tc_plugin_rewriters),
+                      TcPluginRewriter, TcPluginRewriteResult(..),
+                      RewriteEnv(..),
+                      runTcPluginM )
 import GHC.Tc.Types.Constraint
 import GHC.Core.Predicate
 import GHC.Tc.Utils.TcType
@@ -21,6 +25,7 @@ import GHC.Core.TyCon
 import GHC.Core.TyCo.Rep   -- performs delicate algorithm on types
 import GHC.Core.Coercion
 import GHC.Core.Reduction
+import GHC.Types.Unique.FM
 import GHC.Types.Var
 import GHC.Types.Var.Set
 import GHC.Types.Var.Env
@@ -46,12 +51,6 @@ import Data.List.NonEmpty ( NonEmpty(..) )
 ************************************************************************
 -}
 
-data RewriteEnv
-  = FE { fe_loc     :: !CtLoc             -- See Note [Rewriter CtLoc]
-       , fe_flavour :: !CtFlavour
-       , fe_eq_rel  :: !EqRel             -- See Note [Rewriter EqRels]
-       }
-
 -- | The 'RewriteM' monad is a wrapper around 'TcS' with a 'RewriteEnv'
 newtype RewriteM a
   = RewriteM { runRewriteM :: RewriteEnv -> TcS a }
@@ -98,6 +97,10 @@ traceRewriteM :: String -> SDoc -> RewriteM ()
 traceRewriteM herald doc = liftTcS $ traceTcS herald doc
 {-# INLINE traceRewriteM #-}  -- see Note [INLINE conditional tracing utilities]
 
+getRewriteEnv :: RewriteM RewriteEnv
+getRewriteEnv
+  = mkRewriteM $ \env -> return env
+
 getRewriteEnvField :: (RewriteEnv -> a) -> RewriteM a
 getRewriteEnvField accessor
   = mkRewriteM $ \env -> return (accessor env)
@@ -698,9 +701,16 @@ Note [How to normalise a family application]
 Given an exactly saturated family application, how should we normalise it?
 This Note spells out the algorithm and its reasoning.
 
-STEP 1. Try the famapp-cache. If we get a cache hit, jump to FINISH.
+First, we attempt to directly rewrite the type family application,
+without simplifying any of the arguments first, in an attempt to avoid
+doing unnecessary work.
+
+STEP 1a. Call the rewriting plugins. If any plugin rewrites the type family
+application, jump to FINISH.
 
-STEP 2. Try top-level instances. Note that we haven't simplified the arguments
+STEP 1b. Try the famapp-cache. If we get a cache hit, jump to FINISH.
+
+STEP 1c. Try top-level instances. Remember: we haven't simplified the arguments
   yet. Example:
     type instance F (Maybe a) = Int
     target: F (Maybe (G Bool))
@@ -709,27 +719,31 @@ STEP 2. Try top-level instances. Note that we haven't simplified the arguments
 
   If an instance is found, jump to FINISH.
 
-STEP 3. Rewrite all arguments. This might expose more information so that we
-  can use a top-level instance.
-
-  Continue to the next step.
+STEP 2: At this point we rewrite all arguments. This might expose more
+  information, which might allow plugins to make progress, or allow us to
+  pick up a top-level instance.
 
-STEP 4. Try the inerts. Note that we try the inerts *after* rewriting the
+STEP 3. Try the inerts. Note that we try the inerts *after* rewriting the
   arguments, because the inerts will have rewritten LHSs.
 
   If an inert is found, jump to FINISH.
 
-STEP 5. Try the famapp-cache again. Now that we've revealed more information
-  in the arguments, the cache might be helpful.
+Next, we try STEP 1 again, as we might be able to make further progress after
+having rewritten the arguments:
+
+STEP 4a. Query the rewriting plugins again.
+
+  If any plugin supplies a rewriting, jump to FINISH.
+
+STEP 4b. Try the famapp-cache again.
 
   If we get a cache hit, jump to FINISH.
 
-STEP 6. Try top-level instances, which might trigger now that we know more
-  about the argumnents.
+STEP 4c. Try top-level instances again.
 
   If an instance is found, jump to FINISH.
 
-STEP 7. No progress to be made. Return what we have. (Do not do FINISH.)
+STEP 5: GIVEUP. No progress to be made. Return what we have. (Do not FINISH.)
 
 FINISH 1. We've made a reduction, but the new type may still have more
   work to do. So rewrite the new type.
@@ -737,11 +751,11 @@ FINISH 1. We've made a reduction, but the new type may still have more
 FINISH 2. Add the result to the famapp-cache, connecting the type we started
   with to the one we ended with.
 
-Because STEP 1/2 and STEP 5/6 happen the same way, they are abstracted into
+Because STEP 1{a,b,c} and STEP 4{a,b,c} happen the same way, they are abstracted into
 try_to_reduce.
 
 FINISH is naturally implemented in `finish`. But, Note [rewrite_exact_fam_app performance]
-tells us that we should not add to the famapp-cache after STEP 1/2. So `finish`
+tells us that we should not add to the famapp-cache after STEP 1. So `finish`
 is inlined in that case, and only FINISH 1 is performed.
 
 -}
@@ -768,15 +782,19 @@ rewrite_exact_fam_app :: TyCon -> [TcType] -> RewriteM Reduction
 rewrite_exact_fam_app tc tys
   = do { checkStackDepth (mkTyConApp tc tys)
 
-       -- STEP 1/2. Try to reduce without reducing arguments first.
-       ; result1 <- try_to_reduce tc tys
+       -- Query the typechecking plugins for all their rewriting functions
+       -- which apply to a type family application headed by the TyCon 'tc'.
+       ; tc_rewriters <- getTcPluginRewritersForTyCon tc
+
+       -- STEP 1. Try to reduce without reducing arguments first.
+       ; result1 <- try_to_reduce tc tys tc_rewriters
        ; case result1 of
              -- Don't use the cache;
              -- See Note [rewrite_exact_fam_app performance]
          { Just redn -> finish False redn
          ; Nothing ->
 
-        -- That didn't work. So reduce the arguments, in STEP 3.
+        -- That didn't work. So reduce the arguments, in STEP 2.
     do { eq_rel <- getEqRel
           -- checking eq_rel == NomEq saves ~0.5% in T9872a
        ; ArgsReductions (Reductions cos xis) kind_co <-
@@ -808,7 +826,11 @@ rewrite_exact_fam_app tc tys
                     (args_co `mkTransRedn` redn)
                     kind_co
 
-         -- STEP 4: try the inerts
+              give_up :: Reduction
+              give_up = homogenise $ mkReflRedn role reduced
+                where reduced = mkTyConApp tc xis
+
+         -- STEP 3: try the inerts
        ; result2 <- liftTcS $ lookupFamAppInert tc xis
        ; flavour <- getFlavour
        ; case result2 of
@@ -828,14 +850,12 @@ rewrite_exact_fam_app tc tys
 
          ; _ ->
 
-         -- inert didn't work. Try to reduce again, in STEP 5/6.
-    do { result3 <- try_to_reduce tc xis
+         -- inerts didn't work. Try to reduce again, in STEP 4.
+    do { result3 <- try_to_reduce tc xis tc_rewriters
        ; case result3 of
            Just redn -> finish True (homogenise redn)
-           Nothing   -> -- we have made no progress at all: STEP 7.
-                        return (homogenise $ mkReflRedn role reduced)
-             where
-               reduced = mkTyConApp tc xis }}}}}
+           -- we have made no progress at all: STEP 5 (GIVEUP).
+           _         -> return give_up }}}}}
   where
       -- call this if the above attempts made progress.
       -- This recursively rewrites the result and then adds to the cache
@@ -858,17 +878,21 @@ rewrite_exact_fam_app tc tys
 
 -- Returned coercion is input ~r output, where r is the role in the RewriteM monad
 -- See Note [How to normalise a family application]
-try_to_reduce :: TyCon -> [TcType] -> RewriteM (Maybe Reduction)
-try_to_reduce tc tys
-  = do { result <- liftTcS $ firstJustsM [ lookupFamAppCache tc tys  -- STEP 5
-                                         , matchFam tc tys ]         -- STEP 6
-       ; downgrade result }
+try_to_reduce :: TyCon -> [TcType] -> [TcPluginRewriter]
+              -> RewriteM (Maybe Reduction)
+try_to_reduce tc tys tc_rewriters
+  = do { rewrite_env <- getRewriteEnv
+       ; result <-
+            liftTcS $ firstJustsM
+              [ runTcPluginRewriters rewrite_env tc_rewriters tys -- STEP 1a & STEP 4a
+              , lookupFamAppCache tc tys                          -- STEP 1b & STEP 4b
+              , matchFam tc tys ]                                 -- STEP 1c & STEP 4c
+       ; traverse downgrade result }
   where
     -- The result above is always Nominal. We might want a Representational
     -- coercion; this downgrades (and prints, out of convenience).
-    downgrade :: Maybe Reduction -> RewriteM (Maybe Reduction)
-    downgrade Nothing = return Nothing
-    downgrade result@(Just redn)
+    downgrade :: Reduction -> RewriteM Reduction
+    downgrade redn
       = do { traceRewriteM "Eager T.F. reduction success" $
              vcat [ ppr tc
                   , ppr tys
@@ -878,8 +902,45 @@ try_to_reduce tc tys
               -- manually doing it this way avoids allocation in the vastly
               -- common NomEq case
            ; case eq_rel of
-               NomEq  -> return result
-               ReprEq -> return $ Just (mkSubRedn redn) }
+               NomEq  -> return redn
+               ReprEq -> return $ mkSubRedn redn }
+
+-- Retrieve all type-checking plugins that can rewrite a (saturated) type-family application
+-- headed by the given 'TyCon`.
+getTcPluginRewritersForTyCon :: TyCon -> RewriteM [TcPluginRewriter]
+getTcPluginRewritersForTyCon tc
+  = liftTcS $ do { rewriters <- tcg_tc_plugin_rewriters <$> getGblEnv
+                 ; return (lookupWithDefaultUFM rewriters [] tc) }
+
+-- Run a collection of rewriting functions obtained from type-checking plugins,
+-- querying in sequence if any plugin wants to rewrite the type family
+-- applied to the given arguments.
+--
+-- Note that the 'TcPluginRewriter's provided all pertain to the same type family
+-- (the 'TyCon' of which has been obtained ahead of calling this function).
+runTcPluginRewriters :: RewriteEnv
+                     -> [TcPluginRewriter]
+                     -> [TcType]
+                     -> TcS (Maybe Reduction)
+runTcPluginRewriters rewriteEnv rewriterFunctions tys
+  | null rewriterFunctions
+  = return Nothing -- short-circuit for common case
+  | otherwise
+  = do { givens <- getInertGivens
+       ; runRewriters givens rewriterFunctions }
+  where
+  runRewriters :: [Ct] -> [TcPluginRewriter] -> TcS (Maybe Reduction)
+  runRewriters _ []
+    = return Nothing
+  runRewriters givens (rewriter:rewriters)
+    = do
+        rewriteResult <- wrapTcS . runTcPluginM $ rewriter rewriteEnv givens tys
+        case rewriteResult of
+           TcPluginRewriteTo
+             { tcPluginReduction    = redn
+             , tcRewriterNewWanteds = wanteds
+             } -> do { emitWork wanteds; return $ Just redn }
+           TcPluginNoRewrite {} -> runRewriters givens rewriters
 
 {-
 ************************************************************************
diff --git a/compiler/GHC/Tc/Types.hs b/compiler/GHC/Tc/Types.hs
index b3f47a8dc2..684bee4a59 100644
--- a/compiler/GHC/Tc/Types.hs
+++ b/compiler/GHC/Tc/Types.hs
@@ -1,6 +1,7 @@
 
-{-# LANGUAGE DeriveFunctor              #-}
+{-# LANGUAGE DerivingStrategies         #-}
 {-# LANGUAGE ExistentialQuantification  #-}
+{-# LANGUAGE GADTs                      #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 
 {-
@@ -32,6 +33,7 @@ module GHC.Tc.Types(
         setLclEnvLoc, getLclEnvLoc,
         IfGblEnv(..), IfLclEnv(..),
         tcVisibleOrphanMods,
+        RewriteEnv(..),
 
         -- Frontend types (shouldn't really be here)
         FrontendResult(..),
@@ -72,9 +74,9 @@ module GHC.Tc.Types(
         getPlatform,
 
         -- Constraint solver plugins
-        TcPlugin(..), TcPluginResult(..), TcPluginSolver,
-        TcPluginM, runTcPluginM, unsafeTcPluginTcM,
-        getEvBindsTcPluginM,
+        TcPlugin(..), TcPluginSolveResult(..), TcPluginRewriteResult(..),
+        TcPluginSolver, TcPluginRewriter,
+        TcPluginM(runTcPluginM), unsafeTcPluginTcM,
 
         -- Role annotations
         RoleAnnotEnv, emptyRoleAnnotEnv, mkRoleAnnotEnv,
@@ -103,6 +105,7 @@ import GHC.Tc.Types.Evidence
 import {-# SOURCE #-} GHC.Tc.Errors.Hole.FitTypes ( HoleFitPlugin )
 import GHC.Tc.Errors.Types
 
+import GHC.Core.Reduction ( Reduction(..) )
 import GHC.Core.Type
 import GHC.Core.TyCon  ( TyCon, tyConKind )
 import GHC.Core.PatSyn ( PatSyn )
@@ -110,6 +113,7 @@ import GHC.Core.Lint   ( lintAxioms )
 import GHC.Core.UsageEnv
 import GHC.Core.InstEnv
 import GHC.Core.FamInstEnv
+import GHC.Core.Predicate
 
 import GHC.Types.Id         ( idType, idName )
 import GHC.Types.FieldLabel ( FieldLabel )
@@ -151,7 +155,6 @@ import GHC.Utils.Logger
 
 import GHC.Builtin.Names ( isUnboundName )
 
-import Control.Monad (ap)
 import Data.Set      ( Set )
 import qualified Data.Set as S
 import Data.Map ( Map )
@@ -250,6 +253,40 @@ instance ContainsLogger (Env gbl lcl) where
 instance ContainsModule gbl => ContainsModule (Env gbl lcl) where
     extractModule env = extractModule (env_gbl env)
 
+{-
+************************************************************************
+*                                                                      *
+*                            RewriteEnv
+*                     The rewriting environment
+*                                                                      *
+************************************************************************
+-}
+
+-- | A 'RewriteEnv' carries the necessary context for performing rewrites
+-- (i.e. type family reductions and following filled-in metavariables)
+-- in the solver.
+data RewriteEnv
+  = FE { fe_loc     :: !CtLoc
+       -- ^ In which context are we rewriting?
+       --
+       -- Type-checking plugins might want to use this location information
+       -- when emitting new Wanted constraints when rewriting type family
+       -- applications. This ensures that such Wanted constraints will,
+       -- when unsolved, give rise to error messages with the
+       -- correct source location.
+
+       -- Within GHC, we use this field to keep track of reduction depth.
+       -- See Note [Rewriter CtLoc] in GHC.Tc.Solver.Rewrite.
+       , fe_flavour :: !CtFlavour
+       , fe_eq_rel  :: !EqRel
+       -- ^ At what role are we rewriting?
+       --
+       -- See Note [Rewriter EqRels] in GHC.Tc.Solver.Rewrite
+       }
+-- RewriteEnv is mostly used in @GHC.Tc.Solver.Rewrite@, but it is defined
+-- here so that it can also be passed to rewriting plugins.
+-- See the 'tcPluginRewrite' field of 'TcPlugin'.
+
 
 {-
 ************************************************************************
@@ -572,8 +609,13 @@ data TcGblEnv
         -- are supplied (#19714), or if those reasons have already been
         -- reported by GHC.Driver.Main.markUnsafeInfer
 
-        tcg_tc_plugins :: [TcPluginSolver],
-        -- ^ A list of user-defined plugins for the constraint solver.
+        tcg_tc_plugin_solvers :: [TcPluginSolver],
+        -- ^ A list of user-defined type-checking plugins for constraint solving.
+
+        tcg_tc_plugin_rewriters :: UniqFM TyCon [TcPluginRewriter],
+        -- ^ A collection of all the user-defined type-checking plugins for rewriting
+        -- type family applications, collated by their type family 'TyCon's.
+
         tcg_hf_plugins :: [HoleFitPlugin],
         -- ^ A list of user-defined plugins for hole fit suggestions.
 
@@ -1665,66 +1707,106 @@ Constraint Solver Plugins
 -------------------------
 -}
 
-type TcPluginSolver = [Ct]    -- given
-                   -> [Ct]    -- derived
-                   -> [Ct]    -- wanted
-                   -> TcPluginM TcPluginResult
-
-newtype TcPluginM a = TcPluginM (EvBindsVar -> TcM a) deriving (Functor)
-
-instance Applicative TcPluginM where
-  pure x = TcPluginM (const $ pure x)
-  (<*>) = ap
-
-instance Monad TcPluginM where
-  TcPluginM m >>= k =
-    TcPluginM (\ ev -> do a <- m ev
-                          runTcPluginM (k a) ev)
-
-instance MonadFail TcPluginM where
-  fail x   = TcPluginM (const $ fail x)
-
-runTcPluginM :: TcPluginM a -> EvBindsVar -> TcM a
-runTcPluginM (TcPluginM m) = m
+-- | The @solve@ function of a type-checking plugin takes in Given, Derived
+-- and Wanted constraints, and should return a 'TcPluginSolveResult'
+-- indicating which Wanted constraints it could solve, or whether any are
+-- insoluble.
+type TcPluginSolver = [Ct] -- ^ Givens
+                   -> [Ct] -- ^ Deriveds
+                   -> [Ct] -- ^ Wanteds
+                   -> TcPluginM TcPluginSolveResult
+
+-- | For rewriting type family applications, a type-checking plugin provides
+-- a function of this type for each type family 'TyCon'.
+--
+-- The function is provided with the current set of Given constraints, together
+-- with the arguments to the type family.
+-- The type family application will always be fully saturated.
+type TcPluginRewriter
+  =  RewriteEnv -- ^ Rewriter environment
+  -> [Ct]       -- ^ Givens
+  -> [TcType]   -- ^ type family arguments
+  -> TcPluginM TcPluginRewriteResult
+
+-- | 'TcPluginM' is the monad in which type-checking plugins operate.
+newtype TcPluginM a = TcPluginM { runTcPluginM :: TcM a }
+  deriving newtype (Functor, Applicative, Monad, MonadFail)
 
 -- | This function provides an escape for direct access to
 -- the 'TcM` monad.  It should not be used lightly, and
 -- the provided 'TcPluginM' API should be favoured instead.
 unsafeTcPluginTcM :: TcM a -> TcPluginM a
-unsafeTcPluginTcM = TcPluginM . const
-
--- | Access the 'EvBindsVar' carried by the 'TcPluginM' during
--- constraint solving.  Returns 'Nothing' if invoked during
--- 'tcPluginInit' or 'tcPluginStop'.
-getEvBindsTcPluginM :: TcPluginM EvBindsVar
-getEvBindsTcPluginM = TcPluginM return
-
+unsafeTcPluginTcM = TcPluginM
 
 data TcPlugin = forall s. TcPlugin
-  { tcPluginInit  :: TcPluginM s
+  { tcPluginInit :: TcPluginM s
     -- ^ Initialize plugin, when entering type-checker.
 
-  , tcPluginSolve :: s -> TcPluginSolver
+  , tcPluginSolve :: s -> EvBindsVar -> TcPluginSolver
     -- ^ Solve some constraints.
-    -- TODO: WRITE MORE DETAILS ON HOW THIS WORKS.
-
-  , tcPluginStop  :: s -> TcPluginM ()
+    --
+    -- This function will be invoked at two points in the constraint solving
+    -- process: once to simplify Given constraints, and once to solve
+    -- Wanted constraints. In the first case (and only in the first case),
+    -- no Wanted constraints will be passed to the plugin.
+    --
+    -- The plugin can either return a contradiction,
+    -- or specify that it has solved some constraints (with evidence),
+    -- and possibly emit additional constraints. These returned constraints
+    -- must be Givens in the first case, and Wanteds in the second.
+    --
+    -- Use @ \\ _ _ _ _ _ -> pure $ TcPluginOK [] [] @ if your plugin
+    -- does not provide this functionality.
+
+  , tcPluginRewrite :: s -> UniqFM TyCon TcPluginRewriter
+    -- ^ Rewrite saturated type family applications.
+    --
+    -- The plugin is expected to supply a mapping from type family names to
+    -- rewriting functions. For each type family 'TyCon', the plugin should
+    -- provide a function which takes in the given constraints and arguments
+    -- of a saturated type family application, and return a possible rewriting.
+    -- See 'TcPluginRewriter' for the expected shape of such a function.
+    --
+    -- Use @ \\ _ -> emptyUFM @ if your plugin does not provide this functionality.
+
+  , tcPluginStop :: s -> TcPluginM ()
    -- ^ Clean up after the plugin, when exiting the type-checker.
   }
 
-data TcPluginResult
+data TcPluginSolveResult
   = TcPluginContradiction [Ct]
     -- ^ The plugin found a contradiction.
     -- The returned constraints are removed from the inert set,
     -- and recorded as insoluble.
+    --
+    -- The returned list of constraints should never be empty.
 
-  | TcPluginOk [(EvTerm,Ct)] [Ct]
+  | TcPluginOk
+    { tcPluginSolvedCts :: [(EvTerm,Ct)]
+    , tcPluginNewCts :: [Ct] }
     -- ^ The first field is for constraints that were solved.
     -- These are removed from the inert set,
     -- and the evidence for them is recorded.
     -- The second field contains new work, that should be processed by
     -- the constraint solver.
 
+
+data TcPluginRewriteResult
+  =
+  -- | The plugin does not rewrite the type family application.
+    TcPluginNoRewrite
+
+  -- | The plugin rewrites the type family application
+  -- providing a rewriting together with evidence: a 'Reduction',
+  -- which contains the rewritten type together with a 'Coercion'
+  -- whose right-hand-side type is the rewritten type.
+  --
+  -- The plugin can also emit additional Wanted constraints.
+  | TcPluginRewriteTo
+    { tcPluginReduction    :: !Reduction
+    , tcRewriterNewWanteds :: [Ct]
+    }
+
 {- *********************************************************************
 *                                                                      *
                         Role annotations
diff --git a/compiler/GHC/Tc/Utils/Monad.hs b/compiler/GHC/Tc/Utils/Monad.hs
index 3a38e56f6c..1645333f32 100644
--- a/compiler/GHC/Tc/Utils/Monad.hs
+++ b/compiler/GHC/Tc/Utils/Monad.hs
@@ -205,6 +205,7 @@ import GHC.Types.SrcLoc
 import GHC.Types.Name.Env
 import GHC.Types.Name.Set
 import GHC.Types.Name.Ppr
+import GHC.Types.Unique.FM ( emptyUFM )
 import GHC.Types.Unique.Supply
 import GHC.Types.Annotations
 import GHC.Types.Basic( TopLevelFlag, TypeOrKind(..) )
@@ -348,7 +349,8 @@ initTc hsc_env hsc_src keep_rn_syntax mod loc do_this
                 tcg_safe_infer     = infer_var,
                 tcg_safe_infer_reasons = infer_reasons_var,
                 tcg_dependent_files = dependent_files_var,
-                tcg_tc_plugins     = [],
+                tcg_tc_plugin_solvers   = [],
+                tcg_tc_plugin_rewriters = emptyUFM,
                 tcg_hf_plugins     = [],
                 tcg_top_loc        = loc,
                 tcg_static_wc      = static_wc_var,
diff --git a/compiler/GHC/Types/Unique/FM.hs b/compiler/GHC/Types/Unique/FM.hs
index 35a8a2b3fc..7c80359d0e 100644
--- a/compiler/GHC/Types/Unique/FM.hs
+++ b/compiler/GHC/Types/Unique/FM.hs
@@ -57,6 +57,7 @@ module GHC.Types.Unique.FM (
         mergeUFM,
         plusMaybeUFM_C,
         plusUFMList,
+        sequenceUFMList,
         minusUFM,
         intersectUFM,
         intersectUFM_C,
@@ -301,6 +302,15 @@ plusMaybeUFM_C f (UFM xm) (UFM ym)
 plusUFMList :: [UniqFM key elt] -> UniqFM key elt
 plusUFMList = foldl' plusUFM emptyUFM
 
+sequenceUFMList :: forall key elt. [UniqFM key elt] -> UniqFM key [elt]
+sequenceUFMList = foldr (plusUFM_CD2 cons) emptyUFM
+  where
+    cons :: Maybe elt -> Maybe [elt] -> [elt]
+    cons (Just x) (Just ys) = x : ys
+    cons Nothing  (Just ys) = ys
+    cons (Just x) Nothing   = [x]
+    cons Nothing  Nothing   = []
+
 minusUFM :: UniqFM key elt1 -> UniqFM key elt2 -> UniqFM key elt1
 minusUFM (UFM x) (UFM y) = UFM (M.difference x y)
 
diff --git a/docs/users_guide/extending_ghc.rst b/docs/users_guide/extending_ghc.rst
index 340c324614..0020c0213f 100644
--- a/docs/users_guide/extending_ghc.rst
+++ b/docs/users_guide/extending_ghc.rst
@@ -545,14 +545,28 @@ is defined thus:
 ::
 
     data TcPlugin = forall s . TcPlugin
-      { tcPluginInit  :: TcPluginM s
-      , tcPluginSolve :: s -> TcPluginSolver
-      , tcPluginStop  :: s -> TcPluginM ()
+      { tcPluginInit    :: TcPluginM s
+      , tcPluginSolve   :: s -> EvBindsVar -> TcPluginSolver
+      , tcPluginRewrite :: s -> UniqFM TyCon TcPluginRewriter
+      , tcPluginStop    :: s -> TcPluginM ()
       }
 
     type TcPluginSolver = [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginResult
 
-    data TcPluginResult = TcPluginContradiction [Ct] | TcPluginOk [(EvTerm,Ct)] [Ct]
+    type TcPluginRewriter = RewriteEnv -> [Ct] -> [Type] -> TcPluginM TcPluginRewriteResult
+
+    data TcPluginResult
+      = TcPluginContradiction [Ct]
+      | TcPluginOk
+        { tcPluginSolvedCts :: [(EvTerm,Ct)]
+        , tcPluginNewCts :: [Ct] }
+
+    data TcPluginRewriteResult
+      = TcPluginNoRewrite
+      | TcPluginRewriteTo
+          { tcPluginRewriteTo    :: Reduction
+          , tcRewriterNewWanteds :: [Ct]
+          }
 
 (The details of this representation are subject to change as we gain
 more experience writing typechecker plugins. It should not be assumed to
@@ -565,7 +579,7 @@ The basic idea is as follows:
    in the context, initialise mutable state or open a connection to an
    external process (e.g. an external SMT solver). The plugin can return
    a result of any type it likes, and the result will be passed to the
-   other two fields.
+   other fields of the ``TcPlugin`` record.
 
 -  During constraint solving, GHC repeatedly calls ``tcPluginSolve``.
    This function is provided with the current set of constraints, and
@@ -574,6 +588,13 @@ The basic idea is as follows:
    makes progress, GHC will re-start the constraint solving pipeline,
    looping until a fixed point is reached.
 
+-  When rewriting type family applications, GHC calls ``tcPluginRewriter``.
+   The plugin supplies a collection of type families which it is interested
+   in rewriting. For each of those, the rewriter is provided with the
+   the arguments to that type family, as well as the current collection of
+   Given constraints. The plugin can then specify a rewriting for this
+   type family application, if desired.
+
 -  Finally, GHC calls ``tcPluginStop`` after constraint solving is
    finished, allowing the plugin to dispose of any resources it has
    allocated (e.g. terminating the SMT solver process).
@@ -602,19 +623,27 @@ The key component of a typechecker plugin is a function of type
     solve :: [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginResult
     solve givens deriveds wanteds = ...
 
-This function will be invoked at two points in the constraint solving
-process: after simplification of given constraints, and after
-unflattening of wanted constraints. The two phases can be distinguished
-because the deriveds and wanteds will be empty in the first case. In
-each case, the plugin should either
+This function will be invoked in two different ways:
+
+1. after simplification of Given constraints, where the plugin gets the
+   opportunity to rewrite givens,
+
+2. after GHC has attempted to solve Wanted constraints.
+
+The two ways can be distinguished by checking the Wanted constraints: in the
+first case (and the first case only), the plugin will be passed an empty list
+of Wanted constraints.
 
--  return ``TcPluginContradiction`` with a list of impossible
-   constraints (which must be a subset of those passed in), so they can
-   be turned into errors; or
+The plugin is then expected to respond in either of the following ways:
 
--  return ``TcPluginOk`` with lists of solved and new constraints (the
-   former must be a subset of those passed in and must be supplied with
-   corresponding evidence terms).
+* return ``TcPluginOk`` with lists of solved and new constraints, or
+
+* return ``TcPluginContradiction`` with a list of impossible
+  constraints, so they can be turned into errors.
+
+In both cases, the plugin must respond with constraints of the same flavour,
+i.e. in (1) it should return only Givens, and for (2) it should return only
+Wanteds (or Deriveds); all other constraints will be ignored.
 
 If the plugin cannot make any progress, it should return
 ``TcPluginOk [] []``. Otherwise, if there were any new constraints, the
@@ -630,15 +659,62 @@ by solving or contradicting them).
 
 Constraints that have been solved by the plugin must be provided with
 evidence in the form of an ``EvTerm`` of the type of the constraint.
-This evidence is ignored for given and derived constraints, which GHC
+This evidence is ignored for Given and Derived constraints, which GHC
 "solves" simply by discarding them; typically this is used when they are
-uninformative (e.g. reflexive equations). For wanted constraints, the
+uninformative (e.g. reflexive equations). For Wanted constraints, the
 evidence will form part of the Core term that is generated after
 typechecking, and can be checked by ``-dcore-lint``. It is possible for
 the plugin to create equality axioms for use in evidence terms, but GHC
 does not check their consistency, and inconsistent axiom sets may lead
 to segfaults or other runtime misbehaviour.
 
+.. _type-family-rewriting-with-plugins:
+
+Type family rewriting with plugins
+^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+Typechecker plugins can also directly rewrite type family applications,
+by supplying the ``tcPluginRewrite`` field of the ``TcPlugin`` record.
+
+::
+
+    tcPluginRewrite :: s -> UniqFM TyCon TcPluginRewriter
+
+That is, the plugin registers a map, from a type family's ``TyCon`` to its
+associated rewriting function: ::
+
+    type TcPluginRewriter = [Ct] -> [Type] -> TcPluginM TcPluginRewriteResult
+
+This rewriting function is supplied with the Given constraints from the current
+context, and the type family arguments.
+Note that the type family application is guaranteed to be exactly saturated.
+This function should then return a possible rewriting of the type family
+application, by means of the following datatype: ::
+
+    data TcPluginRewriteResult
+      = TcPluginNoRewrite
+      | TcPluginRewriteTo
+          { tcPluginRewriteTo    :: Reduction
+          , tcRewriterNewWanteds :: [Ct]
+          }
+
+That is, the rewriter can specify a rewriting of the type family application --
+in which case it can also emit new Wanted constraints -- or it can do nothing.
+
+To specify a rewriting, the plugin must provide a ``Reduction``, which is
+defined as follows: ::
+
+    data Reduction = Reduction Coercion !Type
+
+That is, on top of specifying what type the type-family application rewrites to,
+the plugin must also supply a coercion which witnesses this rewriting: ::
+
+  co :: F orig_arg_1 ... orig_arg_n ~ rewritten_ty
+
+Note in particular that the LHS type of the coercion should be the original
+type-family application, while its RHS type is the type that the plugin wants
+to rewrite the type-family application to.
+
 .. _source-plugins:
 
 Source plugins
diff --git a/testsuite/tests/ghci/should_run/tc-plugin-ghci/TcPluginGHCi.hs b/testsuite/tests/ghci/should_run/tc-plugin-ghci/TcPluginGHCi.hs
index b16e217acd..b194d8f2b5 100644
--- a/testsuite/tests/ghci/should_run/tc-plugin-ghci/TcPluginGHCi.hs
+++ b/testsuite/tests/ghci/should_run/tc-plugin-ghci/TcPluginGHCi.hs
@@ -1,7 +1,8 @@
 module TcPluginGHCi where
 
-import GHC.Tc.Utils.Monad ( TcPlugin(..), TcPluginResult(..) )
+import GHC.Tc.Utils.Monad ( TcPlugin(..), TcPluginSolveResult(..), TcPluginRewriteResult(..) )
 import GHC.Driver.Plugins ( defaultPlugin, Plugin(..), CommandLineOption )
+import GHC.Types.Unique.FM ( emptyUFM )
 import Debug.Trace
 
 plugin :: Plugin
@@ -9,7 +10,8 @@ plugin = defaultPlugin { tcPlugin = Just . thePlugin }
 
 thePlugin :: [CommandLineOption] -> TcPlugin
 thePlugin opts = TcPlugin
-  { tcPluginInit  = trace "TcPluginGHCi" (return ())
-  , tcPluginSolve = \_ _ _ _ -> return $ TcPluginOk [] []
-  , tcPluginStop  = \_ -> return ()
+  { tcPluginInit    = trace "TcPluginGHCi" (return ())
+  , tcPluginSolve   = \_ _ _ _ _ -> return $ TcPluginOk [] []
+  , tcPluginRewrite = \_ -> emptyUFM
+  , tcPluginStop    = \_ -> return ()
   }
diff --git a/testsuite/tests/tcplugins/ArgsPlugin.hs b/testsuite/tests/tcplugins/ArgsPlugin.hs
index c4ebbb0305..c25c8dc8a3 100644
--- a/testsuite/tests/tcplugins/ArgsPlugin.hs
+++ b/testsuite/tests/tcplugins/ArgsPlugin.hs
@@ -24,16 +24,16 @@ import GHC.Plugins
 import GHC.Tc.Plugin
   ( TcPluginM )
 import GHC.Tc.Types
-  ( TcPluginResult(..) )
+  ( TcPluginSolveResult(..) )
 import GHC.Tc.Types.Constraint
   ( Ct(..) )
 import GHC.Tc.Types.Evidence
-  ( EvTerm(EvExpr) )
+  ( EvBindsVar, EvTerm(EvExpr) )
 
 -- common
 import Common
   ( PluginDefs(..)
-  , mkPlugin
+  , mkPlugin, don'tRewrite
   )
 
 --------------------------------------------------------------------------------
@@ -49,14 +49,14 @@ import Common
 -- as an argument to the plugin.
 
 plugin :: Plugin
-plugin = mkPlugin solver
+plugin = mkPlugin solver don'tRewrite
 
 -- Solve "MyClass Integer" with a class dictionary that depends on
 -- a plugin argument.
 solver :: [String]
-       -> PluginDefs -> [Ct] -> [Ct] -> [Ct]
-       -> TcPluginM TcPluginResult
-solver args defs _gs _ds ws = do
+       -> PluginDefs -> EvBindsVar -> [Ct] -> [Ct] -> [Ct]
+       -> TcPluginM TcPluginSolveResult
+solver args defs _ev _gs _ds ws = do
   let
     argsVal :: Integer
     argsVal = case args of
diff --git a/testsuite/tests/tcplugins/Common.hs b/testsuite/tests/tcplugins/Common.hs
index 615897b910..e3ec1338a5 100644
--- a/testsuite/tests/tcplugins/Common.hs
+++ b/testsuite/tests/tcplugins/Common.hs
@@ -4,6 +4,7 @@
 module Common
   ( PluginDefs(..)
   , mkPlugin
+  , don'tSolve, don'tRewrite
   )
   where
 
@@ -28,11 +29,17 @@ import GHC.Tc.Plugin
   , tcLookupClass, tcLookupDataCon, tcLookupTyCon
   )
 import GHC.Tc.Types
-  ( TcPlugin(..), TcPluginResult )
+  ( TcPlugin(..), TcPluginSolveResult(..), TcPluginRewriteResult(..)
+  , TcPluginRewriter
+  )
 import GHC.Tc.Types.Constraint
   ( Ct )
+import GHC.Tc.Types.Evidence
+  ( EvBindsVar )
 import GHC.Types.Name.Occurrence
   ( mkClsOcc, mkDataOcc, mkTcOcc )
+import GHC.Types.Unique.FM
+  ( UniqFM, emptyUFM )
 import GHC.Unit.Finder
   ( FindResult(..) )
 import GHC.Unit.Module
@@ -81,19 +88,28 @@ lookupDefs = do
   add                           <- tcLookupTyCon   =<< lookupOrig defs ( mkTcOcc   "Add"      )
   pure ( PluginDefs { .. } )
 
-mkPlugin :: ( [String] -> PluginDefs -> [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginResult )
+mkPlugin :: ( [String] -> PluginDefs -> EvBindsVar -> [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginSolveResult )
+         -> ( [String] -> PluginDefs -> UniqFM TyCon TcPluginRewriter )
          -> Plugin
-mkPlugin solve =
+mkPlugin solve rewrite =
   defaultPlugin
-    { tcPlugin        = \ args -> Just $ mkTcPlugin ( solve args )
+    { tcPlugin        = \ args -> Just $ mkTcPlugin ( solve args ) ( rewrite args )
     , pluginRecompile = purePlugin
     }
 
-mkTcPlugin :: ( PluginDefs -> [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginResult )
+mkTcPlugin :: ( PluginDefs -> EvBindsVar -> [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginSolveResult )
+           -> ( PluginDefs -> UniqFM TyCon TcPluginRewriter )
            -> TcPlugin
-mkTcPlugin solve =
+mkTcPlugin solve rewrite =
   TcPlugin
-    { tcPluginInit  = lookupDefs
-    , tcPluginSolve = solve
-    , tcPluginStop  = \ _ -> pure ()
+    { tcPluginInit    = lookupDefs
+    , tcPluginSolve   = solve
+    , tcPluginRewrite = rewrite
+    , tcPluginStop    = \ _ -> pure ()
     }
+
+don'tSolve :: [String] -> s -> EvBindsVar -> [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginSolveResult
+don'tSolve _ _ _ _ _ _ = pure $ TcPluginOk [] []
+
+don'tRewrite :: [String] -> s -> UniqFM TyCon TcPluginRewriter
+don'tRewrite _ _ = emptyUFM
diff --git a/testsuite/tests/tcplugins/NullaryPlugin.hs b/testsuite/tests/tcplugins/NullaryPlugin.hs
index a8176c16b3..060c1aa2f2 100644
--- a/testsuite/tests/tcplugins/NullaryPlugin.hs
+++ b/testsuite/tests/tcplugins/NullaryPlugin.hs
@@ -18,16 +18,16 @@ import GHC.Plugins
 import GHC.Tc.Plugin
   ( TcPluginM )
 import GHC.Tc.Types
-  ( TcPluginResult(..) )
+  ( TcPluginSolveResult(..) )
 import GHC.Tc.Types.Constraint
   ( Ct(..) )
 import GHC.Tc.Types.Evidence
-  ( EvTerm(EvExpr) )
+  ( EvBindsVar, EvTerm(EvExpr) )
 
 -- common
 import Common
   ( PluginDefs(..)
-  , mkPlugin
+  , mkPlugin, don'tRewrite
   )
 
 --------------------------------------------------------------------------------
@@ -38,13 +38,13 @@ import Common
 -- in which case we provide evidence (a nullary dictionary).
 
 plugin :: Plugin
-plugin = mkPlugin solver
+plugin = mkPlugin solver don'tRewrite
 
 -- Solve "Nullary".
 solver :: [String]
-       -> PluginDefs -> [Ct] -> [Ct] -> [Ct]
-       -> TcPluginM TcPluginResult
-solver _args defs _gs _ds ws = do
+       -> PluginDefs -> EvBindsVar -> [Ct] -> [Ct] -> [Ct]
+       -> TcPluginM TcPluginSolveResult
+solver _args defs _ev _gs _ds ws = do
   solved <- catMaybes <$> traverse ( solveCt defs ) ws
   pure $ TcPluginOk solved []
 
diff --git a/testsuite/tests/tcplugins/RewritePerfDefs.hs b/testsuite/tests/tcplugins/RewritePerfDefs.hs
new file mode 100644
index 0000000000..ce1e0fa6d5
--- /dev/null
+++ b/testsuite/tests/tcplugins/RewritePerfDefs.hs
@@ -0,0 +1,102 @@
+
+-- Testing performance of type-checking rewriting plugins.
+-- Test based on T9872b.
+
+{-# OPTIONS_GHC -freduction-depth=400 #-}
+
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE DataKinds, KindSignatures, PolyKinds #-}
+{-# LANGUAGE TypeOperators #-}
+
+module RewritePerfDefs where
+
+data Color = R | G | B | W
+
+data Cube = Cube Color Color Color Color Color Color
+
+type family And (b1 :: Bool) (b2 :: Bool) :: Bool where
+    And True True = True
+    And b1 b2 = False
+
+type family NE (x :: Color) (y :: Color) :: Bool where
+    NE x x = False
+    NE x y = True
+
+type family EQ (x :: Color) (y :: Color) :: Bool where
+    EQ a a = True
+    EQ a b = False
+
+type family All (l :: [Bool]) :: Bool where
+    All '[] = True
+    All (False ': xs) = False
+    All (True ': xs) = All xs
+
+type family ListConcat (xs :: [k]) (ys :: [k]) :: [k] where
+    ListConcat '[] ys = ys
+    ListConcat (x ': xs) ys = x ': ListConcat xs ys
+
+type family AppendIf (b :: Bool) (a :: [Cube]) (as :: [[Cube]]) :: [[Cube]] where
+    AppendIf False a as = as
+    AppendIf True a as = a ': as
+
+data Transform = Rotate | Twist | Flip
+
+type family Apply (f :: Transform) (a :: Cube) :: Cube where
+    Apply Rotate ('Cube u f r b l d) = ('Cube u r b l f d)
+    Apply Twist  ('Cube u f r b l d) = ('Cube f r u l d b)
+    Apply Flip   ('Cube u f r b l d) = ('Cube d l b r f u)
+
+type family Map (f :: Transform) (as :: [Cube]) :: [Cube] where
+    Map f '[] = '[]
+    Map f (a ': as) = (Apply f a) ': (Map f as)
+
+type family MapAppend (f :: Transform) (as :: [Cube]) :: [Cube] where
+    MapAppend f xs = ListConcat xs (Map f xs)
+
+type family MapAppend2 (f :: Transform) (as :: [Cube]) :: [Cube] where
+    MapAppend2 f xs = ListConcat xs (MapAppend f (Map f xs))
+
+type family MapAppend3 (f :: Transform) (as :: [Cube]) :: [Cube] where
+    MapAppend3 f xs = ListConcat xs (MapAppend2 f (Map f xs))
+
+type family Iterate2 (f :: Transform) (as :: [Cube]) :: [Cube] where
+    Iterate2 f '[] = '[]
+    Iterate2 f (a ': as) = ListConcat [Apply f a, a] (Iterate2 f as)
+
+type family Iterate3 (f :: Transform) (as :: [Cube]) :: [Cube] where
+    Iterate3 f '[] = '[]
+    Iterate3 f (a ': as) =
+        ListConcat [a, Apply f a, Apply f (Apply f a)] (Iterate3 f as)
+
+type family Iterate4 (f :: Transform) (as :: [Cube]) :: [Cube] where
+    Iterate4 f '[] = '[]
+    Iterate4 f (a ': as) =
+        ListConcat [a, Apply f a, Apply f (Apply f a), Apply f (Apply f (Apply f a))]
+                   (Iterate4 f as)
+
+type family Orientations (c :: Cube) :: [Cube] where
+    Orientations c = MapAppend3 Rotate (MapAppend2 Twist (MapAppend Flip '[c]))
+
+type family Compatible (c :: Cube) (d :: Cube) :: Bool where
+    Compatible ('Cube u1 f1 r1 b1 l1 d1) ('Cube u2 f2 r2 b2 l2 d2) =
+        All [NE f1 f2, NE r1 r2, NE b1 b2, NE l1 l2]
+
+type family Allowed (c :: Cube) (cs :: [Cube]) :: Bool where
+    Allowed c '[] = True
+    Allowed c (s ': ss) = And (Compatible c s) (Allowed c ss)
+
+type family MatchingOrientations (as :: [Cube]) (sol :: [Cube]) :: [[Cube]] where
+    MatchingOrientations '[] sol = '[]
+    MatchingOrientations (o ': os) sol =
+        AppendIf (Allowed o sol) (o ': sol) (MatchingOrientations os sol)
+
+type family AllowedCombinations (os :: [Cube]) (sols :: [[Cube]]) where
+    AllowedCombinations os '[] = '[]
+    AllowedCombinations os (sol ': sols) =
+        ListConcat (MatchingOrientations os sol) (AllowedCombinations os sols)
+
+type family Solutions (cs :: [Cube]) :: [[Cube]] where
+    Solutions '[] = '[ '[] ]
+    Solutions (c ': cs) = AllowedCombinations (Orientations c) (Solutions cs)
diff --git a/testsuite/tests/tcplugins/RewritePerfPlugin.hs b/testsuite/tests/tcplugins/RewritePerfPlugin.hs
new file mode 100644
index 0000000000..8659375c5d
--- /dev/null
+++ b/testsuite/tests/tcplugins/RewritePerfPlugin.hs
@@ -0,0 +1,96 @@
+{-# LANGUAGE TupleSections #-}
+
+module RewritePerfPlugin where
+-- Testing performance of rewriting type-family applications.
+
+-- ghc
+import GHC.Core
+  ( Expr(Coercion) )
+import GHC.Core.Coercion
+  ( mkUnivCo )
+import GHC.Core.TyCo.Rep
+  ( Type, UnivCoProvenance(PluginProv) )
+import GHC.Core.TyCon
+  ( TyCon )
+import GHC.Core.Type
+  ( eqType, mkTyConApp, splitTyConApp_maybe )
+import GHC.Plugins
+  ( Plugin(..), defaultPlugin, purePlugin )
+import GHC.Tc.Plugin
+  ( TcPluginM
+  , findImportedModule, lookupOrig
+  , tcLookupClass, tcLookupDataCon, tcLookupTyCon
+  , unsafeTcPluginTcM
+  )
+import GHC.Tc.Types
+  ( TcPlugin(..)
+  , TcPluginSolveResult(..), TcPluginRewriteResult(..)
+  , TcPluginRewriter, RewriteEnv
+  )
+import GHC.Tc.Types.Constraint
+  ( Ct(..), CanEqLHS(..)
+  , ctPred
+  )
+import GHC.Types.Name.Occurrence
+  ( mkTcOcc )
+import GHC.Types.Unique.FM
+  ( UniqFM, listToUFM )
+import GHC.Unit.Finder
+  ( FindResult(..) )
+import GHC.Unit.Module
+  ( Module
+  , mkModuleName
+  )
+
+--------------------------------------------------------------------------------
+
+-- In this test, we write a plugin which returns "TcPluginNoRewrite"
+-- for all the type families in RewritePerfDefs.
+--
+-- Comparing the result with T9872b gives an indication of the performance
+-- impact of rewriting plugins in code that heavily rewrites type families.
+
+type PluginDefs = [ TyCon ]
+
+definitionsModule :: TcPluginM Module
+definitionsModule = do
+  findResult <- findImportedModule ( mkModuleName "RewritePerfDefs" ) Nothing
+  case findResult of
+    Found _ res     -> pure res
+    FoundMultiple _ -> error $ "RewritePerfPlugin: found multiple modules named 'RewritePerfDefs'."
+    _               -> error $ "RewritePerfPlugin: could not find any module named 'RewritePerfDefs'."
+
+lookupDefs :: TcPluginM PluginDefs
+lookupDefs = do
+  defs <- definitionsModule
+  traverse ( \ tyConName -> lookupOrig defs ( mkTcOcc tyConName ) >>= tcLookupTyCon )
+    [ "And", "NE", "EQ", "All", "ListConcat", "AppendIf", "Apply"
+    , "Map", "MapAppend", "MapAppend2", "MapAppend3"
+    , "Iterate2", "Iterate3", "Iterate4"
+    , "Orientations", "Compatible", "Allowed"
+    , "MatchingOrientations", "AllowedCombinations"
+    , "Solutions"
+    ]
+
+plugin :: Plugin
+plugin =
+  defaultPlugin
+    { tcPlugin        = \ _args -> Just $ rewritingPlugin
+    , pluginRecompile = purePlugin
+    }
+
+rewritingPlugin :: TcPlugin
+rewritingPlugin =
+  TcPlugin
+    { tcPluginInit    = lookupDefs
+    , tcPluginSolve   = \ _ _ _ _ _ -> pure $ TcPluginOk [] []
+    , tcPluginRewrite = rewriter
+    , tcPluginStop    = \ _ -> pure ()
+    }
+
+rewriter :: PluginDefs -> UniqFM TyCon TcPluginRewriter
+rewriter tyCons =
+  listToUFM $ map ( , don'tRewrite ) tyCons
+
+don'tRewrite :: RewriteEnv -> [ Ct ] -> [ Type ] -> TcPluginM TcPluginRewriteResult
+don'tRewrite _ _ _ = pure TcPluginNoRewrite
diff --git a/testsuite/tests/tcplugins/RewritePlugin.hs b/testsuite/tests/tcplugins/RewritePlugin.hs
new file mode 100644
index 0000000000..c9a3d6fe91
--- /dev/null
+++ b/testsuite/tests/tcplugins/RewritePlugin.hs
@@ -0,0 +1,87 @@
+{-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE ViewPatterns #-}
+
+module RewritePlugin where
+-- Rewriting type family applications.
+
+-- base
+import Data.Maybe
+  ( catMaybes )
+
+-- ghc
+import GHC.Builtin.Types
+  ( unitTy )
+import GHC.Core
+  ( Expr(Coercion) )
+import GHC.Core.Coercion
+  ( Coercion, mkUnivCo )
+import GHC.Core.Predicate
+  ( EqRel(NomEq), Pred(EqPred)
+  , classifyPredType
+  )
+import GHC.Core.Reduction
+  ( Reduction(..) )
+import GHC.Core.TyCo.Rep
+  ( Type, UnivCoProvenance(PluginProv) )
+import GHC.Core.TyCon
+  ( TyCon )
+import GHC.Core.Type
+  ( eqType, mkTyConApp, splitTyConApp_maybe )
+import GHC.Plugins
+  ( Plugin )
+import GHC.Tc.Plugin
+  ( TcPluginM
+  , unsafeTcPluginTcM
+  )
+import GHC.Tc.Types
+  ( RewriteEnv
+  , TcPluginRewriter, TcPluginRewriteResult(..)
+  )
+import GHC.Tc.Types.Constraint
+  ( Ct(..), CanEqLHS(..)
+  , ctPred
+  )
+import GHC.Tc.Types.Evidence
+  ( EvTerm(EvExpr), Role(Nominal) )
+import GHC.Types.Unique.FM
+  ( UniqFM, listToUFM )
+
+-- common
+import Common
+  ( PluginDefs(..)
+  , mkPlugin, don'tSolve
+  )
+
+--------------------------------------------------------------------------------
+
+-- This plugin rewrites @Add a Zero@ to @a@ and @Add Zero a@ to @a@,
+-- by using the plugin rewriting functionality,
+-- and not the constraint solver plugin functionality.
+
+plugin :: Plugin
+plugin = mkPlugin don'tSolve rewriter
+
+rewriter :: [String]
+         -> PluginDefs
+         -> UniqFM TyCon TcPluginRewriter
+rewriter _args defs@( PluginDefs { add } ) =
+  listToUFM
+    [ ( add, rewriteAdd defs ) ]
+
+rewriteAdd :: PluginDefs -> RewriteEnv -> [ Ct ] -> [ Type ] -> TcPluginM TcPluginRewriteResult
+rewriteAdd ( PluginDefs { .. } ) _env givens args@[ arg1, arg2 ]
+  | Just ( tyCon, [] ) <- splitTyConApp_maybe arg1
+  , tyCon == zero
+  = pure $ TcPluginRewriteTo ( mkTyFamReduction add args arg2 ) []
+  | Just ( tyCon, [] ) <- splitTyConApp_maybe arg2
+  , tyCon == zero
+  = pure $ TcPluginRewriteTo ( mkTyFamReduction add args arg1 ) []
+rewriteAdd _ _ _ _ = pure TcPluginNoRewrite
+
+
+mkTyFamReduction :: TyCon -> [ Type ] -> Type -> Reduction
+mkTyFamReduction tyCon args res = Reduction co res
+  where
+    co :: Coercion
+    co = mkUnivCo ( PluginProv "RewritePlugin" ) Nominal
+           ( mkTyConApp tyCon args ) res
diff --git a/testsuite/tests/tcplugins/TcPlugin_Rewrite.hs b/testsuite/tests/tcplugins/TcPlugin_Rewrite.hs
new file mode 100644
index 0000000000..6df19b7b62
--- /dev/null
+++ b/testsuite/tests/tcplugins/TcPlugin_Rewrite.hs
@@ -0,0 +1,23 @@
+{-# OPTIONS_GHC -dcore-lint #-}
+{-# OPTIONS_GHC -fplugin RewritePlugin #-}
+
+{-# LANGUAGE Haskell2010 #-}
+{-# LANGUAGE DataKinds, ScopedTypeVariables, TypeFamilies #-}
+
+module TcPlugin_Rewrite where
+
+import Data.Kind
+  ( Type )
+
+import Definitions
+  ( Add, Nat(..) )
+
+
+foo :: forall (proxy :: Nat -> Type) (n :: Nat)
+    .  ( Add Zero n ~ n )
+    => proxy n -> ()
+foo _ = ()
+
+bar :: forall (proxy :: Nat -> Type) (n :: Nat)
+    .  proxy n -> ()
+bar n = foo n
diff --git a/testsuite/tests/tcplugins/TcPlugin_Rewrite.stderr b/testsuite/tests/tcplugins/TcPlugin_Rewrite.stderr
new file mode 100644
index 0000000000..5fd74e759e
--- /dev/null
+++ b/testsuite/tests/tcplugins/TcPlugin_Rewrite.stderr
@@ -0,0 +1 @@
+[4 of 4] Compiling TcPlugin_Rewrite ( TcPlugin_Rewrite.hs, TcPlugin_Rewrite.o )
diff --git a/testsuite/tests/tcplugins/TcPlugin_RewritePerf.hs b/testsuite/tests/tcplugins/TcPlugin_RewritePerf.hs
new file mode 100644
index 0000000000..00fe3bc558
--- /dev/null
+++ b/testsuite/tests/tcplugins/TcPlugin_RewritePerf.hs
@@ -0,0 +1,25 @@
+
+-- Testing performance of type-checking rewriting plugins.
+-- Test based on T9872b.
+
+{-# OPTIONS_GHC -dcore-lint #-}
+{-# OPTIONS_GHC -freduction-depth=400 #-}
+{-# OPTIONS_GHC -fplugin RewritePerfPlugin #-}
+
+{-# LANGUAGE DataKinds, KindSignatures, PolyKinds #-}
+{-# LANGUAGE TypeOperators #-}
+
+module Main where
+
+import RewritePerfDefs
+
+data Proxy (a :: k) = Proxy
+
+type Cube1 = 'Cube B G W G B R
+type Cube2 = 'Cube W G B W R R
+type Cube3 = 'Cube G W R B R R
+type Cube4 = 'Cube B R G G W W
+
+type Cubes = [Cube1, Cube2, Cube3, Cube4]
+
+main = print (Proxy :: Proxy (Solutions Cubes))
diff --git a/testsuite/tests/tcplugins/TcPlugin_RewritePerf.stderr b/testsuite/tests/tcplugins/TcPlugin_RewritePerf.stderr
new file mode 100644
index 0000000000..3d4801cc51
--- /dev/null
+++ b/testsuite/tests/tcplugins/TcPlugin_RewritePerf.stderr
@@ -0,0 +1,25 @@
+[3 of 3] Compiling Main             ( TcPlugin_RewritePerf.hs, TcPlugin_RewritePerf.o )
+
+TcPlugin_RewritePerf.hs:25:8: error:
+    • No instance for (Show
+                         (Proxy
+                            '[ '[ 'Cube 'G 'B 'W 'R 'B 'G, 'Cube 'W 'G 'B 'W 'R 'R,
+                                  'Cube 'R 'W 'R 'B 'G 'R, 'Cube 'B 'R 'G 'G 'W 'W],
+                               '[ 'Cube 'G 'B 'R 'W 'B 'G, 'Cube 'R 'R 'W 'B 'G 'W,
+                                  'Cube 'R 'G 'B 'R 'W 'R, 'Cube 'W 'W 'G 'G 'R 'B],
+                               '[ 'Cube 'G 'W 'R 'B 'B 'G, 'Cube 'W 'B 'W 'R 'G 'R,
+                                  'Cube 'R 'R 'B 'G 'W 'R, 'Cube 'B 'G 'G 'W 'R 'W],
+                               '[ 'Cube 'G 'R 'W 'B 'B 'G, 'Cube 'R 'W 'B 'G 'R 'W,
+                                  'Cube 'R 'B 'R 'W 'G 'R, 'Cube 'W 'G 'G 'R 'W 'B],
+                               '[ 'Cube 'G 'R 'B 'B 'W 'G, 'Cube 'W 'W 'R 'G 'B 'R,
+                                  'Cube 'R 'B 'G 'W 'R 'R, 'Cube 'B 'G 'W 'R 'G 'W],
+                               '[ 'Cube 'G 'W 'B 'B 'R 'G, 'Cube 'R 'B 'G 'R 'W 'W,
+                                  'Cube 'R 'R 'W 'G 'B 'R, 'Cube 'W 'G 'R 'W 'G 'B],
+                               '[ 'Cube 'G 'B 'B 'W 'R 'G, 'Cube 'W 'R 'G 'B 'W 'R,
+                                  'Cube 'R 'G 'W 'R 'B 'R, 'Cube 'B 'W 'R 'G 'G 'W],
+                               '[ 'Cube 'G 'B 'B 'R 'W 'G, 'Cube 'R 'G 'R 'W 'B 'W,
+                                  'Cube 'R 'W 'G 'B 'R 'R, 'Cube 'W 'R 'W 'G 'G 'B]]))
+        arising from a use of ‘print’
+    • In the expression: print (Proxy :: Proxy (Solutions Cubes))
+      In an equation for ‘main’:
+          main = print (Proxy :: Proxy (Solutions Cubes))
diff --git a/testsuite/tests/tcplugins/TyFamPlugin.hs b/testsuite/tests/tcplugins/TyFamPlugin.hs
index 523bdc10c1..1ae0390df0 100644
--- a/testsuite/tests/tcplugins/TyFamPlugin.hs
+++ b/testsuite/tests/tcplugins/TyFamPlugin.hs
@@ -30,18 +30,18 @@ import GHC.Tc.Plugin
   , unsafeTcPluginTcM
   )
 import GHC.Tc.Types
-  ( TcPluginResult(..) )
+  ( TcPluginSolveResult(..) )
 import GHC.Tc.Types.Constraint
   ( Ct(..), CanEqLHS(..)
   , ctPred
   )
 import GHC.Tc.Types.Evidence
-  ( EvTerm(EvExpr), Role(Nominal) )
+  ( EvBindsVar, EvTerm(EvExpr), Role(Nominal) )
 
 -- common
 import Common
   ( PluginDefs(..)
-  , mkPlugin
+  , mkPlugin, don'tRewrite
   )
 
 --------------------------------------------------------------------------------
@@ -57,12 +57,12 @@ import Common
 -- with Plugin provenance to prove the equality constraint.
 
 plugin :: Plugin
-plugin = mkPlugin solver
+plugin = mkPlugin solver don'tRewrite
 
 solver :: [String]
-       -> PluginDefs -> [Ct] -> [Ct] -> [Ct]
-       -> TcPluginM TcPluginResult
-solver _args defs _gs _ds ws = do
+       -> PluginDefs -> EvBindsVar -> [Ct] -> [Ct] -> [Ct]
+       -> TcPluginM TcPluginSolveResult
+solver _args defs _ev _gs _ds ws = do
   solved <- catMaybes <$> traverse ( solveCt defs ) ws
   pure $ TcPluginOk solved []
 
diff --git a/testsuite/tests/tcplugins/all.T b/testsuite/tests/tcplugins/all.T
index 1fe0727e0d..8af9ceefa8 100644
--- a/testsuite/tests/tcplugins/all.T
+++ b/testsuite/tests/tcplugins/all.T
@@ -52,3 +52,40 @@ test('TcPlugin_TyFam'
         ]
       ,'-dynamic -package ghc' if have_dynamic() else '-package ghc']
     )
+
+# See RewritePlugin.hs for a description of this plugin.
+test('TcPlugin_Rewrite'
+    , [ extra_files(
+        [ 'Definitions.hs'
+        , 'Common.hs'
+        , 'RewritePlugin.hs'
+        , 'TcPlugin_Rewrite.hs'
+        ])
+      ]
+    , multi_compile
+    , [ 'TcPlugin_Rewrite.hs'
+      , [ ('Definitions.hs', '')
+        , ('Common.hs', '')
+        , ('RewritePlugin.hs', '')
+        ]
+      ,'-dynamic -package ghc' if have_dynamic() else '-package ghc']
+    )
+
+# See RewritePerfPlugin.hs for a description of this plugin.
+test('TcPlugin_RewritePerf'
+    , [ extra_files(
+        [ 'RewritePerfDefs.hs'
+        , 'RewritePerfPlugin.hs'
+        , 'TcPlugin_RewritePerf.hs'
+        ])
+      , only_ways(['normal'])
+      , collect_compiler_stats('bytes allocated', 1)
+      , high_memory_usage
+      ]
+    , multi_compile_fail
+    , [ 'TcPlugin_RewritePerf.hs'
+      , [ ('RewritePerfDefs.hs', '')
+        , ('RewritePerfPlugin.hs', '')
+        ]
+      ,'-dynamic -package ghc' if have_dynamic() else '-package ghc']
+    )
diff --git a/testsuite/tests/typecheck/should_compile/T11462_Plugin.hs b/testsuite/tests/typecheck/should_compile/T11462_Plugin.hs
index 2f0297cf2d..fc6b3348fa 100644
--- a/testsuite/tests/typecheck/should_compile/T11462_Plugin.hs
+++ b/testsuite/tests/typecheck/should_compile/T11462_Plugin.hs
@@ -1,14 +1,16 @@
 module T11462_Plugin(plugin) where
 
-import GHC.Tc.Utils.Monad ( TcPlugin(..), TcPluginResult(..) )
+import GHC.Tc.Utils.Monad ( TcPlugin(..), TcPluginSolveResult(..), TcPluginRewriteResult(..) )
 import GHC.Driver.Plugins ( defaultPlugin, Plugin(..), CommandLineOption )
+import GHC.Types.Unique.FM ( emptyUFM )
 
 plugin :: Plugin
 plugin = defaultPlugin { tcPlugin = Just . thePlugin }
 
 thePlugin :: [CommandLineOption] -> TcPlugin
 thePlugin opts = TcPlugin
-  { tcPluginInit  = return ()
-  , tcPluginSolve = \_ _ _ _ -> return $ TcPluginOk [] []
-  , tcPluginStop  = \_ -> return ()
+  { tcPluginInit    = return ()
+  , tcPluginSolve   = \_ _ _ _ _ -> return $ TcPluginOk [] []
+  , tcPluginRewrite = \_ -> emptyUFM
+  , tcPluginStop    = \_ -> return ()
   }
diff --git a/testsuite/tests/typecheck/should_compile/T11525_Plugin.hs b/testsuite/tests/typecheck/should_compile/T11525_Plugin.hs
index 206c3c2a8f..5aedad2a6b 100644
--- a/testsuite/tests/typecheck/should_compile/T11525_Plugin.hs
+++ b/testsuite/tests/typecheck/should_compile/T11525_Plugin.hs
@@ -1,14 +1,16 @@
 module T11525_Plugin(plugin) where
 
-import GHC.Tc.Utils.Monad ( TcPlugin(..), TcPluginResult(..) )
+import GHC.Tc.Utils.Monad ( TcPlugin(..), TcPluginSolveResult(..), TcPluginRewriteResult(..) )
 import GHC.Driver.Plugins ( defaultPlugin, Plugin(..), CommandLineOption )
+import GHC.Types.Unique.FM ( emptyUFM )
 
 plugin :: Plugin
 plugin = defaultPlugin { tcPlugin = Just . thePlugin }
 
 thePlugin :: [CommandLineOption] -> TcPlugin
 thePlugin opts = TcPlugin
-  { tcPluginInit  = return ()
-  , tcPluginSolve = \_ _ _ _ -> return $ TcPluginOk [] []
-  , tcPluginStop  = \_ -> return ()
+  { tcPluginInit    = return ()
+  , tcPluginSolve   = \_ _ _ _ _ -> return $ TcPluginOk [] []
+  , tcPluginRewrite = \_ -> emptyUFM
+  , tcPluginStop    = \_ -> return ()
   }