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.

12 files changed, 442 insertions, 30 deletions

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']
+    )