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.

8 files changed, 297 insertions, 135 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)