From 4552fb80226e351b32f7d270649562d71123542c Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Fri, 12 Feb 2021 12:45:37 -0800
Subject: [PATCH 01/38] Agda splitting machinery

---
 .../src/Ide/Plugin/Tactic/GHC.hs              | 112 +++++++++++++++++-
 .../src/Ide/Plugin/Tactic/Types.hs            |   6 +
 2 files changed, 113 insertions(+), 5 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
index 5cba1d20b6..854c1aa7d8 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
@@ -1,17 +1,21 @@
-{-# LANGUAGE CPP              #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE PatternSynonyms  #-}
-{-# LANGUAGE ViewPatterns     #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE CPP               #-}
+{-# LANGUAGE FlexibleContexts  #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE PatternSynonyms   #-}
+{-# LANGUAGE TypeApplications  #-}
+{-# LANGUAGE ViewPatterns      #-}
 
 module Ide.Plugin.Tactic.GHC where
 
+import Control.Arrow
 import           Control.Monad.State
 import qualified Data.Map as M
 import           Data.Maybe (isJust)
 import           Data.Traversable
 import qualified DataCon as DataCon
 import           Development.IDE.GHC.Compat
-import           Generics.SYB (mkT, everywhere)
+import           Generics.SYB (Data, mkT, everywhere)
 import           Ide.Plugin.Tactic.Types
 import           OccName
 import           TcType
@@ -20,6 +24,9 @@ import           Type
 import           TysWiredIn (intTyCon, floatTyCon, doubleTyCon, charTyCon)
 import           Unique
 import           Var
+import GHC.SourceGen (int, var, bvar, match, case', lambda)
+import Control.Lens
+import GHC.SourceGen.Pat
 
 tcTyVar_maybe :: Type -> Maybe Var
 tcTyVar_maybe ty | Just ty' <- tcView ty = tcTyVar_maybe ty'
@@ -100,6 +107,101 @@ algebraicTyCon (splitTyConApp_maybe -> Just (tycon, _))
   | otherwise = Just tycon
 algebraicTyCon _ = Nothing
 
+
+data AgdaMatch = AgdaMatch
+  { amPats :: [Pat GhcPs]
+  , amBody :: HsExpr GhcPs
+  }
+  deriving (Show)
+
+
+agdaSplit :: AgdaMatch -> [AgdaMatch]
+agdaSplit (AgdaMatch pats (Lambda pats' body)) =
+  agdaSplit (AgdaMatch (pats <> pats') body)
+agdaSplit (AgdaMatch pats (Case (HsVar _ (L _ var)) matches)) = do
+  (i, pat) <- zip [id @Int 0 ..] pats
+  case pat of
+    VarPat _ (L _ patname) | patname == var -> do
+      (case_pat, body) <- matches
+      -- TODO(sandy): use an at pattern if necessar
+      pure $ AgdaMatch (pats & ix i .~ case_pat) body
+    _ -> []
+agdaSplit x = [x]
+
+
+iterateSplit :: AgdaMatch -> [AgdaMatch]
+iterateSplit am =
+  let iterated =  iterate (agdaSplit =<<) $ pure am
+   in fst . head
+          . dropWhile (\(a, b) -> length a /= length b)
+          . zip iterated
+          $ tail iterated
+
+
+------------------------------------------------------------------------------
+-- | A pattern over the otherwise (extremely) messy AST for lambdas.
+pattern Lambda :: [Pat GhcPs] -> HsExpr GhcPs -> HsExpr GhcPs
+pattern Lambda pats body <-
+  HsLam _
+    (MG {mg_alts = L _ [L _
+      (Match { m_pats = pats
+             , m_grhss = UnguardedRHSs body
+             })]})
+  where
+    -- If there are no patterns to bind, just stick in the body
+    Lambda [] body   = body
+    Lambda pats body = lambda pats body
+
+
+pattern UnguardedRHSs :: HsExpr GhcPs -> GRHSs GhcPs (LHsExpr GhcPs)
+pattern UnguardedRHSs body <-
+  GRHSs {grhssGRHSs = [L _ (GRHS _ [] (L _ body))]}
+
+
+pattern SinglePatMatch :: Pat GhcPs -> HsExpr GhcPs -> Match GhcPs (LHsExpr GhcPs)
+pattern SinglePatMatch pat body <-
+  Match { m_pats = [pat]
+        , m_grhss = UnguardedRHSs body
+        }
+
+
+unpackMatches :: [Match GhcPs (LHsExpr GhcPs)] -> Maybe [(Pat GhcPs, HsExpr GhcPs)]
+unpackMatches [] = Just []
+unpackMatches (SinglePatMatch pat body : matches) =
+  (:) <$> pure (pat, body) <*> unpackMatches matches
+unpackMatches _ = Nothing
+
+
+------------------------------------------------------------------------------
+-- | A pattern over the otherwise (extremely) messy AST for lambdas.
+pattern Case :: HsExpr GhcPs -> [(Pat GhcPs, HsExpr GhcPs)] -> HsExpr GhcPs
+pattern Case scrutinee matches <-
+  HsCase _ (L _ scrutinee)
+    (MG {mg_alts = L _ (fmap unLoc -> unpackMatches -> Just matches)})
+  where
+    Case scrutinee matches =
+      case' scrutinee $ fmap (\(pat, body) -> match [pat] body) matches
+
+test :: HsExpr GhcPs
+test =
+  Lambda [bvar "b", bvar "c"] $ Case (var "c")
+    [ (conP "True" [], var "True")
+    , (conP "False" [],
+        Case (var "b")
+          [ (int 0, var "b")
+          , (wildP, int 5)
+          ]
+      )
+    ]
+
+testAgda :: AgdaMatch
+testAgda = AgdaMatch [bvar "a"] test
+
+
+
+
+
+
 ------------------------------------------------------------------------------
 -- | Can ths type be lambda-cased?
 --
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs
index ac0ab3dff1..c1879591d6 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs
@@ -70,6 +70,12 @@ instance Show DataCon where
 instance Show Class where
   show  = unsafeRender
 
+instance Show (HsExpr GhcPs) where
+  show  = unsafeRender
+
+instance Show (Pat GhcPs) where
+  show  = unsafeRender
+
 
 ------------------------------------------------------------------------------
 data TacticState = TacticState

From 81c74118eb95241ad12217ca934fc581d5538331 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Fri, 12 Feb 2021 14:23:55 -0800
Subject: [PATCH 02/38] Expand decls!

---
 ghcide/src/Development/IDE/GHC/ExactPrint.hs  | 54 ++++++++++++++++++-
 .../src/Ide/Plugin/Tactic.hs                  | 12 ++++-
 .../src/Ide/Plugin/Tactic/GHC.hs              | 11 +++-
 3 files changed, 74 insertions(+), 3 deletions(-)

diff --git a/ghcide/src/Development/IDE/GHC/ExactPrint.hs b/ghcide/src/Development/IDE/GHC/ExactPrint.hs
index b0636174a1..610a94689e 100644
--- a/ghcide/src/Development/IDE/GHC/ExactPrint.hs
+++ b/ghcide/src/Development/IDE/GHC/ExactPrint.hs
@@ -14,6 +14,7 @@ module Development.IDE.GHC.ExactPrint
       hoistGraft,
       graftWithM,
       graftWithSmallestM,
+      graftSmallestDecls,
       transform,
       transformM,
       useAnnotatedSource,
@@ -61,6 +62,10 @@ import Retrie.ExactPrint hiding (parseDecl, parseExpr, parsePattern, parseType)
 import Parser (parseIdentifier)
 #if __GLASGOW_HASKELL__ == 808
 import Control.Arrow
+import Data.List (isPrefixOf)
+import Data.Traversable (for)
+import Data.Foldable (Foldable(fold))
+import Debug.Trace (traceM)
 #endif
 
 
@@ -191,6 +196,36 @@ graft dst val = Graft $ \dflags a -> do
             )
             a
 
+
+parseDecls :: DynFlags -> FilePath -> String -> ParseResult (LHsDecl GhcPs)
+parseDecls dflags fp str = do
+  let mono_decls = fmap unlines $ groupByFirstLine $ lines str
+  decls <- for (zip [0..] mono_decls) $ \(ix, line) -> parseDecl dflags (fp <> show ix) line
+  pure $ mergeDecls decls
+
+
+mergeDecls :: [(Anns, LHsDecl GhcPs)] -> (Anns, LHsDecl GhcPs)
+mergeDecls [x] = x
+mergeDecls ((anns,  L _ (ValD ext fb@FunBind{fun_matches = mg@MG {mg_alts = L _ alts}}))
+          : (anns', L _ (ValD _ FunBind{fun_matches = MG {mg_alts = L _ [alt]}}))
+          : decls) =
+  mergeDecls $
+    ( anns <> setPrecedingLines alt 1 0 anns'
+    , noLoc $ ValD ext $ fb
+        { fun_matches = mg { mg_alts = noLoc $ alts <> [alt] }
+        }
+    ) : decls
+mergeDecls _ = error "huh"
+
+
+groupByFirstLine :: [String] -> [[String]]
+groupByFirstLine [] = []
+groupByFirstLine (str : strs) =
+  let (same, diff) = span (isPrefixOf " ") strs
+   in (str : same) : groupByFirstLine diff
+
+
+
 ------------------------------------------------------------------------------
 
 graftWithM ::
@@ -260,6 +295,23 @@ graftDecls dst decs0 = Graft $ \dflags a -> do
             | otherwise = DL.singleton (L src e) <> go rest
     modifyDeclsT (pure . DL.toList . go) a
 
+graftSmallestDecls ::
+    forall a.
+    (HasDecls a) =>
+    SrcSpan ->
+    [LHsDecl GhcPs] ->
+    Graft (Either String) a
+graftSmallestDecls dst decs0 = Graft $ \dflags a -> do
+    decs <- forM decs0 $ \decl -> do
+        (anns, decl') <- annotateDecl dflags decl
+        modifyAnnsT $ mappend anns
+        pure decl'
+    let go [] = DL.empty
+        go (L src e : rest)
+            | dst `isSubspanOf` src = DL.fromList decs <> DL.fromList rest
+            | otherwise = DL.singleton (L src e) <> go rest
+    modifyDeclsT (pure . DL.toList . go) a
+
 graftDeclsWithM ::
     forall a m.
     (HasDecls a, Fail.MonadFail m) =>
@@ -347,7 +399,7 @@ annotateDecl :: DynFlags -> LHsDecl GhcPs -> TransformT (Either String) (Anns, L
 annotateDecl dflags ast = do
     uniq <- show <$> uniqueSrcSpanT
     let rendered = render dflags ast
-    (anns, expr') <- lift $ mapLeft show $ parseDecl dflags uniq rendered
+    (anns, expr') <- lift $ mapLeft show $ parseDecls dflags uniq rendered
     let anns' = setPrecedingLines expr' 1 0 anns
     pure (anns', expr')
 ------------------------------------------------------------------------------
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
index 5182161f25..ae5e7ae4a0 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
@@ -63,6 +63,7 @@ import           Refinery.Tactic (goal)
 import           SrcLoc (containsSpan)
 import           System.Timeout
 import           TcRnTypes (tcg_binds)
+import Development.IDE.GHC.ExactPrint (graftSmallestDecls)
 
 
 descriptor :: PluginId -> PluginDescriptor IdeState
@@ -327,7 +328,16 @@ tacticCmd tac lf state (TacticParams uri range var_name)
                 $ ResponseError InvalidRequest (T.pack $ show err) Nothing
             Right rtr -> do
               traceMX "solns" $ rtr_other_solns rtr
-              let g = graft (RealSrcSpan span) $ rtr_extract rtr
+              let g =
+                    if _jIsTopHole jdg
+                       then graftSmallestDecls (RealSrcSpan span)
+                          $ pure
+                          $ splitToDecl (fst $ last $ ctxDefiningFuncs ctx)
+                          $ iterateSplit $ AgdaMatch []
+                          $ unLoc
+                          $ rtr_extract rtr
+                       else graft (RealSrcSpan span)
+                          $ rtr_extract rtr
                   response = transform dflags (clientCapabilities lf) uri g pm
               pure $ case response of
                 Right res -> (Right Null , Just (WorkspaceApplyEdit, ApplyWorkspaceEditParams res))
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
index 854c1aa7d8..d56791f3c1 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
@@ -24,9 +24,10 @@ import           Type
 import           TysWiredIn (intTyCon, floatTyCon, doubleTyCon, charTyCon)
 import           Unique
 import           Var
-import GHC.SourceGen (int, var, bvar, match, case', lambda)
+import GHC.SourceGen (funBinds, funBind, int, var, bvar, match, case', lambda)
 import Control.Lens
 import GHC.SourceGen.Pat
+import GHC.Exts (IsString(fromString))
 
 tcTyVar_maybe :: Type -> Maybe Var
 tcTyVar_maybe ty | Just ty' <- tcView ty = tcTyVar_maybe ty'
@@ -129,6 +130,12 @@ agdaSplit (AgdaMatch pats (Case (HsVar _ (L _ var)) matches)) = do
 agdaSplit x = [x]
 
 
+splitToDecl :: OccName -> [AgdaMatch] -> LHsDecl GhcPs
+splitToDecl name ams = noLoc $ funBinds (fromString . occNameString . occName $ name) $ do
+  AgdaMatch pats body <- ams
+  pure $ match pats body
+
+
 iterateSplit :: AgdaMatch -> [AgdaMatch]
 iterateSplit am =
   let iterated =  iterate (agdaSplit =<<) $ pure am
@@ -138,6 +145,8 @@ iterateSplit am =
           $ tail iterated
 
 
+
+
 ------------------------------------------------------------------------------
 -- | A pattern over the otherwise (extremely) messy AST for lambdas.
 pattern Lambda :: [Pat GhcPs] -> HsExpr GhcPs -> HsExpr GhcPs

From bf4e67087b933a92398d7eeccc731eb0213932cb Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Fri, 12 Feb 2021 14:35:19 -0800
Subject: [PATCH 03/38] Only very top-level lambda to args

---
 plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs     | 3 ++-
 plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs | 9 +++++++--
 2 files changed, 9 insertions(+), 3 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
index ae5e7ae4a0..436286d706 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
@@ -333,7 +333,8 @@ tacticCmd tac lf state (TacticParams uri range var_name)
                        then graftSmallestDecls (RealSrcSpan span)
                           $ pure
                           $ splitToDecl (fst $ last $ ctxDefiningFuncs ctx)
-                          $ iterateSplit $ AgdaMatch []
+                          $ iterateSplit
+                          $ mkFirstAgda
                           $ unLoc
                           $ rtr_extract rtr
                        else graft (RealSrcSpan span)
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
index d56791f3c1..91cfc1ab73 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
@@ -116,9 +116,14 @@ data AgdaMatch = AgdaMatch
   deriving (Show)
 
 
+mkFirstAgda :: HsExpr GhcPs -> AgdaMatch
+mkFirstAgda = go []
+  where
+    go pats (Lambda pats' body) = go (pats <> pats') body
+    go pats body = AgdaMatch pats body
+
+
 agdaSplit :: AgdaMatch -> [AgdaMatch]
-agdaSplit (AgdaMatch pats (Lambda pats' body)) =
-  agdaSplit (AgdaMatch (pats <> pats') body)
 agdaSplit (AgdaMatch pats (Case (HsVar _ (L _ var)) matches)) = do
   (i, pat) <- zip [id @Int 0 ..] pats
   case pat of

From ee2094e53060c9c51f0776c02c03e9391ee2d229 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Fri, 12 Feb 2021 14:41:51 -0800
Subject: [PATCH 04/38] Preserve top-level args (but it doesnt work very well)

---
 plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs     | 7 +++++++
 plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs | 8 +++-----
 2 files changed, 10 insertions(+), 5 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
index 436286d706..9e1d6f6322 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
@@ -15,6 +15,7 @@ module Ide.Plugin.Tactic
   , TacticCommand (..)
   ) where
 
+
 import           Control.Arrow
 import           Control.Monad
 import           Control.Monad.Error.Class (MonadError(throwError))
@@ -54,6 +55,7 @@ import           Ide.Plugin.Tactic.Range
 import           Ide.Plugin.Tactic.Tactics
 import           Ide.Plugin.Tactic.TestTypes
 import           Ide.Plugin.Tactic.Types
+import           Ide.Plugin.Tactic.CodeGen (bvar')
 import           Ide.PluginUtils
 import           Ide.Types
 import           Language.Haskell.LSP.Core (clientCapabilities)
@@ -335,6 +337,11 @@ tacticCmd tac lf state (TacticParams uri range var_name)
                           $ splitToDecl (fst $ last $ ctxDefiningFuncs ctx)
                           $ iterateSplit
                           $ mkFirstAgda
+                              ( fmap (bvar' . hi_name)
+                              . filter (isTopLevel . hi_provenance)
+                              . unHypothesis
+                              $ jHypothesis jdg
+                              )
                           $ unLoc
                           $ rtr_extract rtr
                        else graft (RealSrcSpan span)
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
index 91cfc1ab73..246219c770 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
@@ -116,11 +116,9 @@ data AgdaMatch = AgdaMatch
   deriving (Show)
 
 
-mkFirstAgda :: HsExpr GhcPs -> AgdaMatch
-mkFirstAgda = go []
-  where
-    go pats (Lambda pats' body) = go (pats <> pats') body
-    go pats body = AgdaMatch pats body
+mkFirstAgda :: [Pat GhcPs] -> HsExpr GhcPs -> AgdaMatch
+mkFirstAgda pats (Lambda pats' body) = mkFirstAgda (pats <> pats') body
+mkFirstAgda pats body = AgdaMatch pats body
 
 
 agdaSplit :: AgdaMatch -> [AgdaMatch]

From cf75b1e3d986347d0c96feceaba9c3cec61bc364 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Sat, 13 Feb 2021 16:07:08 -0800
Subject: [PATCH 05/38] Preserve existing patterns and matches when
 agdasplitting

---
 ghcide/src/Development/IDE/GHC/ExactPrint.hs  | 26 ++++++++++--
 .../src/Ide/Plugin/Tactic.hs                  | 41 +++++++++++++++----
 .../src/Ide/Plugin/Tactic/GHC.hs              | 36 ++++------------
 3 files changed, 64 insertions(+), 39 deletions(-)

diff --git a/ghcide/src/Development/IDE/GHC/ExactPrint.hs b/ghcide/src/Development/IDE/GHC/ExactPrint.hs
index 610a94689e..f121e1232f 100644
--- a/ghcide/src/Development/IDE/GHC/ExactPrint.hs
+++ b/ghcide/src/Development/IDE/GHC/ExactPrint.hs
@@ -15,6 +15,7 @@ module Development.IDE.GHC.ExactPrint
       graftWithM,
       graftWithSmallestM,
       graftSmallestDecls,
+      graftSmallestDeclsWithM,
       transform,
       transformM,
       useAnnotatedSource,
@@ -64,8 +65,6 @@ import Parser (parseIdentifier)
 import Control.Arrow
 import Data.List (isPrefixOf)
 import Data.Traversable (for)
-import Data.Foldable (Foldable(fold))
-import Debug.Trace (traceM)
 #endif
 
 
@@ -200,7 +199,7 @@ graft dst val = Graft $ \dflags a -> do
 parseDecls :: DynFlags -> FilePath -> String -> ParseResult (LHsDecl GhcPs)
 parseDecls dflags fp str = do
   let mono_decls = fmap unlines $ groupByFirstLine $ lines str
-  decls <- for (zip [0..] mono_decls) $ \(ix, line) -> parseDecl dflags (fp <> show ix) line
+  decls <- for (zip [id @Int 0..] mono_decls) $ \(ix, line) -> parseDecl dflags (fp <> show ix) line
   pure $ mergeDecls decls
 
 
@@ -312,6 +311,27 @@ graftSmallestDecls dst decs0 = Graft $ \dflags a -> do
             | otherwise = DL.singleton (L src e) <> go rest
     modifyDeclsT (pure . DL.toList . go) a
 
+graftSmallestDeclsWithM ::
+    forall a.
+    (HasDecls a) =>
+    SrcSpan ->
+    (LHsDecl GhcPs -> TransformT (Either String) (Maybe [LHsDecl GhcPs])) ->
+    Graft (Either String) a
+graftSmallestDeclsWithM dst toDecls = Graft $ \dflags a -> do
+    let go [] = pure DL.empty
+        go (e@(L src _) : rest)
+            | dst `isSubspanOf` src = toDecls e >>= \case
+                Just decs0 -> do
+                    decs <- forM decs0 $ \decl -> do
+                        (anns, decl') <-
+                            annotateDecl dflags decl
+                        modifyAnnsT $ mappend anns
+                        pure decl'
+                    pure $ DL.fromList decs <> DL.fromList rest
+                Nothing -> (DL.singleton e <>) <$> go rest
+            | otherwise = (DL.singleton e <>) <$> go rest
+    modifyDeclsT (fmap DL.toList . go) a
+
 graftDeclsWithM ::
     forall a m.
     (HasDecls a, Fail.MonadFail m) =>
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
index 9e1d6f6322..9cbeeb468c 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
@@ -66,6 +66,7 @@ import           SrcLoc (containsSpan)
 import           System.Timeout
 import           TcRnTypes (tcg_binds)
 import Development.IDE.GHC.ExactPrint (graftSmallestDecls)
+import Development.IDE.GHC.ExactPrint (graftSmallestDeclsWithM, TransformT)
 
 
 descriptor :: PluginId -> PluginDescriptor IdeState
@@ -332,16 +333,12 @@ tacticCmd tac lf state (TacticParams uri range var_name)
               traceMX "solns" $ rtr_other_solns rtr
               let g =
                     if _jIsTopHole jdg
-                       then graftSmallestDecls (RealSrcSpan span)
-                          $ pure
-                          $ splitToDecl (fst $ last $ ctxDefiningFuncs ctx)
+                       then graftSmallestDeclsWithM (RealSrcSpan span)
+                          $ stickItIn (RealSrcSpan span)
+                          $ \pats ->
+                            splitToDecl (fst $ last $ ctxDefiningFuncs ctx)
                           $ iterateSplit
-                          $ mkFirstAgda
-                              ( fmap (bvar' . hi_name)
-                              . filter (isTopLevel . hi_provenance)
-                              . unHypothesis
-                              $ jHypothesis jdg
-                              )
+                          $ mkFirstAgda (fmap unXPat pats)
                           $ unLoc
                           $ rtr_extract rtr
                        else graft (RealSrcSpan span)
@@ -360,6 +357,32 @@ tacticCmd _ _ _ _ =
        , Nothing
        )
 
+stickItIn
+    :: SrcSpan
+    -> ([Pat GhcPs] -> LHsDecl GhcPs)
+    -> LHsDecl GhcPs
+    -> TransformT (Either String) (Maybe [LHsDecl GhcPs])
+stickItIn span
+    make_decl
+    (L src (ValD ext fb@FunBind {fun_matches = mg@MG {mg_alts = L alt_src alts}}))
+  = pure $ Just $ pure $ L src $ ValD ext $ fb
+      { fun_matches = mg
+        { mg_alts = L alt_src $ do
+            alt@(L alt_src match) <- alts
+            case span `isSubspanOf` alt_src of
+              True -> do
+                let pats = m_pats match
+                    (L _ (ValD _ (FunBind {fun_matches = MG {mg_alts = L _ to_add}}))) =
+                        make_decl pats
+                to_add
+              False -> pure alt
+        }
+      }
+
+unXPat :: Pat GhcPs -> Pat GhcPs
+unXPat (XPat (L _ pat)) = unXPat pat
+unXPat pat = pat
+
 
 fromMaybeT :: Functor m => a -> MaybeT m a -> m a
 fromMaybeT def = fmap (fromMaybe def) . runMaybeT
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
index 246219c770..4a59e66a06 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
@@ -8,14 +8,18 @@
 
 module Ide.Plugin.Tactic.GHC where
 
-import Control.Arrow
+import           Control.Lens
 import           Control.Monad.State
+import           Data.Function (on)
 import qualified Data.Map as M
 import           Data.Maybe (isJust)
 import           Data.Traversable
 import qualified DataCon as DataCon
 import           Development.IDE.GHC.Compat
-import           Generics.SYB (Data, mkT, everywhere)
+import           GHC.Exts (IsString(fromString))
+import           GHC.SourceGen (funBinds, var, bvar, match, case', lambda)
+import           GHC.SourceGen.Pat
+import           Generics.SYB (mkT, everywhere)
 import           Ide.Plugin.Tactic.Types
 import           OccName
 import           TcType
@@ -24,10 +28,7 @@ import           Type
 import           TysWiredIn (intTyCon, floatTyCon, doubleTyCon, charTyCon)
 import           Unique
 import           Var
-import GHC.SourceGen (funBinds, funBind, int, var, bvar, match, case', lambda)
-import Control.Lens
-import GHC.SourceGen.Pat
-import GHC.Exts (IsString(fromString))
+
 
 tcTyVar_maybe :: Type -> Maybe Var
 tcTyVar_maybe ty | Just ty' <- tcView ty = tcTyVar_maybe ty'
@@ -125,7 +126,7 @@ agdaSplit :: AgdaMatch -> [AgdaMatch]
 agdaSplit (AgdaMatch pats (Case (HsVar _ (L _ var)) matches)) = do
   (i, pat) <- zip [id @Int 0 ..] pats
   case pat of
-    VarPat _ (L _ patname) | patname == var -> do
+    VarPat _ (L _ patname) | on (==) (occNameString . occName) patname var -> do
       (case_pat, body) <- matches
       -- TODO(sandy): use an at pattern if necessar
       pure $ AgdaMatch (pats & ix i .~ case_pat) body
@@ -141,7 +142,7 @@ splitToDecl name ams = noLoc $ funBinds (fromString . occNameString . occName $
 
 iterateSplit :: AgdaMatch -> [AgdaMatch]
 iterateSplit am =
-  let iterated =  iterate (agdaSplit =<<) $ pure am
+  let iterated = iterate (agdaSplit =<<) $ pure am
    in fst . head
           . dropWhile (\(a, b) -> length a /= length b)
           . zip iterated
@@ -194,25 +195,6 @@ pattern Case scrutinee matches <-
     Case scrutinee matches =
       case' scrutinee $ fmap (\(pat, body) -> match [pat] body) matches
 
-test :: HsExpr GhcPs
-test =
-  Lambda [bvar "b", bvar "c"] $ Case (var "c")
-    [ (conP "True" [], var "True")
-    , (conP "False" [],
-        Case (var "b")
-          [ (int 0, var "b")
-          , (wildP, int 5)
-          ]
-      )
-    ]
-
-testAgda :: AgdaMatch
-testAgda = AgdaMatch [bvar "a"] test
-
-
-
-
-
 
 ------------------------------------------------------------------------------
 -- | Can ths type be lambda-cased?

From 14fa9f6f6d523afbfdf8893fe49c3a90a184cae0 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Sat, 13 Feb 2021 16:40:36 -0800
Subject: [PATCH 06/38] Add traceFX debug function

---
 plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Debug.hs | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Debug.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Debug.hs
index 6c528da4e3..f32562cc2e 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Debug.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Debug.hs
@@ -11,6 +11,7 @@ module Ide.Plugin.Tactic.Debug
   , traceX
   , traceIdX
   , traceMX
+  , traceFX
   ) where
 
 import Control.DeepSeq
@@ -53,3 +54,6 @@ traceX str a = trace (mappend ("!!!" <> str <> ": ") $ show a)
 traceIdX :: (Show a) => String -> a -> a
 traceIdX str a = trace (mappend ("!!!" <> str <> ": ") $ show a) a
 
+traceFX :: String -> (a -> String) -> a -> a
+traceFX str f a = trace (mappend ("!!!" <> str <> ": ") $ f a) a
+

From f3ea83fb69a77438b007582f18caa994f72b19bb Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Sat, 13 Feb 2021 16:40:44 -0800
Subject: [PATCH 07/38] Force a few iterations of splitAgda

---
 plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs | 8 ++------
 1 file changed, 2 insertions(+), 6 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
index 4a59e66a06..679780b096 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
@@ -17,8 +17,7 @@ import           Data.Traversable
 import qualified DataCon as DataCon
 import           Development.IDE.GHC.Compat
 import           GHC.Exts (IsString(fromString))
-import           GHC.SourceGen (funBinds, var, bvar, match, case', lambda)
-import           GHC.SourceGen.Pat
+import           GHC.SourceGen (funBinds, match, case', lambda)
 import           Generics.SYB (mkT, everywhere)
 import           Ide.Plugin.Tactic.Types
 import           OccName
@@ -143,10 +142,7 @@ splitToDecl name ams = noLoc $ funBinds (fromString . occNameString . occName $
 iterateSplit :: AgdaMatch -> [AgdaMatch]
 iterateSplit am =
   let iterated = iterate (agdaSplit =<<) $ pure am
-   in fst . head
-          . dropWhile (\(a, b) -> length a /= length b)
-          . zip iterated
-          $ tail iterated
+   in head . drop 5 $ iterated
 
 
 

From d573e7a5cf0658480055ebb34aad98c01ee21eab Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Sat, 13 Feb 2021 16:52:58 -0800
Subject: [PATCH 08/38] Cleanup imports

---
 ghcide/src/Development/IDE/GHC/ExactPrint.hs        | 4 ++--
 plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs | 5 ++---
 2 files changed, 4 insertions(+), 5 deletions(-)

diff --git a/ghcide/src/Development/IDE/GHC/ExactPrint.hs b/ghcide/src/Development/IDE/GHC/ExactPrint.hs
index 644e7470cf..5a57ca72cb 100644
--- a/ghcide/src/Development/IDE/GHC/ExactPrint.hs
+++ b/ghcide/src/Development/IDE/GHC/ExactPrint.hs
@@ -62,10 +62,10 @@ import Language.Haskell.LSP.Types.Capabilities (ClientCapabilities)
 import Outputable (Outputable, ppr, showSDoc)
 import Retrie.ExactPrint hiding (parseDecl, parseExpr, parsePattern, parseType)
 import Parser (parseIdentifier)
-#if __GLASGOW_HASKELL__ == 808
-import Control.Arrow
 import Data.List (isPrefixOf)
 import Data.Traversable (for)
+#if __GLASGOW_HASKELL__ == 808
+import Control.Arrow
 #endif
 
 
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
index 6d3aae89bd..7b5f2f13b0 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
@@ -42,6 +42,7 @@ import           Development.IDE.Core.Shake (useWithStale, IdeState (..))
 import           Development.IDE.GHC.Compat
 import           Development.IDE.GHC.Error (realSrcSpanToRange)
 import           Development.IDE.GHC.ExactPrint (graft, transform, useAnnotatedSource, maybeParensAST)
+import           Development.IDE.GHC.ExactPrint (graftSmallestDeclsWithM, TransformT)
 import           Development.IDE.GHC.ExactPrint (graftWithoutParentheses)
 import           Development.IDE.Spans.LocalBindings (getDefiningBindings)
 import           Development.Shake (Action)
@@ -50,6 +51,7 @@ import qualified FastString
 import           GHC.Generics (Generic)
 import           GHC.LanguageExtensions.Type (Extension (LambdaCase))
 import           Ide.Plugin.Tactic.Auto
+import           Ide.Plugin.Tactic.CodeGen (bvar')
 import           Ide.Plugin.Tactic.Context
 import           Ide.Plugin.Tactic.GHC
 import           Ide.Plugin.Tactic.Judgements
@@ -57,7 +59,6 @@ import           Ide.Plugin.Tactic.Range
 import           Ide.Plugin.Tactic.Tactics
 import           Ide.Plugin.Tactic.TestTypes
 import           Ide.Plugin.Tactic.Types
-import           Ide.Plugin.Tactic.CodeGen (bvar')
 import           Ide.PluginUtils
 import           Ide.Types
 import           Language.Haskell.LSP.Core (clientCapabilities)
@@ -67,8 +68,6 @@ import           Refinery.Tactic (goal)
 import           SrcLoc (containsSpan)
 import           System.Timeout
 import           TcRnTypes (tcg_binds)
-import Development.IDE.GHC.ExactPrint (graftSmallestDecls)
-import Development.IDE.GHC.ExactPrint (graftSmallestDeclsWithM, TransformT)
 
 
 descriptor :: PluginId -> PluginDescriptor IdeState

From de541c2b74707e9bcb69ec313aaac1f03d83037b Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Sat, 13 Feb 2021 17:20:18 -0800
Subject: [PATCH 09/38] Put wildcard patterns in for unused variables

---
 .../src/Ide/Plugin/Tactic.hs                  |  2 +-
 .../src/Ide/Plugin/Tactic/GHC.hs              | 48 +++++++++++++++++--
 .../src/Ide/Plugin/Tactic/Simplify.hs         | 20 ++------
 3 files changed, 47 insertions(+), 23 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
index 7b5f2f13b0..fb0420c39b 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
@@ -425,7 +425,7 @@ getRhsPosVals rss tcs
   ) tcs
 
 
-
 -- TODO(sandy): Make this more robust
 isHole :: OccName -> Bool
 isHole = isPrefixOf "_" . occNameString
+
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
index 68137bc226..078ad24fa2 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE CPP               #-}
 {-# LANGUAGE FlexibleContexts  #-}
@@ -8,6 +9,8 @@
 
 module Ide.Plugin.Tactic.GHC where
 
+import qualified Data.Set as S
+import Data.Set (Set)
 import           Control.Lens
 import           Control.Monad.State
 import           Data.Function (on)
@@ -17,8 +20,8 @@ import           Data.Traversable
 import           DataCon
 import           Development.IDE.GHC.Compat
 import           GHC.Exts (IsString(fromString))
-import           GHC.SourceGen (funBinds, match, case', lambda)
-import           Generics.SYB (mkT, everywhere)
+import           GHC.SourceGen (wildP, funBinds, match, case', lambda)
+import           Generics.SYB (mkQ, everything, listify, Data, mkT, everywhere)
 import           Ide.Plugin.Tactic.Types
 import           OccName
 import           TcType
@@ -27,6 +30,8 @@ import           Type
 import           TysWiredIn (intTyCon, floatTyCon, doubleTyCon, charTyCon)
 import           Unique
 import           Var
+import Data.Bool (bool)
+import Data.List (isPrefixOf)
 
 
 tcTyVar_maybe :: Type -> Maybe Var
@@ -137,10 +142,11 @@ agdaSplit :: AgdaMatch -> [AgdaMatch]
 agdaSplit (AgdaMatch pats (Case (HsVar _ (L _ var)) matches)) = do
   (i, pat) <- zip [id @Int 0 ..] pats
   case pat of
-    VarPat _ (L _ patname) | on (==) (occNameString . occName) patname var -> do
+    VarPat _ (L _ patname) | eqRdrName patname var -> do
       (case_pat, body) <- matches
-      -- TODO(sandy): use an at pattern if necessar
-      pure $ AgdaMatch (pats & ix i .~ case_pat) body
+      let make_wild = bool id (wildify (allOccNames body)) $ not $ containsHole body
+      -- TODO(sandy): use an at pattern if necessary
+      pure $ AgdaMatch (make_wild $ pats & ix i .~ case_pat) body
     _ -> []
 agdaSplit x = [x]
 
@@ -157,6 +163,38 @@ iterateSplit am =
    in head . drop 5 $ iterated
 
 
+eqRdrName :: RdrName -> RdrName -> Bool
+eqRdrName = (==) `on` occNameString . occName
+
+
+------------------------------------------------------------------------------
+-- | Does this thing contain any references to 'HsVar's with the given
+-- 'RdrName'?
+containsHsVar :: Data a => RdrName -> a -> Bool
+containsHsVar name x = not $ null $ listify (
+  \case
+    ((HsVar _ (L _ a)) :: HsExpr GhcPs) | eqRdrName a name -> True
+    _ -> False
+  ) x
+
+containsHole :: Data a => a -> Bool
+containsHole x = not $ null $ listify (
+  \case
+    ((HsVar _ (L _ name)) :: HsExpr GhcPs) -> isPrefixOf "_" $ occNameString $ occName name
+    _ -> False
+  ) x
+
+
+allOccNames :: Data a => a -> Set OccName
+allOccNames = everything (<>) $ mkQ mempty $ \case
+    a -> S.singleton a
+
+wildify :: Data a => Set OccName -> a -> a
+wildify (S.map occNameString -> used) = everywhere $ mkT $ \case
+  VarPat _ (L _ var) | S.notMember (occNameString $ occName var) used -> wildP
+  (x :: Pat GhcPs) -> x
+
+
 
 
 ------------------------------------------------------------------------------
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Simplify.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Simplify.hs
index c125d50876..2f5e5a4e0d 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Simplify.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Simplify.hs
@@ -8,17 +8,14 @@ module Ide.Plugin.Tactic.Simplify
   ( simplify
   ) where
 
-import Data.Data (Data)
-import Data.Generics (everywhere, somewhere, something, listify, extT, mkT, GenericT, mkQ)
+import Data.Generics (everywhere, mkT, GenericT)
 import Data.List.Extra (unsnoc)
-import Data.Maybe (isJust)
 import Data.Monoid (Endo (..))
 import Development.IDE.GHC.Compat
-import GHC.Exts (fromString)
-import GHC.SourceGen (var, op)
+import GHC.SourceGen (var)
 import GHC.SourceGen.Expr (lambda)
 import Ide.Plugin.Tactic.CodeGen.Utils
-import Ide.Plugin.Tactic.GHC (fromPatCompatPs)
+import Ide.Plugin.Tactic.GHC (fromPatCompatPs, containsHsVar)
 
 
 ------------------------------------------------------------------------------
@@ -57,17 +54,6 @@ foldEndo :: Foldable t => t (a -> a) -> a -> a
 foldEndo = appEndo . foldMap Endo
 
 
-------------------------------------------------------------------------------
--- | Does this thing contain any references to 'HsVar's with the given
--- 'RdrName'?
-containsHsVar :: Data a => RdrName -> a -> Bool
-containsHsVar name x = not $ null $ listify (
-  \case
-    ((HsVar _ (L _ a)) :: HsExpr GhcPs) | a == name -> True
-    _ -> False
-  ) x
-
-
 ------------------------------------------------------------------------------
 -- | Perform an eta reduction. For example, transforms @\x -> (f g) x@ into
 -- @f g@.

From af02f058d63069d1a6e2c352b09b47cde7c969c3 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Sun, 14 Feb 2021 15:02:04 -0800
Subject: [PATCH 10/38] Update tests

---
 .../src/Ide/Plugin/Tactic.hs                  | 77 ++++++++++++-------
 test/testdata/tactic/FmapBoth.hs.expected     |  3 +-
 .../tactic/GoldenApplicativeThen.hs.expected  |  2 -
 .../tactic/GoldenArbitrary.hs.expected        | 55 ++++++-------
 .../tactic/GoldenBigTuple.hs.expected         |  2 +-
 .../tactic/GoldenEitherAuto.hs.expected       |  6 +-
 .../GoldenEitherHomomorphic.hs.expected       |  6 +-
 .../tactic/GoldenFmapTree.hs.expected         |  7 --
 test/testdata/tactic/GoldenFoldr.hs.expected  |  6 +-
 .../tactic/GoldenFromMaybe.hs.expected        |  6 +-
 .../tactic/GoldenGADTDestruct.hs.expected     |  2 +-
 .../GoldenGADTDestructCoercion.hs.expected    |  2 +-
 .../tactic/GoldenIdentityFunctor.hs.expected  |  3 -
 test/testdata/tactic/GoldenIntros.hs.expected |  2 +-
 .../tactic/GoldenJoinCont.hs.expected         |  2 +-
 .../tactic/GoldenListFmap.hs.expected         |  6 +-
 test/testdata/tactic/GoldenNote.hs.expected   |  6 +-
 .../tactic/GoldenPureList.hs.expected         |  2 +-
 .../tactic/GoldenSafeHead.hs.expected         |  6 +-
 .../tactic/GoldenShowCompose.hs.expected      |  2 +-
 .../tactic/GoldenShowMapChar.hs.expected      |  2 +-
 test/testdata/tactic/GoldenSwap.hs.expected   |  2 +-
 .../tactic/GoldenSwapMany.hs.expected         |  2 +-
 test/testdata/tactic/RecordCon.hs.expected    |  2 +-
 24 files changed, 104 insertions(+), 107 deletions(-)
 delete mode 100644 test/testdata/tactic/GoldenApplicativeThen.hs.expected
 delete mode 100644 test/testdata/tactic/GoldenFmapTree.hs.expected
 delete mode 100644 test/testdata/tactic/GoldenIdentityFunctor.hs.expected

diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
index fb0420c39b..4da0d9dbc2 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
@@ -41,7 +41,7 @@ import           Development.IDE.Core.Service (runAction)
 import           Development.IDE.Core.Shake (useWithStale, IdeState (..))
 import           Development.IDE.GHC.Compat
 import           Development.IDE.GHC.Error (realSrcSpanToRange)
-import           Development.IDE.GHC.ExactPrint (graft, transform, useAnnotatedSource, maybeParensAST)
+import           Development.IDE.GHC.ExactPrint (Graft, Annotated, graft, transform, useAnnotatedSource, maybeParensAST)
 import           Development.IDE.GHC.ExactPrint (graftSmallestDeclsWithM, TransformT)
 import           Development.IDE.GHC.ExactPrint (graftWithoutParentheses)
 import           Development.IDE.Spans.LocalBindings (getDefiningBindings)
@@ -61,7 +61,7 @@ import           Ide.Plugin.Tactic.TestTypes
 import           Ide.Plugin.Tactic.Types
 import           Ide.PluginUtils
 import           Ide.Types
-import           Language.Haskell.LSP.Core (clientCapabilities)
+import           Language.Haskell.LSP.Core (LspFuncs, clientCapabilities)
 import           Language.Haskell.LSP.Types
 import           OccName
 import           Refinery.Tactic (goal)
@@ -322,35 +322,12 @@ tacticCmd tac lf state (TacticParams uri range var_name)
         let span = rangeToRealSrcSpan (fromNormalizedFilePath nfp) range'
         pm <- MaybeT $ useAnnotatedSource "tacticsCmd" state nfp
         x <- lift $ timeout 2e8 $
-          case runTactic ctx jdg
-                $ tac
-                $ mkVarOcc
-                $ T.unpack var_name of
+          case runTactic ctx jdg $ tac $ mkVarOcc $ T.unpack var_name of
             Left err ->
               pure $ (, Nothing)
                 $ Left
                 $ ResponseError InvalidRequest (T.pack $ show err) Nothing
-            Right rtr -> do
-              traceMX "solns" $ rtr_other_solns rtr
-              traceMX "simplified" $ rtr_extract rtr
-              let g =
-                    if _jIsTopHole jdg
-                       then graftSmallestDeclsWithM (RealSrcSpan span)
-                          $ stickItIn (RealSrcSpan span)
-                          $ \pats ->
-                            splitToDecl (fst $ last $ ctxDefiningFuncs ctx)
-                          $ iterateSplit
-                          $ mkFirstAgda (fmap unXPat pats)
-                          $ unLoc
-                          $ rtr_extract rtr
-                       else graftWithoutParentheses (RealSrcSpan span)
-                            -- Parenthesize the extract iff we're not in a top level hole
-                          $ bool maybeParensAST id (_jIsTopHole jdg)
-                          $ rtr_extract rtr
-                  response = transform dflags (clientCapabilities lf) uri g pm
-              pure $ case response of
-                Right res -> (Right Null , Just (WorkspaceApplyEdit, ApplyWorkspaceEditParams res))
-                Left err -> (Left $ ResponseError InternalError (T.pack err) Nothing, Nothing)
+            Right rtr -> pure $ mkWorkspaceEdits rtr jdg span ctx dflags lf uri pm
         pure $ case x of
           Just y -> y
           Nothing -> (, Nothing)
@@ -361,6 +338,50 @@ tacticCmd _ _ _ _ =
        , Nothing
        )
 
+
+mkWorkspaceEdits
+  :: RunTacticResults
+  -> Judgement' a
+  -> RealSrcSpan
+  -> Context
+  -> DynFlags
+  -> LspFuncs c
+  -> Uri
+  -> Annotated ParsedSource
+  -> ( Either ResponseError Value
+     , Maybe (ServerMethod, ApplyWorkspaceEditParams)
+     )
+mkWorkspaceEdits rtr jdg span ctx dflags lf uri pm = do
+  let g = graftHole jdg (RealSrcSpan span) ctx rtr
+      response = transform dflags (clientCapabilities lf) uri g pm
+   in case response of
+        Right res -> (Right Null , Just (WorkspaceApplyEdit, ApplyWorkspaceEditParams res))
+        Left err -> (Left $ ResponseError InternalError (T.pack err) Nothing, Nothing)
+
+
+graftHole
+  :: Judgement' a2
+  -> SrcSpan
+  -> Context
+  -> RunTacticResults
+  -> Graft (Either String) ParsedSource
+graftHole jdg span ctx rtr
+  | _jIsTopHole jdg
+      = graftSmallestDeclsWithM span
+      $ stickItIn span
+      $ \pats ->
+        splitToDecl (fst $ last $ ctxDefiningFuncs ctx)
+      $ iterateSplit
+      $ mkFirstAgda (fmap unXPat pats)
+      $ unLoc
+      $ rtr_extract rtr
+graftHole jdg span _ rtr
+  = graftWithoutParentheses span
+    -- Parenthesize the extract iff we're not in a top level hole
+  $ bool maybeParensAST id (_jIsTopHole jdg)
+  $ rtr_extract rtr
+
+
 stickItIn
     :: SrcSpan
     -> ([Pat GhcPs] -> LHsDecl GhcPs)
@@ -383,6 +404,7 @@ stickItIn span
         }
       }
 
+
 unXPat :: Pat GhcPs -> Pat GhcPs
 unXPat (XPat (L _ pat)) = unXPat pat
 unXPat pat = pat
@@ -391,6 +413,7 @@ unXPat pat = pat
 fromMaybeT :: Functor m => a -> MaybeT m a -> m a
 fromMaybeT def = fmap (fromMaybe def) . runMaybeT
 
+
 liftMaybe :: Monad m => Maybe a -> MaybeT m a
 liftMaybe a = MaybeT $ pure a
 
diff --git a/test/testdata/tactic/FmapBoth.hs.expected b/test/testdata/tactic/FmapBoth.hs.expected
index 3160676e8f..825b00ebea 100644
--- a/test/testdata/tactic/FmapBoth.hs.expected
+++ b/test/testdata/tactic/FmapBoth.hs.expected
@@ -1,4 +1,3 @@
 fmapBoth :: (Functor f, Functor g) => (a -> b) -> (f a, g a) -> (f b, g b)
-fmapBoth = \ fab p_faga
-  -> case p_faga of { (fa, ga) -> (fmap fab fa, fmap fab ga) }
+fmapBoth fab (fa, ga) = (fmap fab fa, fmap fab ga)
 
diff --git a/test/testdata/tactic/GoldenApplicativeThen.hs.expected b/test/testdata/tactic/GoldenApplicativeThen.hs.expected
deleted file mode 100644
index fc7816581b..0000000000
--- a/test/testdata/tactic/GoldenApplicativeThen.hs.expected
+++ /dev/null
@@ -1,2 +0,0 @@
-useThen :: Applicative f => f Int -> f a -> f a
-useThen = (\ x x8 -> (*>) x x8)
diff --git a/test/testdata/tactic/GoldenArbitrary.hs.expected b/test/testdata/tactic/GoldenArbitrary.hs.expected
index 1d533bef3f..6f7af5c3fd 100644
--- a/test/testdata/tactic/GoldenArbitrary.hs.expected
+++ b/test/testdata/tactic/GoldenArbitrary.hs.expected
@@ -22,31 +22,32 @@ data Obj
 
 
 arbitrary :: Gen Obj
-arbitrary = let
-              terminal
-                = [(Square <$> arbitrary) <*> arbitrary, Circle <$> arbitrary,
-                   Polygon <$> arbitrary, pure Empty, pure Full]
-            in
-              sized
-                $ (\ n
-                     -> case n <= 1 of
-                          True -> oneof terminal
-                          False
-                            -> oneof
-                                 $ ([(Rotate2 <$> arbitrary) <*> scale (subtract 1) arbitrary,
-                                     Complement <$> scale (subtract 1) arbitrary,
-                                     (UnionR <$> arbitrary) <*> scale (subtract 1) arbitrary,
-                                     ((DifferenceR <$> arbitrary) <*> scale (flip div 2) arbitrary)
-                                       <*> scale (flip div 2) arbitrary,
-                                     (IntersectR <$> arbitrary) <*> scale (subtract 1) arbitrary,
-                                     ((Translate <$> arbitrary) <*> arbitrary)
-                                       <*> scale (subtract 1) arbitrary,
-                                     ((Scale <$> arbitrary) <*> arbitrary)
-                                       <*> scale (subtract 1) arbitrary,
-                                     ((Mirror <$> arbitrary) <*> arbitrary)
-                                       <*> scale (subtract 1) arbitrary,
-                                     (Outset <$> arbitrary) <*> scale (subtract 1) arbitrary,
-                                     (Shell <$> arbitrary) <*> scale (subtract 1) arbitrary,
-                                     (WithRounding <$> arbitrary) <*> scale (subtract 1) arbitrary]
-                                      <> terminal))
+arbitrary
+  = let
+      terminal
+        = [(Square <$> arbitrary) <*> arbitrary, Circle <$> arbitrary,
+           Polygon <$> arbitrary, pure Empty, pure Full]
+    in
+      sized
+        $ (\ n
+             -> case n <= 1 of
+                  True -> oneof terminal
+                  False
+                    -> oneof
+                         $ ([(Rotate2 <$> arbitrary) <*> scale (subtract 1) arbitrary,
+                             Complement <$> scale (subtract 1) arbitrary,
+                             (UnionR <$> arbitrary) <*> scale (subtract 1) arbitrary,
+                             ((DifferenceR <$> arbitrary) <*> scale (flip div 2) arbitrary)
+                               <*> scale (flip div 2) arbitrary,
+                             (IntersectR <$> arbitrary) <*> scale (subtract 1) arbitrary,
+                             ((Translate <$> arbitrary) <*> arbitrary)
+                               <*> scale (subtract 1) arbitrary,
+                             ((Scale <$> arbitrary) <*> arbitrary)
+                               <*> scale (subtract 1) arbitrary,
+                             ((Mirror <$> arbitrary) <*> arbitrary)
+                               <*> scale (subtract 1) arbitrary,
+                             (Outset <$> arbitrary) <*> scale (subtract 1) arbitrary,
+                             (Shell <$> arbitrary) <*> scale (subtract 1) arbitrary,
+                             (WithRounding <$> arbitrary) <*> scale (subtract 1) arbitrary]
+                              <> terminal))
 
diff --git a/test/testdata/tactic/GoldenBigTuple.hs.expected b/test/testdata/tactic/GoldenBigTuple.hs.expected
index c750f48356..1e7ccecde4 100644
--- a/test/testdata/tactic/GoldenBigTuple.hs.expected
+++ b/test/testdata/tactic/GoldenBigTuple.hs.expected
@@ -1,4 +1,4 @@
 -- There used to be a bug where we were unable to perform a nested split. The
 -- more serious regression test of this is 'AutoTupleSpec'.
 bigTuple :: (a, b, c, d) -> (a, b, (c, d))
-bigTuple = \ pabcd -> case pabcd of { (a, b, c, d) -> (a, b, (c, d)) }
+bigTuple (a, b, c, d) = (a, b, (c, d))
diff --git a/test/testdata/tactic/GoldenEitherAuto.hs.expected b/test/testdata/tactic/GoldenEitherAuto.hs.expected
index 833c250f0b..f7756898e0 100644
--- a/test/testdata/tactic/GoldenEitherAuto.hs.expected
+++ b/test/testdata/tactic/GoldenEitherAuto.hs.expected
@@ -1,5 +1,3 @@
 either' :: (a -> c) -> (b -> c) -> Either a b -> c
-either' = \ fac fbc eab
-  -> case eab of
-       (Left a) -> fac a
-       (Right b) -> fbc b
+either' fac _ (Left a) = fac a
+either' _ fbc (Right b) = fbc b
diff --git a/test/testdata/tactic/GoldenEitherHomomorphic.hs.expected b/test/testdata/tactic/GoldenEitherHomomorphic.hs.expected
index af8e10f357..c18f2ec476 100644
--- a/test/testdata/tactic/GoldenEitherHomomorphic.hs.expected
+++ b/test/testdata/tactic/GoldenEitherHomomorphic.hs.expected
@@ -1,5 +1,3 @@
 eitherSplit :: a -> Either (a -> b) (a -> c) -> Either b c
-eitherSplit = \ a efabfac
-  -> case efabfac of
-       (Left fab) -> Left (fab a)
-       (Right fac) -> Right (fac a)
+eitherSplit a (Left fab) = Left (fab a)
+eitherSplit a (Right fac) = Right (fac a)
diff --git a/test/testdata/tactic/GoldenFmapTree.hs.expected b/test/testdata/tactic/GoldenFmapTree.hs.expected
deleted file mode 100644
index ed608dcbbd..0000000000
--- a/test/testdata/tactic/GoldenFmapTree.hs.expected
+++ /dev/null
@@ -1,7 +0,0 @@
-data Tree a = Leaf a | Branch (Tree a) (Tree a)
-
-instance Functor Tree where
-   fmap = \ fab ta
-     -> case ta of
-          (Leaf a) -> Leaf (fab a)
-          (Branch ta2 ta3) -> Branch (fmap fab ta2) (fmap fab ta3)
diff --git a/test/testdata/tactic/GoldenFoldr.hs.expected b/test/testdata/tactic/GoldenFoldr.hs.expected
index e043416a4d..4e98d0c50e 100644
--- a/test/testdata/tactic/GoldenFoldr.hs.expected
+++ b/test/testdata/tactic/GoldenFoldr.hs.expected
@@ -1,5 +1,3 @@
 foldr2 :: (a -> b -> b) -> b -> [a] -> b
-foldr2 = \ f_b b l_a
-  -> case l_a of
-       [] -> b
-       (a : l_a4) -> f_b a (foldr2 f_b b l_a4)
+foldr2 _ b [] = b
+foldr2 f_b b (a : l_a4) = f_b a (foldr2 f_b b l_a4)
diff --git a/test/testdata/tactic/GoldenFromMaybe.hs.expected b/test/testdata/tactic/GoldenFromMaybe.hs.expected
index 7d08d130e5..90f8edcb79 100644
--- a/test/testdata/tactic/GoldenFromMaybe.hs.expected
+++ b/test/testdata/tactic/GoldenFromMaybe.hs.expected
@@ -1,5 +1,3 @@
 fromMaybe :: a -> Maybe a -> a
-fromMaybe = \ a ma
-  -> case ma of
-       Nothing -> a
-       (Just a2) -> a2
+fromMaybe a Nothing = a
+fromMaybe _ (Just a2) = a2
diff --git a/test/testdata/tactic/GoldenGADTDestruct.hs.expected b/test/testdata/tactic/GoldenGADTDestruct.hs.expected
index fe8d1a8bd8..7f9975ba33 100644
--- a/test/testdata/tactic/GoldenGADTDestruct.hs.expected
+++ b/test/testdata/tactic/GoldenGADTDestruct.hs.expected
@@ -4,4 +4,4 @@ data CtxGADT where
   MkCtxGADT :: (Show a, Eq a) => a -> CtxGADT
 
 ctxGADT :: CtxGADT -> String
-ctxGADT gadt = case gadt of { (MkCtxGADT a) -> _ }
+ctxGADT (MkCtxGADT a) = _
diff --git a/test/testdata/tactic/GoldenGADTDestructCoercion.hs.expected b/test/testdata/tactic/GoldenGADTDestructCoercion.hs.expected
index e3a3e4ed80..57aab53bb4 100644
--- a/test/testdata/tactic/GoldenGADTDestructCoercion.hs.expected
+++ b/test/testdata/tactic/GoldenGADTDestructCoercion.hs.expected
@@ -5,4 +5,4 @@ data E a b where
   E :: forall a b. (b ~ a, Ord a) => b -> E a [a]
 
 ctxGADT :: E a b -> String
-ctxGADT gadt = case gadt of { (E b) -> _ }
+ctxGADT (E b) = _
diff --git a/test/testdata/tactic/GoldenIdentityFunctor.hs.expected b/test/testdata/tactic/GoldenIdentityFunctor.hs.expected
deleted file mode 100644
index 91d1e22d3d..0000000000
--- a/test/testdata/tactic/GoldenIdentityFunctor.hs.expected
+++ /dev/null
@@ -1,3 +0,0 @@
-data Ident a = Ident a
-instance Functor Ident where
-   fmap = \ fab ia -> case ia of { (Ident a) -> Ident (fab a) }
diff --git a/test/testdata/tactic/GoldenIntros.hs.expected b/test/testdata/tactic/GoldenIntros.hs.expected
index 8da62d6b9b..23eadc5edc 100644
--- a/test/testdata/tactic/GoldenIntros.hs.expected
+++ b/test/testdata/tactic/GoldenIntros.hs.expected
@@ -1,2 +1,2 @@
 blah :: Int -> Bool -> (a -> b) -> String -> Int
-blah = \ i b fab l_c -> _
+blah i b fab l_c = _
diff --git a/test/testdata/tactic/GoldenJoinCont.hs.expected b/test/testdata/tactic/GoldenJoinCont.hs.expected
index 7397859c4d..042675ab0b 100644
--- a/test/testdata/tactic/GoldenJoinCont.hs.expected
+++ b/test/testdata/tactic/GoldenJoinCont.hs.expected
@@ -1,4 +1,4 @@
 type Cont r a = ((a -> r) -> r)
 
 joinCont :: Cont r (Cont r a) -> Cont r a
-joinCont = \ f_r far -> f_r (\ f_r2 -> f_r2 far)
+joinCont f_r far = f_r (\ f_r2 -> f_r2 far)
diff --git a/test/testdata/tactic/GoldenListFmap.hs.expected b/test/testdata/tactic/GoldenListFmap.hs.expected
index 7ff6fabfce..4a0af02b09 100644
--- a/test/testdata/tactic/GoldenListFmap.hs.expected
+++ b/test/testdata/tactic/GoldenListFmap.hs.expected
@@ -1,5 +1,3 @@
 fmapList :: (a -> b) -> [a] -> [b]
-fmapList = \ fab l_a
-  -> case l_a of
-       [] -> []
-       (a : l_a3) -> fab a : fmapList fab l_a3
+fmapList _ [] = []
+fmapList fab (a : l_a3) = fab a : fmapList fab l_a3
diff --git a/test/testdata/tactic/GoldenNote.hs.expected b/test/testdata/tactic/GoldenNote.hs.expected
index 420ce242a0..99bc0cd6d0 100644
--- a/test/testdata/tactic/GoldenNote.hs.expected
+++ b/test/testdata/tactic/GoldenNote.hs.expected
@@ -1,5 +1,3 @@
 note :: e -> Maybe a -> Either e a
-note = \ e ma
-  -> case ma of
-       Nothing -> Left e
-       (Just a) -> Right a
+note e Nothing = Left e
+note _ (Just a) = Right a
diff --git a/test/testdata/tactic/GoldenPureList.hs.expected b/test/testdata/tactic/GoldenPureList.hs.expected
index fc5bcdc2a3..8f2bc80ea7 100644
--- a/test/testdata/tactic/GoldenPureList.hs.expected
+++ b/test/testdata/tactic/GoldenPureList.hs.expected
@@ -1,2 +1,2 @@
 pureList :: a -> [a]
-pureList = \ a -> a : []
+pureList a = a : []
diff --git a/test/testdata/tactic/GoldenSafeHead.hs.expected b/test/testdata/tactic/GoldenSafeHead.hs.expected
index 194b8922c0..7f8f73e5b7 100644
--- a/test/testdata/tactic/GoldenSafeHead.hs.expected
+++ b/test/testdata/tactic/GoldenSafeHead.hs.expected
@@ -1,5 +1,3 @@
 safeHead :: [x] -> Maybe x
-safeHead = \ l_x
-  -> case l_x of
-       [] -> Nothing
-       (x : l_x2) -> Just x
+safeHead [] = Nothing
+safeHead (x : _) = Just x
diff --git a/test/testdata/tactic/GoldenShowCompose.hs.expected b/test/testdata/tactic/GoldenShowCompose.hs.expected
index 8152b5a0ae..d8a78b3017 100644
--- a/test/testdata/tactic/GoldenShowCompose.hs.expected
+++ b/test/testdata/tactic/GoldenShowCompose.hs.expected
@@ -1,2 +1,2 @@
 showCompose :: Show a => (b -> a) -> b -> String
-showCompose = \ fba -> show . fba
+showCompose fba = show . fba
diff --git a/test/testdata/tactic/GoldenShowMapChar.hs.expected b/test/testdata/tactic/GoldenShowMapChar.hs.expected
index d4cb942825..22ab0bec15 100644
--- a/test/testdata/tactic/GoldenShowMapChar.hs.expected
+++ b/test/testdata/tactic/GoldenShowMapChar.hs.expected
@@ -1,2 +1,2 @@
 test :: Show a => a -> (String -> b) -> b
-test = \ a fl_cb -> fl_cb (show a)
+test a fl_cb = fl_cb (show a)
diff --git a/test/testdata/tactic/GoldenSwap.hs.expected b/test/testdata/tactic/GoldenSwap.hs.expected
index 2560c15acb..e09cb3800a 100644
--- a/test/testdata/tactic/GoldenSwap.hs.expected
+++ b/test/testdata/tactic/GoldenSwap.hs.expected
@@ -1,2 +1,2 @@
 swap :: (a, b) -> (b, a)
-swap = \ p_ab -> case p_ab of { (a, b) -> (b, a) }
+swap (a, b) = (b, a)
diff --git a/test/testdata/tactic/GoldenSwapMany.hs.expected b/test/testdata/tactic/GoldenSwapMany.hs.expected
index aaffc2d873..1d2bc0a605 100644
--- a/test/testdata/tactic/GoldenSwapMany.hs.expected
+++ b/test/testdata/tactic/GoldenSwapMany.hs.expected
@@ -1,2 +1,2 @@
 swapMany :: (a, b, c, d, e) -> (e, d, c, b, a)
-swapMany = \ pabcde -> case pabcde of { (a, b, c, d, e) -> (e, d, c, b, a) }
+swapMany (a, b, c, d, e) = (e, d, c, b, a)
diff --git a/test/testdata/tactic/RecordCon.hs.expected b/test/testdata/tactic/RecordCon.hs.expected
index 235efbdbfa..9abb0ff3f9 100644
--- a/test/testdata/tactic/RecordCon.hs.expected
+++ b/test/testdata/tactic/RecordCon.hs.expected
@@ -4,6 +4,6 @@ data MyRecord a = Record
     }
 
 blah :: (a -> Int) -> a -> MyRecord a
-blah = \ fai a -> Record {field1 = a, field2 = fai a}
+blah fai a = Record {field1 = a, field2 = fai a}
 
 

From 6a5f2e4b916a4388e24aec9631d2fa5220a10491 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Sun, 14 Feb 2021 20:17:31 -0800
Subject: [PATCH 11/38] Agda-unfold on instance deps

---
 .../src/Ide/Plugin/Tactic.hs                  | 76 ++++++++++++++++---
 .../tactic/GoldenFmapTree.hs.expected         |  4 +
 .../tactic/GoldenIdentityFunctor.hs.expected  |  3 +
 3 files changed, 73 insertions(+), 10 deletions(-)
 create mode 100644 test/testdata/tactic/GoldenFmapTree.hs.expected
 create mode 100644 test/testdata/tactic/GoldenIdentityFunctor.hs.expected

diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
index 4da0d9dbc2..6920f21b5e 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE DeriveAnyClass      #-}
 {-# LANGUAGE DeriveGeneric       #-}
 {-# LANGUAGE GADTs               #-}
@@ -25,7 +26,7 @@ import           Data.Aeson
 import           Data.Bool (bool)
 import           Data.Coerce
 import           Data.Functor ((<&>))
-import           Data.Generics.Aliases (mkQ)
+import           Data.Generics.Aliases (GenericQ, mkQ)
 import           Data.Generics.Schemes (everything)
 import           Data.List
 import           Data.Map (Map)
@@ -68,6 +69,9 @@ import           Refinery.Tactic (goal)
 import           SrcLoc (containsSpan)
 import           System.Timeout
 import           TcRnTypes (tcg_binds)
+import HsDumpAst
+import Data.Data (Data)
+import Bag (listToBag, bagToList)
 
 
 descriptor :: PluginId -> PluginDescriptor IdeState
@@ -382,15 +386,11 @@ graftHole jdg span _ rtr
   $ rtr_extract rtr
 
 
-stickItIn
-    :: SrcSpan
-    -> ([Pat GhcPs] -> LHsDecl GhcPs)
-    -> LHsDecl GhcPs
-    -> TransformT (Either String) (Maybe [LHsDecl GhcPs])
-stickItIn span
-    make_decl
-    (L src (ValD ext fb@FunBind {fun_matches = mg@MG {mg_alts = L alt_src alts}}))
-  = pure $ Just $ pure $ L src $ ValD ext $ fb
+notSure
+  :: ([LPat GhcPs] -> LHsDecl GhcPs)
+     -> SrcSpan -> HsBind GhcPs -> HsBind GhcPs
+notSure make_decl span (fb@FunBind {fun_matches = mg@MG {mg_alts = L alt_src alts}}) =
+    fb
       { fun_matches = mg
         { mg_alts = L alt_src $ do
             alt@(L alt_src match) <- alts
@@ -403,6 +403,35 @@ stickItIn span
               False -> pure alt
         }
       }
+notSure _ _ _ = error "called on something that isnt a funbind"
+
+stickItIn
+    :: SrcSpan
+    -> ([Pat GhcPs] -> LHsDecl GhcPs)
+    -> LHsDecl GhcPs
+    -> TransformT (Either String) (Maybe [LHsDecl GhcPs])
+stickItIn span
+    make_decl
+    (L src (ValD ext fb))
+  = pure $ Just $ pure $ L src $ ValD ext $ notSure make_decl span fb
+stickItIn span
+    make_decl
+    (L src (InstD ext cid@ClsInstD{cid_inst = cidi@ClsInstDecl{cid_sigs = sigs, cid_binds = binds}}))
+  = pure $ Just $ pure $ L src $ InstD ext $ cid
+      { cid_inst = cidi
+        { cid_binds = listToBag $ do
+            b@(L bsrc bind) <- bagToList binds
+            case bind of
+              fb@FunBind{}
+                | span `isSubspanOf` bsrc -> pure $ L bsrc $ notSure make_decl span fb
+              _ -> pure b
+        }
+      }
+stickItIn span _ x = do
+  traceM $ mappend "!!!stickItIn: " $ unsafeRender' $ showAstData BlankSrcSpan x
+  traceMX "biggest" $ unsafeRender $ locateBiggest @(Match GhcPs (LHsExpr GhcPs)) span x
+  traceMX "first" $ unsafeRender $ locateFirst @(Match GhcPs (LHsExpr GhcPs)) x
+  undefined
 
 
 unXPat :: Pat GhcPs -> Pat GhcPs
@@ -452,3 +481,30 @@ getRhsPosVals rss tcs
 isHole :: OccName -> Bool
 isHole = isPrefixOf "_" . occNameString
 
+
+locateBiggest :: (Data r, Data a) => SrcSpan -> a -> Maybe r
+locateBiggest ss x = getFirst $ everything (<>)
+  ( mkQ mempty $ \case
+    L span r | ss `isSubspanOf` span -> pure r
+    _ -> mempty
+  )x
+
+locateSmallest :: (Data r, Data a) => SrcSpan -> a -> Maybe r
+locateSmallest ss x = getLast $ everything (<>)
+  ( mkQ mempty $ \case
+    L span r | ss `isSubspanOf` span -> pure r
+    _ -> mempty
+  )x
+
+locateFirst :: (Data r, Data a) => a -> Maybe r
+locateFirst x = getFirst $ everything (<>)
+  ( mkQ mempty $ \case
+    r -> pure r
+  ) x
+
+locateLast :: (Data r, Data a) => a -> Maybe r
+locateLast x = getLast $ everything (<>)
+  ( mkQ mempty $ \case
+    r -> pure r
+  ) x
+
diff --git a/test/testdata/tactic/GoldenFmapTree.hs.expected b/test/testdata/tactic/GoldenFmapTree.hs.expected
new file mode 100644
index 0000000000..64eef825fa
--- /dev/null
+++ b/test/testdata/tactic/GoldenFmapTree.hs.expected
@@ -0,0 +1,4 @@
+data Tree a = Leaf a | Branch (Tree a) (Tree a)
+instance Functor Tree where
+  fmap fab (Leaf a) = Leaf (fab a)
+  fmap fab (Branch ta2 ta3) = Branch (fmap fab ta2) (fmap fab ta3)
diff --git a/test/testdata/tactic/GoldenIdentityFunctor.hs.expected b/test/testdata/tactic/GoldenIdentityFunctor.hs.expected
new file mode 100644
index 0000000000..757bc8347a
--- /dev/null
+++ b/test/testdata/tactic/GoldenIdentityFunctor.hs.expected
@@ -0,0 +1,3 @@
+data Ident a = Ident a
+instance Functor Ident where
+  fmap fab (Ident a) = Ident (fab a)

From 5a3855776662721b5a010554be7dc6bd13d8fad1 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Sun, 14 Feb 2021 22:13:02 -0800
Subject: [PATCH 12/38] wildify at the very end of simplifying

---
 .../src/Ide/Plugin/Tactic/GHC.hs                  | 15 ++++++++++-----
 1 file changed, 10 insertions(+), 5 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
index 078ad24fa2..338f69b5c3 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
@@ -144,13 +144,18 @@ agdaSplit (AgdaMatch pats (Case (HsVar _ (L _ var)) matches)) = do
   case pat of
     VarPat _ (L _ patname) | eqRdrName patname var -> do
       (case_pat, body) <- matches
-      let make_wild = bool id (wildify (allOccNames body)) $ not $ containsHole body
       -- TODO(sandy): use an at pattern if necessary
-      pure $ AgdaMatch (make_wild $ pats & ix i .~ case_pat) body
+      pure $ AgdaMatch (pats & ix i .~ case_pat) body
     _ -> []
 agdaSplit x = [x]
 
 
+wildify :: AgdaMatch -> AgdaMatch
+wildify (AgdaMatch pats body) =
+  let make_wild = bool id (wildifyT (allOccNames body)) $ not $ containsHole body
+   in AgdaMatch (make_wild pats) body
+
+
 splitToDecl :: OccName -> [AgdaMatch] -> LHsDecl GhcPs
 splitToDecl name ams = noLoc $ funBinds (fromString . occNameString . occName $ name) $ do
   AgdaMatch pats body <- ams
@@ -160,7 +165,7 @@ splitToDecl name ams = noLoc $ funBinds (fromString . occNameString . occName $
 iterateSplit :: AgdaMatch -> [AgdaMatch]
 iterateSplit am =
   let iterated = iterate (agdaSplit =<<) $ pure am
-   in head . drop 5 $ iterated
+   in fmap wildify . head . drop 5 $ iterated
 
 
 eqRdrName :: RdrName -> RdrName -> Bool
@@ -189,8 +194,8 @@ allOccNames :: Data a => a -> Set OccName
 allOccNames = everything (<>) $ mkQ mempty $ \case
     a -> S.singleton a
 
-wildify :: Data a => Set OccName -> a -> a
-wildify (S.map occNameString -> used) = everywhere $ mkT $ \case
+wildifyT :: Data a => Set OccName -> a -> a
+wildifyT (S.map occNameString -> used) = everywhere $ mkT $ \case
   VarPat _ (L _ var) | S.notMember (occNameString $ occName var) used -> wildP
   (x :: Pat GhcPs) -> x
 

From e78549c90ef6804512b40f1429c7502a34d7b439 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 15 Feb 2021 12:54:22 -0800
Subject: [PATCH 13/38] Haddock for top-level functions

---
 .../src/Ide/Plugin/Tactic.hs                  | 48 +++++++++++++------
 1 file changed, 33 insertions(+), 15 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
index 6920f21b5e..e7cf1cf435 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
@@ -343,6 +343,9 @@ tacticCmd _ _ _ _ =
        )
 
 
+------------------------------------------------------------------------------
+-- | Turn a 'RunTacticResults' into concrete edits to make in the source
+-- document.
 mkWorkspaceEdits
   :: RunTacticResults
   -> Judgement' a
@@ -363,6 +366,10 @@ mkWorkspaceEdits rtr jdg span ctx dflags lf uri pm = do
         Left err -> (Left $ ResponseError InternalError (T.pack err) Nothing, 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
+-- 'Match's that bind variables.
 graftHole
   :: Judgement' a2
   -> SrcSpan
@@ -372,7 +379,7 @@ graftHole
 graftHole jdg span ctx rtr
   | _jIsTopHole jdg
       = graftSmallestDeclsWithM span
-      $ stickItIn span
+      $ graftDecl span
       $ \pats ->
         splitToDecl (fst $ last $ ctxDefiningFuncs ctx)
       $ iterateSplit
@@ -386,10 +393,17 @@ graftHole jdg span _ rtr
   $ rtr_extract rtr
 
 
-notSure
-  :: ([LPat GhcPs] -> LHsDecl GhcPs)
-     -> SrcSpan -> HsBind GhcPs -> HsBind GhcPs
-notSure make_decl span (fb@FunBind {fun_matches = mg@MG {mg_alts = L alt_src alts}}) =
+------------------------------------------------------------------------------
+-- | Merge in the 'Match'es of a 'FunBind' into a 'HsDecl'. Used to perform
+-- agda-style case splitting in which we need to separate one 'Match' into
+-- many, without affecting any matches which might exist but don't need to be
+-- split.
+mergeFunBindMatches
+    :: ([LPat GhcPs] -> LHsDecl GhcPs)
+    -> SrcSpan
+    -> HsBind GhcPs
+    -> HsBind GhcPs
+mergeFunBindMatches make_decl span (fb@FunBind {fun_matches = mg@MG {mg_alts = L alt_src alts}}) =
     fb
       { fun_matches = mg
         { mg_alts = L alt_src $ do
@@ -403,35 +417,39 @@ notSure make_decl span (fb@FunBind {fun_matches = mg@MG {mg_alts = L alt_src alt
               False -> pure alt
         }
       }
-notSure _ _ _ = error "called on something that isnt a funbind"
+mergeFunBindMatches _ _ _ = error "called on something that isnt a funbind"
 
-stickItIn
+------------------------------------------------------------------------------
+-- | Helper function to route 'mergeFunBindMatches' into the right place in an
+-- AST --- correctly dealing with inserting into instance declarations.
+graftDecl
     :: SrcSpan
     -> ([Pat GhcPs] -> LHsDecl GhcPs)
     -> LHsDecl GhcPs
     -> TransformT (Either String) (Maybe [LHsDecl GhcPs])
-stickItIn span
+graftDecl span
     make_decl
     (L src (ValD ext fb))
-  = pure $ Just $ pure $ L src $ ValD ext $ notSure make_decl span fb
-stickItIn span
+  = pure $ Just $ pure $ L src $ ValD ext $ mergeFunBindMatches make_decl span fb
+-- TODO(sandy): default methods
+graftDecl span
     make_decl
-    (L src (InstD ext cid@ClsInstD{cid_inst = cidi@ClsInstDecl{cid_sigs = sigs, cid_binds = binds}}))
+    (L src (InstD ext cid@ClsInstD{cid_inst = cidi@ClsInstDecl{cid_sigs = _sigs, cid_binds = binds}}))
   = pure $ Just $ pure $ L src $ InstD ext $ cid
       { cid_inst = cidi
         { cid_binds = listToBag $ do
             b@(L bsrc bind) <- bagToList binds
             case bind of
               fb@FunBind{}
-                | span `isSubspanOf` bsrc -> pure $ L bsrc $ notSure make_decl span fb
+                | span `isSubspanOf` bsrc -> pure $ L bsrc $ mergeFunBindMatches make_decl span fb
               _ -> pure b
         }
       }
-stickItIn span _ x = do
-  traceM $ mappend "!!!stickItIn: " $ unsafeRender' $ showAstData BlankSrcSpan x
+graftDecl span _ x = do
+  traceM $ mappend "!!!graftDecl: " $ unsafeRender' $ showAstData BlankSrcSpan x
   traceMX "biggest" $ unsafeRender $ locateBiggest @(Match GhcPs (LHsExpr GhcPs)) span x
   traceMX "first" $ unsafeRender $ locateFirst @(Match GhcPs (LHsExpr GhcPs)) x
-  undefined
+  pure $ Just [x]
 
 
 unXPat :: Pat GhcPs -> Pat GhcPs

From cca1f345b3b451cb671eaabfb04dfe8ffac3ffab Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 15 Feb 2021 13:00:29 -0800
Subject: [PATCH 14/38] Move case splitting stuff into its own module

---
 .../hls-tactics-plugin.cabal                  |  1 +
 .../src/Ide/Plugin/Tactic.hs                  | 15 ++---
 .../src/Ide/Plugin/Tactic/CaseSplit.hs        | 53 ++++++++++++++++++
 .../src/Ide/Plugin/Tactic/GHC.hs              | 55 ++-----------------
 .../src/Ide/Plugin/Tactic/Types.hs            |  8 +++
 5 files changed, 73 insertions(+), 59 deletions(-)
 create mode 100644 plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/CaseSplit.hs

diff --git a/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal b/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal
index f6e6b8fd4e..068fe56285 100644
--- a/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal
+++ b/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal
@@ -24,6 +24,7 @@ library
   exposed-modules:
     Ide.Plugin.Tactic
     Ide.Plugin.Tactic.Auto
+    Ide.Plugin.Tactic.CaseSplit
     Ide.Plugin.Tactic.CodeGen
     Ide.Plugin.Tactic.CodeGen.Utils
     Ide.Plugin.Tactic.Context
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
index e7cf1cf435..b944adf896 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
@@ -17,6 +17,7 @@ module Ide.Plugin.Tactic
   ) where
 
 
+import           Bag (listToBag, bagToList)
 import           Control.Arrow
 import           Control.Monad
 import           Control.Monad.Error.Class (MonadError(throwError))
@@ -25,8 +26,9 @@ import           Control.Monad.Trans.Maybe
 import           Data.Aeson
 import           Data.Bool (bool)
 import           Data.Coerce
+import           Data.Data (Data)
 import           Data.Functor ((<&>))
-import           Data.Generics.Aliases (GenericQ, mkQ)
+import           Data.Generics.Aliases (mkQ)
 import           Data.Generics.Schemes (everything)
 import           Data.List
 import           Data.Map (Map)
@@ -42,17 +44,15 @@ import           Development.IDE.Core.Service (runAction)
 import           Development.IDE.Core.Shake (useWithStale, IdeState (..))
 import           Development.IDE.GHC.Compat
 import           Development.IDE.GHC.Error (realSrcSpanToRange)
-import           Development.IDE.GHC.ExactPrint (Graft, Annotated, graft, transform, useAnnotatedSource, maybeParensAST)
-import           Development.IDE.GHC.ExactPrint (graftSmallestDeclsWithM, TransformT)
-import           Development.IDE.GHC.ExactPrint (graftWithoutParentheses)
+import           Development.IDE.GHC.ExactPrint
 import           Development.IDE.Spans.LocalBindings (getDefiningBindings)
 import           Development.Shake (Action)
-import           DynFlags (xopt)
 import qualified FastString
 import           GHC.Generics (Generic)
 import           GHC.LanguageExtensions.Type (Extension (LambdaCase))
+import           HsDumpAst
 import           Ide.Plugin.Tactic.Auto
-import           Ide.Plugin.Tactic.CodeGen (bvar')
+import           Ide.Plugin.Tactic.CaseSplit
 import           Ide.Plugin.Tactic.Context
 import           Ide.Plugin.Tactic.GHC
 import           Ide.Plugin.Tactic.Judgements
@@ -69,9 +69,6 @@ import           Refinery.Tactic (goal)
 import           SrcLoc (containsSpan)
 import           System.Timeout
 import           TcRnTypes (tcg_binds)
-import HsDumpAst
-import Data.Data (Data)
-import Bag (listToBag, bagToList)
 
 
 descriptor :: PluginId -> PluginDescriptor IdeState
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/CaseSplit.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/CaseSplit.hs
new file mode 100644
index 0000000000..9b014ae504
--- /dev/null
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/CaseSplit.hs
@@ -0,0 +1,53 @@
+{-# LANGUAGE TypeApplications #-}
+
+module Ide.Plugin.Tactic.CaseSplit
+  ( mkFirstAgda
+  , iterateSplit
+  , splitToDecl
+  ) where
+
+import Control.Lens
+import Data.Bool (bool)
+import Development.IDE.GHC.Compat
+import GHC.Exts (IsString(fromString))
+import GHC.SourceGen (funBinds, match)
+import Ide.Plugin.Tactic.GHC
+import Ide.Plugin.Tactic.Types
+import OccName
+
+
+
+mkFirstAgda :: [Pat GhcPs] -> HsExpr GhcPs -> AgdaMatch
+mkFirstAgda pats (Lambda pats' body) = mkFirstAgda (pats <> pats') body
+mkFirstAgda pats body = AgdaMatch pats body
+
+
+agdaSplit :: AgdaMatch -> [AgdaMatch]
+agdaSplit (AgdaMatch pats (Case (HsVar _ (L _ var)) matches)) = do
+  (i, pat) <- zip [id @Int 0 ..] pats
+  case pat of
+    VarPat _ (L _ patname) | eqRdrName patname var -> do
+      (case_pat, body) <- matches
+      -- TODO(sandy): use an at pattern if necessary
+      pure $ AgdaMatch (pats & ix i .~ case_pat) body
+    _ -> []
+agdaSplit x = [x]
+
+
+wildify :: AgdaMatch -> AgdaMatch
+wildify (AgdaMatch pats body) =
+  let make_wild = bool id (wildifyT (allOccNames body)) $ not $ containsHole body
+   in AgdaMatch (make_wild pats) body
+
+
+splitToDecl :: OccName -> [AgdaMatch] -> LHsDecl GhcPs
+splitToDecl name ams = noLoc $ funBinds (fromString . occNameString . occName $ name) $ do
+  AgdaMatch pats body <- ams
+  pure $ match pats body
+
+
+iterateSplit :: AgdaMatch -> [AgdaMatch]
+iterateSplit am =
+  let iterated = iterate (agdaSplit =<<) $ pure am
+   in fmap wildify . head . drop 5 $ iterated
+
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
index 338f69b5c3..86b7fdcacd 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
@@ -9,18 +9,17 @@
 
 module Ide.Plugin.Tactic.GHC where
 
-import qualified Data.Set as S
-import Data.Set (Set)
-import           Control.Lens
 import           Control.Monad.State
 import           Data.Function (on)
+import           Data.List (isPrefixOf)
 import qualified Data.Map as M
 import           Data.Maybe (isJust)
+import           Data.Set (Set)
+import qualified Data.Set as S
 import           Data.Traversable
 import           DataCon
 import           Development.IDE.GHC.Compat
-import           GHC.Exts (IsString(fromString))
-import           GHC.SourceGen (wildP, funBinds, match, case', lambda)
+import           GHC.SourceGen (wildP, match, case', lambda)
 import           Generics.SYB (mkQ, everything, listify, Data, mkT, everywhere)
 import           Ide.Plugin.Tactic.Types
 import           OccName
@@ -30,8 +29,6 @@ import           Type
 import           TysWiredIn (intTyCon, floatTyCon, doubleTyCon, charTyCon)
 import           Unique
 import           Var
-import Data.Bool (bool)
-import Data.List (isPrefixOf)
 
 
 tcTyVar_maybe :: Type -> Maybe Var
@@ -125,49 +122,6 @@ algebraicTyCon (splitTyConApp_maybe -> Just (tycon, _))
   | otherwise = Just tycon
 algebraicTyCon _ = Nothing
 
-
-data AgdaMatch = AgdaMatch
-  { amPats :: [Pat GhcPs]
-  , amBody :: HsExpr GhcPs
-  }
-  deriving (Show)
-
-
-mkFirstAgda :: [Pat GhcPs] -> HsExpr GhcPs -> AgdaMatch
-mkFirstAgda pats (Lambda pats' body) = mkFirstAgda (pats <> pats') body
-mkFirstAgda pats body = AgdaMatch pats body
-
-
-agdaSplit :: AgdaMatch -> [AgdaMatch]
-agdaSplit (AgdaMatch pats (Case (HsVar _ (L _ var)) matches)) = do
-  (i, pat) <- zip [id @Int 0 ..] pats
-  case pat of
-    VarPat _ (L _ patname) | eqRdrName patname var -> do
-      (case_pat, body) <- matches
-      -- TODO(sandy): use an at pattern if necessary
-      pure $ AgdaMatch (pats & ix i .~ case_pat) body
-    _ -> []
-agdaSplit x = [x]
-
-
-wildify :: AgdaMatch -> AgdaMatch
-wildify (AgdaMatch pats body) =
-  let make_wild = bool id (wildifyT (allOccNames body)) $ not $ containsHole body
-   in AgdaMatch (make_wild pats) body
-
-
-splitToDecl :: OccName -> [AgdaMatch] -> LHsDecl GhcPs
-splitToDecl name ams = noLoc $ funBinds (fromString . occNameString . occName $ name) $ do
-  AgdaMatch pats body <- ams
-  pure $ match pats body
-
-
-iterateSplit :: AgdaMatch -> [AgdaMatch]
-iterateSplit am =
-  let iterated = iterate (agdaSplit =<<) $ pure am
-   in fmap wildify . head . drop 5 $ iterated
-
-
 eqRdrName :: RdrName -> RdrName -> Bool
 eqRdrName = (==) `on` occNameString . occName
 
@@ -305,3 +259,4 @@ dataConExTys = DataCon.dataConExTyCoVars
 #else
 dataConExTys = DataCon.dataConExTyVars
 #endif
+
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs
index c1879591d6..e17ea2e895 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs
@@ -376,3 +376,11 @@ data RunTacticResults = RunTacticResults
   , rtr_extract     :: LHsExpr GhcPs
   , rtr_other_solns :: [(Trace, LHsExpr GhcPs)]
   } deriving Show
+
+
+data AgdaMatch = AgdaMatch
+  { amPats :: [Pat GhcPs]
+  , amBody :: HsExpr GhcPs
+  }
+  deriving (Show)
+

From 8fcb93660b80965e54ab15dc0d0931b63cec46e2 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 15 Feb 2021 13:10:35 -0800
Subject: [PATCH 15/38] Exactprint comments

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

diff --git a/ghcide/src/Development/IDE/GHC/ExactPrint.hs b/ghcide/src/Development/IDE/GHC/ExactPrint.hs
index 5a57ca72cb..6002419d73 100644
--- a/ghcide/src/Development/IDE/GHC/ExactPrint.hs
+++ b/ghcide/src/Development/IDE/GHC/ExactPrint.hs
@@ -207,6 +207,17 @@ graftWithoutParentheses dst val = Graft $ \dflags a -> do
             a
 
 
+------------------------------------------------------------------------------
+-- | 'parseDecl' fails to parse decls that span multiple lines at the top
+-- layout --- eg. things like:
+--
+-- @
+-- not True = False
+-- not False = True
+-- @
+--
+-- This function splits up each top-layout declaration, parses them
+-- individually, and then merges them back into a single decl.
 parseDecls :: DynFlags -> FilePath -> String -> ParseResult (LHsDecl GhcPs)
 parseDecls dflags fp str = do
   let mono_decls = fmap unlines $ groupByFirstLine $ lines str
@@ -214,9 +225,14 @@ parseDecls dflags fp str = do
   pure $ mergeDecls decls
 
 
+------------------------------------------------------------------------------
+-- | Combine decls together. See 'parseDecl' for more information.
 mergeDecls :: [(Anns, LHsDecl GhcPs)] -> (Anns, LHsDecl GhcPs)
 mergeDecls [x] = x
 mergeDecls ((anns,  L _ (ValD ext fb@FunBind{fun_matches = mg@MG {mg_alts = L _ alts}}))
+          -- Since 'groupByFirstLine' separates matches, we are guaranteed to
+          -- only have a single alternative here. We want to add it to 'alts'
+          -- above.
           : (anns', L _ (ValD _ FunBind{fun_matches = MG {mg_alts = L _ [alt]}}))
           : decls) =
   mergeDecls $
@@ -225,9 +241,18 @@ mergeDecls ((anns,  L _ (ValD ext fb@FunBind{fun_matches = mg@MG {mg_alts = L _
         { fun_matches = mg { mg_alts = noLoc $ alts <> [alt] }
         }
     ) : decls
-mergeDecls _ = error "huh"
+mergeDecls _ = error "mergeDecls called with something that isn't a ValD FunBind"
 
 
+------------------------------------------------------------------------------
+-- | Groups strings by the Haskell top-layout rules, assuming each element of
+-- the list corresponds to a line. For example, the list
+--
+-- @["a", " a1", " a2", "b", " b1"]@
+--
+-- will be grouped to
+--
+-- @[["a", " a1", " a2"], ["b", " b1"]]@
 groupByFirstLine :: [String] -> [[String]]
 groupByFirstLine [] = []
 groupByFirstLine (str : strs) =
@@ -235,7 +260,6 @@ groupByFirstLine (str : strs) =
    in (str : same) : groupByFirstLine diff
 
 
-
 ------------------------------------------------------------------------------
 
 graftWithM ::

From 41c7461e54e73a7811aa7da37a2570d517a3047f Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 15 Feb 2021 13:19:44 -0800
Subject: [PATCH 16/38] Haddock for casesplit

---
 .../src/Ide/Plugin/Tactic/CaseSplit.hs        | 51 +++++++++++++++----
 .../src/Ide/Plugin/Tactic/GHC.hs              | 21 +++-----
 2 files changed, 49 insertions(+), 23 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/CaseSplit.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/CaseSplit.hs
index 9b014ae504..04d0f9bb12 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/CaseSplit.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/CaseSplit.hs
@@ -1,4 +1,7 @@
-{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE LambdaCase          #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications    #-}
+{-# LANGUAGE ViewPatterns        #-}
 
 module Ide.Plugin.Tactic.CaseSplit
   ( mkFirstAgda
@@ -6,22 +9,32 @@ module Ide.Plugin.Tactic.CaseSplit
   , splitToDecl
   ) where
 
-import Control.Lens
-import Data.Bool (bool)
-import Development.IDE.GHC.Compat
-import GHC.Exts (IsString(fromString))
-import GHC.SourceGen (funBinds, match)
-import Ide.Plugin.Tactic.GHC
-import Ide.Plugin.Tactic.Types
-import OccName
+import           Control.Lens
+import           Data.Bool (bool)
+import           Data.Data
+import           Data.Generics
+import           Data.Set (Set)
+import qualified Data.Set as S
+import           Development.IDE.GHC.Compat
+import           GHC.Exts (IsString(fromString))
+import           GHC.SourceGen (funBinds, match, wildP)
+import           Ide.Plugin.Tactic.GHC
+import           Ide.Plugin.Tactic.Types
+import           OccName
 
 
 
+------------------------------------------------------------------------------
+-- | Construct an 'AgdaMatch' from patterns in scope (should be the LHS of the
+-- match) and a body.
 mkFirstAgda :: [Pat GhcPs] -> HsExpr GhcPs -> AgdaMatch
 mkFirstAgda pats (Lambda pats' body) = mkFirstAgda (pats <> pats') body
 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
   (i, pat) <- zip [id @Int 0 ..] pats
@@ -34,18 +47,36 @@ agdaSplit (AgdaMatch pats (Case (HsVar _ (L _ var)) matches)) = do
 agdaSplit x = [x]
 
 
+------------------------------------------------------------------------------
+-- | Replace unused bound patterns with wild patterns.
 wildify :: AgdaMatch -> AgdaMatch
 wildify (AgdaMatch pats body) =
   let make_wild = bool id (wildifyT (allOccNames body)) $ not $ containsHole body
    in AgdaMatch (make_wild pats) body
 
 
-splitToDecl :: OccName -> [AgdaMatch] -> LHsDecl GhcPs
+------------------------------------------------------------------------------
+-- | Helper function for 'wildify'.
+wildifyT :: Data a => Set OccName -> a -> a
+wildifyT (S.map occNameString -> used) = everywhere $ mkT $ \case
+  VarPat _ (L _ var) | S.notMember (occNameString $ occName var) used -> wildP
+  (x :: Pat GhcPs) -> x
+
+
+------------------------------------------------------------------------------
+-- | Construct an 'HsDecl' from a set of 'AgdaMatch'es.
+splitToDecl
+    :: OccName  -- ^ The name of the function
+    -> [AgdaMatch]
+    -> LHsDecl GhcPs
 splitToDecl name ams = noLoc $ funBinds (fromString . occNameString . occName $ name) $ do
   AgdaMatch pats body <- ams
   pure $ match pats body
 
 
+------------------------------------------------------------------------------
+-- | Sometimes 'agdaSplit' exposes another opportunity to do 'agdaSplit'. This
+-- function runs it a few times, hoping it will find a fixpoint.
 iterateSplit :: AgdaMatch -> [AgdaMatch]
 iterateSplit am =
   let iterated = iterate (agdaSplit =<<) $ pure am
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
index 86b7fdcacd..c1bf04b309 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
@@ -1,11 +1,11 @@
+{-# LANGUAGE CPP                 #-}
+{-# LANGUAGE FlexibleContexts    #-}
+{-# LANGUAGE LambdaCase          #-}
+{-# LANGUAGE OverloadedStrings   #-}
+{-# LANGUAGE PatternSynonyms     #-}
 {-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE LambdaCase #-}
-{-# LANGUAGE CPP               #-}
-{-# LANGUAGE FlexibleContexts  #-}
-{-# LANGUAGE OverloadedStrings #-}
-{-# LANGUAGE PatternSynonyms   #-}
-{-# LANGUAGE TypeApplications  #-}
-{-# LANGUAGE ViewPatterns      #-}
+{-# LANGUAGE TypeApplications    #-}
+{-# LANGUAGE ViewPatterns        #-}
 
 module Ide.Plugin.Tactic.GHC where
 
@@ -19,7 +19,7 @@ import qualified Data.Set as S
 import           Data.Traversable
 import           DataCon
 import           Development.IDE.GHC.Compat
-import           GHC.SourceGen (wildP, match, case', lambda)
+import           GHC.SourceGen (match, case', lambda)
 import           Generics.SYB (mkQ, everything, listify, Data, mkT, everywhere)
 import           Ide.Plugin.Tactic.Types
 import           OccName
@@ -148,11 +148,6 @@ allOccNames :: Data a => a -> Set OccName
 allOccNames = everything (<>) $ mkQ mempty $ \case
     a -> S.singleton a
 
-wildifyT :: Data a => Set OccName -> a -> a
-wildifyT (S.map occNameString -> used) = everywhere $ mkT $ \case
-  VarPat _ (L _ var) | S.notMember (occNameString $ occName var) used -> wildP
-  (x :: Pat GhcPs) -> x
-
 
 
 

From c6112c4c1c1db8cd72c329ba00400998f429102b Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 15 Feb 2021 15:49:09 -0800
Subject: [PATCH 17/38] Use PatCompat

---
 plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
index c1bf04b309..8c61e96660 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
@@ -157,7 +157,7 @@ pattern Lambda :: [Pat GhcPs] -> HsExpr GhcPs -> HsExpr GhcPs
 pattern Lambda pats body <-
   HsLam _
     (MG {mg_alts = L _ [L _
-      (Match { m_pats = pats
+      (Match { m_pats = fmap fromPatCompatPs -> pats
              , m_grhss = UnguardedRHSs body
              })]})
   where
@@ -173,7 +173,7 @@ pattern UnguardedRHSs body <-
 
 pattern SinglePatMatch :: Pat GhcPs -> HsExpr GhcPs -> Match GhcPs (LHsExpr GhcPs)
 pattern SinglePatMatch pat body <-
-  Match { m_pats = [pat]
+  Match { m_pats = [fromPatCompatPs -> pat]
         , m_grhss = UnguardedRHSs body
         }
 

From 57c2da244aeb42e550cad0a790dca3bf3e04f574 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 15 Feb 2021 15:56:06 -0800
Subject: [PATCH 18/38] Remove HsDumpAst

---
 plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs | 2 --
 1 file changed, 2 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
index b944adf896..ab94a2ad51 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
@@ -50,7 +50,6 @@ import           Development.Shake (Action)
 import qualified FastString
 import           GHC.Generics (Generic)
 import           GHC.LanguageExtensions.Type (Extension (LambdaCase))
-import           HsDumpAst
 import           Ide.Plugin.Tactic.Auto
 import           Ide.Plugin.Tactic.CaseSplit
 import           Ide.Plugin.Tactic.Context
@@ -443,7 +442,6 @@ graftDecl span
         }
       }
 graftDecl span _ x = do
-  traceM $ mappend "!!!graftDecl: " $ unsafeRender' $ showAstData BlankSrcSpan x
   traceMX "biggest" $ unsafeRender $ locateBiggest @(Match GhcPs (LHsExpr GhcPs)) span x
   traceMX "first" $ unsafeRender $ locateFirst @(Match GhcPs (LHsExpr GhcPs)) x
   pure $ Just [x]

From 0d698aa898643594d37a39138d247bf92a039474 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 15 Feb 2021 16:08:23 -0800
Subject: [PATCH 19/38] Use Pat, not LPat

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

diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
index ab94a2ad51..b1b6b3bf58 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
@@ -395,7 +395,7 @@ graftHole jdg span _ rtr
 -- many, without affecting any matches which might exist but don't need to be
 -- split.
 mergeFunBindMatches
-    :: ([LPat GhcPs] -> LHsDecl GhcPs)
+    :: ([Pat GhcPs] -> LHsDecl GhcPs)
     -> SrcSpan
     -> HsBind GhcPs
     -> HsBind GhcPs

From 5c1f3e0fe7355dbb235998d56692557ecc1bf61d Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 15 Feb 2021 16:16:44 -0800
Subject: [PATCH 20/38] More massaging Pats

---
 plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs     | 6 +-----
 plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs | 7 +++++++
 2 files changed, 8 insertions(+), 5 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
index b1b6b3bf58..d2cda3add4 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
@@ -406,7 +406,7 @@ mergeFunBindMatches make_decl span (fb@FunBind {fun_matches = mg@MG {mg_alts = L
             alt@(L alt_src match) <- alts
             case span `isSubspanOf` alt_src of
               True -> do
-                let pats = m_pats match
+                let pats = fmap fromPatCompatPs $ m_pats match
                     (L _ (ValD _ (FunBind {fun_matches = MG {mg_alts = L _ to_add}}))) =
                         make_decl pats
                 to_add
@@ -447,10 +447,6 @@ graftDecl span _ x = do
   pure $ Just [x]
 
 
-unXPat :: Pat GhcPs -> Pat GhcPs
-unXPat (XPat (L _ pat)) = unXPat pat
-unXPat pat = pat
-
 
 fromMaybeT :: Functor m => a -> MaybeT m a -> m a
 fromMaybeT def = fmap (fromMaybe def) . runMaybeT
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
index 8c61e96660..9aa0bdcbb9 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
@@ -255,3 +255,10 @@ dataConExTys = DataCon.dataConExTyCoVars
 dataConExTys = DataCon.dataConExTyVars
 #endif
 
+
+unXPat :: Pat GhcPs -> Pat GhcPs
+#if __GLASGOW_HASKELL__ <= 808
+unXPat (XPat (L _ pat)) = unXPat pat
+#endif
+unXPat pat = pat
+

From 96f566be2c50bbf2ebbf7f681b54cef74de8e573 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 15 Feb 2021 16:29:18 -0800
Subject: [PATCH 21/38] Only unXPat on 8.0.8

---
 plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
index 9aa0bdcbb9..dfe6d4d701 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
@@ -257,7 +257,7 @@ dataConExTys = DataCon.dataConExTyVars
 
 
 unXPat :: Pat GhcPs -> Pat GhcPs
-#if __GLASGOW_HASKELL__ <= 808
+#if __GLASGOW_HASKELL__ == 808
 unXPat (XPat (L _ pat)) = unXPat pat
 #endif
 unXPat pat = pat

From 57e906ff9b96b79b0593ac8fd486c5f986a4b47d Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 15 Feb 2021 18:07:44 -0800
Subject: [PATCH 22/38] Haddock and cleanup -Wall

---
 .../src/Ide/Plugin/Tactic.hs                  | 41 +++++--------------
 .../src/Ide/Plugin/Tactic/GHC.hs              | 28 ++++++++++++-
 2 files changed, 38 insertions(+), 31 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
index d2cda3add4..35b6a3fd7b 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
@@ -1,4 +1,3 @@
-{-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE DeriveAnyClass      #-}
 {-# LANGUAGE DeriveGeneric       #-}
 {-# LANGUAGE GADTs               #-}
@@ -7,6 +6,7 @@
 {-# LANGUAGE OverloadedStrings   #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TupleSections       #-}
+{-# LANGUAGE TypeApplications    #-}
 {-# LANGUAGE ViewPatterns        #-}
 
 -- | A plugin that uses tactics to synthesize code
@@ -16,7 +16,6 @@ module Ide.Plugin.Tactic
   , TacticCommand (..)
   ) where
 
-
 import           Bag (listToBag, bagToList)
 import           Control.Arrow
 import           Control.Monad
@@ -30,7 +29,6 @@ import           Data.Data (Data)
 import           Data.Functor ((<&>))
 import           Data.Generics.Aliases (mkQ)
 import           Data.Generics.Schemes (everything)
-import           Data.List
 import           Data.Map (Map)
 import qualified Data.Map as M
 import           Data.Maybe
@@ -64,6 +62,7 @@ import           Ide.Types
 import           Language.Haskell.LSP.Core (LspFuncs, clientCapabilities)
 import           Language.Haskell.LSP.Types
 import           OccName
+import           Prelude hiding (span)
 import           Refinery.Tactic (goal)
 import           SrcLoc (containsSpan)
 import           System.Timeout
@@ -196,7 +195,7 @@ codeActions = List . fmap CACodeAction
 provide :: TacticCommand -> T.Text -> TacticProvider
 provide tc name _ plId uri range _ = do
   let title = tacticTitle tc name
-      params = TacticParams { file = uri , range = range , var_name = name }
+      params = TacticParams { tp_file = uri , tp_range = range , tp_var_name = name }
   cmd <- mkLspCommand plId (tcCommandId tc) title (Just [toJSON params])
   pure
     $ pure
@@ -243,9 +242,9 @@ filterBindingType p tp dflags plId uri range jdg =
 
 
 data TacticParams = TacticParams
-    { file :: Uri -- ^ Uri of the file to fill the hole in
-    , range :: Range -- ^ The range of the hole
-    , var_name :: T.Text
+    { tp_file :: Uri -- ^ Uri of the file to fill the hole in
+    , tp_range :: Range -- ^ The range of the hole
+    , tp_var_name :: T.Text
     }
   deriving (Show, Eq, Generic, ToJSON, FromJSON)
 
@@ -271,7 +270,7 @@ judgementForHole state nfp range = do
 
   case asts of
     (HAR _ hf _ _ kind) -> do
-      (rss, goal) <- liftMaybe $ join $ listToMaybe $ M.elems $ flip M.mapWithKey (getAsts hf) $ \fs ast ->
+      (rss, g) <- liftMaybe $ 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
@@ -293,14 +292,14 @@ judgementForHole state nfp range = do
                    $ hypothesisFromBindings rss binds
           cls_hy = contextMethodHypothesis ctx
       case kind of
-        HieFromDisk hf' ->
+        HieFromDisk _hf' ->
           fail "Need a fresh hie file"
         HieFresh ->
           pure ( resulting_range
                , mkFirstJudgement
                    (local_hy <> cls_hy)
                    (isRhsHole rss tcs)
-                   goal
+                   g
                , ctx
                , dflags
                )
@@ -399,10 +398,10 @@ mergeFunBindMatches
     -> SrcSpan
     -> HsBind GhcPs
     -> HsBind GhcPs
-mergeFunBindMatches make_decl span (fb@FunBind {fun_matches = mg@MG {mg_alts = L alt_src alts}}) =
+mergeFunBindMatches make_decl span (fb@FunBind {fun_matches = mg@MG {mg_alts = L alts_src alts}}) =
     fb
       { fun_matches = mg
-        { mg_alts = L alt_src $ do
+        { mg_alts = L alts_src $ do
             alt@(L alt_src match) <- alts
             case span `isSubspanOf` alt_src of
               True -> do
@@ -486,11 +485,6 @@ getRhsPosVals rss tcs
   ) tcs
 
 
--- TODO(sandy): Make this more robust
-isHole :: OccName -> Bool
-isHole = isPrefixOf "_" . occNameString
-
-
 locateBiggest :: (Data r, Data a) => SrcSpan -> a -> Maybe r
 locateBiggest ss x = getFirst $ everything (<>)
   ( mkQ mempty $ \case
@@ -498,22 +492,9 @@ locateBiggest ss x = getFirst $ everything (<>)
     _ -> mempty
   )x
 
-locateSmallest :: (Data r, Data a) => SrcSpan -> a -> Maybe r
-locateSmallest ss x = getLast $ everything (<>)
-  ( mkQ mempty $ \case
-    L span r | ss `isSubspanOf` span -> pure r
-    _ -> mempty
-  )x
-
 locateFirst :: (Data r, Data a) => a -> Maybe r
 locateFirst x = getFirst $ everything (<>)
   ( mkQ mempty $ \case
     r -> pure r
   ) x
 
-locateLast :: (Data r, Data a) => a -> Maybe r
-locateLast x = getLast $ everything (<>)
-  ( mkQ mempty $ \case
-    r -> pure r
-  ) x
-
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
index dfe6d4d701..3e10e9685d 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
@@ -122,6 +122,10 @@ algebraicTyCon (splitTyConApp_maybe -> Just (tycon, _))
   | otherwise = Just tycon
 algebraicTyCon _ = Nothing
 
+
+------------------------------------------------------------------------------
+-- | We can't compare 'RdrName' for equality directly. Instead, compare them by
+-- their 'OccName's.
 eqRdrName :: RdrName -> RdrName -> Bool
 eqRdrName = (==) `on` occNameString . occName
 
@@ -136,14 +140,26 @@ containsHsVar name x = not $ null $ listify (
     _ -> False
   ) x
 
+
+------------------------------------------------------------------------------
+-- | Does this thing contain any holes?
 containsHole :: Data a => a -> Bool
 containsHole x = not $ null $ listify (
   \case
-    ((HsVar _ (L _ name)) :: HsExpr GhcPs) -> isPrefixOf "_" $ occNameString $ occName name
+    ((HsVar _ (L _ name)) :: HsExpr GhcPs) -> isHole $ occName name
     _ -> False
   ) x
 
 
+------------------------------------------------------------------------------
+-- | Check if an 'OccName' is a hole
+isHole :: OccName -> Bool
+-- TODO(sandy): Make this more robust
+isHole = isPrefixOf "_" . occNameString
+
+
+------------------------------------------------------------------------------
+-- | Get all of the referenced occnames.
 allOccNames :: Data a => a -> Set OccName
 allOccNames = everything (<>) $ mkQ mempty $ \case
     a -> S.singleton a
@@ -166,11 +182,15 @@ pattern Lambda pats body <-
     Lambda pats body = lambda pats body
 
 
+------------------------------------------------------------------------------
+-- | A GRHS that caontains no guards.
 pattern UnguardedRHSs :: HsExpr GhcPs -> GRHSs GhcPs (LHsExpr GhcPs)
 pattern UnguardedRHSs body <-
   GRHSs {grhssGRHSs = [L _ (GRHS _ [] (L _ body))]}
 
 
+------------------------------------------------------------------------------
+-- | A match with a single pattern. Case matches are always 'SinglePatMatch'es.
 pattern SinglePatMatch :: Pat GhcPs -> HsExpr GhcPs -> Match GhcPs (LHsExpr GhcPs)
 pattern SinglePatMatch pat body <-
   Match { m_pats = [fromPatCompatPs -> pat]
@@ -178,6 +198,8 @@ pattern SinglePatMatch pat body <-
         }
 
 
+------------------------------------------------------------------------------
+-- | Helper function for defining the 'Case' pattern.
 unpackMatches :: [Match GhcPs (LHsExpr GhcPs)] -> Maybe [(Pat GhcPs, HsExpr GhcPs)]
 unpackMatches [] = Just []
 unpackMatches (SinglePatMatch pat body : matches) =
@@ -256,6 +278,10 @@ dataConExTys = DataCon.dataConExTyVars
 #endif
 
 
+------------------------------------------------------------------------------
+-- | In GHC 8.8, sometimes patterns are wrapped in 'XPat'. It's not clear why,
+-- but if we don't remove these wrappers, many functions that operate on
+-- patterns fail to match.
 unXPat :: Pat GhcPs -> Pat GhcPs
 #if __GLASGOW_HASKELL__ == 808
 unXPat (XPat (L _ pat)) = unXPat pat

From b857ca79ae763d347b61f2016dea772e0112b3c5 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 15 Feb 2021 19:18:51 -0800
Subject: [PATCH 23/38] Cleanup sus errors

---
 ghcide/src/Development/IDE/GHC/ExactPrint.hs  | 13 ++++---
 .../src/Ide/Plugin/Tactic.hs                  | 37 ++++++++++++-------
 2 files changed, 31 insertions(+), 19 deletions(-)

diff --git a/ghcide/src/Development/IDE/GHC/ExactPrint.hs b/ghcide/src/Development/IDE/GHC/ExactPrint.hs
index 6002419d73..6ba6fc84d1 100644
--- a/ghcide/src/Development/IDE/GHC/ExactPrint.hs
+++ b/ghcide/src/Development/IDE/GHC/ExactPrint.hs
@@ -221,14 +221,16 @@ graftWithoutParentheses dst val = Graft $ \dflags a -> do
 parseDecls :: DynFlags -> FilePath -> String -> ParseResult (LHsDecl GhcPs)
 parseDecls dflags fp str = do
   let mono_decls = fmap unlines $ groupByFirstLine $ lines str
-  decls <- for (zip [id @Int 0..] mono_decls) $ \(ix, line) -> parseDecl dflags (fp <> show ix) line
-  pure $ mergeDecls decls
+  decls <-
+    for (zip [id @Int 0..] mono_decls) $ \(ix, line) ->
+      parseDecl dflags (fp <> show ix) line
+  mergeDecls decls
 
 
 ------------------------------------------------------------------------------
 -- | Combine decls together. See 'parseDecl' for more information.
-mergeDecls :: [(Anns, LHsDecl GhcPs)] -> (Anns, LHsDecl GhcPs)
-mergeDecls [x] = x
+mergeDecls :: [(Anns, LHsDecl GhcPs)] -> ParseResult (LHsDecl GhcPs)
+mergeDecls [x] = pure x
 mergeDecls ((anns,  L _ (ValD ext fb@FunBind{fun_matches = mg@MG {mg_alts = L _ alts}}))
           -- Since 'groupByFirstLine' separates matches, we are guaranteed to
           -- only have a single alternative here. We want to add it to 'alts'
@@ -241,7 +243,8 @@ mergeDecls ((anns,  L _ (ValD ext fb@FunBind{fun_matches = mg@MG {mg_alts = L _
         { fun_matches = mg { mg_alts = noLoc $ alts <> [alt] }
         }
     ) : decls
-mergeDecls _ = error "mergeDecls called with something that isn't a ValD FunBind"
+mergeDecls _ =
+  Left (noSrcSpan, "mergeDecls: attempted to merge something that wasn't a ValD FunBind")
 
 
 ------------------------------------------------------------------------------
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
index 35b6a3fd7b..d9c7433979 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
@@ -397,8 +397,9 @@ mergeFunBindMatches
     :: ([Pat GhcPs] -> LHsDecl GhcPs)
     -> SrcSpan
     -> HsBind GhcPs
-    -> HsBind GhcPs
+    -> Either String (HsBind GhcPs)
 mergeFunBindMatches make_decl span (fb@FunBind {fun_matches = mg@MG {mg_alts = L alts_src alts}}) =
+  pure $
     fb
       { fun_matches = mg
         { mg_alts = L alts_src $ do
@@ -412,7 +413,11 @@ mergeFunBindMatches make_decl span (fb@FunBind {fun_matches = mg@MG {mg_alts = L
               False -> pure alt
         }
       }
-mergeFunBindMatches _ _ _ = error "called on something that isnt a funbind"
+mergeFunBindMatches _ _ _ = Left "mergeFunBindMatches: called on something that isnt a funbind"
+
+
+noteT :: String -> TransformT (Either String) a
+noteT = lift . Left
 
 ------------------------------------------------------------------------------
 -- | Helper function to route 'mergeFunBindMatches' into the right place in an
@@ -425,25 +430,29 @@ graftDecl
 graftDecl span
     make_decl
     (L src (ValD ext fb))
-  = pure $ Just $ pure $ L src $ ValD ext $ mergeFunBindMatches make_decl span fb
--- TODO(sandy): default methods
+  = either noteT (pure . Just . pure . L src . ValD ext) $
+      mergeFunBindMatches make_decl span fb
+-- TODO(sandy): add another case for default methods in class definitions
 graftDecl span
     make_decl
     (L src (InstD ext cid@ClsInstD{cid_inst = cidi@ClsInstDecl{cid_sigs = _sigs, cid_binds = binds}}))
-  = pure $ Just $ pure $ L src $ InstD ext $ cid
-      { cid_inst = cidi
-        { cid_binds = listToBag $ do
-            b@(L bsrc bind) <- bagToList binds
-            case bind of
-              fb@FunBind{}
-                | span `isSubspanOf` bsrc -> pure $ L bsrc $ mergeFunBindMatches make_decl span fb
-              _ -> pure b
+  = do
+      binds' <-
+        for (bagToList binds) $ \b@(L bsrc bind) -> do
+          case bind of
+            fb@FunBind{}
+              | span `isSubspanOf` bsrc -> either noteT (pure . L bsrc) $ mergeFunBindMatches make_decl span fb
+            _ -> pure b
+
+      pure $ Just $ pure $ L src $ InstD ext $ cid
+        { cid_inst = cidi
+          { cid_binds = listToBag binds'
+          }
         }
-      }
 graftDecl span _ x = do
   traceMX "biggest" $ unsafeRender $ locateBiggest @(Match GhcPs (LHsExpr GhcPs)) span x
   traceMX "first" $ unsafeRender $ locateFirst @(Match GhcPs (LHsExpr GhcPs)) x
-  pure $ Just [x]
+  noteT "graftDecl: don't know about this AST form"
 
 
 

From 3ea09c372b63b3610f97b003963d7fcb604f16a8 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 15 Feb 2021 21:23:15 -0800
Subject: [PATCH 24/38] Fix parse errors in GHC > 8.8

---
 ghcide/src/Development/IDE/GHC/ExactPrint.hs | 28 +++++++++++++++-----
 1 file changed, 21 insertions(+), 7 deletions(-)

diff --git a/ghcide/src/Development/IDE/GHC/ExactPrint.hs b/ghcide/src/Development/IDE/GHC/ExactPrint.hs
index 6ba6fc84d1..e026ca0f0d 100644
--- a/ghcide/src/Development/IDE/GHC/ExactPrint.hs
+++ b/ghcide/src/Development/IDE/GHC/ExactPrint.hs
@@ -1,9 +1,10 @@
-{-# LANGUAGE CPP #-}
+{-# LANGUAGE CPP                #-}
 {-# LANGUAGE DerivingStrategies #-}
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE OverloadedStrings #-}
-{-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE GADTs              #-}
+{-# LANGUAGE OverloadedStrings  #-}
+{-# LANGUAGE RankNTypes         #-}
+{-# LANGUAGE TupleSections      #-}
+{-# LANGUAGE TypeFamilies       #-}
 
 module Development.IDE.GHC.ExactPrint
     ( Graft(..),
@@ -67,6 +68,11 @@ import Data.Traversable (for)
 #if __GLASGOW_HASKELL__ == 808
 import Control.Arrow
 #endif
+#if __GLASGOW_HASKELL__ > 808
+import Bag (listToBag)
+import ErrUtils (mkErrMsg)
+import Outputable (text, neverQualify)
+#endif
 
 
 ------------------------------------------------------------------------------
@@ -243,8 +249,16 @@ mergeDecls ((anns,  L _ (ValD ext fb@FunBind{fun_matches = mg@MG {mg_alts = L _
         { fun_matches = mg { mg_alts = noLoc $ alts <> [alt] }
         }
     ) : decls
-mergeDecls _ =
-  Left (noSrcSpan, "mergeDecls: attempted to merge something that wasn't a ValD FunBind")
+mergeDecls _ = throwParseError "mergeDecls: attempted to merge something that wasn't a ValD FunBind"
+
+
+throwParseError :: String -> ParseResult a
+#if __GLASGOW_HASKELL__ > 808
+throwParseError
+  = Left . listToBag . pure . mkErrMsg unsafeGlobalDynFlags noSrcSpan neverQualify . text
+#else
+throwParseError = Left . (noSrcSpan, )
+#endif
 
 
 ------------------------------------------------------------------------------

From b2236b86136bacdb6c29f63a232daf8a6272a5d8 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Tue, 16 Feb 2021 12:07:24 -0800
Subject: [PATCH 25/38] Update comment around unXPat

---
 plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
index 3e10e9685d..a3efa75a6b 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
@@ -279,9 +279,11 @@ dataConExTys = DataCon.dataConExTyVars
 
 
 ------------------------------------------------------------------------------
--- | In GHC 8.8, sometimes patterns are wrapped in 'XPat'. It's not clear why,
--- but if we don't remove these wrappers, many functions that operate on
--- patterns fail to match.
+-- | In GHC 8.8, sometimes patterns are wrapped in 'XPat'.
+-- The nitty gritty details are explained at
+-- https://blog.shaynefletcher.org/2020/03/ghc-haskell-pats-and-lpats.html
+--
+-- We need to remove these in order to succesfull find patterns.
 unXPat :: Pat GhcPs -> Pat GhcPs
 #if __GLASGOW_HASKELL__ == 808
 unXPat (XPat (L _ pat)) = unXPat pat

From 1261489ef44484a078379a3adee0fbb19120b114 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Tue, 16 Feb 2021 12:41:03 -0800
Subject: [PATCH 26/38] Cleanup ExactPrint to split FunBind matches

---
 ghcide/src/Development/IDE/GHC/ExactPrint.hs | 94 ++++++--------------
 1 file changed, 28 insertions(+), 66 deletions(-)

diff --git a/ghcide/src/Development/IDE/GHC/ExactPrint.hs b/ghcide/src/Development/IDE/GHC/ExactPrint.hs
index 397493c0e3..2fb95bbbdb 100644
--- a/ghcide/src/Development/IDE/GHC/ExactPrint.hs
+++ b/ghcide/src/Development/IDE/GHC/ExactPrint.hs
@@ -63,8 +63,9 @@ import Language.LSP.Types.Capabilities (ClientCapabilities)
 import Outputable (Outputable, ppr, showSDoc)
 import Retrie.ExactPrint hiding (parseDecl, parseExpr, parsePattern, parseType)
 import Parser (parseIdentifier)
-import Data.List (isPrefixOf)
 import Data.Traversable (for)
+import Data.Foldable (Foldable(fold))
+import Data.Bool (bool)
 #if __GLASGOW_HASKELL__ == 808
 import Control.Arrow
 #endif
@@ -213,70 +214,6 @@ graftWithoutParentheses dst val = Graft $ \dflags a -> do
             a
 
 
-------------------------------------------------------------------------------
--- | 'parseDecl' fails to parse decls that span multiple lines at the top
--- layout --- eg. things like:
---
--- @
--- not True = False
--- not False = True
--- @
---
--- This function splits up each top-layout declaration, parses them
--- individually, and then merges them back into a single decl.
-parseDecls :: DynFlags -> FilePath -> String -> ParseResult (LHsDecl GhcPs)
-parseDecls dflags fp str = do
-  let mono_decls = fmap unlines $ groupByFirstLine $ lines str
-  decls <-
-    for (zip [id @Int 0..] mono_decls) $ \(ix, line) ->
-      parseDecl dflags (fp <> show ix) line
-  mergeDecls decls
-
-
-------------------------------------------------------------------------------
--- | Combine decls together. See 'parseDecl' for more information.
-mergeDecls :: [(Anns, LHsDecl GhcPs)] -> ParseResult (LHsDecl GhcPs)
-mergeDecls [x] = pure x
-mergeDecls ((anns,  L _ (ValD ext fb@FunBind{fun_matches = mg@MG {mg_alts = L _ alts}}))
-          -- Since 'groupByFirstLine' separates matches, we are guaranteed to
-          -- only have a single alternative here. We want to add it to 'alts'
-          -- above.
-          : (anns', L _ (ValD _ FunBind{fun_matches = MG {mg_alts = L _ [alt]}}))
-          : decls) =
-  mergeDecls $
-    ( anns <> setPrecedingLines alt 1 0 anns'
-    , noLoc $ ValD ext $ fb
-        { fun_matches = mg { mg_alts = noLoc $ alts <> [alt] }
-        }
-    ) : decls
-mergeDecls _ = throwParseError "mergeDecls: attempted to merge something that wasn't a ValD FunBind"
-
-
-throwParseError :: String -> ParseResult a
-#if __GLASGOW_HASKELL__ > 808
-throwParseError
-  = Left . listToBag . pure . mkErrMsg unsafeGlobalDynFlags noSrcSpan neverQualify . text
-#else
-throwParseError = Left . (noSrcSpan, )
-#endif
-
-
-------------------------------------------------------------------------------
--- | Groups strings by the Haskell top-layout rules, assuming each element of
--- the list corresponds to a line. For example, the list
---
--- @["a", " a1", " a2", "b", " b1"]@
---
--- will be grouped to
---
--- @[["a", " a1", " a2"], ["b", " b1"]]@
-groupByFirstLine :: [String] -> [[String]]
-groupByFirstLine [] = []
-groupByFirstLine (str : strs) =
-  let (same, diff) = span (isPrefixOf " ") strs
-   in (str : same) : groupByFirstLine diff
-
-
 ------------------------------------------------------------------------------
 
 graftWithM ::
@@ -468,13 +405,38 @@ annotate dflags ast = do
 
 -- | Given an 'LHsDecl', compute its exactprint annotations.
 annotateDecl :: DynFlags -> LHsDecl GhcPs -> TransformT (Either String) (Anns, LHsDecl GhcPs)
+-- The 'parseDecl' function fails to parse 'FunBind' 'ValD's which contain
+-- multiple matches. To work around this, we split the single
+-- 'FunBind'-of-multiple-matches into multiple 'FunBind's-of-single-matchs, and
+-- then merge them all back together.
+annotateDecl dflags
+            (L src (
+                ValD ext fb@FunBind
+                  { fun_matches = mg@MG { mg_alts = L alt_src alts@(_:_)}
+                  })) = do
+    let set_matches matches =
+          ValD ext fb { fun_matches = mg { mg_alts = L alt_src matches }}
+
+    (anns', alts') <- fmap unzip $ for (zip [0..] alts) $ \(ix :: Int, alt) -> do
+      uniq <- show <$> uniqueSrcSpanT
+      let rendered = render dflags $ set_matches [alt]
+      lift (mapLeft show $ parseDecl dflags uniq rendered) >>= \case
+        (ann, L _ (ValD _ FunBind { fun_matches = MG { mg_alts = L _ [alt']}}))
+           -> pure (bool id (setPrecedingLines alt' 1 0) (ix /= 0) ann, alt')
+        _ ->  lift $ Left "annotateDecl: didn't parse a single FunBind match"
+
+    let expr' = L src $ set_matches alts'
+        anns'' = setPrecedingLines expr' 1 0 $ fold anns'
+
+    pure (anns'', expr')
 annotateDecl dflags ast = do
     uniq <- show <$> uniqueSrcSpanT
     let rendered = render dflags ast
-    (anns, expr') <- lift $ mapLeft show $ parseDecls dflags uniq rendered
+    (anns, expr') <- lift $ mapLeft show $ parseDecl dflags uniq rendered
     let anns' = setPrecedingLines expr' 1 0 anns
     pure (anns', expr')
 ------------------------------------------------------------------------------
+------------------------------------------------------------------------------
 
 -- | Print out something 'Outputable'.
 render :: Outputable a => DynFlags -> a -> String

From d8a81982de71ffcd974fec120be5724b4cc83e80 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Tue, 16 Feb 2021 12:50:21 -0800
Subject: [PATCH 27/38] Minor haddock tweak

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

diff --git a/ghcide/src/Development/IDE/GHC/ExactPrint.hs b/ghcide/src/Development/IDE/GHC/ExactPrint.hs
index 2fb95bbbdb..5e2001b03a 100644
--- a/ghcide/src/Development/IDE/GHC/ExactPrint.hs
+++ b/ghcide/src/Development/IDE/GHC/ExactPrint.hs
@@ -407,8 +407,8 @@ annotate dflags ast = do
 annotateDecl :: DynFlags -> LHsDecl GhcPs -> TransformT (Either String) (Anns, LHsDecl GhcPs)
 -- The 'parseDecl' function fails to parse 'FunBind' 'ValD's which contain
 -- multiple matches. To work around this, we split the single
--- 'FunBind'-of-multiple-matches into multiple 'FunBind's-of-single-matchs, and
--- then merge them all back together.
+-- 'FunBind'-of-multiple-'Match'es into multiple 'FunBind's-of-one-'Match',
+-- and then merge them all back together.
 annotateDecl dflags
             (L src (
                 ValD ext fb@FunBind
@@ -435,7 +435,7 @@ annotateDecl dflags ast = do
     (anns, expr') <- lift $ mapLeft show $ parseDecl dflags uniq rendered
     let anns' = setPrecedingLines expr' 1 0 anns
     pure (anns', expr')
-------------------------------------------------------------------------------
+
 ------------------------------------------------------------------------------
 
 -- | Print out something 'Outputable'.

From 529e4dd229c7eda10c3eaa6b1613ac69d4aec1f5 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Tue, 16 Feb 2021 13:17:08 -0800
Subject: [PATCH 28/38] Bad suggest, hlint

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

diff --git a/ghcide/src/Development/IDE/GHC/ExactPrint.hs b/ghcide/src/Development/IDE/GHC/ExactPrint.hs
index 5e2001b03a..cacf7450bc 100644
--- a/ghcide/src/Development/IDE/GHC/ExactPrint.hs
+++ b/ghcide/src/Development/IDE/GHC/ExactPrint.hs
@@ -6,6 +6,8 @@
 {-# LANGUAGE TupleSections      #-}
 {-# LANGUAGE TypeFamilies       #-}
 
+{- HLINT ignore "Use zipFrom" -}
+
 module Development.IDE.GHC.ExactPrint
     ( Graft(..),
       graft,

From cffba271ca1ef208ef5be0db2752ee1a232d9463 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Tue, 16 Feb 2021 15:39:36 -0800
Subject: [PATCH 29/38] I hate hlint with so much passion

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

diff --git a/ghcide/src/Development/IDE/GHC/ExactPrint.hs b/ghcide/src/Development/IDE/GHC/ExactPrint.hs
index cacf7450bc..4e038aced3 100644
--- a/ghcide/src/Development/IDE/GHC/ExactPrint.hs
+++ b/ghcide/src/Development/IDE/GHC/ExactPrint.hs
@@ -3,7 +3,6 @@
 {-# LANGUAGE GADTs              #-}
 {-# LANGUAGE OverloadedStrings  #-}
 {-# LANGUAGE RankNTypes         #-}
-{-# LANGUAGE TupleSections      #-}
 {-# LANGUAGE TypeFamilies       #-}
 
 {- HLINT ignore "Use zipFrom" -}

From d8b37535509be421ab43e5d66985614b936205ed Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Tue, 16 Feb 2021 17:59:49 -0800
Subject: [PATCH 30/38] Pull out tactic providers

---
 .../hls-tactics-plugin.cabal                  |   2 +
 .../src/Ide/Plugin/Tactic.hs                  | 159 +--------------
 .../Tactic/LanguageServer/TacticProviders.hs  | 181 ++++++++++++++++++
 3 files changed, 190 insertions(+), 152 deletions(-)
 create mode 100644 plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs

diff --git a/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal b/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal
index 113380f3eb..c043564807 100644
--- a/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal
+++ b/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal
@@ -33,6 +33,8 @@ library
     Ide.Plugin.Tactic.Judgements
     Ide.Plugin.Tactic.KnownStrategies
     Ide.Plugin.Tactic.KnownStrategies.QuickCheck
+    Ide.Plugin.Tactic.LanguageServer
+    Ide.Plugin.Tactic.LanguageServer.TacticProviders
     Ide.Plugin.Tactic.Machinery
     Ide.Plugin.Tactic.Naming
     Ide.Plugin.Tactic.Range
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
index 8fd10c326d..fae7fed137 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
@@ -1,13 +1,8 @@
-{-# LANGUAGE DeriveAnyClass      #-}
-{-# LANGUAGE DeriveGeneric       #-}
-{-# LANGUAGE GADTs               #-}
-{-# LANGUAGE LambdaCase          #-}
-{-# LANGUAGE NumDecimals         #-}
-{-# LANGUAGE OverloadedStrings   #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TupleSections       #-}
-{-# LANGUAGE TypeApplications    #-}
-{-# LANGUAGE ViewPatterns        #-}
+{-# LANGUAGE GADTs             #-}
+{-# LANGUAGE LambdaCase        #-}
+{-# LANGUAGE NumDecimals       #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE TypeApplications  #-}
 
 -- | A plugin that uses tactics to synthesize code
 module Ide.Plugin.Tactic
@@ -19,7 +14,6 @@ module Ide.Plugin.Tactic
 import           Bag (listToBag, bagToList)
 import           Control.Arrow
 import           Control.Monad
-import           Control.Monad.Error.Class (MonadError(throwError))
 import           Control.Monad.Trans
 import           Control.Monad.Trans.Maybe
 import           Data.Aeson
@@ -46,9 +40,6 @@ import           Development.IDE.GHC.ExactPrint
 import           Development.IDE.Spans.LocalBindings (getDefiningBindings)
 import           Development.Shake (Action)
 import qualified FastString
-import           GHC.Generics (Generic)
-import           GHC.LanguageExtensions.Type (Extension (LambdaCase))
-import           Ide.Plugin.Tactic.Auto
 import           Ide.Plugin.Tactic.CaseSplit
 import           Ide.Plugin.Tactic.Context
 import           Ide.Plugin.Tactic.GHC
@@ -57,16 +48,15 @@ import           Ide.Plugin.Tactic.Range
 import           Ide.Plugin.Tactic.Tactics
 import           Ide.Plugin.Tactic.TestTypes
 import           Ide.Plugin.Tactic.Types
-import           Ide.PluginUtils
 import           Ide.Types
 import           Language.LSP.Server
 import           Language.LSP.Types
 import           OccName
 import           Prelude hiding (span)
-import           Refinery.Tactic (goal)
 import           SrcLoc (containsSpan)
 import           System.Timeout
 import           TcRnTypes (tcg_binds)
+import           Ide.Plugin.Tactic.LanguageServer.TacticProviders
 
 
 descriptor :: PluginId -> PluginDescriptor IdeState
@@ -84,16 +74,6 @@ descriptor plId = (defaultPluginDescriptor plId)
 tacticDesc :: T.Text -> T.Text
 tacticDesc name = "fill the hole using the " <> name <> " tactic"
 
-------------------------------------------------------------------------------
--- | A 'TacticProvider' is a way of giving context-sensitive actions to the LS
--- UI.
-type TacticProvider = DynFlags -> PluginId -> Uri -> Range -> Judgement -> IO [Command |? CodeAction]
-
-
-------------------------------------------------------------------------------
--- | Construct a 'CommandId'
-tcCommandId :: TacticCommand -> CommandId
-tcCommandId c = coerce $ T.pack $ "tactics" <> show c <> "Command"
 
 
 ------------------------------------------------------------------------------
@@ -101,68 +81,6 @@ tcCommandId c = coerce $ T.pack $ "tactics" <> show c <> "Command"
 tcCommandName :: TacticCommand -> T.Text
 tcCommandName = T.pack . show
 
-------------------------------------------------------------------------------
--- | Mapping from tactic commands to their contextual providers. See 'provide',
--- 'filterGoalType' and 'filterBindingType' for the nitty gritty.
-commandProvider :: TacticCommand -> TacticProvider
-commandProvider Auto  = provide Auto ""
-commandProvider Intros =
-  filterGoalType isFunction $
-    provide Intros ""
-commandProvider Destruct =
-  filterBindingType destructFilter $ \occ _ ->
-    provide Destruct $ T.pack $ occNameString occ
-commandProvider Homomorphism =
-  filterBindingType homoFilter $ \occ _ ->
-    provide Homomorphism $ T.pack $ occNameString occ
-commandProvider DestructLambdaCase =
-  requireExtension LambdaCase $
-    filterGoalType (isJust . lambdaCaseable) $
-      provide DestructLambdaCase ""
-commandProvider HomomorphismLambdaCase =
-  requireExtension LambdaCase $
-    filterGoalType ((== Just True) . lambdaCaseable) $
-      provide HomomorphismLambdaCase ""
-
-
-------------------------------------------------------------------------------
--- | A mapping from tactic commands to actual tactics for refinery.
-commandTactic :: TacticCommand -> OccName -> TacticsM ()
-commandTactic Auto         = const auto
-commandTactic Intros       = const intros
-commandTactic Destruct     = useNameFromHypothesis destruct
-commandTactic Homomorphism = useNameFromHypothesis homo
-commandTactic DestructLambdaCase     = const destructLambdaCase
-commandTactic HomomorphismLambdaCase = const homoLambdaCase
-
-
-------------------------------------------------------------------------------
--- | Lift a function over 'HyInfo's to one that takes an 'OccName' and tries to
--- look it up in the hypothesis.
-useNameFromHypothesis :: (HyInfo CType -> TacticsM a) -> OccName -> TacticsM a
-useNameFromHypothesis f name = do
-  hy <- jHypothesis <$> goal
-  case M.lookup name $ hyByName hy of
-    Just hi -> f hi
-    Nothing -> throwError $ NotInScope name
-
-
-
-------------------------------------------------------------------------------
--- | We should show homos only when the goal type is the same as the binding
--- type, and that both are usual algebraic types.
-homoFilter :: Type -> Type -> Bool
-homoFilter (algebraicTyCon -> Just t1) (algebraicTyCon -> Just t2) = t1 == t2
-homoFilter _ _ = False
-
-
-------------------------------------------------------------------------------
--- | We should show destruct for bindings only when those bindings have usual
--- algebraic types.
-destructFilter :: Type -> Type -> Bool
-destructFilter _ (algebraicTyCon -> Just _) = True
-destructFilter _ _ = False
-
 
 runIde :: IdeState -> Action a -> IO a
 runIde state = runAction "tactic" state
@@ -182,71 +100,8 @@ codeActionProvider state plId (CodeActionParams _ _ (TextDocumentIdentifier uri)
             range
             jdg
         pure $ Right $ List actions
-codeActionProvider _ _ _ = pure $ Right $ codeActions []
-
-
-codeActions :: [CodeAction] -> List (Command |? CodeAction)
-codeActions = List . fmap InR
-
-
-------------------------------------------------------------------------------
--- | Terminal constructor for providing context-sensitive tactics. Tactics
--- given by 'provide' are always available.
-provide :: TacticCommand -> T.Text -> TacticProvider
-provide tc name _ plId uri range _ = do
-  let title = tacticTitle tc name
-      params = TacticParams { tp_file = uri , tp_range = range , tp_var_name = name }
-      cmd = mkLspCommand plId (tcCommandId tc) title (Just [toJSON params])
-  pure
-    $ pure
-    $ InR
-    $ CodeAction title (Just CodeActionQuickFix) Nothing Nothing Nothing Nothing
-    $ Just cmd
-
+codeActionProvider _ _ _ = pure $ Right $ List []
 
-------------------------------------------------------------------------------
--- | Restrict a 'TacticProvider', making sure it appears only when the given
--- predicate holds for the goal.
-requireExtension :: Extension -> TacticProvider -> TacticProvider
-requireExtension ext tp dflags plId uri range jdg =
-  case xopt ext dflags of
-    True  -> tp dflags plId uri range jdg
-    False -> pure []
-
-
-------------------------------------------------------------------------------
--- | Restrict a 'TacticProvider', making sure it appears only when the given
--- predicate holds for the goal.
-filterGoalType :: (Type -> Bool) -> TacticProvider -> TacticProvider
-filterGoalType p tp dflags plId uri range jdg =
-  case p $ unCType $ jGoal jdg of
-    True  -> tp dflags plId uri range jdg
-    False -> pure []
-
-
-------------------------------------------------------------------------------
--- | Multiply a 'TacticProvider' for each binding, making sure it appears only
--- when the given predicate holds over the goal and binding types.
-filterBindingType
-    :: (Type -> Type -> Bool)  -- ^ Goal and then binding types.
-    -> (OccName -> Type -> TacticProvider)
-    -> TacticProvider
-filterBindingType p tp dflags plId uri range jdg =
-  let hy = jHypothesis 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 dflags plId uri range jdg
-              False -> pure []
-
-
-data TacticParams = TacticParams
-    { tp_file :: Uri -- ^ Uri of the file to fill the hole in
-    , tp_range :: Range -- ^ The range of the hole
-    , tp_var_name :: T.Text
-    }
-  deriving (Show, Eq, Generic, ToJSON, FromJSON)
 
 
 ------------------------------------------------------------------------------
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs
new file mode 100644
index 0000000000..c66c4d7bd7
--- /dev/null
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs
@@ -0,0 +1,181 @@
+{-# LANGUAGE DeriveAnyClass     #-}
+{-# LANGUAGE DeriveGeneric      #-}
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE OverloadedStrings  #-}
+{-# LANGUAGE ViewPatterns       #-}
+
+module Ide.Plugin.Tactic.LanguageServer.TacticProviders
+  ( commandProvider
+  , commandTactic
+  , tcCommandId
+  , TacticParams (..)
+  ) where
+
+import           Control.Monad
+import           Control.Monad.Error.Class (MonadError(throwError))
+import           Data.Aeson
+import           Data.Coerce
+import qualified Data.Map as M
+import           Data.Maybe
+import           Data.Monoid
+import qualified Data.Text as T
+import           Data.Traversable
+import           Development.IDE.GHC.Compat
+import           GHC.Generics (Generic)
+import           GHC.LanguageExtensions.Type (Extension (LambdaCase))
+import           Ide.Plugin.Tactic.Auto
+import           Ide.Plugin.Tactic.GHC
+import           Ide.Plugin.Tactic.Judgements
+import           Ide.Plugin.Tactic.Tactics
+import           Ide.Plugin.Tactic.TestTypes
+import           Ide.Plugin.Tactic.Types
+import           Ide.PluginUtils
+import           Ide.Types
+import           Language.LSP.Types
+import           OccName
+import           Prelude hiding (span)
+import           Refinery.Tactic (goal)
+
+
+------------------------------------------------------------------------------
+-- | A mapping from tactic commands to actual tactics for refinery.
+commandTactic :: TacticCommand -> OccName -> TacticsM ()
+commandTactic Auto         = const auto
+commandTactic Intros       = const intros
+commandTactic Destruct     = useNameFromHypothesis destruct
+commandTactic Homomorphism = useNameFromHypothesis homo
+commandTactic DestructLambdaCase     = const destructLambdaCase
+commandTactic HomomorphismLambdaCase = const homoLambdaCase
+
+
+------------------------------------------------------------------------------
+-- | Mapping from tactic commands to their contextual providers. See 'provide',
+-- 'filterGoalType' and 'filterBindingType' for the nitty gritty.
+commandProvider :: TacticCommand -> TacticProvider
+commandProvider Auto  = provide Auto ""
+commandProvider Intros =
+  filterGoalType isFunction $
+    provide Intros ""
+commandProvider Destruct =
+  filterBindingType destructFilter $ \occ _ ->
+    provide Destruct $ T.pack $ occNameString occ
+commandProvider Homomorphism =
+  filterBindingType homoFilter $ \occ _ ->
+    provide Homomorphism $ T.pack $ occNameString occ
+commandProvider DestructLambdaCase =
+  requireExtension LambdaCase $
+    filterGoalType (isJust . lambdaCaseable) $
+      provide DestructLambdaCase ""
+commandProvider HomomorphismLambdaCase =
+  requireExtension LambdaCase $
+    filterGoalType ((== Just True) . lambdaCaseable) $
+      provide HomomorphismLambdaCase ""
+
+
+------------------------------------------------------------------------------
+-- | A 'TacticProvider' is a way of giving context-sensitive actions to the LS
+-- UI.
+type TacticProvider
+     = DynFlags
+    -> PluginId
+    -> Uri
+    -> Range
+    -> Judgement
+    -> IO [Command |? CodeAction]
+
+
+data TacticParams = TacticParams
+    { tp_file     :: Uri    -- ^ Uri of the file to fill the hole in
+    , tp_range    :: Range  -- ^ The range of the hole
+    , tp_var_name :: T.Text
+    }
+  deriving stock (Show, Eq, Generic)
+  deriving anyclass (ToJSON, FromJSON)
+
+
+------------------------------------------------------------------------------
+-- | Restrict a 'TacticProvider', making sure it appears only when the given
+-- predicate holds for the goal.
+requireExtension :: Extension -> TacticProvider -> TacticProvider
+requireExtension ext tp dflags plId uri range jdg =
+  case xopt ext dflags of
+    True  -> tp dflags plId uri range jdg
+    False -> pure []
+
+
+------------------------------------------------------------------------------
+-- | Restrict a 'TacticProvider', making sure it appears only when the given
+-- predicate holds for the goal.
+filterGoalType :: (Type -> Bool) -> TacticProvider -> TacticProvider
+filterGoalType p tp dflags plId uri range jdg =
+  case p $ unCType $ jGoal jdg of
+    True  -> tp dflags plId uri range jdg
+    False -> pure []
+
+
+------------------------------------------------------------------------------
+-- | Multiply a 'TacticProvider' for each binding, making sure it appears only
+-- when the given predicate holds over the goal and binding types.
+filterBindingType
+    :: (Type -> Type -> Bool)  -- ^ Goal and then binding types.
+    -> (OccName -> Type -> TacticProvider)
+    -> TacticProvider
+filterBindingType p tp dflags plId uri range jdg =
+  let hy = jHypothesis 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 dflags plId uri range jdg
+              False -> pure []
+
+
+
+------------------------------------------------------------------------------
+-- | Lift a function over 'HyInfo's to one that takes an 'OccName' and tries to
+-- look it up in the hypothesis.
+useNameFromHypothesis :: (HyInfo CType -> TacticsM a) -> OccName -> TacticsM a
+useNameFromHypothesis f name = do
+  hy <- jHypothesis <$> goal
+  case M.lookup name $ hyByName hy of
+    Just hi -> f hi
+    Nothing -> throwError $ NotInScope name
+
+
+------------------------------------------------------------------------------
+-- | Terminal constructor for providing context-sensitive tactics. Tactics
+-- given by 'provide' are always available.
+provide :: TacticCommand -> T.Text -> TacticProvider
+provide tc name _ plId uri range _ = do
+  let title = tacticTitle tc name
+      params = TacticParams { tp_file = uri , tp_range = range , tp_var_name = name }
+      cmd = mkLspCommand plId (tcCommandId tc) title (Just [toJSON params])
+  pure
+    $ pure
+    $ InR
+    $ CodeAction title (Just CodeActionQuickFix) Nothing Nothing Nothing Nothing
+    $ Just cmd
+
+
+------------------------------------------------------------------------------
+-- | Construct a 'CommandId'
+tcCommandId :: TacticCommand -> CommandId
+tcCommandId c = coerce $ T.pack $ "tactics" <> show c <> "Command"
+
+
+
+------------------------------------------------------------------------------
+-- | We should show homos only when the goal type is the same as the binding
+-- type, and that both are usual algebraic types.
+homoFilter :: Type -> Type -> Bool
+homoFilter (algebraicTyCon -> Just t1) (algebraicTyCon -> Just t2) = t1 == t2
+homoFilter _ _ = False
+
+
+------------------------------------------------------------------------------
+-- | We should show destruct for bindings only when those bindings have usual
+-- algebraic types.
+destructFilter :: Type -> Type -> Bool
+destructFilter _ (algebraicTyCon -> Just _) = True
+destructFilter _ _ = False
+

From a73a3055a2fe2eb8bb6df814c274e6818af58c65 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Tue, 16 Feb 2021 18:04:44 -0800
Subject: [PATCH 31/38] Stick judgment and context into the RTR

---
 .../src/Ide/Plugin/Tactic.hs                  | 27 +++++++++----------
 .../src/Ide/Plugin/Tactic/Machinery.hs        | 13 +++++----
 .../src/Ide/Plugin/Tactic/Types.hs            |  4 ++-
 3 files changed, 23 insertions(+), 21 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
index fae7fed137..f95a5fe87f 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
@@ -182,7 +182,7 @@ tacticCmd tac state (TacticParams uri range var_name)
             Left err ->
               Left $ mkErr InvalidRequest $ T.pack $ show err
             Right rtr ->
-              mkWorkspaceEdits rtr jdg span ctx dflags clientCapabilities uri pm
+              mkWorkspaceEdits rtr span dflags clientCapabilities uri pm
         pure $ joinNote (mkErr InvalidRequest "timed out") x
 
       case res of
@@ -206,8 +206,8 @@ joinNote _ (Just a) = a
 ------------------------------------------------------------------------------
 -- | Turn a 'RunTacticResults' into concrete edits to make in the source
 -- document.
-mkWorkspaceEdits rtr jdg span ctx dflags clientCapabilities uri pm = do
-  let g = graftHole jdg (RealSrcSpan span) ctx rtr
+mkWorkspaceEdits rtr span dflags clientCapabilities uri pm = do
+  let g = graftHole (RealSrcSpan span) rtr
       response = transform dflags clientCapabilities uri g pm
    in case response of
         Right res -> Right $ Just res
@@ -219,25 +219,22 @@ mkWorkspaceEdits rtr jdg span ctx dflags clientCapabilities uri pm = do
 -- deals with top-level holes, in which we might need to fiddle with the
 -- 'Match's that bind variables.
 graftHole
-  :: Judgement' a2
-  -> SrcSpan
-  -> Context
-  -> RunTacticResults
-  -> Graft (Either String) ParsedSource
-graftHole jdg span ctx rtr
-  | _jIsTopHole jdg
+    :: SrcSpan
+    -> RunTacticResults
+    -> Graft (Either String) ParsedSource
+graftHole span rtr
+  | _jIsTopHole (rtr_jdg rtr)
       = graftSmallestDeclsWithM span
-      $ graftDecl span
-      $ \pats ->
-        splitToDecl (fst $ last $ ctxDefiningFuncs ctx)
+      $ graftDecl span $ \pats ->
+        splitToDecl (fst $ last $ ctxDefiningFuncs $ rtr_ctx rtr)
       $ iterateSplit
       $ mkFirstAgda (fmap unXPat pats)
       $ unLoc
       $ rtr_extract rtr
-graftHole jdg span _ rtr
+graftHole span rtr
   = graftWithoutParentheses span
     -- Parenthesize the extract iff we're not in a top level hole
-  $ bool maybeParensAST id (_jIsTopHole jdg)
+  $ bool maybeParensAST id (_jIsTopHole $ rtr_jdg rtr)
   $ rtr_extract rtr
 
 
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Machinery.hs
index 787fb6bb7d..a061aa43cd 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Machinery.hs
@@ -97,11 +97,14 @@ runTactic ctx jdg t =
                 Down $ scoreSolution ext jdg holes
         case sorted of
           (((tr, ext), _) : _) ->
-            Right
-              . RunTacticResults tr (simplify ext)
-              . reverse
-              . fmap fst
-              $ take 5 sorted
+            Right $
+              RunTacticResults
+                { rtr_trace = tr
+                , rtr_extract = simplify ext
+                , rtr_other_solns = reverse . fmap fst $ take 5 sorted
+                , rtr_jdg = jdg
+                , rtr_ctx = ctx
+                }
           -- guaranteed to not be empty
           _ -> Left []
 
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs
index 1c38cd15b2..c9744bab78 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs
@@ -337,7 +337,7 @@ data Context = Context
   , ctxModuleFuncs :: [(OccName, CType)]
     -- ^ Everything defined in the current module
   }
-  deriving stock (Eq, Ord)
+  deriving stock (Eq, Ord, Show)
 
 
 ------------------------------------------------------------------------------
@@ -374,6 +374,8 @@ data RunTacticResults = RunTacticResults
   { rtr_trace       :: Trace
   , rtr_extract     :: LHsExpr GhcPs
   , rtr_other_solns :: [(Trace, LHsExpr GhcPs)]
+  , rtr_jdg         :: Judgement
+  , rtr_ctx         :: Context
   } deriving Show
 
 

From b16c73035827677050e0499e818c595bdf99a1f4 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Tue, 16 Feb 2021 18:08:30 -0800
Subject: [PATCH 32/38] Add type for mkWorkspaceEdits

---
 plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
index f95a5fe87f..a3a6704d4a 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
@@ -44,19 +44,20 @@ import           Ide.Plugin.Tactic.CaseSplit
 import           Ide.Plugin.Tactic.Context
 import           Ide.Plugin.Tactic.GHC
 import           Ide.Plugin.Tactic.Judgements
+import           Ide.Plugin.Tactic.LanguageServer.TacticProviders
 import           Ide.Plugin.Tactic.Range
 import           Ide.Plugin.Tactic.Tactics
 import           Ide.Plugin.Tactic.TestTypes
 import           Ide.Plugin.Tactic.Types
 import           Ide.Types
 import           Language.LSP.Server
+import           Language.LSP.Types.Capabilities
 import           Language.LSP.Types
 import           OccName
 import           Prelude hiding (span)
 import           SrcLoc (containsSpan)
 import           System.Timeout
 import           TcRnTypes (tcg_binds)
-import           Ide.Plugin.Tactic.LanguageServer.TacticProviders
 
 
 descriptor :: PluginId -> PluginDescriptor IdeState
@@ -206,6 +207,14 @@ joinNote _ (Just a) = a
 ------------------------------------------------------------------------------
 -- | Turn a 'RunTacticResults' into concrete edits to make in the source
 -- document.
+mkWorkspaceEdits
+    :: RunTacticResults
+    -> RealSrcSpan
+    -> DynFlags
+    -> ClientCapabilities
+    -> Uri
+    -> Annotated ParsedSource
+    -> Either ResponseError (Maybe WorkspaceEdit)
 mkWorkspaceEdits rtr span dflags clientCapabilities uri pm = do
   let g = graftHole (RealSrcSpan span) rtr
       response = transform dflags clientCapabilities uri g pm

From c71b3f73b93183ef42c40c2b9d672f1995401f15 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Tue, 16 Feb 2021 18:30:57 -0800
Subject: [PATCH 33/38] Split up judgementForHole

---
 .../src/Ide/Plugin/Tactic.hs                  | 108 ++++++++++++------
 1 file changed, 72 insertions(+), 36 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
index a3a6704d4a..ef3c2eaba0 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
@@ -1,8 +1,10 @@
-{-# LANGUAGE GADTs             #-}
-{-# LANGUAGE LambdaCase        #-}
-{-# LANGUAGE NumDecimals       #-}
-{-# LANGUAGE OverloadedStrings #-}
-{-# LANGUAGE TypeApplications  #-}
+{-# LANGUAGE FlexibleContexts    #-}
+{-# LANGUAGE GADTs               #-}
+{-# LANGUAGE LambdaCase          #-}
+{-# LANGUAGE NumDecimals         #-}
+{-# LANGUAGE OverloadedStrings   #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications    #-}
 
 -- | A plugin that uses tactics to synthesize code
 module Ide.Plugin.Tactic
@@ -37,8 +39,8 @@ import           Development.IDE.Core.Shake (useWithStale, IdeState (..))
 import           Development.IDE.GHC.Compat
 import           Development.IDE.GHC.Error (realSrcSpanToRange)
 import           Development.IDE.GHC.ExactPrint
-import           Development.IDE.Spans.LocalBindings (getDefiningBindings)
-import           Development.Shake (Action)
+import           Development.IDE.Spans.LocalBindings (Bindings, getDefiningBindings)
+import           Development.Shake (RuleResult, Action)
 import qualified FastString
 import           Ide.Plugin.Tactic.CaseSplit
 import           Ide.Plugin.Tactic.Context
@@ -58,6 +60,7 @@ import           Prelude hiding (span)
 import           SrcLoc (containsSpan)
 import           System.Timeout
 import           TcRnTypes (tcg_binds)
+import Development.Shake.Classes
 
 
 descriptor :: PluginId -> PluginDescriptor IdeState
@@ -86,6 +89,18 @@ tcCommandName = T.pack . show
 runIde :: IdeState -> Action a -> IO a
 runIde state = runAction "tactic" state
 
+runStaleIde
+    :: forall a r
+     . ( r ~ RuleResult a
+       , Eq a , Hashable a , Binary a , Show a , Typeable a , NFData a
+       , Show r, Typeable r, NFData r
+       )
+    => IdeState
+    -> NormalizedFilePath
+    -> a
+    -> MaybeT IO (r, PositionMapping)
+runStaleIde state nfp a = MaybeT $ runIde state $ useWithStale a nfp
+
 
 codeActionProvider :: PluginMethodHandler IdeState TextDocumentCodeAction
 codeActionProvider state plId (CodeActionParams _ _ (TextDocumentIdentifier uri) range _ctx)
@@ -114,29 +129,54 @@ judgementForHole
     -> Range
     -> MaybeT IO (Range, Judgement, Context, DynFlags)
 judgementForHole state nfp range = do
-  (asts, amapping) <- MaybeT $ runIde state $ useWithStale GetHieAst nfp
-  range' <- liftMaybe $ fromCurrentRange amapping range
+  (asts, amapping) <- runStaleIde state nfp GetHieAst
+  case asts of
+    HAR _ _  _ _ (HieFromDisk _) -> fail "Need a fresh hie file"
+    HAR _ hf _ _ HieFresh -> do
+      (binds, _) <- runStaleIde state nfp GetBindings
+      (tcmod, _) <- runStaleIde state nfp TypeCheck
+      (rss, g)   <- liftMaybe $ getSpanAndTypeAtHole amapping range hf
+      resulting_range <- liftMaybe $ toCurrentRange amapping $ realSrcSpanToRange rss
+      let (jdg, ctx) = mkJudgementAndContext g binds rss tcmod
+      dflags <- getIdeDynflags state nfp
+      pure (resulting_range, jdg, ctx, dflags)
 
-  (binds, _) <- MaybeT $ runIde state $ useWithStale GetBindings nfp
 
+getIdeDynflags
+    :: IdeState
+    -> NormalizedFilePath
+    -> MaybeT IO DynFlags
+getIdeDynflags state nfp = do
   -- Ok to use the stale 'ModIface', since all we need is its 'DynFlags'
   -- which don't change very often.
-  ((modsum,_), _) <- MaybeT $ runIde state $ useWithStale GetModSummaryWithoutTimestamps nfp
-  let dflags = ms_hspp_opts modsum
+  ((modsum,_), _) <- runStaleIde state nfp GetModSummaryWithoutTimestamps
+  pure $ ms_hspp_opts modsum
 
-  case asts of
-    (HAR _ hf _ _ kind) -> do
-      (rss, g) <- liftMaybe $ 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
-              let info = nodeInfo ast'
-              ty <- listToMaybe $ nodeType info
-              guard $ ("HsUnboundVar","HsExpr") `S.member` nodeAnnotations info
-              pure (nodeSpan ast', ty)
 
-      resulting_range <- liftMaybe $ toCurrentRange amapping $ realSrcSpanToRange rss
-      (tcmod, _) <- MaybeT $ runIde state $ useWithStale TypeCheck nfp
+getSpanAndTypeAtHole
+    :: PositionMapping
+    -> Range
+    -> HieASTs b
+    -> Maybe (Span, b)
+getSpanAndTypeAtHole amapping range hf = do
+  range' <- fromCurrentRange amapping range
+  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
+        let info = nodeInfo ast'
+        ty <- listToMaybe $ nodeType info
+        guard $ ("HsUnboundVar","HsExpr") `S.member` nodeAnnotations info
+        pure (nodeSpan ast', ty)
+
+
+mkJudgementAndContext
+    :: Type
+    -> Bindings
+    -> RealSrcSpan
+    -> TcModuleResult
+    -> (Judgement, Context)
+mkJudgementAndContext g binds rss tcmod = do
       let tcg  = tmrTypechecked tcmod
           tcs = tcg_binds tcg
           ctx = mkContext
@@ -147,18 +187,12 @@ judgementForHole state nfp range = do
           local_hy = spliceProvenance top_provs
                    $ hypothesisFromBindings rss binds
           cls_hy = contextMethodHypothesis ctx
-      case kind of
-        HieFromDisk _hf' ->
-          fail "Need a fresh hie file"
-        HieFresh ->
-          pure ( resulting_range
-               , mkFirstJudgement
-                   (local_hy <> cls_hy)
-                   (isRhsHole rss tcs)
-                   g
-               , ctx
-               , dflags
-               )
+       in ( mkFirstJudgement
+              (local_hy <> cls_hy)
+              (isRhsHole rss tcs)
+              g
+          , ctx
+          )
 
 spliceProvenance
     :: Map OccName Provenance
@@ -195,6 +229,7 @@ tacticCmd tac state (TacticParams uri range var_name)
 tacticCmd _ _ _ =
   pure $ Left $ mkErr InvalidRequest "Bad URI"
 
+
 mkErr :: ErrorCode -> T.Text -> ResponseError
 mkErr code err = ResponseError code err Nothing
 
@@ -278,6 +313,7 @@ mergeFunBindMatches _ _ _ = Left "mergeFunBindMatches: called on something that
 noteT :: String -> TransformT (Either String) a
 noteT = lift . Left
 
+
 ------------------------------------------------------------------------------
 -- | Helper function to route 'mergeFunBindMatches' into the right place in an
 -- AST --- correctly dealing with inserting into instance declarations.

From 41ebd2e11b72189b452a8b7e31a57ec1a611f2f4 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Tue, 16 Feb 2021 18:39:03 -0800
Subject: [PATCH 34/38] Pull LSP-specific stuff out of the main module

---
 .../src/Ide/Plugin/Tactic.hs                  | 156 +--------------
 .../src/Ide/Plugin/Tactic/LanguageServer.hs   | 177 ++++++++++++++++++
 2 files changed, 183 insertions(+), 150 deletions(-)
 create mode 100644 plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs

diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
index ef3c2eaba0..1439a5d8a2 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
@@ -14,38 +14,25 @@ module Ide.Plugin.Tactic
   ) where
 
 import           Bag (listToBag, bagToList)
-import           Control.Arrow
 import           Control.Monad
 import           Control.Monad.Trans
 import           Control.Monad.Trans.Maybe
 import           Data.Aeson
 import           Data.Bool (bool)
-import           Data.Coerce
 import           Data.Data (Data)
-import           Data.Functor ((<&>))
 import           Data.Generics.Aliases (mkQ)
 import           Data.Generics.Schemes (everything)
-import           Data.Map (Map)
-import qualified Data.Map as M
 import           Data.Maybe
 import           Data.Monoid
-import qualified Data.Set as S
 import qualified Data.Text as T
 import           Data.Traversable
-import           Development.IDE.Core.PositionMapping
-import           Development.IDE.Core.RuleTypes
-import           Development.IDE.Core.Service (runAction)
-import           Development.IDE.Core.Shake (useWithStale, IdeState (..))
+import           Development.IDE.Core.Shake (IdeState (..))
 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 (RuleResult, Action)
-import qualified FastString
+import           Development.Shake.Classes
 import           Ide.Plugin.Tactic.CaseSplit
-import           Ide.Plugin.Tactic.Context
 import           Ide.Plugin.Tactic.GHC
-import           Ide.Plugin.Tactic.Judgements
+import           Ide.Plugin.Tactic.LanguageServer
 import           Ide.Plugin.Tactic.LanguageServer.TacticProviders
 import           Ide.Plugin.Tactic.Range
 import           Ide.Plugin.Tactic.Tactics
@@ -53,14 +40,11 @@ import           Ide.Plugin.Tactic.TestTypes
 import           Ide.Plugin.Tactic.Types
 import           Ide.Types
 import           Language.LSP.Server
-import           Language.LSP.Types.Capabilities
 import           Language.LSP.Types
+import           Language.LSP.Types.Capabilities
 import           OccName
 import           Prelude hiding (span)
-import           SrcLoc (containsSpan)
 import           System.Timeout
-import           TcRnTypes (tcg_binds)
-import Development.Shake.Classes
 
 
 descriptor :: PluginId -> PluginDescriptor IdeState
@@ -86,20 +70,6 @@ tcCommandName :: TacticCommand -> T.Text
 tcCommandName = T.pack . show
 
 
-runIde :: IdeState -> Action a -> IO a
-runIde state = runAction "tactic" state
-
-runStaleIde
-    :: forall a r
-     . ( r ~ RuleResult a
-       , Eq a , Hashable a , Binary a , Show a , Typeable a , NFData a
-       , Show r, Typeable r, NFData r
-       )
-    => IdeState
-    -> NormalizedFilePath
-    -> a
-    -> MaybeT IO (r, PositionMapping)
-runStaleIde state nfp a = MaybeT $ runIde state $ useWithStale a nfp
 
 
 codeActionProvider :: PluginMethodHandler IdeState TextDocumentCodeAction
@@ -119,90 +89,6 @@ codeActionProvider state plId (CodeActionParams _ _ (TextDocumentIdentifier uri)
 codeActionProvider _ _ _ = pure $ Right $ List []
 
 
-
-------------------------------------------------------------------------------
--- | Find the last typechecked module, and find the most specific span, as well
--- as the judgement at the given range.
-judgementForHole
-    :: IdeState
-    -> NormalizedFilePath
-    -> Range
-    -> MaybeT IO (Range, Judgement, Context, DynFlags)
-judgementForHole state nfp range = do
-  (asts, amapping) <- runStaleIde state nfp GetHieAst
-  case asts of
-    HAR _ _  _ _ (HieFromDisk _) -> fail "Need a fresh hie file"
-    HAR _ hf _ _ HieFresh -> do
-      (binds, _) <- runStaleIde state nfp GetBindings
-      (tcmod, _) <- runStaleIde state nfp TypeCheck
-      (rss, g)   <- liftMaybe $ getSpanAndTypeAtHole amapping range hf
-      resulting_range <- liftMaybe $ toCurrentRange amapping $ realSrcSpanToRange rss
-      let (jdg, ctx) = mkJudgementAndContext g binds rss tcmod
-      dflags <- getIdeDynflags state nfp
-      pure (resulting_range, jdg, ctx, dflags)
-
-
-getIdeDynflags
-    :: IdeState
-    -> NormalizedFilePath
-    -> MaybeT IO DynFlags
-getIdeDynflags state nfp = do
-  -- Ok to use the stale 'ModIface', since all we need is its 'DynFlags'
-  -- which don't change very often.
-  ((modsum,_), _) <- runStaleIde state nfp GetModSummaryWithoutTimestamps
-  pure $ ms_hspp_opts modsum
-
-
-getSpanAndTypeAtHole
-    :: PositionMapping
-    -> Range
-    -> HieASTs b
-    -> Maybe (Span, b)
-getSpanAndTypeAtHole amapping range hf = do
-  range' <- fromCurrentRange amapping range
-  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
-        let info = nodeInfo ast'
-        ty <- listToMaybe $ nodeType info
-        guard $ ("HsUnboundVar","HsExpr") `S.member` nodeAnnotations info
-        pure (nodeSpan ast', ty)
-
-
-mkJudgementAndContext
-    :: Type
-    -> Bindings
-    -> RealSrcSpan
-    -> TcModuleResult
-    -> (Judgement, Context)
-mkJudgementAndContext g binds rss tcmod = do
-      let tcg  = tmrTypechecked tcmod
-          tcs = tcg_binds tcg
-          ctx = mkContext
-                  (mapMaybe (sequenceA . (occName *** coerce))
-                    $ getDefiningBindings binds rss)
-                  tcg
-          top_provs = getRhsPosVals rss tcs
-          local_hy = spliceProvenance top_provs
-                   $ hypothesisFromBindings rss binds
-          cls_hy = contextMethodHypothesis ctx
-       in ( mkFirstJudgement
-              (local_hy <> cls_hy)
-              (isRhsHole rss tcs)
-              g
-          , ctx
-          )
-
-spliceProvenance
-    :: Map OccName Provenance
-    -> Hypothesis a
-    -> Hypothesis a
-spliceProvenance provs x =
-  Hypothesis $ flip fmap (unHypothesis x) $ \hi ->
-    overProvenance (maybe id const $ M.lookup (hi_name hi) provs) hi
-
-
 tacticCmd :: (OccName -> TacticsM ()) -> CommandFunction IdeState TacticParams
 tacticCmd tac state (TacticParams uri range var_name)
   | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do
@@ -355,46 +241,16 @@ fromMaybeT :: Functor m => a -> MaybeT m a -> m a
 fromMaybeT def = fmap (fromMaybe def) . runMaybeT
 
 
-liftMaybe :: Monad m => Maybe a -> MaybeT m a
-liftMaybe a = MaybeT $ pure a
 
 
-------------------------------------------------------------------------------
--- | Is this hole immediately to the right of an equals sign?
-isRhsHole :: RealSrcSpan -> TypecheckedSource -> Bool
-isRhsHole rss tcs = everything (||) (mkQ False $ \case
-  TopLevelRHS _ _ (L (RealSrcSpan span) _) -> containsSpan rss span
-  _ -> False
-  ) tcs
-
-
-------------------------------------------------------------------------------
--- | Compute top-level position vals of a function
-getRhsPosVals :: RealSrcSpan -> TypecheckedSource -> Map OccName Provenance
-getRhsPosVals rss tcs
-  = M.fromList
-  $ join
-  $ maybeToList
-  $ getFirst
-  $ everything (<>) (mkQ mempty $ \case
-      TopLevelRHS name ps
-          (L (RealSrcSpan span)  -- body with no guards and a single defn
-            (HsVar _ (L _ hole)))
-        | containsSpan rss span  -- which contains our span
-        , isHole $ occName hole  -- and the span is a hole
-        -> First $ do
-            patnames <- traverse getPatName ps
-            pure $ zip patnames $ [0..] <&> TopLevelArgPrv name
-      _ -> mempty
-  ) tcs
-
 
 locateBiggest :: (Data r, Data a) => SrcSpan -> a -> Maybe r
 locateBiggest ss x = getFirst $ everything (<>)
   ( mkQ mempty $ \case
     L span r | ss `isSubspanOf` span -> pure r
     _ -> mempty
-  )x
+  ) x
+
 
 locateFirst :: (Data r, Data a) => a -> Maybe r
 locateFirst x = getFirst $ everything (<>)
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs
new file mode 100644
index 0000000000..18a0789d3a
--- /dev/null
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs
@@ -0,0 +1,177 @@
+{-# LANGUAGE GADTs               #-}
+{-# LANGUAGE LambdaCase          #-}
+{-# LANGUAGE OverloadedStrings   #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module Ide.Plugin.Tactic.LanguageServer where
+
+import           Control.Arrow
+import           Control.Monad
+import           Control.Monad.Trans.Maybe
+import           Data.Coerce
+import           Data.Functor ((<&>))
+import           Data.Generics.Aliases (mkQ)
+import           Data.Generics.Schemes (everything)
+import           Data.Map (Map)
+import qualified Data.Map as M
+import           Data.Maybe
+import           Data.Monoid
+import qualified Data.Set as S
+import           Data.Traversable
+import           Development.IDE.Core.PositionMapping
+import           Development.IDE.Core.RuleTypes
+import           Development.IDE.Core.Service (runAction)
+import           Development.IDE.Core.Shake (useWithStale, IdeState (..))
+import           Development.IDE.GHC.Compat
+import           Development.IDE.GHC.Error (realSrcSpanToRange)
+import           Development.IDE.Spans.LocalBindings (Bindings, getDefiningBindings)
+import           Development.Shake (RuleResult, Action)
+import           Development.Shake.Classes
+import qualified FastString
+import           Ide.Plugin.Tactic.Context
+import           Ide.Plugin.Tactic.GHC
+import           Ide.Plugin.Tactic.Judgements
+import           Ide.Plugin.Tactic.Range
+import           Ide.Plugin.Tactic.Types
+import           Language.LSP.Types
+import           OccName
+import           Prelude hiding (span)
+import           SrcLoc (containsSpan)
+import           TcRnTypes (tcg_binds)
+
+
+runIde :: IdeState -> Action a -> IO a
+runIde state = runAction "tactic" state
+
+
+runStaleIde
+    :: forall a r
+     . ( r ~ RuleResult a
+       , Eq a , Hashable a , Binary a , Show a , Typeable a , NFData a
+       , Show r, Typeable r, NFData r
+       )
+    => IdeState
+    -> NormalizedFilePath
+    -> a
+    -> MaybeT IO (r, PositionMapping)
+runStaleIde state nfp a = MaybeT $ runIde state $ useWithStale a nfp
+
+
+getIdeDynflags
+    :: IdeState
+    -> NormalizedFilePath
+    -> MaybeT IO DynFlags
+getIdeDynflags state nfp = do
+  -- Ok to use the stale 'ModIface', since all we need is its 'DynFlags'
+  -- which don't change very often.
+  ((modsum,_), _) <- runStaleIde state nfp GetModSummaryWithoutTimestamps
+  pure $ ms_hspp_opts modsum
+
+
+------------------------------------------------------------------------------
+-- | Find the last typechecked module, and find the most specific span, as well
+-- as the judgement at the given range.
+judgementForHole
+    :: IdeState
+    -> NormalizedFilePath
+    -> Range
+    -> MaybeT IO (Range, Judgement, Context, DynFlags)
+judgementForHole state nfp range = do
+  (asts, amapping) <- runStaleIde state nfp GetHieAst
+  case asts of
+    HAR _ _  _ _ (HieFromDisk _) -> fail "Need a fresh hie file"
+    HAR _ hf _ _ HieFresh -> do
+      (binds, _) <- runStaleIde state nfp GetBindings
+      (tcmod, _) <- runStaleIde state nfp TypeCheck
+      (rss, g)   <- liftMaybe $ getSpanAndTypeAtHole amapping range hf
+      resulting_range <- liftMaybe $ toCurrentRange amapping $ realSrcSpanToRange rss
+      let (jdg, ctx) = mkJudgementAndContext g binds rss tcmod
+      dflags <- getIdeDynflags state nfp
+      pure (resulting_range, jdg, ctx, dflags)
+
+
+mkJudgementAndContext
+    :: Type
+    -> Bindings
+    -> RealSrcSpan
+    -> TcModuleResult
+    -> (Judgement, Context)
+mkJudgementAndContext g binds rss tcmod = do
+      let tcg  = tmrTypechecked tcmod
+          tcs = tcg_binds tcg
+          ctx = mkContext
+                  (mapMaybe (sequenceA . (occName *** coerce))
+                    $ getDefiningBindings binds rss)
+                  tcg
+          top_provs = getRhsPosVals rss tcs
+          local_hy = spliceProvenance top_provs
+                   $ hypothesisFromBindings rss binds
+          cls_hy = contextMethodHypothesis ctx
+       in ( mkFirstJudgement
+              (local_hy <> cls_hy)
+              (isRhsHole rss tcs)
+              g
+          , ctx
+          )
+
+
+getSpanAndTypeAtHole
+    :: PositionMapping
+    -> Range
+    -> HieASTs b
+    -> Maybe (Span, b)
+getSpanAndTypeAtHole amapping range hf = do
+  range' <- fromCurrentRange amapping range
+  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
+        let info = nodeInfo ast'
+        ty <- listToMaybe $ nodeType info
+        guard $ ("HsUnboundVar","HsExpr") `S.member` nodeAnnotations info
+        pure (nodeSpan ast', ty)
+
+
+
+liftMaybe :: Monad m => Maybe a -> MaybeT m a
+liftMaybe a = MaybeT $ pure a
+
+
+spliceProvenance
+    :: Map OccName Provenance
+    -> Hypothesis a
+    -> Hypothesis a
+spliceProvenance provs x =
+  Hypothesis $ flip fmap (unHypothesis x) $ \hi ->
+    overProvenance (maybe id const $ M.lookup (hi_name hi) provs) hi
+
+
+------------------------------------------------------------------------------
+-- | Compute top-level position vals of a function
+getRhsPosVals :: RealSrcSpan -> TypecheckedSource -> Map OccName Provenance
+getRhsPosVals rss tcs
+  = M.fromList
+  $ join
+  $ maybeToList
+  $ getFirst
+  $ everything (<>) (mkQ mempty $ \case
+      TopLevelRHS name ps
+          (L (RealSrcSpan span)  -- body with no guards and a single defn
+            (HsVar _ (L _ hole)))
+        | containsSpan rss span  -- which contains our span
+        , isHole $ occName hole  -- and the span is a hole
+        -> First $ do
+            patnames <- traverse getPatName ps
+            pure $ zip patnames $ [0..] <&> TopLevelArgPrv name
+      _ -> mempty
+  ) tcs
+
+
+------------------------------------------------------------------------------
+-- | Is this hole immediately to the right of an equals sign?
+isRhsHole :: RealSrcSpan -> TypecheckedSource -> Bool
+isRhsHole rss tcs = everything (||) (mkQ False $ \case
+  TopLevelRHS _ _ (L (RealSrcSpan span) _) -> containsSpan rss span
+  _ -> False
+  ) tcs
+

From 0563434daf07a09bf267796fd2ac5281bfa1c0a0 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Tue, 16 Feb 2021 18:48:10 -0800
Subject: [PATCH 35/38] Clean up tacticCmd

---
 .../src/Ide/Plugin/Tactic.hs                  | 33 +++++++++++--------
 .../src/Ide/Plugin/Tactic/LanguageServer.hs   |  1 -
 2 files changed, 20 insertions(+), 14 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
index 1439a5d8a2..eaec6739be 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
@@ -45,6 +45,8 @@ import           Language.LSP.Types.Capabilities
 import           OccName
 import           Prelude hiding (span)
 import           System.Timeout
+import Control.Exception (evaluate)
+import Data.Bifunctor (Bifunctor(bimap))
 
 
 descriptor :: PluginId -> PluginDescriptor IdeState
@@ -59,11 +61,11 @@ descriptor plId = (defaultPluginDescriptor plId)
     , pluginHandlers = mkPluginHandler STextDocumentCodeAction codeActionProvider
     }
 
+
 tacticDesc :: T.Text -> T.Text
 tacticDesc name = "fill the hole using the " <> name <> " tactic"
 
 
-
 ------------------------------------------------------------------------------
 -- | The name of the command for the LS.
 tcCommandName :: TacticCommand -> T.Text
@@ -71,7 +73,6 @@ tcCommandName = T.pack . show
 
 
 
-
 codeActionProvider :: PluginMethodHandler IdeState TextDocumentCodeAction
 codeActionProvider state plId (CodeActionParams _ _ (TextDocumentIdentifier uri) range _ctx)
   | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri =
@@ -98,24 +99,30 @@ tacticCmd tac state (TacticParams uri range var_name)
         let span = rangeToRealSrcSpan (fromNormalizedFilePath nfp) range'
         pm <- MaybeT $ useAnnotatedSource "tacticsCmd" state nfp
 
-        x <- lift $ timeout 2e8 $ pure $
-          case runTactic ctx jdg $ tac $ mkVarOcc $ T.unpack var_name of
-            Left err ->
-              Left $ mkErr InvalidRequest $ T.pack $ show err
-            Right rtr ->
-              mkWorkspaceEdits rtr span dflags clientCapabilities uri pm
-        pure $ joinNote (mkErr InvalidRequest "timed out") x
+        timingOut 2e8 $ join $
+          bimap (mkErr InvalidRequest . T.pack . show)
+                (mkWorkspaceEdits span dflags clientCapabilities uri pm)
+            $ runTactic ctx jdg $ tac $ mkVarOcc $ T.unpack var_name
 
       case res of
         Left err -> pure $ Left err
         Right medit -> do
           forM_ medit $ \edit ->
-            sendRequest SWorkspaceApplyEdit (ApplyWorkspaceEditParams Nothing edit) (\_ -> pure ())
+            sendRequest
+              SWorkspaceApplyEdit
+              (ApplyWorkspaceEditParams Nothing edit)
+              (const $ pure ())
           pure $ Right Null
 tacticCmd _ _ _ =
   pure $ Left $ mkErr InvalidRequest "Bad URI"
 
 
+timingOut :: Int -> (Either ResponseError a) -> MaybeT IO (Either ResponseError a)
+timingOut t m = do
+  x <- lift $ timeout t $ evaluate m
+  pure $ joinNote (mkErr InvalidRequest "timed out") x
+
+
 mkErr :: ErrorCode -> T.Text -> ResponseError
 mkErr code err = ResponseError code err Nothing
 
@@ -129,14 +136,14 @@ joinNote _ (Just a) = a
 -- | Turn a 'RunTacticResults' into concrete edits to make in the source
 -- document.
 mkWorkspaceEdits
-    :: RunTacticResults
-    -> RealSrcSpan
+    :: RealSrcSpan
     -> DynFlags
     -> ClientCapabilities
     -> Uri
     -> Annotated ParsedSource
+    -> RunTacticResults
     -> Either ResponseError (Maybe WorkspaceEdit)
-mkWorkspaceEdits rtr span dflags clientCapabilities uri pm = do
+mkWorkspaceEdits span dflags clientCapabilities uri pm rtr = do
   let g = graftHole (RealSrcSpan span) rtr
       response = transform dflags clientCapabilities uri g pm
    in case response of
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs
index 18a0789d3a..948574be7d 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs
@@ -132,7 +132,6 @@ getSpanAndTypeAtHole amapping range hf = do
         pure (nodeSpan ast', ty)
 
 
-
 liftMaybe :: Monad m => Maybe a -> MaybeT m a
 liftMaybe a = MaybeT $ pure a
 

From c1ded82e3eb560e550f0343d4d4d0214b8e9a89d Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 17 Feb 2021 11:30:37 -0800
Subject: [PATCH 36/38] Minor renaming

---
 .../hls-tactics-plugin/src/Ide/Plugin/Tactic.hs  | 16 ++++++----------
 1 file changed, 6 insertions(+), 10 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
index eaec6739be..9abf06443a 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
@@ -14,10 +14,12 @@ module Ide.Plugin.Tactic
   ) where
 
 import           Bag (listToBag, bagToList)
+import           Control.Exception (evaluate)
 import           Control.Monad
 import           Control.Monad.Trans
 import           Control.Monad.Trans.Maybe
 import           Data.Aeson
+import           Data.Bifunctor (Bifunctor(bimap))
 import           Data.Bool (bool)
 import           Data.Data (Data)
 import           Data.Generics.Aliases (mkQ)
@@ -45,8 +47,6 @@ import           Language.LSP.Types.Capabilities
 import           OccName
 import           Prelude hiding (span)
 import           System.Timeout
-import Control.Exception (evaluate)
-import Data.Bifunctor (Bifunctor(bimap))
 
 
 descriptor :: PluginId -> PluginDescriptor IdeState
@@ -93,7 +93,7 @@ codeActionProvider _ _ _ = pure $ Right $ List []
 tacticCmd :: (OccName -> TacticsM ()) -> CommandFunction IdeState TacticParams
 tacticCmd tac state (TacticParams uri range var_name)
   | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do
-      clientCapabilities <- getClientCapabilities
+      ccs <- getClientCapabilities
       res <- liftIO $ fromMaybeT (Right Nothing) $ do
         (range', jdg, ctx, dflags) <- judgementForHole state nfp range
         let span = rangeToRealSrcSpan (fromNormalizedFilePath nfp) range'
@@ -101,7 +101,7 @@ tacticCmd tac state (TacticParams uri range var_name)
 
         timingOut 2e8 $ join $
           bimap (mkErr InvalidRequest . T.pack . show)
-                (mkWorkspaceEdits span dflags clientCapabilities uri pm)
+                (mkWorkspaceEdits span dflags ccs uri pm)
             $ runTactic ctx jdg $ tac $ mkVarOcc $ T.unpack var_name
 
       case res of
@@ -143,9 +143,9 @@ mkWorkspaceEdits
     -> Annotated ParsedSource
     -> RunTacticResults
     -> Either ResponseError (Maybe WorkspaceEdit)
-mkWorkspaceEdits span dflags clientCapabilities uri pm rtr = do
+mkWorkspaceEdits span dflags ccs uri pm rtr = do
   let g = graftHole (RealSrcSpan span) rtr
-      response = transform dflags clientCapabilities uri g pm
+      response = transform dflags ccs uri g pm
    in case response of
         Right res -> Right $ Just res
         Left err -> Left $ mkErr InternalError $ T.pack err
@@ -243,14 +243,10 @@ graftDecl span _ x = do
   noteT "graftDecl: don't know about this AST form"
 
 
-
 fromMaybeT :: Functor m => a -> MaybeT m a -> m a
 fromMaybeT def = fmap (fromMaybe def) . runMaybeT
 
 
-
-
-
 locateBiggest :: (Data r, Data a) => SrcSpan -> a -> Maybe r
 locateBiggest ss x = getFirst $ everything (<>)
   ( mkQ mempty $ \case

From 67badc847be26a4fcfc0f1bc8f1efe9caa9d3ad9 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 17 Feb 2021 11:39:12 -0800
Subject: [PATCH 37/38] Rename noteT to throwError; minor haddock

---
 .../hls-tactics-plugin/src/Ide/Plugin/Tactic.hs   | 15 +++++++++------
 1 file changed, 9 insertions(+), 6 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
index 9abf06443a..8207960cf8 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
@@ -117,7 +117,10 @@ tacticCmd _ _ _ =
   pure $ Left $ mkErr InvalidRequest "Bad URI"
 
 
-timingOut :: Int -> (Either ResponseError a) -> MaybeT IO (Either ResponseError a)
+timingOut
+    :: Int                     -- ^ Time in microseconds
+    -> Either ResponseError a  -- ^ Computation to run
+    -> MaybeT IO (Either ResponseError a)
 timingOut t m = do
   x <- lift $ timeout t $ evaluate m
   pure $ joinNote (mkErr InvalidRequest "timed out") x
@@ -203,8 +206,8 @@ mergeFunBindMatches make_decl span (fb@FunBind {fun_matches = mg@MG {mg_alts = L
 mergeFunBindMatches _ _ _ = Left "mergeFunBindMatches: called on something that isnt a funbind"
 
 
-noteT :: String -> TransformT (Either String) a
-noteT = lift . Left
+throwError :: String -> TransformT (Either String) a
+throwError = lift . Left
 
 
 ------------------------------------------------------------------------------
@@ -218,7 +221,7 @@ graftDecl
 graftDecl span
     make_decl
     (L src (ValD ext fb))
-  = either noteT (pure . Just . pure . L src . ValD ext) $
+  = either throwError (pure . Just . pure . L src . ValD ext) $
       mergeFunBindMatches make_decl span fb
 -- TODO(sandy): add another case for default methods in class definitions
 graftDecl span
@@ -229,7 +232,7 @@ graftDecl span
         for (bagToList binds) $ \b@(L bsrc bind) -> do
           case bind of
             fb@FunBind{}
-              | span `isSubspanOf` bsrc -> either noteT (pure . L bsrc) $ mergeFunBindMatches make_decl span fb
+              | span `isSubspanOf` bsrc -> either throwError (pure . L bsrc) $ mergeFunBindMatches make_decl span fb
             _ -> pure b
 
       pure $ Just $ pure $ L src $ InstD ext $ cid
@@ -240,7 +243,7 @@ graftDecl span
 graftDecl span _ x = do
   traceMX "biggest" $ unsafeRender $ locateBiggest @(Match GhcPs (LHsExpr GhcPs)) span x
   traceMX "first" $ unsafeRender $ locateFirst @(Match GhcPs (LHsExpr GhcPs)) x
-  noteT "graftDecl: don't know about this AST form"
+  throwError "graftDecl: don't know about this AST form"
 
 
 fromMaybeT :: Functor m => a -> MaybeT m a -> m a

From ae0830d41acd6d1b55e0eb4cd55a22c4c5070362 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 17 Feb 2021 11:45:36 -0800
Subject: [PATCH 38/38] Move a few more things into the LanguageServer

---
 .../src/Ide/Plugin/Tactic.hs                  | 61 +++++++++----------
 .../src/Ide/Plugin/Tactic/LanguageServer.hs   | 12 ++++
 2 files changed, 42 insertions(+), 31 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
index 8207960cf8..e17d3c727e 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
@@ -58,20 +58,11 @@ descriptor plId = (defaultPluginDescriptor plId)
               (tacticDesc $ tcCommandName tc)
               (tacticCmd $ commandTactic tc))
               [minBound .. maxBound]
-    , pluginHandlers = mkPluginHandler STextDocumentCodeAction codeActionProvider
+    , pluginHandlers =
+        mkPluginHandler STextDocumentCodeAction codeActionProvider
     }
 
 
-tacticDesc :: T.Text -> T.Text
-tacticDesc name = "fill the hole using the " <> name <> " tactic"
-
-
-------------------------------------------------------------------------------
--- | The name of the command for the LS.
-tcCommandName :: TacticCommand -> T.Text
-tcCommandName = T.pack . show
-
-
 
 codeActionProvider :: PluginMethodHandler IdeState TextDocumentCodeAction
 codeActionProvider state plId (CodeActionParams _ _ (TextDocumentIdentifier uri) range _ctx)
@@ -188,22 +179,23 @@ mergeFunBindMatches
     -> SrcSpan
     -> HsBind GhcPs
     -> Either String (HsBind GhcPs)
-mergeFunBindMatches make_decl span (fb@FunBind {fun_matches = mg@MG {mg_alts = L alts_src alts}}) =
-  pure $
-    fb
-      { fun_matches = mg
-        { mg_alts = L alts_src $ do
-            alt@(L alt_src match) <- alts
-            case span `isSubspanOf` alt_src of
-              True -> do
-                let pats = fmap fromPatCompatPs $ m_pats match
-                    (L _ (ValD _ (FunBind {fun_matches = MG {mg_alts = L _ to_add}}))) =
-                        make_decl pats
-                to_add
-              False -> pure alt
-        }
+mergeFunBindMatches make_decl span
+    (fb@FunBind {fun_matches = mg@MG {mg_alts = L alts_src alts}}) =
+  pure $ fb
+    { fun_matches = mg
+      { mg_alts = L alts_src $ do
+          alt@(L alt_src match) <- alts
+          case span `isSubspanOf` alt_src of
+            True -> do
+              let pats = fmap fromPatCompatPs $ m_pats match
+                  L _ (ValD _ (FunBind {fun_matches = MG
+                        {mg_alts = L _ to_add}})) = make_decl pats
+              to_add
+            False -> pure alt
       }
-mergeFunBindMatches _ _ _ = Left "mergeFunBindMatches: called on something that isnt a funbind"
+    }
+mergeFunBindMatches _ _ _ =
+  Left "mergeFunBindMatches: called on something that isnt a funbind"
 
 
 throwError :: String -> TransformT (Either String) a
@@ -226,13 +218,16 @@ graftDecl span
 -- TODO(sandy): add another case for default methods in class definitions
 graftDecl span
     make_decl
-    (L src (InstD ext cid@ClsInstD{cid_inst = cidi@ClsInstDecl{cid_sigs = _sigs, cid_binds = binds}}))
+    (L src (InstD ext
+      cid@ClsInstD{cid_inst =
+        cidi@ClsInstDecl{cid_sigs = _sigs, cid_binds = binds}}))
   = do
       binds' <-
         for (bagToList binds) $ \b@(L bsrc bind) -> do
           case bind of
-            fb@FunBind{}
-              | span `isSubspanOf` bsrc -> either throwError (pure . L bsrc) $ mergeFunBindMatches make_decl span fb
+            fb@FunBind{} | span `isSubspanOf` bsrc ->
+              either throwError (pure . L bsrc) $
+                mergeFunBindMatches make_decl span fb
             _ -> pure b
 
       pure $ Just $ pure $ L src $ InstD ext $ cid
@@ -241,8 +236,12 @@ graftDecl span
           }
         }
 graftDecl span _ x = do
-  traceMX "biggest" $ unsafeRender $ locateBiggest @(Match GhcPs (LHsExpr GhcPs)) span x
-  traceMX "first" $ unsafeRender $ locateFirst @(Match GhcPs (LHsExpr GhcPs)) x
+  traceMX "biggest" $
+    unsafeRender $
+      locateBiggest @(Match GhcPs (LHsExpr GhcPs)) span x
+  traceMX "first" $
+    unsafeRender $
+      locateFirst @(Match GhcPs (LHsExpr GhcPs)) x
   throwError "graftDecl: don't know about this AST form"
 
 
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs
index 948574be7d..d130410091 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs
@@ -17,6 +17,7 @@ import qualified Data.Map as M
 import           Data.Maybe
 import           Data.Monoid
 import qualified Data.Set as S
+import qualified Data.Text as T
 import           Data.Traversable
 import           Development.IDE.Core.PositionMapping
 import           Development.IDE.Core.RuleTypes
@@ -32,6 +33,7 @@ import           Ide.Plugin.Tactic.Context
 import           Ide.Plugin.Tactic.GHC
 import           Ide.Plugin.Tactic.Judgements
 import           Ide.Plugin.Tactic.Range
+import           Ide.Plugin.Tactic.TestTypes (TacticCommand)
 import           Ide.Plugin.Tactic.Types
 import           Language.LSP.Types
 import           OccName
@@ -40,6 +42,16 @@ import           SrcLoc (containsSpan)
 import           TcRnTypes (tcg_binds)
 
 
+tacticDesc :: T.Text -> T.Text
+tacticDesc name = "fill the hole using the " <> name <> " tactic"
+
+
+------------------------------------------------------------------------------
+-- | The name of the command for the LS.
+tcCommandName :: TacticCommand -> T.Text
+tcCommandName = T.pack . show
+
+
 runIde :: IdeState -> Action a -> IO a
 runIde state = runAction "tactic" state