From 2cc54a4093961be1a886fbc7c6e39166fe679739 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Sun, 25 Apr 2021 20:15:57 -0700
Subject: [PATCH 01/52] Metaprogramming parser

---
 .../hls-tactics-plugin.cabal                  |  4 +
 .../Wingman/LanguageServer/TacticProviders.hs |  1 +
 .../src/Wingman/Metaprogramming/Lexer.hs      | 72 ++++++++++++++++
 .../src/Wingman/Metaprogramming/Parser.hs     | 84 +++++++++++++++++++
 4 files changed, 161 insertions(+)
 create mode 100644 plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Lexer.hs
 create mode 100644 plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs

diff --git a/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal b/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal
index 81553f0ab9..1e1f563cbd 100644
--- a/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal
+++ b/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal
@@ -45,6 +45,8 @@ library
     Wingman.LanguageServer
     Wingman.LanguageServer.TacticProviders
     Wingman.Machinery
+    Wingman.Metaprogramming.Lexer
+    Wingman.Metaprogramming.Parser
     Wingman.Naming
     Wingman.Plugin
     Wingman.Range
@@ -86,6 +88,8 @@ library
     , transformers
     , unordered-containers
     , hyphenation
+    , megaparsec ^>=9
+    , parser-combinators
 
   default-language:   Haskell2010
   default-extensions:
diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs
index 1c205d8bab..71ed57d560 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs
@@ -7,6 +7,7 @@ module Wingman.LanguageServer.TacticProviders
   , tcCommandId
   , TacticParams (..)
   , TacticProviderData (..)
+  , useNameFromHypothesis
   ) where
 
 import           Control.Monad
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Lexer.hs b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Lexer.hs
new file mode 100644
index 0000000000..7e0d089115
--- /dev/null
+++ b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Lexer.hs
@@ -0,0 +1,72 @@
+{-# LANGUAGE DataKinds         #-}
+{-# LANGUAGE LambdaCase        #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE TypeApplications  #-}
+
+module Wingman.Metaprogramming.Lexer where
+
+import           Control.Applicative
+import           Control.Monad
+import           Data.Functor
+import           Data.Text (Text)
+import qualified Data.Text as T
+import           Data.Void
+import           Name
+import qualified Text.Megaparsec as P
+import qualified Text.Megaparsec.Char as P
+import qualified Text.Megaparsec.Char.Lexer as L
+import           Wingman.Types
+
+
+type Parser = P.Parsec Void Text
+
+lineComment :: Parser ()
+lineComment = L.skipLineComment "--"
+
+blockComment :: Parser ()
+blockComment = L.skipBlockComment "{-" "-}"
+
+sc :: Parser ()
+sc = L.space P.space1 lineComment blockComment
+
+lexeme :: Parser a -> Parser a
+lexeme = L.lexeme sc
+
+symbol :: Text -> Parser Text
+symbol = L.symbol sc
+
+symbol_ :: Text -> Parser ()
+symbol_ = void . symbol
+
+brackets :: Parser a -> Parser a
+brackets = P.between (symbol "[") (symbol "]")
+
+braces :: Parser a -> Parser a
+braces = P.between (symbol "{") (symbol "}")
+
+identifier :: Text -> Parser ()
+identifier i = lexeme (P.string i *> P.notFollowedBy P.alphaNumChar)
+
+-- FIXME [Reed M. 2020-10-18] Check to see if the variables are in the reserved list
+variable :: Parser OccName
+variable = lexeme $ do
+    c <- P.alphaNumChar
+    cs <- P.many (P.alphaNumChar <|> P.char '\'')
+    pure $ mkVarOcc (c:cs)
+
+-- FIXME [Reed M. 2020-10-18] Check to see if the variables are in the reserved list
+name :: Parser Text
+name = lexeme $ do
+    c <- P.alphaNumChar
+    cs <- P.many (P.alphaNumChar <|> P.char '\'' <|> P.char '-')
+    pure $ T.pack (c:cs)
+
+named :: Text -> TacticsM () -> Parser (TacticsM ())
+named name tac = identifier name $> tac
+
+named' :: Text -> (OccName -> TacticsM ()) -> Parser (TacticsM ())
+named' name tac = tac <$> (identifier name *> variable)
+
+keyword :: Text -> Parser ()
+keyword = identifier
+
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
new file mode 100644
index 0000000000..d78f672934
--- /dev/null
+++ b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
@@ -0,0 +1,84 @@
+{-# LANGUAGE DataKinds         #-}
+{-# LANGUAGE LambdaCase        #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE TypeApplications  #-}
+
+module Wingman.Metaprogramming.Parser where
+
+import qualified Control.Monad.Combinators.Expr as P
+import           Data.Function
+import           Data.Functor
+import           Data.List (foldl')
+import           Development.IDE.GHC.Compat (alphaTyVars)
+import           GhcPlugins (mkTyVarTy, mkFunTys, mkListTy, mkVarOcc)
+import qualified Refinery.Tactic as R
+import qualified Text.Megaparsec as P
+import           Wingman.Auto
+import           Wingman.Judgements (mkFirstJudgement)
+import           Wingman.LanguageServer.TacticProviders (useNameFromHypothesis)
+import           Wingman.Metaprogramming.Lexer
+import           Wingman.Tactics
+import           Wingman.Types
+
+
+tactic :: Parser (TacticsM ())
+tactic = flip P.makeExprParser operators $  P.choice
+    [ named  "assumption" assumption
+    , named' "assume" assume
+    , named  "intros" intros
+    -- , named' "intro" intro
+    , named' "destruct" $ useNameFromHypothesis destruct
+    , named' "homo" $ useNameFromHypothesis homo
+    , named' "apply" $ useNameFromHypothesis apply
+    -- , named  "split" $ useNameFromHypothesis split
+    , named  "auto" auto
+    , R.try <$> (keyword "try" *> tactics)
+    ]
+
+multitactic :: Parser (TacticsM () -> TacticsM ())
+multitactic = P.choice
+    [ (flip (R.<@>)) <$> brackets (P.sepBy1 tactic (symbol ";"))
+    , (flip (>>)) <$> tactic
+    ]
+
+operators :: [[P.Operator Parser (TacticsM ())]]
+operators =
+    [ [ P.Prefix (symbol "*" $> R.many_) ]
+    , [ P.InfixR (symbol "|" $> (R.<%>) )]
+    ]
+
+tactics :: Parser (TacticsM ())
+tactics = do
+    t <- tactic
+    ts <- P.many ((symbol ",") *> multitactic)
+    pure $ foldl' (&) t ts
+
+
+skolems :: [Type]
+skolems = fmap mkTyVarTy alphaTyVars
+
+a_skolem, b_skolem, c_skolem :: Type
+(a_skolem : b_skolem : c_skolem : _) = skolems
+
+
+main :: IO ()
+main = do
+  case P.runParser (tactics <* P.eof)
+          "<splice>"
+          "intros, destruct as, [ assumption; auto ]" of
+    Left peb -> putStrLn $ P.errorBundlePretty peb
+    Right tt -> do
+      let ty = mkFunTys
+                [ mkFunTys [a_skolem, b_skolem] b_skolem
+                , b_skolem
+                , mkListTy a_skolem
+                ] b_skolem
+      case runTactic
+             emptyContext { ctxDefiningFuncs = [(mkVarOcc "hello", CType ty)] }
+             (mkFirstJudgement mempty True ty)
+             tt
+        of
+          Left tes -> putStrLn $ "failed: " <> show tes
+          Right rtr -> print $ rtr_extract rtr
+

From 352dbb072f03b5f4e4ad5f00551e2b05d677222b Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Sun, 25 Apr 2021 22:01:31 -0700
Subject: [PATCH 02/52] Enable quasiquotes by default in ghcide

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

diff --git a/ghcide/session-loader/Development/IDE/Session.hs b/ghcide/session-loader/Development/IDE/Session.hs
index 3c776cb36b..3c96369b0a 100644
--- a/ghcide/session-loader/Development/IDE/Session.hs
+++ b/ghcide/session-loader/Development/IDE/Session.hs
@@ -90,7 +90,7 @@ import           HieDb.Create
 import           HieDb.Types
 import           HieDb.Utils
 import           Maybes                               (MaybeT (runMaybeT))
-import           GHC.LanguageExtensions               (Extension(EmptyCase))
+import           GHC.LanguageExtensions               (Extension(EmptyCase, QuasiQuotes))
 
 -- | Bump this version number when making changes to the format of the data stored in hiedb
 hiedbDataVersion :: String
@@ -774,6 +774,7 @@ setOptions (ComponentOptions theOpts compRoot _) dflags = do
           disableOptimisation $
           allowEmptyCaseButWithWarning $
           setUpTypedHoles $
+          enableQuasiQuotes $
           makeDynFlagsAbsolute compRoot dflags'
     -- initPackages parses the -package flags and
     -- sets up the visibility for each component.
@@ -781,6 +782,8 @@ setOptions (ComponentOptions theOpts compRoot _) dflags = do
     (final_df, _) <- liftIO $ wrapPackageSetupException $ initPackages dflags''
     return (final_df, targets)
 
+enableQuasiQuotes :: DynFlags -> DynFlags
+enableQuasiQuotes = flip xopt_set QuasiQuotes
 
 -- | Wingman wants to support destructing of empty cases, but these are a parse
 -- error by default. So we want to enable 'EmptyCase', but then that leads to

From a32d5631037d11d8b3f59f9cf7f1e8c5041d767c Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Sun, 25 Apr 2021 22:01:47 -0700
Subject: [PATCH 03/52] Install the Wingman tactic syntax in ghcide

---
 ghcide/src/Development/IDE/Core/Compile.hs | 41 +++++++++++++++++++++-
 1 file changed, 40 insertions(+), 1 deletion(-)

diff --git a/ghcide/src/Development/IDE/Core/Compile.hs b/ghcide/src/Development/IDE/Core/Compile.hs
index ff8f5f1c0c..311703400f 100644
--- a/ghcide/src/Development/IDE/Core/Compile.hs
+++ b/ghcide/src/Development/IDE/Core/Compile.hs
@@ -4,6 +4,7 @@
 {-# LANGUAGE CPP        #-}
 {-# LANGUAGE GADTs      #-}
 {-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE PatternSynonyms #-}
 #include "ghc-api-version.h"
 
 -- | Based on https://ghc.haskell.org/trac/ghc/wiki/Commentary/Compiler/API.
@@ -31,6 +32,7 @@ module Development.IDE.Core.Compile
   , setupFinderCache
   , getDocsBatch
   , lookupName
+  , pattern WingmanMetaprogram
   ) where
 
 import           Development.IDE.Core.Preprocessor
@@ -122,6 +124,7 @@ import           Data.Unique
 import           GHC.Fingerprint
 import qualified Language.LSP.Server               as LSP
 import qualified Language.LSP.Types                as LSP
+import Generics.SYB hiding (orElse)
 
 -- | Given a string buffer, return the string (after preprocessing) and the 'ParsedModule'.
 parseModule
@@ -208,6 +211,36 @@ captureSplices dflags k = do
             pure $ f aw'
 
 
+wingmanMetaprogrammingPlugin :: StaticPlugin
+wingmanMetaprogrammingPlugin =
+    StaticPlugin $ PluginWithArgs (defaultPlugin { parsedResultAction = worker })  []
+  where
+    worker :: [CommandLineOption] -> ModSummary -> HsParsedModule -> Hsc HsParsedModule
+    worker _ _ pm = pure $ pm { hpm_module = addWingmanMetaprogrammingSyntax $ hpm_module pm }
+
+
+pattern WingmanMetaprogram :: FastString -> HsExpr p
+pattern WingmanMetaprogram mp
+  <- HsSCC _ (SourceText "wingman-meta-program") (StringLiteral NoSourceText mp)
+      (L _ ( HsVar _ _))
+
+mkWingmanMetaprogram :: (XVar p ~ NoExt, XSCC p ~ NoExt, IdP p ~ RdrName) => SrcSpan -> FastString -> HsExpr p
+mkWingmanMetaprogram ss mp =
+  HsSCC noExt (SourceText "wingman-meta-program") (StringLiteral NoSourceText mp)
+    $ L ss
+    $ HsVar noExt
+    $ L ss
+    $ mkRdrUnqual
+    $ mkVarOcc "_"
+
+
+addWingmanMetaprogrammingSyntax :: Data a => a -> a
+addWingmanMetaprogrammingSyntax =
+  everywhere $ mkT $ \case
+    L ss (HsSpliceE _ (HsQuasiQuote _ _ (occNameString . rdrNameOcc -> "wingman") _ mp)) ->
+      L ss $ mkWingmanMetaprogram ss mp
+    (x :: LHsExpr GhcPs) -> x
+
 tcRnModule :: HscEnv -> [Linkable] -> ParsedModule -> IO TcModuleResult
 tcRnModule hsc_env keep_lbls pmod = do
   let ms = pm_mod_summary pmod
@@ -817,7 +850,13 @@ parseFileContents
        -> ExceptT [FileDiagnostic] IO ([FileDiagnostic], ParsedModule)
 parseFileContents env customPreprocessor filename ms = do
    let loc  = mkRealSrcLoc (mkFastString filename) 1 1
-       dflags = ms_hspp_opts ms
+       dflags' = ms_hspp_opts ms
+       dflags =
+         dflags'
+            { staticPlugins =
+                staticPlugins dflags' <> [wingmanMetaprogrammingPlugin]
+            }
+
        contents = fromJust $ ms_hspp_buf ms
    case unP Parser.parseModule (mkPState dflags contents loc) of
 #if MIN_GHC_API_VERSION(8,10,0)

From 643fb8875689d03bb61af4893f9cc96679b08df8 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Sun, 25 Apr 2021 22:02:21 -0700
Subject: [PATCH 04/52] Underscores are allowed in identifiers too

---
 .../hls-tactics-plugin/src/Wingman/Metaprogramming/Lexer.hs   | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Lexer.hs b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Lexer.hs
index 7e0d089115..2fcf32dca5 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Lexer.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Lexer.hs
@@ -51,14 +51,14 @@ identifier i = lexeme (P.string i *> P.notFollowedBy P.alphaNumChar)
 variable :: Parser OccName
 variable = lexeme $ do
     c <- P.alphaNumChar
-    cs <- P.many (P.alphaNumChar <|> P.char '\'')
+    cs <- P.many (P.alphaNumChar <|> P.char '_' <|> P.char '\'')
     pure $ mkVarOcc (c:cs)
 
 -- FIXME [Reed M. 2020-10-18] Check to see if the variables are in the reserved list
 name :: Parser Text
 name = lexeme $ do
     c <- P.alphaNumChar
-    cs <- P.many (P.alphaNumChar <|> P.char '\'' <|> P.char '-')
+    cs <- P.many (P.alphaNumChar <|> P.char '_' <|> P.char '\'' <|> P.char '-')
     pure $ T.pack (c:cs)
 
 named :: Text -> TacticsM () -> Parser (TacticsM ())

From 22a509fa90645e9d9e3a6d85669c991ae6ae8865 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Sun, 25 Apr 2021 22:02:33 -0700
Subject: [PATCH 05/52] Test showing we can expand out tactics

---
 .../src/Wingman/LanguageServer.hs             | 15 +++++++++-
 .../src/Wingman/Metaprogramming/Parser.hs     | 28 ++++++++-----------
 2 files changed, 26 insertions(+), 17 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
index 784f5f475f..dc4becf6ec 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
@@ -42,7 +42,7 @@ import           Development.IDE.Graph (Action, RuleResult, Rules, action)
 import           Development.IDE.Graph.Classes (Typeable, Binary, Hashable, NFData)
 import qualified FastString
 import           GHC.Generics (Generic)
-import           GhcPlugins (tupleDataCon, consDataCon, substTyAddInScope, ExternalPackageState, HscEnv (hsc_EPS), liftIO)
+import           GhcPlugins (tupleDataCon, consDataCon, substTyAddInScope, ExternalPackageState, HscEnv (hsc_EPS), liftIO, unpackFS)
 import qualified Ide.Plugin.Config as Plugin
 import           Ide.Plugin.Properties
 import           Ide.PluginUtils (usePropertyLsp)
@@ -62,6 +62,10 @@ import           Wingman.Judgements.SYB (everythingContaining)
 import           Wingman.Judgements.Theta
 import           Wingman.Range
 import           Wingman.Types
+import Generics.SYB hiding (Generic)
+import Development.IDE.Core.Compile (pattern WingmanMetaprogram)
+import Data.Foldable (for_)
+import Wingman.Metaprogramming.Parser (attempt_it)
 
 
 tacticDesc :: T.Text -> T.Text
@@ -178,6 +182,10 @@ getIdeDynflags state nfp = do
   msr <- unsafeRunStaleIde "getIdeDynflags" state nfp GetModSummaryWithoutTimestamps
   pure $ ms_hspp_opts $ msrModSummary msr
 
+getAllMetaprograms :: Data a => a -> [String]
+getAllMetaprograms = everything (<>) $ mkQ mempty $ \case
+  WingmanMetaprogram fs -> [ unpackFS fs ]
+  (_ :: HsExpr GhcTc)  -> mempty
 
 ------------------------------------------------------------------------------
 -- | Find the last typechecked module, and find the most specific span, as well
@@ -199,6 +207,7 @@ judgementForHole state nfp range cfg = do
       binds <- stale GetBindings
       tcg <- fmap (fmap tmrTypechecked)
            $ stale TypeCheck
+
       hscenv <- stale GhcSessionDeps
 
       (rss, g) <- liftMaybe $ getSpanAndTypeAtHole range' hf
@@ -212,6 +221,10 @@ judgementForHole state nfp range cfg = do
 
       (jdg, ctx) <- liftMaybe $ mkJudgementAndContext cfg g binds new_rss tcg eps kt
 
+      let mps = getAllMetaprograms $ tcg_binds $ untrackedStaleValue tcg
+      for_ mps $ \prog ->
+        liftIO $ putStrLn $ either id show $ attempt_it ctx jdg prog
+
       dflags <- getIdeDynflags state nfp
       pure (fmap realSrcSpanToRange new_rss, jdg, ctx, dflags)
 
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
index d78f672934..6c2640ec18 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
@@ -10,16 +10,18 @@ import qualified Control.Monad.Combinators.Expr as P
 import           Data.Function
 import           Data.Functor
 import           Data.List (foldl')
-import           Development.IDE.GHC.Compat (alphaTyVars)
+import           Development.IDE.GHC.Compat (alphaTyVars, LHsExpr, GhcPs)
 import           GhcPlugins (mkTyVarTy, mkFunTys, mkListTy, mkVarOcc)
 import qualified Refinery.Tactic as R
 import qualified Text.Megaparsec as P
+import qualified Text.Megaparsec.Char as C
 import           Wingman.Auto
 import           Wingman.Judgements (mkFirstJudgement)
 import           Wingman.LanguageServer.TacticProviders (useNameFromHypothesis)
 import           Wingman.Metaprogramming.Lexer
 import           Wingman.Tactics
 import           Wingman.Types
+import qualified Data.Text as T
 
 
 tactic :: Parser (TacticsM ())
@@ -29,6 +31,7 @@ tactic = flip P.makeExprParser operators $  P.choice
     , named  "intros" intros
     -- , named' "intro" intro
     , named' "destruct" $ useNameFromHypothesis destruct
+    , named "destruct_all" destructAll
     , named' "homo" $ useNameFromHypothesis homo
     , named' "apply" $ useNameFromHypothesis apply
     -- , named  "split" $ useNameFromHypothesis split
@@ -62,23 +65,16 @@ a_skolem, b_skolem, c_skolem :: Type
 (a_skolem : b_skolem : c_skolem : _) = skolems
 
 
-main :: IO ()
-main = do
-  case P.runParser (tactics <* P.eof)
-          "<splice>"
-          "intros, destruct as, [ assumption; auto ]" of
-    Left peb -> putStrLn $ P.errorBundlePretty peb
+attempt_it :: Context -> Judgement -> String -> Either String (LHsExpr GhcPs)
+attempt_it ctx jdg program =
+  case P.runParser (sc *> tactics <* P.eof) "<splice>" (T.pack program) of
+    Left peb -> Left $ P.errorBundlePretty peb
     Right tt -> do
-      let ty = mkFunTys
-                [ mkFunTys [a_skolem, b_skolem] b_skolem
-                , b_skolem
-                , mkListTy a_skolem
-                ] b_skolem
       case runTactic
-             emptyContext { ctxDefiningFuncs = [(mkVarOcc "hello", CType ty)] }
-             (mkFirstJudgement mempty True ty)
+             ctx
+             jdg
              tt
         of
-          Left tes -> putStrLn $ "failed: " <> show tes
-          Right rtr -> print $ rtr_extract rtr
+          Left tes -> Left $ show tes
+          Right rtr -> Right $ rtr_extract rtr
 

From 762f43c95a6e6f522a2cac18f020f203fc80c794 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 26 Apr 2021 07:28:14 -0700
Subject: [PATCH 06/52] Use a more concrete type for mkWingmanMetaprogram

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

diff --git a/ghcide/src/Development/IDE/Core/Compile.hs b/ghcide/src/Development/IDE/Core/Compile.hs
index 311703400f..156ab3af9f 100644
--- a/ghcide/src/Development/IDE/Core/Compile.hs
+++ b/ghcide/src/Development/IDE/Core/Compile.hs
@@ -224,7 +224,7 @@ pattern WingmanMetaprogram mp
   <- HsSCC _ (SourceText "wingman-meta-program") (StringLiteral NoSourceText mp)
       (L _ ( HsVar _ _))
 
-mkWingmanMetaprogram :: (XVar p ~ NoExt, XSCC p ~ NoExt, IdP p ~ RdrName) => SrcSpan -> FastString -> HsExpr p
+mkWingmanMetaprogram :: SrcSpan -> FastString -> HsExpr GhcPs
 mkWingmanMetaprogram ss mp =
   HsSCC noExt (SourceText "wingman-meta-program") (StringLiteral NoSourceText mp)
     $ L ss

From 7ddb88d83998a42d50490b1b806ab1054c3777e9 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 26 Apr 2021 07:48:02 -0700
Subject: [PATCH 07/52] Cleanup lexer

---
 .../src/Wingman/Metaprogramming/Lexer.hs                 | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Lexer.hs b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Lexer.hs
index 2fcf32dca5..ecb66481d7 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Lexer.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Lexer.hs
@@ -29,6 +29,9 @@ blockComment = L.skipBlockComment "{-" "-}"
 sc :: Parser ()
 sc = L.space P.space1 lineComment blockComment
 
+ichar :: Parser Char
+ichar = P.alphaNumChar <|> P.char '_' <|> P.char '\''
+
 lexeme :: Parser a -> Parser a
 lexeme = L.lexeme sc
 
@@ -45,20 +48,20 @@ braces :: Parser a -> Parser a
 braces = P.between (symbol "{") (symbol "}")
 
 identifier :: Text -> Parser ()
-identifier i = lexeme (P.string i *> P.notFollowedBy P.alphaNumChar)
+identifier i = lexeme (P.string i *> P.notFollowedBy ichar)
 
 -- FIXME [Reed M. 2020-10-18] Check to see if the variables are in the reserved list
 variable :: Parser OccName
 variable = lexeme $ do
     c <- P.alphaNumChar
-    cs <- P.many (P.alphaNumChar <|> P.char '_' <|> P.char '\'')
+    cs <- P.many ichar
     pure $ mkVarOcc (c:cs)
 
 -- FIXME [Reed M. 2020-10-18] Check to see if the variables are in the reserved list
 name :: Parser Text
 name = lexeme $ do
     c <- P.alphaNumChar
-    cs <- P.many (P.alphaNumChar <|> P.char '_' <|> P.char '\'' <|> P.char '-')
+    cs <- P.many (ichar <|> P.char '-')
     pure $ T.pack (c:cs)
 
 named :: Text -> TacticsM () -> Parser (TacticsM ())

From 0cd6a0e830edf5fef59ce61152951dae3ef5fbbe Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 26 Apr 2021 07:48:12 -0700
Subject: [PATCH 08/52] Use operator parsing for multiple tactics

---
 .../src/Wingman/Metaprogramming/Parser.hs     | 27 ++++++++-----------
 1 file changed, 11 insertions(+), 16 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
index 6c2640ec18..90dd8ad0bc 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
@@ -26,37 +26,32 @@ import qualified Data.Text as T
 
 tactic :: Parser (TacticsM ())
 tactic = flip P.makeExprParser operators $  P.choice
-    [ named  "assumption" assumption
+    [ braces tactic
+    , named  "assumption" assumption
     , named' "assume" assume
     , named  "intros" intros
     -- , named' "intro" intro
-    , named' "destruct" $ useNameFromHypothesis destruct
     , named "destruct_all" destructAll
+    , named' "destruct" $ useNameFromHypothesis destruct
     , named' "homo" $ useNameFromHypothesis homo
     , named' "apply" $ useNameFromHypothesis apply
-    -- , named  "split" $ useNameFromHypothesis split
+    , named'  "split" userSplit
     , named  "auto" auto
-    , R.try <$> (keyword "try" *> tactics)
+    , R.try <$> (keyword "try" *> tactic)
     ]
 
-multitactic :: Parser (TacticsM () -> TacticsM ())
-multitactic = P.choice
-    [ (flip (R.<@>)) <$> brackets (P.sepBy1 tactic (symbol ";"))
-    , (flip (>>)) <$> tactic
-    ]
+bindOne :: TacticsM a -> TacticsM a -> TacticsM a
+bindOne t t1 = t R.<@> [t1]
 
 operators :: [[P.Operator Parser (TacticsM ())]]
 operators =
     [ [ P.Prefix (symbol "*" $> R.many_) ]
     , [ P.InfixR (symbol "|" $> (R.<%>) )]
+    , [ P.InfixL (symbol ";" $> (>>))
+      , P.InfixL (symbol "," $> bindOne)
+      ]
     ]
 
-tactics :: Parser (TacticsM ())
-tactics = do
-    t <- tactic
-    ts <- P.many ((symbol ",") *> multitactic)
-    pure $ foldl' (&) t ts
-
 
 skolems :: [Type]
 skolems = fmap mkTyVarTy alphaTyVars
@@ -67,7 +62,7 @@ a_skolem, b_skolem, c_skolem :: Type
 
 attempt_it :: Context -> Judgement -> String -> Either String (LHsExpr GhcPs)
 attempt_it ctx jdg program =
-  case P.runParser (sc *> tactics <* P.eof) "<splice>" (T.pack program) of
+  case P.runParser (sc *> tactic <* P.eof) "<splice>" (T.pack program) of
     Left peb -> Left $ P.errorBundlePretty peb
     Right tt -> do
       case runTactic

From 10105a91c3dbd666136db1926b1adfe72f8ebeda Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 26 Apr 2021 07:58:22 -0700
Subject: [PATCH 09/52] Tidy the parser

---
 .../src/Wingman/Metaprogramming/Parser.hs                   | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
index 90dd8ad0bc..5a8899e013 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
@@ -7,16 +7,12 @@
 module Wingman.Metaprogramming.Parser where
 
 import qualified Control.Monad.Combinators.Expr as P
-import           Data.Function
 import           Data.Functor
-import           Data.List (foldl')
 import           Development.IDE.GHC.Compat (alphaTyVars, LHsExpr, GhcPs)
-import           GhcPlugins (mkTyVarTy, mkFunTys, mkListTy, mkVarOcc)
+import           GhcPlugins (mkTyVarTy)
 import qualified Refinery.Tactic as R
 import qualified Text.Megaparsec as P
-import qualified Text.Megaparsec.Char as C
 import           Wingman.Auto
-import           Wingman.Judgements (mkFirstJudgement)
 import           Wingman.LanguageServer.TacticProviders (useNameFromHypothesis)
 import           Wingman.Metaprogramming.Lexer
 import           Wingman.Tactics

From 65ff47268d024e8d2b31284f0e1b9df19ba770d8 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 26 Apr 2021 07:58:39 -0700
Subject: [PATCH 10/52] Add 'obvious' tactic

---
 .../src/Wingman/Metaprogramming/Parser.hs                 | 3 ++-
 plugins/hls-tactics-plugin/src/Wingman/Tactics.hs         | 8 +++++++-
 2 files changed, 9 insertions(+), 2 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
index 5a8899e013..868150fdff 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
@@ -31,7 +31,8 @@ tactic = flip P.makeExprParser operators $  P.choice
     , named' "destruct" $ useNameFromHypothesis destruct
     , named' "homo" $ useNameFromHypothesis homo
     , named' "apply" $ useNameFromHypothesis apply
-    , named'  "split" userSplit
+    , named' "split" userSplit
+    , named  "obvious" obvious
     , named  "auto" auto
     , R.try <$> (keyword "try" *> tactic)
     ]
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs
index 429931f631..38492a1c87 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs
@@ -10,6 +10,7 @@ import           Control.Monad (unless)
 import           Control.Monad.Except (throwError)
 import           Control.Monad.Reader.Class (MonadReader (ask))
 import           Control.Monad.State.Strict (StateT(..), runStateT)
+import           Data.Bool (bool)
 import           Data.Foldable
 import           Data.Functor ((<&>))
 import           Data.Generics.Labels ()
@@ -255,6 +256,12 @@ splitSingle = tracing "splitSingle" $ do
       splitDataCon dc
     _ -> throwError $ GoalMismatch "splitSingle" g
 
+------------------------------------------------------------------------------
+-- | Like 'split', but prunes any data constructors which have holes.
+obvious :: TacticsM ()
+obvious = tracing "obvious" $ do
+  pruning split $ bool (Just NoProgress) Nothing . null
+
 
 ------------------------------------------------------------------------------
 -- | Allow the given tactic to proceed if and only if it introduces holes that
@@ -402,4 +409,3 @@ applyByName name = do
       True  -> apply hi
       False -> empty
 
-

From f24c7b71bfe0b239414f2cfcf71ffc01846e72e8 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 26 Apr 2021 08:16:20 -0700
Subject: [PATCH 11/52] Add intros', which lets you bind the names you want

---
 .../src/Wingman/Metaprogramming/Lexer.hs      |  8 -----
 .../src/Wingman/Metaprogramming/Parser.hs     | 33 ++++++++++++-------
 .../hls-tactics-plugin/src/Wingman/Tactics.hs | 17 +++++++---
 3 files changed, 35 insertions(+), 23 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Lexer.hs b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Lexer.hs
index ecb66481d7..393e077c01 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Lexer.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Lexer.hs
@@ -7,7 +7,6 @@ module Wingman.Metaprogramming.Lexer where
 
 import           Control.Applicative
 import           Control.Monad
-import           Data.Functor
 import           Data.Text (Text)
 import qualified Data.Text as T
 import           Data.Void
@@ -15,7 +14,6 @@ import           Name
 import qualified Text.Megaparsec as P
 import qualified Text.Megaparsec.Char as P
 import qualified Text.Megaparsec.Char.Lexer as L
-import           Wingman.Types
 
 
 type Parser = P.Parsec Void Text
@@ -64,12 +62,6 @@ name = lexeme $ do
     cs <- P.many (ichar <|> P.char '-')
     pure $ T.pack (c:cs)
 
-named :: Text -> TacticsM () -> Parser (TacticsM ())
-named name tac = identifier name $> tac
-
-named' :: Text -> (OccName -> TacticsM ()) -> Parser (TacticsM ())
-named' name tac = tac <$> (identifier name *> variable)
-
 keyword :: Text -> Parser ()
 keyword = identifier
 
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
index 868150fdff..d2d6503ea2 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
@@ -20,20 +20,31 @@ import           Wingman.Types
 import qualified Data.Text as T
 
 
+nullary :: T.Text -> TacticsM () -> Parser (TacticsM ())
+nullary name tac = identifier name $> tac
+
+unary_occ :: T.Text -> (OccName -> TacticsM ()) -> Parser (TacticsM ())
+unary_occ name tac = tac <$> (identifier name *> variable)
+
+variadic_occ :: T.Text -> ([OccName] -> TacticsM ()) -> Parser (TacticsM ())
+variadic_occ name tac = tac <$> (identifier name *> P.many variable)
+
+
 tactic :: Parser (TacticsM ())
 tactic = flip P.makeExprParser operators $  P.choice
     [ braces tactic
-    , named  "assumption" assumption
-    , named' "assume" assume
-    , named  "intros" intros
-    -- , named' "intro" intro
-    , named "destruct_all" destructAll
-    , named' "destruct" $ useNameFromHypothesis destruct
-    , named' "homo" $ useNameFromHypothesis homo
-    , named' "apply" $ useNameFromHypothesis apply
-    , named' "split" userSplit
-    , named  "obvious" obvious
-    , named  "auto" auto
+    , nullary   "assumption" assumption
+    , unary_occ "assume" assume
+    , variadic_occ   "intros" $ \case
+        []    -> intros
+        names -> intros' $ Just names
+    , nullary   "destruct_all" destructAll
+    , unary_occ "destruct" $ useNameFromHypothesis destruct
+    , unary_occ "homo" $ useNameFromHypothesis homo
+    , unary_occ "apply" $ useNameFromHypothesis apply
+    , unary_occ "split" userSplit
+    , nullary   "obvious" obvious
+    , nullary   "auto" auto
     , R.try <$> (keyword "try" *> tactic)
     ]
 
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs
index 38492a1c87..0313c1707b 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs
@@ -94,17 +94,26 @@ restrictPositionForApplication f app = do
 ------------------------------------------------------------------------------
 -- | Introduce a lambda binding every variable.
 intros :: TacticsM ()
-intros = rule $ \jdg -> do
+intros = intros' Nothing
+
+------------------------------------------------------------------------------
+-- | Introduce a lambda binding every variable.
+intros'
+    :: Maybe [OccName]  -- ^ When 'Nothing', generate a new name for every
+                        -- variable. Otherwise, only bind the variables named.
+    -> TacticsM ()
+intros' names = rule $ \jdg -> do
   let g  = jGoal jdg
   ctx <- ask
   case tcSplitFunTys $ unCType g of
     ([], _) -> throwError $ GoalMismatch "intros" g
     (as, b) -> do
-      let vs = mkManyGoodNames (hyNamesInScope $ jEntireHypothesis jdg) as
-      let top_hole = isTopHole ctx jdg
+      let vs = fromMaybe (mkManyGoodNames (hyNamesInScope $ jEntireHypothesis jdg) as) names
+          num_args = length vs
+          top_hole = isTopHole ctx jdg
           hy' = lambdaHypothesis top_hole $ zip vs $ coerce as
           jdg' = introduce hy'
-               $ withNewGoal (CType b) jdg
+               $ withNewGoal (CType $ mkFunTys (drop num_args as) b) jdg
       ext <- newSubgoal jdg'
       pure $
         ext

From 6162a8116c9123a362aa6e7238e0c6d306190db9 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 26 Apr 2021 10:47:12 -0700
Subject: [PATCH 12/52] Add intro to the parser

---
 plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs | 1 +
 1 file changed, 1 insertion(+)

diff --git a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
index d2d6503ea2..025ebc5687 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
@@ -38,6 +38,7 @@ tactic = flip P.makeExprParser operators $  P.choice
     , variadic_occ   "intros" $ \case
         []    -> intros
         names -> intros' $ Just names
+    , unary_occ  "intro" $ intros' . Just . pure
     , nullary   "destruct_all" destructAll
     , unary_occ "destruct" $ useNameFromHypothesis destruct
     , unary_occ "homo" $ useNameFromHypothesis homo

From dd548ba9df77a047ec87aeb96cc69d6fc8009944 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 26 Apr 2021 11:26:28 -0700
Subject: [PATCH 13/52] Add a modifyDynFlags field to plugins; push it into the
 parsed module

---
 ghcide/src/Development/IDE/Core/Compile.hs | 15 ++++++-------
 ghcide/src/Development/IDE/Core/Rules.hs   | 25 +++++++++++++++-------
 ghcide/src/Development/IDE/Core/Service.hs |  5 ++++-
 ghcide/src/Development/IDE/Core/Shake.hs   |  5 ++++-
 ghcide/src/Development/IDE/Main.hs         |  8 ++++---
 ghcide/src/Development/IDE/Plugin.hs       |  7 ++++--
 ghcide/src/Development/IDE/Plugin/HLS.hs   | 18 +++++++++++-----
 ghcide/src/Development/IDE/Plugin/Test.hs  |  8 ++++---
 hls-plugin-api/hls-plugin-api.cabal        |  1 +
 hls-plugin-api/src/Ide/Types.hs            |  4 ++++
 10 files changed, 64 insertions(+), 32 deletions(-)

diff --git a/ghcide/src/Development/IDE/Core/Compile.hs b/ghcide/src/Development/IDE/Core/Compile.hs
index 156ab3af9f..d210cfb81f 100644
--- a/ghcide/src/Development/IDE/Core/Compile.hs
+++ b/ghcide/src/Development/IDE/Core/Compile.hs
@@ -130,13 +130,14 @@ import Generics.SYB hiding (orElse)
 parseModule
     :: IdeOptions
     -> HscEnv
+    -> (DynFlags -> DynFlags)
     -> FilePath
     -> ModSummary
     -> IO (IdeResult ParsedModule)
-parseModule IdeOptions{..} env filename ms =
+parseModule IdeOptions{..} env modifyDynFlags filename ms =
     fmap (either (, Nothing) id) $
     runExceptT $ do
-        (diag, modu) <- parseFileContents env optPreprocessor filename ms
+        (diag, modu) <- parseFileContents env modifyDynFlags optPreprocessor filename ms
         return (diag, Just modu)
 
 
@@ -844,18 +845,14 @@ parseHeader dflags filename contents = do
 -- ModSummary must contain the (preprocessed) contents of the buffer
 parseFileContents
        :: HscEnv
+       -> (DynFlags -> DynFlags)
        -> (GHC.ParsedSource -> IdePreprocessedSource)
        -> FilePath  -- ^ the filename (for source locations)
        -> ModSummary
        -> ExceptT [FileDiagnostic] IO ([FileDiagnostic], ParsedModule)
-parseFileContents env customPreprocessor filename ms = do
+parseFileContents env modifyDynFlags customPreprocessor filename ms = do
    let loc  = mkRealSrcLoc (mkFastString filename) 1 1
-       dflags' = ms_hspp_opts ms
-       dflags =
-         dflags'
-            { staticPlugins =
-                staticPlugins dflags' <> [wingmanMetaprogrammingPlugin]
-            }
+       dflags = modifyDynFlags $ ms_hspp_opts ms
 
        contents = fromJust $ ms_hspp_buf ms
    case unP Parser.parseModule (mkPState dflags contents loc) of
diff --git a/ghcide/src/Development/IDE/Core/Rules.hs b/ghcide/src/Development/IDE/Core/Rules.hs
index f63da383a0..b8323145be 100644
--- a/ghcide/src/Development/IDE/Core/Rules.hs
+++ b/ghcide/src/Development/IDE/Core/Rules.hs
@@ -112,7 +112,7 @@ import           Development.IDE.GHC.Compat                   hiding
                                                                writeHieFile)
 import           Development.IDE.GHC.Error
 import           Development.IDE.GHC.ExactPrint
-import           Development.IDE.GHC.Util
+import           Development.IDE.GHC.Util hiding (modifyDynFlags)
 import           Development.IDE.Import.DependencyInformation
 import           Development.IDE.Import.FindImports
 import qualified Development.IDE.Spans.AtPoint                as AtPoint
@@ -216,16 +216,18 @@ getParsedModuleRule =
     sess <- use_ GhcSession file
     let hsc = hscEnv sess
     opt <- getIdeOptions
+    modify_dflags <- getModifyDynFlags
 
+    -- TODO(sandy): should we apply modify_dflags here?
     let dflags    = ms_hspp_opts ms
-        mainParse = getParsedModuleDefinition hsc opt file ms
+        mainParse = getParsedModuleDefinition hsc modify_dflags opt file ms
 
     -- Parse again (if necessary) to capture Haddock parse errors
     res@(_,pmod) <- if gopt Opt_Haddock dflags
         then
             liftIO mainParse
         else do
-            let haddockParse = getParsedModuleDefinition hsc opt file (withOptHaddock ms)
+            let haddockParse = getParsedModuleDefinition hsc modify_dflags opt file (withOptHaddock ms)
 
             -- parse twice, with and without Haddocks, concurrently
             -- we cannot ignore Haddock parse errors because files of
@@ -283,19 +285,25 @@ getParsedModuleWithCommentsRule =
     ModSummaryResult{msrModSummary = ms} <- use_ GetModSummary file
     sess <- use_ GhcSession file
     opt <- getIdeOptions
+    modify_dflags <- getModifyDynFlags
 
     let ms' = withoutOption Opt_Haddock $ withOption Opt_KeepRawTokenStream ms
 
-    liftIO $ snd <$> getParsedModuleDefinition (hscEnv sess) opt file ms'
+    liftIO $ snd <$> getParsedModuleDefinition (hscEnv sess) modify_dflags opt file ms'
+
+getModifyDynFlags :: Action (DynFlags -> DynFlags)
+getModifyDynFlags = maybe id modifyDynFlags <$> getShakeExtra
+
 
 getParsedModuleDefinition
     :: HscEnv
+   -> (DynFlags -> DynFlags)
     -> IdeOptions
     -> NormalizedFilePath
     -> ModSummary -> IO ([FileDiagnostic], Maybe ParsedModule)
-getParsedModuleDefinition packageState opt file ms = do
+getParsedModuleDefinition packageState modifyDynFlags opt file ms = do
     let fp = fromNormalizedFilePath file
-    (diag, res) <- parseModule opt packageState fp ms
+    (diag, res) <- parseModule opt packageState modifyDynFlags fp ms
     case res of
         Nothing   -> pure (diag, Nothing)
         Just modu -> pure (diag, Just modu)
@@ -863,14 +871,15 @@ regenerateHiFile :: HscEnvEq -> NormalizedFilePath -> ModSummary -> Maybe Linkab
 regenerateHiFile sess f ms compNeeded = do
     let hsc = hscEnv sess
     opt <- getIdeOptions
+    modify_dflags <- getModifyDynFlags
 
     -- Embed haddocks in the interface file
-    (diags, mb_pm) <- liftIO $ getParsedModuleDefinition hsc opt f (withOptHaddock ms)
+    (diags, mb_pm) <- liftIO $ getParsedModuleDefinition hsc modify_dflags opt f (withOptHaddock ms)
     (diags, mb_pm) <- case mb_pm of
         Just _ -> return (diags, mb_pm)
         Nothing -> do
             -- if parsing fails, try parsing again with Haddock turned off
-            (diagsNoHaddock, mb_pm) <- liftIO $ getParsedModuleDefinition hsc opt f ms
+            (diagsNoHaddock, mb_pm) <- liftIO $ getParsedModuleDefinition hsc modify_dflags opt f ms
             return (mergeParseErrorsHaddock diagsNoHaddock diags, mb_pm)
     case mb_pm of
         Nothing -> return (diags, Nothing)
diff --git a/ghcide/src/Development/IDE/Core/Service.hs b/ghcide/src/Development/IDE/Core/Service.hs
index b03da9fd42..5d010c416c 100644
--- a/ghcide/src/Development/IDE/Core/Service.hs
+++ b/ghcide/src/Development/IDE/Core/Service.hs
@@ -30,6 +30,7 @@ import qualified Language.LSP.Types              as LSP
 
 import           Control.Monad
 import           Development.IDE.Core.Shake
+import Development.IDE.GHC.Compat (DynFlags)
 
 
 ------------------------------------------------------------
@@ -38,6 +39,7 @@ import           Development.IDE.Core.Shake
 -- | Initialise the Compiler Service.
 initialise :: Config
            -> Rules ()
+           -> (DynFlags -> DynFlags)
            -> Maybe (LSP.LanguageContextEnv Config)
            -> Logger
            -> Debouncer LSP.NormalizedUri
@@ -46,10 +48,11 @@ initialise :: Config
            -> HieDb
            -> IndexQueue
            -> IO IdeState
-initialise defaultConfig mainRule lspEnv logger debouncer options vfs hiedb hiedbChan =
+initialise defaultConfig mainRule modifyDynFlags lspEnv logger debouncer options vfs hiedb hiedbChan =
     shakeOpen
         lspEnv
         defaultConfig
+        modifyDynFlags
         logger
         debouncer
         (optShakeProfiling options)
diff --git a/ghcide/src/Development/IDE/Core/Shake.hs b/ghcide/src/Development/IDE/Core/Shake.hs
index badb8628f9..200c01ae78 100644
--- a/ghcide/src/Development/IDE/Core/Shake.hs
+++ b/ghcide/src/Development/IDE/Core/Shake.hs
@@ -149,6 +149,7 @@ import           Ide.Plugin.Config
 import qualified Ide.PluginUtils                      as HLS
 import           Ide.Types                            (PluginId)
 import           UnliftIO.Exception                   (bracket_)
+import DynFlags (DynFlags)
 
 -- | We need to serialize writes to the database, so we send any function that
 -- needs to write to the database over the channel, where it will be picked up by
@@ -171,6 +172,7 @@ data ShakeExtras = ShakeExtras
      lspEnv :: Maybe (LSP.LanguageContextEnv Config)
     ,debouncer :: Debouncer NormalizedUri
     ,logger :: Logger
+    ,modifyDynFlags :: DynFlags -> DynFlags
     ,globals :: Var (HMap.HashMap TypeRep Dynamic)
     ,state :: Var Values
     ,diagnostics :: Var DiagnosticStore
@@ -461,6 +463,7 @@ seqValue v b = case v of
 -- | Open a 'IdeState', should be shut using 'shakeShut'.
 shakeOpen :: Maybe (LSP.LanguageContextEnv Config)
           -> Config
+          -> (DynFlags -> DynFlags)
           -> Logger
           -> Debouncer NormalizedUri
           -> Maybe FilePath
@@ -472,7 +475,7 @@ shakeOpen :: Maybe (LSP.LanguageContextEnv Config)
           -> ShakeOptions
           -> Rules ()
           -> IO IdeState
-shakeOpen lspEnv defaultConfig logger debouncer
+shakeOpen lspEnv defaultConfig modifyDynFlags logger debouncer
   shakeProfileDir (IdeReportProgress reportProgress) ideTesting@(IdeTesting testing) hiedb indexQueue vfs opts rules = mdo
 
     inProgress <- newVar HMap.empty
diff --git a/ghcide/src/Development/IDE/Main.hs b/ghcide/src/Development/IDE/Main.hs
index c3a34415cc..fb36e52522 100644
--- a/ghcide/src/Development/IDE/Main.hs
+++ b/ghcide/src/Development/IDE/Main.hs
@@ -46,7 +46,7 @@ import           Development.IDE.Core.Shake            (IdeState (shakeExtras),
 import           Development.IDE.Core.Tracing          (measureMemory)
 import           Development.IDE.Graph                 (action)
 import           Development.IDE.LSP.LanguageServer    (runLanguageServer)
-import           Development.IDE.Plugin                (Plugin (pluginHandlers, pluginRules))
+import           Development.IDE.Plugin                (Plugin (pluginHandlers, pluginRules, pluginModifyDynflags))
 import           Development.IDE.Plugin.HLS            (asGhcIdePlugin)
 import qualified Development.IDE.Plugin.HLS.GhcIde     as Ghcide
 import           Development.IDE.Session               (SessionLoadingOptions,
@@ -89,6 +89,7 @@ import           System.IO                             (BufferMode (LineBufferin
 import           System.Time.Extra                     (offsetTime,
                                                         showDuration)
 import           Text.Printf                           (printf)
+import Data.Monoid (Endo(appEndo))
 
 data Command
     = Check [FilePath]  -- ^ Typecheck some paths and print diagnostics. Exit code is the number of failures
@@ -223,6 +224,7 @@ defaultMain Arguments{..} = do
                 initialise
                     argsDefaultHlsConfig
                     rules
+                    (appEndo $ pluginModifyDynflags plugins)
                     (Just env)
                     logger
                     debouncer
@@ -260,7 +262,7 @@ defaultMain Arguments{..} = do
                         { optCheckParents = pure NeverCheck
                         , optCheckProject = pure False
                         }
-            ide <- initialise argsDefaultHlsConfig rules Nothing logger debouncer options vfs hiedb hieChan
+            ide <- initialise argsDefaultHlsConfig rules (appEndo $ pluginModifyDynflags plugins) Nothing logger debouncer options vfs hiedb hieChan
             shakeSessionInit ide
             registerIdeConfiguration (shakeExtras ide) $ IdeConfiguration mempty (hashed Nothing)
 
@@ -309,7 +311,7 @@ defaultMain Arguments{..} = do
                     { optCheckParents = pure NeverCheck,
                       optCheckProject = pure False
                     }
-            ide <- initialise argsDefaultHlsConfig rules Nothing logger debouncer options vfs hiedb hieChan
+            ide <- initialise argsDefaultHlsConfig rules (appEndo $ pluginModifyDynflags plugins) Nothing logger debouncer options vfs hiedb hieChan
             shakeSessionInit ide
             registerIdeConfiguration (shakeExtras ide) $ IdeConfiguration mempty (hashed Nothing)
             c ide
diff --git a/ghcide/src/Development/IDE/Plugin.hs b/ghcide/src/Development/IDE/Plugin.hs
index c29e6a5470..ef2d5e319a 100644
--- a/ghcide/src/Development/IDE/Plugin.hs
+++ b/ghcide/src/Development/IDE/Plugin.hs
@@ -5,17 +5,20 @@ import           Development.IDE.Graph
 
 import           Development.IDE.LSP.Server
 import qualified Language.LSP.Server        as LSP
+import Development.IDE.GHC.Compat (DynFlags)
+import Data.Monoid (Endo)
 
 data Plugin c = Plugin
     {pluginRules    :: Rules ()
     ,pluginHandlers :: LSP.Handlers (ServerM c)
+    ,pluginModifyDynflags :: Endo DynFlags
     }
 
 instance Default (Plugin c) where
-    def = Plugin mempty mempty
+    def = Plugin mempty mempty mempty
 
 instance Semigroup (Plugin c) where
-    Plugin x1 h1 <> Plugin x2 h2 = Plugin (x1<>x2) (h1 <> h2)
+    Plugin x1 h1 d1 <> Plugin x2 h2 d2 = Plugin (x1<>x2) (h1 <> h2) (d1 <> d2)
 
 instance Monoid (Plugin c) where
     mempty = def
diff --git a/ghcide/src/Development/IDE/Plugin/HLS.hs b/ghcide/src/Development/IDE/Plugin/HLS.hs
index c208a2c21e..39f9a25025 100644
--- a/ghcide/src/Development/IDE/Plugin/HLS.hs
+++ b/ghcide/src/Development/IDE/Plugin/HLS.hs
@@ -38,6 +38,8 @@ import           Text.Regex.TDFA.Text         ()
 import           UnliftIO                     (MonadUnliftIO)
 import           UnliftIO.Async               (forConcurrently)
 import           UnliftIO.Exception           (catchAny)
+import Development.IDE.GHC.Compat (DynFlags)
+import Data.Monoid (Endo(Endo))
 
 -- ---------------------------------------------------------------------
 --
@@ -48,7 +50,8 @@ asGhcIdePlugin (IdePlugins ls) =
     mkPlugin rulesPlugins HLS.pluginRules <>
     mkPlugin executeCommandPlugins HLS.pluginCommands <>
     mkPlugin extensiblePlugins HLS.pluginHandlers <>
-    mkPlugin extensibleNotificationPlugins HLS.pluginNotificationHandlers
+    mkPlugin extensibleNotificationPlugins HLS.pluginNotificationHandlers <>
+    mkPlugin dynFlagsPlugins HLS.pluginModifyDynflags
     where
 
         mkPlugin :: ([(PluginId, b)] -> Plugin Config) -> (PluginDescriptor IdeState -> b) -> Plugin Config
@@ -63,14 +66,19 @@ asGhcIdePlugin (IdePlugins ls) =
 -- ---------------------------------------------------------------------
 
 rulesPlugins :: [(PluginId, Rules ())] -> Plugin Config
-rulesPlugins rs = Plugin rules mempty
+rulesPlugins rs = Plugin rules mempty mempty
     where
         rules = foldMap snd rs
 
+dynFlagsPlugins :: [(PluginId, DynFlags -> DynFlags)] -> Plugin Config
+dynFlagsPlugins rs = Plugin mempty mempty endo
+    where
+        endo = foldMap (Endo . snd) rs
+
 -- ---------------------------------------------------------------------
 
 executeCommandPlugins :: [(PluginId, [PluginCommand IdeState])] -> Plugin Config
-executeCommandPlugins ecs = Plugin mempty (executeCommandHandlers ecs)
+executeCommandPlugins ecs = Plugin mempty (executeCommandHandlers ecs) mempty
 
 executeCommandHandlers :: [(PluginId, [PluginCommand IdeState])] -> LSP.Handlers (ServerM Config)
 executeCommandHandlers ecs = requestHandler SWorkspaceExecuteCommand execCmd
@@ -132,7 +140,7 @@ executeCommandHandlers ecs = requestHandler SWorkspaceExecuteCommand execCmd
 -- ---------------------------------------------------------------------
 
 extensiblePlugins :: [(PluginId, PluginHandlers IdeState)] -> Plugin Config
-extensiblePlugins xs = Plugin mempty handlers
+extensiblePlugins xs = Plugin mempty handlers mempty
   where
     IdeHandlers handlers' = foldMap bakePluginId xs
     bakePluginId :: (PluginId, PluginHandlers IdeState) -> IdeHandlers
@@ -160,7 +168,7 @@ extensiblePlugins xs = Plugin mempty handlers
 -- ---------------------------------------------------------------------
 
 extensibleNotificationPlugins :: [(PluginId, PluginNotificationHandlers IdeState)] -> Plugin Config
-extensibleNotificationPlugins xs = Plugin mempty handlers
+extensibleNotificationPlugins xs = Plugin mempty handlers mempty
   where
     IdeNotificationHandlers handlers' = foldMap bakePluginId xs
     bakePluginId :: (PluginId, PluginNotificationHandlers IdeState) -> IdeNotificationHandlers
diff --git a/ghcide/src/Development/IDE/Plugin/Test.hs b/ghcide/src/Development/IDE/Plugin/Test.hs
index e8643d9471..47fa49f14f 100644
--- a/ghcide/src/Development/IDE/Plugin/Test.hs
+++ b/ghcide/src/Development/IDE/Plugin/Test.hs
@@ -37,6 +37,8 @@ import           Ide.Types
 import qualified Language.LSP.Server            as LSP
 import           Language.LSP.Types
 import           System.Time.Extra
+import qualified Development.IDE.Plugin as P
+import Data.Default (def)
 
 data TestRequest
     = BlockSeconds Seconds           -- ^ :: Null
@@ -51,9 +53,9 @@ newtype WaitForIdeRuleResult = WaitForIdeRuleResult { ideResultSuccess::Bool}
     deriving newtype (FromJSON, ToJSON)
 
 plugin :: Plugin c
-plugin = Plugin {
-    pluginRules = return (),
-    pluginHandlers = requestHandler (SCustomMethod "test") testRequestHandler'
+plugin = def {
+    P.pluginRules = return (),
+    P.pluginHandlers = requestHandler (SCustomMethod "test") testRequestHandler'
 }
   where
       testRequestHandler' ide req
diff --git a/hls-plugin-api/hls-plugin-api.cabal b/hls-plugin-api/hls-plugin-api.cabal
index acec2485d4..c486e7a96b 100644
--- a/hls-plugin-api/hls-plugin-api.cabal
+++ b/hls-plugin-api/hls-plugin-api.cabal
@@ -43,6 +43,7 @@ library
     , dependent-sum
     , Diff                  ^>=0.4.0
     , dlist
+    , ghc
     , hashable
     , hslogger
     , lens
diff --git a/hls-plugin-api/src/Ide/Types.hs b/hls-plugin-api/src/Ide/Types.hs
index c17171b2f0..fbd9660cae 100644
--- a/hls-plugin-api/src/Ide/Types.hs
+++ b/hls-plugin-api/src/Ide/Types.hs
@@ -50,6 +50,8 @@ import           Language.LSP.VFS
 import           OpenTelemetry.Eventlog
 import           System.IO.Unsafe
 import           Text.Regex.TDFA.Text            ()
+import GhcPlugins (StaticPlugin)
+import DynFlags (DynFlags)
 
 -- ---------------------------------------------------------------------
 
@@ -65,6 +67,7 @@ data PluginDescriptor ideState =
                    , pluginHandlers     :: PluginHandlers ideState
                    , pluginConfigDescriptor :: ConfigDescriptor
                    , pluginNotificationHandlers :: PluginNotificationHandlers ideState
+                   , pluginModifyDynflags :: DynFlags -> DynFlags
                    }
 
 -- | An existential wrapper of 'Properties'
@@ -297,6 +300,7 @@ defaultPluginDescriptor plId =
     mempty
     defaultConfigDescriptor
     mempty
+    id
 
 newtype CommandId = CommandId T.Text
   deriving (Show, Read, Eq, Ord)

From fe4f84ad2092c573a5619df3b9a6e1ddeefdfd17 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 26 Apr 2021 11:31:04 -0700
Subject: [PATCH 14/52] Modify dflags when typechecking too

---
 ghcide/src/Development/IDE/Core/Compile.hs | 11 ++++++-----
 ghcide/src/Development/IDE/Core/Rules.hs   |  3 ++-
 2 files changed, 8 insertions(+), 6 deletions(-)

diff --git a/ghcide/src/Development/IDE/Core/Compile.hs b/ghcide/src/Development/IDE/Core/Compile.hs
index d210cfb81f..391c26b0d6 100644
--- a/ghcide/src/Development/IDE/Core/Compile.hs
+++ b/ghcide/src/Development/IDE/Core/Compile.hs
@@ -155,10 +155,11 @@ computePackageDeps env pkg = do
 
 typecheckModule :: IdeDefer
                 -> HscEnv
+                -> (DynFlags -> DynFlags)
                 -> [Linkable] -- ^ linkables not to unload
                 -> ParsedModule
                 -> IO (IdeResult TcModuleResult)
-typecheckModule (IdeDefer defer) hsc keep_lbls pm = do
+typecheckModule (IdeDefer defer) hsc modify_dflags keep_lbls pm = do
     fmap (either (,Nothing) id) $
       catchSrcErrors (hsc_dflags hsc) "typecheck" $ do
 
@@ -167,7 +168,7 @@ typecheckModule (IdeDefer defer) hsc keep_lbls pm = do
 
         modSummary' <- initPlugins hsc modSummary
         (warnings, tcm) <- withWarnings "typecheck" $ \tweak ->
-            tcRnModule hsc keep_lbls $ demoteIfDefer pm{pm_mod_summary = tweak modSummary'}
+            tcRnModule hsc modify_dflags keep_lbls $ demoteIfDefer pm{pm_mod_summary = tweak modSummary'}
         let errorPipeline = unDefer . hideDiag dflags . tagDiag
             diags = map errorPipeline warnings
             deferedError = any fst diags
@@ -242,10 +243,10 @@ addWingmanMetaprogrammingSyntax =
       L ss $ mkWingmanMetaprogram ss mp
     (x :: LHsExpr GhcPs) -> x
 
-tcRnModule :: HscEnv -> [Linkable] -> ParsedModule -> IO TcModuleResult
-tcRnModule hsc_env keep_lbls pmod = do
+tcRnModule :: HscEnv -> (DynFlags -> DynFlags) -> [Linkable] -> ParsedModule -> IO TcModuleResult
+tcRnModule hsc_env modify_dflags keep_lbls pmod = do
   let ms = pm_mod_summary pmod
-      hsc_env_tmp = hsc_env { hsc_dflags = ms_hspp_opts ms }
+      hsc_env_tmp = hsc_env { hsc_dflags = modify_dflags $ ms_hspp_opts ms }
 
   unload hsc_env_tmp keep_lbls
 
diff --git a/ghcide/src/Development/IDE/Core/Rules.hs b/ghcide/src/Development/IDE/Core/Rules.hs
index b8323145be..59b8ef39dc 100644
--- a/ghcide/src/Development/IDE/Core/Rules.hs
+++ b/ghcide/src/Development/IDE/Core/Rules.hs
@@ -620,10 +620,11 @@ typeCheckRuleDefinition
 typeCheckRuleDefinition hsc pm = do
   setPriority priorityTypeCheck
   IdeOptions { optDefer = defer } <- getIdeOptions
+  modify_dflags <- getModifyDynFlags
 
   linkables_to_keep <- currentLinkables
   addUsageDependencies $ liftIO $
-    typecheckModule defer hsc linkables_to_keep pm
+    typecheckModule defer hsc modify_dflags linkables_to_keep pm
   where
     addUsageDependencies :: Action (a, Maybe TcModuleResult) -> Action (a, Maybe TcModuleResult)
     addUsageDependencies a = do

From 796124542fb32593545cc629e35f6bec69d8ed8c Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Tue, 27 Apr 2021 09:08:56 -0700
Subject: [PATCH 15/52] Use the dynflags modifier to remove wingman specific
 code from ghcide

---
 ghcide/session-loader/Development/IDE/Session.hs |  9 ---------
 plugins/hls-tactics-plugin/src/Wingman/Plugin.hs | 10 ++++++++++
 2 files changed, 10 insertions(+), 9 deletions(-)

diff --git a/ghcide/session-loader/Development/IDE/Session.hs b/ghcide/session-loader/Development/IDE/Session.hs
index 3c96369b0a..9c8e572068 100644
--- a/ghcide/session-loader/Development/IDE/Session.hs
+++ b/ghcide/session-loader/Development/IDE/Session.hs
@@ -772,7 +772,6 @@ setOptions (ComponentOptions theOpts compRoot _) dflags = do
           setIgnoreInterfacePragmas $
           setLinkerOptions $
           disableOptimisation $
-          allowEmptyCaseButWithWarning $
           setUpTypedHoles $
           enableQuasiQuotes $
           makeDynFlagsAbsolute compRoot dflags'
@@ -785,14 +784,6 @@ setOptions (ComponentOptions theOpts compRoot _) dflags = do
 enableQuasiQuotes :: DynFlags -> DynFlags
 enableQuasiQuotes = flip xopt_set QuasiQuotes
 
--- | Wingman wants to support destructing of empty cases, but these are a parse
--- error by default. So we want to enable 'EmptyCase', but then that leads to
--- silent errors without 'Opt_WarnIncompletePatterns'.
-allowEmptyCaseButWithWarning :: DynFlags -> DynFlags
-allowEmptyCaseButWithWarning =
-  flip xopt_set EmptyCase . flip wopt_set Opt_WarnIncompletePatterns
-
-
 -- we don't want to generate object code so we compile to bytecode
 -- (HscInterpreted) which implies LinkInMemory
 -- HscInterpreted
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs b/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs
index 58cfd7b9ad..54c92fc07f 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs
@@ -20,6 +20,7 @@ import           Development.IDE.Core.Shake (IdeState (..))
 import           Development.IDE.Core.UseStale (Tracked, TrackedStale(..), unTrack, mapAgeFrom, unsafeMkCurrent)
 import           Development.IDE.GHC.Compat
 import           Development.IDE.GHC.ExactPrint
+import           GHC.LanguageExtensions.Type (Extension(EmptyCase))
 import           Generics.SYB.GHC
 import           Ide.Types
 import           Language.LSP.Server
@@ -62,9 +63,18 @@ descriptor plId = (defaultPluginDescriptor plId)
   , pluginRules = wingmanRules plId
   , pluginConfigDescriptor =
       defaultConfigDescriptor {configCustomConfig = mkCustomConfig properties}
+  , pluginModifyDynflags = allowEmptyCaseButWithWarning
   }
 
 
+-- | Wingman wants to support destructing of empty cases, but these are a parse
+-- error by default. So we want to enable 'EmptyCase', but then that leads to
+-- silent errors without 'Opt_WarnIncompletePatterns'.
+allowEmptyCaseButWithWarning :: DynFlags -> DynFlags
+allowEmptyCaseButWithWarning =
+  flip xopt_set EmptyCase . flip wopt_set Opt_WarnIncompletePatterns
+
+
 codeActionProvider :: PluginMethodHandler IdeState TextDocumentCodeAction
 codeActionProvider state plId (CodeActionParams _ _ (TextDocumentIdentifier uri) (unsafeMkCurrent -> range) _ctx)
   | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do

From 3383f64d906671d9999e1a8a3f695b3703ab8344 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Tue, 27 Apr 2021 09:50:37 -0700
Subject: [PATCH 16/52] Move the staticplugin out of ghcide

---
 .../session-loader/Development/IDE/Session.hs |  4 --
 ghcide/src/Development/IDE/Core/Compile.hs    | 33 ---------
 .../hls-tactics-plugin.cabal                  |  1 +
 .../src/Wingman/LanguageServer.hs             | 14 ++--
 .../hls-tactics-plugin/src/Wingman/Plugin.hs  | 12 +---
 .../src/Wingman/StaticPlugin.hs               | 68 +++++++++++++++++++
 6 files changed, 77 insertions(+), 55 deletions(-)
 create mode 100644 plugins/hls-tactics-plugin/src/Wingman/StaticPlugin.hs

diff --git a/ghcide/session-loader/Development/IDE/Session.hs b/ghcide/session-loader/Development/IDE/Session.hs
index 9c8e572068..387fe1b6fb 100644
--- a/ghcide/session-loader/Development/IDE/Session.hs
+++ b/ghcide/session-loader/Development/IDE/Session.hs
@@ -773,7 +773,6 @@ setOptions (ComponentOptions theOpts compRoot _) dflags = do
           setLinkerOptions $
           disableOptimisation $
           setUpTypedHoles $
-          enableQuasiQuotes $
           makeDynFlagsAbsolute compRoot dflags'
     -- initPackages parses the -package flags and
     -- sets up the visibility for each component.
@@ -781,9 +780,6 @@ setOptions (ComponentOptions theOpts compRoot _) dflags = do
     (final_df, _) <- liftIO $ wrapPackageSetupException $ initPackages dflags''
     return (final_df, targets)
 
-enableQuasiQuotes :: DynFlags -> DynFlags
-enableQuasiQuotes = flip xopt_set QuasiQuotes
-
 -- we don't want to generate object code so we compile to bytecode
 -- (HscInterpreted) which implies LinkInMemory
 -- HscInterpreted
diff --git a/ghcide/src/Development/IDE/Core/Compile.hs b/ghcide/src/Development/IDE/Core/Compile.hs
index 391c26b0d6..5d318275d6 100644
--- a/ghcide/src/Development/IDE/Core/Compile.hs
+++ b/ghcide/src/Development/IDE/Core/Compile.hs
@@ -32,7 +32,6 @@ module Development.IDE.Core.Compile
   , setupFinderCache
   , getDocsBatch
   , lookupName
-  , pattern WingmanMetaprogram
   ) where
 
 import           Development.IDE.Core.Preprocessor
@@ -124,7 +123,6 @@ import           Data.Unique
 import           GHC.Fingerprint
 import qualified Language.LSP.Server               as LSP
 import qualified Language.LSP.Types                as LSP
-import Generics.SYB hiding (orElse)
 
 -- | Given a string buffer, return the string (after preprocessing) and the 'ParsedModule'.
 parseModule
@@ -212,37 +210,6 @@ captureSplices dflags k = do
             liftIO $ modifyIORef' var $ awSplicesL %~ ((e, aw') :)
             pure $ f aw'
 
-
-wingmanMetaprogrammingPlugin :: StaticPlugin
-wingmanMetaprogrammingPlugin =
-    StaticPlugin $ PluginWithArgs (defaultPlugin { parsedResultAction = worker })  []
-  where
-    worker :: [CommandLineOption] -> ModSummary -> HsParsedModule -> Hsc HsParsedModule
-    worker _ _ pm = pure $ pm { hpm_module = addWingmanMetaprogrammingSyntax $ hpm_module pm }
-
-
-pattern WingmanMetaprogram :: FastString -> HsExpr p
-pattern WingmanMetaprogram mp
-  <- HsSCC _ (SourceText "wingman-meta-program") (StringLiteral NoSourceText mp)
-      (L _ ( HsVar _ _))
-
-mkWingmanMetaprogram :: SrcSpan -> FastString -> HsExpr GhcPs
-mkWingmanMetaprogram ss mp =
-  HsSCC noExt (SourceText "wingman-meta-program") (StringLiteral NoSourceText mp)
-    $ L ss
-    $ HsVar noExt
-    $ L ss
-    $ mkRdrUnqual
-    $ mkVarOcc "_"
-
-
-addWingmanMetaprogrammingSyntax :: Data a => a -> a
-addWingmanMetaprogrammingSyntax =
-  everywhere $ mkT $ \case
-    L ss (HsSpliceE _ (HsQuasiQuote _ _ (occNameString . rdrNameOcc -> "wingman") _ mp)) ->
-      L ss $ mkWingmanMetaprogram ss mp
-    (x :: LHsExpr GhcPs) -> x
-
 tcRnModule :: HscEnv -> (DynFlags -> DynFlags) -> [Linkable] -> ParsedModule -> IO TcModuleResult
 tcRnModule hsc_env modify_dflags keep_lbls pmod = do
   let ms = pm_mod_summary pmod
diff --git a/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal b/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal
index 1e1f563cbd..5177bb6017 100644
--- a/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal
+++ b/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal
@@ -49,6 +49,7 @@ library
     Wingman.Metaprogramming.Parser
     Wingman.Naming
     Wingman.Plugin
+    Wingman.StaticPlugin
     Wingman.Range
     Wingman.Simplify
     Wingman.Tactics
diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
index dc4becf6ec..5018ffe119 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
@@ -14,9 +14,8 @@ import           Control.Monad.State (State, get, put, evalState)
 import           Control.Monad.Trans.Maybe
 import           Data.Bifunctor (first)
 import           Data.Coerce
+import           Data.Foldable (for_)
 import           Data.Functor ((<&>))
-import           Data.Generics.Aliases (mkQ)
-import           Data.Generics.Schemes (everything)
 import qualified Data.HashMap.Strict as Map
 import           Data.IORef (readIORef)
 import qualified Data.Map as M
@@ -37,11 +36,12 @@ import           Development.IDE.Core.UseStale
 import           Development.IDE.GHC.Compat
 import           Development.IDE.GHC.Error (realSrcSpanToRange)
 import           Development.IDE.GHC.ExactPrint
-import           Development.IDE.Spans.LocalBindings (Bindings, getDefiningBindings)
 import           Development.IDE.Graph (Action, RuleResult, Rules, action)
-import           Development.IDE.Graph.Classes (Typeable, Binary, Hashable, NFData)
+import           Development.IDE.Graph.Classes (Binary, Hashable, NFData)
+import           Development.IDE.Spans.LocalBindings (Bindings, getDefiningBindings)
 import qualified FastString
 import           GHC.Generics (Generic)
+import           Generics.SYB hiding (Generic)
 import           GhcPlugins (tupleDataCon, consDataCon, substTyAddInScope, ExternalPackageState, HscEnv (hsc_EPS), liftIO, unpackFS)
 import qualified Ide.Plugin.Config as Plugin
 import           Ide.Plugin.Properties
@@ -60,12 +60,10 @@ import           Wingman.GHC
 import           Wingman.Judgements
 import           Wingman.Judgements.SYB (everythingContaining)
 import           Wingman.Judgements.Theta
+import           Wingman.Metaprogramming.Parser (attempt_it)
 import           Wingman.Range
+import           Wingman.StaticPlugin (pattern WingmanMetaprogram)
 import           Wingman.Types
-import Generics.SYB hiding (Generic)
-import Development.IDE.Core.Compile (pattern WingmanMetaprogram)
-import Data.Foldable (for_)
-import Wingman.Metaprogramming.Parser (attempt_it)
 
 
 tacticDesc :: T.Text -> T.Text
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs b/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs
index 54c92fc07f..3750844831 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs
@@ -20,7 +20,6 @@ import           Development.IDE.Core.Shake (IdeState (..))
 import           Development.IDE.Core.UseStale (Tracked, TrackedStale(..), unTrack, mapAgeFrom, unsafeMkCurrent)
 import           Development.IDE.GHC.Compat
 import           Development.IDE.GHC.ExactPrint
-import           GHC.LanguageExtensions.Type (Extension(EmptyCase))
 import           Generics.SYB.GHC
 import           Ide.Types
 import           Language.LSP.Server
@@ -36,6 +35,7 @@ import           Wingman.LanguageServer
 import           Wingman.LanguageServer.TacticProviders
 import           Wingman.Machinery (scoreSolution)
 import           Wingman.Range
+import           Wingman.StaticPlugin
 import           Wingman.Tactics
 import           Wingman.Types
 
@@ -63,18 +63,10 @@ descriptor plId = (defaultPluginDescriptor plId)
   , pluginRules = wingmanRules plId
   , pluginConfigDescriptor =
       defaultConfigDescriptor {configCustomConfig = mkCustomConfig properties}
-  , pluginModifyDynflags = allowEmptyCaseButWithWarning
+  , pluginModifyDynflags = staticPlugin
   }
 
 
--- | Wingman wants to support destructing of empty cases, but these are a parse
--- error by default. So we want to enable 'EmptyCase', but then that leads to
--- silent errors without 'Opt_WarnIncompletePatterns'.
-allowEmptyCaseButWithWarning :: DynFlags -> DynFlags
-allowEmptyCaseButWithWarning =
-  flip xopt_set EmptyCase . flip wopt_set Opt_WarnIncompletePatterns
-
-
 codeActionProvider :: PluginMethodHandler IdeState TextDocumentCodeAction
 codeActionProvider state plId (CodeActionParams _ _ (TextDocumentIdentifier uri) (unsafeMkCurrent -> range) _ctx)
   | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do
diff --git a/plugins/hls-tactics-plugin/src/Wingman/StaticPlugin.hs b/plugins/hls-tactics-plugin/src/Wingman/StaticPlugin.hs
new file mode 100644
index 0000000000..08bda9fceb
--- /dev/null
+++ b/plugins/hls-tactics-plugin/src/Wingman/StaticPlugin.hs
@@ -0,0 +1,68 @@
+module Wingman.StaticPlugin
+  ( staticPlugin
+  , pattern WingmanMetaprogram
+  ) where
+
+import           Data.Data
+import           Development.IDE.GHC.Compat
+import           GHC.LanguageExtensions.Type (Extension(EmptyCase, QuasiQuotes))
+import           Generics.SYB
+import           GhcPlugins hiding ((<>))
+
+
+staticPlugin :: DynFlags -> DynFlags
+staticPlugin df
+  = allowEmptyCaseButWithWarning
+  $ enableQuasiQuotes
+  $ df
+    { staticPlugins = staticPlugins df <> [metaprogrammingPlugin] }
+
+
+pattern MetaprogramSourceText :: SourceText
+pattern MetaprogramSourceText = SourceText "wingman-meta-program"
+
+
+
+pattern WingmanMetaprogram :: FastString -> HsExpr p
+pattern WingmanMetaprogram mp
+  <- HsSCC _ MetaprogramSourceText (StringLiteral NoSourceText mp)
+      (L _ ( HsVar _ _))
+
+
+enableQuasiQuotes :: DynFlags -> DynFlags
+enableQuasiQuotes = flip xopt_set QuasiQuotes
+
+
+-- | Wingman wants to support destructing of empty cases, but these are a parse
+-- error by default. So we want to enable 'EmptyCase', but then that leads to
+-- silent errors without 'Opt_WarnIncompletePatterns'.
+allowEmptyCaseButWithWarning :: DynFlags -> DynFlags
+allowEmptyCaseButWithWarning =
+  flip xopt_set EmptyCase . flip wopt_set Opt_WarnIncompletePatterns
+
+
+metaprogrammingPlugin :: StaticPlugin
+metaprogrammingPlugin =
+    StaticPlugin $ PluginWithArgs (defaultPlugin { parsedResultAction = worker })  []
+  where
+    worker :: [CommandLineOption] -> ModSummary -> HsParsedModule -> Hsc HsParsedModule
+    worker _ _ pm = pure $ pm { hpm_module = addMetaprogrammingSyntax $ hpm_module pm }
+
+
+mkMetaprogram :: SrcSpan -> FastString -> HsExpr GhcPs
+mkMetaprogram ss mp =
+  HsSCC noExt MetaprogramSourceText (StringLiteral NoSourceText mp)
+    $ L ss
+    $ HsVar noExt
+    $ L ss
+    $ mkRdrUnqual
+    $ mkVarOcc "_"
+
+
+addMetaprogrammingSyntax :: Data a => a -> a
+addMetaprogrammingSyntax =
+  everywhere $ mkT $ \case
+    L ss (HsSpliceE _ (HsQuasiQuote _ _ (occNameString . rdrNameOcc -> "wingman") _ mp)) ->
+      L ss $ mkMetaprogram ss mp
+    (x :: LHsExpr GhcPs) -> x
+

From b586b8573fb75031104a3dd0c73325acf4321277 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Tue, 27 Apr 2021 10:14:32 -0700
Subject: [PATCH 17/52] Add application, add split, rename split to ctor

---
 .../src/Wingman/Metaprogramming/Lexer.hs      |  3 +++
 .../src/Wingman/Metaprogramming/Parser.hs     | 19 ++++++++++++++-----
 .../hls-tactics-plugin/src/Wingman/Tactics.hs |  3 +++
 3 files changed, 20 insertions(+), 5 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Lexer.hs b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Lexer.hs
index 393e077c01..fb396029a4 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Lexer.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Lexer.hs
@@ -45,6 +45,9 @@ brackets = P.between (symbol "[") (symbol "]")
 braces :: Parser a -> Parser a
 braces = P.between (symbol "{") (symbol "}")
 
+parens :: Parser a -> Parser a
+parens = P.between (symbol "(") (symbol ")")
+
 identifier :: Text -> Parser ()
 identifier i = lexeme (P.string i *> P.notFollowedBy ichar)
 
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
index 025ebc5687..7832d2f311 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
@@ -29,10 +29,13 @@ unary_occ name tac = tac <$> (identifier name *> variable)
 variadic_occ :: T.Text -> ([OccName] -> TacticsM ()) -> Parser (TacticsM ())
 variadic_occ name tac = tac <$> (identifier name *> P.many variable)
 
-
-tactic :: Parser (TacticsM ())
-tactic = flip P.makeExprParser operators $  P.choice
+oneTactic :: Parser (TacticsM ())
+oneTactic =
+  P.choice
     [ braces tactic
+      -- TODO(sandy): lean uses braces for control flow, but i always forget
+      -- and want to use parens. is there a semantic difference?
+    , parens tactic
     , nullary   "assumption" assumption
     , unary_occ "assume" assume
     , variadic_occ   "intros" $ \case
@@ -42,19 +45,25 @@ tactic = flip P.makeExprParser operators $  P.choice
     , nullary   "destruct_all" destructAll
     , unary_occ "destruct" $ useNameFromHypothesis destruct
     , unary_occ "homo" $ useNameFromHypothesis homo
+    , nullary   "application" application
     , unary_occ "apply" $ useNameFromHypothesis apply
-    , unary_occ "split" userSplit
+    , nullary   "split" split
+    , unary_occ "ctor" userSplit
     , nullary   "obvious" obvious
     , nullary   "auto" auto
-    , R.try <$> (keyword "try" *> tactic)
     ]
 
+
+tactic :: Parser (TacticsM ())
+tactic = flip P.makeExprParser operators oneTactic
+
 bindOne :: TacticsM a -> TacticsM a -> TacticsM a
 bindOne t t1 = t R.<@> [t1]
 
 operators :: [[P.Operator Parser (TacticsM ())]]
 operators =
     [ [ P.Prefix (symbol "*" $> R.many_) ]
+    , [ P.Prefix (symbol "try" $> R.try) ]
     , [ P.InfixR (symbol "|" $> (R.<%>) )]
     , [ P.InfixL (symbol ";" $> (>>))
       , P.InfixL (symbol "," $> bindOne)
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs
index 0313c1707b..873c4b5792 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs
@@ -223,6 +223,9 @@ apply hi = requireConcreteHole $ tracing ("apply' " <> show (hi_name hi)) $ do
         & #syn_used_vals %~ S.insert func
         & #syn_val       %~ mkApply func . fmap unLoc
 
+application :: TacticsM ()
+application = overFunctions apply
+
 
 ------------------------------------------------------------------------------
 -- | Choose between each of the goal's data constructors.

From 74d4e6482d04eb435f6bcb2b6ce1c0cc83e0d9f4 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Tue, 27 Apr 2021 12:04:46 -0700
Subject: [PATCH 18/52] Tidy parser

---
 .../src/Wingman/Metaprogramming/Parser.hs     | 22 ++++++-------------
 1 file changed, 7 insertions(+), 15 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
index 7832d2f311..8243c6e117 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
@@ -8,8 +8,8 @@ module Wingman.Metaprogramming.Parser where
 
 import qualified Control.Monad.Combinators.Expr as P
 import           Data.Functor
-import           Development.IDE.GHC.Compat (alphaTyVars, LHsExpr, GhcPs)
-import           GhcPlugins (mkTyVarTy)
+import qualified Data.Text as T
+import           Development.IDE.GHC.Compat (LHsExpr, GhcPs)
 import qualified Refinery.Tactic as R
 import qualified Text.Megaparsec as P
 import           Wingman.Auto
@@ -17,7 +17,6 @@ import           Wingman.LanguageServer.TacticProviders (useNameFromHypothesis)
 import           Wingman.Metaprogramming.Lexer
 import           Wingman.Tactics
 import           Wingman.Types
-import qualified Data.Text as T
 
 
 nullary :: T.Text -> TacticsM () -> Parser (TacticsM ())
@@ -62,25 +61,18 @@ bindOne t t1 = t R.<@> [t1]
 
 operators :: [[P.Operator Parser (TacticsM ())]]
 operators =
-    [ [ P.Prefix (symbol "*" $> R.many_) ]
+    [ [ P.Prefix (symbol "*"   $> R.many_) ]
     , [ P.Prefix (symbol "try" $> R.try) ]
-    , [ P.InfixR (symbol "|" $> (R.<%>) )]
-    , [ P.InfixL (symbol ";" $> (>>))
-      , P.InfixL (symbol "," $> bindOne)
+    , [ P.InfixR (symbol "|"   $> (R.<%>) )]
+    , [ P.InfixL (symbol ";"   $> (>>))
+      , P.InfixL (symbol ","   $> bindOne)
       ]
     ]
 
 
-skolems :: [Type]
-skolems = fmap mkTyVarTy alphaTyVars
-
-a_skolem, b_skolem, c_skolem :: Type
-(a_skolem : b_skolem : c_skolem : _) = skolems
-
-
 attempt_it :: Context -> Judgement -> String -> Either String (LHsExpr GhcPs)
 attempt_it ctx jdg program =
-  case P.runParser (sc *> tactic <* P.eof) "<splice>" (T.pack program) of
+  case P.runParser (sc *> tactic <* P.eof) "<splice>" $ T.pack program of
     Left peb -> Left $ P.errorBundlePretty peb
     Right tt -> do
       case runTactic

From f488be81443324b75dc5146742b2bf7fad48b8dd Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Tue, 27 Apr 2021 12:17:58 -0700
Subject: [PATCH 19/52] Track remaining subgoals for interactive proofstate

---
 plugins/hls-tactics-plugin/src/Wingman/Machinery.hs | 7 ++++---
 plugins/hls-tactics-plugin/src/Wingman/Types.hs     | 1 +
 2 files changed, 5 insertions(+), 3 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs b/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs
index 34dcb449c6..8c1afce251 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs
@@ -82,11 +82,12 @@ runTactic ctx jdg t =
               flip sortBy solns $ comparing $ \(ext, (_, holes)) ->
                 Down $ scoreSolution ext jdg holes
         case sorted of
-          ((syn, _) : _) ->
+          ((syn, (_, subgoals)) : _) ->
             Right $
               RunTacticResults
-                { rtr_trace = syn_trace syn
-                , rtr_extract = simplify $ syn_val syn
+                { rtr_trace    = syn_trace syn
+                , rtr_extract  = simplify $ syn_val syn
+                , rtr_subgoals = subgoals
                 , rtr_other_solns = reverse . fmap fst $ sorted
                 , rtr_jdg = jdg
                 , rtr_ctx = ctx
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Types.hs b/plugins/hls-tactics-plugin/src/Wingman/Types.hs
index 1494336562..37b20d13e2 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Types.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Types.hs
@@ -476,6 +476,7 @@ rose a rs = Rose $ Node a $ coerce rs
 data RunTacticResults = RunTacticResults
   { rtr_trace       :: Trace
   , rtr_extract     :: LHsExpr GhcPs
+  , rtr_subgoals    :: [Judgement]
   , rtr_other_solns :: [Synthesized (LHsExpr GhcPs)]
   , rtr_jdg         :: Judgement
   , rtr_ctx         :: Context

From 735a28da2b11dab7b8612a9e4b2d21ff3b9d20ae Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Tue, 27 Apr 2021 13:10:11 -0700
Subject: [PATCH 20/52] Add a pretty printer of the proofstate

---
 .../hls-tactics-plugin.cabal                  |  2 +
 .../src/Wingman/LanguageServer.hs             |  2 +-
 .../src/Wingman/Metaprogramming/Parser.hs     |  5 +-
 .../src/Wingman/Metaprogramming/ProofState.hs | 52 +++++++++++++++++++
 4 files changed, 58 insertions(+), 3 deletions(-)
 create mode 100644 plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/ProofState.hs

diff --git a/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal b/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal
index 5177bb6017..5910e294e8 100644
--- a/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal
+++ b/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal
@@ -47,6 +47,7 @@ library
     Wingman.Machinery
     Wingman.Metaprogramming.Lexer
     Wingman.Metaprogramming.Parser
+    Wingman.Metaprogramming.ProofState
     Wingman.Naming
     Wingman.Plugin
     Wingman.StaticPlugin
@@ -91,6 +92,7 @@ library
     , hyphenation
     , megaparsec ^>=9
     , parser-combinators
+    , prettyprinter
 
   default-language:   Haskell2010
   default-extensions:
diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
index 5018ffe119..549c8df0e9 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
@@ -221,7 +221,7 @@ judgementForHole state nfp range cfg = do
 
       let mps = getAllMetaprograms $ tcg_binds $ untrackedStaleValue tcg
       for_ mps $ \prog ->
-        liftIO $ putStrLn $ either id show $ attempt_it ctx jdg prog
+        liftIO $ putStrLn $ either id id $ attempt_it ctx jdg prog
 
       dflags <- getIdeDynflags state nfp
       pure (fmap realSrcSpanToRange new_rss, jdg, ctx, dflags)
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
index 8243c6e117..9a60c8b2cd 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
@@ -17,6 +17,7 @@ import           Wingman.LanguageServer.TacticProviders (useNameFromHypothesis)
 import           Wingman.Metaprogramming.Lexer
 import           Wingman.Tactics
 import           Wingman.Types
+import Wingman.Metaprogramming.ProofState (proofState, layout)
 
 
 nullary :: T.Text -> TacticsM () -> Parser (TacticsM ())
@@ -70,7 +71,7 @@ operators =
     ]
 
 
-attempt_it :: Context -> Judgement -> String -> Either String (LHsExpr GhcPs)
+attempt_it :: Context -> Judgement -> String -> Either String String
 attempt_it ctx jdg program =
   case P.runParser (sc *> tactic <* P.eof) "<splice>" $ T.pack program of
     Left peb -> Left $ P.errorBundlePretty peb
@@ -81,5 +82,5 @@ attempt_it ctx jdg program =
              tt
         of
           Left tes -> Left $ show tes
-          Right rtr -> Right $ rtr_extract rtr
+          Right rtr -> Right $ layout $ proofState rtr
 
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/ProofState.hs b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/ProofState.hs
new file mode 100644
index 0000000000..946a061ef1
--- /dev/null
+++ b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/ProofState.hs
@@ -0,0 +1,52 @@
+{-# LANGUAGE NamedFieldPuns    #-}
+{-# LANGUAGE OverloadedStrings #-}
+
+module Wingman.Metaprogramming.ProofState where
+
+import Data.Text.Prettyprint.Doc
+import Wingman.Types
+import Data.Bool (bool)
+import Wingman.Judgements (jLocalHypothesis, isDisallowed)
+import Data.Functor ((<&>))
+import Data.Text.Prettyprint.Doc.Render.String (renderString)
+
+layout :: Doc ann -> String
+layout = renderString . layoutPretty (LayoutOptions $ AvailablePerLine 80 0.6)
+
+proofState :: RunTacticResults -> Doc ann
+proofState RunTacticResults{rtr_subgoals} =
+  vsep
+    $ (countFinished "goals accomplished" "goal" $ length rtr_subgoals)
+    : fmap prettySubgoal rtr_subgoals
+
+
+prettySubgoal :: Judgement -> Doc ann
+prettySubgoal jdg =
+  vsep
+    [ mempty
+    , prettyHypothesis $ jLocalHypothesis jdg
+    , "⊢" <+> prettyType (_jGoal jdg)
+    ]
+
+
+prettyHypothesis :: Hypothesis CType -> Doc ann
+prettyHypothesis hy =
+  vsep $ filter (not . isDisallowed . hi_provenance) (unHypothesis hy) <&> \hi ->
+    prettyHyInfo hi
+
+prettyHyInfo :: HyInfo CType -> Doc ann
+prettyHyInfo hi = viaShow (hi_name hi) <+> "::" <+> prettyType (hi_type hi)
+
+
+prettyType :: CType -> Doc ann
+prettyType (CType ty) = viaShow ty
+
+
+countFinished :: Doc ann -> Doc ann -> Int -> Doc ann
+countFinished finished _ 0 = finished
+countFinished _ thing n    = count thing n
+
+count :: Doc ann -> Int -> Doc ann
+count thing n =
+  pretty n <+> thing <> bool "" "s" (n /= 1)
+

From d18cbf559daf718e1c2da56d9fd3be487bb6e3c3 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Tue, 27 Apr 2021 13:12:58 -0700
Subject: [PATCH 21/52] Add sorry

---
 .../src/Wingman/Metaprogramming/Parser.hs                  | 2 +-
 plugins/hls-tactics-plugin/src/Wingman/Tactics.hs          | 7 +++++++
 2 files changed, 8 insertions(+), 1 deletion(-)

diff --git a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
index 9a60c8b2cd..24c4bc255f 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
@@ -9,7 +9,6 @@ module Wingman.Metaprogramming.Parser where
 import qualified Control.Monad.Combinators.Expr as P
 import           Data.Functor
 import qualified Data.Text as T
-import           Development.IDE.GHC.Compat (LHsExpr, GhcPs)
 import qualified Refinery.Tactic as R
 import qualified Text.Megaparsec as P
 import           Wingman.Auto
@@ -51,6 +50,7 @@ oneTactic =
     , unary_occ "ctor" userSplit
     , nullary   "obvious" obvious
     , nullary   "auto" auto
+    , nullary   "sorry" sorry
     ]
 
 
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs
index 873c4b5792..aa722ff003 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs
@@ -35,6 +35,7 @@ import           Wingman.Judgements
 import           Wingman.Machinery
 import           Wingman.Naming
 import           Wingman.Types
+import OccName (mkVarOcc)
 
 
 ------------------------------------------------------------------------------
@@ -275,6 +276,12 @@ obvious = tracing "obvious" $ do
   pruning split $ bool (Just NoProgress) Nothing . null
 
 
+------------------------------------------------------------------------------
+-- | Sorry leaves a hole in its extract
+sorry :: TacticsM ()
+sorry = rule $ const $ pure $ (pure $ noLoc $ var' $ mkVarOcc "_")
+
+
 ------------------------------------------------------------------------------
 -- | Allow the given tactic to proceed if and only if it introduces holes that
 -- have a different goal than current goal.

From da1bec0c54bfc00a3303dde5a428e94f714d0c84 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Tue, 27 Apr 2021 14:05:19 -0700
Subject: [PATCH 22/52] Attach proof state as a hover action

---
 .../hls-tactics-plugin.cabal                  |  1 +
 .../src/Wingman/LanguageServer.hs             |  4 -
 .../src/Wingman/LanguageServer/Metaprogram.hs | 94 +++++++++++++++++++
 .../src/Wingman/Metaprogramming/ProofState.hs | 15 ++-
 .../hls-tactics-plugin/src/Wingman/Plugin.hs  |  2 +
 5 files changed, 109 insertions(+), 7 deletions(-)
 create mode 100644 plugins/hls-tactics-plugin/src/Wingman/LanguageServer/Metaprogram.hs

diff --git a/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal b/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal
index 5910e294e8..4e04c8fd6f 100644
--- a/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal
+++ b/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal
@@ -44,6 +44,7 @@ library
     Wingman.KnownStrategies.QuickCheck
     Wingman.LanguageServer
     Wingman.LanguageServer.TacticProviders
+    Wingman.LanguageServer.Metaprogram
     Wingman.Machinery
     Wingman.Metaprogramming.Lexer
     Wingman.Metaprogramming.Parser
diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
index 549c8df0e9..0e142b72fa 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
@@ -219,10 +219,6 @@ judgementForHole state nfp range cfg = do
 
       (jdg, ctx) <- liftMaybe $ mkJudgementAndContext cfg g binds new_rss tcg eps kt
 
-      let mps = getAllMetaprograms $ tcg_binds $ untrackedStaleValue tcg
-      for_ mps $ \prog ->
-        liftIO $ putStrLn $ either id id $ attempt_it ctx jdg prog
-
       dflags <- getIdeDynflags state nfp
       pure (fmap realSrcSpanToRange new_rss, jdg, ctx, dflags)
 
diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/Metaprogram.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/Metaprogram.hs
new file mode 100644
index 0000000000..7aadbeaebc
--- /dev/null
+++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/Metaprogram.hs
@@ -0,0 +1,94 @@
+{-# LANGUAGE DuplicateRecordFields #-}
+{-# LANGUAGE OverloadedStrings     #-}
+
+{-# LANGUAGE NoMonoLocalBinds  #-}
+
+module Wingman.LanguageServer.Metaprogram (hoverProvider) where
+
+import           Control.Applicative (empty)
+import           Control.Monad
+import           Control.Monad.Trans
+import           Control.Monad.Trans.Maybe
+import           Data.Generics.Aliases (mkQ, GenericQ)
+import           Data.Generics.Schemes (everything)
+import           Data.List (find)
+import           Data.Maybe
+import           Data.Monoid
+import qualified Data.Text as T
+import           Data.Traversable
+import           Development.IDE (positionToRealSrcLoc)
+import           Development.IDE (realSrcSpanToRange)
+import           Development.IDE.Core.RuleTypes
+import           Development.IDE.Core.Shake (IdeState (..))
+import           Development.IDE.Core.UseStale
+import           Development.IDE.GHC.Compat
+import           GhcPlugins (unpackFS, containsSpan, realSrcLocSpan)
+import           Ide.Types
+import           Language.LSP.Types
+import           Prelude hiding (span)
+import           Prelude hiding (span)
+import           TcRnTypes (tcg_binds)
+import           Wingman.GHC
+import           Wingman.LanguageServer
+import           Wingman.Metaprogramming.Parser (attempt_it)
+import           Wingman.StaticPlugin (pattern WingmanMetaprogram)
+
+
+------------------------------------------------------------------------------
+-- | Provide the "empty case completion" code lens
+hoverProvider :: PluginMethodHandler IdeState TextDocumentHover
+hoverProvider state plId (HoverParams (TextDocumentIdentifier uri) pos _)
+  | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do
+      let loc = positionToRealSrcLoc nfp pos
+
+      cfg <- getTacticConfig plId
+      liftIO $ fromMaybeT (Right Nothing) $ do
+        -- guard $ hasFeature FeatureEmptyCase $ cfg_feature_set cfg
+
+        holes <- emptyCaseScrutinees state nfp
+
+        fmap (Right . Just) $
+          case (find (flip containsSpan (realSrcLocSpan loc) . unTrack . fst) holes) of
+            Just (trss, program) -> do
+              let tr_range = fmap realSrcSpanToRange trss
+              (_, jdg, ctx, _) <- judgementForHole state nfp tr_range cfg
+              pure $ Hover
+                { _contents = HoverContents $ MarkupContent MkPlainText $ either T.pack T.pack $ attempt_it ctx jdg $ T.unpack program
+                , _range = Just $ unTrack tr_range
+                }
+            Nothing -> empty
+hoverProvider _ _ _ = pure $ Right Nothing
+
+
+fromMaybeT :: Functor m => a -> MaybeT m a -> m a
+fromMaybeT def = fmap (fromMaybe def) . runMaybeT
+
+
+------------------------------------------------------------------------------
+-- | Find the last typechecked module, and find the most specific span, as well
+-- as the judgement at the given range.
+emptyCaseScrutinees
+    :: IdeState
+    -> NormalizedFilePath
+    -> MaybeT IO [(Tracked 'Current RealSrcSpan, T.Text)]
+emptyCaseScrutinees state nfp = do
+    let stale a = runStaleIde "emptyCaseScrutinees" state nfp a
+
+    TrackedStale tcg tcg_map <- fmap (fmap tmrTypechecked) $ stale TypeCheck
+
+    let scrutinees = traverse (emptyCaseQ . tcg_binds) tcg
+    for scrutinees $ \aged@(unTrack -> (ss, program)) -> do
+      case ss of
+        RealSrcSpan r   -> do
+          rss' <- liftMaybe $ mapAgeTo tcg_map $ unsafeCopyAge aged r
+          pure (rss', program)
+        UnhelpfulSpan _ -> empty
+
+
+------------------------------------------------------------------------------
+-- | Get the 'SrcSpan' and scrutinee of every empty case.
+emptyCaseQ :: GenericQ [(SrcSpan, T.Text)]
+emptyCaseQ = everything (<>) $ mkQ mempty $ \case
+  L new_span (WingmanMetaprogram program) -> pure (new_span, T.pack $ unpackFS $ program)
+  (_ :: LHsExpr GhcTc) -> mempty
+
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/ProofState.hs b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/ProofState.hs
index 946a061ef1..6ede7ebdbc 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/ProofState.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/ProofState.hs
@@ -9,14 +9,23 @@ import Data.Bool (bool)
 import Wingman.Judgements (jLocalHypothesis, isDisallowed)
 import Data.Functor ((<&>))
 import Data.Text.Prettyprint.Doc.Render.String (renderString)
+import qualified Data.Text as T
+import Language.LSP.Types (sectionSeparator)
+
+forceMarkdownNewlines :: String -> String
+forceMarkdownNewlines = unlines . fmap (<> "  ") . lines
 
 layout :: Doc ann -> String
-layout = renderString . layoutPretty (LayoutOptions $ AvailablePerLine 80 0.6)
+layout
+  = flip mappend (T.unpack sectionSeparator)
+  . forceMarkdownNewlines
+  . renderString
+  . layoutPretty (LayoutOptions $ AvailablePerLine 80 0.6)
 
 proofState :: RunTacticResults -> Doc ann
-proofState RunTacticResults{rtr_subgoals} =
+proofState RunTacticResults{rtr_extract, rtr_subgoals} =
   vsep
-    $ (countFinished "goals accomplished" "goal" $ length rtr_subgoals)
+    $ (countFinished (viaShow rtr_extract) "goal" $ length rtr_subgoals)
     : fmap prettySubgoal rtr_subgoals
 
 
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs b/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs
index 3750844831..12d29a0996 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs
@@ -38,6 +38,7 @@ import           Wingman.Range
 import           Wingman.StaticPlugin
 import           Wingman.Tactics
 import           Wingman.Types
+import Wingman.LanguageServer.Metaprogram (hoverProvider)
 
 
 descriptor :: PluginId -> PluginDescriptor IdeState
@@ -59,6 +60,7 @@ descriptor plId = (defaultPluginDescriptor plId)
   , pluginHandlers = mconcat
       [ mkPluginHandler STextDocumentCodeAction codeActionProvider
       , mkPluginHandler STextDocumentCodeLens codeLensProvider
+      , mkPluginHandler STextDocumentHover hoverProvider
       ]
   , pluginRules = wingmanRules plId
   , pluginConfigDescriptor =

From ce85e9f6d0e05f796fc31d1c6b514f670ea9db9d Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Tue, 27 Apr 2021 17:18:51 -0700
Subject: [PATCH 23/52] Much prettier proof state

---
 .../src/Wingman/Metaprogramming/ProofState.hs | 98 ++++++++++++++-----
 1 file changed, 73 insertions(+), 25 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/ProofState.hs b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/ProofState.hs
index 6ede7ebdbc..9c3e736b93 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/ProofState.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/ProofState.hs
@@ -3,59 +3,107 @@
 
 module Wingman.Metaprogramming.ProofState where
 
-import Data.Text.Prettyprint.Doc
-import Wingman.Types
-import Data.Bool (bool)
-import Wingman.Judgements (jLocalHypothesis, isDisallowed)
-import Data.Functor ((<&>))
-import Data.Text.Prettyprint.Doc.Render.String (renderString)
+import           Data.Bool (bool)
+import           Data.Functor ((<&>))
 import qualified Data.Text as T
-import Language.LSP.Types (sectionSeparator)
+import           Data.Text.Prettyprint.Doc
+import           Data.Text.Prettyprint.Doc.Internal (textSpaces)
+import           Data.Text.Prettyprint.Doc.Render.Util.Panic
+import           Language.LSP.Types (sectionSeparator)
+import           Wingman.Judgements (jHypothesis)
+import           Wingman.Types
+
+renderSimplyDecorated
+    :: Monoid out
+    => (T.Text -> out) -- ^ Render plain 'Text'
+    -> (ann -> out)  -- ^ How to render an annotation
+    -> (ann -> out)  -- ^ How to render the removed annotation
+    -> SimpleDocStream ann
+    -> out
+renderSimplyDecorated text push pop = go []
+  where
+    go _           SFail               = panicUncaughtFail
+    go []          SEmpty              = mempty
+    go (_:_)       SEmpty              = panicInputNotFullyConsumed
+    go stack       (SChar c rest)      = text (T.singleton c) <> go stack rest
+    go stack       (SText _l t rest)   = text t <> go stack rest
+    go stack       (SLine i rest)      = text (T.singleton '\n') <> text (textSpaces i) <> go stack rest
+    go stack       (SAnnPush ann rest) = push ann <> go (ann : stack) rest
+    go (ann:stack) (SAnnPop rest)      = pop ann <> go stack rest
+    go []          SAnnPop{}           = panicUnpairedPop
+{-# INLINE renderSimplyDecorated #-}
+
+
+data Ann
+  = Goal
+  | Hypoth
+  | Status
+  deriving (Eq, Ord, Show, Enum, Bounded)
 
 forceMarkdownNewlines :: String -> String
 forceMarkdownNewlines = unlines . fmap (<> "  ") . lines
 
-layout :: Doc ann -> String
+layout :: Doc Ann -> String
 layout
-  = flip mappend (T.unpack sectionSeparator)
-  . forceMarkdownNewlines
-  . renderString
+  = forceMarkdownNewlines
+  . T.unpack
+  . renderSimplyDecorated id
+    renderAnn
+    renderUnann
   . layoutPretty (LayoutOptions $ AvailablePerLine 80 0.6)
 
-proofState :: RunTacticResults -> Doc ann
-proofState RunTacticResults{rtr_extract, rtr_subgoals} =
+renderAnn :: Ann -> T.Text
+renderAnn Goal = "<span style='color:#ef4026;'>"
+renderAnn Hypoth = "```haskell\n"
+renderAnn Status = "<span style='color:#6495ED;'>"
+
+renderUnann :: Ann -> T.Text
+renderUnann Goal = "</span>"
+renderUnann Hypoth = "\n```\n"
+renderUnann Status = "</span>"
+
+proofState :: RunTacticResults -> Doc Ann
+proofState RunTacticResults{rtr_subgoals} =
   vsep
-    $ (countFinished (viaShow rtr_extract) "goal" $ length rtr_subgoals)
+    $ ( annotate Status
+      . countFinished "goals accomplished 🎉" "goal"
+      $ length rtr_subgoals
+      )
+    : pretty sectionSeparator
     : fmap prettySubgoal rtr_subgoals
 
 
-prettySubgoal :: Judgement -> Doc ann
+prettySubgoal :: Judgement -> Doc Ann
 prettySubgoal jdg =
-  vsep
-    [ mempty
-    , prettyHypothesis $ jLocalHypothesis jdg
-    , "⊢" <+> prettyType (_jGoal jdg)
+  vsep $
+    [ mempty | has_hy] <>
+    [ annotate Hypoth $ prettyHypothesis hy | has_hy] <>
+    [ "⊢" <+> annotate Goal (prettyType (_jGoal jdg))
+    , pretty sectionSeparator
     ]
+  where
+    hy = jHypothesis jdg
+    has_hy = not $ null $ unHypothesis hy
 
 
-prettyHypothesis :: Hypothesis CType -> Doc ann
+prettyHypothesis :: Hypothesis CType -> Doc Ann
 prettyHypothesis hy =
-  vsep $ filter (not . isDisallowed . hi_provenance) (unHypothesis hy) <&> \hi ->
+  vsep $ unHypothesis hy <&> \hi ->
     prettyHyInfo hi
 
-prettyHyInfo :: HyInfo CType -> Doc ann
+prettyHyInfo :: HyInfo CType -> Doc Ann
 prettyHyInfo hi = viaShow (hi_name hi) <+> "::" <+> prettyType (hi_type hi)
 
 
-prettyType :: CType -> Doc ann
+prettyType :: CType -> Doc Ann
 prettyType (CType ty) = viaShow ty
 
 
-countFinished :: Doc ann -> Doc ann -> Int -> Doc ann
+countFinished :: Doc Ann -> Doc Ann -> Int -> Doc Ann
 countFinished finished _ 0 = finished
 countFinished _ thing n    = count thing n
 
-count :: Doc ann -> Int -> Doc ann
+count :: Doc Ann -> Int -> Doc Ann
 count thing n =
   pretty n <+> thing <> bool "" "s" (n /= 1)
 

From f8abb95313b844156e0bc2ac98620a2244fb719b Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Tue, 27 Apr 2021 17:27:41 -0700
Subject: [PATCH 24/52] Tidy and tag hover as markdown

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

diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
index 0e142b72fa..1e9b54cd97 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
@@ -14,7 +14,6 @@ import           Control.Monad.State (State, get, put, evalState)
 import           Control.Monad.Trans.Maybe
 import           Data.Bifunctor (first)
 import           Data.Coerce
-import           Data.Foldable (for_)
 import           Data.Functor ((<&>))
 import qualified Data.HashMap.Strict as Map
 import           Data.IORef (readIORef)
@@ -60,7 +59,6 @@ import           Wingman.GHC
 import           Wingman.Judgements
 import           Wingman.Judgements.SYB (everythingContaining)
 import           Wingman.Judgements.Theta
-import           Wingman.Metaprogramming.Parser (attempt_it)
 import           Wingman.Range
 import           Wingman.StaticPlugin (pattern WingmanMetaprogram)
 import           Wingman.Types
diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/Metaprogram.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/Metaprogram.hs
index 7aadbeaebc..00c60bc579 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/Metaprogram.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/Metaprogram.hs
@@ -53,7 +53,11 @@ hoverProvider state plId (HoverParams (TextDocumentIdentifier uri) pos _)
               let tr_range = fmap realSrcSpanToRange trss
               (_, jdg, ctx, _) <- judgementForHole state nfp tr_range cfg
               pure $ Hover
-                { _contents = HoverContents $ MarkupContent MkPlainText $ either T.pack T.pack $ attempt_it ctx jdg $ T.unpack program
+                { _contents = HoverContents
+                            $ MarkupContent MkMarkdown
+                            $ either T.pack T.pack
+                            $ attempt_it ctx jdg
+                            $ T.unpack program
                 , _range = Just $ unTrack tr_range
                 }
             Nothing -> empty

From 3e3bff5aec3aca8f11e6eccb0366fbda5743ba15 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Tue, 27 Apr 2021 18:15:27 -0700
Subject: [PATCH 25/52] Be smarter about where we run the dflags endo

---
 ghcide/src/Development/IDE/Core/Compile.hs | 21 ++++++++----------
 ghcide/src/Development/IDE/Core/Rules.hs   | 25 ++++++++++------------
 2 files changed, 20 insertions(+), 26 deletions(-)

diff --git a/ghcide/src/Development/IDE/Core/Compile.hs b/ghcide/src/Development/IDE/Core/Compile.hs
index 5d318275d6..64d710f8a9 100644
--- a/ghcide/src/Development/IDE/Core/Compile.hs
+++ b/ghcide/src/Development/IDE/Core/Compile.hs
@@ -128,14 +128,13 @@ import qualified Language.LSP.Types                as LSP
 parseModule
     :: IdeOptions
     -> HscEnv
-    -> (DynFlags -> DynFlags)
     -> FilePath
     -> ModSummary
     -> IO (IdeResult ParsedModule)
-parseModule IdeOptions{..} env modifyDynFlags filename ms =
+parseModule IdeOptions{..} env filename ms =
     fmap (either (, Nothing) id) $
     runExceptT $ do
-        (diag, modu) <- parseFileContents env modifyDynFlags optPreprocessor filename ms
+        (diag, modu) <- parseFileContents env optPreprocessor filename ms
         return (diag, Just modu)
 
 
@@ -153,11 +152,10 @@ computePackageDeps env pkg = do
 
 typecheckModule :: IdeDefer
                 -> HscEnv
-                -> (DynFlags -> DynFlags)
                 -> [Linkable] -- ^ linkables not to unload
                 -> ParsedModule
                 -> IO (IdeResult TcModuleResult)
-typecheckModule (IdeDefer defer) hsc modify_dflags keep_lbls pm = do
+typecheckModule (IdeDefer defer) hsc keep_lbls pm = do
     fmap (either (,Nothing) id) $
       catchSrcErrors (hsc_dflags hsc) "typecheck" $ do
 
@@ -166,7 +164,7 @@ typecheckModule (IdeDefer defer) hsc modify_dflags keep_lbls pm = do
 
         modSummary' <- initPlugins hsc modSummary
         (warnings, tcm) <- withWarnings "typecheck" $ \tweak ->
-            tcRnModule hsc modify_dflags keep_lbls $ demoteIfDefer pm{pm_mod_summary = tweak modSummary'}
+            tcRnModule hsc keep_lbls $ demoteIfDefer pm{pm_mod_summary = tweak modSummary'}
         let errorPipeline = unDefer . hideDiag dflags . tagDiag
             diags = map errorPipeline warnings
             deferedError = any fst diags
@@ -210,10 +208,10 @@ captureSplices dflags k = do
             liftIO $ modifyIORef' var $ awSplicesL %~ ((e, aw') :)
             pure $ f aw'
 
-tcRnModule :: HscEnv -> (DynFlags -> DynFlags) -> [Linkable] -> ParsedModule -> IO TcModuleResult
-tcRnModule hsc_env modify_dflags keep_lbls pmod = do
+tcRnModule :: HscEnv -> [Linkable] -> ParsedModule -> IO TcModuleResult
+tcRnModule hsc_env keep_lbls pmod = do
   let ms = pm_mod_summary pmod
-      hsc_env_tmp = hsc_env { hsc_dflags = modify_dflags $ ms_hspp_opts ms }
+      hsc_env_tmp = hsc_env { hsc_dflags = ms_hspp_opts ms }
 
   unload hsc_env_tmp keep_lbls
 
@@ -813,14 +811,13 @@ parseHeader dflags filename contents = do
 -- ModSummary must contain the (preprocessed) contents of the buffer
 parseFileContents
        :: HscEnv
-       -> (DynFlags -> DynFlags)
        -> (GHC.ParsedSource -> IdePreprocessedSource)
        -> FilePath  -- ^ the filename (for source locations)
        -> ModSummary
        -> ExceptT [FileDiagnostic] IO ([FileDiagnostic], ParsedModule)
-parseFileContents env modifyDynFlags customPreprocessor filename ms = do
+parseFileContents env customPreprocessor filename ms = do
    let loc  = mkRealSrcLoc (mkFastString filename) 1 1
-       dflags = modifyDynFlags $ ms_hspp_opts ms
+       dflags = ms_hspp_opts ms
 
        contents = fromJust $ ms_hspp_buf ms
    case unP Parser.parseModule (mkPState dflags contents loc) of
diff --git a/ghcide/src/Development/IDE/Core/Rules.hs b/ghcide/src/Development/IDE/Core/Rules.hs
index 59b8ef39dc..5609b4479a 100644
--- a/ghcide/src/Development/IDE/Core/Rules.hs
+++ b/ghcide/src/Development/IDE/Core/Rules.hs
@@ -216,18 +216,17 @@ getParsedModuleRule =
     sess <- use_ GhcSession file
     let hsc = hscEnv sess
     opt <- getIdeOptions
-    modify_dflags <- getModifyDynFlags
 
     -- TODO(sandy): should we apply modify_dflags here?
     let dflags    = ms_hspp_opts ms
-        mainParse = getParsedModuleDefinition hsc modify_dflags opt file ms
+        mainParse = getParsedModuleDefinition hsc opt file ms
 
     -- Parse again (if necessary) to capture Haddock parse errors
     res@(_,pmod) <- if gopt Opt_Haddock dflags
         then
             liftIO mainParse
         else do
-            let haddockParse = getParsedModuleDefinition hsc modify_dflags opt file (withOptHaddock ms)
+            let haddockParse = getParsedModuleDefinition hsc opt file (withOptHaddock ms)
 
             -- parse twice, with and without Haddocks, concurrently
             -- we cannot ignore Haddock parse errors because files of
@@ -285,11 +284,10 @@ getParsedModuleWithCommentsRule =
     ModSummaryResult{msrModSummary = ms} <- use_ GetModSummary file
     sess <- use_ GhcSession file
     opt <- getIdeOptions
-    modify_dflags <- getModifyDynFlags
 
     let ms' = withoutOption Opt_Haddock $ withOption Opt_KeepRawTokenStream ms
 
-    liftIO $ snd <$> getParsedModuleDefinition (hscEnv sess) modify_dflags opt file ms'
+    liftIO $ snd <$> getParsedModuleDefinition (hscEnv sess) opt file ms'
 
 getModifyDynFlags :: Action (DynFlags -> DynFlags)
 getModifyDynFlags = maybe id modifyDynFlags <$> getShakeExtra
@@ -297,13 +295,12 @@ getModifyDynFlags = maybe id modifyDynFlags <$> getShakeExtra
 
 getParsedModuleDefinition
     :: HscEnv
-   -> (DynFlags -> DynFlags)
     -> IdeOptions
     -> NormalizedFilePath
     -> ModSummary -> IO ([FileDiagnostic], Maybe ParsedModule)
-getParsedModuleDefinition packageState modifyDynFlags opt file ms = do
+getParsedModuleDefinition packageState opt file ms = do
     let fp = fromNormalizedFilePath file
-    (diag, res) <- parseModule opt packageState modifyDynFlags fp ms
+    (diag, res) <- parseModule opt packageState fp ms
     case res of
         Nothing   -> pure (diag, Nothing)
         Just modu -> pure (diag, Just modu)
@@ -620,11 +617,10 @@ typeCheckRuleDefinition
 typeCheckRuleDefinition hsc pm = do
   setPriority priorityTypeCheck
   IdeOptions { optDefer = defer } <- getIdeOptions
-  modify_dflags <- getModifyDynFlags
 
   linkables_to_keep <- currentLinkables
   addUsageDependencies $ liftIO $
-    typecheckModule defer hsc modify_dflags linkables_to_keep pm
+    typecheckModule defer hsc linkables_to_keep pm
   where
     addUsageDependencies :: Action (a, Maybe TcModuleResult) -> Action (a, Maybe TcModuleResult)
     addUsageDependencies a = do
@@ -792,7 +788,9 @@ isHiFileStableRule = defineEarlyCutoff $ RuleNoDiagnostics $ \IsHiFileStable f -
 getModSummaryRule :: Rules ()
 getModSummaryRule = do
     defineEarlyCutoff $ Rule $ \GetModSummary f -> do
-        session <- hscEnv <$> use_ GhcSession f
+        session' <- hscEnv <$> use_ GhcSession f
+        modify_dflags <- getModifyDynFlags
+        let session = session' { hsc_dflags = modify_dflags $ hsc_dflags session' }
         (modTime, mFileContent) <- getFileContents f
         let fp = fromNormalizedFilePath f
         modS <- liftIO $ runExceptT $
@@ -872,15 +870,14 @@ regenerateHiFile :: HscEnvEq -> NormalizedFilePath -> ModSummary -> Maybe Linkab
 regenerateHiFile sess f ms compNeeded = do
     let hsc = hscEnv sess
     opt <- getIdeOptions
-    modify_dflags <- getModifyDynFlags
 
     -- Embed haddocks in the interface file
-    (diags, mb_pm) <- liftIO $ getParsedModuleDefinition hsc modify_dflags opt f (withOptHaddock ms)
+    (diags, mb_pm) <- liftIO $ getParsedModuleDefinition hsc opt f (withOptHaddock ms)
     (diags, mb_pm) <- case mb_pm of
         Just _ -> return (diags, mb_pm)
         Nothing -> do
             -- if parsing fails, try parsing again with Haddock turned off
-            (diagsNoHaddock, mb_pm) <- liftIO $ getParsedModuleDefinition hsc modify_dflags opt f ms
+            (diagsNoHaddock, mb_pm) <- liftIO $ getParsedModuleDefinition hsc opt f ms
             return (mergeParseErrorsHaddock diagsNoHaddock diags, mb_pm)
     case mb_pm of
         Nothing -> return (diags, Nothing)

From 5a57078c8018864a4c0b07244fa57926cc59f120 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Tue, 27 Apr 2021 18:17:53 -0700
Subject: [PATCH 26/52] Undo changes

---
 ghcide/src/Development/IDE/Core/Compile.hs | 3 +--
 ghcide/src/Development/IDE/Core/Rules.hs   | 1 -
 2 files changed, 1 insertion(+), 3 deletions(-)

diff --git a/ghcide/src/Development/IDE/Core/Compile.hs b/ghcide/src/Development/IDE/Core/Compile.hs
index 64d710f8a9..ff8f5f1c0c 100644
--- a/ghcide/src/Development/IDE/Core/Compile.hs
+++ b/ghcide/src/Development/IDE/Core/Compile.hs
@@ -4,7 +4,6 @@
 {-# LANGUAGE CPP        #-}
 {-# LANGUAGE GADTs      #-}
 {-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE PatternSynonyms #-}
 #include "ghc-api-version.h"
 
 -- | Based on https://ghc.haskell.org/trac/ghc/wiki/Commentary/Compiler/API.
@@ -208,6 +207,7 @@ captureSplices dflags k = do
             liftIO $ modifyIORef' var $ awSplicesL %~ ((e, aw') :)
             pure $ f aw'
 
+
 tcRnModule :: HscEnv -> [Linkable] -> ParsedModule -> IO TcModuleResult
 tcRnModule hsc_env keep_lbls pmod = do
   let ms = pm_mod_summary pmod
@@ -818,7 +818,6 @@ parseFileContents
 parseFileContents env customPreprocessor filename ms = do
    let loc  = mkRealSrcLoc (mkFastString filename) 1 1
        dflags = ms_hspp_opts ms
-
        contents = fromJust $ ms_hspp_buf ms
    case unP Parser.parseModule (mkPState dflags contents loc) of
 #if MIN_GHC_API_VERSION(8,10,0)
diff --git a/ghcide/src/Development/IDE/Core/Rules.hs b/ghcide/src/Development/IDE/Core/Rules.hs
index 5609b4479a..ab2240cd39 100644
--- a/ghcide/src/Development/IDE/Core/Rules.hs
+++ b/ghcide/src/Development/IDE/Core/Rules.hs
@@ -217,7 +217,6 @@ getParsedModuleRule =
     let hsc = hscEnv sess
     opt <- getIdeOptions
 
-    -- TODO(sandy): should we apply modify_dflags here?
     let dflags    = ms_hspp_opts ms
         mainParse = getParsedModuleDefinition hsc opt file ms
 

From 9e74afc836627b966dabe640ef4b65e84b1ea933 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Tue, 27 Apr 2021 18:21:50 -0700
Subject: [PATCH 27/52] Make Plugin accumulators robust to changing defs

---
 ghcide/src/Development/IDE/Plugin/HLS.hs | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

diff --git a/ghcide/src/Development/IDE/Plugin/HLS.hs b/ghcide/src/Development/IDE/Plugin/HLS.hs
index 39f9a25025..113d319f04 100644
--- a/ghcide/src/Development/IDE/Plugin/HLS.hs
+++ b/ghcide/src/Development/IDE/Plugin/HLS.hs
@@ -26,6 +26,7 @@ import           Development.IDE.Core.Shake
 import           Development.IDE.Core.Tracing
 import           Development.IDE.LSP.Server
 import           Development.IDE.Plugin
+import qualified Development.IDE.Plugin       as P
 import           Development.IDE.Types.Logger
 import           Development.IDE.Graph            (Rules)
 import           Ide.Plugin.Config
@@ -66,19 +67,19 @@ asGhcIdePlugin (IdePlugins ls) =
 -- ---------------------------------------------------------------------
 
 rulesPlugins :: [(PluginId, Rules ())] -> Plugin Config
-rulesPlugins rs = Plugin rules mempty mempty
+rulesPlugins rs = mempty { P.pluginRules = rules }
     where
         rules = foldMap snd rs
 
 dynFlagsPlugins :: [(PluginId, DynFlags -> DynFlags)] -> Plugin Config
-dynFlagsPlugins rs = Plugin mempty mempty endo
+dynFlagsPlugins rs = mempty { P.pluginModifyDynflags = endo }
     where
         endo = foldMap (Endo . snd) rs
 
 -- ---------------------------------------------------------------------
 
 executeCommandPlugins :: [(PluginId, [PluginCommand IdeState])] -> Plugin Config
-executeCommandPlugins ecs = Plugin mempty (executeCommandHandlers ecs) mempty
+executeCommandPlugins ecs = mempty { P.pluginHandlers = executeCommandHandlers ecs }
 
 executeCommandHandlers :: [(PluginId, [PluginCommand IdeState])] -> LSP.Handlers (ServerM Config)
 executeCommandHandlers ecs = requestHandler SWorkspaceExecuteCommand execCmd
@@ -140,7 +141,7 @@ executeCommandHandlers ecs = requestHandler SWorkspaceExecuteCommand execCmd
 -- ---------------------------------------------------------------------
 
 extensiblePlugins :: [(PluginId, PluginHandlers IdeState)] -> Plugin Config
-extensiblePlugins xs = Plugin mempty handlers mempty
+extensiblePlugins xs = mempty { P.pluginHandlers = handlers }
   where
     IdeHandlers handlers' = foldMap bakePluginId xs
     bakePluginId :: (PluginId, PluginHandlers IdeState) -> IdeHandlers
@@ -168,7 +169,7 @@ extensiblePlugins xs = Plugin mempty handlers mempty
 -- ---------------------------------------------------------------------
 
 extensibleNotificationPlugins :: [(PluginId, PluginNotificationHandlers IdeState)] -> Plugin Config
-extensibleNotificationPlugins xs = Plugin mempty handlers mempty
+extensibleNotificationPlugins xs = mempty { P.pluginHandlers = handlers }
   where
     IdeNotificationHandlers handlers' = foldMap bakePluginId xs
     bakePluginId :: (PluginId, PluginNotificationHandlers IdeState) -> IdeNotificationHandlers

From 5adc27995d60a372d7671d5d82196de039741546 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 28 Apr 2021 11:09:33 -0700
Subject: [PATCH 28/52] Remove unused exts from Session

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

diff --git a/ghcide/session-loader/Development/IDE/Session.hs b/ghcide/session-loader/Development/IDE/Session.hs
index 387fe1b6fb..826f42c1b6 100644
--- a/ghcide/session-loader/Development/IDE/Session.hs
+++ b/ghcide/session-loader/Development/IDE/Session.hs
@@ -90,7 +90,6 @@ import           HieDb.Create
 import           HieDb.Types
 import           HieDb.Utils
 import           Maybes                               (MaybeT (runMaybeT))
-import           GHC.LanguageExtensions               (Extension(EmptyCase, QuasiQuotes))
 
 -- | Bump this version number when making changes to the format of the data stored in hiedb
 hiedbDataVersion :: String

From 92e95c530f0ea9c510a29cfb4b577796a49c84dd Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 28 Apr 2021 11:09:46 -0700
Subject: [PATCH 29/52] Reannotate the AST with tactic blocks

---
 .../src/Wingman/LanguageServer.hs             | 33 ++++++++++++++++---
 1 file changed, 29 insertions(+), 4 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
index 1e9b54cd97..c13e3ecea7 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
@@ -10,7 +10,7 @@ module Wingman.LanguageServer where
 import           ConLike
 import           Control.Arrow ((***))
 import           Control.Monad
-import           Control.Monad.State (State, get, put, evalState)
+import           Control.Monad.State (State, evalState)
 import           Control.Monad.Trans.Maybe
 import           Data.Bifunctor (first)
 import           Data.Coerce
@@ -32,7 +32,7 @@ import           Development.IDE.Core.Service (runAction)
 import           Development.IDE.Core.Shake (IdeState (..), uses, define, use)
 import qualified Development.IDE.Core.Shake as IDE
 import           Development.IDE.Core.UseStale
-import           Development.IDE.GHC.Compat
+import           Development.IDE.GHC.Compat hiding (parseExpr)
 import           Development.IDE.GHC.Error (realSrcSpanToRange)
 import           Development.IDE.GHC.ExactPrint
 import           Development.IDE.Graph (Action, RuleResult, Rules, action)
@@ -41,7 +41,7 @@ import           Development.IDE.Spans.LocalBindings (Bindings, getDefiningBindi
 import qualified FastString
 import           GHC.Generics (Generic)
 import           Generics.SYB hiding (Generic)
-import           GhcPlugins (tupleDataCon, consDataCon, substTyAddInScope, ExternalPackageState, HscEnv (hsc_EPS), liftIO, unpackFS)
+import           GhcPlugins (tupleDataCon, consDataCon, substTyAddInScope, ExternalPackageState, HscEnv (hsc_EPS), unpackFS)
 import qualified Ide.Plugin.Config as Plugin
 import           Ide.Plugin.Properties
 import           Ide.PluginUtils (usePropertyLsp)
@@ -62,6 +62,13 @@ import           Wingman.Judgements.Theta
 import           Wingman.Range
 import           Wingman.StaticPlugin (pattern WingmanMetaprogram)
 import           Wingman.Types
+import Control.Monad.IO.Class
+import Control.Monad.RWS
+import Language.Haskell.GHC.ExactPrint (modifyAnnsT, addAnnotationsForPretty)
+import Retrie (transformA)
+import GhcPlugins (mkRdrUnqual)
+import Language.Haskell.GHC.ExactPrint (Transform)
+import Data.Functor.Identity (runIdentity)
 
 
 tacticDesc :: T.Text -> T.Text
@@ -548,5 +555,23 @@ mkWorkspaceEdits
     -> Graft (Either String) ParsedSource
     -> Either UserFacingMessage WorkspaceEdit
 mkWorkspaceEdits dflags ccs uri pm g = do
-  let response = transform dflags ccs uri g pm
+  let pm' = runIdentity $ transformA pm annotateMetaprograms
+  let response = transform dflags ccs uri g pm'
    in first (InfrastructureError . T.pack) response
+
+
+annotateMetaprograms :: Data a => a -> Transform a
+annotateMetaprograms = everywhereM $ mkM $ \case
+  L ss (WingmanMetaprogram mp) -> do
+    let x = L ss
+          $ HsSpliceE noExt
+          $ HsQuasiQuote noExt
+              (mkRdrUnqual $ mkVarOcc "splice")
+              (mkRdrUnqual $ mkVarOcc "wingman")
+              noSrcSpan
+              mp
+    let anns = addAnnotationsForPretty [] x mempty
+    modifyAnnsT $ mappend anns
+    pure x
+  (x :: LHsExpr GhcPs) -> pure x
+

From 2c98fec63649ddf03b0fe5b235f71fae1adcbc74 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 28 Apr 2021 11:31:11 -0700
Subject: [PATCH 30/52] Tidy parser

---
 .../src/Wingman/Metaprogramming/Parser.hs      | 18 +++++++++++++++---
 1 file changed, 15 insertions(+), 3 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
index 24c4bc255f..8b66a336b6 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
@@ -71,16 +71,28 @@ operators =
     ]
 
 
+tacticProgram :: Parser (TacticsM ())
+tacticProgram = do
+  sc
+  r <- tactic P.<|> pure (pure ())
+  P.eof
+  pure r
+
+
+wrapError :: String -> String
+wrapError err = "```\n" <> err <> "\n```\n"
+
+
 attempt_it :: Context -> Judgement -> String -> Either String String
 attempt_it ctx jdg program =
-  case P.runParser (sc *> tactic <* P.eof) "<splice>" $ T.pack program of
-    Left peb -> Left $ P.errorBundlePretty peb
+  case P.runParser tacticProgram "<splice>" $ T.pack program of
+    Left peb -> Left $ wrapError $ P.errorBundlePretty peb
     Right tt -> do
       case runTactic
              ctx
              jdg
              tt
         of
-          Left tes -> Left $ show tes
+          Left tes -> Left $ wrapError $ show tes
           Right rtr -> Right $ layout $ proofState rtr
 

From e3d2e8d61c17daef44cde068de566c73864f449e Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 28 Apr 2021 15:13:43 -0700
Subject: [PATCH 31/52] MetaprogramSyntax and exact combinator

---
 .../src/Wingman/LanguageServer.hs               | 11 ++---------
 .../hls-tactics-plugin/src/Wingman/Machinery.hs |  6 ++++++
 .../src/Wingman/StaticPlugin.hs                 | 17 ++++++++++++++++-
 .../hls-tactics-plugin/src/Wingman/Tactics.hs   | 11 ++++++++++-
 4 files changed, 34 insertions(+), 11 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
index c13e3ecea7..ec5cc5dcec 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
@@ -60,13 +60,12 @@ import           Wingman.Judgements
 import           Wingman.Judgements.SYB (everythingContaining)
 import           Wingman.Judgements.Theta
 import           Wingman.Range
-import           Wingman.StaticPlugin (pattern WingmanMetaprogram)
+import           Wingman.StaticPlugin (pattern WingmanMetaprogram, pattern MetaprogramSyntax)
 import           Wingman.Types
 import Control.Monad.IO.Class
 import Control.Monad.RWS
 import Language.Haskell.GHC.ExactPrint (modifyAnnsT, addAnnotationsForPretty)
 import Retrie (transformA)
-import GhcPlugins (mkRdrUnqual)
 import Language.Haskell.GHC.ExactPrint (Transform)
 import Data.Functor.Identity (runIdentity)
 
@@ -563,13 +562,7 @@ mkWorkspaceEdits dflags ccs uri pm g = do
 annotateMetaprograms :: Data a => a -> Transform a
 annotateMetaprograms = everywhereM $ mkM $ \case
   L ss (WingmanMetaprogram mp) -> do
-    let x = L ss
-          $ HsSpliceE noExt
-          $ HsQuasiQuote noExt
-              (mkRdrUnqual $ mkVarOcc "splice")
-              (mkRdrUnqual $ mkVarOcc "wingman")
-              noSrcSpan
-              mp
+    let x = L ss $ MetaprogramSyntax mp
     let anns = addAnnotationsForPretty [] x mempty
     modifyAnnsT $ mappend anns
     pure x
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs b/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs
index 8c1afce251..c87e2bcbee 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs
@@ -299,3 +299,9 @@ try'
     -> TacticT jdg ext err s m ()
 try' t = commit t $ pure ()
 
+
+------------------------------------------------------------------------------
+-- | Sorry leaves a hole in its extract
+exact :: HsExpr GhcPs -> TacticsM ()
+exact = rule . const . pure . pure . noLoc
+
diff --git a/plugins/hls-tactics-plugin/src/Wingman/StaticPlugin.hs b/plugins/hls-tactics-plugin/src/Wingman/StaticPlugin.hs
index 08bda9fceb..8439448662 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/StaticPlugin.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/StaticPlugin.hs
@@ -1,6 +1,7 @@
 module Wingman.StaticPlugin
   ( staticPlugin
   , pattern WingmanMetaprogram
+  , pattern MetaprogramSyntax
   ) where
 
 import           Data.Data
@@ -62,7 +63,21 @@ mkMetaprogram ss mp =
 addMetaprogrammingSyntax :: Data a => a -> a
 addMetaprogrammingSyntax =
   everywhere $ mkT $ \case
-    L ss (HsSpliceE _ (HsQuasiQuote _ _ (occNameString . rdrNameOcc -> "wingman") _ mp)) ->
+    L ss (MetaprogramSyntax mp) ->
       L ss $ mkMetaprogram ss mp
     (x :: LHsExpr GhcPs) -> x
 
+
+pattern MetaprogramSyntax :: FastString -> HsExpr GhcPs
+pattern MetaprogramSyntax mp <-
+    HsSpliceE _ (HsQuasiQuote _ _ (occNameString . rdrNameOcc -> "wingman") _ mp)
+  where
+    MetaprogramSyntax mp =
+      HsSpliceE noExt $
+        HsQuasiQuote
+          noExt
+          (mkRdrUnqual $ mkVarOcc "splice")
+          (mkRdrUnqual $ mkVarOcc "wingman")
+          noSrcSpan
+          mp
+
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs
index aa722ff003..4d9204621c 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs
@@ -1,3 +1,5 @@
+{-# LANGUAGE OverloadedStrings #-}
+
 module Wingman.Tactics
   ( module Wingman.Tactics
   , runTactic
@@ -36,6 +38,7 @@ import           Wingman.Machinery
 import           Wingman.Naming
 import           Wingman.Types
 import OccName (mkVarOcc)
+import Wingman.StaticPlugin (pattern MetaprogramSyntax)
 
 
 ------------------------------------------------------------------------------
@@ -279,7 +282,13 @@ obvious = tracing "obvious" $ do
 ------------------------------------------------------------------------------
 -- | Sorry leaves a hole in its extract
 sorry :: TacticsM ()
-sorry = rule $ const $ pure $ (pure $ noLoc $ var' $ mkVarOcc "_")
+sorry = exact $ var' $ mkVarOcc "_"
+
+
+------------------------------------------------------------------------------
+-- | Sorry leaves a hole in its extract
+metaprogram :: TacticsM ()
+metaprogram = exact $ MetaprogramSyntax ""
 
 
 ------------------------------------------------------------------------------

From cf6fc2ed683ca8b81512e88ee8bb2773f9ddadc8 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 28 Apr 2021 16:05:08 -0700
Subject: [PATCH 32/52] Add introduce metaprogram code action

---
 .../src/Wingman/LanguageServer/TacticProviders.hs           | 6 ++++++
 plugins/hls-tactics-plugin/src/Wingman/Types.hs             | 2 ++
 2 files changed, 8 insertions(+)

diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs
index 71ed57d560..dd7320a40e 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs
@@ -52,6 +52,7 @@ commandTactic HomomorphismLambdaCase = const homoLambdaCase
 commandTactic DestructAll            = const destructAll
 commandTactic UseDataCon             = userSplit
 commandTactic Refine                 = const refine
+commandTactic BeginMetaprogram       = const metaprogram
 
 
 ------------------------------------------------------------------------------
@@ -67,6 +68,7 @@ tacticKind HomomorphismLambdaCase = "homomorphicLambdaCase"
 tacticKind DestructAll            = "splitFuncArgs"
 tacticKind UseDataCon             = "useConstructor"
 tacticKind Refine                 = "refine"
+tacticKind BeginMetaprogram       = "metaprogram"
 
 
 ------------------------------------------------------------------------------
@@ -83,6 +85,7 @@ tacticPreferred HomomorphismLambdaCase = False
 tacticPreferred DestructAll            = True
 tacticPreferred UseDataCon             = True
 tacticPreferred Refine                 = True
+tacticPreferred BeginMetaprogram       = False
 
 
 mkTacticKind :: TacticCommand -> CodeActionKind
@@ -139,6 +142,9 @@ commandProvider UseDataCon =
 commandProvider Refine =
   requireFeature FeatureRefineHole $
     provide Refine ""
+commandProvider BeginMetaprogram =
+  -- requireFeature FeatureMetaprogram $
+    provide BeginMetaprogram ""
 
 
 ------------------------------------------------------------------------------
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Types.hs b/plugins/hls-tactics-plugin/src/Wingman/Types.hs
index 37b20d13e2..2774a1dbf3 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Types.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Types.hs
@@ -56,6 +56,7 @@ data TacticCommand
   | DestructAll
   | UseDataCon
   | Refine
+  | BeginMetaprogram
   deriving (Eq, Ord, Show, Enum, Bounded)
 
 -- | Generate a title for the command.
@@ -72,6 +73,7 @@ tacticTitle = (mappend "Wingman: " .) . go
     go DestructAll _            = "Split all function arguments"
     go UseDataCon dcon          = "Use constructor " <> dcon
     go Refine _                 = "Refine hole"
+    go BeginMetaprogram _       = "Use custom tactic block"
 
 
 ------------------------------------------------------------------------------

From 89b7e63eb000571b5f7ed303550770c89342166a Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 3 May 2021 21:30:06 -0700
Subject: [PATCH 33/52] Use noExtField

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

diff --git a/plugins/hls-tactics-plugin/src/Wingman/StaticPlugin.hs b/plugins/hls-tactics-plugin/src/Wingman/StaticPlugin.hs
index 8439448662..1721b8bc94 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/StaticPlugin.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/StaticPlugin.hs
@@ -52,9 +52,9 @@ metaprogrammingPlugin =
 
 mkMetaprogram :: SrcSpan -> FastString -> HsExpr GhcPs
 mkMetaprogram ss mp =
-  HsSCC noExt MetaprogramSourceText (StringLiteral NoSourceText mp)
+  HsSCC noExtField MetaprogramSourceText (StringLiteral NoSourceText mp)
     $ L ss
-    $ HsVar noExt
+    $ HsVar noExtField
     $ L ss
     $ mkRdrUnqual
     $ mkVarOcc "_"
@@ -73,9 +73,9 @@ pattern MetaprogramSyntax mp <-
     HsSpliceE _ (HsQuasiQuote _ _ (occNameString . rdrNameOcc -> "wingman") _ mp)
   where
     MetaprogramSyntax mp =
-      HsSpliceE noExt $
+      HsSpliceE noExtField $
         HsQuasiQuote
-          noExt
+          noExtField
           (mkRdrUnqual $ mkVarOcc "splice")
           (mkRdrUnqual $ mkVarOcc "wingman")
           noSrcSpan

From c032f7b59dddf858af6f4624e0c33e543eec5a89 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 3 May 2021 21:34:02 -0700
Subject: [PATCH 34/52] Appease Hlint

---
 ghcide/session-loader/Development/IDE/Session.hs | 1 -
 ghcide/src/Development/IDE/Core/Shake.hs         | 3 ---
 2 files changed, 4 deletions(-)

diff --git a/ghcide/session-loader/Development/IDE/Session.hs b/ghcide/session-loader/Development/IDE/Session.hs
index 3fb8577cf6..449d6bd3f2 100644
--- a/ghcide/session-loader/Development/IDE/Session.hs
+++ b/ghcide/session-loader/Development/IDE/Session.hs
@@ -84,7 +84,6 @@ import           Control.Concurrent.STM               (atomically)
 import           Control.Concurrent.STM.TQueue
 import qualified Data.HashSet                         as Set
 import           Database.SQLite.Simple
-import           GHC.LanguageExtensions               (Extension (EmptyCase))
 import           HieDb.Create
 import           HieDb.Types
 import           HieDb.Utils
diff --git a/ghcide/src/Development/IDE/Core/Shake.hs b/ghcide/src/Development/IDE/Core/Shake.hs
index 31f1eeca09..30255ae6e8 100644
--- a/ghcide/src/Development/IDE/Core/Shake.hs
+++ b/ghcide/src/Development/IDE/Core/Shake.hs
@@ -149,10 +149,7 @@ import           HieDb.Types
 import           Ide.Plugin.Config
 import qualified Ide.PluginUtils                      as HLS
 import           Ide.Types                            (PluginId)
-import           UnliftIO.Exception                   (bracket_)
 import DynFlags (DynFlags)
-import qualified Ide.PluginUtils                        as HLS
-import           Ide.Types                              (PluginId)
 
 -- | We need to serialize writes to the database, so we send any function that
 -- needs to write to the database over the channel, where it will be picked up by

From 69d32963d2c77213d8a7b53a86976230537e4c74 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 3 May 2021 21:51:02 -0700
Subject: [PATCH 35/52] Compat for mkFunTys

---
 plugins/hls-tactics-plugin/src/Wingman/GHC.hs     | 9 +++++++++
 plugins/hls-tactics-plugin/src/Wingman/Tactics.hs | 2 +-
 2 files changed, 10 insertions(+), 1 deletion(-)

diff --git a/plugins/hls-tactics-plugin/src/Wingman/GHC.hs b/plugins/hls-tactics-plugin/src/Wingman/GHC.hs
index 83ed6a93fb..30ad63bd57 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/GHC.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/GHC.hs
@@ -355,3 +355,12 @@ liftMaybe a = MaybeT $ pure a
 typeCheck :: HscEnv -> TcGblEnv -> HsExpr GhcTc -> IO (Maybe Type)
 typeCheck hscenv tcg = fmap snd . initDs hscenv tcg . fmap exprType . dsExpr
 
+
+mkFunTys' :: [Type] -> Type -> Type
+mkFunTys' =
+#if __GLASGOW_HASKELL__ <= 808
+  mkFunTys
+#else
+  mkVisFunTys
+#endif
+
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs
index 4d9204621c..6f3d36354b 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs
@@ -117,7 +117,7 @@ intros' names = rule $ \jdg -> do
           top_hole = isTopHole ctx jdg
           hy' = lambdaHypothesis top_hole $ zip vs $ coerce as
           jdg' = introduce hy'
-               $ withNewGoal (CType $ mkFunTys (drop num_args as) b) jdg
+               $ withNewGoal (CType $ mkFunTys' (drop num_args as) b) jdg
       ext <- newSubgoal jdg'
       pure $
         ext

From 56572863d9cc072ef340741efda44e8a68a1374b Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 5 May 2021 20:31:54 -0700
Subject: [PATCH 36/52] Guard the static plugin

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

diff --git a/plugins/hls-tactics-plugin/src/Wingman/StaticPlugin.hs b/plugins/hls-tactics-plugin/src/Wingman/StaticPlugin.hs
index 1721b8bc94..b9476abee0 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/StaticPlugin.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/StaticPlugin.hs
@@ -1,3 +1,5 @@
+{-# LANGUAGE CPP #-}
+
 module Wingman.StaticPlugin
   ( staticPlugin
   , pattern WingmanMetaprogram
@@ -16,7 +18,9 @@ staticPlugin df
   = allowEmptyCaseButWithWarning
   $ enableQuasiQuotes
   $ df
+#if __GLASGOW_HASKELL__ >= 808
     { staticPlugins = staticPlugins df <> [metaprogrammingPlugin] }
+#endif
 
 
 pattern MetaprogramSourceText :: SourceText
@@ -42,12 +46,14 @@ allowEmptyCaseButWithWarning =
   flip xopt_set EmptyCase . flip wopt_set Opt_WarnIncompletePatterns
 
 
+#if __GLASGOW_HASKELL__ >= 808
 metaprogrammingPlugin :: StaticPlugin
 metaprogrammingPlugin =
     StaticPlugin $ PluginWithArgs (defaultPlugin { parsedResultAction = worker })  []
   where
     worker :: [CommandLineOption] -> ModSummary -> HsParsedModule -> Hsc HsParsedModule
     worker _ _ pm = pure $ pm { hpm_module = addMetaprogrammingSyntax $ hpm_module pm }
+#endif
 
 
 mkMetaprogram :: SrcSpan -> FastString -> HsExpr GhcPs

From 86e58b982920f4af604c6d66da67d9de1fc3c76f Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 5 May 2021 21:31:27 -0700
Subject: [PATCH 37/52] Static plugin doesn't even need to be here!

---
 hls-plugin-api/src/Ide/Types.hs | 1 -
 1 file changed, 1 deletion(-)

diff --git a/hls-plugin-api/src/Ide/Types.hs b/hls-plugin-api/src/Ide/Types.hs
index fbd9660cae..9e28cbfd77 100644
--- a/hls-plugin-api/src/Ide/Types.hs
+++ b/hls-plugin-api/src/Ide/Types.hs
@@ -50,7 +50,6 @@ import           Language.LSP.VFS
 import           OpenTelemetry.Eventlog
 import           System.IO.Unsafe
 import           Text.Regex.TDFA.Text            ()
-import GhcPlugins (StaticPlugin)
 import DynFlags (DynFlags)
 
 -- ---------------------------------------------------------------------

From 994662dc595ad390b50d4284033a6693534c712e Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Thu, 6 May 2021 09:09:15 -0700
Subject: [PATCH 38/52] textSpaces doesn't exist in old versions of
 prettyprinter

---
 .../src/Wingman/Metaprogramming/ProofState.hs                | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/ProofState.hs b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/ProofState.hs
index 9c3e736b93..07921f6ad7 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/ProofState.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/ProofState.hs
@@ -7,7 +7,6 @@ import           Data.Bool (bool)
 import           Data.Functor ((<&>))
 import qualified Data.Text as T
 import           Data.Text.Prettyprint.Doc
-import           Data.Text.Prettyprint.Doc.Internal (textSpaces)
 import           Data.Text.Prettyprint.Doc.Render.Util.Panic
 import           Language.LSP.Types (sectionSeparator)
 import           Wingman.Judgements (jHypothesis)
@@ -107,3 +106,7 @@ count :: Doc Ann -> Int -> Doc Ann
 count thing n =
   pretty n <+> thing <> bool "" "s" (n /= 1)
 
+textSpaces :: Int -> T.Text
+textSpaces n = T.replicate n $ T.singleton ' '
+
+

From 8ad359e35235debd27b0c01565d46129e1694203 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Thu, 6 May 2021 09:32:40 -0700
Subject: [PATCH 39/52] Use a record for the result of judgmentForHole

---
 .../src/Wingman/LanguageServer.hs               | 17 +++++++++++++++--
 .../src/Wingman/LanguageServer/Metaprogram.hs   |  2 +-
 .../hls-tactics-plugin/src/Wingman/Plugin.hs    | 11 ++++++-----
 3 files changed, 22 insertions(+), 8 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
index ec5cc5dcec..45ca550f49 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
@@ -189,6 +189,14 @@ getAllMetaprograms = everything (<>) $ mkQ mempty $ \case
   WingmanMetaprogram fs -> [ unpackFS fs ]
   (_ :: HsExpr GhcTc)  -> mempty
 
+
+data HoleJudgment = HoleJudgment
+  { hj_range :: Tracked 'Current Range
+  , hj_jdg :: Judgement
+  , hj_ctx :: Context
+  , hj_dflags :: DynFlags
+  }
+
 ------------------------------------------------------------------------------
 -- | Find the last typechecked module, and find the most specific span, as well
 -- as the judgement at the given range.
@@ -197,7 +205,7 @@ judgementForHole
     -> NormalizedFilePath
     -> Tracked 'Current Range
     -> Config
-    -> MaybeT IO (Tracked 'Current Range, Judgement, Context, DynFlags)
+    -> MaybeT IO HoleJudgment
 judgementForHole state nfp range cfg = do
   let stale a = runStaleIde "judgementForHole" state nfp a
 
@@ -224,7 +232,12 @@ judgementForHole state nfp range cfg = do
       (jdg, ctx) <- liftMaybe $ mkJudgementAndContext cfg g binds new_rss tcg eps kt
 
       dflags <- getIdeDynflags state nfp
-      pure (fmap realSrcSpanToRange new_rss, jdg, ctx, dflags)
+      pure $ HoleJudgment
+        { hj_range = fmap realSrcSpanToRange new_rss
+        , hj_jdg = jdg
+        , hj_ctx = ctx
+        , hj_dflags = dflags
+        }
 
 
 
diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/Metaprogram.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/Metaprogram.hs
index 00c60bc579..2fc9f29675 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/Metaprogram.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/Metaprogram.hs
@@ -51,7 +51,7 @@ hoverProvider state plId (HoverParams (TextDocumentIdentifier uri) pos _)
           case (find (flip containsSpan (realSrcLocSpan loc) . unTrack . fst) holes) of
             Just (trss, program) -> do
               let tr_range = fmap realSrcSpanToRange trss
-              (_, jdg, ctx, _) <- judgementForHole state nfp tr_range cfg
+              HoleJudgment{hj_jdg=jdg, hj_ctx=ctx} <- judgementForHole state nfp tr_range cfg
               pure $ Hover
                 { _contents = HoverContents
                             $ MarkupContent MkMarkdown
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs b/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs
index 12d29a0996..7a5c00cfd4 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE RecordWildCards #-}
 
 -- | A plugin that uses tactics to synthesize code
 module Wingman.Plugin
@@ -74,7 +75,7 @@ codeActionProvider state plId (CodeActionParams _ _ (TextDocumentIdentifier uri)
   | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do
       cfg <- getTacticConfig plId
       liftIO $ fromMaybeT (Right $ List []) $ do
-        (_, jdg, _, dflags) <- judgementForHole state nfp range cfg
+        HoleJudgment{hj_jdg = jdg, hj_dflags = dflags} <- judgementForHole state nfp range cfg
         actions <- lift $
           -- This foldMap is over the function monoid.
           foldMap commandProvider [minBound .. maxBound] $ TacticProviderData
@@ -106,19 +107,19 @@ tacticCmd tac pId state (TacticParams uri range var_name)
       ccs <- getClientCapabilities
       cfg <- getTacticConfig pId
       res <- liftIO $ runMaybeT $ do
-        (range', jdg, ctx, dflags) <- judgementForHole state nfp range cfg
-        let span = fmap (rangeToRealSrcSpan (fromNormalizedFilePath nfp)) range'
+        HoleJudgment{..} <- judgementForHole state nfp range cfg
+        let span = fmap (rangeToRealSrcSpan (fromNormalizedFilePath nfp)) hj_range
         TrackedStale pm pmmap <- stale GetAnnotatedParsedSource
         pm_span <- liftMaybe $ mapAgeFrom pmmap span
 
         timingOut (cfg_timeout_seconds cfg * seconds) $ join $
-          case runTactic ctx jdg $ tac $ mkVarOcc $ T.unpack var_name of
+          case runTactic hj_ctx hj_jdg $ tac $ mkVarOcc $ T.unpack var_name of
             Left _ -> Left TacticErrors
             Right rtr ->
               case rtr_extract rtr of
                 L _ (HsVar _ (L _ rdr)) | isHole (occName rdr) ->
                   Left NothingToDo
-                _ -> pure $ mkTacticResultEdits pm_span dflags ccs uri pm rtr
+                _ -> pure $ mkTacticResultEdits pm_span hj_dflags ccs uri pm rtr
 
       case res of
         Nothing -> do

From 9f43fcafc7a85204488ea92a1251786bad3b4249 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Thu, 6 May 2021 09:49:04 -0700
Subject: [PATCH 40/52] Return the hole's occName

---
 .../src/Wingman/LanguageServer.hs                  | 14 +++++++++-----
 1 file changed, 9 insertions(+), 5 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
index 45ca550f49..4588576ed1 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
@@ -220,7 +220,7 @@ judgementForHole state nfp range cfg = do
 
       hscenv <- stale GhcSessionDeps
 
-      (rss, g) <- liftMaybe $ getSpanAndTypeAtHole range' hf
+      (rss, occ, g) <- liftMaybe $ getSpanAndTypeAtHole range' hf
       new_rss <- liftMaybe $ mapAgeTo amapping rss
 
       -- KnownThings is just the instances in scope. There are no ranges
@@ -299,7 +299,7 @@ getAlreadyDestructed (unTrack -> span) (unTrack -> binds) =
 getSpanAndTypeAtHole
     :: Tracked age Range
     -> Tracked age (HieASTs b)
-    -> Maybe (Tracked age RealSrcSpan, b)
+    -> Maybe (Tracked age RealSrcSpan, OccName, b)
 getSpanAndTypeAtHole r@(unTrack -> range) (unTrack -> hf) = do
   join $ listToMaybe $ M.elems $ flip M.mapWithKey (getAsts hf) $ \fs ast ->
     case selectSmallestContaining (rangeToRealSrcSpan (FastString.unpackFS fs) range) ast of
@@ -309,9 +309,13 @@ getSpanAndTypeAtHole r@(unTrack -> range) (unTrack -> hf) = do
         ty <- listToMaybe $ nodeType info
         guard $ ("HsUnboundVar","HsExpr") `S.member` nodeAnnotations info
         -- Ensure we're actually looking at a hole here
-        guard $ all (either (const False) $ isHole . occName)
-          $ M.keysSet $ nodeIdentifiers info
-        pure (unsafeCopyAge r $ nodeSpan ast', ty)
+        occ <- (either (const Nothing) (Just . occName) =<<)
+             . listToMaybe
+             . S.toList
+             . M.keysSet
+             $ nodeIdentifiers info
+        guard $ isHole occ
+        pure (unsafeCopyAge r $ nodeSpan ast', occ, ty)
 
 
 

From 0fae78ca0eee839aae80bb74931ad2921c397fd9 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Thu, 6 May 2021 09:49:51 -0700
Subject: [PATCH 41/52] Add HoleSort; filter code actions by their holesort

---
 .../src/Wingman/LanguageServer.hs             | 16 +++++++---
 .../src/Wingman/LanguageServer/Metaprogram.hs | 18 +++++------
 .../Wingman/LanguageServer/TacticProviders.hs | 32 +++++++++++++++++--
 .../hls-tactics-plugin/src/Wingman/Plugin.hs  |  7 ++--
 .../src/Wingman/StaticPlugin.hs               |  6 +++-
 .../hls-tactics-plugin/src/Wingman/Types.hs   |  6 ++++
 6 files changed, 64 insertions(+), 21 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
index 4588576ed1..9ce79bf54d 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
@@ -60,7 +60,7 @@ import           Wingman.Judgements
 import           Wingman.Judgements.SYB (everythingContaining)
 import           Wingman.Judgements.Theta
 import           Wingman.Range
-import           Wingman.StaticPlugin (pattern WingmanMetaprogram, pattern MetaprogramSyntax)
+import           Wingman.StaticPlugin (pattern WingmanMetaprogram, pattern MetaprogramSyntax, metaprogramHoleName)
 import           Wingman.Types
 import Control.Monad.IO.Class
 import Control.Monad.RWS
@@ -191,10 +191,11 @@ getAllMetaprograms = everything (<>) $ mkQ mempty $ \case
 
 
 data HoleJudgment = HoleJudgment
-  { hj_range :: Tracked 'Current Range
-  , hj_jdg :: Judgement
-  , hj_ctx :: Context
-  , hj_dflags :: DynFlags
+  { hj_range     :: Tracked 'Current Range
+  , hj_jdg       :: Judgement
+  , hj_ctx       :: Context
+  , hj_dflags    :: DynFlags
+  , hj_hole_sort :: HoleSort
   }
 
 ------------------------------------------------------------------------------
@@ -237,9 +238,14 @@ judgementForHole state nfp range cfg = do
         , hj_jdg = jdg
         , hj_ctx = ctx
         , hj_dflags = dflags
+        , hj_hole_sort = classifyHoleName occ
         }
 
 
+classifyHoleName :: OccName -> HoleSort
+classifyHoleName occ | occ == metaprogramHoleName = Metaprogram
+classifyHoleName _ = Hole
+
 
 mkJudgementAndContext
     :: Config
diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/Metaprogram.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/Metaprogram.hs
index 2fc9f29675..a234f4d893 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/Metaprogram.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/Metaprogram.hs
@@ -2,6 +2,7 @@
 {-# LANGUAGE OverloadedStrings     #-}
 
 {-# LANGUAGE NoMonoLocalBinds  #-}
+{-# LANGUAGE RankNTypes #-}
 
 module Wingman.LanguageServer.Metaprogram (hoverProvider) where
 
@@ -32,6 +33,7 @@ import           Wingman.GHC
 import           Wingman.LanguageServer
 import           Wingman.Metaprogramming.Parser (attempt_it)
 import           Wingman.StaticPlugin (pattern WingmanMetaprogram)
+import Wingman.Judgements.SYB (everythingContaining)
 
 
 ------------------------------------------------------------------------------
@@ -45,7 +47,7 @@ hoverProvider state plId (HoverParams (TextDocumentIdentifier uri) pos _)
       liftIO $ fromMaybeT (Right Nothing) $ do
         -- guard $ hasFeature FeatureEmptyCase $ cfg_feature_set cfg
 
-        holes <- emptyCaseScrutinees state nfp
+        holes <- emptyCaseScrutinees state nfp $ RealSrcSpan $ realSrcLocSpan loc
 
         fmap (Right . Just) $
           case (find (flip containsSpan (realSrcLocSpan loc) . unTrack . fst) holes) of
@@ -68,19 +70,17 @@ fromMaybeT :: Functor m => a -> MaybeT m a -> m a
 fromMaybeT def = fmap (fromMaybe def) . runMaybeT
 
 
-------------------------------------------------------------------------------
--- | Find the last typechecked module, and find the most specific span, as well
--- as the judgement at the given range.
 emptyCaseScrutinees
     :: IdeState
     -> NormalizedFilePath
+    -> SrcSpan
     -> MaybeT IO [(Tracked 'Current RealSrcSpan, T.Text)]
-emptyCaseScrutinees state nfp = do
+emptyCaseScrutinees state nfp ss = do
     let stale a = runStaleIde "emptyCaseScrutinees" state nfp a
 
     TrackedStale tcg tcg_map <- fmap (fmap tmrTypechecked) $ stale TypeCheck
 
-    let scrutinees = traverse (emptyCaseQ . tcg_binds) tcg
+    let scrutinees = traverse (metaprogramQ ss . tcg_binds) tcg
     for scrutinees $ \aged@(unTrack -> (ss, program)) -> do
       case ss of
         RealSrcSpan r   -> do
@@ -89,10 +89,8 @@ emptyCaseScrutinees state nfp = do
         UnhelpfulSpan _ -> empty
 
 
-------------------------------------------------------------------------------
--- | Get the 'SrcSpan' and scrutinee of every empty case.
-emptyCaseQ :: GenericQ [(SrcSpan, T.Text)]
-emptyCaseQ = everything (<>) $ mkQ mempty $ \case
+metaprogramQ :: SrcSpan -> GenericQ [(SrcSpan, T.Text)]
+metaprogramQ ss = everythingContaining ss $ mkQ mempty $ \case
   L new_span (WingmanMetaprogram program) -> pure (new_span, T.pack $ unpackFS $ program)
   (_ :: LHsExpr GhcTc) -> mempty
 
diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs
index dd7320a40e..2243e3d15f 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs
@@ -53,6 +53,7 @@ commandTactic DestructAll            = const destructAll
 commandTactic UseDataCon             = userSplit
 commandTactic Refine                 = const refine
 commandTactic BeginMetaprogram       = const metaprogram
+commandTactic RunMetaprogram         = const $ pure ()
 
 
 ------------------------------------------------------------------------------
@@ -68,7 +69,8 @@ tacticKind HomomorphismLambdaCase = "homomorphicLambdaCase"
 tacticKind DestructAll            = "splitFuncArgs"
 tacticKind UseDataCon             = "useConstructor"
 tacticKind Refine                 = "refine"
-tacticKind BeginMetaprogram       = "metaprogram"
+tacticKind BeginMetaprogram       = "beginMetaprogram"
+tacticKind RunMetaprogram         = "runMetaprogram"
 
 
 ------------------------------------------------------------------------------
@@ -86,6 +88,7 @@ tacticPreferred DestructAll            = True
 tacticPreferred UseDataCon             = True
 tacticPreferred Refine                 = True
 tacticPreferred BeginMetaprogram       = False
+tacticPreferred RunMetaprogram         = True
 
 
 mkTacticKind :: TacticCommand -> CodeActionKind
@@ -97,35 +100,45 @@ mkTacticKind =
 -- | 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 Auto  =
+  requireHoleSort Hole $
+  provide Auto ""
 commandProvider Intros =
+  requireHoleSort Hole $
   filterGoalType isFunction $
     provide Intros ""
 commandProvider Destruct =
+  requireHoleSort Hole $
   filterBindingType destructFilter $ \occ _ ->
     provide Destruct $ T.pack $ occNameString occ
 commandProvider DestructPun =
+  requireHoleSort Hole $
   requireFeature FeatureDestructPun $
     filterBindingType destructPunFilter $ \occ _ ->
       provide DestructPun $ T.pack $ occNameString occ
 commandProvider Homomorphism =
+  requireHoleSort Hole $
   filterBindingType homoFilter $ \occ _ ->
     provide Homomorphism $ T.pack $ occNameString occ
 commandProvider DestructLambdaCase =
+  requireHoleSort Hole $
   requireExtension LambdaCase $
     filterGoalType (isJust . lambdaCaseable) $
       provide DestructLambdaCase ""
 commandProvider HomomorphismLambdaCase =
+  requireHoleSort Hole $
   requireExtension LambdaCase $
     filterGoalType ((== Just True) . lambdaCaseable) $
       provide HomomorphismLambdaCase ""
 commandProvider DestructAll =
+  requireHoleSort Hole $
   requireFeature FeatureDestructAll $
     withJudgement $ \jdg ->
       case _jIsTopHole jdg && jHasBoundArgs jdg of
         True  -> provide DestructAll ""
         False -> mempty
 commandProvider UseDataCon =
+  requireHoleSort Hole $
   withConfig $ \cfg ->
     requireFeature FeatureUseDataCon $
       filterTypeProjection
@@ -140,11 +153,17 @@ commandProvider UseDataCon =
           . occName
           $ dataConName dcon
 commandProvider Refine =
+  requireHoleSort Hole $
   requireFeature FeatureRefineHole $
     provide Refine ""
 commandProvider BeginMetaprogram =
+  requireHoleSort Hole $
   -- requireFeature FeatureMetaprogram $
     provide BeginMetaprogram ""
+commandProvider RunMetaprogram =
+  requireHoleSort Metaprogram $
+  -- requireFeature FeatureMetaprogram $
+    provide RunMetaprogram ""
 
 
 ------------------------------------------------------------------------------
@@ -160,6 +179,7 @@ type TacticProvider
      = TacticProviderData
     -> IO [Command |? CodeAction]
 
+
 data TacticProviderData = TacticProviderData
   { tpd_dflags :: DynFlags
   , tpd_config :: Config
@@ -167,6 +187,7 @@ data TacticProviderData = TacticProviderData
   , tpd_uri    :: Uri
   , tpd_range  :: Tracked 'Current Range
   , tpd_jdg    :: Judgement
+  , tpd_hole_sort :: HoleSort
   }
 
 
@@ -189,6 +210,13 @@ requireFeature f tp tpd =
     False -> pure []
 
 
+requireHoleSort :: HoleSort -> TacticProvider -> TacticProvider
+requireHoleSort hs tp tpd =
+  case (== hs) $ tpd_hole_sort tpd of
+    True  -> tp tpd
+    False -> pure []
+
+
 ------------------------------------------------------------------------------
 -- | Restrict a 'TacticProvider', making sure it appears only when the given
 -- predicate holds for the goal.
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs b/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs
index 7a5c00cfd4..8623c1b9c2 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs
@@ -75,16 +75,17 @@ codeActionProvider state plId (CodeActionParams _ _ (TextDocumentIdentifier uri)
   | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do
       cfg <- getTacticConfig plId
       liftIO $ fromMaybeT (Right $ List []) $ do
-        HoleJudgment{hj_jdg = jdg, hj_dflags = dflags} <- judgementForHole state nfp range cfg
+        HoleJudgment{..} <- judgementForHole state nfp range cfg
         actions <- lift $
           -- This foldMap is over the function monoid.
           foldMap commandProvider [minBound .. maxBound] $ TacticProviderData
-            { tpd_dflags = dflags
+            { tpd_dflags = hj_dflags
             , tpd_config = cfg
             , tpd_plid   = plId
             , tpd_uri    = uri
             , tpd_range  = range
-            , tpd_jdg    = jdg
+            , tpd_jdg    = hj_jdg
+            , tpd_hole_sort = hj_hole_sort
             }
         pure $ Right $ List actions
 codeActionProvider _ _ _ = pure $ Right $ List []
diff --git a/plugins/hls-tactics-plugin/src/Wingman/StaticPlugin.hs b/plugins/hls-tactics-plugin/src/Wingman/StaticPlugin.hs
index b9476abee0..ccefb19d02 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/StaticPlugin.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/StaticPlugin.hs
@@ -2,6 +2,7 @@
 
 module Wingman.StaticPlugin
   ( staticPlugin
+  , metaprogramHoleName
   , pattern WingmanMetaprogram
   , pattern MetaprogramSyntax
   ) where
@@ -55,6 +56,9 @@ metaprogrammingPlugin =
     worker _ _ pm = pure $ pm { hpm_module = addMetaprogrammingSyntax $ hpm_module pm }
 #endif
 
+metaprogramHoleName :: OccName
+metaprogramHoleName = mkVarOcc "_$WINGMAN_HOLE"
+
 
 mkMetaprogram :: SrcSpan -> FastString -> HsExpr GhcPs
 mkMetaprogram ss mp =
@@ -63,7 +67,7 @@ mkMetaprogram ss mp =
     $ HsVar noExtField
     $ L ss
     $ mkRdrUnqual
-    $ mkVarOcc "_"
+    $ metaprogramHoleName
 
 
 addMetaprogrammingSyntax :: Data a => a -> a
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Types.hs b/plugins/hls-tactics-plugin/src/Wingman/Types.hs
index 2774a1dbf3..783c18ed23 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Types.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Types.hs
@@ -57,6 +57,7 @@ data TacticCommand
   | UseDataCon
   | Refine
   | BeginMetaprogram
+  | RunMetaprogram
   deriving (Eq, Ord, Show, Enum, Bounded)
 
 -- | Generate a title for the command.
@@ -74,6 +75,7 @@ tacticTitle = (mappend "Wingman: " .) . go
     go UseDataCon dcon          = "Use constructor " <> dcon
     go Refine _                 = "Refine hole"
     go BeginMetaprogram _       = "Use custom tactic block"
+    go RunMetaprogram _         = "Run custom tactic"
 
 
 ------------------------------------------------------------------------------
@@ -505,3 +507,7 @@ instance Show UserFacingMessage where
   show NothingToDo             = "Nothing to do"
   show (InfrastructureError t) = "Internal error: " <> T.unpack t
 
+
+data HoleSort = Hole | Metaprogram
+  deriving (Eq, Ord, Show, Enum, Bounded)
+

From 4100b2d118180583fa9fc1c898f1b49c3b22d6eb Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Thu, 6 May 2021 09:50:33 -0700
Subject: [PATCH 42/52] Minor tidying

---
 .../src/Wingman/Metaprogramming/ProofState.hs | 19 ++++++++++---------
 1 file changed, 10 insertions(+), 9 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/ProofState.hs b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/ProofState.hs
index 07921f6ad7..4bfa95cec8 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/ProofState.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/ProofState.hs
@@ -21,15 +21,16 @@ renderSimplyDecorated
     -> out
 renderSimplyDecorated text push pop = go []
   where
-    go _           SFail               = panicUncaughtFail
-    go []          SEmpty              = mempty
-    go (_:_)       SEmpty              = panicInputNotFullyConsumed
-    go stack       (SChar c rest)      = text (T.singleton c) <> go stack rest
-    go stack       (SText _l t rest)   = text t <> go stack rest
-    go stack       (SLine i rest)      = text (T.singleton '\n') <> text (textSpaces i) <> go stack rest
-    go stack       (SAnnPush ann rest) = push ann <> go (ann : stack) rest
-    go (ann:stack) (SAnnPop rest)      = pop ann <> go stack rest
-    go []          SAnnPop{}           = panicUnpairedPop
+    go _        SFail               = panicUncaughtFail
+    go []       SEmpty              = mempty
+    go (_:_)    SEmpty              = panicInputNotFullyConsumed
+    go st       (SChar c rest)      = text (T.singleton c) <> go st rest
+    go st       (SText _l t rest)   = text t <> go st rest
+    go st       (SLine i rest)      =
+      text (T.singleton '\n') <> text (textSpaces i) <> go st rest
+    go st       (SAnnPush ann rest) = push ann <> go (ann : st) rest
+    go (ann:st) (SAnnPop rest)      = pop ann <> go st rest
+    go []       SAnnPop{}           = panicUnpairedPop
 {-# INLINE renderSimplyDecorated #-}
 
 

From 1b9cafa5e2df6d89cba924d1afc171538afa2f69 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Thu, 6 May 2021 13:29:02 -0700
Subject: [PATCH 43/52] Better name for metaprogram holes

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

diff --git a/plugins/hls-tactics-plugin/src/Wingman/StaticPlugin.hs b/plugins/hls-tactics-plugin/src/Wingman/StaticPlugin.hs
index ccefb19d02..b26080fb23 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/StaticPlugin.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/StaticPlugin.hs
@@ -57,7 +57,7 @@ metaprogrammingPlugin =
 #endif
 
 metaprogramHoleName :: OccName
-metaprogramHoleName = mkVarOcc "_$WINGMAN_HOLE"
+metaprogramHoleName = mkVarOcc "_$metaprogram"
 
 
 mkMetaprogram :: SrcSpan -> FastString -> HsExpr GhcPs

From e0786351586bbd6589b72c8b374ec70b1854c2f5 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Thu, 6 May 2021 14:02:44 -0700
Subject: [PATCH 44/52] Use a record for DynFlags modifications

---
 ghcide/src/Development/IDE/Core/Rules.hs      | 12 ++++----
 ghcide/src/Development/IDE/Core/Service.hs    |  7 +++--
 ghcide/src/Development/IDE/Core/Shake.hs      |  7 +++--
 ghcide/src/Development/IDE/Main.hs            |  7 ++---
 ghcide/src/Development/IDE/Plugin.hs          |  3 +-
 ghcide/src/Development/IDE/Plugin/HLS.hs      |  7 ++---
 hls-plugin-api/src/Ide/Types.hs               | 17 +++++++++--
 .../src/Wingman/StaticPlugin.hs               | 29 ++++++++++---------
 8 files changed, 53 insertions(+), 36 deletions(-)

diff --git a/ghcide/src/Development/IDE/Core/Rules.hs b/ghcide/src/Development/IDE/Core/Rules.hs
index 4b383e32ec..2a900fa69c 100644
--- a/ghcide/src/Development/IDE/Core/Rules.hs
+++ b/ghcide/src/Development/IDE/Core/Rules.hs
@@ -140,7 +140,7 @@ import           Module
 import           TcRnMonad                                    (tcg_dependent_files)
 
 import           Ide.Plugin.Properties (HasProperty, KeyNameProxy, Properties, ToHsType, useProperty)
-import           Ide.Types (PluginId)
+import           Ide.Types (PluginId, DynFlagsModifications(dynFlagsModifyGlobal, dynFlagsModifyParser))
 import           Data.Default (def)
 import           Ide.PluginUtils (configForPlugin)
 import           Control.Applicative
@@ -211,10 +211,12 @@ getParsedModuleRule :: Rules ()
 getParsedModuleRule =
   -- this rule does not have early cutoff since all its dependencies already have it
   define $ \GetParsedModule file -> do
-    ModSummaryResult{msrModSummary = ms} <- use_ GetModSummary file
+    ModSummaryResult{msrModSummary = ms'} <- use_ GetModSummary file
     sess <- use_ GhcSession file
     let hsc = hscEnv sess
     opt <- getIdeOptions
+    modify_dflags <- getModifyDynFlags id dynFlagsModifyParser
+    let ms = ms' { ms_hspp_opts = modify_dflags $ ms_hspp_opts ms' }
 
     let dflags    = ms_hspp_opts ms
         mainParse = getParsedModuleDefinition hsc opt file ms
@@ -287,8 +289,8 @@ getParsedModuleWithCommentsRule =
 
     liftIO $ snd <$> getParsedModuleDefinition (hscEnv sess) opt file ms'
 
-getModifyDynFlags :: Action (DynFlags -> DynFlags)
-getModifyDynFlags = maybe id modifyDynFlags <$> getShakeExtra
+getModifyDynFlags :: a -> (DynFlagsModifications -> a) -> Action a
+getModifyDynFlags a f = maybe a (f . dynFlagsMods) <$> getShakeExtra
 
 
 getParsedModuleDefinition
@@ -787,7 +789,7 @@ getModSummaryRule :: Rules ()
 getModSummaryRule = do
     defineEarlyCutoff $ Rule $ \GetModSummary f -> do
         session' <- hscEnv <$> use_ GhcSession f
-        modify_dflags <- getModifyDynFlags
+        modify_dflags <- getModifyDynFlags id dynFlagsModifyGlobal
         let session = session' { hsc_dflags = modify_dflags $ hsc_dflags session' }
         (modTime, mFileContent) <- getFileContents f
         let fp = fromNormalizedFilePath f
diff --git a/ghcide/src/Development/IDE/Core/Service.hs b/ghcide/src/Development/IDE/Core/Service.hs
index 5d010c416c..c11d4cec12 100644
--- a/ghcide/src/Development/IDE/Core/Service.hs
+++ b/ghcide/src/Development/IDE/Core/Service.hs
@@ -31,6 +31,7 @@ import qualified Language.LSP.Types              as LSP
 import           Control.Monad
 import           Development.IDE.Core.Shake
 import Development.IDE.GHC.Compat (DynFlags)
+import Ide.Types (DynFlagsModifications)
 
 
 ------------------------------------------------------------
@@ -39,7 +40,7 @@ import Development.IDE.GHC.Compat (DynFlags)
 -- | Initialise the Compiler Service.
 initialise :: Config
            -> Rules ()
-           -> (DynFlags -> DynFlags)
+           -> DynFlagsModifications
            -> Maybe (LSP.LanguageContextEnv Config)
            -> Logger
            -> Debouncer LSP.NormalizedUri
@@ -48,11 +49,11 @@ initialise :: Config
            -> HieDb
            -> IndexQueue
            -> IO IdeState
-initialise defaultConfig mainRule modifyDynFlags lspEnv logger debouncer options vfs hiedb hiedbChan =
+initialise defaultConfig mainRule dynFlagsMods lspEnv logger debouncer options vfs hiedb hiedbChan =
     shakeOpen
         lspEnv
         defaultConfig
-        modifyDynFlags
+        dynFlagsMods
         logger
         debouncer
         (optShakeProfiling options)
diff --git a/ghcide/src/Development/IDE/Core/Shake.hs b/ghcide/src/Development/IDE/Core/Shake.hs
index 30255ae6e8..be052d3691 100644
--- a/ghcide/src/Development/IDE/Core/Shake.hs
+++ b/ghcide/src/Development/IDE/Core/Shake.hs
@@ -150,6 +150,7 @@ import           Ide.Plugin.Config
 import qualified Ide.PluginUtils                      as HLS
 import           Ide.Types                            (PluginId)
 import DynFlags (DynFlags)
+import Ide.Types (DynFlagsModifications)
 
 -- | We need to serialize writes to the database, so we send any function that
 -- needs to write to the database over the channel, where it will be picked up by
@@ -172,7 +173,7 @@ data ShakeExtras = ShakeExtras
      lspEnv :: Maybe (LSP.LanguageContextEnv Config)
     ,debouncer :: Debouncer NormalizedUri
     ,logger :: Logger
-    ,modifyDynFlags :: DynFlags -> DynFlags
+    ,dynFlagsMods :: DynFlagsModifications
     ,globals :: Var (HMap.HashMap TypeRep Dynamic)
     ,state :: Var Values
     ,diagnostics :: Var DiagnosticStore
@@ -456,7 +457,7 @@ seqValue v b = case v of
 -- | Open a 'IdeState', should be shut using 'shakeShut'.
 shakeOpen :: Maybe (LSP.LanguageContextEnv Config)
           -> Config
-          -> (DynFlags -> DynFlags)
+          -> DynFlagsModifications
           -> Logger
           -> Debouncer NormalizedUri
           -> Maybe FilePath
@@ -468,7 +469,7 @@ shakeOpen :: Maybe (LSP.LanguageContextEnv Config)
           -> ShakeOptions
           -> Rules ()
           -> IO IdeState
-shakeOpen lspEnv defaultConfig modifyDynFlags logger debouncer
+shakeOpen lspEnv defaultConfig dynFlagsMods logger debouncer
   shakeProfileDir (IdeReportProgress reportProgress) ideTesting@(IdeTesting testing) hiedb indexQueue vfs opts rules = mdo
 
     us <- mkSplitUniqSupply 'r'
diff --git a/ghcide/src/Development/IDE/Main.hs b/ghcide/src/Development/IDE/Main.hs
index fb36e52522..1655b329ad 100644
--- a/ghcide/src/Development/IDE/Main.hs
+++ b/ghcide/src/Development/IDE/Main.hs
@@ -89,7 +89,6 @@ import           System.IO                             (BufferMode (LineBufferin
 import           System.Time.Extra                     (offsetTime,
                                                         showDuration)
 import           Text.Printf                           (printf)
-import Data.Monoid (Endo(appEndo))
 
 data Command
     = Check [FilePath]  -- ^ Typecheck some paths and print diagnostics. Exit code is the number of failures
@@ -224,7 +223,7 @@ defaultMain Arguments{..} = do
                 initialise
                     argsDefaultHlsConfig
                     rules
-                    (appEndo $ pluginModifyDynflags plugins)
+                    (pluginModifyDynflags plugins)
                     (Just env)
                     logger
                     debouncer
@@ -262,7 +261,7 @@ defaultMain Arguments{..} = do
                         { optCheckParents = pure NeverCheck
                         , optCheckProject = pure False
                         }
-            ide <- initialise argsDefaultHlsConfig rules (appEndo $ pluginModifyDynflags plugins) Nothing logger debouncer options vfs hiedb hieChan
+            ide <- initialise argsDefaultHlsConfig rules (pluginModifyDynflags plugins) Nothing logger debouncer options vfs hiedb hieChan
             shakeSessionInit ide
             registerIdeConfiguration (shakeExtras ide) $ IdeConfiguration mempty (hashed Nothing)
 
@@ -311,7 +310,7 @@ defaultMain Arguments{..} = do
                     { optCheckParents = pure NeverCheck,
                       optCheckProject = pure False
                     }
-            ide <- initialise argsDefaultHlsConfig rules (appEndo $ pluginModifyDynflags plugins) Nothing logger debouncer options vfs hiedb hieChan
+            ide <- initialise argsDefaultHlsConfig rules (pluginModifyDynflags plugins) Nothing logger debouncer options vfs hiedb hieChan
             shakeSessionInit ide
             registerIdeConfiguration (shakeExtras ide) $ IdeConfiguration mempty (hashed Nothing)
             c ide
diff --git a/ghcide/src/Development/IDE/Plugin.hs b/ghcide/src/Development/IDE/Plugin.hs
index ef2d5e319a..95d9f2a226 100644
--- a/ghcide/src/Development/IDE/Plugin.hs
+++ b/ghcide/src/Development/IDE/Plugin.hs
@@ -7,11 +7,12 @@ import           Development.IDE.LSP.Server
 import qualified Language.LSP.Server        as LSP
 import Development.IDE.GHC.Compat (DynFlags)
 import Data.Monoid (Endo)
+import Ide.Types (DynFlagsModifications)
 
 data Plugin c = Plugin
     {pluginRules    :: Rules ()
     ,pluginHandlers :: LSP.Handlers (ServerM c)
-    ,pluginModifyDynflags :: Endo DynFlags
+    ,pluginModifyDynflags :: DynFlagsModifications
     }
 
 instance Default (Plugin c) where
diff --git a/ghcide/src/Development/IDE/Plugin/HLS.hs b/ghcide/src/Development/IDE/Plugin/HLS.hs
index 113d319f04..c957bee171 100644
--- a/ghcide/src/Development/IDE/Plugin/HLS.hs
+++ b/ghcide/src/Development/IDE/Plugin/HLS.hs
@@ -40,7 +40,6 @@ import           UnliftIO                     (MonadUnliftIO)
 import           UnliftIO.Async               (forConcurrently)
 import           UnliftIO.Exception           (catchAny)
 import Development.IDE.GHC.Compat (DynFlags)
-import Data.Monoid (Endo(Endo))
 
 -- ---------------------------------------------------------------------
 --
@@ -71,10 +70,8 @@ rulesPlugins rs = mempty { P.pluginRules = rules }
     where
         rules = foldMap snd rs
 
-dynFlagsPlugins :: [(PluginId, DynFlags -> DynFlags)] -> Plugin Config
-dynFlagsPlugins rs = mempty { P.pluginModifyDynflags = endo }
-    where
-        endo = foldMap (Endo . snd) rs
+dynFlagsPlugins :: [(PluginId, DynFlagsModifications)] -> Plugin Config
+dynFlagsPlugins rs = mempty { P.pluginModifyDynflags = foldMap snd rs }
 
 -- ---------------------------------------------------------------------
 
diff --git a/hls-plugin-api/src/Ide/Types.hs b/hls-plugin-api/src/Ide/Types.hs
index 9e28cbfd77..52ede7dc6e 100644
--- a/hls-plugin-api/src/Ide/Types.hs
+++ b/hls-plugin-api/src/Ide/Types.hs
@@ -57,6 +57,19 @@ import DynFlags (DynFlags)
 newtype IdePlugins ideState = IdePlugins
   { ipMap :: [(PluginId, PluginDescriptor ideState)]}
 
+data DynFlagsModifications =
+  DynFlagsModifications { dynFlagsModifyGlobal :: DynFlags -> DynFlags
+                        , dynFlagsModifyParser :: DynFlags -> DynFlags
+                        }
+
+instance Semigroup DynFlagsModifications where
+  DynFlagsModifications g1 p1 <> DynFlagsModifications g2 p2 =
+    DynFlagsModifications (g2 . g1) (p2 . p1)
+
+instance Monoid DynFlagsModifications where
+  mempty = DynFlagsModifications id id
+
+
 -- ---------------------------------------------------------------------
 
 data PluginDescriptor ideState =
@@ -66,7 +79,7 @@ data PluginDescriptor ideState =
                    , pluginHandlers     :: PluginHandlers ideState
                    , pluginConfigDescriptor :: ConfigDescriptor
                    , pluginNotificationHandlers :: PluginNotificationHandlers ideState
-                   , pluginModifyDynflags :: DynFlags -> DynFlags
+                   , pluginModifyDynflags :: DynFlagsModifications
                    }
 
 -- | An existential wrapper of 'Properties'
@@ -299,7 +312,7 @@ defaultPluginDescriptor plId =
     mempty
     defaultConfigDescriptor
     mempty
-    id
+    mempty
 
 newtype CommandId = CommandId T.Text
   deriving (Show, Read, Eq, Ord)
diff --git a/plugins/hls-tactics-plugin/src/Wingman/StaticPlugin.hs b/plugins/hls-tactics-plugin/src/Wingman/StaticPlugin.hs
index b26080fb23..af054ccd6c 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/StaticPlugin.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/StaticPlugin.hs
@@ -7,21 +7,24 @@ module Wingman.StaticPlugin
   , pattern MetaprogramSyntax
   ) where
 
-import           Data.Data
-import           Development.IDE.GHC.Compat
-import           GHC.LanguageExtensions.Type (Extension(EmptyCase, QuasiQuotes))
-import           Generics.SYB
-import           GhcPlugins hiding ((<>))
-
-
-staticPlugin :: DynFlags -> DynFlags
-staticPlugin df
-  = allowEmptyCaseButWithWarning
-  $ enableQuasiQuotes
-  $ df
+import Data.Data
+import Development.IDE.GHC.Compat
+import GHC.LanguageExtensions.Type (Extension(EmptyCase, QuasiQuotes))
+import Generics.SYB
+import GhcPlugins hiding ((<>))
+import Ide.Types
+
+
+staticPlugin :: DynFlagsModifications
+staticPlugin = DynFlagsModifications
+  { dynFlagsModifyGlobal =
+      \df -> allowEmptyCaseButWithWarning
+           $ df
 #if __GLASGOW_HASKELL__ >= 808
-    { staticPlugins = staticPlugins df <> [metaprogrammingPlugin] }
+             { staticPlugins = staticPlugins df <> [metaprogrammingPlugin] }
 #endif
+  , dynFlagsModifyParser = enableQuasiQuotes
+  }
 
 
 pattern MetaprogramSourceText :: SourceText

From 4cf4a799d7561dfcb5b4765a50025f265483d365 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Thu, 6 May 2021 14:10:38 -0700
Subject: [PATCH 45/52] More hlint

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

diff --git a/ghcide/src/Development/IDE/Core/Shake.hs b/ghcide/src/Development/IDE/Core/Shake.hs
index be052d3691..39c6c42525 100644
--- a/ghcide/src/Development/IDE/Core/Shake.hs
+++ b/ghcide/src/Development/IDE/Core/Shake.hs
@@ -148,9 +148,8 @@ import           Data.Default
 import           HieDb.Types
 import           Ide.Plugin.Config
 import qualified Ide.PluginUtils                      as HLS
-import           Ide.Types                            (PluginId)
+import           Ide.Types                            (PluginId, DynFlagsModifications)
 import DynFlags (DynFlags)
-import Ide.Types (DynFlagsModifications)
 
 -- | We need to serialize writes to the database, so we send any function that
 -- needs to write to the database over the channel, where it will be picked up by

From 64350ddcddaf2693245177c1ea91f04dfa78297b Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Sat, 8 May 2021 14:31:18 -0700
Subject: [PATCH 46/52] Use modified dynflags for parser with comments

---
 ghcide/src/Development/IDE/Core/Rules.hs | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/ghcide/src/Development/IDE/Core/Rules.hs b/ghcide/src/Development/IDE/Core/Rules.hs
index 2a900fa69c..a021d0414f 100644
--- a/ghcide/src/Development/IDE/Core/Rules.hs
+++ b/ghcide/src/Development/IDE/Core/Rules.hs
@@ -286,8 +286,10 @@ getParsedModuleWithCommentsRule =
     opt <- getIdeOptions
 
     let ms' = withoutOption Opt_Haddock $ withOption Opt_KeepRawTokenStream ms
+    modify_dflags <- getModifyDynFlags id dynFlagsModifyParser
+    let ms = ms' { ms_hspp_opts = modify_dflags $ ms_hspp_opts ms' }
 
-    liftIO $ snd <$> getParsedModuleDefinition (hscEnv sess) opt file ms'
+    liftIO $ snd <$> getParsedModuleDefinition (hscEnv sess) opt file ms
 
 getModifyDynFlags :: a -> (DynFlagsModifications -> a) -> Action a
 getModifyDynFlags a f = maybe a (f . dynFlagsMods) <$> getShakeExtra

From 5ee9c1f9371cf54e8eb4aa040b5d8f45b96f764e Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Sat, 8 May 2021 14:31:50 -0700
Subject: [PATCH 47/52] Allow running custom code blocks

---
 .../src/Wingman/Judgements/SYB.hs             | 21 +++++--
 .../src/Wingman/LanguageServer.hs             | 55 ++++++++++---------
 .../src/Wingman/LanguageServer/Metaprogram.hs | 34 +++++-------
 .../Wingman/LanguageServer/TacticProviders.hs | 54 +++++++++---------
 .../src/Wingman/Machinery.hs                  | 10 ++++
 .../src/Wingman/Metaprogramming/Parser.hs     |  7 ++-
 .../hls-tactics-plugin/src/Wingman/Types.hs   | 14 ++++-
 7 files changed, 111 insertions(+), 84 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Wingman/Judgements/SYB.hs b/plugins/hls-tactics-plugin/src/Wingman/Judgements/SYB.hs
index c1b5fe63c6..0365e5e392 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Judgements/SYB.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Judgements/SYB.hs
@@ -4,12 +4,15 @@
 -- | Custom SYB traversals
 module Wingman.Judgements.SYB where
 
-import Data.Foldable (foldl')
-import Data.Generics hiding (typeRep)
-import Development.IDE.GHC.Compat
-import GHC.Exts (Any)
-import Type.Reflection
-import Unsafe.Coerce (unsafeCoerce)
+import           Data.Foldable (foldl')
+import           Data.Generics hiding (typeRep)
+import qualified Data.Text as T
+import           Development.IDE.GHC.Compat
+import           GHC.Exts (Any)
+import           GhcPlugins (unpackFS)
+import           Type.Reflection
+import           Unsafe.Coerce (unsafeCoerce)
+import           Wingman.StaticPlugin (pattern WingmanMetaprogram)
 
 
 ------------------------------------------------------------------------------
@@ -81,3 +84,9 @@ sameTypeModuloLastApp =
             Nothing    -> False
         _ -> False
 
+
+metaprogramQ :: SrcSpan -> GenericQ [(SrcSpan, T.Text)]
+metaprogramQ ss = everythingContaining ss $ mkQ mempty $ \case
+  L new_span (WingmanMetaprogram program) -> pure (new_span, T.pack $ unpackFS $ program)
+  (_ :: LHsExpr GhcTc) -> mempty
+
diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
index 9ce79bf54d..9c3372a880 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
@@ -10,16 +10,18 @@ module Wingman.LanguageServer where
 import           ConLike
 import           Control.Arrow ((***))
 import           Control.Monad
+import           Control.Monad.IO.Class
+import           Control.Monad.RWS
 import           Control.Monad.State (State, evalState)
 import           Control.Monad.Trans.Maybe
 import           Data.Bifunctor (first)
 import           Data.Coerce
 import           Data.Functor ((<&>))
+import           Data.Functor.Identity (runIdentity)
 import qualified Data.HashMap.Strict as Map
 import           Data.IORef (readIORef)
 import qualified Data.Map as M
 import           Data.Maybe
-import           Data.Monoid
 import           Data.Set (Set)
 import qualified Data.Set as S
 import qualified Data.Text as T
@@ -46,28 +48,25 @@ import qualified Ide.Plugin.Config as Plugin
 import           Ide.Plugin.Properties
 import           Ide.PluginUtils (usePropertyLsp)
 import           Ide.Types (PluginId)
+import           Language.Haskell.GHC.ExactPrint (Transform)
+import           Language.Haskell.GHC.ExactPrint (modifyAnnsT, addAnnotationsForPretty)
 import           Language.LSP.Server (MonadLsp, sendNotification)
 import           Language.LSP.Types
 import           Language.LSP.Types.Capabilities
 import           OccName
 import           Prelude hiding (span)
+import           Retrie (transformA)
 import           SrcLoc (containsSpan)
 import           TcRnTypes (tcg_binds, TcGblEnv)
 import           Wingman.Context
 import           Wingman.FeatureSet
 import           Wingman.GHC
 import           Wingman.Judgements
-import           Wingman.Judgements.SYB (everythingContaining)
+import           Wingman.Judgements.SYB (everythingContaining, metaprogramQ)
 import           Wingman.Judgements.Theta
 import           Wingman.Range
-import           Wingman.StaticPlugin (pattern WingmanMetaprogram, pattern MetaprogramSyntax, metaprogramHoleName)
+import           Wingman.StaticPlugin (pattern WingmanMetaprogram, pattern MetaprogramSyntax)
 import           Wingman.Types
-import Control.Monad.IO.Class
-import Control.Monad.RWS
-import Language.Haskell.GHC.ExactPrint (modifyAnnsT, addAnnotationsForPretty)
-import Retrie (transformA)
-import Language.Haskell.GHC.ExactPrint (Transform)
-import Data.Functor.Identity (runIdentity)
 
 
 tacticDesc :: T.Text -> T.Text
@@ -190,14 +189,6 @@ getAllMetaprograms = everything (<>) $ mkQ mempty $ \case
   (_ :: HsExpr GhcTc)  -> mempty
 
 
-data HoleJudgment = HoleJudgment
-  { hj_range     :: Tracked 'Current Range
-  , hj_jdg       :: Judgement
-  , hj_ctx       :: Context
-  , hj_dflags    :: DynFlags
-  , hj_hole_sort :: HoleSort
-  }
-
 ------------------------------------------------------------------------------
 -- | Find the last typechecked module, and find the most specific span, as well
 -- as the judgement at the given range.
@@ -216,13 +207,16 @@ judgementForHole state nfp range cfg = do
     HAR _ (unsafeCopyAge asts -> hf) _ _ HieFresh -> do
       range' <- liftMaybe $ mapAgeFrom amapping range
       binds <- stale GetBindings
-      tcg <- fmap (fmap tmrTypechecked)
+      tcg@(TrackedStale tcg_t tcg_map)
+          <- fmap (fmap tmrTypechecked)
            $ stale TypeCheck
 
       hscenv <- stale GhcSessionDeps
 
-      (rss, occ, g) <- liftMaybe $ getSpanAndTypeAtHole range' hf
+      (rss, g) <- liftMaybe $ getSpanAndTypeAtHole range' hf
+
       new_rss <- liftMaybe $ mapAgeTo amapping rss
+      tcg_rss <- liftMaybe $ mapAgeFrom tcg_map new_rss
 
       -- KnownThings is just the instances in scope. There are no ranges
       -- involved, so it's not crucial to track ages.
@@ -231,6 +225,7 @@ judgementForHole state nfp range cfg = do
       kt <- knownThings (untrackedStaleValue tcg) henv
 
       (jdg, ctx) <- liftMaybe $ mkJudgementAndContext cfg g binds new_rss tcg eps kt
+      let mp = getMetaprogramAtSpan (fmap RealSrcSpan tcg_rss) tcg_t
 
       dflags <- getIdeDynflags state nfp
       pure $ HoleJudgment
@@ -238,13 +233,12 @@ judgementForHole state nfp range cfg = do
         , hj_jdg = jdg
         , hj_ctx = ctx
         , hj_dflags = dflags
-        , hj_hole_sort = classifyHoleName occ
+        , hj_hole_sort = holeSortFor mp
         }
 
 
-classifyHoleName :: OccName -> HoleSort
-classifyHoleName occ | occ == metaprogramHoleName = Metaprogram
-classifyHoleName _ = Hole
+holeSortFor :: Maybe T.Text -> HoleSort
+holeSortFor = maybe Hole Metaprogram
 
 
 mkJudgementAndContext
@@ -305,7 +299,7 @@ getAlreadyDestructed (unTrack -> span) (unTrack -> binds) =
 getSpanAndTypeAtHole
     :: Tracked age Range
     -> Tracked age (HieASTs b)
-    -> Maybe (Tracked age RealSrcSpan, OccName, b)
+    -> Maybe (Tracked age RealSrcSpan, b)
 getSpanAndTypeAtHole r@(unTrack -> range) (unTrack -> hf) = do
   join $ listToMaybe $ M.elems $ flip M.mapWithKey (getAsts hf) $ \fs ast ->
     case selectSmallestContaining (rangeToRealSrcSpan (FastString.unpackFS fs) range) ast of
@@ -321,7 +315,7 @@ getSpanAndTypeAtHole r@(unTrack -> range) (unTrack -> hf) = do
              . M.keysSet
              $ nodeIdentifiers info
         guard $ isHole occ
-        pure (unsafeCopyAge r $ nodeSpan ast', occ, ty)
+        pure (unsafeCopyAge r $ nodeSpan ast', ty)
 
 
 
@@ -591,3 +585,14 @@ annotateMetaprograms = everywhereM $ mkM $ \case
     pure x
   (x :: LHsExpr GhcPs) -> pure x
 
+getMetaprogramAtSpan
+    :: Tracked age SrcSpan
+    -> Tracked age TcGblEnv
+    -> Maybe T.Text
+getMetaprogramAtSpan (unTrack -> ss)
+  = fmap snd
+  . listToMaybe
+  . metaprogramQ ss
+  . tcg_binds
+  . unTrack
+
diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/Metaprogram.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/Metaprogram.hs
index a234f4d893..37e8581928 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/Metaprogram.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/Metaprogram.hs
@@ -4,17 +4,16 @@
 {-# LANGUAGE NoMonoLocalBinds  #-}
 {-# LANGUAGE RankNTypes #-}
 
-module Wingman.LanguageServer.Metaprogram (hoverProvider) where
+module Wingman.LanguageServer.Metaprogram
+  ( hoverProvider
+  ) where
 
 import           Control.Applicative (empty)
 import           Control.Monad
 import           Control.Monad.Trans
 import           Control.Monad.Trans.Maybe
-import           Data.Generics.Aliases (mkQ, GenericQ)
-import           Data.Generics.Schemes (everything)
 import           Data.List (find)
 import           Data.Maybe
-import           Data.Monoid
 import qualified Data.Text as T
 import           Data.Traversable
 import           Development.IDE (positionToRealSrcLoc)
@@ -23,34 +22,34 @@ import           Development.IDE.Core.RuleTypes
 import           Development.IDE.Core.Shake (IdeState (..))
 import           Development.IDE.Core.UseStale
 import           Development.IDE.GHC.Compat
-import           GhcPlugins (unpackFS, containsSpan, realSrcLocSpan)
+import           GhcPlugins (containsSpan, realSrcLocSpan)
 import           Ide.Types
 import           Language.LSP.Types
 import           Prelude hiding (span)
 import           Prelude hiding (span)
 import           TcRnTypes (tcg_binds)
 import           Wingman.GHC
-import           Wingman.LanguageServer
+import           Wingman.Judgements.SYB (metaprogramQ)
 import           Wingman.Metaprogramming.Parser (attempt_it)
-import           Wingman.StaticPlugin (pattern WingmanMetaprogram)
-import Wingman.Judgements.SYB (everythingContaining)
+import           Wingman.LanguageServer
+import           Wingman.Types
 
 
 ------------------------------------------------------------------------------
 -- | Provide the "empty case completion" code lens
 hoverProvider :: PluginMethodHandler IdeState TextDocumentHover
-hoverProvider state plId (HoverParams (TextDocumentIdentifier uri) pos _)
+hoverProvider state plId (HoverParams (TextDocumentIdentifier uri) (unsafeMkCurrent -> pos) _)
   | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do
-      let loc = positionToRealSrcLoc nfp pos
+      let loc = fmap (realSrcLocSpan . positionToRealSrcLoc nfp) pos
 
       cfg <- getTacticConfig plId
       liftIO $ fromMaybeT (Right Nothing) $ do
         -- guard $ hasFeature FeatureEmptyCase $ cfg_feature_set cfg
 
-        holes <- emptyCaseScrutinees state nfp $ RealSrcSpan $ realSrcLocSpan loc
+        holes <- getMetaprogramsAtSpan state nfp $ RealSrcSpan $ unTrack loc
 
         fmap (Right . Just) $
-          case (find (flip containsSpan (realSrcLocSpan loc) . unTrack . fst) holes) of
+          case (find (flip containsSpan (unTrack loc) . unTrack . fst) holes) of
             Just (trss, program) -> do
               let tr_range = fmap realSrcSpanToRange trss
               HoleJudgment{hj_jdg=jdg, hj_ctx=ctx} <- judgementForHole state nfp tr_range cfg
@@ -70,13 +69,13 @@ fromMaybeT :: Functor m => a -> MaybeT m a -> m a
 fromMaybeT def = fmap (fromMaybe def) . runMaybeT
 
 
-emptyCaseScrutinees
+getMetaprogramsAtSpan
     :: IdeState
     -> NormalizedFilePath
     -> SrcSpan
     -> MaybeT IO [(Tracked 'Current RealSrcSpan, T.Text)]
-emptyCaseScrutinees state nfp ss = do
-    let stale a = runStaleIde "emptyCaseScrutinees" state nfp a
+getMetaprogramsAtSpan state nfp ss = do
+    let stale a = runStaleIde "getMetaprogramsAtSpan" state nfp a
 
     TrackedStale tcg tcg_map <- fmap (fmap tmrTypechecked) $ stale TypeCheck
 
@@ -89,8 +88,3 @@ emptyCaseScrutinees state nfp ss = do
         UnhelpfulSpan _ -> empty
 
 
-metaprogramQ :: SrcSpan -> GenericQ [(SrcSpan, T.Text)]
-metaprogramQ ss = everythingContaining ss $ mkQ mempty $ \case
-  L new_span (WingmanMetaprogram program) -> pure (new_span, T.pack $ unpackFS $ program)
-  (_ :: LHsExpr GhcTc) -> mempty
-
diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs
index 2243e3d15f..5f6fd62ceb 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs
@@ -35,6 +35,8 @@ import           Wingman.Auto
 import           Wingman.FeatureSet
 import           Wingman.GHC
 import           Wingman.Judgements
+import           Wingman.Machinery (useNameFromHypothesis)
+import           Wingman.Metaprogramming.Parser (parseMetaprogram)
 import           Wingman.Tactics
 import           Wingman.Types
 
@@ -53,7 +55,7 @@ commandTactic DestructAll            = const destructAll
 commandTactic UseDataCon             = userSplit
 commandTactic Refine                 = const refine
 commandTactic BeginMetaprogram       = const metaprogram
-commandTactic RunMetaprogram         = const $ pure ()
+commandTactic RunMetaprogram         = parseMetaprogram .T.pack . occNameString
 
 
 ------------------------------------------------------------------------------
@@ -101,44 +103,44 @@ mkTacticKind =
 -- 'filterGoalType' and 'filterBindingType' for the nitty gritty.
 commandProvider :: TacticCommand -> TacticProvider
 commandProvider Auto  =
-  requireHoleSort Hole $
+  requireHoleSort (== Hole) $
   provide Auto ""
 commandProvider Intros =
-  requireHoleSort Hole $
+  requireHoleSort (== Hole) $
   filterGoalType isFunction $
     provide Intros ""
 commandProvider Destruct =
-  requireHoleSort Hole $
+  requireHoleSort (== Hole) $
   filterBindingType destructFilter $ \occ _ ->
     provide Destruct $ T.pack $ occNameString occ
 commandProvider DestructPun =
-  requireHoleSort Hole $
+  requireHoleSort (== Hole) $
   requireFeature FeatureDestructPun $
     filterBindingType destructPunFilter $ \occ _ ->
       provide DestructPun $ T.pack $ occNameString occ
 commandProvider Homomorphism =
-  requireHoleSort Hole $
+  requireHoleSort (== Hole) $
   filterBindingType homoFilter $ \occ _ ->
     provide Homomorphism $ T.pack $ occNameString occ
 commandProvider DestructLambdaCase =
-  requireHoleSort Hole $
+  requireHoleSort (== Hole) $
   requireExtension LambdaCase $
     filterGoalType (isJust . lambdaCaseable) $
       provide DestructLambdaCase ""
 commandProvider HomomorphismLambdaCase =
-  requireHoleSort Hole $
+  requireHoleSort (== Hole) $
   requireExtension LambdaCase $
     filterGoalType ((== Just True) . lambdaCaseable) $
       provide HomomorphismLambdaCase ""
 commandProvider DestructAll =
-  requireHoleSort Hole $
+  requireHoleSort (== Hole) $
   requireFeature FeatureDestructAll $
     withJudgement $ \jdg ->
       case _jIsTopHole jdg && jHasBoundArgs jdg of
         True  -> provide DestructAll ""
         False -> mempty
 commandProvider UseDataCon =
-  requireHoleSort Hole $
+  requireHoleSort (== Hole) $
   withConfig $ \cfg ->
     requireFeature FeatureUseDataCon $
       filterTypeProjection
@@ -153,17 +155,17 @@ commandProvider UseDataCon =
           . occName
           $ dataConName dcon
 commandProvider Refine =
-  requireHoleSort Hole $
+  requireHoleSort (== Hole) $
   requireFeature FeatureRefineHole $
     provide Refine ""
 commandProvider BeginMetaprogram =
-  requireHoleSort Hole $
+  requireHoleSort (== Hole) $
   -- requireFeature FeatureMetaprogram $
     provide BeginMetaprogram ""
 commandProvider RunMetaprogram =
-  requireHoleSort Metaprogram $
+  withMetaprogram $ \mp ->
   -- requireFeature FeatureMetaprogram $
-    provide RunMetaprogram ""
+    provide RunMetaprogram mp
 
 
 ------------------------------------------------------------------------------
@@ -210,12 +212,18 @@ requireFeature f tp tpd =
     False -> pure []
 
 
-requireHoleSort :: HoleSort -> TacticProvider -> TacticProvider
-requireHoleSort hs tp tpd =
-  case (== hs) $ tpd_hole_sort tpd of
+requireHoleSort :: (HoleSort -> Bool) -> TacticProvider -> TacticProvider
+requireHoleSort p tp tpd =
+  case p $ tpd_hole_sort tpd of
     True  -> tp tpd
     False -> pure []
 
+withMetaprogram :: (T.Text -> TacticProvider) -> TacticProvider
+withMetaprogram tp tpd =
+  case tpd_hole_sort tpd of
+    Metaprogram mp -> tp mp tpd
+    _ -> pure []
+
 
 ------------------------------------------------------------------------------
 -- | Restrict a 'TacticProvider', making sure it appears only when the given
@@ -280,18 +288,6 @@ withConfig :: (Config -> TacticProvider) -> TacticProvider
 withConfig tp tpd = tp (tpd_config tpd) tpd
 
 
-
-------------------------------------------------------------------------------
--- | 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.
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs b/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs
index c87e2bcbee..d0f5368e47 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs
@@ -305,3 +305,13 @@ try' t = commit t $ pure ()
 exact :: HsExpr GhcPs -> TacticsM ()
 exact = rule . const . pure . pure . noLoc
 
+------------------------------------------------------------------------------
+-- | 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
+
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
index 8b66a336b6..c9f26aa10a 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
@@ -12,11 +12,11 @@ import qualified Data.Text as T
 import qualified Refinery.Tactic as R
 import qualified Text.Megaparsec as P
 import           Wingman.Auto
-import           Wingman.LanguageServer.TacticProviders (useNameFromHypothesis)
+import           Wingman.Machinery (useNameFromHypothesis)
 import           Wingman.Metaprogramming.Lexer
+import           Wingman.Metaprogramming.ProofState (proofState, layout)
 import           Wingman.Tactics
 import           Wingman.Types
-import Wingman.Metaprogramming.ProofState (proofState, layout)
 
 
 nullary :: T.Text -> TacticsM () -> Parser (TacticsM ())
@@ -96,3 +96,6 @@ attempt_it ctx jdg program =
           Left tes -> Left $ wrapError $ show tes
           Right rtr -> Right $ layout $ proofState rtr
 
+parseMetaprogram :: T.Text -> TacticsM ()
+parseMetaprogram = either (const $ pure ()) id . P.runParser tacticProgram "<splice>"
+
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Types.hs b/plugins/hls-tactics-plugin/src/Wingman/Types.hs
index 783c18ed23..657b6ad4c8 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Types.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Types.hs
@@ -39,6 +39,8 @@ import           UniqSupply (takeUniqFromSupply, mkSplitUniqSupply, UniqSupply)
 import           Unique (nonDetCmpUnique, Uniquable, getUnique, Unique)
 import           Wingman.Debug
 import           Wingman.FeatureSet
+import Development.IDE.Core.UseStale
+import Development.IDE (Range)
 
 
 ------------------------------------------------------------------------------
@@ -508,6 +510,14 @@ instance Show UserFacingMessage where
   show (InfrastructureError t) = "Internal error: " <> T.unpack t
 
 
-data HoleSort = Hole | Metaprogram
-  deriving (Eq, Ord, Show, Enum, Bounded)
+data HoleSort = Hole | Metaprogram T.Text
+  deriving (Eq, Ord, Show)
+
+data HoleJudgment = HoleJudgment
+  { hj_range     :: Tracked 'Current Range
+  , hj_jdg       :: Judgement
+  , hj_ctx       :: Context
+  , hj_dflags    :: DynFlags
+  , hj_hole_sort :: HoleSort
+  }
 

From 1dce53e48d4730cedfe3faedba081d08b8bbb65a Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Sat, 8 May 2021 14:36:06 -0700
Subject: [PATCH 48/52] Don't assume tactic providers use occnames

---
 .../src/Wingman/LanguageServer/TacticProviders.hs | 15 ++++++---------
 plugins/hls-tactics-plugin/src/Wingman/Plugin.hs  |  9 ++++++---
 2 files changed, 12 insertions(+), 12 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs
index 5f6fd62ceb..2a77a28b1e 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs
@@ -11,11 +11,9 @@ module Wingman.LanguageServer.TacticProviders
   ) where
 
 import           Control.Monad
-import           Control.Monad.Error.Class (MonadError (throwError))
 import           Data.Aeson
 import           Data.Bool (bool)
 import           Data.Coerce
-import qualified Data.Map as M
 import           Data.Maybe
 import           Data.Monoid
 import qualified Data.Text as T
@@ -30,7 +28,6 @@ import           Ide.Types
 import           Language.LSP.Types
 import           OccName
 import           Prelude hiding (span)
-import           Refinery.Tactic (goal)
 import           Wingman.Auto
 import           Wingman.FeatureSet
 import           Wingman.GHC
@@ -43,19 +40,19 @@ import           Wingman.Types
 
 ------------------------------------------------------------------------------
 -- | A mapping from tactic commands to actual tactics for refinery.
-commandTactic :: TacticCommand -> OccName -> TacticsM ()
+commandTactic :: TacticCommand -> T.Text -> TacticsM ()
 commandTactic Auto                   = const auto
 commandTactic Intros                 = const intros
-commandTactic Destruct               = useNameFromHypothesis destruct
-commandTactic DestructPun            = useNameFromHypothesis destructPun
-commandTactic Homomorphism           = useNameFromHypothesis homo
+commandTactic Destruct               = useNameFromHypothesis destruct . mkVarOcc . T.unpack
+commandTactic DestructPun            = useNameFromHypothesis destructPun . mkVarOcc . T.unpack
+commandTactic Homomorphism           = useNameFromHypothesis homo . mkVarOcc . T.unpack
 commandTactic DestructLambdaCase     = const destructLambdaCase
 commandTactic HomomorphismLambdaCase = const homoLambdaCase
 commandTactic DestructAll            = const destructAll
-commandTactic UseDataCon             = userSplit
+commandTactic UseDataCon             = userSplit . mkVarOcc . T.unpack
 commandTactic Refine                 = const refine
 commandTactic BeginMetaprogram       = const metaprogram
-commandTactic RunMetaprogram         = parseMetaprogram .T.pack . occNameString
+commandTactic RunMetaprogram         = parseMetaprogram
 
 
 ------------------------------------------------------------------------------
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs b/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs
index 8623c1b9c2..9f0c0ecce3 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs
@@ -33,13 +33,13 @@ import           Wingman.CaseSplit
 import           Wingman.EmptyCase
 import           Wingman.GHC
 import           Wingman.LanguageServer
+import           Wingman.LanguageServer.Metaprogram (hoverProvider)
 import           Wingman.LanguageServer.TacticProviders
 import           Wingman.Machinery (scoreSolution)
 import           Wingman.Range
 import           Wingman.StaticPlugin
 import           Wingman.Tactics
 import           Wingman.Types
-import Wingman.LanguageServer.Metaprogram (hoverProvider)
 
 
 descriptor :: PluginId -> PluginDescriptor IdeState
@@ -100,7 +100,10 @@ showUserFacingMessage ufm = do
   pure $ Left $ mkErr InternalError $ T.pack $ show ufm
 
 
-tacticCmd :: (OccName -> TacticsM ()) -> PluginId -> CommandFunction IdeState TacticParams
+tacticCmd
+    :: (T.Text -> TacticsM ())
+    -> PluginId
+    -> CommandFunction IdeState TacticParams
 tacticCmd tac pId state (TacticParams uri range var_name)
   | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do
       let stale a = runStaleIde "tacticCmd" state nfp a
@@ -114,7 +117,7 @@ tacticCmd tac pId state (TacticParams uri range var_name)
         pm_span <- liftMaybe $ mapAgeFrom pmmap span
 
         timingOut (cfg_timeout_seconds cfg * seconds) $ join $
-          case runTactic hj_ctx hj_jdg $ tac $ mkVarOcc $ T.unpack var_name of
+          case runTactic hj_ctx hj_jdg $ tac var_name of
             Left _ -> Left TacticErrors
             Right rtr ->
               case rtr_extract rtr of

From 37ac02bfda295a55a8fceb46a1cb8d29e9faedb0 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Tue, 11 May 2021 19:35:30 -0700
Subject: [PATCH 49/52] Revert changes to ghcide

---
 .../session-loader/Development/IDE/Session.hs | 11 ++++++++++
 ghcide/src/Development/IDE/Core/Rules.hs      | 20 +++++--------------
 ghcide/src/Development/IDE/Core/Service.hs    |  6 +-----
 ghcide/src/Development/IDE/Core/Shake.hs      |  9 +++------
 ghcide/src/Development/IDE/Main.hs            |  7 +++----
 ghcide/src/Development/IDE/Plugin.hs          |  8 ++------
 ghcide/src/Development/IDE/Plugin/HLS.hs      | 16 +++++----------
 ghcide/src/Development/IDE/Plugin/Test.hs     |  8 +++-----
 hls-plugin-api/hls-plugin-api.cabal           |  1 -
 hls-plugin-api/src/Ide/Types.hs               | 16 ---------------
 10 files changed, 33 insertions(+), 69 deletions(-)

diff --git a/ghcide/session-loader/Development/IDE/Session.hs b/ghcide/session-loader/Development/IDE/Session.hs
index 449d6bd3f2..4ccbe0fa93 100644
--- a/ghcide/session-loader/Development/IDE/Session.hs
+++ b/ghcide/session-loader/Development/IDE/Session.hs
@@ -84,6 +84,7 @@ import           Control.Concurrent.STM               (atomically)
 import           Control.Concurrent.STM.TQueue
 import qualified Data.HashSet                         as Set
 import           Database.SQLite.Simple
+import           GHC.LanguageExtensions               (Extension (EmptyCase))
 import           HieDb.Create
 import           HieDb.Types
 import           HieDb.Utils
@@ -793,6 +794,7 @@ setOptions (ComponentOptions theOpts compRoot _) dflags = do
           setIgnoreInterfacePragmas $
           setLinkerOptions $
           disableOptimisation $
+          allowEmptyCaseButWithWarning $
           setUpTypedHoles $
           makeDynFlagsAbsolute compRoot dflags'
     -- initPackages parses the -package flags and
@@ -801,6 +803,15 @@ setOptions (ComponentOptions theOpts compRoot _) dflags = do
     (final_df, _) <- liftIO $ wrapPackageSetupException $ initPackages dflags''
     return (final_df, targets)
 
+
+-- | Wingman wants to support destructing of empty cases, but these are a parse
+-- error by default. So we want to enable 'EmptyCase', but then that leads to
+-- silent errors without 'Opt_WarnIncompletePatterns'.
+allowEmptyCaseButWithWarning :: DynFlags -> DynFlags
+allowEmptyCaseButWithWarning =
+  flip xopt_set EmptyCase . flip wopt_set Opt_WarnIncompletePatterns
+
+
 -- we don't want to generate object code so we compile to bytecode
 -- (HscInterpreted) which implies LinkInMemory
 -- HscInterpreted
diff --git a/ghcide/src/Development/IDE/Core/Rules.hs b/ghcide/src/Development/IDE/Core/Rules.hs
index a021d0414f..d4525d8dd3 100644
--- a/ghcide/src/Development/IDE/Core/Rules.hs
+++ b/ghcide/src/Development/IDE/Core/Rules.hs
@@ -111,7 +111,7 @@ import           Development.IDE.GHC.Compat                   hiding
                                                                writeHieFile)
 import           Development.IDE.GHC.Error
 import           Development.IDE.GHC.ExactPrint
-import           Development.IDE.GHC.Util hiding (modifyDynFlags)
+import           Development.IDE.GHC.Util
 import           Development.IDE.Import.DependencyInformation
 import           Development.IDE.Import.FindImports
 import qualified Development.IDE.Spans.AtPoint                as AtPoint
@@ -140,7 +140,7 @@ import           Module
 import           TcRnMonad                                    (tcg_dependent_files)
 
 import           Ide.Plugin.Properties (HasProperty, KeyNameProxy, Properties, ToHsType, useProperty)
-import           Ide.Types (PluginId, DynFlagsModifications(dynFlagsModifyGlobal, dynFlagsModifyParser))
+import           Ide.Types (PluginId)
 import           Data.Default (def)
 import           Ide.PluginUtils (configForPlugin)
 import           Control.Applicative
@@ -211,12 +211,10 @@ getParsedModuleRule :: Rules ()
 getParsedModuleRule =
   -- this rule does not have early cutoff since all its dependencies already have it
   define $ \GetParsedModule file -> do
-    ModSummaryResult{msrModSummary = ms'} <- use_ GetModSummary file
+    ModSummaryResult{msrModSummary = ms} <- use_ GetModSummary file
     sess <- use_ GhcSession file
     let hsc = hscEnv sess
     opt <- getIdeOptions
-    modify_dflags <- getModifyDynFlags id dynFlagsModifyParser
-    let ms = ms' { ms_hspp_opts = modify_dflags $ ms_hspp_opts ms' }
 
     let dflags    = ms_hspp_opts ms
         mainParse = getParsedModuleDefinition hsc opt file ms
@@ -286,14 +284,8 @@ getParsedModuleWithCommentsRule =
     opt <- getIdeOptions
 
     let ms' = withoutOption Opt_Haddock $ withOption Opt_KeepRawTokenStream ms
-    modify_dflags <- getModifyDynFlags id dynFlagsModifyParser
-    let ms = ms' { ms_hspp_opts = modify_dflags $ ms_hspp_opts ms' }
-
-    liftIO $ snd <$> getParsedModuleDefinition (hscEnv sess) opt file ms
-
-getModifyDynFlags :: a -> (DynFlagsModifications -> a) -> Action a
-getModifyDynFlags a f = maybe a (f . dynFlagsMods) <$> getShakeExtra
 
+    liftIO $ snd <$> getParsedModuleDefinition (hscEnv sess) opt file ms'
 
 getParsedModuleDefinition
     :: HscEnv
@@ -790,9 +782,7 @@ isHiFileStableRule = defineEarlyCutoff $ RuleNoDiagnostics $ \IsHiFileStable f -
 getModSummaryRule :: Rules ()
 getModSummaryRule = do
     defineEarlyCutoff $ Rule $ \GetModSummary f -> do
-        session' <- hscEnv <$> use_ GhcSession f
-        modify_dflags <- getModifyDynFlags id dynFlagsModifyGlobal
-        let session = session' { hsc_dflags = modify_dflags $ hsc_dflags session' }
+        session <- hscEnv <$> use_ GhcSession f
         (modTime, mFileContent) <- getFileContents f
         let fp = fromNormalizedFilePath f
         modS <- liftIO $ runExceptT $
diff --git a/ghcide/src/Development/IDE/Core/Service.hs b/ghcide/src/Development/IDE/Core/Service.hs
index c11d4cec12..b03da9fd42 100644
--- a/ghcide/src/Development/IDE/Core/Service.hs
+++ b/ghcide/src/Development/IDE/Core/Service.hs
@@ -30,8 +30,6 @@ import qualified Language.LSP.Types              as LSP
 
 import           Control.Monad
 import           Development.IDE.Core.Shake
-import Development.IDE.GHC.Compat (DynFlags)
-import Ide.Types (DynFlagsModifications)
 
 
 ------------------------------------------------------------
@@ -40,7 +38,6 @@ import Ide.Types (DynFlagsModifications)
 -- | Initialise the Compiler Service.
 initialise :: Config
            -> Rules ()
-           -> DynFlagsModifications
            -> Maybe (LSP.LanguageContextEnv Config)
            -> Logger
            -> Debouncer LSP.NormalizedUri
@@ -49,11 +46,10 @@ initialise :: Config
            -> HieDb
            -> IndexQueue
            -> IO IdeState
-initialise defaultConfig mainRule dynFlagsMods lspEnv logger debouncer options vfs hiedb hiedbChan =
+initialise defaultConfig mainRule lspEnv logger debouncer options vfs hiedb hiedbChan =
     shakeOpen
         lspEnv
         defaultConfig
-        dynFlagsMods
         logger
         debouncer
         (optShakeProfiling options)
diff --git a/ghcide/src/Development/IDE/Core/Shake.hs b/ghcide/src/Development/IDE/Core/Shake.hs
index 39c6c42525..52463e51f6 100644
--- a/ghcide/src/Development/IDE/Core/Shake.hs
+++ b/ghcide/src/Development/IDE/Core/Shake.hs
@@ -147,9 +147,8 @@ import           Control.Exception.Extra                hiding (bracket_)
 import           Data.Default
 import           HieDb.Types
 import           Ide.Plugin.Config
-import qualified Ide.PluginUtils                      as HLS
-import           Ide.Types                            (PluginId, DynFlagsModifications)
-import DynFlags (DynFlags)
+import qualified Ide.PluginUtils                        as HLS
+import           Ide.Types                              (PluginId)
 
 -- | We need to serialize writes to the database, so we send any function that
 -- needs to write to the database over the channel, where it will be picked up by
@@ -172,7 +171,6 @@ data ShakeExtras = ShakeExtras
      lspEnv :: Maybe (LSP.LanguageContextEnv Config)
     ,debouncer :: Debouncer NormalizedUri
     ,logger :: Logger
-    ,dynFlagsMods :: DynFlagsModifications
     ,globals :: Var (HMap.HashMap TypeRep Dynamic)
     ,state :: Var Values
     ,diagnostics :: Var DiagnosticStore
@@ -456,7 +454,6 @@ seqValue v b = case v of
 -- | Open a 'IdeState', should be shut using 'shakeShut'.
 shakeOpen :: Maybe (LSP.LanguageContextEnv Config)
           -> Config
-          -> DynFlagsModifications
           -> Logger
           -> Debouncer NormalizedUri
           -> Maybe FilePath
@@ -468,7 +465,7 @@ shakeOpen :: Maybe (LSP.LanguageContextEnv Config)
           -> ShakeOptions
           -> Rules ()
           -> IO IdeState
-shakeOpen lspEnv defaultConfig dynFlagsMods logger debouncer
+shakeOpen lspEnv defaultConfig logger debouncer
   shakeProfileDir (IdeReportProgress reportProgress) ideTesting@(IdeTesting testing) hiedb indexQueue vfs opts rules = mdo
 
     us <- mkSplitUniqSupply 'r'
diff --git a/ghcide/src/Development/IDE/Main.hs b/ghcide/src/Development/IDE/Main.hs
index 1655b329ad..c3a34415cc 100644
--- a/ghcide/src/Development/IDE/Main.hs
+++ b/ghcide/src/Development/IDE/Main.hs
@@ -46,7 +46,7 @@ import           Development.IDE.Core.Shake            (IdeState (shakeExtras),
 import           Development.IDE.Core.Tracing          (measureMemory)
 import           Development.IDE.Graph                 (action)
 import           Development.IDE.LSP.LanguageServer    (runLanguageServer)
-import           Development.IDE.Plugin                (Plugin (pluginHandlers, pluginRules, pluginModifyDynflags))
+import           Development.IDE.Plugin                (Plugin (pluginHandlers, pluginRules))
 import           Development.IDE.Plugin.HLS            (asGhcIdePlugin)
 import qualified Development.IDE.Plugin.HLS.GhcIde     as Ghcide
 import           Development.IDE.Session               (SessionLoadingOptions,
@@ -223,7 +223,6 @@ defaultMain Arguments{..} = do
                 initialise
                     argsDefaultHlsConfig
                     rules
-                    (pluginModifyDynflags plugins)
                     (Just env)
                     logger
                     debouncer
@@ -261,7 +260,7 @@ defaultMain Arguments{..} = do
                         { optCheckParents = pure NeverCheck
                         , optCheckProject = pure False
                         }
-            ide <- initialise argsDefaultHlsConfig rules (pluginModifyDynflags plugins) Nothing logger debouncer options vfs hiedb hieChan
+            ide <- initialise argsDefaultHlsConfig rules Nothing logger debouncer options vfs hiedb hieChan
             shakeSessionInit ide
             registerIdeConfiguration (shakeExtras ide) $ IdeConfiguration mempty (hashed Nothing)
 
@@ -310,7 +309,7 @@ defaultMain Arguments{..} = do
                     { optCheckParents = pure NeverCheck,
                       optCheckProject = pure False
                     }
-            ide <- initialise argsDefaultHlsConfig rules (pluginModifyDynflags plugins) Nothing logger debouncer options vfs hiedb hieChan
+            ide <- initialise argsDefaultHlsConfig rules Nothing logger debouncer options vfs hiedb hieChan
             shakeSessionInit ide
             registerIdeConfiguration (shakeExtras ide) $ IdeConfiguration mempty (hashed Nothing)
             c ide
diff --git a/ghcide/src/Development/IDE/Plugin.hs b/ghcide/src/Development/IDE/Plugin.hs
index 95d9f2a226..c29e6a5470 100644
--- a/ghcide/src/Development/IDE/Plugin.hs
+++ b/ghcide/src/Development/IDE/Plugin.hs
@@ -5,21 +5,17 @@ import           Development.IDE.Graph
 
 import           Development.IDE.LSP.Server
 import qualified Language.LSP.Server        as LSP
-import Development.IDE.GHC.Compat (DynFlags)
-import Data.Monoid (Endo)
-import Ide.Types (DynFlagsModifications)
 
 data Plugin c = Plugin
     {pluginRules    :: Rules ()
     ,pluginHandlers :: LSP.Handlers (ServerM c)
-    ,pluginModifyDynflags :: DynFlagsModifications
     }
 
 instance Default (Plugin c) where
-    def = Plugin mempty mempty mempty
+    def = Plugin mempty mempty
 
 instance Semigroup (Plugin c) where
-    Plugin x1 h1 d1 <> Plugin x2 h2 d2 = Plugin (x1<>x2) (h1 <> h2) (d1 <> d2)
+    Plugin x1 h1 <> Plugin x2 h2 = Plugin (x1<>x2) (h1 <> h2)
 
 instance Monoid (Plugin c) where
     mempty = def
diff --git a/ghcide/src/Development/IDE/Plugin/HLS.hs b/ghcide/src/Development/IDE/Plugin/HLS.hs
index c957bee171..c208a2c21e 100644
--- a/ghcide/src/Development/IDE/Plugin/HLS.hs
+++ b/ghcide/src/Development/IDE/Plugin/HLS.hs
@@ -26,7 +26,6 @@ import           Development.IDE.Core.Shake
 import           Development.IDE.Core.Tracing
 import           Development.IDE.LSP.Server
 import           Development.IDE.Plugin
-import qualified Development.IDE.Plugin       as P
 import           Development.IDE.Types.Logger
 import           Development.IDE.Graph            (Rules)
 import           Ide.Plugin.Config
@@ -39,7 +38,6 @@ import           Text.Regex.TDFA.Text         ()
 import           UnliftIO                     (MonadUnliftIO)
 import           UnliftIO.Async               (forConcurrently)
 import           UnliftIO.Exception           (catchAny)
-import Development.IDE.GHC.Compat (DynFlags)
 
 -- ---------------------------------------------------------------------
 --
@@ -50,8 +48,7 @@ asGhcIdePlugin (IdePlugins ls) =
     mkPlugin rulesPlugins HLS.pluginRules <>
     mkPlugin executeCommandPlugins HLS.pluginCommands <>
     mkPlugin extensiblePlugins HLS.pluginHandlers <>
-    mkPlugin extensibleNotificationPlugins HLS.pluginNotificationHandlers <>
-    mkPlugin dynFlagsPlugins HLS.pluginModifyDynflags
+    mkPlugin extensibleNotificationPlugins HLS.pluginNotificationHandlers
     where
 
         mkPlugin :: ([(PluginId, b)] -> Plugin Config) -> (PluginDescriptor IdeState -> b) -> Plugin Config
@@ -66,17 +63,14 @@ asGhcIdePlugin (IdePlugins ls) =
 -- ---------------------------------------------------------------------
 
 rulesPlugins :: [(PluginId, Rules ())] -> Plugin Config
-rulesPlugins rs = mempty { P.pluginRules = rules }
+rulesPlugins rs = Plugin rules mempty
     where
         rules = foldMap snd rs
 
-dynFlagsPlugins :: [(PluginId, DynFlagsModifications)] -> Plugin Config
-dynFlagsPlugins rs = mempty { P.pluginModifyDynflags = foldMap snd rs }
-
 -- ---------------------------------------------------------------------
 
 executeCommandPlugins :: [(PluginId, [PluginCommand IdeState])] -> Plugin Config
-executeCommandPlugins ecs = mempty { P.pluginHandlers = executeCommandHandlers ecs }
+executeCommandPlugins ecs = Plugin mempty (executeCommandHandlers ecs)
 
 executeCommandHandlers :: [(PluginId, [PluginCommand IdeState])] -> LSP.Handlers (ServerM Config)
 executeCommandHandlers ecs = requestHandler SWorkspaceExecuteCommand execCmd
@@ -138,7 +132,7 @@ executeCommandHandlers ecs = requestHandler SWorkspaceExecuteCommand execCmd
 -- ---------------------------------------------------------------------
 
 extensiblePlugins :: [(PluginId, PluginHandlers IdeState)] -> Plugin Config
-extensiblePlugins xs = mempty { P.pluginHandlers = handlers }
+extensiblePlugins xs = Plugin mempty handlers
   where
     IdeHandlers handlers' = foldMap bakePluginId xs
     bakePluginId :: (PluginId, PluginHandlers IdeState) -> IdeHandlers
@@ -166,7 +160,7 @@ extensiblePlugins xs = mempty { P.pluginHandlers = handlers }
 -- ---------------------------------------------------------------------
 
 extensibleNotificationPlugins :: [(PluginId, PluginNotificationHandlers IdeState)] -> Plugin Config
-extensibleNotificationPlugins xs = mempty { P.pluginHandlers = handlers }
+extensibleNotificationPlugins xs = Plugin mempty handlers
   where
     IdeNotificationHandlers handlers' = foldMap bakePluginId xs
     bakePluginId :: (PluginId, PluginNotificationHandlers IdeState) -> IdeNotificationHandlers
diff --git a/ghcide/src/Development/IDE/Plugin/Test.hs b/ghcide/src/Development/IDE/Plugin/Test.hs
index 47fa49f14f..e8643d9471 100644
--- a/ghcide/src/Development/IDE/Plugin/Test.hs
+++ b/ghcide/src/Development/IDE/Plugin/Test.hs
@@ -37,8 +37,6 @@ import           Ide.Types
 import qualified Language.LSP.Server            as LSP
 import           Language.LSP.Types
 import           System.Time.Extra
-import qualified Development.IDE.Plugin as P
-import Data.Default (def)
 
 data TestRequest
     = BlockSeconds Seconds           -- ^ :: Null
@@ -53,9 +51,9 @@ newtype WaitForIdeRuleResult = WaitForIdeRuleResult { ideResultSuccess::Bool}
     deriving newtype (FromJSON, ToJSON)
 
 plugin :: Plugin c
-plugin = def {
-    P.pluginRules = return (),
-    P.pluginHandlers = requestHandler (SCustomMethod "test") testRequestHandler'
+plugin = Plugin {
+    pluginRules = return (),
+    pluginHandlers = requestHandler (SCustomMethod "test") testRequestHandler'
 }
   where
       testRequestHandler' ide req
diff --git a/hls-plugin-api/hls-plugin-api.cabal b/hls-plugin-api/hls-plugin-api.cabal
index c486e7a96b..acec2485d4 100644
--- a/hls-plugin-api/hls-plugin-api.cabal
+++ b/hls-plugin-api/hls-plugin-api.cabal
@@ -43,7 +43,6 @@ library
     , dependent-sum
     , Diff                  ^>=0.4.0
     , dlist
-    , ghc
     , hashable
     , hslogger
     , lens
diff --git a/hls-plugin-api/src/Ide/Types.hs b/hls-plugin-api/src/Ide/Types.hs
index 52ede7dc6e..c17171b2f0 100644
--- a/hls-plugin-api/src/Ide/Types.hs
+++ b/hls-plugin-api/src/Ide/Types.hs
@@ -50,26 +50,12 @@ import           Language.LSP.VFS
 import           OpenTelemetry.Eventlog
 import           System.IO.Unsafe
 import           Text.Regex.TDFA.Text            ()
-import DynFlags (DynFlags)
 
 -- ---------------------------------------------------------------------
 
 newtype IdePlugins ideState = IdePlugins
   { ipMap :: [(PluginId, PluginDescriptor ideState)]}
 
-data DynFlagsModifications =
-  DynFlagsModifications { dynFlagsModifyGlobal :: DynFlags -> DynFlags
-                        , dynFlagsModifyParser :: DynFlags -> DynFlags
-                        }
-
-instance Semigroup DynFlagsModifications where
-  DynFlagsModifications g1 p1 <> DynFlagsModifications g2 p2 =
-    DynFlagsModifications (g2 . g1) (p2 . p1)
-
-instance Monoid DynFlagsModifications where
-  mempty = DynFlagsModifications id id
-
-
 -- ---------------------------------------------------------------------
 
 data PluginDescriptor ideState =
@@ -79,7 +65,6 @@ data PluginDescriptor ideState =
                    , pluginHandlers     :: PluginHandlers ideState
                    , pluginConfigDescriptor :: ConfigDescriptor
                    , pluginNotificationHandlers :: PluginNotificationHandlers ideState
-                   , pluginModifyDynflags :: DynFlagsModifications
                    }
 
 -- | An existential wrapper of 'Properties'
@@ -312,7 +297,6 @@ defaultPluginDescriptor plId =
     mempty
     defaultConfigDescriptor
     mempty
-    mempty
 
 newtype CommandId = CommandId T.Text
   deriving (Show, Read, Eq, Ord)

From 0399ce4a968d906034124460bfbccbb58f3b68d2 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Thu, 13 May 2021 14:14:47 -0700
Subject: [PATCH 50/52] Add tests

---
 .../hls-tactics-plugin.cabal                  |  1 +
 .../hls-tactics-plugin/src/Wingman/Plugin.hs  | 10 -------
 .../test/CodeAction/RunMetaprogramSpec.hs     | 28 +++++++++++++++++++
 .../test/golden/MetaBegin.hs                  |  1 +
 .../test/golden/MetaBegin.hs.expected         |  1 +
 .../test/golden/MetaBindAll.hs                |  2 ++
 .../test/golden/MetaBindAll.hs.expected       |  2 ++
 .../test/golden/MetaBindOne.hs                |  2 ++
 .../test/golden/MetaBindOne.hs.expected       |  2 ++
 .../test/golden/MetaChoice.hs                 |  2 ++
 .../test/golden/MetaChoice.hs.expected        |  2 ++
 .../test/golden/MetaMaybeAp.hs                | 11 ++++++++
 .../test/golden/MetaMaybeAp.hs.expected       |  5 ++++
 .../hls-tactics-plugin/test/golden/MetaTry.hs |  2 ++
 .../test/golden/MetaTry.hs.expected           |  2 ++
 15 files changed, 63 insertions(+), 10 deletions(-)
 create mode 100644 plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs
 create mode 100644 plugins/hls-tactics-plugin/test/golden/MetaBegin.hs
 create mode 100644 plugins/hls-tactics-plugin/test/golden/MetaBegin.hs.expected
 create mode 100644 plugins/hls-tactics-plugin/test/golden/MetaBindAll.hs
 create mode 100644 plugins/hls-tactics-plugin/test/golden/MetaBindAll.hs.expected
 create mode 100644 plugins/hls-tactics-plugin/test/golden/MetaBindOne.hs
 create mode 100644 plugins/hls-tactics-plugin/test/golden/MetaBindOne.hs.expected
 create mode 100644 plugins/hls-tactics-plugin/test/golden/MetaChoice.hs
 create mode 100644 plugins/hls-tactics-plugin/test/golden/MetaChoice.hs.expected
 create mode 100644 plugins/hls-tactics-plugin/test/golden/MetaMaybeAp.hs
 create mode 100644 plugins/hls-tactics-plugin/test/golden/MetaMaybeAp.hs.expected
 create mode 100644 plugins/hls-tactics-plugin/test/golden/MetaTry.hs
 create mode 100644 plugins/hls-tactics-plugin/test/golden/MetaTry.hs.expected

diff --git a/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal b/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal
index 7ae1afe014..56573c5223 100644
--- a/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal
+++ b/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal
@@ -131,6 +131,7 @@ test-suite tests
     CodeAction.DestructSpec
     CodeAction.IntrosSpec
     CodeAction.RefineSpec
+    CodeAction.RunMetaprogramSpec
     CodeAction.UseDataConSpec
     CodeLens.EmptyCaseSpec
     ProviderSpec
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs b/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs
index 32967b5e66..9f0c0ecce3 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs
@@ -21,7 +21,6 @@ import           Development.IDE.Core.Shake (IdeState (..))
 import           Development.IDE.Core.UseStale (Tracked, TrackedStale(..), unTrack, mapAgeFrom, unsafeMkCurrent)
 import           Development.IDE.GHC.Compat
 import           Development.IDE.GHC.ExactPrint
-import           GHC.LanguageExtensions.Type (Extension(EmptyCase))
 import           Generics.SYB.GHC
 import           Ide.Types
 import           Language.LSP.Server
@@ -71,15 +70,6 @@ descriptor plId = (defaultPluginDescriptor plId)
   }
 
 
--- | Wingman wants to support destructing of empty cases, but these are a parse
--- error by default. So we want to enable 'EmptyCase', but then that leads to
--- silent errors without 'Opt_WarnIncompletePatterns'.
-allowEmptyCaseButWithWarning :: DynFlags -> DynFlags
-allowEmptyCaseButWithWarning =
-  flip xopt_set EmptyCase . flip wopt_set Opt_WarnIncompletePatterns
-
-
-
 codeActionProvider :: PluginMethodHandler IdeState TextDocumentCodeAction
 codeActionProvider state plId (CodeActionParams _ _ (TextDocumentIdentifier uri) (unsafeMkCurrent -> range) _ctx)
   | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do
diff --git a/plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs b/plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs
new file mode 100644
index 0000000000..f7e75008fd
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs
@@ -0,0 +1,28 @@
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE DuplicateRecordFields #-}
+{-# LANGUAGE OverloadedStrings     #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE ViewPatterns          #-}
+
+module CodeAction.RunMetaprogramSpec where
+
+import Wingman.Types
+import Test.Hspec
+import Utils
+
+
+spec :: Spec
+spec = do
+  let metaTest = goldenTest RunMetaprogram ""
+
+  describe "beginMetaprogram" $ do
+    goldenTest BeginMetaprogram ""  1  7 "MetaBegin.hs"
+
+  describe "golden" $ do
+    metaTest  6 11 "MetaMaybeAp.hs"
+    metaTest  2 32 "MetaBindOne.hs"
+    metaTest  2 32 "MetaBindAll.hs"
+    metaTest  2 13 "MetaTry.hs"
+    metaTest  2 74 "MetaChoice.hs"
+
diff --git a/plugins/hls-tactics-plugin/test/golden/MetaBegin.hs b/plugins/hls-tactics-plugin/test/golden/MetaBegin.hs
new file mode 100644
index 0000000000..fdfbd7289d
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/MetaBegin.hs
@@ -0,0 +1 @@
+foo = _
diff --git a/plugins/hls-tactics-plugin/test/golden/MetaBegin.hs.expected b/plugins/hls-tactics-plugin/test/golden/MetaBegin.hs.expected
new file mode 100644
index 0000000000..3c56bdbee9
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/MetaBegin.hs.expected
@@ -0,0 +1 @@
+foo = [wingman||]
diff --git a/plugins/hls-tactics-plugin/test/golden/MetaBindAll.hs b/plugins/hls-tactics-plugin/test/golden/MetaBindAll.hs
new file mode 100644
index 0000000000..d25670bca1
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/MetaBindAll.hs
@@ -0,0 +1,2 @@
+foo :: a -> (a, a)
+foo a = [wingman| split; assumption |]
diff --git a/plugins/hls-tactics-plugin/test/golden/MetaBindAll.hs.expected b/plugins/hls-tactics-plugin/test/golden/MetaBindAll.hs.expected
new file mode 100644
index 0000000000..00421ee479
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/MetaBindAll.hs.expected
@@ -0,0 +1,2 @@
+foo :: a -> (a, a)
+foo a = (a, a)
diff --git a/plugins/hls-tactics-plugin/test/golden/MetaBindOne.hs b/plugins/hls-tactics-plugin/test/golden/MetaBindOne.hs
new file mode 100644
index 0000000000..fe6c118829
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/MetaBindOne.hs
@@ -0,0 +1,2 @@
+foo :: a -> (a, a)
+foo a = [wingman| split, assumption |]
diff --git a/plugins/hls-tactics-plugin/test/golden/MetaBindOne.hs.expected b/plugins/hls-tactics-plugin/test/golden/MetaBindOne.hs.expected
new file mode 100644
index 0000000000..5c28b9649e
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/MetaBindOne.hs.expected
@@ -0,0 +1,2 @@
+foo :: a -> (a, a)
+foo a = (a, _)
diff --git a/plugins/hls-tactics-plugin/test/golden/MetaChoice.hs b/plugins/hls-tactics-plugin/test/golden/MetaChoice.hs
new file mode 100644
index 0000000000..97e5b424ba
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/MetaChoice.hs
@@ -0,0 +1,2 @@
+reassoc :: (a, (b, c)) -> ((a, b), c)
+reassoc (a, (b, c)) = [wingman| split; split | assume c; assume a | assume b |]
diff --git a/plugins/hls-tactics-plugin/test/golden/MetaChoice.hs.expected b/plugins/hls-tactics-plugin/test/golden/MetaChoice.hs.expected
new file mode 100644
index 0000000000..c9d2f0cff9
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/MetaChoice.hs.expected
@@ -0,0 +1,2 @@
+reassoc :: (a, (b, c)) -> ((a, b), c)
+reassoc (a, (b, c)) = ((a, b), c)
diff --git a/plugins/hls-tactics-plugin/test/golden/MetaMaybeAp.hs b/plugins/hls-tactics-plugin/test/golden/MetaMaybeAp.hs
new file mode 100644
index 0000000000..6159db4ecd
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/MetaMaybeAp.hs
@@ -0,0 +1,11 @@
+maybeAp :: Maybe (a -> b) -> Maybe a -> Maybe b
+maybeAp = [wingman|
+  intros,
+  destruct_all,
+  obvious,
+  obvious,
+  obvious,
+  ctor Just,
+  application,
+  assumption
+  |]
diff --git a/plugins/hls-tactics-plugin/test/golden/MetaMaybeAp.hs.expected b/plugins/hls-tactics-plugin/test/golden/MetaMaybeAp.hs.expected
new file mode 100644
index 0000000000..8e40c9fa3f
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/MetaMaybeAp.hs.expected
@@ -0,0 +1,5 @@
+maybeAp :: Maybe (a -> b) -> Maybe a -> Maybe b
+maybeAp Nothing Nothing = Nothing
+maybeAp (Just _) Nothing = Nothing
+maybeAp Nothing (Just _) = Nothing
+maybeAp (Just fab) (Just a) = Just (fab a)
diff --git a/plugins/hls-tactics-plugin/test/golden/MetaTry.hs b/plugins/hls-tactics-plugin/test/golden/MetaTry.hs
new file mode 100644
index 0000000000..d92c4a5763
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/MetaTry.hs
@@ -0,0 +1,2 @@
+foo :: a -> (b, a)
+foo a = [wingman| split; try assumption |]
diff --git a/plugins/hls-tactics-plugin/test/golden/MetaTry.hs.expected b/plugins/hls-tactics-plugin/test/golden/MetaTry.hs.expected
new file mode 100644
index 0000000000..807b9bdcb5
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/MetaTry.hs.expected
@@ -0,0 +1,2 @@
+foo :: a -> (b, a)
+foo a = (_, a)

From 6424855be6858b787635618003dd155c358cf96d Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Thu, 13 May 2021 14:31:05 -0700
Subject: [PATCH 51/52] Feature gate

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

diff --git a/plugins/hls-tactics-plugin/src/Wingman/FeatureSet.hs b/plugins/hls-tactics-plugin/src/Wingman/FeatureSet.hs
index 190a654a31..1bde1a06ca 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/FeatureSet.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/FeatureSet.hs
@@ -27,6 +27,7 @@ data Feature
   | FeatureKnownMonoid
   | FeatureEmptyCase
   | FeatureDestructPun
+  | FeatureMetaprogram
   deriving (Eq, Ord, Show, Read, Enum, Bounded)
 
 
diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs
index 2a77a28b1e..9080b360ca 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs
@@ -156,12 +156,12 @@ commandProvider Refine =
   requireFeature FeatureRefineHole $
     provide Refine ""
 commandProvider BeginMetaprogram =
+  requireFeature FeatureMetaprogram $
   requireHoleSort (== Hole) $
-  -- requireFeature FeatureMetaprogram $
     provide BeginMetaprogram ""
 commandProvider RunMetaprogram =
+  requireFeature FeatureMetaprogram $
   withMetaprogram $ \mp ->
-  -- requireFeature FeatureMetaprogram $
     provide RunMetaprogram mp
 
 

From 6da17ee15c63426a4b0a5ebc8c0995b906624136 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Fri, 14 May 2021 09:35:45 -0700
Subject: [PATCH 52/52] Restrict metaprograms to >=8.8

---
 .../Wingman/LanguageServer/TacticProviders.hs    | 12 ++++++++++++
 .../src/Wingman/StaticPlugin.hs                  |  4 ++--
 .../test/CodeAction/RunMetaprogramSpec.hs        | 16 ++++++++++++----
 3 files changed, 26 insertions(+), 6 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs
index 9080b360ca..8c23873726 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE CPP               #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE RecordWildCards   #-}
 
@@ -156,15 +157,26 @@ commandProvider Refine =
   requireFeature FeatureRefineHole $
     provide Refine ""
 commandProvider BeginMetaprogram =
+  requireGHC88OrHigher $
   requireFeature FeatureMetaprogram $
   requireHoleSort (== Hole) $
     provide BeginMetaprogram ""
 commandProvider RunMetaprogram =
+  requireGHC88OrHigher $
   requireFeature FeatureMetaprogram $
   withMetaprogram $ \mp ->
     provide RunMetaprogram mp
 
 
+requireGHC88OrHigher :: TacticProvider -> TacticProvider
+requireGHC88OrHigher tp tpd =
+#if __GLASGOW_HASKELL__ >= 808
+  tp tpd
+#else
+  mempty
+#endif
+
+
 ------------------------------------------------------------------------------
 -- | Return an empty list if the given predicate doesn't hold over the length
 guardLength :: (Int -> Bool) -> [a] -> [a]
diff --git a/plugins/hls-tactics-plugin/src/Wingman/StaticPlugin.hs b/plugins/hls-tactics-plugin/src/Wingman/StaticPlugin.hs
index af054ccd6c..868a040570 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/StaticPlugin.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/StaticPlugin.hs
@@ -16,14 +16,14 @@ import Ide.Types
 
 
 staticPlugin :: DynFlagsModifications
-staticPlugin = DynFlagsModifications
+staticPlugin = mempty
   { dynFlagsModifyGlobal =
       \df -> allowEmptyCaseButWithWarning
            $ df
 #if __GLASGOW_HASKELL__ >= 808
              { staticPlugins = staticPlugins df <> [metaprogrammingPlugin] }
-#endif
   , dynFlagsModifyParser = enableQuasiQuotes
+#endif
   }
 
 
diff --git a/plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs b/plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs
index f7e75008fd..bc42de54a1 100644
--- a/plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs
+++ b/plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE CPP                   #-}
 {-# LANGUAGE DataKinds             #-}
 {-# LANGUAGE DuplicateRecordFields #-}
 {-# LANGUAGE OverloadedStrings     #-}
@@ -7,17 +8,24 @@
 
 module CodeAction.RunMetaprogramSpec where
 
-import Wingman.Types
-import Test.Hspec
-import Utils
+import  Utils
+import  Test.Hspec
+import  Wingman.Types
 
 
 spec :: Spec
 spec = do
-  let metaTest = goldenTest RunMetaprogram ""
+  let metaTest l c f =
+#if __GLASGOW_HASKELL__ >= 808
+        goldenTest RunMetaprogram "" l c f
+#else
+        pure ()
+#endif
 
+#if __GLASGOW_HASKELL__ >= 808
   describe "beginMetaprogram" $ do
     goldenTest BeginMetaprogram ""  1  7 "MetaBegin.hs"
+#endif
 
   describe "golden" $ do
     metaTest  6 11 "MetaMaybeAp.hs"