From 6733246ba03463169ddb0c1d11c9d7bcff416f36 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 12 Apr 2021 11:52:27 -0700
Subject: [PATCH 01/31] Add typechecking machinery

---
 plugins/hls-tactics-plugin/src/Wingman/GHC.hs | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/plugins/hls-tactics-plugin/src/Wingman/GHC.hs b/plugins/hls-tactics-plugin/src/Wingman/GHC.hs
index c77d183ceb..f4939fbf0b 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/GHC.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/GHC.hs
@@ -7,6 +7,7 @@ import           ConLike
 import           Control.Applicative (empty)
 import           Control.Monad.State
 import           Control.Monad.Trans.Maybe (MaybeT(..))
+import           CoreUtils (exprType)
 import           Data.Function (on)
 import           Data.Functor ((<&>))
 import           Data.List (isPrefixOf)
@@ -18,7 +19,9 @@ import           Data.Traversable
 import           DataCon
 import           Development.IDE (HscEnvEq (hscEnv))
 import           Development.IDE.Core.Compile (lookupName)
-import           Development.IDE.GHC.Compat
+import           Development.IDE.GHC.Compat hiding (exprType)
+import           DsExpr (dsExpr)
+import           DsMonad (initDs)
 import           GHC.SourceGen (lambda)
 import           Generics.SYB (Data, everything, everywhere, listify, mkQ, mkT)
 import           GhcPlugins (extractModule, GlobalRdrElt (gre_name))
@@ -344,3 +347,7 @@ knownThing f tcg hscenv occ = do
 liftMaybe :: Monad m => Maybe a -> MaybeT m a
 liftMaybe a = MaybeT $ pure a
 
+
+typeCheck :: HscEnv -> TcGblEnv -> HsExpr GhcTc -> IO (Maybe Type)
+typeCheck hscenv tcg = fmap snd . initDs hscenv tcg . fmap exprType . dsExpr
+

From 9f91fb4493c464b8b83e8fd90e576412a7f9f4ec Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 12 Apr 2021 11:53:29 -0700
Subject: [PATCH 02/31] Add smallestQ SYB traversal

---
 .../src/Wingman/Judgements/SYB.hs             | 36 +++++++++++++++----
 1 file changed, 30 insertions(+), 6 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Wingman/Judgements/SYB.hs b/plugins/hls-tactics-plugin/src/Wingman/Judgements/SYB.hs
index c1b5fe63c6..2e318eae17 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Judgements/SYB.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Judgements/SYB.hs
@@ -4,12 +4,14 @@
 -- | 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)
+import           Data.Bool (bool)
+import           Data.Foldable (foldl')
+import           Data.Generics hiding (typeRep)
+import qualified Data.Monoid as M
+import           Development.IDE.GHC.Compat
+import           GHC.Exts (Any)
+import           Type.Reflection
+import           Unsafe.Coerce (unsafeCoerce)
 
 
 ------------------------------------------------------------------------------
@@ -44,6 +46,28 @@ genericIsSubspan dst = mkQ1 (L noSrcSpan ()) Nothing $ \case
   L span _ -> Just $ dst `isSubspanOf` span
 
 
+genericDefinitelyNotIsSubspan
+    :: SrcSpan
+    -> GenericQ (Maybe Bool)
+genericDefinitelyNotIsSubspan dst = mkQ1 (L noSrcSpan ()) Nothing $ \case
+  L span _ -> bool (Just False) Nothing $ dst `isSubspanOf` span
+
+
+smallestQ :: forall r. Monoid r => GenericQ (Maybe Bool) -> GenericQ r -> GenericQ r
+smallestQ q f = snd . go
+  where
+    go :: GenericQ (M.Any, r)
+    go x = do
+      case q x of
+        Nothing -> mconcat $ gmapQ go x
+        Just True ->
+          let it@(r, x') = mconcat $ gmapQ go x
+           in case r of
+                M.Any True -> it
+                M.Any False -> (M.Any True, x' <> f x)
+        Just False -> mempty
+
+
 ------------------------------------------------------------------------------
 -- | Like 'mkQ', but allows for polymorphic instantiation of its specific case.
 -- This instantation matches whenever the dynamic value has the same

From f6888880a73673a8d98d70d49850c4ed49ed4adb Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 12 Apr 2021 11:54:15 -0700
Subject: [PATCH 03/31] emptyCaseQ to find an empty case

---
 .../src/Wingman/LanguageServer.hs               | 17 +++++++++++++++--
 1 file changed, 15 insertions(+), 2 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
index 64d33f9d6a..b91cda4a72 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
@@ -1,5 +1,6 @@
 {-# LANGUAGE CPP               #-}
 {-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE RankNTypes        #-}
 {-# LANGUAGE TypeFamilies      #-}
 
 module Wingman.LanguageServer where
@@ -11,7 +12,7 @@ import           Control.Monad.State (State, get, put, evalState)
 import           Control.Monad.Trans.Maybe
 import           Data.Coerce
 import           Data.Functor ((<&>))
-import           Data.Generics.Aliases (mkQ)
+import           Data.Generics.Aliases (mkQ, GenericQ, extQ)
 import           Data.Generics.Schemes (everything)
 import qualified Data.HashMap.Strict as Map
 import           Data.IORef (readIORef)
@@ -52,7 +53,7 @@ import           Wingman.Context
 import           Wingman.FeatureSet
 import           Wingman.GHC
 import           Wingman.Judgements
-import           Wingman.Judgements.SYB (everythingContaining)
+import           Wingman.Judgements.SYB (everythingContaining, smallestQ, genericDefinitelyNotIsSubspan)
 import           Wingman.Judgements.Theta
 import           Wingman.Range
 import           Wingman.Types
@@ -199,6 +200,18 @@ judgementForHole state nfp range features = do
       pure (fmap realSrcSpanToRange new_rss, jdg, ctx, dflags)
 
 
+
+emptyCaseQ :: SrcSpan -> GenericQ (First (SrcSpan, HsExpr GhcTc))
+emptyCaseQ span =
+  smallestQ
+    (genericDefinitelyNotIsSubspan span `extQ` \case
+      (L _ (Case _ _)) -> Just True
+      (_ :: LHsExpr GhcTc) -> Nothing
+    ) $ mkQ mempty $ \case
+          L new_span (Case scrutinee []) -> pure (new_span, scrutinee)
+          (_ :: LHsExpr GhcTc) -> mempty
+
+
 mkJudgementAndContext
     :: FeatureSet
     -> Type

From 6bbd7c155cd5c204f4c82b6b3fc6c859fa71d93a Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 12 Apr 2021 11:54:54 -0700
Subject: [PATCH 04/31] Get scrutinee and its type if hovering over an empty
 case split

---
 .../src/Wingman/LanguageServer.hs                | 16 ++++++++++++++++
 plugins/hls-tactics-plugin/src/Wingman/Types.hs  |  3 +++
 2 files changed, 19 insertions(+)

diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
index b91cda4a72..1349f4c5e3 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
@@ -185,6 +185,11 @@ judgementForHole state nfp range features = do
            $ runStaleIde state nfp TypeCheck
       hscenv <- runStaleIde state nfp GhcSessionDeps
 
+      rss2 <- liftMaybe $ getSpanAtCursor range' hf
+      (new_span, scrutinee) <- liftMaybe $ getFirst $
+        emptyCaseQ (RealSrcSpan $ unTrack rss2) $ tcg_binds $ untrackedStaleValue tcg
+      x <- MaybeT $ typeCheck (hscEnv $ untrackedStaleValue hscenv) (untrackedStaleValue tcg) scrutinee
+
       (rss, g) <- liftMaybe $ getSpanAndTypeAtHole range' hf
       new_rss <- liftMaybe $ mapAgeTo amapping rss
 
@@ -267,6 +272,17 @@ getAlreadyDestructed (unTrack -> span) (unTrack -> binds) =
     ) binds
 
 
+getSpanAtCursor
+    :: Tracked age Range
+    -> Tracked age (HieASTs b)
+    -> Maybe (Tracked age RealSrcSpan)
+getSpanAtCursor r@(unTrack -> range) (unTrack -> hf) = do
+  join $ listToMaybe $ M.elems $ flip M.mapWithKey (getAsts hf) $ \fs ast ->
+    case selectSmallestContaining (rangeToRealSrcSpan (FastString.unpackFS fs) range) ast of
+      Nothing -> Nothing
+      Just ast' -> do
+        pure $ unsafeCopyAge r $ nodeSpan ast'
+
 getSpanAndTypeAtHole
     :: Tracked age Range
     -> Tracked age (HieASTs b)
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Types.hs b/plugins/hls-tactics-plugin/src/Wingman/Types.hs
index bb38c15d3a..64e7f5e00e 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Types.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Types.hs
@@ -117,6 +117,9 @@ instance Show Class where
 instance Show (HsExpr GhcPs) where
   show  = unsafeRender
 
+instance Show (HsExpr GhcTc) where
+  show  = unsafeRender
+
 instance Show (HsDecl GhcPs) where
   show  = unsafeRender
 

From a0a669ebf773c0f32c31e2610eb418ed0eacaae4 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 12 Apr 2021 13:04:52 -0700
Subject: [PATCH 05/31] Allow ghcide to operate on emptycase

---
 ghcide/session-loader/Development/IDE/Session.hs | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/ghcide/session-loader/Development/IDE/Session.hs b/ghcide/session-loader/Development/IDE/Session.hs
index 0b9386ec70..91f0428788 100644
--- a/ghcide/session-loader/Development/IDE/Session.hs
+++ b/ghcide/session-loader/Development/IDE/Session.hs
@@ -90,6 +90,7 @@ import           HieDb.Create
 import           HieDb.Types
 import           HieDb.Utils
 import           Maybes                               (MaybeT (runMaybeT))
+import           GHC.LanguageExtensions               (Extension(EmptyCase))
 
 -- | Bump this version number when making changes to the format of the data stored in hiedb
 hiedbDataVersion :: String
@@ -771,6 +772,7 @@ setOptions (ComponentOptions theOpts compRoot _) dflags = do
           setIgnoreInterfacePragmas $
           setLinkerOptions $
           disableOptimisation $
+          allowEmptyCaseButWithWarning $
           setUpTypedHoles $
           makeDynFlagsAbsolute compRoot dflags'
     -- initPackages parses the -package flags and
@@ -780,6 +782,14 @@ setOptions (ComponentOptions theOpts compRoot _) dflags = do
     return (final_df, targets)
 
 
+-- | Wingman wants to support destructing of empty cases, but these are a parse
+-- error by default. So we want to enable 'EmptyCase', but then that leads to
+-- silent errors without 'Opt_WarnIncompletePatterns'.
+allowEmptyCaseButWithWarning :: DynFlags -> DynFlags
+allowEmptyCaseButWithWarning =
+  flip xopt_set EmptyCase . flip wopt_set Opt_WarnIncompletePatterns
+
+
 -- we don't want to generate object code so we compile to bytecode
 -- (HscInterpreted) which implies LinkInMemory
 -- HscInterpreted

From f2378f452e395b7ad3f94483fe3462fa02b97e41 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 12 Apr 2021 13:05:16 -0700
Subject: [PATCH 06/31] [wip] not working, but most of the pieces are here

---
 .../hls-tactics-plugin/src/Wingman/CodeGen.hs |  9 +++
 .../src/Wingman/LanguageServer.hs             | 63 ++++++++++++-------
 .../Wingman/LanguageServer/TacticProviders.hs | 42 ++++++++-----
 .../src/Wingman/Machinery.hs                  |  2 +
 .../hls-tactics-plugin/src/Wingman/Plugin.hs  | 14 ++++-
 .../hls-tactics-plugin/src/Wingman/Types.hs   |  6 ++
 6 files changed, 94 insertions(+), 42 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs b/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs
index 528a2056f8..70ce62fc15 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs
@@ -167,6 +167,15 @@ destruct' f hi jdg = do
     & #syn_val       %~ noLoc . case' (var' term)
 
 
+destructExpr :: (ConLike -> Judgement -> Rule) -> HsExpr GhcPs -> Type -> Judgement -> Rule
+destructExpr f term ty jdg = do
+  ext
+      <- destructMatches f Nothing (CType ty) jdg
+  pure $ ext
+    & #syn_trace     %~ rose ("destruct " <> show term) . pure
+    & #syn_val       %~ noLoc . case' term
+
+
 ------------------------------------------------------------------------------
 -- | Combinator for performign case splitting, and running sub-rules on the
 -- resulting matches.
diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
index 1349f4c5e3..6e35605bdf 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
@@ -57,6 +57,7 @@ import           Wingman.Judgements.SYB (everythingContaining, smallestQ, generi
 import           Wingman.Judgements.Theta
 import           Wingman.Range
 import           Wingman.Types
+import Control.Applicative (empty)
 
 
 tacticDesc :: T.Text -> T.Text
@@ -165,6 +166,11 @@ getIdeDynflags state nfp = do
   pure $ ms_hspp_opts $ msrModSummary msr
 
 
+data GoalOrScrutinee
+  = Goal Type
+  | Scrutinee (HsExpr GhcPs) Type
+
+
 ------------------------------------------------------------------------------
 -- | Find the last typechecked module, and find the most specific span, as well
 -- as the judgement at the given range.
@@ -173,7 +179,7 @@ judgementForHole
     -> NormalizedFilePath
     -> Tracked 'Current Range
     -> FeatureSet
-    -> MaybeT IO (Tracked 'Current Range, Judgement, Context, DynFlags)
+    -> MaybeT IO (Tracked 'Current Range, Hook (), Context, DynFlags)
 judgementForHole state nfp range features = do
   TrackedStale asts amapping  <- runStaleIde state nfp GetHieAst
   case unTrack asts of
@@ -185,24 +191,30 @@ judgementForHole state nfp range features = do
            $ runStaleIde state nfp TypeCheck
       hscenv <- runStaleIde state nfp GhcSessionDeps
 
-      rss2 <- liftMaybe $ getSpanAtCursor range' hf
-      (new_span, scrutinee) <- liftMaybe $ getFirst $
-        emptyCaseQ (RealSrcSpan $ unTrack rss2) $ tcg_binds $ untrackedStaleValue tcg
-      x <- MaybeT $ typeCheck (hscEnv $ untrackedStaleValue hscenv) (untrackedStaleValue tcg) scrutinee
-
-      (rss, g) <- liftMaybe $ getSpanAndTypeAtHole range' hf
-      new_rss <- liftMaybe $ mapAgeTo amapping rss
-
       -- KnownThings is just the instances in scope. There are no ranges
       -- involved, so it's not crucial to track ages.
-      let henv = untrackedStaleValue $ hscenv
+      let henv = untrackedStaleValue hscenv
+          untracked_tcg = untrackedStaleValue tcg
       eps <- liftIO $ readIORef $ hsc_EPS $ hscEnv henv
-      kt <- knownThings (untrackedStaleValue tcg) henv
+      kt <- knownThings untracked_tcg henv
+
+      (rss, g_or_s) <-
+        case getSpanAndTypeAtHole range' hf of
+          Just (rss, g) -> pure (rss, Goal g)
+          Nothing -> do
+            rss2 <- liftMaybe $ getSpanAtCursor range' hf
+            (new_span, scrutinee) <- liftMaybe $ getFirst $
+              emptyCaseQ (RealSrcSpan $ unTrack rss2) $ tcg_binds untracked_tcg
+            ty <- MaybeT $ typeCheck (hscEnv henv) untracked_tcg scrutinee
+            case new_span of
+              RealSrcSpan rss -> pure (pure rss, Scrutinee scrutinee ty)
+              UnhelpfulSpan _ -> empty
 
-      (jdg, ctx) <- liftMaybe $ mkJudgementAndContext features g binds new_rss tcg eps kt
+      new_rss <- liftMaybe $ mapAgeTo amapping rss
+      (hook, ctx) <- liftMaybe $ mkJudgementAndContext features g_or_s binds new_rss tcg eps kt
 
       dflags <- getIdeDynflags state nfp
-      pure (fmap realSrcSpanToRange new_rss, jdg, ctx, dflags)
+      pure (fmap realSrcSpanToRange new_rss, hook, ctx, dflags)
 
 
 
@@ -219,14 +231,14 @@ emptyCaseQ span =
 
 mkJudgementAndContext
     :: FeatureSet
-    -> Type
+    -> GoalOrScrutinee
     -> TrackedStale Bindings
     -> Tracked 'Current RealSrcSpan
     -> TrackedStale TcGblEnv
     -> ExternalPackageState
     -> KnownThings
-    -> Maybe (Judgement, Context)
-mkJudgementAndContext features g (TrackedStale binds bmap) rss (TrackedStale tcg tcgmap) eps kt = do
+    -> Maybe (Hook (), Context)
+mkJudgementAndContext features g_or_s (TrackedStale binds bmap) rss (TrackedStale tcg tcgmap) eps kt = do
   binds_rss <- mapAgeFrom bmap rss
   tcg_rss <- mapAgeFrom tcgmap rss
 
@@ -246,14 +258,19 @@ mkJudgementAndContext features g (TrackedStale binds bmap) rss (TrackedStale tcg
       evidence = getEvidenceAtHole (fmap RealSrcSpan tcg_rss) tcs
       cls_hy = foldMap evidenceToHypothesis evidence
       subst = ts_unifier $ appEndo (foldMap (Endo . evidenceToSubst) evidence) defaultTacticState
+
   pure $
-    ( disallowing AlreadyDestructed already_destructed
-    $ fmap (CType . substTyAddInScope subst . unCType) $ mkFirstJudgement
-          (local_hy <> cls_hy)
-          (isRhsHole tcg_rss tcs)
-          g
-    , ctx
-    )
+    case g_or_s of
+      Goal g ->
+        ( Tactic ()
+        $ disallowing AlreadyDestructed already_destructed
+        $ fmap (CType . substTyAddInScope subst . unCType) $ mkFirstJudgement
+              (local_hy <> cls_hy)
+              (isRhsHole tcg_rss tcs)
+              g
+        , ctx
+        )
+      Scrutinee scrutinee ty -> (EmptyCase scrutinee ty, ctx)
 
 
 ------------------------------------------------------------------------------
diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs
index 4c278a6b9e..4bb84cae8a 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs
@@ -152,7 +152,7 @@ data TacticProviderData = TacticProviderData
   , tpd_plid   :: PluginId
   , tpd_uri    :: Uri
   , tpd_range  :: Tracked 'Current Range
-  , tpd_jdg    :: Judgement
+  , tpd_hook   :: Hook ()
   }
 
 
@@ -189,17 +189,21 @@ requireExtension ext tp tpd =
 -- | Restrict a 'TacticProvider', making sure it appears only when the given
 -- predicate holds for the goal.
 filterGoalType :: (Type -> Bool) -> TacticProvider -> TacticProvider
-filterGoalType p tp tpd =
-  case p $ unCType $ jGoal $ tpd_jdg tpd of
-    True  -> tp tpd
-    False -> pure []
+filterGoalType p tp =
+  withJudgement $ \jdg ->
+    case p $ unCType $ jGoal jdg of
+      True  -> tp
+      False -> mempty
 
 
 ------------------------------------------------------------------------------
 -- | Restrict a 'TacticProvider', making sure it appears only when the given
 -- predicate holds for the goal.
 withJudgement :: (Judgement -> TacticProvider) -> TacticProvider
-withJudgement tp tpd = tp (tpd_jdg tpd) tpd
+withJudgement tp tpd =
+  case tpd_hook tpd of
+    Tactic _ jdg -> tp jdg tpd
+    _ -> pure []
 
 
 ------------------------------------------------------------------------------
@@ -210,14 +214,16 @@ filterBindingType
     -> (OccName -> Type -> TacticProvider)
     -> TacticProvider
 filterBindingType p tp tpd =
-  let jdg = tpd_jdg tpd
-      hy  = jLocalHypothesis jdg
-      g   = jGoal jdg
-   in fmap join $ for (unHypothesis hy) $ \hi ->
-        let ty = unCType $ hi_type hi
-         in case p (unCType g) ty of
-              True  -> tp (hi_name hi) ty tpd
-              False -> pure []
+  case tpd_hook tpd of
+    Tactic _ jdg ->
+      let hy  = jLocalHypothesis jdg
+          g   = jGoal jdg
+      in fmap join $ for (unHypothesis hy) $ \hi ->
+            let ty = unCType $ hi_type hi
+            in case p (unCType g) ty of
+                  True  -> tp (hi_name hi) ty tpd
+                  False -> pure []
+    _ -> mempty
 
 
 ------------------------------------------------------------------------------
@@ -228,9 +234,11 @@ filterTypeProjection
     -> (a -> TacticProvider)
     -> TacticProvider
 filterTypeProjection p tp tpd =
-  fmap join $ for (p $ unCType $ jGoal $ tpd_jdg tpd) $ \a ->
-      tp a tpd
-
+  case tpd_hook tpd of
+    Tactic _ jdg ->
+      fmap join $ for (p $ unCType $ jGoal jdg) $ \a ->
+          tp a tpd
+    _ -> mempty
 
 ------------------------------------------------------------------------------
 -- | Get access to the 'Config' when building a 'TacticProvider'.
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs b/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs
index 34dcb449c6..9cd9f6e3cd 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs
@@ -33,6 +33,7 @@ import           Unify
 import           Wingman.Judgements
 import           Wingman.Simplify (simplify)
 import           Wingman.Types
+import GhcPlugins (unitTy)
 
 
 substCTy :: TCvSubst -> CType -> CType
@@ -52,6 +53,7 @@ newSubgoal j = do
       $ unsetIsTopHole j
 
 
+
 ------------------------------------------------------------------------------
 -- | Attempt to generate a term of the right type using in-scope bindings, and
 -- a given tactic.
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs b/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs
index ec38683a4c..d51cb0d83c 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs
@@ -36,6 +36,8 @@ import           Wingman.Machinery (scoreSolution)
 import           Wingman.Range
 import           Wingman.Tactics
 import           Wingman.Types
+import GhcPlugins (unitTy)
+import Wingman.Judgements (mkFirstJudgement)
 
 
 descriptor :: PluginId -> PluginDescriptor IdeState
@@ -60,7 +62,7 @@ codeActionProvider state plId (CodeActionParams _ _ (TextDocumentIdentifier uri)
   | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do
       cfg <- getTacticConfig plId
       liftIO $ fromMaybeT (Right $ List []) $ do
-        (_, jdg, _, dflags) <- judgementForHole state nfp range $ cfg_feature_set cfg
+        (_, hook, _, dflags) <- judgementForHole state nfp range $ cfg_feature_set cfg
         actions <- lift $
           -- This foldMap is over the function monoid.
           foldMap commandProvider [minBound .. maxBound] $ TacticProviderData
@@ -69,7 +71,7 @@ codeActionProvider state plId (CodeActionParams _ _ (TextDocumentIdentifier uri)
             , tpd_plid   = plId
             , tpd_uri    = uri
             , tpd_range  = range
-            , tpd_jdg    = jdg
+            , tpd_hook   = hook
             }
         pure $ Right $ List actions
 codeActionProvider _ _ _ = pure $ Right $ List []
@@ -214,3 +216,11 @@ graftDecl _ _ _ _ x = pure $ pure x
 fromMaybeT :: Functor m => a -> MaybeT m a -> m a
 fromMaybeT def = fmap (fromMaybe def) . runMaybeT
 
+
+runHook
+    :: Context
+    -> Hook (TacticsM ())
+    -> Either [TacticError] RunTacticResults
+runHook ctx (Tactic t jdg) = runTactic ctx jdg t
+runHook ctx (EmptyCase ty) = runTactic ctx (mkFirstJudgement mempty False unitTy) _
+
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Types.hs b/plugins/hls-tactics-plugin/src/Wingman/Types.hs
index 64e7f5e00e..0a6532c0e8 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Types.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Types.hs
@@ -490,3 +490,9 @@ instance Show UserFacingMessage where
   show NothingToDo             = "Nothing to do"
   show (InfrastructureError t) = "Internal error: " <> T.unpack t
 
+
+data Hook a
+  = Tactic a Judgement
+  | EmptyCase (HsExpr GhcPs) Type
+  deriving Functor
+

From 8dcea255c5bf4a5f0683100cf86f016e95cecdcc Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 14 Apr 2021 14:08:39 -0700
Subject: [PATCH 07/31] Revert "[wip] not working, but most of the pieces are
 here"

This reverts commit fc8d8e5d1a272750ba6de71e0b57b310f11b314c.
---
 .../hls-tactics-plugin/src/Wingman/CodeGen.hs |  9 ---
 .../src/Wingman/LanguageServer.hs             | 63 +++++++------------
 .../Wingman/LanguageServer/TacticProviders.hs | 42 +++++--------
 .../src/Wingman/Machinery.hs                  |  2 -
 .../hls-tactics-plugin/src/Wingman/Plugin.hs  | 14 +----
 .../hls-tactics-plugin/src/Wingman/Types.hs   |  6 --
 6 files changed, 42 insertions(+), 94 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs b/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs
index 70ce62fc15..528a2056f8 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs
@@ -167,15 +167,6 @@ destruct' f hi jdg = do
     & #syn_val       %~ noLoc . case' (var' term)
 
 
-destructExpr :: (ConLike -> Judgement -> Rule) -> HsExpr GhcPs -> Type -> Judgement -> Rule
-destructExpr f term ty jdg = do
-  ext
-      <- destructMatches f Nothing (CType ty) jdg
-  pure $ ext
-    & #syn_trace     %~ rose ("destruct " <> show term) . pure
-    & #syn_val       %~ noLoc . case' term
-
-
 ------------------------------------------------------------------------------
 -- | Combinator for performign case splitting, and running sub-rules on the
 -- resulting matches.
diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
index 6e35605bdf..1349f4c5e3 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
@@ -57,7 +57,6 @@ import           Wingman.Judgements.SYB (everythingContaining, smallestQ, generi
 import           Wingman.Judgements.Theta
 import           Wingman.Range
 import           Wingman.Types
-import Control.Applicative (empty)
 
 
 tacticDesc :: T.Text -> T.Text
@@ -166,11 +165,6 @@ getIdeDynflags state nfp = do
   pure $ ms_hspp_opts $ msrModSummary msr
 
 
-data GoalOrScrutinee
-  = Goal Type
-  | Scrutinee (HsExpr GhcPs) Type
-
-
 ------------------------------------------------------------------------------
 -- | Find the last typechecked module, and find the most specific span, as well
 -- as the judgement at the given range.
@@ -179,7 +173,7 @@ judgementForHole
     -> NormalizedFilePath
     -> Tracked 'Current Range
     -> FeatureSet
-    -> MaybeT IO (Tracked 'Current Range, Hook (), Context, DynFlags)
+    -> MaybeT IO (Tracked 'Current Range, Judgement, Context, DynFlags)
 judgementForHole state nfp range features = do
   TrackedStale asts amapping  <- runStaleIde state nfp GetHieAst
   case unTrack asts of
@@ -191,30 +185,24 @@ judgementForHole state nfp range features = do
            $ runStaleIde state nfp TypeCheck
       hscenv <- runStaleIde state nfp GhcSessionDeps
 
+      rss2 <- liftMaybe $ getSpanAtCursor range' hf
+      (new_span, scrutinee) <- liftMaybe $ getFirst $
+        emptyCaseQ (RealSrcSpan $ unTrack rss2) $ tcg_binds $ untrackedStaleValue tcg
+      x <- MaybeT $ typeCheck (hscEnv $ untrackedStaleValue hscenv) (untrackedStaleValue tcg) scrutinee
+
+      (rss, g) <- liftMaybe $ getSpanAndTypeAtHole range' hf
+      new_rss <- liftMaybe $ mapAgeTo amapping rss
+
       -- KnownThings is just the instances in scope. There are no ranges
       -- involved, so it's not crucial to track ages.
-      let henv = untrackedStaleValue hscenv
-          untracked_tcg = untrackedStaleValue tcg
+      let henv = untrackedStaleValue $ hscenv
       eps <- liftIO $ readIORef $ hsc_EPS $ hscEnv henv
-      kt <- knownThings untracked_tcg henv
-
-      (rss, g_or_s) <-
-        case getSpanAndTypeAtHole range' hf of
-          Just (rss, g) -> pure (rss, Goal g)
-          Nothing -> do
-            rss2 <- liftMaybe $ getSpanAtCursor range' hf
-            (new_span, scrutinee) <- liftMaybe $ getFirst $
-              emptyCaseQ (RealSrcSpan $ unTrack rss2) $ tcg_binds untracked_tcg
-            ty <- MaybeT $ typeCheck (hscEnv henv) untracked_tcg scrutinee
-            case new_span of
-              RealSrcSpan rss -> pure (pure rss, Scrutinee scrutinee ty)
-              UnhelpfulSpan _ -> empty
+      kt <- knownThings (untrackedStaleValue tcg) henv
 
-      new_rss <- liftMaybe $ mapAgeTo amapping rss
-      (hook, ctx) <- liftMaybe $ mkJudgementAndContext features g_or_s binds new_rss tcg eps kt
+      (jdg, ctx) <- liftMaybe $ mkJudgementAndContext features g binds new_rss tcg eps kt
 
       dflags <- getIdeDynflags state nfp
-      pure (fmap realSrcSpanToRange new_rss, hook, ctx, dflags)
+      pure (fmap realSrcSpanToRange new_rss, jdg, ctx, dflags)
 
 
 
@@ -231,14 +219,14 @@ emptyCaseQ span =
 
 mkJudgementAndContext
     :: FeatureSet
-    -> GoalOrScrutinee
+    -> Type
     -> TrackedStale Bindings
     -> Tracked 'Current RealSrcSpan
     -> TrackedStale TcGblEnv
     -> ExternalPackageState
     -> KnownThings
-    -> Maybe (Hook (), Context)
-mkJudgementAndContext features g_or_s (TrackedStale binds bmap) rss (TrackedStale tcg tcgmap) eps kt = do
+    -> Maybe (Judgement, Context)
+mkJudgementAndContext features g (TrackedStale binds bmap) rss (TrackedStale tcg tcgmap) eps kt = do
   binds_rss <- mapAgeFrom bmap rss
   tcg_rss <- mapAgeFrom tcgmap rss
 
@@ -258,19 +246,14 @@ mkJudgementAndContext features g_or_s (TrackedStale binds bmap) rss (TrackedStal
       evidence = getEvidenceAtHole (fmap RealSrcSpan tcg_rss) tcs
       cls_hy = foldMap evidenceToHypothesis evidence
       subst = ts_unifier $ appEndo (foldMap (Endo . evidenceToSubst) evidence) defaultTacticState
-
   pure $
-    case g_or_s of
-      Goal g ->
-        ( Tactic ()
-        $ disallowing AlreadyDestructed already_destructed
-        $ fmap (CType . substTyAddInScope subst . unCType) $ mkFirstJudgement
-              (local_hy <> cls_hy)
-              (isRhsHole tcg_rss tcs)
-              g
-        , ctx
-        )
-      Scrutinee scrutinee ty -> (EmptyCase scrutinee ty, ctx)
+    ( disallowing AlreadyDestructed already_destructed
+    $ fmap (CType . substTyAddInScope subst . unCType) $ mkFirstJudgement
+          (local_hy <> cls_hy)
+          (isRhsHole tcg_rss tcs)
+          g
+    , ctx
+    )
 
 
 ------------------------------------------------------------------------------
diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs
index 4bb84cae8a..4c278a6b9e 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs
@@ -152,7 +152,7 @@ data TacticProviderData = TacticProviderData
   , tpd_plid   :: PluginId
   , tpd_uri    :: Uri
   , tpd_range  :: Tracked 'Current Range
-  , tpd_hook   :: Hook ()
+  , tpd_jdg    :: Judgement
   }
 
 
@@ -189,21 +189,17 @@ requireExtension ext tp tpd =
 -- | Restrict a 'TacticProvider', making sure it appears only when the given
 -- predicate holds for the goal.
 filterGoalType :: (Type -> Bool) -> TacticProvider -> TacticProvider
-filterGoalType p tp =
-  withJudgement $ \jdg ->
-    case p $ unCType $ jGoal jdg of
-      True  -> tp
-      False -> mempty
+filterGoalType p tp tpd =
+  case p $ unCType $ jGoal $ tpd_jdg tpd of
+    True  -> tp tpd
+    False -> pure []
 
 
 ------------------------------------------------------------------------------
 -- | Restrict a 'TacticProvider', making sure it appears only when the given
 -- predicate holds for the goal.
 withJudgement :: (Judgement -> TacticProvider) -> TacticProvider
-withJudgement tp tpd =
-  case tpd_hook tpd of
-    Tactic _ jdg -> tp jdg tpd
-    _ -> pure []
+withJudgement tp tpd = tp (tpd_jdg tpd) tpd
 
 
 ------------------------------------------------------------------------------
@@ -214,16 +210,14 @@ filterBindingType
     -> (OccName -> Type -> TacticProvider)
     -> TacticProvider
 filterBindingType p tp tpd =
-  case tpd_hook tpd of
-    Tactic _ jdg ->
-      let hy  = jLocalHypothesis jdg
-          g   = jGoal jdg
-      in fmap join $ for (unHypothesis hy) $ \hi ->
-            let ty = unCType $ hi_type hi
-            in case p (unCType g) ty of
-                  True  -> tp (hi_name hi) ty tpd
-                  False -> pure []
-    _ -> mempty
+  let jdg = tpd_jdg tpd
+      hy  = jLocalHypothesis jdg
+      g   = jGoal jdg
+   in fmap join $ for (unHypothesis hy) $ \hi ->
+        let ty = unCType $ hi_type hi
+         in case p (unCType g) ty of
+              True  -> tp (hi_name hi) ty tpd
+              False -> pure []
 
 
 ------------------------------------------------------------------------------
@@ -234,11 +228,9 @@ filterTypeProjection
     -> (a -> TacticProvider)
     -> TacticProvider
 filterTypeProjection p tp tpd =
-  case tpd_hook tpd of
-    Tactic _ jdg ->
-      fmap join $ for (p $ unCType $ jGoal jdg) $ \a ->
-          tp a tpd
-    _ -> mempty
+  fmap join $ for (p $ unCType $ jGoal $ tpd_jdg tpd) $ \a ->
+      tp a tpd
+
 
 ------------------------------------------------------------------------------
 -- | Get access to the 'Config' when building a 'TacticProvider'.
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs b/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs
index 9cd9f6e3cd..34dcb449c6 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs
@@ -33,7 +33,6 @@ import           Unify
 import           Wingman.Judgements
 import           Wingman.Simplify (simplify)
 import           Wingman.Types
-import GhcPlugins (unitTy)
 
 
 substCTy :: TCvSubst -> CType -> CType
@@ -53,7 +52,6 @@ newSubgoal j = do
       $ unsetIsTopHole j
 
 
-
 ------------------------------------------------------------------------------
 -- | Attempt to generate a term of the right type using in-scope bindings, and
 -- a given tactic.
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs b/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs
index d51cb0d83c..ec38683a4c 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs
@@ -36,8 +36,6 @@ import           Wingman.Machinery (scoreSolution)
 import           Wingman.Range
 import           Wingman.Tactics
 import           Wingman.Types
-import GhcPlugins (unitTy)
-import Wingman.Judgements (mkFirstJudgement)
 
 
 descriptor :: PluginId -> PluginDescriptor IdeState
@@ -62,7 +60,7 @@ codeActionProvider state plId (CodeActionParams _ _ (TextDocumentIdentifier uri)
   | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do
       cfg <- getTacticConfig plId
       liftIO $ fromMaybeT (Right $ List []) $ do
-        (_, hook, _, dflags) <- judgementForHole state nfp range $ cfg_feature_set cfg
+        (_, jdg, _, dflags) <- judgementForHole state nfp range $ cfg_feature_set cfg
         actions <- lift $
           -- This foldMap is over the function monoid.
           foldMap commandProvider [minBound .. maxBound] $ TacticProviderData
@@ -71,7 +69,7 @@ codeActionProvider state plId (CodeActionParams _ _ (TextDocumentIdentifier uri)
             , tpd_plid   = plId
             , tpd_uri    = uri
             , tpd_range  = range
-            , tpd_hook   = hook
+            , tpd_jdg    = jdg
             }
         pure $ Right $ List actions
 codeActionProvider _ _ _ = pure $ Right $ List []
@@ -216,11 +214,3 @@ graftDecl _ _ _ _ x = pure $ pure x
 fromMaybeT :: Functor m => a -> MaybeT m a -> m a
 fromMaybeT def = fmap (fromMaybe def) . runMaybeT
 
-
-runHook
-    :: Context
-    -> Hook (TacticsM ())
-    -> Either [TacticError] RunTacticResults
-runHook ctx (Tactic t jdg) = runTactic ctx jdg t
-runHook ctx (EmptyCase ty) = runTactic ctx (mkFirstJudgement mempty False unitTy) _
-
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Types.hs b/plugins/hls-tactics-plugin/src/Wingman/Types.hs
index 0a6532c0e8..64e7f5e00e 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Types.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Types.hs
@@ -490,9 +490,3 @@ instance Show UserFacingMessage where
   show NothingToDo             = "Nothing to do"
   show (InfrastructureError t) = "Internal error: " <> T.unpack t
 
-
-data Hook a
-  = Tactic a Judgement
-  | EmptyCase (HsExpr GhcPs) Type
-  deriving Functor
-

From 8230d0cae6c0e76dc53ed15b2aa88b9eff7ed77e Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 14 Apr 2021 15:54:51 -0700
Subject: [PATCH 08/31] Got it hooked up as a code lens, modulo actually
 putting in the ctors

---
 .../src/Wingman/LanguageServer.hs             | 44 ++++++++++-----
 .../hls-tactics-plugin/src/Wingman/Plugin.hs  | 56 ++++++++++++++++---
 2 files changed, 78 insertions(+), 22 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
index 1349f4c5e3..c2658a3127 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
@@ -24,6 +24,7 @@ import qualified Data.Set as S
 import qualified Data.Text as T
 import           Data.Traversable
 import           Development.IDE (getFilesOfInterest, ShowDiagnostic (ShowDiag), srcSpanToRange)
+import qualified Development.IDE as GHCIDE
 import           Development.IDE (hscEnv)
 import           Development.IDE.Core.RuleTypes
 import           Development.IDE.Core.Rules (usePropertyAction)
@@ -57,6 +58,7 @@ import           Wingman.Judgements.SYB (everythingContaining, smallestQ, generi
 import           Wingman.Judgements.Theta
 import           Wingman.Range
 import           Wingman.Types
+import Control.Applicative (empty)
 
 
 tacticDesc :: T.Text -> T.Text
@@ -185,11 +187,6 @@ judgementForHole state nfp range features = do
            $ runStaleIde state nfp TypeCheck
       hscenv <- runStaleIde state nfp GhcSessionDeps
 
-      rss2 <- liftMaybe $ getSpanAtCursor range' hf
-      (new_span, scrutinee) <- liftMaybe $ getFirst $
-        emptyCaseQ (RealSrcSpan $ unTrack rss2) $ tcg_binds $ untrackedStaleValue tcg
-      x <- MaybeT $ typeCheck (hscEnv $ untrackedStaleValue hscenv) (untrackedStaleValue tcg) scrutinee
-
       (rss, g) <- liftMaybe $ getSpanAndTypeAtHole range' hf
       new_rss <- liftMaybe $ mapAgeTo amapping rss
 
@@ -205,16 +202,35 @@ judgementForHole state nfp range features = do
       pure (fmap realSrcSpanToRange new_rss, jdg, ctx, dflags)
 
 
+------------------------------------------------------------------------------
+-- | Find the last typechecked module, and find the most specific span, as well
+-- as the judgement at the given range.
+completionForHole
+    :: IdeState
+    -> NormalizedFilePath
+    -> FeatureSet
+    -> MaybeT IO [(Tracked 'Current RealSrcSpan, Type)]
+completionForHole state nfp features = do
+    TrackedStale tcg tcg_map <- fmap (fmap tmrTypechecked) $ runStaleIde state nfp TypeCheck
+    let tcg' = unTrack tcg
+    hscenv <- runStaleIde state nfp GhcSessionDeps
+
+    let zz = traverse (emptyCaseQ . tcg_binds) tcg
+
+    for zz $ \aged@(unTrack -> (ss, scrutinee)) -> do
+      ty <- MaybeT $ typeCheck (hscEnv $ untrackedStaleValue hscenv) tcg' scrutinee
+      case ss of
+        RealSrcSpan r   -> do
+          rss' <- liftMaybe $ mapAgeTo tcg_map $ unsafeCopyAge aged r
+          pure (rss', ty)
+        UnhelpfulSpan _ -> empty
+
+
 
-emptyCaseQ :: SrcSpan -> GenericQ (First (SrcSpan, HsExpr GhcTc))
-emptyCaseQ span =
-  smallestQ
-    (genericDefinitelyNotIsSubspan span `extQ` \case
-      (L _ (Case _ _)) -> Just True
-      (_ :: LHsExpr GhcTc) -> Nothing
-    ) $ mkQ mempty $ \case
-          L new_span (Case scrutinee []) -> pure (new_span, scrutinee)
-          (_ :: LHsExpr GhcTc) -> mempty
+emptyCaseQ :: GenericQ [(SrcSpan, HsExpr GhcTc)]
+emptyCaseQ = everything (<>) $ mkQ mempty $ \case
+  L new_span (Case scrutinee []) -> pure (new_span, scrutinee)
+  (_ :: LHsExpr GhcTc) -> mempty
 
 
 mkJudgementAndContext
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs b/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs
index ec38683a4c..3c22d2c3d2 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs
@@ -36,24 +36,64 @@ import           Wingman.Machinery (scoreSolution)
 import           Wingman.Range
 import           Wingman.Tactics
 import           Wingman.Types
+import Data.Functor ((<&>))
+import Development.IDE (srcSpanToRange, realSrcSpanToRange)
+import qualified Data.HashMap.Strict as HM
 
 
 descriptor :: PluginId -> PluginDescriptor IdeState
 descriptor plId = (defaultPluginDescriptor plId)
   { pluginCommands
-      = fmap (\tc ->
-          PluginCommand
-            (tcCommandId tc)
-            (tacticDesc $ tcCommandName tc)
-            (tacticCmd (commandTactic tc) plId))
-            [minBound .. maxBound]
-  , pluginHandlers =
-      mkPluginHandler STextDocumentCodeAction codeActionProvider
+      = mconcat
+          [ fmap (\tc ->
+              PluginCommand
+                (tcCommandId tc)
+                (tacticDesc $ tcCommandName tc)
+                (tacticCmd (commandTactic tc) plId))
+                [minBound .. maxBound]
+          , pure $ PluginCommand (CommandId "emptycase.complete") "Complete the empty case" commandHandler
+          ]
+  , pluginHandlers = mconcat
+      [ mkPluginHandler STextDocumentCodeAction codeActionProvider
+      , mkPluginHandler STextDocumentCodeLens completionProvider
+      ]
   , pluginRules = wingmanRules plId
   , pluginCustomConfig =
       mkCustomConfig properties
   }
 
+commandHandler :: CommandFunction IdeState WorkspaceEdit
+commandHandler _ideState wedit = do
+  _ <- sendRequest SWorkspaceApplyEdit (ApplyWorkspaceEditParams Nothing wedit) (\_ -> pure ())
+  return $ Right Null
+
+completionProvider :: PluginMethodHandler IdeState TextDocumentCodeLens
+completionProvider state plId (CodeLensParams _ _ (TextDocumentIdentifier uri))
+  | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do
+      cfg <- getTacticConfig plId
+      traceM "got a cfg"
+      liftIO $ fromMaybeT (Right $ List []) $ do
+        holes <- completionForHole  state nfp $ cfg_feature_set cfg
+        traceMX "found holes" holes
+        pure $ Right $ List $ holes <&> \(ss, ty) ->
+          let range = realSrcSpanToRange $ unTrack ss
+           in CodeLens
+                range
+                (Just $ mkLspCommand plId
+                  (CommandId "emptycase.complete")
+                  "Complete case constructors" $
+                    Just $ pure $ toJSON $
+                      WorkspaceEdit
+                        (Just $ HM.singleton uri $ List $ pure $ TextEdit range $ T.pack $ unsafeRender ty)
+                        Nothing
+                        Nothing
+                )
+                Nothing
+                -- (Just $ Command "Complete case constructors" "emptycase.complete" $
+                --   Just $ List
+                -- Nothing
+completionProvider _ _ _ = pure $ Right $ List []
+
 
 codeActionProvider :: PluginMethodHandler IdeState TextDocumentCodeAction
 codeActionProvider state plId (CodeActionParams _ _ (TextDocumentIdentifier uri) (unsafeMkCurrent -> range) _ctx)

From 67ff25f0f44cc789b434001c69fa9550567d0805 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 14 Apr 2021 16:27:45 -0700
Subject: [PATCH 09/31] It works as a code lens!

---
 .../hls-tactics-plugin/src/Wingman/CodeGen.hs | 25 +++++++++++++++----
 .../hls-tactics-plugin/src/Wingman/Naming.hs  |  6 ++---
 .../hls-tactics-plugin/src/Wingman/Plugin.hs  | 15 ++++++-----
 .../hls-tactics-plugin/src/Wingman/Tactics.hs |  2 +-
 4 files changed, 33 insertions(+), 15 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs b/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs
index 528a2056f8..b904012d71 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs
@@ -1,7 +1,8 @@
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE OverloadedLabels #-}
-{-# LANGUAGE TupleSections    #-}
-{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE FlexibleContexts  #-}
+{-# LANGUAGE OverloadedLabels  #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE TupleSections     #-}
+{-# LANGUAGE TypeApplications  #-}
 
 module Wingman.CodeGen
   ( module Wingman.CodeGen
@@ -65,7 +66,7 @@ destructMatches f scrut t jdg = do
               args = conLikeInstOrigArgTys' con apps
           modify $ appEndo $ foldMap (Endo . evidenceToSubst) ev
           subst <- gets ts_unifier
-          names <- mkManyGoodNames (hyNamesInScope hy) args
+          let names = mkManyGoodNames (hyNamesInScope hy) args
           let hy' = patternHypothesis scrut con jdg
                   $ zip names
                   $ coerce args
@@ -81,6 +82,20 @@ destructMatches f scrut t jdg = do
             & #syn_val     %~ match [mkDestructPat con names] . unLoc
 
 
+destructionFor :: Hypothesis a -> Type -> Maybe [RawMatch]
+destructionFor hy t = do
+  case tacticsGetDataCons t of
+    Nothing -> Nothing
+    Just ([], _) -> Nothing
+    Just (dcs, apps) -> do
+      for dcs $ \dc -> do
+        let con = RealDataCon dc
+            args = conLikeInstOrigArgTys' con apps
+            names = mkManyGoodNames (hyNamesInScope hy) args
+        pure $ match [mkDestructPat con names] $ var "_"
+
+
+
 ------------------------------------------------------------------------------
 -- | Produces a pattern for a data con and the names of its fields.
 mkDestructPat :: ConLike -> [OccName] -> Pat GhcPs
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Naming.hs b/plugins/hls-tactics-plugin/src/Wingman/Naming.hs
index 810cb5311f..f0d133d837 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Naming.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Naming.hs
@@ -77,12 +77,12 @@ mkGoodName in_scope t =
 ------------------------------------------------------------------------------
 -- | Like 'mkGoodName' but creates several apart names.
 mkManyGoodNames
-  :: (Traversable t, Monad m)
+  :: (Traversable t)
   => Set OccName
   -> t Type
-  -> m (t OccName)
+  -> t OccName
 mkManyGoodNames in_scope args =
-  flip evalStateT in_scope $ for args $ \at -> do
+  flip evalState in_scope $ for args $ \at -> do
     in_scope <- get
     let n = mkGoodName in_scope at
     modify $ S.insert n
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs b/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs
index 3c22d2c3d2..93dc306bcf 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs
@@ -15,8 +15,11 @@ import           Data.Aeson
 import           Data.Bifunctor (first)
 import           Data.Data
 import           Data.Foldable (for_)
+import           Data.Functor ((<&>))
+import qualified Data.HashMap.Strict as HM
 import           Data.Maybe
 import qualified Data.Text as T
+import           Development.IDE (realSrcSpanToRange)
 import           Development.IDE.Core.Shake (IdeState (..))
 import           Development.IDE.Core.UseStale (Tracked, TrackedStale(..), unTrack, mapAgeFrom, unsafeMkCurrent)
 import           Development.IDE.GHC.Compat
@@ -36,9 +39,8 @@ import           Wingman.Machinery (scoreSolution)
 import           Wingman.Range
 import           Wingman.Tactics
 import           Wingman.Types
-import Data.Functor ((<&>))
-import Development.IDE (srcSpanToRange, realSrcSpanToRange)
-import qualified Data.HashMap.Strict as HM
+import Wingman.CodeGen (destructionFor)
+import GHC.SourceGen (case', var)
 
 
 descriptor :: PluginId -> PluginDescriptor IdeState
@@ -76,15 +78,16 @@ completionProvider state plId (CodeLensParams _ _ (TextDocumentIdentifier uri))
         holes <- completionForHole  state nfp $ cfg_feature_set cfg
         traceMX "found holes" holes
         pure $ Right $ List $ holes <&> \(ss, ty) ->
-          let range = realSrcSpanToRange $ unTrack ss
+          let range@(Range _ ep) = realSrcSpanToRange $ unTrack ss
+              rep_range = Range ep ep
            in CodeLens
                 range
                 (Just $ mkLspCommand plId
                   (CommandId "emptycase.complete")
-                  "Complete case constructors" $
+                  ("Complete case constructors (" <> T.pack (unsafeRender ty) <> ")") $
                     Just $ pure $ toJSON $
                       WorkspaceEdit
-                        (Just $ HM.singleton uri $ List $ pure $ TextEdit range $ T.pack $ unsafeRender ty)
+                        (Just $ HM.singleton uri $ List $ pure $ TextEdit rep_range $ T.pack $ mappend "\n" $ unlines $ drop 1 $ lines $ unsafeRender $ case' (var "_")  $ fromJust $ destructionFor mempty ty)
                         Nothing
                         Nothing
                 )
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs
index 30f9c953fa..a64233ca6f 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs
@@ -99,7 +99,7 @@ intros = rule $ \jdg -> do
   case tcSplitFunTys $ unCType g of
     ([], _) -> throwError $ GoalMismatch "intros" g
     (as, b) -> do
-      vs <- mkManyGoodNames (hyNamesInScope $ jEntireHypothesis jdg) as
+      let vs = mkManyGoodNames (hyNamesInScope $ jEntireHypothesis jdg) as
       let top_hole = isTopHole ctx jdg
           hy' = lambdaHypothesis top_hole $ zip vs $ coerce as
           jdg' = introduce hy'

From f69d068e006a13ab3cc6080b959abbf09ab3ad8a Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 14 Apr 2021 18:38:21 -0700
Subject: [PATCH 10/31] Allow MagicHash; gracefully exit if cant typecheck

---
 .../src/Wingman/CodeGen/Utils.hs              |  4 ++--
 .../hls-tactics-plugin/src/Wingman/Plugin.hs  | 22 ++++++++++++++-----
 2 files changed, 19 insertions(+), 7 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Wingman/CodeGen/Utils.hs b/plugins/hls-tactics-plugin/src/Wingman/CodeGen/Utils.hs
index 22237904b9..1f1738dacc 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/CodeGen/Utils.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/CodeGen/Utils.hs
@@ -5,7 +5,7 @@ import Data.List
 import DataCon
 import Development.IDE.GHC.Compat
 import GHC.Exts
-import GHC.SourceGen (RdrNameStr, recordConE, string)
+import GHC.SourceGen (RdrNameStr (UnqualStr), recordConE, string)
 import GHC.SourceGen.Overloaded
 import GhcPlugins (nilDataCon, charTy, eqType)
 import Name
@@ -43,7 +43,7 @@ mkCon con apps (fmap unLoc -> args)
 
 
 coerceName :: HasOccName a => a -> RdrNameStr
-coerceName = fromString . occNameString . occName
+coerceName = UnqualStr . fromString . occNameString . occName
 
 
 ------------------------------------------------------------------------------
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs b/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs
index 93dc306bcf..87f4d2e054 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs
@@ -19,11 +19,13 @@ import           Data.Functor ((<&>))
 import qualified Data.HashMap.Strict as HM
 import           Data.Maybe
 import qualified Data.Text as T
+import           Data.Traversable (for)
 import           Development.IDE (realSrcSpanToRange)
 import           Development.IDE.Core.Shake (IdeState (..))
 import           Development.IDE.Core.UseStale (Tracked, TrackedStale(..), unTrack, mapAgeFrom, unsafeMkCurrent)
 import           Development.IDE.GHC.Compat
 import           Development.IDE.GHC.ExactPrint
+import           GHC.SourceGen (case', var)
 import           Ide.Types
 import           Language.LSP.Server
 import           Language.LSP.Types
@@ -32,6 +34,7 @@ import           OccName
 import           Prelude hiding (span)
 import           System.Timeout
 import           Wingman.CaseSplit
+import           Wingman.CodeGen (destructionFor)
 import           Wingman.GHC
 import           Wingman.LanguageServer
 import           Wingman.LanguageServer.TacticProviders
@@ -39,8 +42,6 @@ import           Wingman.Machinery (scoreSolution)
 import           Wingman.Range
 import           Wingman.Tactics
 import           Wingman.Types
-import Wingman.CodeGen (destructionFor)
-import GHC.SourceGen (case', var)
 
 
 descriptor :: PluginId -> PluginDescriptor IdeState
@@ -77,17 +78,28 @@ completionProvider state plId (CodeLensParams _ _ (TextDocumentIdentifier uri))
       liftIO $ fromMaybeT (Right $ List []) $ do
         holes <- completionForHole  state nfp $ cfg_feature_set cfg
         traceMX "found holes" holes
-        pure $ Right $ List $ holes <&> \(ss, ty) ->
+        fmap (Right . List) $ for holes $ \(ss, ty) -> do
           let range@(Range _ ep) = realSrcSpanToRange $ unTrack ss
               rep_range = Range ep ep
-           in CodeLens
+          matches <- liftMaybe $ destructionFor mempty ty
+          pure $ CodeLens
                 range
                 (Just $ mkLspCommand plId
                   (CommandId "emptycase.complete")
                   ("Complete case constructors (" <> T.pack (unsafeRender ty) <> ")") $
                     Just $ pure $ toJSON $
                       WorkspaceEdit
-                        (Just $ HM.singleton uri $ List $ pure $ TextEdit rep_range $ T.pack $ mappend "\n" $ unlines $ drop 1 $ lines $ unsafeRender $ case' (var "_")  $ fromJust $ destructionFor mempty ty)
+                        (Just $ HM.singleton uri
+                              $ List
+                              $ pure
+                              $ TextEdit rep_range
+                              $ T.pack
+                              $ mappend "\n"
+                              $ unlines
+                              $ drop 1
+                              $ lines
+                              $ unsafeRender
+                              $ case' (var "_")  matches)
                         Nothing
                         Nothing
                 )

From 6d1882b2f4ce244a8b5ebb35a58bfd98786a7066 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 14 Apr 2021 18:51:00 -0700
Subject: [PATCH 11/31] Don't shadow bindings

---
 .../hls-tactics-plugin/src/Wingman/Plugin.hs   | 18 +++++++++++++++---
 1 file changed, 15 insertions(+), 3 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs b/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs
index 87f4d2e054..ce9f281b88 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs
@@ -15,16 +15,16 @@ import           Data.Aeson
 import           Data.Bifunctor (first)
 import           Data.Data
 import           Data.Foldable (for_)
-import           Data.Functor ((<&>))
 import qualified Data.HashMap.Strict as HM
 import           Data.Maybe
 import qualified Data.Text as T
 import           Data.Traversable (for)
-import           Development.IDE (realSrcSpanToRange)
+import           Development.IDE (realSrcSpanToRange, GetBindings(..))
 import           Development.IDE.Core.Shake (IdeState (..))
 import           Development.IDE.Core.UseStale (Tracked, TrackedStale(..), unTrack, mapAgeFrom, unsafeMkCurrent)
 import           Development.IDE.GHC.Compat
 import           Development.IDE.GHC.ExactPrint
+import           Development.IDE.Spans.LocalBindings (getLocalScope)
 import           GHC.SourceGen (case', var)
 import           Ide.Types
 import           Language.LSP.Server
@@ -70,18 +70,30 @@ commandHandler _ideState wedit = do
   _ <- sendRequest SWorkspaceApplyEdit (ApplyWorkspaceEditParams Nothing wedit) (\_ -> pure ())
   return $ Right Null
 
+
+hySingleton :: OccName -> Hypothesis ()
+hySingleton n = Hypothesis . pure $ HyInfo n UserPrv ()
+
+
 completionProvider :: PluginMethodHandler IdeState TextDocumentCodeLens
 completionProvider state plId (CodeLensParams _ _ (TextDocumentIdentifier uri))
   | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do
       cfg <- getTacticConfig plId
       traceM "got a cfg"
       liftIO $ fromMaybeT (Right $ List []) $ do
+        TrackedStale binds bind_map <- runStaleIde state nfp GetBindings
         holes <- completionForHole  state nfp $ cfg_feature_set cfg
         traceMX "found holes" holes
         fmap (Right . List) $ for holes $ \(ss, ty) -> do
+          binds_ss <- liftMaybe $ mapAgeFrom bind_map ss
+          let bindings = getLocalScope (unTrack binds) $ unTrack binds_ss
           let range@(Range _ ep) = realSrcSpanToRange $ unTrack ss
               rep_range = Range ep ep
-          matches <- liftMaybe $ destructionFor mempty ty
+          matches <-
+            liftMaybe $
+              destructionFor
+                (foldMap (hySingleton . occName . fst) bindings)
+                ty
           pure $ CodeLens
                 range
                 (Just $ mkLspCommand plId

From 23e5d06d5dee2860c143eb8092b4380407a7a7df Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 14 Apr 2021 19:07:37 -0700
Subject: [PATCH 12/31] Extract the src span of the case's match group

---
 plugins/hls-tactics-plugin/src/Wingman/CaseSplit.hs      | 2 +-
 plugins/hls-tactics-plugin/src/Wingman/GHC.hs            | 6 +++---
 plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs | 4 ++--
 3 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Wingman/CaseSplit.hs b/plugins/hls-tactics-plugin/src/Wingman/CaseSplit.hs
index dffb9f30ca..1f732f7703 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/CaseSplit.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/CaseSplit.hs
@@ -30,7 +30,7 @@ mkFirstAgda pats body                = AgdaMatch pats body
 -- | Transform an 'AgdaMatch' whose body is a case over a bound pattern, by
 -- splitting it into multiple matches: one for each alternative of the case.
 agdaSplit :: AgdaMatch -> [AgdaMatch]
-agdaSplit (AgdaMatch pats (Case (HsVar _ (L _ var)) matches)) = do
+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) $ unLoc body
diff --git a/plugins/hls-tactics-plugin/src/Wingman/GHC.hs b/plugins/hls-tactics-plugin/src/Wingman/GHC.hs
index f4939fbf0b..e719c20e0f 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/GHC.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/GHC.hs
@@ -235,10 +235,10 @@ unpackMatches _ = Nothing
 
 ------------------------------------------------------------------------------
 -- | A pattern over the otherwise (extremely) messy AST for lambdas.
-pattern Case :: PatCompattable p => HsExpr p -> [(Pat p, LHsExpr p)] -> HsExpr p
-pattern Case scrutinee matches <-
+pattern Case :: PatCompattable p => HsExpr p -> SrcSpan -> [(Pat p, LHsExpr p)] -> HsExpr p
+pattern Case scrutinee span matches <-
   HsCase _ (L _ scrutinee)
-    (MG {mg_alts = L _ (fmap unLoc -> unpackMatches -> Just matches)})
+    (MG {mg_alts = L span (fmap unLoc -> unpackMatches -> Just matches)})
 
 
 ------------------------------------------------------------------------------
diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
index c2658a3127..c8ff91a61c 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
@@ -229,7 +229,7 @@ completionForHole state nfp features = do
 
 emptyCaseQ :: GenericQ [(SrcSpan, HsExpr GhcTc)]
 emptyCaseQ = everything (<>) $ mkQ mempty $ \case
-  L new_span (Case scrutinee []) -> pure (new_span, scrutinee)
+  L new_span (Case scrutinee _ []) -> pure (new_span, scrutinee)
   (_ :: LHsExpr GhcTc) -> mempty
 
 
@@ -282,7 +282,7 @@ getAlreadyDestructed
 getAlreadyDestructed (unTrack -> span) (unTrack -> binds) =
   everythingContaining span
     (mkQ mempty $ \case
-      Case (HsVar _ (L _ (occName -> var))) _ ->
+      Case (HsVar _ (L _ (occName -> var))) _ _ ->
         S.singleton var
       (_ :: HsExpr GhcTc) -> mempty
     ) binds

From 848f9d258cf3ee8c72e5e6d2faf3cebbb840ac33 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 14 Apr 2021 21:16:05 -0700
Subject: [PATCH 13/31] Improve how parenthesizing happens in ExactPrint

---
 ghcide/src/Development/IDE/GHC/ExactPrint.hs  | 66 +++++++++++++++----
 .../test/golden/LayoutSplitGuard.hs.expected  |  6 +-
 2 files changed, 55 insertions(+), 17 deletions(-)

diff --git a/ghcide/src/Development/IDE/GHC/ExactPrint.hs b/ghcide/src/Development/IDE/GHC/ExactPrint.hs
index 4e494eb82d..7535ba4c0a 100644
--- a/ghcide/src/Development/IDE/GHC/ExactPrint.hs
+++ b/ghcide/src/Development/IDE/GHC/ExactPrint.hs
@@ -12,6 +12,7 @@ module Development.IDE.GHC.ExactPrint
       annotateDecl,
       hoistGraft,
       graftWithM,
+      graftExprWithM,
       genericGraftWithSmallestM,
       genericGraftWithLargestM,
       graftSmallestDeclsWithM,
@@ -66,11 +67,9 @@ import Parser (parseIdentifier)
 import Data.Traversable (for)
 import Data.Foldable (Foldable(fold))
 import Data.Bool (bool)
-import Data.Monoid (All(All), Any(Any))
+import Data.Monoid (All(All), Any(Any), getAll)
 import Data.Functor.Compose (Compose(Compose))
-#if __GLASGOW_HASKELL__ == 808
 import Control.Arrow
-#endif
 
 
 ------------------------------------------------------------------------------
@@ -246,25 +245,64 @@ graftExpr ::
     LHsExpr GhcPs ->
     Graft (Either String) a
 graftExpr dst val = Graft $ \dflags a -> do
-    -- Traverse the tree, looking for our replacement node. But keep track of
-    -- the context (parent HsExpr constructor) we're in while we do it. This
-    -- lets us determine wehther or not we need parentheses.
-    let (All needs_parens, All needs_space) =
-          everythingWithContext (All True, All True) (<>)
-            ( mkQ (mempty, ) $ \x s -> case x of
-                (L src _ :: LHsExpr GhcPs) | src == dst ->
-                  (s, s)
-                L _ x' -> (mempty, needsParensSpace x')
-            ) a
+    let (needs_space, mk_parens) = getNeedsSpaceAndParenthesize dst a
 
     runGraft
-      (graft' needs_space dst $ bool id maybeParensAST needs_parens val)
+      (graft' needs_space dst $ mk_parens val)
       dflags
       a
 
 
+getNeedsSpaceAndParenthesize ::
+    (ASTElement ast, Data a) =>
+    SrcSpan ->
+    a ->
+    (Bool, Located ast -> Located ast)
+getNeedsSpaceAndParenthesize dst a =
+  -- Traverse the tree, looking for our replacement node. But keep track of
+  -- the context (parent HsExpr constructor) we're in while we do it. This
+  -- lets us determine wehther or not we need parentheses.
+  let (needs_parens, needs_space) =
+          everythingWithContext (Nothing, Nothing) (<>)
+            ( mkQ (mempty, ) $ \x s -> case x of
+                (L src _ :: LHsExpr GhcPs) | src == dst ->
+                  (s, s)
+                L _ x' -> (mempty, Just *** Just $ needsParensSpace x')
+            ) a
+   in ( maybe True getAll needs_space
+      , bool id maybeParensAST $ maybe False getAll needs_parens
+      )
+
+
 ------------------------------------------------------------------------------
 
+graftExprWithM ::
+    forall m a.
+    (Fail.MonadFail m, Data a) =>
+    SrcSpan ->
+    (LHsExpr GhcPs -> TransformT m (Maybe (LHsExpr GhcPs))) ->
+    Graft m a
+graftExprWithM dst trans = Graft $ \dflags a -> do
+    let (needs_space, mk_parens) = getNeedsSpaceAndParenthesize dst a
+
+    everywhereM'
+        ( mkM $
+            \case
+                val@(L src _ :: LHsExpr GhcPs)
+                    | src == dst -> do
+                        mval <- trans val
+                        case mval of
+                            Just val' -> do
+                                (anns, val'') <-
+                                    hoistTransform (either Fail.fail pure) $
+                                        annotate dflags needs_space $ mk_parens val'
+                                modifyAnnsT $ mappend anns
+                                pure val''
+                            Nothing -> pure val
+                l -> pure l
+        )
+        a
+
 graftWithM ::
     forall ast m a.
     (Fail.MonadFail m, Data a, ASTElement ast) =>
diff --git a/plugins/hls-tactics-plugin/test/golden/LayoutSplitGuard.hs.expected b/plugins/hls-tactics-plugin/test/golden/LayoutSplitGuard.hs.expected
index 3d68d8ac96..cd3cca6c2e 100644
--- a/plugins/hls-tactics-plugin/test/golden/LayoutSplitGuard.hs.expected
+++ b/plugins/hls-tactics-plugin/test/golden/LayoutSplitGuard.hs.expected
@@ -1,5 +1,5 @@
 test :: Bool -> Bool -> Bool
 test a b
-  | a = (case b of
-   False -> _
-   True -> _)
+  | a = case b of
+  False -> _
+  True -> _

From eba96315786967754cdde8431f69c5c646b0dad9 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 14 Apr 2021 21:16:23 -0700
Subject: [PATCH 14/31] Remove a field that pedantic is yelling about

---
 ghcide/src/Development/IDE/Core/UseStale.hs | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/ghcide/src/Development/IDE/Core/UseStale.hs b/ghcide/src/Development/IDE/Core/UseStale.hs
index c9f3df3aec..f82a7a9e57 100644
--- a/ghcide/src/Development/IDE/Core/UseStale.hs
+++ b/ghcide/src/Development/IDE/Core/UseStale.hs
@@ -3,6 +3,8 @@
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE RankNTypes     #-}
 
+{-# OPTIONS_GHC -fno-warn-unused-top-binds #-}
+
 module Development.IDE.Core.UseStale
   ( Age(..)
   , Tracked

From af77d0a3036ba706d5a7ca319e1180814d484e03 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 14 Apr 2021 21:22:14 -0700
Subject: [PATCH 15/31] It works!

---
 .../hls-tactics-plugin/src/Wingman/CodeGen.hs | 17 ++++-
 .../src/Wingman/LanguageServer.hs             | 10 +--
 .../hls-tactics-plugin/src/Wingman/Plugin.hs  | 76 ++++++++++++-------
 3 files changed, 64 insertions(+), 39 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs b/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs
index b904012d71..1fe9844478 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs
@@ -48,6 +48,8 @@ destructMatches
        -- ^ Type being destructed
     -> Judgement
     -> RuleM (Synthesized [RawMatch])
+-- TODO(sandy): In an ideal world, this would be the same codepath as
+-- 'destructionFor'. Make sure to change that if you ever change this.
 destructMatches f scrut t jdg = do
   let hy = jEntireHypothesis jdg
       g  = jGoal jdg
@@ -82,17 +84,24 @@ destructMatches f scrut t jdg = do
             & #syn_val     %~ match [mkDestructPat con names] . unLoc
 
 
-destructionFor :: Hypothesis a -> Type -> Maybe [RawMatch]
+destructionFor :: Hypothesis a -> Type -> Maybe [LMatch GhcPs (LHsExpr GhcPs)]
+-- TODO(sandy): In an ideal world, this would be the same codepath as
+-- 'destructMatches'. Make sure to change that if you ever change this.
 destructionFor hy t = do
   case tacticsGetDataCons t of
     Nothing -> Nothing
     Just ([], _) -> Nothing
     Just (dcs, apps) -> do
       for dcs $ \dc -> do
-        let con = RealDataCon dc
-            args = conLikeInstOrigArgTys' con apps
+        let con   = RealDataCon dc
+            args  = conLikeInstOrigArgTys' con apps
             names = mkManyGoodNames (hyNamesInScope hy) args
-        pure $ match [mkDestructPat con names] $ var "_"
+        pure
+          . noLoc
+          . Match noExt CaseAlt [mkDestructPat con names]
+          . GRHSs noExt (pure $ noLoc $ GRHS noExt [] $ noLoc $ var "_")
+          . noLoc
+          $ EmptyLocalBinds noExt
 
 
 
diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
index c8ff91a61c..6cd8126a53 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
@@ -6,13 +6,14 @@
 module Wingman.LanguageServer where
 
 import           ConLike
+import           Control.Applicative (empty)
 import           Control.Arrow
 import           Control.Monad
 import           Control.Monad.State (State, get, put, evalState)
 import           Control.Monad.Trans.Maybe
 import           Data.Coerce
 import           Data.Functor ((<&>))
-import           Data.Generics.Aliases (mkQ, GenericQ, extQ)
+import           Data.Generics.Aliases (mkQ, GenericQ)
 import           Data.Generics.Schemes (everything)
 import qualified Data.HashMap.Strict as Map
 import           Data.IORef (readIORef)
@@ -24,7 +25,6 @@ import qualified Data.Set as S
 import qualified Data.Text as T
 import           Data.Traversable
 import           Development.IDE (getFilesOfInterest, ShowDiagnostic (ShowDiag), srcSpanToRange)
-import qualified Development.IDE as GHCIDE
 import           Development.IDE (hscEnv)
 import           Development.IDE.Core.RuleTypes
 import           Development.IDE.Core.Rules (usePropertyAction)
@@ -54,11 +54,10 @@ import           Wingman.Context
 import           Wingman.FeatureSet
 import           Wingman.GHC
 import           Wingman.Judgements
-import           Wingman.Judgements.SYB (everythingContaining, smallestQ, genericDefinitelyNotIsSubspan)
+import           Wingman.Judgements.SYB (everythingContaining)
 import           Wingman.Judgements.Theta
 import           Wingman.Range
 import           Wingman.Types
-import Control.Applicative (empty)
 
 
 tacticDesc :: T.Text -> T.Text
@@ -214,7 +213,6 @@ completionForHole state nfp features = do
     TrackedStale tcg tcg_map <- fmap (fmap tmrTypechecked) $ runStaleIde state nfp TypeCheck
     let tcg' = unTrack tcg
     hscenv <- runStaleIde state nfp GhcSessionDeps
-
     let zz = traverse (emptyCaseQ . tcg_binds) tcg
 
     for zz $ \aged@(unTrack -> (ss, scrutinee)) -> do
@@ -229,7 +227,7 @@ completionForHole state nfp features = do
 
 emptyCaseQ :: GenericQ [(SrcSpan, HsExpr GhcTc)]
 emptyCaseQ = everything (<>) $ mkQ mempty $ \case
-  L new_span (Case scrutinee _ []) -> pure (new_span, scrutinee)
+  L case_span (Case scrutinee _ []) -> pure (case_span, scrutinee)
   (_ :: LHsExpr GhcTc) -> mempty
 
 
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs b/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs
index ce9f281b88..bf1602f531 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs
@@ -15,7 +15,6 @@ import           Data.Aeson
 import           Data.Bifunctor (first)
 import           Data.Data
 import           Data.Foldable (for_)
-import qualified Data.HashMap.Strict as HM
 import           Data.Maybe
 import qualified Data.Text as T
 import           Data.Traversable (for)
@@ -25,7 +24,6 @@ import           Development.IDE.Core.UseStale (Tracked, TrackedStale(..), unTra
 import           Development.IDE.GHC.Compat
 import           Development.IDE.GHC.ExactPrint
 import           Development.IDE.Spans.LocalBindings (getLocalScope)
-import           GHC.SourceGen (case', var)
 import           Ide.Types
 import           Language.LSP.Server
 import           Language.LSP.Types
@@ -79,48 +77,39 @@ completionProvider :: PluginMethodHandler IdeState TextDocumentCodeLens
 completionProvider state plId (CodeLensParams _ _ (TextDocumentIdentifier uri))
   | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do
       cfg <- getTacticConfig plId
-      traceM "got a cfg"
+      ccs <- getClientCapabilities
       liftIO $ fromMaybeT (Right $ List []) $ do
+        dflags <- getIdeDynflags state nfp
+        TrackedStale pm _ <- runStaleIde state nfp GetAnnotatedParsedSource
         TrackedStale binds bind_map <- runStaleIde state nfp GetBindings
         holes <- completionForHole  state nfp $ cfg_feature_set cfg
-        traceMX "found holes" holes
         fmap (Right . List) $ for holes $ \(ss, ty) -> do
           binds_ss <- liftMaybe $ mapAgeFrom bind_map ss
           let bindings = getLocalScope (unTrack binds) $ unTrack binds_ss
-          let range@(Range _ ep) = realSrcSpanToRange $ unTrack ss
-              rep_range = Range ep ep
+          let range = realSrcSpanToRange $ unTrack ss
           matches <-
             liftMaybe $
               destructionFor
                 (foldMap (hySingleton . occName . fst) bindings)
                 ty
+          edits <- liftMaybe $ hush $
+                mkWorkspaceEdits dflags ccs uri (unTrack pm) $
+                  graftMatchGroup (RealSrcSpan $ unTrack ss) $
+                    noLoc matches
+
           pure $ CodeLens
                 range
                 (Just $ mkLspCommand plId
                   (CommandId "emptycase.complete")
                   ("Complete case constructors (" <> T.pack (unsafeRender ty) <> ")") $
-                    Just $ pure $ toJSON $
-                      WorkspaceEdit
-                        (Just $ HM.singleton uri
-                              $ List
-                              $ pure
-                              $ TextEdit rep_range
-                              $ T.pack
-                              $ mappend "\n"
-                              $ unlines
-                              $ drop 1
-                              $ lines
-                              $ unsafeRender
-                              $ case' (var "_")  matches)
-                        Nothing
-                        Nothing
+                    Just $ pure $ toJSON $ edits
                 )
                 Nothing
-                -- (Just $ Command "Complete case constructors" "emptycase.complete" $
-                --   Just $ List
-                -- Nothing
 completionProvider _ _ _ = pure $ Right $ List []
 
+hush :: Either e a -> Maybe a
+hush (Left _) = Nothing
+hush (Right a) = Just a
 
 codeActionProvider :: PluginMethodHandler IdeState TextDocumentCodeAction
 codeActionProvider state plId (CodeActionParams _ _ (TextDocumentIdentifier uri) (unsafeMkCurrent -> range) _ctx)
@@ -170,7 +159,7 @@ tacticCmd tac pId state (TacticParams uri range var_name)
               case rtr_extract rtr of
                 L _ (HsVar _ (L _ rdr)) | isHole (occName rdr) ->
                   Left NothingToDo
-                _ -> pure $ mkWorkspaceEdits pm_span dflags ccs uri pm rtr
+                _ -> pure $ mkTacticResultEdits pm_span dflags ccs uri pm rtr
 
       case res of
         Nothing -> do
@@ -207,7 +196,7 @@ mkErr code err = ResponseError code err Nothing
 ------------------------------------------------------------------------------
 -- | Turn a 'RunTacticResults' into concrete edits to make in the source
 -- document.
-mkWorkspaceEdits
+mkTacticResultEdits
     :: Tracked age RealSrcSpan
     -> DynFlags
     -> ClientCapabilities
@@ -215,16 +204,45 @@ mkWorkspaceEdits
     -> Tracked age (Annotated ParsedSource)
     -> RunTacticResults
     -> Either UserFacingMessage WorkspaceEdit
-mkWorkspaceEdits (unTrack -> span) dflags ccs uri (unTrack -> pm) rtr = do
+mkTacticResultEdits (unTrack -> span) dflags ccs uri (unTrack -> pm) rtr = do
   for_ (rtr_other_solns rtr) $ \soln -> do
     traceMX "other solution" $ syn_val soln
     traceMX "with score" $ scoreSolution soln (rtr_jdg rtr) []
   traceMX "solution" $ rtr_extract rtr
-  let g = graftHole (RealSrcSpan span) rtr
-      response = transform dflags ccs uri g pm
+  mkWorkspaceEdits dflags ccs uri pm $ graftHole (RealSrcSpan span) rtr
+
+
+------------------------------------------------------------------------------
+-- | Transform a 'Graft' over the AST into a 'WorkspaceEdit'.
+mkWorkspaceEdits
+    :: DynFlags
+    -> ClientCapabilities
+    -> Uri
+    -> Annotated ParsedSource
+    -> Graft (Either String) ParsedSource
+    -> Either UserFacingMessage WorkspaceEdit
+mkWorkspaceEdits dflags ccs uri pm g = do
+  let response = transform dflags ccs uri g pm
    in first (InfrastructureError . T.pack) response
 
 
+instance MonadFail (Either String) where
+  fail = Left
+
+------------------------------------------------------------------------------
+-- | Graft a 'RunTacticResults' into the correct place in an AST. Correctly
+-- deals with top-level holes, in which we might need to fiddle with the
+-- 'Match's that bind variables.
+graftMatchGroup
+    :: SrcSpan
+    -> Located [LMatch GhcPs (LHsExpr GhcPs)]
+    -> Graft (Either String) ParsedSource
+graftMatchGroup ss l = graftExprWithM ss $ \case
+  L span (HsCase ext scrut mg@_) -> do
+    pure $ Just $ L span $ HsCase ext scrut $ mg { mg_alts = l }
+  (_ :: LHsExpr GhcPs) -> pure Nothing
+
+
 ------------------------------------------------------------------------------
 -- | Graft a 'RunTacticResults' into the correct place in an AST. Correctly
 -- deals with top-level holes, in which we might need to fiddle with the

From 4d8b476e3110dd60ee063e51bd8d4081316516f7 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 14 Apr 2021 21:25:15 -0700
Subject: [PATCH 16/31] Tidying and renaming

---
 .../hls-tactics-plugin/src/Wingman/Plugin.hs  | 45 ++++++++++++-------
 1 file changed, 29 insertions(+), 16 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs b/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs
index bf1602f531..dc34ac0f7d 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs
@@ -42,6 +42,10 @@ import           Wingman.Tactics
 import           Wingman.Types
 
 
+emptyCaseLensCommandId :: CommandId
+emptyCaseLensCommandId = CommandId "wingman.emptyCase"
+
+
 descriptor :: PluginId -> PluginDescriptor IdeState
 descriptor plId = (defaultPluginDescriptor plId)
   { pluginCommands
@@ -52,19 +56,23 @@ descriptor plId = (defaultPluginDescriptor plId)
                 (tacticDesc $ tcCommandName tc)
                 (tacticCmd (commandTactic tc) plId))
                 [minBound .. maxBound]
-          , pure $ PluginCommand (CommandId "emptycase.complete") "Complete the empty case" commandHandler
+          , pure $
+              PluginCommand
+              emptyCaseLensCommandId
+              "Complete the empty case"
+              workspaceEditHandler
           ]
   , pluginHandlers = mconcat
       [ mkPluginHandler STextDocumentCodeAction codeActionProvider
-      , mkPluginHandler STextDocumentCodeLens completionProvider
+      , mkPluginHandler STextDocumentCodeLens codeLensProvider
       ]
   , pluginRules = wingmanRules plId
   , pluginCustomConfig =
       mkCustomConfig properties
   }
 
-commandHandler :: CommandFunction IdeState WorkspaceEdit
-commandHandler _ideState wedit = do
+workspaceEditHandler :: CommandFunction IdeState WorkspaceEdit
+workspaceEditHandler _ideState wedit = do
   _ <- sendRequest SWorkspaceApplyEdit (ApplyWorkspaceEditParams Nothing wedit) (\_ -> pure ())
   return $ Right Null
 
@@ -73,8 +81,8 @@ hySingleton :: OccName -> Hypothesis ()
 hySingleton n = Hypothesis . pure $ HyInfo n UserPrv ()
 
 
-completionProvider :: PluginMethodHandler IdeState TextDocumentCodeLens
-completionProvider state plId (CodeLensParams _ _ (TextDocumentIdentifier uri))
+codeLensProvider :: PluginMethodHandler IdeState TextDocumentCodeLens
+codeLensProvider state plId (CodeLensParams _ _ (TextDocumentIdentifier uri))
   | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do
       cfg <- getTacticConfig plId
       ccs <- getClientCapabilities
@@ -86,7 +94,7 @@ completionProvider state plId (CodeLensParams _ _ (TextDocumentIdentifier uri))
         fmap (Right . List) $ for holes $ \(ss, ty) -> do
           binds_ss <- liftMaybe $ mapAgeFrom bind_map ss
           let bindings = getLocalScope (unTrack binds) $ unTrack binds_ss
-          let range = realSrcSpanToRange $ unTrack ss
+              range = realSrcSpanToRange $ unTrack ss
           matches <-
             liftMaybe $
               destructionFor
@@ -97,20 +105,25 @@ completionProvider state plId (CodeLensParams _ _ (TextDocumentIdentifier uri))
                   graftMatchGroup (RealSrcSpan $ unTrack ss) $
                     noLoc matches
 
-          pure $ CodeLens
-                range
-                (Just $ mkLspCommand plId
-                  (CommandId "emptycase.complete")
-                  ("Complete case constructors (" <> T.pack (unsafeRender ty) <> ")") $
-                    Just $ pure $ toJSON $ edits
-                )
-                Nothing
-completionProvider _ _ _ = pure $ Right $ List []
+          pure $
+            CodeLens
+              range
+              (Just
+                $ mkLspCommand
+                    plId
+                    emptyCaseLensCommandId
+                    ("Complete case constructors (" <> T.pack (unsafeRender ty) <> ")")
+                $ Just $ pure $ toJSON $ edits
+              )
+              Nothing
+codeLensProvider _ _ _ = pure $ Right $ List []
+
 
 hush :: Either e a -> Maybe a
 hush (Left _) = Nothing
 hush (Right a) = Just a
 
+
 codeActionProvider :: PluginMethodHandler IdeState TextDocumentCodeAction
 codeActionProvider state plId (CodeActionParams _ _ (TextDocumentIdentifier uri) (unsafeMkCurrent -> range) _ctx)
   | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do

From 0ad5186cae63a6aa2173efe7a3facf8597768887 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 14 Apr 2021 21:35:50 -0700
Subject: [PATCH 17/31] Move EmptyCase into its own module

---
 .../hls-tactics-plugin.cabal                  |   1 +
 .../src/Wingman/EmptyCase.hs                  | 111 ++++++++++++++++++
 .../src/Wingman/Judgements.hs                 |   7 ++
 .../src/Wingman/LanguageServer.hs             |  19 ++-
 .../hls-tactics-plugin/src/Wingman/Plugin.hs  |  97 +--------------
 5 files changed, 138 insertions(+), 97 deletions(-)
 create mode 100644 plugins/hls-tactics-plugin/src/Wingman/EmptyCase.hs

diff --git a/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal b/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal
index aff9d3f087..bd4ba37319 100644
--- a/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal
+++ b/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal
@@ -34,6 +34,7 @@ library
     Wingman.CodeGen.Utils
     Wingman.Context
     Wingman.Debug
+    Wingman.EmptyCase
     Wingman.FeatureSet
     Wingman.GHC
     Wingman.Judgements
diff --git a/plugins/hls-tactics-plugin/src/Wingman/EmptyCase.hs b/plugins/hls-tactics-plugin/src/Wingman/EmptyCase.hs
new file mode 100644
index 0000000000..248fe756ce
--- /dev/null
+++ b/plugins/hls-tactics-plugin/src/Wingman/EmptyCase.hs
@@ -0,0 +1,111 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+-- | A plugin that uses tactics to synthesize code
+module Wingman.EmptyCase where
+
+import           Control.Monad
+import           Control.Monad.Trans
+import           Control.Monad.Trans.Maybe
+import           Data.Aeson
+import           Data.Maybe
+import qualified Data.Text as T
+import           Data.Traversable (for)
+import           Development.IDE (realSrcSpanToRange, GetBindings(..))
+import           Development.IDE.Core.Shake (IdeState (..))
+import           Development.IDE.Core.UseStale (TrackedStale(..), unTrack, mapAgeFrom)
+import           Development.IDE.GHC.Compat
+import           Development.IDE.GHC.ExactPrint
+import           Development.IDE.Spans.LocalBindings (getLocalScope)
+import           Ide.Types
+import           Language.LSP.Server
+import           Language.LSP.Types
+import           OccName
+import           Prelude hiding (span)
+import           Wingman.CodeGen (destructionFor)
+import           Wingman.GHC
+import           Wingman.Judgements (hySingleton)
+import           Wingman.LanguageServer
+import           Wingman.Types
+
+
+emptyCaseLensCommandId :: CommandId
+emptyCaseLensCommandId = CommandId "wingman.emptyCase"
+
+
+workspaceEditHandler :: CommandFunction IdeState WorkspaceEdit
+workspaceEditHandler _ideState wedit = do
+  _ <- sendRequest SWorkspaceApplyEdit (ApplyWorkspaceEditParams Nothing wedit) (\_ -> pure ())
+  return $ Right Null
+
+
+codeLensProvider :: PluginMethodHandler IdeState TextDocumentCodeLens
+codeLensProvider state plId (CodeLensParams _ _ (TextDocumentIdentifier uri))
+  | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do
+      cfg <- getTacticConfig plId
+      ccs <- getClientCapabilities
+      liftIO $ fromMaybeT (Right $ List []) $ do
+        dflags <- getIdeDynflags state nfp
+
+        TrackedStale pm _ <- runStaleIde state nfp GetAnnotatedParsedSource
+        TrackedStale binds bind_map <- runStaleIde state nfp GetBindings
+        holes <- completionForHole  state nfp $ cfg_feature_set cfg
+
+        fmap (Right . List) $ for holes $ \(ss, ty) -> do
+          binds_ss <- liftMaybe $ mapAgeFrom bind_map ss
+          let bindings = getLocalScope (unTrack binds) $ unTrack binds_ss
+              range = realSrcSpanToRange $ unTrack ss
+          matches <-
+            liftMaybe $
+              destructionFor
+                (foldMap (hySingleton . occName . fst) bindings)
+                ty
+          edits <- liftMaybe $ hush $
+                mkWorkspaceEdits dflags ccs uri (unTrack pm) $
+                  graftMatchGroup (RealSrcSpan $ unTrack ss) $
+                    noLoc matches
+
+          pure $
+            CodeLens range
+              (Just
+                $ mkLspCommand
+                    plId
+                    emptyCaseLensCommandId
+                    (mkEmptyCaseLensDesc ty)
+                $ Just $ pure $ toJSON $ edits
+              )
+              Nothing
+codeLensProvider _ _ _ = pure $ Right $ List []
+
+
+mkEmptyCaseLensDesc :: Type -> T.Text
+mkEmptyCaseLensDesc ty =
+  "Complete case constructors (" <> T.pack (unsafeRender ty) <> ")"
+
+
+------------------------------------------------------------------------------
+-- | Silence an error.
+hush :: Either e a -> Maybe a
+hush (Left _) = Nothing
+hush (Right a) = Just a
+
+
+instance MonadFail (Either String) where
+  fail = Left
+
+------------------------------------------------------------------------------
+-- | Graft a 'RunTacticResults' into the correct place in an AST. Correctly
+-- deals with top-level holes, in which we might need to fiddle with the
+-- 'Match's that bind variables.
+graftMatchGroup
+    :: SrcSpan
+    -> Located [LMatch GhcPs (LHsExpr GhcPs)]
+    -> Graft (Either String) ParsedSource
+graftMatchGroup ss l = graftExprWithM ss $ \case
+  L span (HsCase ext scrut mg@_) -> do
+    pure $ Just $ L span $ HsCase ext scrut $ mg { mg_alts = l }
+  (_ :: LHsExpr GhcPs) -> pure Nothing
+
+
+fromMaybeT :: Functor m => a -> MaybeT m a -> m a
+fromMaybeT def = fmap (fromMaybe def) . runMaybeT
+
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Judgements.hs b/plugins/hls-tactics-plugin/src/Wingman/Judgements.hs
index e551e492c9..27cc02e953 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Judgements.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Judgements.hs
@@ -40,6 +40,13 @@ buildHypothesis
       | otherwise = Nothing
 
 
+------------------------------------------------------------------------------
+-- | Build a trivial hypothesis containing only a single name. The corresponding
+-- HyInfo has no provenance or type.
+hySingleton :: OccName -> Hypothesis ()
+hySingleton n = Hypothesis . pure $ HyInfo n UserPrv ()
+
+
 blacklistingDestruct :: Judgement -> Judgement
 blacklistingDestruct =
   field @"_jBlacklistDestruct" .~ True
diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
index 6cd8126a53..590ea17f6d 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
@@ -7,10 +7,11 @@ module Wingman.LanguageServer where
 
 import           ConLike
 import           Control.Applicative (empty)
-import           Control.Arrow
+import           Control.Arrow ((***))
 import           Control.Monad
 import           Control.Monad.State (State, get, put, evalState)
 import           Control.Monad.Trans.Maybe
+import           Data.Bifunctor (first)
 import           Data.Coerce
 import           Data.Functor ((<&>))
 import           Data.Generics.Aliases (mkQ, GenericQ)
@@ -34,6 +35,7 @@ import qualified Development.IDE.Core.Shake as IDE
 import           Development.IDE.Core.UseStale
 import           Development.IDE.GHC.Compat
 import           Development.IDE.GHC.Error (realSrcSpanToRange)
+import           Development.IDE.GHC.ExactPrint
 import           Development.IDE.Spans.LocalBindings (Bindings, getDefiningBindings)
 import           Development.Shake (Action, RuleResult, Rules, action)
 import           Development.Shake.Classes (Typeable, Binary, Hashable, NFData)
@@ -46,6 +48,7 @@ import           Ide.PluginUtils (usePropertyLsp)
 import           Ide.Types (PluginId)
 import           Language.LSP.Server (MonadLsp, sendNotification)
 import           Language.LSP.Types
+import           Language.LSP.Types.Capabilities
 import           OccName
 import           Prelude hiding (span)
 import           SrcLoc (containsSpan)
@@ -557,3 +560,17 @@ mkDiagnostic severity r =
     (Just $ List [DtUnnecessary])
     Nothing
 
+
+------------------------------------------------------------------------------
+-- | Transform a 'Graft' over the AST into a 'WorkspaceEdit'.
+mkWorkspaceEdits
+    :: DynFlags
+    -> ClientCapabilities
+    -> Uri
+    -> Annotated ParsedSource
+    -> Graft (Either String) ParsedSource
+    -> Either UserFacingMessage WorkspaceEdit
+mkWorkspaceEdits dflags ccs uri pm g = do
+  let response = transform dflags ccs uri g pm
+   in first (InfrastructureError . T.pack) response
+
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs b/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs
index dc34ac0f7d..59f99b3052 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs
@@ -12,18 +12,14 @@ import           Control.Monad
 import           Control.Monad.Trans
 import           Control.Monad.Trans.Maybe
 import           Data.Aeson
-import           Data.Bifunctor (first)
 import           Data.Data
 import           Data.Foldable (for_)
 import           Data.Maybe
 import qualified Data.Text as T
-import           Data.Traversable (for)
-import           Development.IDE (realSrcSpanToRange, GetBindings(..))
 import           Development.IDE.Core.Shake (IdeState (..))
 import           Development.IDE.Core.UseStale (Tracked, TrackedStale(..), unTrack, mapAgeFrom, unsafeMkCurrent)
 import           Development.IDE.GHC.Compat
 import           Development.IDE.GHC.ExactPrint
-import           Development.IDE.Spans.LocalBindings (getLocalScope)
 import           Ide.Types
 import           Language.LSP.Server
 import           Language.LSP.Types
@@ -32,7 +28,7 @@ import           OccName
 import           Prelude hiding (span)
 import           System.Timeout
 import           Wingman.CaseSplit
-import           Wingman.CodeGen (destructionFor)
+import           Wingman.EmptyCase
 import           Wingman.GHC
 import           Wingman.LanguageServer
 import           Wingman.LanguageServer.TacticProviders
@@ -42,10 +38,6 @@ import           Wingman.Tactics
 import           Wingman.Types
 
 
-emptyCaseLensCommandId :: CommandId
-emptyCaseLensCommandId = CommandId "wingman.emptyCase"
-
-
 descriptor :: PluginId -> PluginDescriptor IdeState
 descriptor plId = (defaultPluginDescriptor plId)
   { pluginCommands
@@ -71,58 +63,6 @@ descriptor plId = (defaultPluginDescriptor plId)
       mkCustomConfig properties
   }
 
-workspaceEditHandler :: CommandFunction IdeState WorkspaceEdit
-workspaceEditHandler _ideState wedit = do
-  _ <- sendRequest SWorkspaceApplyEdit (ApplyWorkspaceEditParams Nothing wedit) (\_ -> pure ())
-  return $ Right Null
-
-
-hySingleton :: OccName -> Hypothesis ()
-hySingleton n = Hypothesis . pure $ HyInfo n UserPrv ()
-
-
-codeLensProvider :: PluginMethodHandler IdeState TextDocumentCodeLens
-codeLensProvider state plId (CodeLensParams _ _ (TextDocumentIdentifier uri))
-  | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do
-      cfg <- getTacticConfig plId
-      ccs <- getClientCapabilities
-      liftIO $ fromMaybeT (Right $ List []) $ do
-        dflags <- getIdeDynflags state nfp
-        TrackedStale pm _ <- runStaleIde state nfp GetAnnotatedParsedSource
-        TrackedStale binds bind_map <- runStaleIde state nfp GetBindings
-        holes <- completionForHole  state nfp $ cfg_feature_set cfg
-        fmap (Right . List) $ for holes $ \(ss, ty) -> do
-          binds_ss <- liftMaybe $ mapAgeFrom bind_map ss
-          let bindings = getLocalScope (unTrack binds) $ unTrack binds_ss
-              range = realSrcSpanToRange $ unTrack ss
-          matches <-
-            liftMaybe $
-              destructionFor
-                (foldMap (hySingleton . occName . fst) bindings)
-                ty
-          edits <- liftMaybe $ hush $
-                mkWorkspaceEdits dflags ccs uri (unTrack pm) $
-                  graftMatchGroup (RealSrcSpan $ unTrack ss) $
-                    noLoc matches
-
-          pure $
-            CodeLens
-              range
-              (Just
-                $ mkLspCommand
-                    plId
-                    emptyCaseLensCommandId
-                    ("Complete case constructors (" <> T.pack (unsafeRender ty) <> ")")
-                $ Just $ pure $ toJSON $ edits
-              )
-              Nothing
-codeLensProvider _ _ _ = pure $ Right $ List []
-
-
-hush :: Either e a -> Maybe a
-hush (Left _) = Nothing
-hush (Right a) = Just a
-
 
 codeActionProvider :: PluginMethodHandler IdeState TextDocumentCodeAction
 codeActionProvider state plId (CodeActionParams _ _ (TextDocumentIdentifier uri) (unsafeMkCurrent -> range) _ctx)
@@ -225,37 +165,6 @@ mkTacticResultEdits (unTrack -> span) dflags ccs uri (unTrack -> pm) rtr = do
   mkWorkspaceEdits dflags ccs uri pm $ graftHole (RealSrcSpan span) rtr
 
 
-------------------------------------------------------------------------------
--- | Transform a 'Graft' over the AST into a 'WorkspaceEdit'.
-mkWorkspaceEdits
-    :: DynFlags
-    -> ClientCapabilities
-    -> Uri
-    -> Annotated ParsedSource
-    -> Graft (Either String) ParsedSource
-    -> Either UserFacingMessage WorkspaceEdit
-mkWorkspaceEdits dflags ccs uri pm g = do
-  let response = transform dflags ccs uri g pm
-   in first (InfrastructureError . T.pack) response
-
-
-instance MonadFail (Either String) where
-  fail = Left
-
-------------------------------------------------------------------------------
--- | Graft a 'RunTacticResults' into the correct place in an AST. Correctly
--- deals with top-level holes, in which we might need to fiddle with the
--- 'Match's that bind variables.
-graftMatchGroup
-    :: SrcSpan
-    -> Located [LMatch GhcPs (LHsExpr GhcPs)]
-    -> Graft (Either String) ParsedSource
-graftMatchGroup ss l = graftExprWithM ss $ \case
-  L span (HsCase ext scrut mg@_) -> do
-    pure $ Just $ L span $ HsCase ext scrut $ mg { mg_alts = l }
-  (_ :: LHsExpr GhcPs) -> pure Nothing
-
-
 ------------------------------------------------------------------------------
 -- | Graft a 'RunTacticResults' into the correct place in an AST. Correctly
 -- deals with top-level holes, in which we might need to fiddle with the
@@ -308,7 +217,3 @@ graftDecl dflags dst ix make_decl (L src (AMatch (FunRhs (L _ name) _ _) pats _)
         _ -> lift $ Left "annotateDecl didn't produce a funbind"
 graftDecl _ _ _ _ x = pure $ pure x
 
-
-fromMaybeT :: Functor m => a -> MaybeT m a -> m a
-fromMaybeT def = fmap (fromMaybe def) . runMaybeT
-

From a99bad37289f6807593498437dadaf7dde0b301c Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 14 Apr 2021 21:48:03 -0700
Subject: [PATCH 18/31] Don't need the SYB changes after all

---
 .../src/Wingman/Judgements/SYB.hs             | 36 ++++---------------
 1 file changed, 6 insertions(+), 30 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Wingman/Judgements/SYB.hs b/plugins/hls-tactics-plugin/src/Wingman/Judgements/SYB.hs
index 2e318eae17..c1b5fe63c6 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Judgements/SYB.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Judgements/SYB.hs
@@ -4,14 +4,12 @@
 -- | Custom SYB traversals
 module Wingman.Judgements.SYB where
 
-import           Data.Bool (bool)
-import           Data.Foldable (foldl')
-import           Data.Generics hiding (typeRep)
-import qualified Data.Monoid as M
-import           Development.IDE.GHC.Compat
-import           GHC.Exts (Any)
-import           Type.Reflection
-import           Unsafe.Coerce (unsafeCoerce)
+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)
 
 
 ------------------------------------------------------------------------------
@@ -46,28 +44,6 @@ genericIsSubspan dst = mkQ1 (L noSrcSpan ()) Nothing $ \case
   L span _ -> Just $ dst `isSubspanOf` span
 
 
-genericDefinitelyNotIsSubspan
-    :: SrcSpan
-    -> GenericQ (Maybe Bool)
-genericDefinitelyNotIsSubspan dst = mkQ1 (L noSrcSpan ()) Nothing $ \case
-  L span _ -> bool (Just False) Nothing $ dst `isSubspanOf` span
-
-
-smallestQ :: forall r. Monoid r => GenericQ (Maybe Bool) -> GenericQ r -> GenericQ r
-smallestQ q f = snd . go
-  where
-    go :: GenericQ (M.Any, r)
-    go x = do
-      case q x of
-        Nothing -> mconcat $ gmapQ go x
-        Just True ->
-          let it@(r, x') = mconcat $ gmapQ go x
-           in case r of
-                M.Any True -> it
-                M.Any False -> (M.Any True, x' <> f x)
-        Just False -> mempty
-
-
 ------------------------------------------------------------------------------
 -- | Like 'mkQ', but allows for polymorphic instantiation of its specific case.
 -- This instantation matches whenever the dynamic value has the same

From 0e8c57750e905f3de4d1a5b58b8093cb8a06a123 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 14 Apr 2021 21:48:19 -0700
Subject: [PATCH 19/31] Haddock

---
 plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs   | 2 ++
 plugins/hls-tactics-plugin/src/Wingman/EmptyCase.hs | 8 ++++++++
 plugins/hls-tactics-plugin/src/Wingman/GHC.hs       | 4 ++++
 3 files changed, 14 insertions(+)

diff --git a/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs b/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs
index 1fe9844478..12d2d85063 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs
@@ -84,6 +84,8 @@ destructMatches f scrut t jdg = do
             & #syn_val     %~ match [mkDestructPat con names] . unLoc
 
 
+------------------------------------------------------------------------------
+-- | Generate just the 'Match'es for a case split on a specific type.
 destructionFor :: Hypothesis a -> Type -> Maybe [LMatch GhcPs (LHsExpr GhcPs)]
 -- TODO(sandy): In an ideal world, this would be the same codepath as
 -- 'destructMatches'. Make sure to change that if you ever change this.
diff --git a/plugins/hls-tactics-plugin/src/Wingman/EmptyCase.hs b/plugins/hls-tactics-plugin/src/Wingman/EmptyCase.hs
index 248fe756ce..9fcf8d08f0 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/EmptyCase.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/EmptyCase.hs
@@ -28,16 +28,22 @@ import           Wingman.LanguageServer
 import           Wingman.Types
 
 
+------------------------------------------------------------------------------
+-- | The 'CommandId' for the empty case completion.
 emptyCaseLensCommandId :: CommandId
 emptyCaseLensCommandId = CommandId "wingman.emptyCase"
 
 
+------------------------------------------------------------------------------
+-- | A command function that just applies a 'WorkspaceEdit'.
 workspaceEditHandler :: CommandFunction IdeState WorkspaceEdit
 workspaceEditHandler _ideState wedit = do
   _ <- sendRequest SWorkspaceApplyEdit (ApplyWorkspaceEditParams Nothing wedit) (\_ -> pure ())
   return $ Right Null
 
 
+------------------------------------------------------------------------------
+-- | Provide the "empty case completion" code lens
 codeLensProvider :: PluginMethodHandler IdeState TextDocumentCodeLens
 codeLensProvider state plId (CodeLensParams _ _ (TextDocumentIdentifier uri))
   | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do
@@ -77,6 +83,8 @@ codeLensProvider state plId (CodeLensParams _ _ (TextDocumentIdentifier uri))
 codeLensProvider _ _ _ = pure $ Right $ List []
 
 
+------------------------------------------------------------------------------
+-- | The description for the empty case lens.
 mkEmptyCaseLensDesc :: Type -> T.Text
 mkEmptyCaseLensDesc ty =
   "Complete case constructors (" <> T.pack (unsafeRender ty) <> ")"
diff --git a/plugins/hls-tactics-plugin/src/Wingman/GHC.hs b/plugins/hls-tactics-plugin/src/Wingman/GHC.hs
index e719c20e0f..58e9c6d16b 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/GHC.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/GHC.hs
@@ -344,10 +344,14 @@ knownThing f tcg hscenv occ = do
         Just tt -> liftMaybe $ f tt
         _ -> empty
 
+
 liftMaybe :: Monad m => Maybe a -> MaybeT m a
 liftMaybe a = MaybeT $ pure a
 
 
+------------------------------------------------------------------------------
+-- | Get the type of an @HsExpr GhcTc@. This is slow and you should prefer to
+-- not use it, but sometimes it can't be helped.
 typeCheck :: HscEnv -> TcGblEnv -> HsExpr GhcTc -> IO (Maybe Type)
 typeCheck hscenv tcg = fmap snd . initDs hscenv tcg . fmap exprType . dsExpr
 

From 8e6d3a60cde5ebeeca223e43723bb84342667d03 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 14 Apr 2021 21:48:26 -0700
Subject: [PATCH 20/31] Don't need this function either

---
 .../hls-tactics-plugin/src/Wingman/LanguageServer.hs  | 11 -----------
 1 file changed, 11 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
index 590ea17f6d..a48cb82574 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
@@ -289,17 +289,6 @@ getAlreadyDestructed (unTrack -> span) (unTrack -> binds) =
     ) binds
 
 
-getSpanAtCursor
-    :: Tracked age Range
-    -> Tracked age (HieASTs b)
-    -> Maybe (Tracked age RealSrcSpan)
-getSpanAtCursor r@(unTrack -> range) (unTrack -> hf) = do
-  join $ listToMaybe $ M.elems $ flip M.mapWithKey (getAsts hf) $ \fs ast ->
-    case selectSmallestContaining (rangeToRealSrcSpan (FastString.unpackFS fs) range) ast of
-      Nothing -> Nothing
-      Just ast' -> do
-        pure $ unsafeCopyAge r $ nodeSpan ast'
-
 getSpanAndTypeAtHole
     :: Tracked age Range
     -> Tracked age (HieASTs b)

From b1fc26fff2b4fbdea1be406c9039d976d4171caa Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 14 Apr 2021 21:49:43 -0700
Subject: [PATCH 21/31] Revert "Extract the src span of the case's match group"

This reverts commit 23e5d06d5dee2860c143eb8092b4380407a7a7df.
---
 plugins/hls-tactics-plugin/src/Wingman/CaseSplit.hs      | 2 +-
 plugins/hls-tactics-plugin/src/Wingman/GHC.hs            | 6 +++---
 plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs | 4 ++--
 3 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Wingman/CaseSplit.hs b/plugins/hls-tactics-plugin/src/Wingman/CaseSplit.hs
index 1f732f7703..dffb9f30ca 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/CaseSplit.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/CaseSplit.hs
@@ -30,7 +30,7 @@ mkFirstAgda pats body                = AgdaMatch pats body
 -- | Transform an 'AgdaMatch' whose body is a case over a bound pattern, by
 -- splitting it into multiple matches: one for each alternative of the case.
 agdaSplit :: AgdaMatch -> [AgdaMatch]
-agdaSplit (AgdaMatch pats (Case (HsVar _ (L _ var)) _ matches)) = do
+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) $ unLoc body
diff --git a/plugins/hls-tactics-plugin/src/Wingman/GHC.hs b/plugins/hls-tactics-plugin/src/Wingman/GHC.hs
index 58e9c6d16b..83ed6a93fb 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/GHC.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/GHC.hs
@@ -235,10 +235,10 @@ unpackMatches _ = Nothing
 
 ------------------------------------------------------------------------------
 -- | A pattern over the otherwise (extremely) messy AST for lambdas.
-pattern Case :: PatCompattable p => HsExpr p -> SrcSpan -> [(Pat p, LHsExpr p)] -> HsExpr p
-pattern Case scrutinee span matches <-
+pattern Case :: PatCompattable p => HsExpr p -> [(Pat p, LHsExpr p)] -> HsExpr p
+pattern Case scrutinee matches <-
   HsCase _ (L _ scrutinee)
-    (MG {mg_alts = L span (fmap unLoc -> unpackMatches -> Just matches)})
+    (MG {mg_alts = L _ (fmap unLoc -> unpackMatches -> Just matches)})
 
 
 ------------------------------------------------------------------------------
diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
index a48cb82574..3a7082044c 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
@@ -230,7 +230,7 @@ completionForHole state nfp features = do
 
 emptyCaseQ :: GenericQ [(SrcSpan, HsExpr GhcTc)]
 emptyCaseQ = everything (<>) $ mkQ mempty $ \case
-  L case_span (Case scrutinee _ []) -> pure (case_span, scrutinee)
+  L new_span (Case scrutinee []) -> pure (new_span, scrutinee)
   (_ :: LHsExpr GhcTc) -> mempty
 
 
@@ -283,7 +283,7 @@ getAlreadyDestructed
 getAlreadyDestructed (unTrack -> span) (unTrack -> binds) =
   everythingContaining span
     (mkQ mempty $ \case
-      Case (HsVar _ (L _ (occName -> var))) _ _ ->
+      Case (HsVar _ (L _ (occName -> var))) _ ->
         S.singleton var
       (_ :: HsExpr GhcTc) -> mempty
     ) binds

From 57dc63e5e40b56f103208b57a27da2a343345f20 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 14 Apr 2021 21:51:08 -0700
Subject: [PATCH 22/31] Use noExtField for compatability

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

diff --git a/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs b/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs
index 12d2d85063..940cd6f653 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs
@@ -100,10 +100,10 @@ destructionFor hy t = do
             names = mkManyGoodNames (hyNamesInScope hy) args
         pure
           . noLoc
-          . Match noExt CaseAlt [mkDestructPat con names]
-          . GRHSs noExt (pure $ noLoc $ GRHS noExt [] $ noLoc $ var "_")
+          . Match noExtField CaseAlt [mkDestructPat con names]
+          . GRHSs noExtField (pure $ noLoc $ GRHS noExtField [] $ noLoc $ var "_")
           . noLoc
-          $ EmptyLocalBinds noExt
+          $ EmptyLocalBinds noExtField
 
 
 

From efdd3381954da85d574181532743d1d0ecd616d2 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 14 Apr 2021 21:55:13 -0700
Subject: [PATCH 23/31] Use PatCompat for destructionFor

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

diff --git a/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs b/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs
index 940cd6f653..b4390fdb54 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs
@@ -100,7 +100,7 @@ destructionFor hy t = do
             names = mkManyGoodNames (hyNamesInScope hy) args
         pure
           . noLoc
-          . Match noExtField CaseAlt [mkDestructPat con names]
+          . Match noExtField CaseAlt [toPatCompat $ mkDestructPat con names]
           . GRHSs noExtField (pure $ noLoc $ GRHS noExtField [] $ noLoc $ var "_")
           . noLoc
           $ EmptyLocalBinds noExtField

From 8cb7efb40ab1da365964098f67a2d64aa29f96d8 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 14 Apr 2021 21:59:37 -0700
Subject: [PATCH 24/31] Guard behind a feature

---
 plugins/hls-tactics-plugin/src/Wingman/EmptyCase.hs      | 6 ++++--
 plugins/hls-tactics-plugin/src/Wingman/FeatureSet.hs     | 1 +
 plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs | 3 +--
 3 files changed, 6 insertions(+), 4 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Wingman/EmptyCase.hs b/plugins/hls-tactics-plugin/src/Wingman/EmptyCase.hs
index 9fcf8d08f0..84cfe90ce7 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/EmptyCase.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/EmptyCase.hs
@@ -22,6 +22,7 @@ import           Language.LSP.Types
 import           OccName
 import           Prelude hiding (span)
 import           Wingman.CodeGen (destructionFor)
+import           Wingman.FeatureSet
 import           Wingman.GHC
 import           Wingman.Judgements (hySingleton)
 import           Wingman.LanguageServer
@@ -50,11 +51,12 @@ codeLensProvider state plId (CodeLensParams _ _ (TextDocumentIdentifier uri))
       cfg <- getTacticConfig plId
       ccs <- getClientCapabilities
       liftIO $ fromMaybeT (Right $ List []) $ do
-        dflags <- getIdeDynflags state nfp
+        guard $ hasFeature FeatureEmptyCase $ cfg_feature_set cfg
 
+        dflags <- getIdeDynflags state nfp
         TrackedStale pm _ <- runStaleIde state nfp GetAnnotatedParsedSource
         TrackedStale binds bind_map <- runStaleIde state nfp GetBindings
-        holes <- completionForHole  state nfp $ cfg_feature_set cfg
+        holes <- completionForHole state nfp
 
         fmap (Right . List) $ for holes $ \(ss, ty) -> do
           binds_ss <- liftMaybe $ mapAgeFrom bind_map ss
diff --git a/plugins/hls-tactics-plugin/src/Wingman/FeatureSet.hs b/plugins/hls-tactics-plugin/src/Wingman/FeatureSet.hs
index 962e8e5645..edd6bc4be8 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/FeatureSet.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/FeatureSet.hs
@@ -25,6 +25,7 @@ data Feature
   | FeatureUseDataCon
   | FeatureRefineHole
   | FeatureKnownMonoid
+  | FeatureEmptyCase
   deriving (Eq, Ord, Show, Read, Enum, Bounded)
 
 
diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
index 3a7082044c..4c466ffafe 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
@@ -210,9 +210,8 @@ judgementForHole state nfp range features = do
 completionForHole
     :: IdeState
     -> NormalizedFilePath
-    -> FeatureSet
     -> MaybeT IO [(Tracked 'Current RealSrcSpan, Type)]
-completionForHole state nfp features = do
+completionForHole state nfp = do
     TrackedStale tcg tcg_map <- fmap (fmap tmrTypechecked) $ runStaleIde state nfp TypeCheck
     let tcg' = unTrack tcg
     hscenv <- runStaleIde state nfp GhcSessionDeps

From 9805ee8994e16815ba59ed73e1d9b97224bfa625 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 14 Apr 2021 22:04:19 -0700
Subject: [PATCH 25/31] Forgot to move a few more things into EmptyCase

---
 .../src/Wingman/EmptyCase.hs                  | 48 +++++++++++++++++--
 .../src/Wingman/LanguageServer.hs             | 31 +-----------
 2 files changed, 44 insertions(+), 35 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Wingman/EmptyCase.hs b/plugins/hls-tactics-plugin/src/Wingman/EmptyCase.hs
index 84cfe90ce7..abdf9362d4 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/EmptyCase.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/EmptyCase.hs
@@ -3,16 +3,22 @@
 -- | A plugin that uses tactics to synthesize code
 module Wingman.EmptyCase where
 
+import           Control.Applicative (empty)
 import           Control.Monad
 import           Control.Monad.Trans
 import           Control.Monad.Trans.Maybe
 import           Data.Aeson
+import           Data.Generics.Aliases (mkQ, GenericQ)
+import           Data.Generics.Schemes (everything)
 import           Data.Maybe
+import           Data.Monoid
 import qualified Data.Text as T
-import           Data.Traversable (for)
-import           Development.IDE (realSrcSpanToRange, GetBindings(..))
+import           Data.Traversable
+import           Development.IDE (hscEnv)
+import           Development.IDE (realSrcSpanToRange)
+import           Development.IDE.Core.RuleTypes
 import           Development.IDE.Core.Shake (IdeState (..))
-import           Development.IDE.Core.UseStale (TrackedStale(..), unTrack, mapAgeFrom)
+import           Development.IDE.Core.UseStale
 import           Development.IDE.GHC.Compat
 import           Development.IDE.GHC.ExactPrint
 import           Development.IDE.Spans.LocalBindings (getLocalScope)
@@ -21,10 +27,12 @@ import           Language.LSP.Server
 import           Language.LSP.Types
 import           OccName
 import           Prelude hiding (span)
+import           Prelude hiding (span)
+import           TcRnTypes (tcg_binds)
 import           Wingman.CodeGen (destructionFor)
 import           Wingman.FeatureSet
 import           Wingman.GHC
-import           Wingman.Judgements (hySingleton)
+import           Wingman.Judgements
 import           Wingman.LanguageServer
 import           Wingman.Types
 
@@ -56,7 +64,7 @@ codeLensProvider state plId (CodeLensParams _ _ (TextDocumentIdentifier uri))
         dflags <- getIdeDynflags state nfp
         TrackedStale pm _ <- runStaleIde state nfp GetAnnotatedParsedSource
         TrackedStale binds bind_map <- runStaleIde state nfp GetBindings
-        holes <- completionForHole state nfp
+        holes <- emptyCaseScrutinees state nfp
 
         fmap (Right . List) $ for holes $ \(ss, ty) -> do
           binds_ss <- liftMaybe $ mapAgeFrom bind_map ss
@@ -119,3 +127,33 @@ graftMatchGroup ss l = graftExprWithM ss $ \case
 fromMaybeT :: Functor m => a -> MaybeT m a -> m a
 fromMaybeT def = fmap (fromMaybe def) . runMaybeT
 
+
+------------------------------------------------------------------------------
+-- | Find the last typechecked module, and find the most specific span, as well
+-- as the judgement at the given range.
+emptyCaseScrutinees
+    :: IdeState
+    -> NormalizedFilePath
+    -> MaybeT IO [(Tracked 'Current RealSrcSpan, Type)]
+emptyCaseScrutinees state nfp = do
+    TrackedStale tcg tcg_map <- fmap (fmap tmrTypechecked) $ runStaleIde state nfp TypeCheck
+    let tcg' = unTrack tcg
+    hscenv <- runStaleIde state nfp GhcSessionDeps
+    let zz = traverse (emptyCaseQ . tcg_binds) tcg
+
+    for zz $ \aged@(unTrack -> (ss, scrutinee)) -> do
+      ty <- MaybeT $ typeCheck (hscEnv $ untrackedStaleValue hscenv) tcg' scrutinee
+      case ss of
+        RealSrcSpan r   -> do
+          rss' <- liftMaybe $ mapAgeTo tcg_map $ unsafeCopyAge aged r
+          pure (rss', ty)
+        UnhelpfulSpan _ -> empty
+
+
+------------------------------------------------------------------------------
+-- | Get the 'SrcSpan' and scrutinee of every empty case.
+emptyCaseQ :: GenericQ [(SrcSpan, HsExpr GhcTc)]
+emptyCaseQ = everything (<>) $ mkQ mempty $ \case
+  L new_span (Case scrutinee []) -> pure (new_span, scrutinee)
+  (_ :: LHsExpr GhcTc) -> mempty
+
diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
index 4c466ffafe..204bea81fa 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
@@ -6,7 +6,6 @@
 module Wingman.LanguageServer where
 
 import           ConLike
-import           Control.Applicative (empty)
 import           Control.Arrow ((***))
 import           Control.Monad
 import           Control.Monad.State (State, get, put, evalState)
@@ -14,7 +13,7 @@ import           Control.Monad.Trans.Maybe
 import           Data.Bifunctor (first)
 import           Data.Coerce
 import           Data.Functor ((<&>))
-import           Data.Generics.Aliases (mkQ, GenericQ)
+import           Data.Generics.Aliases (mkQ)
 import           Data.Generics.Schemes (everything)
 import qualified Data.HashMap.Strict as Map
 import           Data.IORef (readIORef)
@@ -204,34 +203,6 @@ judgementForHole state nfp range features = do
       pure (fmap realSrcSpanToRange new_rss, jdg, ctx, dflags)
 
 
-------------------------------------------------------------------------------
--- | Find the last typechecked module, and find the most specific span, as well
--- as the judgement at the given range.
-completionForHole
-    :: IdeState
-    -> NormalizedFilePath
-    -> MaybeT IO [(Tracked 'Current RealSrcSpan, Type)]
-completionForHole state nfp = do
-    TrackedStale tcg tcg_map <- fmap (fmap tmrTypechecked) $ runStaleIde state nfp TypeCheck
-    let tcg' = unTrack tcg
-    hscenv <- runStaleIde state nfp GhcSessionDeps
-    let zz = traverse (emptyCaseQ . tcg_binds) tcg
-
-    for zz $ \aged@(unTrack -> (ss, scrutinee)) -> do
-      ty <- MaybeT $ typeCheck (hscEnv $ untrackedStaleValue hscenv) tcg' scrutinee
-      case ss of
-        RealSrcSpan r   -> do
-          rss' <- liftMaybe $ mapAgeTo tcg_map $ unsafeCopyAge aged r
-          pure (rss', ty)
-        UnhelpfulSpan _ -> empty
-
-
-
-emptyCaseQ :: GenericQ [(SrcSpan, HsExpr GhcTc)]
-emptyCaseQ = everything (<>) $ mkQ mempty $ \case
-  L new_span (Case scrutinee []) -> pure (new_span, scrutinee)
-  (_ :: LHsExpr GhcTc) -> mempty
-
 
 mkJudgementAndContext
     :: FeatureSet

From 941f9c278d865931b85fc240bcf22f08079b29c3 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 14 Apr 2021 22:08:25 -0700
Subject: [PATCH 26/31] Remove the orphan instance

---
 .../src/Wingman/EmptyCase.hs                   | 18 ++++++++----------
 1 file changed, 8 insertions(+), 10 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Wingman/EmptyCase.hs b/plugins/hls-tactics-plugin/src/Wingman/EmptyCase.hs
index abdf9362d4..bd4a2d286d 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/EmptyCase.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/EmptyCase.hs
@@ -1,10 +1,10 @@
 {-# LANGUAGE OverloadedStrings #-}
 
--- | A plugin that uses tactics to synthesize code
 module Wingman.EmptyCase where
 
 import           Control.Applicative (empty)
 import           Control.Monad
+import           Control.Monad.Except (runExcept)
 import           Control.Monad.Trans
 import           Control.Monad.Trans.Maybe
 import           Data.Aeson
@@ -107,9 +107,6 @@ hush (Left _) = Nothing
 hush (Right a) = Just a
 
 
-instance MonadFail (Either String) where
-  fail = Left
-
 ------------------------------------------------------------------------------
 -- | Graft a 'RunTacticResults' into the correct place in an AST. Correctly
 -- deals with top-level holes, in which we might need to fiddle with the
@@ -118,10 +115,11 @@ graftMatchGroup
     :: SrcSpan
     -> Located [LMatch GhcPs (LHsExpr GhcPs)]
     -> Graft (Either String) ParsedSource
-graftMatchGroup ss l = graftExprWithM ss $ \case
-  L span (HsCase ext scrut mg@_) -> do
-    pure $ Just $ L span $ HsCase ext scrut $ mg { mg_alts = l }
-  (_ :: LHsExpr GhcPs) -> pure Nothing
+graftMatchGroup ss l =
+  hoistGraft (runExcept . runExceptString) $ graftExprWithM ss $ \case
+    L span (HsCase ext scrut mg@_) -> do
+      pure $ Just $ L span $ HsCase ext scrut $ mg { mg_alts = l }
+    (_ :: LHsExpr GhcPs) -> pure Nothing
 
 
 fromMaybeT :: Functor m => a -> MaybeT m a -> m a
@@ -139,9 +137,9 @@ emptyCaseScrutinees state nfp = do
     TrackedStale tcg tcg_map <- fmap (fmap tmrTypechecked) $ runStaleIde state nfp TypeCheck
     let tcg' = unTrack tcg
     hscenv <- runStaleIde state nfp GhcSessionDeps
-    let zz = traverse (emptyCaseQ . tcg_binds) tcg
 
-    for zz $ \aged@(unTrack -> (ss, scrutinee)) -> do
+    let scrutinees = traverse (emptyCaseQ . tcg_binds) tcg
+    for scrutinees $ \aged@(unTrack -> (ss, scrutinee)) -> do
       ty <- MaybeT $ typeCheck (hscEnv $ untrackedStaleValue hscenv) tcg' scrutinee
       case ss of
         RealSrcSpan r   -> do

From 58d4017d09f5fc15de17b2308824b71c6dde1f1d Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 14 Apr 2021 22:47:20 -0700
Subject: [PATCH 27/31] Add EmptyCase tests

---
 .../hls-tactics-plugin.cabal                  |  1 +
 .../test/CodeLens/EmptyCaseSpec.hs            | 25 +++++++++++++
 plugins/hls-tactics-plugin/test/Utils.hs      | 35 +++++++++++++++++--
 .../test/golden/EmptyCaseADT.hs               |  5 +++
 .../test/golden/EmptyCaseADT.hs.expected      |  8 +++++
 .../test/golden/EmptyCaseApply.hs             |  1 +
 .../test/golden/EmptyCaseApply.hs.expected    |  3 ++
 .../test/golden/EmptyCaseNested.hs            |  3 ++
 .../test/golden/EmptyCaseNested.hs.expected   |  5 +++
 .../test/golden/EmptyCaseParens.hs            |  1 +
 .../test/golden/EmptyCaseParens.hs.expected   |  3 ++
 .../test/golden/EmptyCaseShadow.hs            |  7 ++++
 .../test/golden/EmptyCaseShadow.hs.expected   | 10 ++++++
 13 files changed, 105 insertions(+), 2 deletions(-)
 create mode 100644 plugins/hls-tactics-plugin/test/CodeLens/EmptyCaseSpec.hs
 create mode 100644 plugins/hls-tactics-plugin/test/golden/EmptyCaseADT.hs
 create mode 100644 plugins/hls-tactics-plugin/test/golden/EmptyCaseADT.hs.expected
 create mode 100644 plugins/hls-tactics-plugin/test/golden/EmptyCaseApply.hs
 create mode 100644 plugins/hls-tactics-plugin/test/golden/EmptyCaseApply.hs.expected
 create mode 100644 plugins/hls-tactics-plugin/test/golden/EmptyCaseNested.hs
 create mode 100644 plugins/hls-tactics-plugin/test/golden/EmptyCaseNested.hs.expected
 create mode 100644 plugins/hls-tactics-plugin/test/golden/EmptyCaseParens.hs
 create mode 100644 plugins/hls-tactics-plugin/test/golden/EmptyCaseParens.hs.expected
 create mode 100644 plugins/hls-tactics-plugin/test/golden/EmptyCaseShadow.hs
 create mode 100644 plugins/hls-tactics-plugin/test/golden/EmptyCaseShadow.hs.expected

diff --git a/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal b/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal
index bd4ba37319..eba0f97916 100644
--- a/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal
+++ b/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal
@@ -122,6 +122,7 @@ test-suite tests
     CodeAction.IntrosSpec
     CodeAction.RefineSpec
     CodeAction.UseDataConSpec
+    CodeLens.EmptyCaseSpec
     ProviderSpec
     Spec
     UnificationSpec
diff --git a/plugins/hls-tactics-plugin/test/CodeLens/EmptyCaseSpec.hs b/plugins/hls-tactics-plugin/test/CodeLens/EmptyCaseSpec.hs
new file mode 100644
index 0000000000..7a6aa90116
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/CodeLens/EmptyCaseSpec.hs
@@ -0,0 +1,25 @@
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE DuplicateRecordFields #-}
+{-# LANGUAGE OverloadedStrings     #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE ViewPatterns          #-}
+
+module CodeLens.EmptyCaseSpec where
+
+import Test.Hspec
+import Utils
+import Wingman.FeatureSet (allFeatures)
+
+
+spec :: Spec
+spec = do
+  let test = mkCodeLensTest allFeatures
+
+  describe "golden" $ do
+    test "EmptyCaseADT.hs"
+    test "EmptyCaseShadow.hs"
+    test "EmptyCaseParens.hs"
+    test "EmptyCaseNested.hs"
+    test "EmptyCaseApply.hs"
+
diff --git a/plugins/hls-tactics-plugin/test/Utils.hs b/plugins/hls-tactics-plugin/test/Utils.hs
index 37f93e16e2..2e78105682 100644
--- a/plugins/hls-tactics-plugin/test/Utils.hs
+++ b/plugins/hls-tactics-plugin/test/Utils.hs
@@ -9,7 +9,7 @@ module Utils where
 
 import           Control.DeepSeq (deepseq)
 import qualified Control.Exception as E
-import           Control.Lens hiding (failing, (<.>), (.=))
+import           Control.Lens hiding (List, failing, (<.>), (.=))
 import           Control.Monad (unless)
 import           Control.Monad.IO.Class
 import           Data.Aeson
@@ -29,11 +29,11 @@ import           System.FilePath
 import           Test.Hls
 import           Test.Hspec
 import           Test.Hspec.Formatters (FailureReason(ExpectedButGot))
-import           Test.Tasty.HUnit (Assertion, HUnitFailure(..))
 import           Wingman.FeatureSet (FeatureSet, allFeatures, prettyFeatureSet)
 import           Wingman.LanguageServer (mkShowMessageParams)
 import           Wingman.Types
 
+
 plugin :: PluginDescriptor IdeState
 plugin = Tactic.descriptor "tactics"
 
@@ -126,6 +126,37 @@ mkGoldenTest eq features tc occ line col input =
       expected <- liftIO $ T.readFile expected_name
       liftIO $ edited `eq` expected
 
+
+mkCodeLensTest
+    :: FeatureSet
+    -> FilePath
+    -> SpecWith ()
+mkCodeLensTest features input =
+  it (input <> " (golden)") $ do
+    runSessionWithServer plugin tacticPath $ do
+      setFeatureSet features
+      doc <- openDoc input "haskell"
+      _ <- waitForDiagnostics
+      lenses <- fmap (reverse . filter isWingmanLens) $ getCodeLenses doc
+      for_ lenses $ \(CodeLens _ (Just cmd) _) ->
+        executeCommand cmd
+      _resp <- skipManyTill anyMessage (message SWorkspaceApplyEdit)
+      edited <- documentContents doc
+      let expected_name = input <.> "expected"
+      -- Write golden tests if they don't already exist
+      liftIO $ (doesFileExist expected_name >>=) $ flip unless $ do
+        T.writeFile expected_name edited
+      expected <- liftIO $ T.readFile expected_name
+      liftIO $ edited `shouldBe` expected
+
+
+
+isWingmanLens :: CodeLens -> Bool
+isWingmanLens (CodeLens _ (Just (Command _ cmd _)) _)
+    = T.isInfixOf ":tactics:" cmd
+isWingmanLens _ = False
+
+
 mkShowMessageTest
     :: FeatureSet
     -> TacticCommand
diff --git a/plugins/hls-tactics-plugin/test/golden/EmptyCaseADT.hs b/plugins/hls-tactics-plugin/test/golden/EmptyCaseADT.hs
new file mode 100644
index 0000000000..37d3b6c357
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/EmptyCaseADT.hs
@@ -0,0 +1,5 @@
+data Foo = A Int | B Bool | C
+
+foo :: Foo -> ()
+foo x = case x of
+
diff --git a/plugins/hls-tactics-plugin/test/golden/EmptyCaseADT.hs.expected b/plugins/hls-tactics-plugin/test/golden/EmptyCaseADT.hs.expected
new file mode 100644
index 0000000000..199bbb0db9
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/EmptyCaseADT.hs.expected
@@ -0,0 +1,8 @@
+data Foo = A Int | B Bool | C
+
+foo :: Foo -> ()
+foo x = case x of
+  A i -> _
+  B b -> _
+  C -> _
+
diff --git a/plugins/hls-tactics-plugin/test/golden/EmptyCaseApply.hs b/plugins/hls-tactics-plugin/test/golden/EmptyCaseApply.hs
new file mode 100644
index 0000000000..29647e2cda
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/EmptyCaseApply.hs
@@ -0,0 +1 @@
+blah = case show 5 of
diff --git a/plugins/hls-tactics-plugin/test/golden/EmptyCaseApply.hs.expected b/plugins/hls-tactics-plugin/test/golden/EmptyCaseApply.hs.expected
new file mode 100644
index 0000000000..fe22299c93
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/EmptyCaseApply.hs.expected
@@ -0,0 +1,3 @@
+blah = case show 5 of
+  [] -> _
+  c : l_c -> _
diff --git a/plugins/hls-tactics-plugin/test/golden/EmptyCaseNested.hs b/plugins/hls-tactics-plugin/test/golden/EmptyCaseNested.hs
new file mode 100644
index 0000000000..a72781a7c6
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/EmptyCaseNested.hs
@@ -0,0 +1,3 @@
+test =
+  case (case (Just "") of) of
+    True -> _
diff --git a/plugins/hls-tactics-plugin/test/golden/EmptyCaseNested.hs.expected b/plugins/hls-tactics-plugin/test/golden/EmptyCaseNested.hs.expected
new file mode 100644
index 0000000000..10c6925951
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/EmptyCaseNested.hs.expected
@@ -0,0 +1,5 @@
+test =
+  case (case (Just "") of
+  Nothing -> _
+  Just l_c -> _) of
+    True -> _
diff --git a/plugins/hls-tactics-plugin/test/golden/EmptyCaseParens.hs b/plugins/hls-tactics-plugin/test/golden/EmptyCaseParens.hs
new file mode 100644
index 0000000000..2ac71b042e
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/EmptyCaseParens.hs
@@ -0,0 +1 @@
+test = True && case True of
diff --git a/plugins/hls-tactics-plugin/test/golden/EmptyCaseParens.hs.expected b/plugins/hls-tactics-plugin/test/golden/EmptyCaseParens.hs.expected
new file mode 100644
index 0000000000..18aacf2ae2
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/EmptyCaseParens.hs.expected
@@ -0,0 +1,3 @@
+test = True && (case True of
+   False -> _
+   True -> _)
diff --git a/plugins/hls-tactics-plugin/test/golden/EmptyCaseShadow.hs b/plugins/hls-tactics-plugin/test/golden/EmptyCaseShadow.hs
new file mode 100644
index 0000000000..c57af5b849
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/EmptyCaseShadow.hs
@@ -0,0 +1,7 @@
+data Foo = A Int | B Bool | C
+
+-- Make sure we don't shadow the i and b bindings when we empty case
+-- split
+foo :: Int -> Bool -> Foo -> ()
+foo i b x = case x of
+
diff --git a/plugins/hls-tactics-plugin/test/golden/EmptyCaseShadow.hs.expected b/plugins/hls-tactics-plugin/test/golden/EmptyCaseShadow.hs.expected
new file mode 100644
index 0000000000..d35cf1a1f5
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/EmptyCaseShadow.hs.expected
@@ -0,0 +1,10 @@
+data Foo = A Int | B Bool | C
+
+-- Make sure we don't shadow the i and b bindings when we empty case
+-- split
+foo :: Int -> Bool -> Foo -> ()
+foo i b x = case x of
+  A i3 -> _
+  B b3 -> _
+  C -> _
+

From a5be902cd5c0ac812a9c3258eb7d3ecef0251092 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 14 Apr 2021 22:49:40 -0700
Subject: [PATCH 28/31] Seriously fuck hlint

---
 ghcide/src/Development/IDE/Core/UseStale.hs | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/ghcide/src/Development/IDE/Core/UseStale.hs b/ghcide/src/Development/IDE/Core/UseStale.hs
index f82a7a9e57..8ea736b7a9 100644
--- a/ghcide/src/Development/IDE/Core/UseStale.hs
+++ b/ghcide/src/Development/IDE/Core/UseStale.hs
@@ -3,8 +3,6 @@
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE RankNTypes     #-}
 
-{-# OPTIONS_GHC -fno-warn-unused-top-binds #-}
-
 module Development.IDE.Core.UseStale
   ( Age(..)
   , Tracked
@@ -60,7 +58,7 @@ newtype Tracked (age :: Age) a  = UnsafeTracked
 -- change. Use the 'Category' instance to compose 'PositionMapping's in order
 -- to transform between values of different stale ages.
 newtype PositionMap (from :: Age) (to :: Age) = PositionMap
-  { getPositionMapping :: P.PositionMapping
+  { _getPositionMapping :: P.PositionMapping
   }
 
 instance Category PositionMap where

From e1cb51e6793e7ed64fd5e6acfc9e7f23d6b251ff Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 14 Apr 2021 22:54:13 -0700
Subject: [PATCH 29/31] GADT apartness test

---
 .../test/CodeLens/EmptyCaseSpec.hs                  |  1 +
 .../hls-tactics-plugin/test/golden/EmptyCaseGADT.hs | 11 +++++++++++
 .../test/golden/EmptyCaseGADT.hs.expected           | 13 +++++++++++++
 3 files changed, 25 insertions(+)
 create mode 100644 plugins/hls-tactics-plugin/test/golden/EmptyCaseGADT.hs
 create mode 100644 plugins/hls-tactics-plugin/test/golden/EmptyCaseGADT.hs.expected

diff --git a/plugins/hls-tactics-plugin/test/CodeLens/EmptyCaseSpec.hs b/plugins/hls-tactics-plugin/test/CodeLens/EmptyCaseSpec.hs
index 7a6aa90116..c670697c6d 100644
--- a/plugins/hls-tactics-plugin/test/CodeLens/EmptyCaseSpec.hs
+++ b/plugins/hls-tactics-plugin/test/CodeLens/EmptyCaseSpec.hs
@@ -22,4 +22,5 @@ spec = do
     test "EmptyCaseParens.hs"
     test "EmptyCaseNested.hs"
     test "EmptyCaseApply.hs"
+    test "EmptyCaseGADT.hs"
 
diff --git a/plugins/hls-tactics-plugin/test/golden/EmptyCaseGADT.hs b/plugins/hls-tactics-plugin/test/golden/EmptyCaseGADT.hs
new file mode 100644
index 0000000000..ba08ddae54
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/EmptyCaseGADT.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE GADTs #-}
+
+data GADT a where
+  MyInt :: GADT Int
+  MyBool :: GADT Bool
+  MyVar :: GADT a
+
+
+test :: GADT Int -> GADT Bool
+test x = case x of
+
diff --git a/plugins/hls-tactics-plugin/test/golden/EmptyCaseGADT.hs.expected b/plugins/hls-tactics-plugin/test/golden/EmptyCaseGADT.hs.expected
new file mode 100644
index 0000000000..409be2aa03
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/EmptyCaseGADT.hs.expected
@@ -0,0 +1,13 @@
+{-# LANGUAGE GADTs #-}
+
+data GADT a where
+  MyInt :: GADT Int
+  MyBool :: GADT Bool
+  MyVar :: GADT a
+
+
+test :: GADT Int -> GADT Bool
+test x = case x of
+  MyInt -> _
+  MyVar -> _
+

From 54abd75d40c5744f330cc26dc578d308a479c0af Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Thu, 15 Apr 2021 08:53:53 -0700
Subject: [PATCH 30/31] Fix splice test

---
 plugins/hls-splice-plugin/test/testdata/TTypeAppExp.hs.expected | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/plugins/hls-splice-plugin/test/testdata/TTypeAppExp.hs.expected b/plugins/hls-splice-plugin/test/testdata/TTypeAppExp.hs.expected
index 0dc0e40f2a..b74d153ee2 100644
--- a/plugins/hls-splice-plugin/test/testdata/TTypeAppExp.hs.expected
+++ b/plugins/hls-splice-plugin/test/testdata/TTypeAppExp.hs.expected
@@ -4,4 +4,4 @@ module TTypeAppExp where
 import Data.Proxy
 
 f :: Proxy Int
-f = (Proxy @Int)
+f = Proxy @Int

From 471d22d7acf8fc07f1b7c6b33033cf80b754e82e Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Thu, 15 Apr 2021 08:59:34 -0700
Subject: [PATCH 31/31] Don't forget about branding!

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

diff --git a/plugins/hls-tactics-plugin/src/Wingman/EmptyCase.hs b/plugins/hls-tactics-plugin/src/Wingman/EmptyCase.hs
index bd4a2d286d..c4635ca40d 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/EmptyCase.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/EmptyCase.hs
@@ -97,7 +97,7 @@ codeLensProvider _ _ _ = pure $ Right $ List []
 -- | The description for the empty case lens.
 mkEmptyCaseLensDesc :: Type -> T.Text
 mkEmptyCaseLensDesc ty =
-  "Complete case constructors (" <> T.pack (unsafeRender ty) <> ")"
+  "Wingman: Complete case constructors (" <> T.pack (unsafeRender ty) <> ")"
 
 
 ------------------------------------------------------------------------------