From d73786c3b145ba572fc18cf3019ed657afcd89b5 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Sun, 11 Apr 2021 22:47:39 -0700
Subject: [PATCH 01/16] SYB improvemnets

---
 ghcide/src/Development/IDE/GHC/ExactPrint.hs  | 16 ++++++++--
 .../src/Wingman/Judgements/SYB.hs             | 31 +++++++++++++++++++
 .../src/Wingman/LanguageServer.hs             |  1 -
 3 files changed, 44 insertions(+), 4 deletions(-)
 create mode 100644 plugins/hls-tactics-plugin/src/Wingman/Judgements/SYB.hs

diff --git a/ghcide/src/Development/IDE/GHC/ExactPrint.hs b/ghcide/src/Development/IDE/GHC/ExactPrint.hs
index 13ec409ab0..6d80510692 100644
--- a/ghcide/src/Development/IDE/GHC/ExactPrint.hs
+++ b/ghcide/src/Development/IDE/GHC/ExactPrint.hs
@@ -302,8 +302,18 @@ genericIsSubspan ::
     Proxy (Located ast) ->
     SrcSpan ->
     GenericQ (Maybe Bool)
-genericIsSubspan _ dst = mkQ Nothing $ \case
-  (L span _ :: Located ast) -> Just $ dst `isSubspanOf` span
+genericIsSubspan _ dst =
+  (mkQ Nothing $ \case
+    (L span _ :: Located ast) -> Just $ dst `isSubspanOf` span
+  ) `ext1Q`
+  \case
+    -- If we're looking at a @Located e@ (anything that is not @Located ast@),
+    -- we can fail fast if we don't contain the span.
+    L span _ ->
+      if dst `isSubspanOf` span
+        then Nothing
+        else Just False
+
 
 -- | Run the given transformation only on the smallest node in the tree that
 -- contains the 'SrcSpan'.
@@ -337,7 +347,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/src/Wingman/Judgements/SYB.hs b/plugins/hls-tactics-plugin/src/Wingman/Judgements/SYB.hs
new file mode 100644
index 0000000000..0432471e71
--- /dev/null
+++ b/plugins/hls-tactics-plugin/src/Wingman/Judgements/SYB.hs
@@ -0,0 +1,31 @@
+{-# LANGUAGE RankNTypes #-}
+
+-- | Custom SYB traversals
+module Wingman.Judgements.SYB where
+
+import Data.Generics
+import Data.Foldable (foldl')
+import Development.IDE.GHC.Compat (SrcSpan, GenLocated (L), isSubspanOf)
+
+
+everythingWithin
+    :: forall r
+     . Monoid r
+    => SrcSpan
+    -> GenericQ r
+    -> GenericQ r
+everythingWithin dst f = go
+  where
+    go :: GenericQ r
+    go x =
+      case genericIsSubspan dst x of
+        Just False -> mempty
+        _ -> foldl' (<>) (f x) (gmapQ go x)
+
+
+genericIsSubspan
+    :: SrcSpan
+    -> GenericQ (Maybe Bool)
+genericIsSubspan dst =
+  empty `ext1Q` \case L span _ -> Just $ dst `isSubspanOf` span
+
diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
index d35dd89452..9168e0ea53 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
@@ -23,7 +23,6 @@ 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)

From 6ad89ce4e2a22493e7b9765e301324d13d216f09 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 12 Apr 2021 00:21:22 -0700
Subject: [PATCH 02/16] Case splits require a space when exactprinting

---
 ghcide/src/Development/IDE/GHC/ExactPrint.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/ghcide/src/Development/IDE/GHC/ExactPrint.hs b/ghcide/src/Development/IDE/GHC/ExactPrint.hs
index 6d80510692..b4667ade53 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)

From 0d1b1cca10a0756c6254e76227b682ebff009a96 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 12 Apr 2021 00:21:46 -0700
Subject: [PATCH 03/16] Add the new SYB module to cabal

---
 plugins/hls-tactics-plugin/hls-tactics-plugin.cabal | 1 +
 1 file changed, 1 insertion(+)

diff --git a/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal b/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal
index 8f0b11ec45..7d3b7b7d50 100644
--- a/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal
+++ b/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal
@@ -38,6 +38,7 @@ library
     Wingman.FeatureSet
     Wingman.GHC
     Wingman.Judgements
+    Wingman.Judgements.SYB
     Wingman.Judgements.Theta
     Wingman.KnownStrategies
     Wingman.KnownStrategies.QuickCheck

From 72a60444099d2cfac1c0ca100d71cd3a734a8266 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 12 Apr 2021 00:23:24 -0700
Subject: [PATCH 04/16] Use a typeclass for PatCompat

---
 .../src/Wingman/CaseSplit.hs                  |  2 +-
 plugins/hls-tactics-plugin/src/Wingman/GHC.hs | 39 +++++++++++++------
 2 files changed, 29 insertions(+), 12 deletions(-)

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/GHC.hs b/plugins/hls-tactics-plugin/src/Wingman/GHC.hs
index c8b198dc23..c24f718e8a 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
@@ -189,7 +189,7 @@ pattern AMatch :: HsMatchContext (NameOrRdrName (IdP GhcPs)) -> [Pat GhcPs] -> H
 pattern AMatch ctx pats body <-
   Match { m_ctxt = ctx
         , m_pats = fmap fromPatCompatPs -> pats
-        , m_grhss = UnguardedRHSs body
+        , 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
 
 
 ------------------------------------------------------------------------------
@@ -254,15 +251,35 @@ lambdaCaseable (splitFunTy_maybe -> Just (arg, res))
 lambdaCaseable _ = Nothing
 
 -- It's hard to generalize over these since weird type families are involved.
+class PatCompattable p where
+  fromPatCompat :: PatCompat p -> Pat p
+  toPatCompat :: Pat p -> PatCompat p
+
 fromPatCompatTc :: PatCompat GhcTc -> Pat GhcTc
 toPatCompatTc :: Pat GhcTc -> PatCompat GhcTc
 fromPatCompatPs :: PatCompat GhcPs -> Pat GhcPs
 #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

From ea058a357913e1bb51af319ae883275c0d146285 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 12 Apr 2021 00:24:02 -0700
Subject: [PATCH 05/16] Change the type of disallowing to use a Set

---
 plugins/hls-tactics-plugin/src/Wingman/Auto.hs       | 2 ++
 plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs    | 2 +-
 plugins/hls-tactics-plugin/src/Wingman/Judgements.hs | 8 ++++----
 3 files changed, 7 insertions(+), 5 deletions(-)

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/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/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

From 2299df9d328095f6f59e0412bdfb16af11a7367f Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 12 Apr 2021 00:24:14 -0700
Subject: [PATCH 06/16] SYB adds a stupid instance that crashes silently....

---
 plugins/hls-tactics-plugin/src/Wingman/Judgements/SYB.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/plugins/hls-tactics-plugin/src/Wingman/Judgements/SYB.hs b/plugins/hls-tactics-plugin/src/Wingman/Judgements/SYB.hs
index 0432471e71..f9bb908a88 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Judgements/SYB.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Judgements/SYB.hs
@@ -27,5 +27,5 @@ genericIsSubspan
     :: SrcSpan
     -> GenericQ (Maybe Bool)
 genericIsSubspan dst =
-  empty `ext1Q` \case L span _ -> Just $ dst `isSubspanOf` span
+  const empty `ext1Q` \case L span _ -> Just $ dst `isSubspanOf` span
 

From 4b88aac14b97b56941be473c13983b1affcf22f5 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 12 Apr 2021 00:24:43 -0700
Subject: [PATCH 07/16] Notify the judgment about already-destructed terms

---
 .../src/Wingman/LanguageServer.hs             | 23 ++++++++++++++++---
 1 file changed, 20 insertions(+), 3 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
index 9168e0ea53..eab24f99bc 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
@@ -18,7 +18,8 @@ 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)
@@ -51,6 +52,7 @@ import           Wingman.Context
 import           Wingman.FeatureSet
 import           Wingman.GHC
 import           Wingman.Judgements
+import           Wingman.Judgements.SYB (everythingWithin)
 import           Wingman.Judgements.Theta
 import           Wingman.Range
 import           Wingman.Types
@@ -220,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
@@ -234,6 +238,19 @@ mkJudgementAndContext features g (TrackedStale binds bmap) rss (TrackedStale tcg
     )
 
 
+getAlreadyDestructed
+    :: Tracked age SrcSpan
+    -> Tracked age (LHsBinds GhcTc)
+    -> Set OccName
+getAlreadyDestructed (unTrack -> span) (unTrack -> binds) =
+  everythingWithin span
+    (mkQ mempty $ \case
+      Case (HsVar _ (L _ (occName -> var))) _ ->
+        S.singleton var
+      (_ :: HsExpr GhcTc) -> mempty
+    ) binds
+
+
 getSpanAndTypeAtHole
     :: Tracked age Range
     -> Tracked age (HieASTs b)

From 30d385a011013033f4f1467073544792e2c0639a Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 12 Apr 2021 00:27:10 -0700
Subject: [PATCH 08/16] Remove specialized to/from patcompat

---
 plugins/hls-tactics-plugin/src/Wingman/GHC.hs         | 11 +----------
 .../hls-tactics-plugin/src/Wingman/LanguageServer.hs  |  4 ++--
 plugins/hls-tactics-plugin/src/Wingman/Simplify.hs    |  4 ++--
 3 files changed, 5 insertions(+), 14 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Wingman/GHC.hs b/plugins/hls-tactics-plugin/src/Wingman/GHC.hs
index c24f718e8a..ebc21371c8 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/GHC.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/GHC.hs
@@ -188,7 +188,7 @@ 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_pats = fmap fromPatCompat -> pats
         , m_grhss = UnguardedRHSs (unLoc -> body)
         }
 
@@ -255,9 +255,6 @@ class PatCompattable p where
   fromPatCompat :: PatCompat p -> Pat p
   toPatCompat :: Pat p -> PatCompat p
 
-fromPatCompatTc :: PatCompat GhcTc -> Pat GhcTc
-toPatCompatTc :: Pat GhcTc -> PatCompat GhcTc
-fromPatCompatPs :: PatCompat GhcPs -> Pat GhcPs
 #if __GLASGOW_HASKELL__ == 808
 instance PatCompattable GhcTc where
   fromPatCompat = id
@@ -268,9 +265,6 @@ instance PatCompattable GhcPs where
   toPatCompat = id
 
 type PatCompat pass = Pat pass
-fromPatCompatTc = id
-fromPatCompatPs = id
-toPatCompatTc = id
 #else
 instance PatCompattable GhcTc where
   fromPatCompat = unLoc
@@ -281,9 +275,6 @@ instance PatCompattable GhcPs where
   toPatCompat = noLoc
 
 type PatCompat pass = LPat pass
-fromPatCompatTc = unLoc
-fromPatCompatPs = unLoc
-toPatCompatTc = noLoc
 #endif
 
 ------------------------------------------------------------------------------
diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
index eab24f99bc..a9f97ee7e9 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
@@ -318,7 +318,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
@@ -333,7 +333,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/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))]}
              })]})

From da924fbba6b9688e303fcc757e88a80bed0a569b Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 12 Apr 2021 00:31:19 -0700
Subject: [PATCH 09/16] Only allow destructing the local hypothesis

---
 .../src/Wingman/LanguageServer/TacticProviders.hs               | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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

From 0a95bc47a4ae4bf6b4251f51ed663870170fdce8 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 12 Apr 2021 00:59:27 -0700
Subject: [PATCH 10/16] ext1Q doesn't do universal quantification SAD

---
 plugins/hls-tactics-plugin/src/Wingman/Judgements/SYB.hs | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Wingman/Judgements/SYB.hs b/plugins/hls-tactics-plugin/src/Wingman/Judgements/SYB.hs
index f9bb908a88..494b801132 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Judgements/SYB.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Judgements/SYB.hs
@@ -5,7 +5,7 @@ module Wingman.Judgements.SYB where
 
 import Data.Generics
 import Data.Foldable (foldl')
-import Development.IDE.GHC.Compat (SrcSpan, GenLocated (L), isSubspanOf)
+import Development.IDE.GHC.Compat
 
 
 everythingWithin
@@ -26,6 +26,6 @@ everythingWithin dst f = go
 genericIsSubspan
     :: SrcSpan
     -> GenericQ (Maybe Bool)
-genericIsSubspan dst =
-  const empty `ext1Q` \case L span _ -> Just $ dst `isSubspanOf` span
+genericIsSubspan dst = mkQ Nothing $ \case
+  (L span _ :: LHsExpr GhcTc) -> Just $ dst `isSubspanOf` span
 

From f1a0cec9f2878976f119ed224699845e703fa811 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 12 Apr 2021 01:00:02 -0700
Subject: [PATCH 11/16] Add new provider tests

---
 .../hls-tactics-plugin/test/ProviderSpec.hs    | 18 ++++++++++++++++++
 .../test/golden/ProvideAlreadyDestructed.hs    |  9 +++++++++
 .../test/golden/ProvideLocalHyOnly.hs          |  2 ++
 3 files changed, 29 insertions(+)
 create mode 100644 plugins/hls-tactics-plugin/test/golden/ProvideAlreadyDestructed.hs
 create mode 100644 plugins/hls-tactics-plugin/test/golden/ProvideLocalHyOnly.hs

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 = _

From c7dfcf6ccc470a8c8853bd0481611fa3a4b5ce1a Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 12 Apr 2021 01:02:16 -0700
Subject: [PATCH 12/16] Revert changes to ExactPrint that didn't help

---
 ghcide/src/Development/IDE/GHC/ExactPrint.hs | 14 ++------------
 1 file changed, 2 insertions(+), 12 deletions(-)

diff --git a/ghcide/src/Development/IDE/GHC/ExactPrint.hs b/ghcide/src/Development/IDE/GHC/ExactPrint.hs
index b4667ade53..4e494eb82d 100644
--- a/ghcide/src/Development/IDE/GHC/ExactPrint.hs
+++ b/ghcide/src/Development/IDE/GHC/ExactPrint.hs
@@ -302,18 +302,8 @@ genericIsSubspan ::
     Proxy (Located ast) ->
     SrcSpan ->
     GenericQ (Maybe Bool)
-genericIsSubspan _ dst =
-  (mkQ Nothing $ \case
-    (L span _ :: Located ast) -> Just $ dst `isSubspanOf` span
-  ) `ext1Q`
-  \case
-    -- If we're looking at a @Located e@ (anything that is not @Located ast@),
-    -- we can fail fast if we don't contain the span.
-    L span _ ->
-      if dst `isSubspanOf` span
-        then Nothing
-        else Just False
-
+genericIsSubspan _ dst = mkQ Nothing $ \case
+  (L span _ :: Located ast) -> Just $ dst `isSubspanOf` span
 
 -- | Run the given transformation only on the smallest node in the tree that
 -- contains the 'SrcSpan'.

From 155a7fd1d62cd76beb9594aedc88b0c1d07ad138 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 12 Apr 2021 01:06:24 -0700
Subject: [PATCH 13/16] Tidy and haddock

---
 plugins/hls-tactics-plugin/src/Wingman/GHC.hs            | 1 -
 plugins/hls-tactics-plugin/src/Wingman/Judgements/SYB.hs | 9 +++++++++
 plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs | 3 +++
 3 files changed, 12 insertions(+), 1 deletion(-)

diff --git a/plugins/hls-tactics-plugin/src/Wingman/GHC.hs b/plugins/hls-tactics-plugin/src/Wingman/GHC.hs
index ebc21371c8..c77d183ceb 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/GHC.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/GHC.hs
@@ -250,7 +250,6 @@ 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.
 class PatCompattable p where
   fromPatCompat :: PatCompat p -> Pat p
   toPatCompat :: Pat p -> PatCompat p
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Judgements/SYB.hs b/plugins/hls-tactics-plugin/src/Wingman/Judgements/SYB.hs
index 494b801132..39863cf6a4 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Judgements/SYB.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Judgements/SYB.hs
@@ -8,6 +8,8 @@ import Data.Foldable (foldl')
 import Development.IDE.GHC.Compat
 
 
+------------------------------------------------------------------------------
+-- | Like 'everything', but only looks inside of the given 'SrcSpan'.
 everythingWithin
     :: forall r
      . Monoid r
@@ -23,6 +25,13 @@ everythingWithin dst f = go
         _ -> 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)
diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
index a9f97ee7e9..4bcbd61d2f 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
@@ -238,6 +238,9 @@ 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)

From b599fca0cb8aefc190d5cc9d5fd77871a98434fb Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 12 Apr 2021 02:17:41 -0700
Subject: [PATCH 14/16] Polymorphic SrcSpan-aware mkQ SYB traversal

---
 .../src/Wingman/Judgements/SYB.hs             | 46 +++++++++++++++++--
 1 file changed, 42 insertions(+), 4 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Wingman/Judgements/SYB.hs b/plugins/hls-tactics-plugin/src/Wingman/Judgements/SYB.hs
index 39863cf6a4..ed9cf15e8a 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Judgements/SYB.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Judgements/SYB.hs
@@ -1,11 +1,15 @@
-{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE RankNTypes          #-}
 
 -- | Custom SYB traversals
 module Wingman.Judgements.SYB where
 
-import Data.Generics
 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)
 
 
 ------------------------------------------------------------------------------
@@ -35,6 +39,40 @@ everythingWithin dst f = go
 genericIsSubspan
     :: SrcSpan
     -> GenericQ (Maybe Bool)
-genericIsSubspan dst = mkQ Nothing $ \case
-  (L span _ :: LHsExpr GhcTc) -> Just $ dst `isSubspanOf` span
+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
+      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
 

From ed426edcf1547e3c729ebe8c1ff26fe61a8dfe60 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 12 Apr 2021 02:22:01 -0700
Subject: [PATCH 15/16] Add a note on why unsafeCoerce is safe

---
 plugins/hls-tactics-plugin/src/Wingman/Judgements/SYB.hs | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/plugins/hls-tactics-plugin/src/Wingman/Judgements/SYB.hs b/plugins/hls-tactics-plugin/src/Wingman/Judgements/SYB.hs
index ed9cf15e8a..46e44f4fca 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Judgements/SYB.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Judgements/SYB.hs
@@ -56,6 +56,10 @@ mkQ1 :: forall a r f
      -> 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

From 867133520794bb5636e4e29424e36b63af3432c8 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 12 Apr 2021 02:24:10 -0700
Subject: [PATCH 16/16] Fix a terrible name

---
 plugins/hls-tactics-plugin/src/Wingman/Judgements/SYB.hs | 7 ++++---
 plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs | 4 ++--
 2 files changed, 6 insertions(+), 5 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Wingman/Judgements/SYB.hs b/plugins/hls-tactics-plugin/src/Wingman/Judgements/SYB.hs
index 46e44f4fca..c1b5fe63c6 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Judgements/SYB.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Judgements/SYB.hs
@@ -13,14 +13,15 @@ import Unsafe.Coerce (unsafeCoerce)
 
 
 ------------------------------------------------------------------------------
--- | Like 'everything', but only looks inside of the given 'SrcSpan'.
-everythingWithin
+-- | Like 'everything', but only looks inside 'Located' terms that contain the
+-- given 'SrcSpan'.
+everythingContaining
     :: forall r
      . Monoid r
     => SrcSpan
     -> GenericQ r
     -> GenericQ r
-everythingWithin dst f = go
+everythingContaining dst f = go
   where
     go :: GenericQ r
     go x =
diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
index 4bcbd61d2f..64d33f9d6a 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
@@ -52,7 +52,7 @@ import           Wingman.Context
 import           Wingman.FeatureSet
 import           Wingman.GHC
 import           Wingman.Judgements
-import           Wingman.Judgements.SYB (everythingWithin)
+import           Wingman.Judgements.SYB (everythingContaining)
 import           Wingman.Judgements.Theta
 import           Wingman.Range
 import           Wingman.Types
@@ -246,7 +246,7 @@ getAlreadyDestructed
     -> Tracked age (LHsBinds GhcTc)
     -> Set OccName
 getAlreadyDestructed (unTrack -> span) (unTrack -> binds) =
-  everythingWithin span
+  everythingContaining span
     (mkQ mempty $ \case
       Case (HsVar _ (L _ (occName -> var))) _ ->
         S.singleton var