diff --git a/ghcide/src/Development/IDE/GHC/ExactPrint.hs b/ghcide/src/Development/IDE/GHC/ExactPrint.hs
index 13ec409ab0..4e494eb82d 100644
--- a/ghcide/src/Development/IDE/GHC/ExactPrint.hs
+++ b/ghcide/src/Development/IDE/GHC/ExactPrint.hs
@@ -196,7 +196,7 @@ needsParensSpace SectionL{}      = (All False, All False)
 needsParensSpace SectionR{}      = (All False, All False)
 needsParensSpace ExplicitTuple{} = (All False, All False)
 needsParensSpace ExplicitSum{}   = (All False, All False)
-needsParensSpace HsCase{}        = (All False, All False)
+needsParensSpace HsCase{}        = (All False, All True)
 needsParensSpace HsIf{}          = (All False, All False)
 needsParensSpace HsMultiIf{}     = (All False, All False)
 needsParensSpace HsLet{}         = (All False, All True)
@@ -337,7 +337,7 @@ genericGraftWithLargestM proxy dst trans = Graft $ \dflags ->
 -- 'everywhereM' or friends.
 --
 -- The 'Int' argument is the index in the list being bound.
-mkBindListT :: forall b m. (Typeable b, Data b, Monad m) => (Int -> b -> m [b]) -> GenericM m
+mkBindListT :: forall b m. (Data b, Monad m) => (Int -> b -> m [b]) -> GenericM m
 mkBindListT f = mkM $ fmap join . traverse (uncurry f) . zip [0..]
 
 
diff --git a/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal b/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal
index a6f4c4e4d2..1d19e74aa2 100644
--- a/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal
+++ b/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal
@@ -37,6 +37,7 @@ library
     Wingman.FeatureSet
     Wingman.GHC
     Wingman.Judgements
+    Wingman.Judgements.SYB
     Wingman.Judgements.Theta
     Wingman.KnownStrategies
     Wingman.KnownStrategies.QuickCheck
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Auto.hs b/plugins/hls-tactics-plugin/src/Wingman/Auto.hs
index 7c42ffd430..31bba590ba 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Auto.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Auto.hs
@@ -1,6 +1,7 @@
 module Wingman.Auto where
 
 import           Control.Monad.State (gets)
+import qualified Data.Set as S
 import           Refinery.Tactic
 import           Wingman.Context
 import           Wingman.Judgements
@@ -24,5 +25,6 @@ auto = do
     . tracing "auto"
     . localTactic (auto' 4)
     . disallowing RecursiveCall
+    . S.fromList
     $ fmap fst current
 
diff --git a/plugins/hls-tactics-plugin/src/Wingman/CaseSplit.hs b/plugins/hls-tactics-plugin/src/Wingman/CaseSplit.hs
index 8083240951..dffb9f30ca 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/CaseSplit.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/CaseSplit.hs
@@ -33,7 +33,7 @@ agdaSplit :: AgdaMatch -> [AgdaMatch]
 agdaSplit (AgdaMatch pats (Case (HsVar _ (L _ var)) matches)) = do
   (pat, body) <- matches
   -- TODO(sandy): use an at pattern if necessary
-  pure $ AgdaMatch (rewriteVarPat var pat pats) body
+  pure $ AgdaMatch (rewriteVarPat var pat pats) $ unLoc body
 agdaSplit x = [x]
 
 
diff --git a/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs b/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs
index 3e38363369..528a2056f8 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs
@@ -160,7 +160,7 @@ destruct' f hi jdg = do
            f
            (Just term)
            (hi_type hi)
-           $ disallowing AlreadyDestructed [term] jdg
+           $ disallowing AlreadyDestructed (S.singleton term) jdg
   pure $ ext
     & #syn_trace     %~ rose ("destruct " <> show term) . pure
     & #syn_used_vals %~ S.insert term
diff --git a/plugins/hls-tactics-plugin/src/Wingman/GHC.hs b/plugins/hls-tactics-plugin/src/Wingman/GHC.hs
index c8b198dc23..c77d183ceb 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/GHC.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/GHC.hs
@@ -19,7 +19,7 @@ import           DataCon
 import           Development.IDE (HscEnvEq (hscEnv))
 import           Development.IDE.Core.Compile (lookupName)
 import           Development.IDE.GHC.Compat
-import           GHC.SourceGen (case', lambda, match)
+import           GHC.SourceGen (lambda)
 import           Generics.SYB (Data, everything, everywhere, listify, mkQ, mkT)
 import           GhcPlugins (extractModule, GlobalRdrElt (gre_name))
 import           OccName
@@ -188,8 +188,8 @@ allOccNames = everything (<>) $ mkQ mempty $ \case
 pattern AMatch :: HsMatchContext (NameOrRdrName (IdP GhcPs)) -> [Pat GhcPs] -> HsExpr GhcPs -> Match GhcPs (LHsExpr GhcPs)
 pattern AMatch ctx pats body <-
   Match { m_ctxt = ctx
-        , m_pats = fmap fromPatCompatPs -> pats
-        , m_grhss = UnguardedRHSs body
+        , m_pats = fmap fromPatCompat -> pats
+        , m_grhss = UnguardedRHSs (unLoc -> body)
         }
 
 
@@ -207,23 +207,23 @@ pattern Lambda pats body <-
 
 ------------------------------------------------------------------------------
 -- | A GRHS that caontains no guards.
-pattern UnguardedRHSs :: HsExpr GhcPs -> GRHSs GhcPs (LHsExpr GhcPs)
+pattern UnguardedRHSs :: LHsExpr p -> GRHSs p (LHsExpr p)
 pattern UnguardedRHSs body <-
-  GRHSs {grhssGRHSs = [L _ (GRHS _ [] (L _ body))]}
+  GRHSs {grhssGRHSs = [L _ (GRHS _ [] body)]}
 
 
 ------------------------------------------------------------------------------
 -- | A match with a single pattern. Case matches are always 'SinglePatMatch'es.
-pattern SinglePatMatch :: Pat GhcPs -> HsExpr GhcPs -> Match GhcPs (LHsExpr GhcPs)
+pattern SinglePatMatch :: PatCompattable p => Pat p -> LHsExpr p -> Match p (LHsExpr p)
 pattern SinglePatMatch pat body <-
-  Match { m_pats = [fromPatCompatPs -> pat]
+  Match { m_pats = [fromPatCompat -> pat]
         , m_grhss = UnguardedRHSs body
         }
 
 
 ------------------------------------------------------------------------------
 -- | Helper function for defining the 'Case' pattern.
-unpackMatches :: [Match GhcPs (LHsExpr GhcPs)] -> Maybe [(Pat GhcPs, HsExpr GhcPs)]
+unpackMatches :: PatCompattable p => [Match p (LHsExpr p)] -> Maybe [(Pat p, LHsExpr p)]
 unpackMatches [] = Just []
 unpackMatches (SinglePatMatch pat body : matches) =
   (:) <$> pure (pat, body) <*> unpackMatches matches
@@ -232,13 +232,10 @@ unpackMatches _ = Nothing
 
 ------------------------------------------------------------------------------
 -- | A pattern over the otherwise (extremely) messy AST for lambdas.
-pattern Case :: HsExpr GhcPs -> [(Pat GhcPs, HsExpr GhcPs)] -> HsExpr GhcPs
+pattern Case :: PatCompattable p => HsExpr p -> [(Pat p, LHsExpr p)] -> HsExpr p
 pattern Case scrutinee matches <-
   HsCase _ (L _ scrutinee)
     (MG {mg_alts = L _ (fmap unLoc -> unpackMatches -> Just matches)})
-  where
-    Case scrutinee matches =
-      case' scrutinee $ fmap (\(pat, body) -> match [pat] body) matches
 
 
 ------------------------------------------------------------------------------
@@ -253,20 +250,30 @@ lambdaCaseable (splitFunTy_maybe -> Just (arg, res))
   = Just $ isJust $ algebraicTyCon res
 lambdaCaseable _ = Nothing
 
--- It's hard to generalize over these since weird type families are involved.
-fromPatCompatTc :: PatCompat GhcTc -> Pat GhcTc
-toPatCompatTc :: Pat GhcTc -> PatCompat GhcTc
-fromPatCompatPs :: PatCompat GhcPs -> Pat GhcPs
+class PatCompattable p where
+  fromPatCompat :: PatCompat p -> Pat p
+  toPatCompat :: Pat p -> PatCompat p
+
 #if __GLASGOW_HASKELL__ == 808
+instance PatCompattable GhcTc where
+  fromPatCompat = id
+  toPatCompat = id
+
+instance PatCompattable GhcPs where
+  fromPatCompat = id
+  toPatCompat = id
+
 type PatCompat pass = Pat pass
-fromPatCompatTc = id
-fromPatCompatPs = id
-toPatCompatTc = id
 #else
+instance PatCompattable GhcTc where
+  fromPatCompat = unLoc
+  toPatCompat = noLoc
+
+instance PatCompattable GhcPs where
+  fromPatCompat = unLoc
+  toPatCompat = noLoc
+
 type PatCompat pass = LPat pass
-fromPatCompatTc = unLoc
-fromPatCompatPs = unLoc
-toPatCompatTc = noLoc
 #endif
 
 ------------------------------------------------------------------------------
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Judgements.hs b/plugins/hls-tactics-plugin/src/Wingman/Judgements.hs
index 37352c5380..e551e492c9 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Judgements.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Judgements.hs
@@ -131,7 +131,7 @@ filterAncestry
     -> Judgement
     -> Judgement
 filterAncestry ancestry reason jdg =
-    disallowing reason (M.keys $ M.filterWithKey go $ hyByName $ jHypothesis jdg) jdg
+    disallowing reason (M.keysSet $ M.filterWithKey go $ hyByName $ jHypothesis jdg) jdg
   where
     go name _
       = not
@@ -198,7 +198,7 @@ filterSameTypeFromOtherPositions dcon pos jdg =
       to_remove =
         M.filter (flip S.member tys . hi_type) (hyByName $ jHypothesis jdg)
           M.\\ hy
-   in disallowing Shadowed (M.keys to_remove) jdg
+   in disallowing Shadowed (M.keysSet to_remove) jdg
 
 
 ------------------------------------------------------------------------------
@@ -258,8 +258,8 @@ patternHypothesis scrutinee dc jdg
 ------------------------------------------------------------------------------
 -- | Prevent some occnames from being used in the hypothesis. This will hide
 -- them from 'jHypothesis', but not from 'jEntireHypothesis'.
-disallowing :: DisallowReason -> [OccName] -> Judgement' a -> Judgement' a
-disallowing reason (S.fromList -> ns) =
+disallowing :: DisallowReason -> S.Set OccName -> Judgement' a -> Judgement' a
+disallowing reason ns =
   field @"_jHypothesis" %~ (\z -> Hypothesis . flip fmap (unHypothesis z) $ \hi ->
     case S.member (hi_name hi) ns of
       True  -> overProvenance (DisallowedPrv reason) hi
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Judgements/SYB.hs b/plugins/hls-tactics-plugin/src/Wingman/Judgements/SYB.hs
new file mode 100644
index 0000000000..c1b5fe63c6
--- /dev/null
+++ b/plugins/hls-tactics-plugin/src/Wingman/Judgements/SYB.hs
@@ -0,0 +1,83 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE RankNTypes          #-}
+
+-- | Custom SYB traversals
+module Wingman.Judgements.SYB where
+
+import Data.Foldable (foldl')
+import Data.Generics hiding (typeRep)
+import Development.IDE.GHC.Compat
+import GHC.Exts (Any)
+import Type.Reflection
+import Unsafe.Coerce (unsafeCoerce)
+
+
+------------------------------------------------------------------------------
+-- | Like 'everything', but only looks inside 'Located' terms that contain the
+-- given 'SrcSpan'.
+everythingContaining
+    :: forall r
+     . Monoid r
+    => SrcSpan
+    -> GenericQ r
+    -> GenericQ r
+everythingContaining dst f = go
+  where
+    go :: GenericQ r
+    go x =
+      case genericIsSubspan dst x of
+        Just False -> mempty
+        _ -> foldl' (<>) (f x) (gmapQ go x)
+
+
+------------------------------------------------------------------------------
+-- | Helper function for implementing 'everythingWithin'
+--
+-- NOTE(sandy): Subtly broken. In an ideal world, this function shuld return
+-- @Just False@ for nodes of /any type/ which do not contain the span. But if
+-- this functionality exists anywhere within the SYB machinery, I have yet to
+-- find it.
+genericIsSubspan
+    :: SrcSpan
+    -> GenericQ (Maybe Bool)
+genericIsSubspan dst = mkQ1 (L noSrcSpan ()) Nothing $ \case
+  L span _ -> Just $ dst `isSubspanOf` span
+
+
+------------------------------------------------------------------------------
+-- | Like 'mkQ', but allows for polymorphic instantiation of its specific case.
+-- This instantation matches whenever the dynamic value has the same
+-- constructor as the proxy @f ()@ value.
+mkQ1 :: forall a r f
+      . (Data a, Data (f ()))
+     => f ()                  -- ^ Polymorphic constructor to match on
+     -> r                     -- ^ Default value
+     -> (forall b. f b -> r)  -- ^ Polymorphic match
+     -> a
+     -> r
+mkQ1 proxy r br a =
+    case l_con == a_con && sameTypeModuloLastApp @a @(f ()) of
+      -- We have proven that the two values share the same constructor, and
+      -- that they have the same type if you ignore the final application.
+      -- Therefore, it is safe to coerce @a@ to @f b@, since @br@ is universal
+      -- over @b@ and can't inspect it.
+      True  -> br $ unsafeCoerce @_ @(f Any) a
+      False -> r
+  where
+    l_con = toConstr proxy
+    a_con = toConstr a
+
+
+------------------------------------------------------------------------------
+-- | Given @a ~ f1 a1@ and @b ~ f2 b2@, returns true if @f1 ~ f2@.
+sameTypeModuloLastApp :: forall a b. (Typeable a, Typeable b) => Bool
+sameTypeModuloLastApp =
+  let tyrep1 = typeRep @a
+      tyrep2 = typeRep @b
+   in case (tyrep1 , tyrep2) of
+        (App a _, App b _) ->
+          case eqTypeRep a b of
+            Just HRefl -> True
+            Nothing    -> False
+        _ -> False
+
diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
index d35dd89452..64d33f9d6a 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
@@ -18,12 +18,12 @@ import           Data.IORef (readIORef)
 import qualified Data.Map as M
 import           Data.Maybe
 import           Data.Monoid
-import qualified Data.Set  as S
+import           Data.Set (Set)
+import qualified Data.Set as S
 import qualified Data.Text as T
 import           Data.Traversable
 import           Development.IDE (getFilesOfInterest, ShowDiagnostic (ShowDiag), srcSpanToRange)
 import           Development.IDE (hscEnv)
-import           Development.IDE.Core.PositionMapping
 import           Development.IDE.Core.RuleTypes
 import           Development.IDE.Core.Rules (usePropertyAction)
 import           Development.IDE.Core.Service (runAction)
@@ -52,6 +52,7 @@ import           Wingman.Context
 import           Wingman.FeatureSet
 import           Wingman.GHC
 import           Wingman.Judgements
+import           Wingman.Judgements.SYB (everythingContaining)
 import           Wingman.Judgements.Theta
 import           Wingman.Range
 import           Wingman.Types
@@ -221,13 +222,15 @@ mkJudgementAndContext features g (TrackedStale binds bmap) rss (TrackedStale tcg
               kt
               evidence
       top_provs = getRhsPosVals tcg_rss tcs
+      already_destructed = getAlreadyDestructed (fmap RealSrcSpan tcg_rss) tcs
       local_hy = spliceProvenance top_provs
                $ hypothesisFromBindings binds_rss binds
       evidence = getEvidenceAtHole (fmap RealSrcSpan tcg_rss) tcs
       cls_hy = foldMap evidenceToHypothesis evidence
       subst = ts_unifier $ appEndo (foldMap (Endo . evidenceToSubst) evidence) defaultTacticState
-  pure
-    ( fmap (CType . substTyAddInScope subst . unCType) $ mkFirstJudgement
+  pure $
+    ( disallowing AlreadyDestructed already_destructed
+    $ fmap (CType . substTyAddInScope subst . unCType) $ mkFirstJudgement
           (local_hy <> cls_hy)
           (isRhsHole tcg_rss tcs)
           g
@@ -235,6 +238,22 @@ mkJudgementAndContext features g (TrackedStale binds bmap) rss (TrackedStale tcg
     )
 
 
+------------------------------------------------------------------------------
+-- | Determine which bindings have already been destructed by the location of
+-- the hole.
+getAlreadyDestructed
+    :: Tracked age SrcSpan
+    -> Tracked age (LHsBinds GhcTc)
+    -> Set OccName
+getAlreadyDestructed (unTrack -> span) (unTrack -> binds) =
+  everythingContaining span
+    (mkQ mempty $ \case
+      Case (HsVar _ (L _ (occName -> var))) _ ->
+        S.singleton var
+      (_ :: HsExpr GhcTc) -> mempty
+    ) binds
+
+
 getSpanAndTypeAtHole
     :: Tracked age Range
     -> Tracked age (HieASTs b)
@@ -302,7 +321,7 @@ buildTopLevelHypothesis name ps = do
 -- | Construct a hypothesis for a single pattern, including building
 -- sub-hypotheses for constructor pattern matches.
 buildPatHy :: Provenance -> PatCompat GhcTc -> State Int (Hypothesis CType)
-buildPatHy prov (fromPatCompatTc -> p0) =
+buildPatHy prov (fromPatCompat -> p0) =
   case p0 of
     VarPat  _ x   -> pure $ mkIdHypothesis (unLoc x) prov
     LazyPat _ p   -> buildPatHy prov p
@@ -317,7 +336,7 @@ buildPatHy prov (fromPatCompatTc -> p0) =
     ListPat x@(ListPatTc ty _) (p : ps) ->
       mkDerivedConHypothesis prov (RealDataCon consDataCon) [ty]
         [ (0, p)
-        , (1, toPatCompatTc $ ListPat x ps)
+        , (1, toPatCompat $ ListPat x ps)
         ]
     -- Desugar tuples into an explicit constructor
     TuplePat tys pats boxity ->
diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs
index f8ef87eb18..4c278a6b9e 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs
@@ -211,7 +211,7 @@ filterBindingType
     -> TacticProvider
 filterBindingType p tp tpd =
   let jdg = tpd_jdg tpd
-      hy  = jHypothesis jdg
+      hy  = jLocalHypothesis jdg
       g   = jGoal jdg
    in fmap join $ for (unHypothesis hy) $ \hi ->
         let ty = unCType $ hi_type hi
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Simplify.hs b/plugins/hls-tactics-plugin/src/Wingman/Simplify.hs
index c21986cf51..cbd293715b 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Simplify.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Simplify.hs
@@ -11,7 +11,7 @@ import Development.IDE.GHC.Compat
 import GHC.SourceGen (var)
 import GHC.SourceGen.Expr (lambda)
 import Wingman.CodeGen.Utils
-import Wingman.GHC (containsHsVar, fromPatCompatPs)
+import Wingman.GHC (containsHsVar, fromPatCompat)
 
 
 ------------------------------------------------------------------------------
@@ -20,7 +20,7 @@ pattern Lambda :: [Pat GhcPs] -> HsExpr GhcPs -> HsExpr GhcPs
 pattern Lambda pats body <-
   HsLam _
     (MG {mg_alts = L _ [L _
-      (Match { m_pats = fmap fromPatCompatPs -> pats
+      (Match { m_pats = fmap fromPatCompat -> pats
              , m_grhss = GRHSs {grhssGRHSs = [L _ (
                  GRHS _ [] (L _ body))]}
              })]})
diff --git a/plugins/hls-tactics-plugin/test/ProviderSpec.hs b/plugins/hls-tactics-plugin/test/ProviderSpec.hs
index 0121c3078e..644a957bb3 100644
--- a/plugins/hls-tactics-plugin/test/ProviderSpec.hs
+++ b/plugins/hls-tactics-plugin/test/ProviderSpec.hs
@@ -52,3 +52,21 @@ spec = do
     [ (not, DestructLambdaCase, "")
     ]
 
+  mkTest
+    "Doesn't suggest destruct if already destructed"
+    "ProvideAlreadyDestructed.hs" 6 18
+    [ (not, Destruct, "x")
+    ]
+
+  mkTest
+    "...but does suggest destruct if destructed in a different branch"
+    "ProvideAlreadyDestructed.hs" 9 7
+    [ (id, Destruct, "x")
+    ]
+
+  mkTest
+    "Doesn't suggest destruct on class methods"
+    "ProvideLocalHyOnly.hs" 2 12
+    [ (not, Destruct, "mempty")
+    ]
+
diff --git a/plugins/hls-tactics-plugin/test/golden/ProvideAlreadyDestructed.hs b/plugins/hls-tactics-plugin/test/golden/ProvideAlreadyDestructed.hs
new file mode 100644
index 0000000000..2da53afbf5
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/ProvideAlreadyDestructed.hs
@@ -0,0 +1,9 @@
+foo :: Bool -> ()
+foo x =
+  if True
+    then
+      case x of
+        True  -> _
+        False -> ()
+    else
+      _
diff --git a/plugins/hls-tactics-plugin/test/golden/ProvideLocalHyOnly.hs b/plugins/hls-tactics-plugin/test/golden/ProvideLocalHyOnly.hs
new file mode 100644
index 0000000000..6a15b198dd
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/ProvideLocalHyOnly.hs
@@ -0,0 +1,2 @@
+basilisk :: Monoid Bool => a
+basilisk = _