diff --git a/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal b/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal
index d500dde464..edab1a8ceb 100644
--- a/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal
+++ b/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal
@@ -87,7 +87,7 @@ library
     , mtl
     , parser-combinators
     , prettyprinter
-    , refinery              ^>=0.3
+    , refinery              ^>=0.4
     , retrie                >=0.1.1.0
     , syb
     , text
diff --git a/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs b/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs
index 478f5e41c0..ab3e266abd 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs
@@ -59,7 +59,7 @@ destructMatches use_field_puns f scrut t jdg = do
   let hy = jEntireHypothesis jdg
       g  = jGoal jdg
   case tacticsGetDataCons $ unCType t of
-    Nothing -> throwError $ GoalMismatch "destruct" g
+    Nothing -> cut -- throwError $ GoalMismatch "destruct" g
     Just (dcs, apps) ->
       fmap unzipTrace $ for dcs $ \dc -> do
         let con = RealDataCon dc
@@ -214,7 +214,7 @@ patSynExTys ps = patSynExTyVars ps
 
 destruct' :: Bool -> (ConLike -> Judgement -> Rule) -> HyInfo CType -> Judgement -> Rule
 destruct' use_field_puns f hi jdg = do
-  when (isDestructBlacklisted jdg) $ throwError NoApplicableTactic
+  when (isDestructBlacklisted jdg) $ cut -- throwError NoApplicableTactic
   let term = hi_name hi
   ext
       <- destructMatches
@@ -234,13 +234,13 @@ destruct' use_field_puns f hi jdg = do
 -- resulting matches.
 destructLambdaCase' :: Bool -> (ConLike -> Judgement -> Rule) -> Judgement -> Rule
 destructLambdaCase' use_field_puns f jdg = do
-  when (isDestructBlacklisted jdg) $ throwError NoApplicableTactic
+  when (isDestructBlacklisted jdg) $ cut -- throwError NoApplicableTactic
   let g  = jGoal jdg
   case splitFunTy_maybe (unCType g) of
     Just (arg, _) | isAlgType arg ->
       fmap (fmap noLoc lambdaCase) <$>
         destructMatches use_field_puns f Nothing (CType arg) jdg
-    _ -> throwError $ GoalMismatch "destructLambdaCase'" g
+    _ -> cut -- throwError $ GoalMismatch "destructLambdaCase'" g
 
 
 ------------------------------------------------------------------------------
@@ -267,7 +267,7 @@ buildDataCon should_blacklist jdg dc tyapps = do
       --
       -- Fortunately, this isn't an issue in practice, since 'PatSyn's are
       -- never in the hypothesis.
-      throwError $ TacticPanic "Can't build Pattern constructors yet"
+      cut -- throwError $ TacticPanic "Can't build Pattern constructors yet"
   ext
       <- fmap unzipTrace
        $ traverse ( \(arg, n) ->
diff --git a/plugins/hls-tactics-plugin/src/Wingman/KnownStrategies.hs b/plugins/hls-tactics-plugin/src/Wingman/KnownStrategies.hs
index 72511b0433..5158ce4fc8 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/KnownStrategies.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/KnownStrategies.hs
@@ -1,6 +1,5 @@
 module Wingman.KnownStrategies where
 
-import Control.Monad.Error.Class
 import Data.Foldable (for_)
 import OccName (mkVarOcc, mkClsOcc)
 import Refinery.Tactic
@@ -26,7 +25,7 @@ known name t = do
   getCurrentDefinitions >>= \case
     [(def, _)] | def == mkVarOcc name ->
       tracing ("known " <> name) t
-    _ -> throwError NoApplicableTactic
+    _ -> failure NoApplicableTactic
 
 
 deriveFmap :: TacticsM ()
diff --git a/plugins/hls-tactics-plugin/src/Wingman/KnownStrategies/QuickCheck.hs b/plugins/hls-tactics-plugin/src/Wingman/KnownStrategies/QuickCheck.hs
index c2383c0fbf..f6013af5af 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/KnownStrategies/QuickCheck.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/KnownStrategies/QuickCheck.hs
@@ -1,7 +1,6 @@
 module Wingman.KnownStrategies.QuickCheck where
 
 import ConLike (ConLike(RealDataCon))
-import Control.Monad.Except (MonadError (throwError))
 import Data.Bool (bool)
 import Data.Generics (everything, mkQ)
 import Data.List (partition)
@@ -15,7 +14,7 @@ import GHC.SourceGen.Expr (case', lambda, let')
 import GHC.SourceGen.Overloaded (App ((@@)), HasList (list))
 import GHC.SourceGen.Pat (conP)
 import OccName (HasOccName (occName), mkVarOcc, occNameString)
-import Refinery.Tactic (goal, rule)
+import Refinery.Tactic (goal, rule, failure)
 import TyCon (TyCon, tyConDataCons, tyConName)
 import Type (splitTyConApp_maybe)
 import Wingman.CodeGen
@@ -61,7 +60,7 @@ deriveArbitrary = do
                             (list $ fmap genExpr big)
                             terminal_expr
                     ]
-    _ -> throwError $ GoalMismatch "deriveArbitrary" ty
+    _ -> failure $ GoalMismatch "deriveArbitrary" ty
 
 
 ------------------------------------------------------------------------------
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs b/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs
index 2f9c4bbb18..499a1b48bc 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs
@@ -5,13 +5,11 @@ module Wingman.Machinery where
 
 import           Control.Applicative (empty)
 import           Control.Lens ((<>~))
-import           Control.Monad.Error.Class
 import           Control.Monad.Reader
 import           Control.Monad.State.Class (gets, modify, MonadState)
 import           Control.Monad.State.Strict (StateT (..), execStateT)
 import           Control.Monad.Trans.Maybe
 import           Data.Coerce
-import           Data.Either
 import           Data.Foldable
 import           Data.Functor ((<&>))
 import           Data.Generics (everything, gcount, mkQ)
@@ -96,20 +94,20 @@ runTactic ctx jdg t = do
     res <- flip runReaderT ctx
          . unExtractM
          $ runTacticT t jdg tacticState
-    pure $ case partitionEithers res of
-      (errs, []) -> Left $ take 50 errs
-      (_, fmap assoc23 -> solns) -> do
+    pure $ case res of
+      (Left errs) -> Left $ take 50 errs
+      (Right solns) -> do
         let sorted =
-              flip sortBy solns $ comparing $ \(ext, (_, holes)) ->
-                Down $ scoreSolution ext jdg holes
+              flip sortBy solns $ comparing $ \(Proof ext _ holes) ->
+                Down $ scoreSolution ext jdg $ fmap snd holes
         case sorted of
-          ((syn, (_, subgoals)) : _) ->
+          ((Proof syn _ subgoals) : _) ->
             Right $
               RunTacticResults
                 { rtr_trace    = syn_trace syn
                 , rtr_extract  = simplify $ syn_val syn
-                , rtr_subgoals = subgoals
-                , rtr_other_solns = reverse . fmap fst $ sorted
+                , rtr_subgoals = fmap snd subgoals
+                , rtr_other_solns = reverse . fmap pf_extract $ sorted
                 , rtr_jdg = jdg
                 , rtr_ctx = ctx
                 }
@@ -154,7 +152,7 @@ mappingExtract
     -> TacticT jdg ext err s m a
 mappingExtract f (TacticT m)
   = TacticT $ StateT $ \jdg ->
-      mapExtract' f $ runStateT m jdg
+      mapExtract id f $ runStateT m jdg
 
 
 ------------------------------------------------------------------------------
@@ -227,7 +225,10 @@ unify goal inst = do
   case tryUnifyUnivarsButNotSkolems skolems goal inst of
     Just subst ->
       modify $ updateSubst subst
-    Nothing -> throwError (UnificationError inst goal)
+    Nothing -> cut -- failure (UnificationError inst goal)
+
+cut :: RuleT jdg ext err s m a
+cut = RuleT Empty
 
 
 ------------------------------------------------------------------------------
@@ -254,26 +255,6 @@ attemptWhen _  t2 False = t2
 attemptWhen t1 t2 True  = commit t1 t2
 
 
-------------------------------------------------------------------------------
--- | Mystical time-traveling combinator for inspecting the extracts produced by
--- a tactic. We can use it to guard that extracts match certain predicates, for
--- example.
---
--- Note, that this thing is WEIRD. To illustrate:
---
--- @@
--- peek f
--- blah
--- @@
---
--- Here, @f@ can inspect the extract _produced by @blah@,_  which means the
--- causality appears to go backwards.
---
--- 'peek' should be exposed directly by @refinery@ in the next release.
-peek :: (ext -> TacticT jdg ext err s m ()) -> TacticT jdg ext err s m ()
-peek k = tactic $ \j -> Subgoal ((), j) $ \e -> proofState (k e) j
-
-
 ------------------------------------------------------------------------------
 -- | Run the given tactic iff the current hole contains no univars. Skolems and
 -- already decided univars are OK though.
@@ -284,7 +265,7 @@ requireConcreteHole m = do
   let vars = S.fromList $ tyCoVarsOfTypeWellScoped $ unCType $ jGoal jdg
   case S.size $ vars S.\\ skolems of
     0 -> m
-    _ -> throwError TooPolymorphic
+    _ -> failure TooPolymorphic
 
 
 ------------------------------------------------------------------------------
@@ -317,7 +298,7 @@ useNameFromHypothesis f name = do
   hy <- jHypothesis <$> goal
   case M.lookup name $ hyByName hy of
     Just hi -> f hi
-    Nothing -> throwError $ NotInScope name
+    Nothing -> failure $ NotInScope name
 
 ------------------------------------------------------------------------------
 -- | Lift a function over 'HyInfo's to one that takes an 'OccName' and tries to
@@ -326,7 +307,7 @@ useNameFromContext :: (HyInfo CType -> TacticsM a) -> OccName -> TacticsM a
 useNameFromContext f name = do
   lookupNameInContext name >>= \case
     Just ty -> f $ createImportedHyInfo name ty
-    Nothing -> throwError $ NotInScope name
+    Nothing -> failure $ NotInScope name
 
 
 ------------------------------------------------------------------------------
@@ -340,12 +321,11 @@ lookupNameInContext name = do
 
 
 getDefiningType
-    :: (MonadError TacticError m, MonadReader Context m)
-    => m CType
+    :: TacticsM CType
 getDefiningType = do
   calling_fun_name <- fst . head <$> asks ctxDefiningFuncs
   maybe
-    (throwError $ NotInScope calling_fun_name)
+    (failure $ NotInScope calling_fun_name)
     pure
       =<< lookupNameInContext calling_fun_name
 
@@ -403,7 +383,7 @@ getOccNameType
 getOccNameType occ = do
   getTyThing occ >>= \case
     Just (AnId v) -> pure $ varType v
-    _ -> throwError $ NotInScope occ
+    _ -> failure $ NotInScope occ
 
 
 getCurrentDefinitions :: TacticsM [(OccName, CType)]
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
index 44b2a535c6..66ef902f2e 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
@@ -7,10 +7,12 @@
 module Wingman.Metaprogramming.Parser where
 
 import qualified Control.Monad.Combinators.Expr as P
-import qualified Control.Monad.Error.Class as E
 import           Data.Functor
 import           Data.Maybe (listToMaybe)
 import qualified Data.Text as T
+import           Development.IDE.GHC.Compat (RealSrcLoc, srcLocLine, srcLocCol, srcLocFile)
+import           FastString (unpackFS)
+import           Refinery.Tactic (failure)
 import qualified Refinery.Tactic as R
 import qualified Text.Megaparsec as P
 import           Wingman.Auto
@@ -20,8 +22,6 @@ import           Wingman.Metaprogramming.Parser.Documentation
 import           Wingman.Metaprogramming.ProofState (proofState, layout)
 import           Wingman.Tactics
 import           Wingman.Types
-import Development.IDE.GHC.Compat (RealSrcLoc, srcLocLine, srcLocCol, srcLocFile)
-import FastString (unpackFS)
 
 
 nullary :: T.Text -> TacticsM () -> Parser (TacticsM ())
@@ -296,7 +296,7 @@ commands =
       ( pure $
           fmap listToMaybe getCurrentDefinitions >>= \case
             Just (self, _) -> useNameFromContext (apply Saturated) self
-            Nothing -> E.throwError $ TacticPanic "no defining function"
+            Nothing -> failure $ TacticPanic "no defining function"
       )
       [ Example
           (Just "In the context of `foo (a :: Int) (b :: b) = _`:")
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs
index a78d0c4f05..c582b2c729 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs
@@ -10,7 +10,6 @@ import           Control.Applicative (Alternative(empty))
 import           Control.Lens ((&), (%~), (<>~))
 import           Control.Monad (filterM)
 import           Control.Monad (unless)
-import           Control.Monad.Except (throwError)
 import           Control.Monad.Extra (anyM)
 import           Control.Monad.Reader.Class (MonadReader (ask))
 import           Control.Monad.State.Strict (StateT(..), runStateT)
@@ -66,7 +65,7 @@ assume name = rule $ \jdg -> do
           { syn_trace = tracePrim $ "assume " <> occNameString name
           , syn_used_vals = S.singleton name
           }
-    Nothing -> throwError $ UndefinedHypothesis name
+    Nothing -> cut -- failure $ UndefinedHypothesis name
 
 
 ------------------------------------------------------------------------------
@@ -87,19 +86,22 @@ recursion :: TacticsM ()
 recursion = requireConcreteHole $ tracing "recursion" $ do
   defs <- getCurrentDefinitions
   attemptOn (const defs) $ \(name, ty) -> markRecursion $ do
+    jdg <- goal
     -- Peek allows us to look at the extract produced by this block.
-    peek $ \ext -> do
-      jdg <- goal
-      let pat_vals = jPatHypothesis jdg
-      -- Make sure that the recursive call contains at least one already-bound
-      -- pattern value. This ensures it is structurally smaller, and thus
-      -- suggests termination.
-      unless (any (flip M.member pat_vals) $ syn_used_vals ext) empty
-
-    let hy' = recursiveHypothesis defs
-    ctx <- ask
-    localTactic (apply Saturated $ HyInfo name RecursivePrv ty) (introduce ctx hy')
-      <@> fmap (localTactic assumption . filterPosition name) [0..]
+    peek
+      ( do
+          let hy' = recursiveHypothesis defs
+          ctx <- ask
+          localTactic (apply Saturated $ HyInfo name RecursivePrv ty) (introduce ctx hy')
+            <@> fmap (localTactic assumption . filterPosition name) [0..]
+      ) $ \ext -> do
+        let pat_vals = jPatHypothesis jdg
+        -- Make sure that the recursive call contains at least one already-bound
+        -- pattern value. This ensures it is structurally smaller, and thus
+        -- suggests termination.
+        case (any (flip M.member pat_vals) $ syn_used_vals ext) of
+          True -> Nothing
+          False -> Just UnhelpfulRecursion
 
 
 restrictPositionForApplication :: TacticsM () -> TacticsM () -> TacticsM ()
@@ -126,7 +128,7 @@ intros'
 intros' names = rule $ \jdg -> do
   let g  = jGoal jdg
   case tacticsSplitFunTy $ unCType g of
-    (_, _, [], _) -> throwError $ GoalMismatch "intros" g
+    (_, _, [], _) -> cut -- failure $ GoalMismatch "intros" g
     (_, _, args, res) -> do
       ctx <- ask
       let occs = fromMaybe (mkManyGoodNames (hyNamesInScope $ jEntireHypothesis jdg) args) names
@@ -209,8 +211,8 @@ homo hi = requireConcreteHole . tracing "homo" $ do
   case (uncoveredDataCons (coerce $ hi_type hi) (coerce g)) of
     Just uncovered_dcs ->
       unless (S.null uncovered_dcs) $
-        throwError  $ TacticPanic "Can't cover every datacon in domain"
-    _ -> throwError $ TacticPanic "Unable to fetch datacons"
+        failure  $ TacticPanic "Can't cover every datacon in domain"
+    _ -> failure $ TacticPanic "Unable to fetch datacons"
 
   rule
     $ destruct'
@@ -281,7 +283,7 @@ split = tracing "split(user)" $ do
   jdg <- goal
   let g = jGoal jdg
   case tacticsGetDataCons $ unCType g of
-    Nothing -> throwError $ GoalMismatch "split" g
+    Nothing -> failure $ GoalMismatch "split" g
     Just (dcs, _) -> choice $ fmap splitDataCon dcs
 
 
@@ -294,7 +296,7 @@ splitAuto = requireConcreteHole $ tracing "split(auto)" $ do
   jdg <- goal
   let g = jGoal jdg
   case tacticsGetDataCons $ unCType g of
-    Nothing -> throwError $ GoalMismatch "split" g
+    Nothing -> failure $ GoalMismatch "split" g
     Just (dcs, _) -> do
       case isSplitWhitelisted jdg of
         True -> choice $ fmap splitDataCon dcs
@@ -313,7 +315,7 @@ splitSingle = tracing "splitSingle" $ do
   case tacticsGetDataCons $ unCType g of
     Just ([dc], _) -> do
       splitDataCon dc
-    _ -> throwError $ GoalMismatch "splitSingle" g
+    _ -> failure $ GoalMismatch "splitSingle" g
 
 ------------------------------------------------------------------------------
 -- | Like 'split', but prunes any data constructors which have holes.
@@ -358,7 +360,7 @@ splitConLike dc =
     case splitTyConApp_maybe $ unCType g of
       Just (_, apps) -> do
         buildDataCon True (unwhitelistingSplit jdg) dc apps
-      Nothing -> throwError $ GoalMismatch "splitDataCon" g
+      Nothing -> cut -- failure $ GoalMismatch "splitDataCon" g
 
 ------------------------------------------------------------------------------
 -- | Attempt to instantiate the given data constructor to solve the goal.
@@ -404,8 +406,8 @@ userSplit occ = do
       case find (sloppyEqOccName occ . occName . dataConName)
              $ tyConDataCons tc of
         Just dc -> splitDataCon dc
-        Nothing -> throwError $ NotInScope occ
-    Nothing -> throwError $ NotInScope occ
+        Nothing -> failure $ NotInScope occ
+    Nothing -> failure $ NotInScope occ
 
 
 ------------------------------------------------------------------------------
@@ -430,7 +432,7 @@ refine = intros <%> splitSingle
 
 
 auto' :: Int -> TacticsM ()
-auto' 0 = throwError NoProgress
+auto' 0 = failure NoProgress
 auto' n = do
   let loop = auto' (n - 1)
   try intros
@@ -468,7 +470,7 @@ applyMethod cls df method_name = do
       let (_, apps) = splitAppTys df
       let ty = piResultTys (idType method) apps
       apply Saturated $ HyInfo method_name (ClassMethodPrv $ Uniquely cls) $ CType ty
-    Nothing -> throwError $ NotInScope method_name
+    Nothing -> failure $ NotInScope method_name
 
 
 applyByName :: OccName -> TacticsM ()
@@ -520,7 +522,7 @@ self :: TacticsM ()
 self =
   fmap listToMaybe getCurrentDefinitions >>= \case
     Just (self, _) -> useNameFromContext (apply Saturated) self
-    Nothing -> throwError $ TacticPanic "no defining function"
+    Nothing -> failure $ TacticPanic "no defining function"
 
 
 ------------------------------------------------------------------------------
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Types.hs b/plugins/hls-tactics-plugin/src/Wingman/Types.hs
index aa2595e119..d15893f3b1 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Types.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Types.hs
@@ -1,5 +1,6 @@
-{-# LANGUAGE OverloadedStrings #-}
-{-# LANGUAGE RecordWildCards   #-}
+{-# LANGUAGE OverloadedStrings    #-}
+{-# LANGUAGE RecordWildCards      #-}
+{-# LANGUAGE UndecidableInstances #-}
 
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 
@@ -17,8 +18,11 @@ import           ConLike (ConLike)
 import           Control.Lens hiding (Context)
 import           Control.Monad.Reader
 import           Control.Monad.State
+import qualified Control.Monad.State.Strict as Strict
 import           Data.Coerce
 import           Data.Function
+import           Data.Generics (mkM, everywhereM, Data, Typeable)
+import           Data.Generics.Labels ()
 import           Data.Generics.Product (field)
 import           Data.List.NonEmpty (NonEmpty (..))
 import           Data.Semigroup
@@ -31,17 +35,21 @@ import           Development.IDE.Core.UseStale
 import           Development.IDE.GHC.Compat hiding (Node)
 import           Development.IDE.GHC.Orphans ()
 import           FamInstEnv (FamInstEnvs)
+import           GHC.Exts (fromString)
 import           GHC.Generics
 import           GHC.SourceGen (var)
-import           GhcPlugins (GlobalRdrElt)
+import           GhcPlugins (GlobalRdrElt, mkRdrUnqual)
 import           InstEnv (InstEnvs(..))
 import           OccName
+import           Refinery.ProofState
 import           Refinery.Tactic
+import           Refinery.Tactic.Internal (TacticT(TacticT), RuleT (RuleT))
 import           System.IO.Unsafe (unsafePerformIO)
 import           Type (TCvSubst, Var, eqType, nonDetCmpType, emptyTCvSubst)
 import           UniqSupply (takeUniqFromSupply, mkSplitUniqSupply, UniqSupply)
-import           Unique (nonDetCmpUnique, Uniquable, getUnique, Unique)
+import           Unique (nonDetCmpUnique, Uniquable, getUnique, Unique, mkUnique)
 import           Wingman.Debug
+import Data.IORef
 
 
 ------------------------------------------------------------------------------
@@ -102,6 +110,7 @@ emptyConfig = Config
 ------------------------------------------------------------------------------
 -- | A wrapper around 'Type' which supports equality and ordering.
 newtype CType = CType { unCType :: Type }
+  deriving stock (Data, Typeable)
 
 instance Eq CType where
   (==) = eqType `on` unCType
@@ -176,7 +185,7 @@ instance Show UniqSupply where
 -- | A 'UniqSupply' to use in 'defaultTacticState'
 unsafeDefaultUniqueSupply :: UniqSupply
 unsafeDefaultUniqueSupply =
-  unsafePerformIO $ mkSplitUniqSupply '🚒'
+  unsafePerformIO $ mkSplitUniqSupply 'w'
 {-# NOINLINE unsafeDefaultUniqueSupply #-}
 
 
@@ -225,7 +234,7 @@ data Provenance
     -- to keep these in the hypothesis set, rather than filtering it, in order
     -- to continue tracking downstream provenance.
   | DisallowedPrv DisallowReason Provenance
-  deriving stock (Eq, Show, Generic, Ord)
+  deriving stock (Eq, Show, Generic, Ord, Data, Typeable)
 
 
 ------------------------------------------------------------------------------
@@ -235,7 +244,7 @@ data DisallowReason
   | Shadowed
   | RecursiveCall
   | AlreadyDestructed
-  deriving stock (Eq, Show, Generic, Ord)
+  deriving stock (Eq, Show, Generic, Ord, Data, Typeable)
 
 
 ------------------------------------------------------------------------------
@@ -251,7 +260,7 @@ data PatVal = PatVal
     -- ^ The datacon which introduced this term.
   , pv_position  :: Int
     -- ^ The position of this binding in the datacon's arguments.
-  } deriving stock (Eq, Show, Generic, Ord)
+  } deriving stock (Eq, Show, Generic, Ord, Data, Typeable)
 
 
 ------------------------------------------------------------------------------
@@ -259,6 +268,7 @@ data PatVal = PatVal
 -- instances.
 newtype Uniquely a = Uniquely { getViaUnique :: a }
   deriving Show via a
+  deriving stock (Data, Typeable)
 
 instance Uniquable a => Eq (Uniquely a) where
   (==) = (==) `on` getUnique . getViaUnique
@@ -274,7 +284,7 @@ instance Uniquable a => Ord (Uniquely a) where
 newtype Hypothesis a = Hypothesis
   { unHypothesis :: [HyInfo a]
   }
-  deriving stock (Functor, Eq, Show, Generic, Ord)
+  deriving stock (Functor, Eq, Show, Generic, Ord, Data, Typeable)
   deriving newtype (Semigroup, Monoid)
 
 
@@ -285,7 +295,7 @@ data HyInfo a = HyInfo
   , hi_provenance :: Provenance
   , hi_type       :: a
   }
-  deriving stock (Functor, Eq, Show, Generic, Ord)
+  deriving stock (Functor, Eq, Show, Generic, Ord, Data, Typeable)
 
 
 ------------------------------------------------------------------------------
@@ -313,9 +323,42 @@ newtype ExtractM a = ExtractM { unExtractM :: ReaderT Context IO a }
     deriving newtype (Functor, Applicative, Monad, MonadReader Context)
 
 ------------------------------------------------------------------------------
--- | Orphan instance for producing holes when attempting to solve tactics.
-instance MonadExtract (Synthesized (LHsExpr GhcPs)) ExtractM where
-  hole = pure . pure . noLoc $ var "_"
+-- | Used to ensure hole names are unique across invocations of runTactic
+globalHoleRef :: IORef Int
+globalHoleRef = unsafePerformIO $ newIORef 10
+{-# NOINLINE globalHoleRef #-}
+
+instance MonadExtract Int (Synthesized (LHsExpr GhcPs)) TacticError TacticState ExtractM where
+  hole = do
+    u <- lift $ ExtractM $ lift $
+          readIORef globalHoleRef <* modifyIORef' globalHoleRef (+ 1)
+    pure
+      ( u
+      , pure . noLoc $ var $ fromString $ occNameString $ occName $ mkMetaHoleName u
+      )
+
+  unsolvableHole _ = hole
+
+
+instance MonadReader r m => MonadReader r (TacticT jdg ext err s m) where
+  ask = TacticT $ lift $ Effect $ fmap pure ask
+  local f (TacticT m) = TacticT $ Strict.StateT $ \jdg ->
+    Effect $ local f $ pure $ Strict.runStateT m jdg
+
+instance MonadReader r m => MonadReader r (RuleT jdg ext err s m) where
+  ask = RuleT $ Effect $ fmap Axiom ask
+  local f (RuleT m) = RuleT $ Effect $ local f $ pure m
+
+mkMetaHoleName :: Int -> RdrName
+mkMetaHoleName u = mkRdrUnqual $ mkVarOcc $ "_" <> show (mkUnique 'w' u)
+
+instance MetaSubst Int (Synthesized (LHsExpr GhcPs)) where
+  -- TODO(sandy): This join is to combine the synthesizeds
+  substMeta u val a =  join $ a <&>
+    everywhereM (mkM $ \case
+      (L _ (HsVar _ (L _ name)))
+        | name == mkMetaHoleName u -> val
+      (t :: LHsExpr GhcPs) -> pure t)
 
 
 ------------------------------------------------------------------------------
@@ -329,6 +372,7 @@ data TacticError
   | NoApplicableTactic
   | IncorrectDataCon DataCon
   | RecursionOnWrongParam OccName Int OccName
+  | UnhelpfulRecursion
   | UnhelpfulDestruct OccName
   | UnhelpfulSplit OccName
   | TooPolymorphic
@@ -363,6 +407,8 @@ instance Show TacticError where
     show (RecursionOnWrongParam call p arg) =
       "Recursion on wrong param (" <> show call <> ") on arg"
         <> show p <> ": " <> show arg
+    show UnhelpfulRecursion =
+      "Recursion wasn't productive"
     show (UnhelpfulDestruct n) =
       "Destructing patval " <> show n <> " leads to no new types"
     show (UnhelpfulSplit n) =
@@ -400,7 +446,20 @@ data Synthesized a = Synthesized
     -- ^ The number of recursive calls
   , syn_val    :: a
   }
-  deriving (Eq, Show, Functor, Foldable, Traversable, Generic)
+  deriving stock (Eq, Show, Functor, Foldable, Traversable, Generic, Data, Typeable)
+
+instance Monad Synthesized where
+  return = pure
+  Synthesized tr1 sc1 uv1 rc1 a >>= f =
+    case f a of
+      Synthesized tr2 sc2 uv2 rc2 b ->
+        Synthesized
+          { syn_trace = tr1 <> tr2
+          , syn_scoped = sc1 <> sc2
+          , syn_used_vals = uv1 <> uv2
+          , syn_recursion_count = rc1 <> rc2
+          , syn_val = b
+          }
 
 mapTrace :: (Trace -> Trace) -> Synthesized a -> Synthesized a
 mapTrace f (Synthesized tr sc uv rc a) = Synthesized (f tr) sc uv rc a
@@ -460,7 +519,7 @@ emptyContext
 
 
 newtype Rose a = Rose (Tree a)
-  deriving stock (Eq, Functor, Generic)
+  deriving stock (Eq, Functor, Generic, Data, Typeable)
 
 instance Show (Rose String) where
   show = unlines . dropEveryOther . lines . drawTree . coerce
diff --git a/plugins/hls-tactics-plugin/test/Utils.hs b/plugins/hls-tactics-plugin/test/Utils.hs
index 26cfc343d1..36bdc8dfc8 100644
--- a/plugins/hls-tactics-plugin/test/Utils.hs
+++ b/plugins/hls-tactics-plugin/test/Utils.hs
@@ -15,6 +15,7 @@ import           Control.Monad.IO.Class
 import           Data.Aeson
 import           Data.Foldable
 import           Data.Function (on)
+import           Data.IORef (writeIORef)
 import           Data.Maybe
 import           Data.Text (Text)
 import qualified Data.Text as T
@@ -53,6 +54,19 @@ codeActionTitle InL{}                               = Nothing
 codeActionTitle (InR(CodeAction title _ _ _ _ _ _ _)) = Just title
 
 
+resetGlobalHoleRef :: IO ()
+resetGlobalHoleRef = writeIORef globalHoleRef 0
+
+
+runSessionForTactics :: Session a -> IO a
+runSessionForTactics =
+  runSessionWithServer'
+    [plugin]
+    def
+    (def { messageTimeout = 5 } )
+    fullCaps
+    tacticPath
+
 ------------------------------------------------------------------------------
 -- | Make a tactic unit test.
 mkTest
@@ -67,7 +81,8 @@ mkTest
          ) -- ^ A collection of (un)expected code actions.
     -> SpecWith (Arg Bool)
 mkTest name fp line col ts = it name $ do
-  runSessionWithServer plugin tacticPath $ do
+  resetGlobalHoleRef
+  runSessionForTactics $ do
     doc <- openDoc (fp <.> "hs") "haskell"
     _ <- waitForDiagnostics
     actions <- getCodeActions doc $ pointRange line col
@@ -89,7 +104,8 @@ mkGoldenTest
     -> SpecWith ()
 mkGoldenTest eq tc occ line col input =
   it (input <> " (golden)") $ do
-    runSessionWithServer plugin tacticPath $ do
+    resetGlobalHoleRef
+    runSessionForTactics $ do
       doc <- openDoc (input <.> "hs") "haskell"
       _ <- waitForDiagnostics
       actions <- getCodeActions doc $ pointRange line col
@@ -111,7 +127,8 @@ mkCodeLensTest
     -> SpecWith ()
 mkCodeLensTest input =
   it (input <> " (golden)") $ do
-    runSessionWithServer plugin tacticPath $ do
+    resetGlobalHoleRef
+    runSessionForTactics $ do
       doc <- openDoc (input <.> "hs") "haskell"
       _ <- waitForDiagnostics
       lenses <- fmap (reverse . filter isWingmanLens) $ getCodeLenses doc
@@ -134,7 +151,8 @@ mkNoCodeLensTest
     -> SpecWith ()
 mkNoCodeLensTest input =
   it (input <> " (no code lenses)") $ do
-    runSessionWithServer plugin tacticPath $ do
+    resetGlobalHoleRef
+    runSessionForTactics $ do
       doc <- openDoc (input <.> "hs") "haskell"
       _ <- waitForDiagnostics
       lenses <- fmap (reverse . filter isWingmanLens) $ getCodeLenses doc
@@ -158,7 +176,8 @@ mkShowMessageTest
     -> SpecWith ()
 mkShowMessageTest tc occ line col input ufm =
   it (input <> " (golden)") $ do
-    runSessionWithServer plugin tacticPath $ do
+    resetGlobalHoleRef
+    runSessionForTactics $ do
       doc <- openDoc (input <.> "hs") "haskell"
       _ <- waitForDiagnostics
       actions <- getCodeActions doc $ pointRange line col
diff --git a/plugins/hls-tactics-plugin/test/golden/DestructAllAnd.expected.hs b/plugins/hls-tactics-plugin/test/golden/DestructAllAnd.expected.hs
index 83a0c09f35..392bd9d2cd 100644
--- a/plugins/hls-tactics-plugin/test/golden/DestructAllAnd.expected.hs
+++ b/plugins/hls-tactics-plugin/test/golden/DestructAllAnd.expected.hs
@@ -1,5 +1,5 @@
 and :: Bool -> Bool -> Bool
-and False False = _
-and False True = _
-and True False = _
-and True True = _
+and False False = _w0
+and False True = _w1
+and True False = _w2
+and True True = _w3
diff --git a/plugins/hls-tactics-plugin/test/golden/DestructAllFunc.expected.hs b/plugins/hls-tactics-plugin/test/golden/DestructAllFunc.expected.hs
index ebc9903a7b..536d15b107 100644
--- a/plugins/hls-tactics-plugin/test/golden/DestructAllFunc.expected.hs
+++ b/plugins/hls-tactics-plugin/test/golden/DestructAllFunc.expected.hs
@@ -1,4 +1,4 @@
 has_a_func :: Bool -> (a -> b) -> Bool
-has_a_func False y = _
-has_a_func True y = _
+has_a_func False y = _w0
+has_a_func True y = _w1
 
diff --git a/plugins/hls-tactics-plugin/test/golden/DestructAllGADTEvidence.expected.hs b/plugins/hls-tactics-plugin/test/golden/DestructAllGADTEvidence.expected.hs
index b0b520347d..0e4c0985fa 100644
--- a/plugins/hls-tactics-plugin/test/golden/DestructAllGADTEvidence.expected.hs
+++ b/plugins/hls-tactics-plugin/test/golden/DestructAllGADTEvidence.expected.hs
@@ -16,6 +16,6 @@ data ElemAt (n :: Nat) t (ts :: [Type]) where
   AtS :: ElemAt k t ts -> ElemAt ('S k) t (u ': ts)
 
 lookMeUp :: ElemAt i ty tys -> HList tys -> ty
-lookMeUp AtZ (HCons t hl') = _
-lookMeUp (AtS ea') (HCons t hl') = _
+lookMeUp AtZ (HCons t hl') = _w0
+lookMeUp (AtS ea') (HCons t hl') = _w1
 
diff --git a/plugins/hls-tactics-plugin/test/golden/DestructAllMany.expected.hs b/plugins/hls-tactics-plugin/test/golden/DestructAllMany.expected.hs
index c443ed795e..366a3eac70 100644
--- a/plugins/hls-tactics-plugin/test/golden/DestructAllMany.expected.hs
+++ b/plugins/hls-tactics-plugin/test/golden/DestructAllMany.expected.hs
@@ -1,27 +1,27 @@
 data ABC = A | B | C
 
 many :: () -> Either a b -> Bool -> Maybe ABC -> ABC -> ()
-many () (Left a) False Nothing A = _
-many () (Left a) False Nothing B = _
-many () (Left a) False Nothing C = _
-many () (Left a) False (Just abc') A = _
-many () (Left a) False (Just abc') B = _
-many () (Left a) False (Just abc') C = _
-many () (Left a) True Nothing A = _
-many () (Left a) True Nothing B = _
-many () (Left a) True Nothing C = _
-many () (Left a) True (Just abc') A = _
-many () (Left a) True (Just abc') B = _
-many () (Left a) True (Just abc') C = _
-many () (Right b') False Nothing A = _
-many () (Right b') False Nothing B = _
-many () (Right b') False Nothing C = _
-many () (Right b') False (Just abc') A = _
-many () (Right b') False (Just abc') B = _
-many () (Right b') False (Just abc') C = _
-many () (Right b') True Nothing A = _
-many () (Right b') True Nothing B = _
-many () (Right b') True Nothing C = _
-many () (Right b') True (Just abc') A = _
-many () (Right b') True (Just abc') B = _
-many () (Right b') True (Just abc') C = _
+many () (Left a) False Nothing A = _w0
+many () (Left a) False Nothing B = _w1
+many () (Left a) False Nothing C = _w2
+many () (Left a) False (Just abc') A = _w3
+many () (Left a) False (Just abc') B = _w4
+many () (Left a) False (Just abc') C = _w5
+many () (Left a) True Nothing A = _w6
+many () (Left a) True Nothing B = _w7
+many () (Left a) True Nothing C = _w8
+many () (Left a) True (Just abc') A = _w9
+many () (Left a) True (Just abc') B = _wa
+many () (Left a) True (Just abc') C = _wb
+many () (Right b') False Nothing A = _wc
+many () (Right b') False Nothing B = _wd
+many () (Right b') False Nothing C = _we
+many () (Right b') False (Just abc') A = _wf
+many () (Right b') False (Just abc') B = _wg
+many () (Right b') False (Just abc') C = _wh
+many () (Right b') True Nothing A = _wi
+many () (Right b') True Nothing B = _wj
+many () (Right b') True Nothing C = _wk
+many () (Right b') True (Just abc') A = _wl
+many () (Right b') True (Just abc') B = _wm
+many () (Right b') True (Just abc') C = _wn
diff --git a/plugins/hls-tactics-plugin/test/golden/DestructAllNonVarTopMatch.expected.hs b/plugins/hls-tactics-plugin/test/golden/DestructAllNonVarTopMatch.expected.hs
index 8588fdcbd2..dc1ea66c51 100644
--- a/plugins/hls-tactics-plugin/test/golden/DestructAllNonVarTopMatch.expected.hs
+++ b/plugins/hls-tactics-plugin/test/golden/DestructAllNonVarTopMatch.expected.hs
@@ -1,6 +1,6 @@
 and :: (a, b) -> Bool -> Bool -> Bool
-and (a, b) False False = _
-and (a, b) False True = _
-and (a, b) True False = _
-and (a, b) True True = _
+and (a, b) False False = _w0
+and (a, b) False True = _w1
+and (a, b) True False = _w2
+and (a, b) True True = _w3
 
diff --git a/plugins/hls-tactics-plugin/test/golden/DestructCthulhu.expected.hs b/plugins/hls-tactics-plugin/test/golden/DestructCthulhu.expected.hs
index 610956daea..e885b489a1 100644
--- a/plugins/hls-tactics-plugin/test/golden/DestructCthulhu.expected.hs
+++ b/plugins/hls-tactics-plugin/test/golden/DestructCthulhu.expected.hs
@@ -28,27 +28,27 @@ data FreePro r c a b where
 
 
 cthulhu :: FreePro r c a b -> FreePro r c a b
-cthulhu ID = _
-cthulhu (Comp fp' fp_rcyb) = _
-cthulhu Copy = _
-cthulhu Consume = _
-cthulhu Swap = _
-cthulhu SwapE = _
-cthulhu Fst = _
-cthulhu Snd = _
-cthulhu InjectL = _
-cthulhu InjectR = _
-cthulhu Unify = _
-cthulhu (First fp') = _
-cthulhu (Second fp') = _
-cthulhu (Alongside fp' fp_rca'b') = _
-cthulhu (Fanout fp' fp_rcab') = _
-cthulhu (Left' fp') = _
-cthulhu (Right' fp') = _
-cthulhu (EitherOf fp' fp_rca'b') = _
-cthulhu (Fanin fp' fp_rca'b) = _
-cthulhu (LiftC cab) = _
-cthulhu Zero = _
-cthulhu (Plus fp' fp_rcab) = _
-cthulhu (Unleft fp') = _
-cthulhu (Unright fp') = _
+cthulhu ID = _w0
+cthulhu (Comp fp' fp_rcyb) = _w1
+cthulhu Copy = _w2
+cthulhu Consume = _w3
+cthulhu Swap = _w4
+cthulhu SwapE = _w5
+cthulhu Fst = _w6
+cthulhu Snd = _w7
+cthulhu InjectL = _w8
+cthulhu InjectR = _w9
+cthulhu Unify = _wa
+cthulhu (First fp') = _wb
+cthulhu (Second fp') = _wc
+cthulhu (Alongside fp' fp_rca'b') = _wd
+cthulhu (Fanout fp' fp_rcab') = _we
+cthulhu (Left' fp') = _wf
+cthulhu (Right' fp') = _wg
+cthulhu (EitherOf fp' fp_rca'b') = _wh
+cthulhu (Fanin fp' fp_rca'b) = _wi
+cthulhu (LiftC cab) = _wj
+cthulhu Zero = _wk
+cthulhu (Plus fp' fp_rcab) = _wl
+cthulhu (Unleft fp') = _wm
+cthulhu (Unright fp') = _wn
diff --git a/plugins/hls-tactics-plugin/test/golden/DestructDataFam.expected.hs b/plugins/hls-tactics-plugin/test/golden/DestructDataFam.expected.hs
index dfe2b4561f..e463935583 100644
--- a/plugins/hls-tactics-plugin/test/golden/DestructDataFam.expected.hs
+++ b/plugins/hls-tactics-plugin/test/golden/DestructDataFam.expected.hs
@@ -4,5 +4,5 @@ data family Yo
 data instance Yo = Heya Int
 
 test :: Yo -> Int
-test (Heya n) = _
+test (Heya n) = _w0
 
diff --git a/plugins/hls-tactics-plugin/test/golden/DestructPun.expected.hs b/plugins/hls-tactics-plugin/test/golden/DestructPun.expected.hs
index 2eb47c5c9a..bfd8d09074 100644
--- a/plugins/hls-tactics-plugin/test/golden/DestructPun.expected.hs
+++ b/plugins/hls-tactics-plugin/test/golden/DestructPun.expected.hs
@@ -3,6 +3,6 @@
 
 data Foo = Foo { a :: Bool, b :: Bool }
 
-foo Foo {a = False, b} = _
-foo Foo {a = True, b} = _
+foo Foo {a = False, b} = _w0
+foo Foo {a = True, b} = _w1
 
diff --git a/plugins/hls-tactics-plugin/test/golden/DestructTyFam.expected.hs b/plugins/hls-tactics-plugin/test/golden/DestructTyFam.expected.hs
index 7f1399e5e9..eee4cbd587 100644
--- a/plugins/hls-tactics-plugin/test/golden/DestructTyFam.expected.hs
+++ b/plugins/hls-tactics-plugin/test/golden/DestructTyFam.expected.hs
@@ -4,6 +4,6 @@ type family Yo where
   Yo = Bool
 
 test :: Yo -> Int
-test False = _
-test True = _
+test False = _w0
+test True = _w1
 
diff --git a/plugins/hls-tactics-plugin/test/golden/DestructTyToDataFam.expected.hs b/plugins/hls-tactics-plugin/test/golden/DestructTyToDataFam.expected.hs
index fe1d75ec92..3016c4ef4e 100644
--- a/plugins/hls-tactics-plugin/test/golden/DestructTyToDataFam.expected.hs
+++ b/plugins/hls-tactics-plugin/test/golden/DestructTyToDataFam.expected.hs
@@ -14,5 +14,5 @@ data family Yo
 data instance Yo = Heya Int
 
 test :: T1 Bool -> Int
-test (Heya n) = _
+test (Heya n) = _w0
 
diff --git a/plugins/hls-tactics-plugin/test/golden/GoldenGADTDestruct.expected.hs b/plugins/hls-tactics-plugin/test/golden/GoldenGADTDestruct.expected.hs
index 7f9975ba33..3f5f4fa157 100644
--- a/plugins/hls-tactics-plugin/test/golden/GoldenGADTDestruct.expected.hs
+++ b/plugins/hls-tactics-plugin/test/golden/GoldenGADTDestruct.expected.hs
@@ -4,4 +4,4 @@ data CtxGADT where
   MkCtxGADT :: (Show a, Eq a) => a -> CtxGADT
 
 ctxGADT :: CtxGADT -> String
-ctxGADT (MkCtxGADT a) = _
+ctxGADT (MkCtxGADT a) = _w0
diff --git a/plugins/hls-tactics-plugin/test/golden/GoldenGADTDestructCoercion.expected.hs b/plugins/hls-tactics-plugin/test/golden/GoldenGADTDestructCoercion.expected.hs
index 57aab53bb4..4f4b2d3a4a 100644
--- a/plugins/hls-tactics-plugin/test/golden/GoldenGADTDestructCoercion.expected.hs
+++ b/plugins/hls-tactics-plugin/test/golden/GoldenGADTDestructCoercion.expected.hs
@@ -5,4 +5,4 @@ data E a b where
   E :: forall a b. (b ~ a, Ord a) => b -> E a [a]
 
 ctxGADT :: E a b -> String
-ctxGADT (E b) = _
+ctxGADT (E b) = _w0
diff --git a/plugins/hls-tactics-plugin/test/golden/GoldenIntros.expected.hs b/plugins/hls-tactics-plugin/test/golden/GoldenIntros.expected.hs
index 1a17ee1be0..0ae8c4bbac 100644
--- a/plugins/hls-tactics-plugin/test/golden/GoldenIntros.expected.hs
+++ b/plugins/hls-tactics-plugin/test/golden/GoldenIntros.expected.hs
@@ -1,2 +1,2 @@
 blah :: Int -> Bool -> (a -> b) -> String -> Int
-blah n b fab s = _
+blah n b fab s = _w0
diff --git a/plugins/hls-tactics-plugin/test/golden/IntrosTooMany.expected.hs b/plugins/hls-tactics-plugin/test/golden/IntrosTooMany.expected.hs
index 0deb964ab6..97668d8c90 100644
--- a/plugins/hls-tactics-plugin/test/golden/IntrosTooMany.expected.hs
+++ b/plugins/hls-tactics-plugin/test/golden/IntrosTooMany.expected.hs
@@ -1,2 +1,2 @@
 too_many :: a -> b -> c
-too_many a b = _
+too_many a b = _w0
diff --git a/plugins/hls-tactics-plugin/test/golden/KnownMissingMonoid.expected.hs b/plugins/hls-tactics-plugin/test/golden/KnownMissingMonoid.expected.hs
index 430db91cba..f64222977b 100644
--- a/plugins/hls-tactics-plugin/test/golden/KnownMissingMonoid.expected.hs
+++ b/plugins/hls-tactics-plugin/test/golden/KnownMissingMonoid.expected.hs
@@ -4,5 +4,5 @@ instance Semigroup (Mono a) where
   (<>) = undefined
 
 instance Monoid (Mono a) where
-  mempty = Monoid mempty _
+  mempty = Monoid mempty _w0
 
diff --git a/plugins/hls-tactics-plugin/test/golden/KnownMissingSemigroup.expected.hs b/plugins/hls-tactics-plugin/test/golden/KnownMissingSemigroup.expected.hs
index 113ca4636d..3f18919e80 100644
--- a/plugins/hls-tactics-plugin/test/golden/KnownMissingSemigroup.expected.hs
+++ b/plugins/hls-tactics-plugin/test/golden/KnownMissingSemigroup.expected.hs
@@ -1,5 +1,5 @@
 data Semi = Semi [String] Int
 
 instance Semigroup Semi where
-  (Semi ss n) <> (Semi strs i) = Semi (ss <> strs) _
+  (Semi ss n) <> (Semi strs i) = Semi (ss <> strs) _w0
 
diff --git a/plugins/hls-tactics-plugin/test/golden/LayoutBind.expected.hs b/plugins/hls-tactics-plugin/test/golden/LayoutBind.expected.hs
index fc9ab411ea..c65b7d07d0 100644
--- a/plugins/hls-tactics-plugin/test/golden/LayoutBind.expected.hs
+++ b/plugins/hls-tactics-plugin/test/golden/LayoutBind.expected.hs
@@ -2,7 +2,7 @@ test :: Bool -> IO ()
 test b = do
   putStrLn "hello"
   case b of
-    False -> _
-    True -> _
+    False -> _w0
+    True -> _w1
   pure ()
 
diff --git a/plugins/hls-tactics-plugin/test/golden/LayoutDollarApp.expected.hs b/plugins/hls-tactics-plugin/test/golden/LayoutDollarApp.expected.hs
index 938561984a..32e08c94a8 100644
--- a/plugins/hls-tactics-plugin/test/golden/LayoutDollarApp.expected.hs
+++ b/plugins/hls-tactics-plugin/test/golden/LayoutDollarApp.expected.hs
@@ -1,5 +1,5 @@
 test :: Bool -> Bool
 test b = id $ (case b of
-   False -> _
-   True -> _)
+   False -> _w0
+   True -> _w1)
 
diff --git a/plugins/hls-tactics-plugin/test/golden/LayoutInfixKeep.expected.hs b/plugins/hls-tactics-plugin/test/golden/LayoutInfixKeep.expected.hs
index 7274905dbe..b4d3ee6a0e 100644
--- a/plugins/hls-tactics-plugin/test/golden/LayoutInfixKeep.expected.hs
+++ b/plugins/hls-tactics-plugin/test/golden/LayoutInfixKeep.expected.hs
@@ -1,5 +1,5 @@
 -- keep layout that was written by the user in infix
 foo :: Bool -> a -> a
-False `foo` a = _
-True `foo` a = _
+False `foo` a = _w0
+True `foo` a = _w1
 
diff --git a/plugins/hls-tactics-plugin/test/golden/LayoutLam.expected.hs b/plugins/hls-tactics-plugin/test/golden/LayoutLam.expected.hs
index e0b2ac2ddf..d8b34c8939 100644
--- a/plugins/hls-tactics-plugin/test/golden/LayoutLam.expected.hs
+++ b/plugins/hls-tactics-plugin/test/golden/LayoutLam.expected.hs
@@ -1,5 +1,5 @@
 test :: Bool -> Bool
 test = \b -> case b of
-  False -> _
-  True -> _
+  False -> _w0
+  True -> _w1
 
diff --git a/plugins/hls-tactics-plugin/test/golden/LayoutOpApp.expected.hs b/plugins/hls-tactics-plugin/test/golden/LayoutOpApp.expected.hs
index 520aaed931..e8bc6ccc87 100644
--- a/plugins/hls-tactics-plugin/test/golden/LayoutOpApp.expected.hs
+++ b/plugins/hls-tactics-plugin/test/golden/LayoutOpApp.expected.hs
@@ -1,4 +1,4 @@
 test :: Bool -> Bool
 test b = True && (case b of
-   False -> _
-   True -> _)
+   False -> _w0
+   True -> _w1)
diff --git a/plugins/hls-tactics-plugin/test/golden/LayoutPrefixKeep.expected.hs b/plugins/hls-tactics-plugin/test/golden/LayoutPrefixKeep.expected.hs
index a71fdba70e..bffe1b6852 100644
--- a/plugins/hls-tactics-plugin/test/golden/LayoutPrefixKeep.expected.hs
+++ b/plugins/hls-tactics-plugin/test/golden/LayoutPrefixKeep.expected.hs
@@ -1,4 +1,4 @@
 (-/) :: Bool -> a -> a
-(-/) False a = _
-(-/) True a = _
+(-/) False a = _w0
+(-/) True a = _w1
 
diff --git a/plugins/hls-tactics-plugin/test/golden/LayoutRec.expected.hs b/plugins/hls-tactics-plugin/test/golden/LayoutRec.expected.hs
index 9818d23e5e..ef639a9839 100644
--- a/plugins/hls-tactics-plugin/test/golden/LayoutRec.expected.hs
+++ b/plugins/hls-tactics-plugin/test/golden/LayoutRec.expected.hs
@@ -1,5 +1,5 @@
 data Pair a b = Pair {pa :: a, pb :: b}
 
 p :: Pair (a -> a) (a -> b -> c -> b)
-p = Pair {pa = _, pb = \ a b c -> _}
+p = Pair {pa = _, pb = \ a b c -> _w0}
 
diff --git a/plugins/hls-tactics-plugin/test/golden/LayoutSplitClass.expected.hs b/plugins/hls-tactics-plugin/test/golden/LayoutSplitClass.expected.hs
index a1e34d3db6..9bcb21c9e7 100644
--- a/plugins/hls-tactics-plugin/test/golden/LayoutSplitClass.expected.hs
+++ b/plugins/hls-tactics-plugin/test/golden/LayoutSplitClass.expected.hs
@@ -1,5 +1,5 @@
 class Test a where
   test :: Bool -> a
-  test False = _
-  test True = _
+  test False = _w0
+  test True = _w1
 
diff --git a/plugins/hls-tactics-plugin/test/golden/LayoutSplitGuard.expected.hs b/plugins/hls-tactics-plugin/test/golden/LayoutSplitGuard.expected.hs
index cd3cca6c2e..6b73dfb0ec 100644
--- a/plugins/hls-tactics-plugin/test/golden/LayoutSplitGuard.expected.hs
+++ b/plugins/hls-tactics-plugin/test/golden/LayoutSplitGuard.expected.hs
@@ -1,5 +1,5 @@
 test :: Bool -> Bool -> Bool
 test a b
   | a = case b of
-  False -> _
-  True -> _
+  False -> _w0
+  True -> _w1
diff --git a/plugins/hls-tactics-plugin/test/golden/LayoutSplitIn.expected.hs b/plugins/hls-tactics-plugin/test/golden/LayoutSplitIn.expected.hs
index a184fe004f..8095217673 100644
--- a/plugins/hls-tactics-plugin/test/golden/LayoutSplitIn.expected.hs
+++ b/plugins/hls-tactics-plugin/test/golden/LayoutSplitIn.expected.hs
@@ -1,5 +1,5 @@
 test :: a
 test =
   let a = (1,"bbb")
-   in case a of { (n, s) -> _ }
+   in case a of { (n, s) -> _w0 }
 
diff --git a/plugins/hls-tactics-plugin/test/golden/LayoutSplitLet.expected.hs b/plugins/hls-tactics-plugin/test/golden/LayoutSplitLet.expected.hs
index a042cb3b13..ba63836df3 100644
--- a/plugins/hls-tactics-plugin/test/golden/LayoutSplitLet.expected.hs
+++ b/plugins/hls-tactics-plugin/test/golden/LayoutSplitLet.expected.hs
@@ -1,7 +1,7 @@
 test :: a
 test =
   let t :: Bool -> a
-      t False = _
-      t True = _
+      t False = _w0
+      t True = _w1
    in _
 
diff --git a/plugins/hls-tactics-plugin/test/golden/LayoutSplitPatSyn.expected.hs b/plugins/hls-tactics-plugin/test/golden/LayoutSplitPatSyn.expected.hs
index 550b8f9296..0f7ee4e388 100644
--- a/plugins/hls-tactics-plugin/test/golden/LayoutSplitPatSyn.expected.hs
+++ b/plugins/hls-tactics-plugin/test/golden/LayoutSplitPatSyn.expected.hs
@@ -5,7 +5,7 @@ pattern JustSingleton a <- Just [a]
 
 
 test :: Maybe [Bool] -> Maybe Bool
-test (JustSingleton False) = _
-test (JustSingleton True) = _
+test (JustSingleton False) = _w0
+test (JustSingleton True) = _w1
 
 
diff --git a/plugins/hls-tactics-plugin/test/golden/LayoutSplitPattern.expected.hs b/plugins/hls-tactics-plugin/test/golden/LayoutSplitPattern.expected.hs
index e99d112e6f..b92544f622 100644
--- a/plugins/hls-tactics-plugin/test/golden/LayoutSplitPattern.expected.hs
+++ b/plugins/hls-tactics-plugin/test/golden/LayoutSplitPattern.expected.hs
@@ -4,6 +4,6 @@ pattern Blah :: a -> Maybe a
 pattern Blah a = Just a
 
 test :: Maybe Bool -> a
-test (Blah False) = _
-test (Blah True) = _
+test (Blah False) = _w0
+test (Blah True) = _w1
 
diff --git a/plugins/hls-tactics-plugin/test/golden/LayoutSplitViewPat.expected.hs b/plugins/hls-tactics-plugin/test/golden/LayoutSplitViewPat.expected.hs
index 132ae26baf..d123c652d7 100644
--- a/plugins/hls-tactics-plugin/test/golden/LayoutSplitViewPat.expected.hs
+++ b/plugins/hls-tactics-plugin/test/golden/LayoutSplitViewPat.expected.hs
@@ -1,6 +1,6 @@
 {-# LANGUAGE ViewPatterns #-}
 
 splitLookup :: [(Int, String)] -> String
-splitLookup (lookup 5 -> Nothing) = _
-splitLookup (lookup 5 -> (Just s)) = _
+splitLookup (lookup 5 -> Nothing) = _w0
+splitLookup (lookup 5 -> (Just s)) = _w1
 
diff --git a/plugins/hls-tactics-plugin/test/golden/LayoutSplitWhere.expected.hs b/plugins/hls-tactics-plugin/test/golden/LayoutSplitWhere.expected.hs
index a6150ce53e..28ad669007 100644
--- a/plugins/hls-tactics-plugin/test/golden/LayoutSplitWhere.expected.hs
+++ b/plugins/hls-tactics-plugin/test/golden/LayoutSplitWhere.expected.hs
@@ -8,7 +8,7 @@ some a = do
       foo = putStrLn "Hi"
 
       bar :: A -> IO ()
-      bar A = _
-      bar B = _
-      bar C = _
+      bar A = _w0
+      bar B = _w1
+      bar C = _w2
 
diff --git a/plugins/hls-tactics-plugin/test/golden/MetaBindOne.expected.hs b/plugins/hls-tactics-plugin/test/golden/MetaBindOne.expected.hs
index 5c28b9649e..05f86c9963 100644
--- a/plugins/hls-tactics-plugin/test/golden/MetaBindOne.expected.hs
+++ b/plugins/hls-tactics-plugin/test/golden/MetaBindOne.expected.hs
@@ -1,2 +1,2 @@
 foo :: a -> (a, a)
-foo a = (a, _)
+foo a = (a, _w0)
diff --git a/plugins/hls-tactics-plugin/test/golden/MetaCataAST.expected.hs b/plugins/hls-tactics-plugin/test/golden/MetaCataAST.expected.hs
index d0597676d2..aac10101ec 100644
--- a/plugins/hls-tactics-plugin/test/golden/MetaCataAST.expected.hs
+++ b/plugins/hls-tactics-plugin/test/golden/MetaCataAST.expected.hs
@@ -14,10 +14,10 @@ eval (If ast ast' ast_a)
       ast_c = eval ast
       ast'_c = eval ast'
       ast_a_c = eval ast_a
-    in _ ast_c ast'_c ast_a_c
+    in _w0 ast_c ast'_c ast_a_c
 eval (Equal ast ast')
   = let
       ast_c = eval ast
       ast'_c = eval ast'
-    in _ ast_c ast'_c
+    in _w1 ast_c ast'_c
 
diff --git a/plugins/hls-tactics-plugin/test/golden/MetaCataCollapse.expected.hs b/plugins/hls-tactics-plugin/test/golden/MetaCataCollapse.expected.hs
index be8310b97f..58b4fb4ffc 100644
--- a/plugins/hls-tactics-plugin/test/golden/MetaCataCollapse.expected.hs
+++ b/plugins/hls-tactics-plugin/test/golden/MetaCataCollapse.expected.hs
@@ -10,5 +10,5 @@ instance (Yo f, Yo g) => Yo (f :*: g) where
     = let
         fx_c = yo fx
         gx_c = yo gx
-      in _ fx_c gx_c
+      in _w0 fx_c gx_c
 
diff --git a/plugins/hls-tactics-plugin/test/golden/MetaTry.expected.hs b/plugins/hls-tactics-plugin/test/golden/MetaTry.expected.hs
index 807b9bdcb5..0940f9ea21 100644
--- a/plugins/hls-tactics-plugin/test/golden/MetaTry.expected.hs
+++ b/plugins/hls-tactics-plugin/test/golden/MetaTry.expected.hs
@@ -1,2 +1,2 @@
 foo :: a -> (b, a)
-foo a = (_, a)
+foo a = (_w0, a)
diff --git a/plugins/hls-tactics-plugin/test/golden/MetaUseSymbol.expected.hs b/plugins/hls-tactics-plugin/test/golden/MetaUseSymbol.expected.hs
index 20db691ef6..85012d7aaf 100644
--- a/plugins/hls-tactics-plugin/test/golden/MetaUseSymbol.expected.hs
+++ b/plugins/hls-tactics-plugin/test/golden/MetaUseSymbol.expected.hs
@@ -1,4 +1,4 @@
 import Data.Monoid
 
 resolve :: Sum Int
-resolve = _ <> _
+resolve = _w0 <> _w1
diff --git a/plugins/hls-tactics-plugin/test/golden/MetaWithArg.expected.hs b/plugins/hls-tactics-plugin/test/golden/MetaWithArg.expected.hs
index 4110ddcbb4..895e9333c0 100644
--- a/plugins/hls-tactics-plugin/test/golden/MetaWithArg.expected.hs
+++ b/plugins/hls-tactics-plugin/test/golden/MetaWithArg.expected.hs
@@ -1,2 +1,2 @@
 wat :: a -> b
-wat a = _ a
+wat a = _w0 a
diff --git a/plugins/hls-tactics-plugin/test/golden/PunGADT.expected.hs b/plugins/hls-tactics-plugin/test/golden/PunGADT.expected.hs
index f0ecf407ff..9bdcd61516 100644
--- a/plugins/hls-tactics-plugin/test/golden/PunGADT.expected.hs
+++ b/plugins/hls-tactics-plugin/test/golden/PunGADT.expected.hs
@@ -8,5 +8,5 @@ data GADT a where
 
 
 split :: GADT a -> a
-split GADT {blah, bar} = _
+split GADT {blah, bar} = _w0
 
diff --git a/plugins/hls-tactics-plugin/test/golden/PunMany.expected.hs b/plugins/hls-tactics-plugin/test/golden/PunMany.expected.hs
index 3c438280b6..7b661c2ee5 100644
--- a/plugins/hls-tactics-plugin/test/golden/PunMany.expected.hs
+++ b/plugins/hls-tactics-plugin/test/golden/PunMany.expected.hs
@@ -3,6 +3,6 @@ data Many
   | Goodbye { a :: Int, b :: Bool, c :: Many }
 
 test :: Many -> Many
-test Hello {world} = _
-test Goodbye {a, b, c} = _
+test Hello {world} = _w0
+test Goodbye {a, b, c} = _w1
 
diff --git a/plugins/hls-tactics-plugin/test/golden/PunManyGADT.expected.hs b/plugins/hls-tactics-plugin/test/golden/PunManyGADT.expected.hs
index f181fafe2d..5b3eaf2559 100644
--- a/plugins/hls-tactics-plugin/test/golden/PunManyGADT.expected.hs
+++ b/plugins/hls-tactics-plugin/test/golden/PunManyGADT.expected.hs
@@ -14,6 +14,6 @@ data GADT a where
 
 
 split :: GADT Bool -> a
-split GADT {blah, bar} = _
-split Bar {zoo, baxter, another} = _
+split GADT {blah, bar} = _w0
+split Bar {zoo, baxter, another} = _w1
 
diff --git a/plugins/hls-tactics-plugin/test/golden/PunShadowing.expected.hs b/plugins/hls-tactics-plugin/test/golden/PunShadowing.expected.hs
index 30085f4711..d3cc689a04 100644
--- a/plugins/hls-tactics-plugin/test/golden/PunShadowing.expected.hs
+++ b/plugins/hls-tactics-plugin/test/golden/PunShadowing.expected.hs
@@ -1,5 +1,5 @@
 data Bar = Bar { ax :: Int, bax :: Bool }
 
 bar :: () -> Bar -> Int
-bar ax Bar {ax = n, bax} = _
+bar ax Bar {ax = n, bax} = _w0
 
diff --git a/plugins/hls-tactics-plugin/test/golden/PunSimple.expected.hs b/plugins/hls-tactics-plugin/test/golden/PunSimple.expected.hs
index 87620ca41a..65bc2d28d0 100644
--- a/plugins/hls-tactics-plugin/test/golden/PunSimple.expected.hs
+++ b/plugins/hls-tactics-plugin/test/golden/PunSimple.expected.hs
@@ -1,5 +1,5 @@
 data Bar = Bar { ax :: Int, bax :: Bool }
 
 bar :: Bar -> Int
-bar Bar {ax, bax} = _
+bar Bar {ax, bax} = _w0
 
diff --git a/plugins/hls-tactics-plugin/test/golden/RefineCon.expected.hs b/plugins/hls-tactics-plugin/test/golden/RefineCon.expected.hs
index 9428bf12d9..7110f637da 100644
--- a/plugins/hls-tactics-plugin/test/golden/RefineCon.expected.hs
+++ b/plugins/hls-tactics-plugin/test/golden/RefineCon.expected.hs
@@ -1,3 +1,3 @@
 test :: ((), (b, c), d)
-test = (_, _, _)
+test = (_w0, _w1, _w2)
 
diff --git a/plugins/hls-tactics-plugin/test/golden/RefineGADT.expected.hs b/plugins/hls-tactics-plugin/test/golden/RefineGADT.expected.hs
index 1562e12171..605f5e0a5c 100644
--- a/plugins/hls-tactics-plugin/test/golden/RefineGADT.expected.hs
+++ b/plugins/hls-tactics-plugin/test/golden/RefineGADT.expected.hs
@@ -5,5 +5,5 @@ data GADT a where
   Two :: GADT Bool
 
 test :: z -> GADT Int
-test z = One _
+test z = One _w0
 
diff --git a/plugins/hls-tactics-plugin/test/golden/RefineIntro.expected.hs b/plugins/hls-tactics-plugin/test/golden/RefineIntro.expected.hs
index 4cacf9e17c..5c99dfc3a1 100644
--- a/plugins/hls-tactics-plugin/test/golden/RefineIntro.expected.hs
+++ b/plugins/hls-tactics-plugin/test/golden/RefineIntro.expected.hs
@@ -1,2 +1,2 @@
 test :: a -> Either a b
-test a = _
+test a = _w0
diff --git a/plugins/hls-tactics-plugin/test/golden/RefineReader.expected.hs b/plugins/hls-tactics-plugin/test/golden/RefineReader.expected.hs
index d7f536ef1f..267e6b8015 100644
--- a/plugins/hls-tactics-plugin/test/golden/RefineReader.expected.hs
+++ b/plugins/hls-tactics-plugin/test/golden/RefineReader.expected.hs
@@ -1,5 +1,5 @@
 newtype Reader r a = Reader (r -> a)
 
 test :: b -> Reader r a
-test b = Reader _
+test b = Reader _w0
 
diff --git a/plugins/hls-tactics-plugin/test/golden/SplitPattern.expected.hs b/plugins/hls-tactics-plugin/test/golden/SplitPattern.expected.hs
index 7691dfdbab..c76acc0d31 100644
--- a/plugins/hls-tactics-plugin/test/golden/SplitPattern.expected.hs
+++ b/plugins/hls-tactics-plugin/test/golden/SplitPattern.expected.hs
@@ -4,9 +4,9 @@ case_split :: ADT -> Int
 case_split One        = _
 case_split (Two i)    = _
 case_split Three      = _
-case_split (Four b One) = _
-case_split (Four b (Two n)) = _
-case_split (Four b Three) = _
-case_split (Four b (Four b' adt)) = _
-case_split (Four b Five) = _
+case_split (Four b One) = _w0
+case_split (Four b (Two n)) = _w1
+case_split (Four b Three) = _w2
+case_split (Four b (Four b' adt)) = _w3
+case_split (Four b Five) = _w4
 case_split Five       = _
diff --git a/plugins/hls-tactics-plugin/test/golden/UseConLeft.expected.hs b/plugins/hls-tactics-plugin/test/golden/UseConLeft.expected.hs
index cd04697d6a..26d6d77b8b 100644
--- a/plugins/hls-tactics-plugin/test/golden/UseConLeft.expected.hs
+++ b/plugins/hls-tactics-plugin/test/golden/UseConLeft.expected.hs
@@ -1,3 +1,3 @@
 test :: Either a b
-test = Left _
+test = Left _w0
 
diff --git a/plugins/hls-tactics-plugin/test/golden/UseConPair.expected.hs b/plugins/hls-tactics-plugin/test/golden/UseConPair.expected.hs
index 130c3dd7c9..1a5caad890 100644
--- a/plugins/hls-tactics-plugin/test/golden/UseConPair.expected.hs
+++ b/plugins/hls-tactics-plugin/test/golden/UseConPair.expected.hs
@@ -1,2 +1,2 @@
 test :: (a, b)
-test = (_, _)
+test = (_w0, _w1)
diff --git a/plugins/hls-tactics-plugin/test/golden/UseConRight.expected.hs b/plugins/hls-tactics-plugin/test/golden/UseConRight.expected.hs
index beaecf28c5..f36809804c 100644
--- a/plugins/hls-tactics-plugin/test/golden/UseConRight.expected.hs
+++ b/plugins/hls-tactics-plugin/test/golden/UseConRight.expected.hs
@@ -1,3 +1,3 @@
 test :: Either a b
-test = Right _
+test = Right _w0
 
diff --git a/stack-8.10.2.yaml b/stack-8.10.2.yaml
index c79e8a3c0a..ef52dc2b8d 100644
--- a/stack-8.10.2.yaml
+++ b/stack-8.10.2.yaml
@@ -52,7 +52,7 @@ extra-deps:
   - implicit-hie-cradle-0.3.0.5
   - implicit-hie-0.1.2.6
   - monad-dijkstra-0.1.1.2
-  - refinery-0.3.0.0
+  - refinery-0.4.0.0
   - retrie-0.1.1.1
   - shake-0.19.4
   - stylish-haskell-0.12.2.0
diff --git a/stack-8.10.3.yaml b/stack-8.10.3.yaml
index 81c14ee9fd..ec391239b2 100644
--- a/stack-8.10.3.yaml
+++ b/stack-8.10.3.yaml
@@ -49,7 +49,7 @@ extra-deps:
   - implicit-hie-cradle-0.3.0.5
   - implicit-hie-0.1.2.6
   - monad-dijkstra-0.1.1.2
-  - refinery-0.3.0.0
+  - refinery-0.4.0.0
   - retrie-0.1.1.1
   - shake-0.19.4
   - stylish-haskell-0.12.2.0
diff --git a/stack-8.10.4.yaml b/stack-8.10.4.yaml
index 21f24efcfc..4d39322727 100644
--- a/stack-8.10.4.yaml
+++ b/stack-8.10.4.yaml
@@ -46,7 +46,7 @@ extra-deps:
   - implicit-hie-cradle-0.3.0.5
   - implicit-hie-0.1.2.6
   - monad-dijkstra-0.1.1.2
-  - refinery-0.3.0.0
+  - refinery-0.4.0.0
   - retrie-0.1.1.1
   - stylish-haskell-0.12.2.0
   - semigroups-0.18.5
diff --git a/stack-8.10.5.yaml b/stack-8.10.5.yaml
index 84e3a600a8..0cc36d24dc 100644
--- a/stack-8.10.5.yaml
+++ b/stack-8.10.5.yaml
@@ -48,7 +48,7 @@ extra-deps:
   - implicit-hie-cradle-0.3.0.5
   - implicit-hie-0.1.2.6
   - monad-dijkstra-0.1.1.2
-  - refinery-0.3.0.0
+  - refinery-0.4.0.0
   - retrie-1.0.0.0
   - stylish-haskell-0.12.2.0
   - semigroups-0.18.5
diff --git a/stack-8.6.4.yaml b/stack-8.6.4.yaml
index 9b97b45a33..a62fe521f8 100644
--- a/stack-8.6.4.yaml
+++ b/stack-8.6.4.yaml
@@ -75,7 +75,7 @@ extra-deps:
   - ormolu-0.1.4.1
   - parser-combinators-1.2.1
   - primitive-0.7.1.0
-  - refinery-0.3.0.0
+  - refinery-0.4.0.0
   - regex-base-0.94.0.0
   - regex-pcre-builtin-0.95.1.1.8.43
   - regex-tdfa-1.3.1.0
diff --git a/stack-8.6.5.yaml b/stack-8.6.5.yaml
index 85c4d09dc4..b5c175f65b 100644
--- a/stack-8.6.5.yaml
+++ b/stack-8.6.5.yaml
@@ -76,7 +76,7 @@ extra-deps:
   - ormolu-0.1.4.1
   - parser-combinators-1.2.1
   - primitive-0.7.1.0
-  - refinery-0.3.0.0
+  - refinery-0.4.0.0
   - regex-base-0.94.0.0
   - regex-pcre-builtin-0.95.1.1.8.43
   - regex-tdfa-1.3.1.0
diff --git a/stack-8.8.3.yaml b/stack-8.8.3.yaml
index 22f98f6612..42536fb4e6 100644
--- a/stack-8.8.3.yaml
+++ b/stack-8.8.3.yaml
@@ -62,7 +62,7 @@ extra-deps:
   - opentelemetry-0.6.1
   - opentelemetry-extra-0.6.1
   - ormolu-0.1.4.1
-  - refinery-0.3.0.0
+  - refinery-0.4.0.0
   - retrie-0.1.1.1
   - semigroups-0.18.5
   - shake-0.19.4
diff --git a/stack-8.8.4.yaml b/stack-8.8.4.yaml
index 06a12b4198..64d008be73 100644
--- a/stack-8.8.4.yaml
+++ b/stack-8.8.4.yaml
@@ -61,7 +61,7 @@ extra-deps:
   - monad-dijkstra-0.1.1.2
   - opentelemetry-0.6.1
   - opentelemetry-extra-0.6.1
-  - refinery-0.3.0.0
+  - refinery-0.4.0.0
   - retrie-0.1.1.1
   - semigroups-0.18.5
   - shake-0.19.4
diff --git a/stack-9.0.1.yaml b/stack-9.0.1.yaml
index aac7310ccd..eea9bbed2b 100644
--- a/stack-9.0.1.yaml
+++ b/stack-9.0.1.yaml
@@ -50,7 +50,7 @@ extra-deps:
 - implicit-hie-cradle-0.3.0.5
 - lens-5.0.1
 - profunctors-5.6.2
-- refinery-0.3.0.0@sha256:5ec9588de8f9752b2a947a87ca6a5a0156150ed7b0197975730c007c4549e7fb,1675
+- refinery-0.4.0.0
 - retrie-1.0.0.0
 - some-1.0.2@sha256:3d460998df32ad7b93bf55657aeae988d97070155e71718b4bc75d0997ce9d62,2244
 
diff --git a/stack.yaml b/stack.yaml
index 7b9e722d6f..465192ff00 100644
--- a/stack.yaml
+++ b/stack.yaml
@@ -43,7 +43,7 @@ extra-deps:
   - implicit-hie-cradle-0.3.0.5
   - implicit-hie-0.1.2.6
   - monad-dijkstra-0.1.1.2
-  - refinery-0.3.0.0
+  - refinery-0.4.0.0
   - retrie-0.1.1.1
   - stylish-haskell-0.12.2.0
   - semigroups-0.18.5