diff --git a/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal b/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal
index c52cd6830b..56573c5223 100644
--- a/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal
+++ b/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal
@@ -44,9 +44,14 @@ library
     Wingman.KnownStrategies.QuickCheck
     Wingman.LanguageServer
     Wingman.LanguageServer.TacticProviders
+    Wingman.LanguageServer.Metaprogram
     Wingman.Machinery
+    Wingman.Metaprogramming.Lexer
+    Wingman.Metaprogramming.Parser
+    Wingman.Metaprogramming.ProofState
     Wingman.Naming
     Wingman.Plugin
+    Wingman.StaticPlugin
     Wingman.Range
     Wingman.Simplify
     Wingman.Tactics
@@ -86,6 +91,9 @@ library
     , transformers
     , unordered-containers
     , hyphenation
+    , megaparsec ^>=9
+    , parser-combinators
+    , prettyprinter
 
   default-language:   Haskell2010
   default-extensions:
@@ -123,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/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/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/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 784f5f475f..9c3372a880 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
@@ -10,18 +10,18 @@ module Wingman.LanguageServer where
 import           ConLike
 import           Control.Arrow ((***))
 import           Control.Monad
-import           Control.Monad.State (State, get, put, evalState)
+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.Generics.Aliases (mkQ)
-import           Data.Generics.Schemes (everything)
+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
@@ -34,33 +34,38 @@ 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.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           GhcPlugins (tupleDataCon, consDataCon, substTyAddInScope, ExternalPackageState, HscEnv (hsc_EPS), liftIO)
+import           Generics.SYB hiding (Generic)
+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)
 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)
 import           Wingman.Types
 
 
@@ -178,6 +183,11 @@ 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
@@ -187,7 +197,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
 
@@ -197,12 +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, 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.
@@ -211,10 +225,20 @@ 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 (fmap realSrcSpanToRange new_rss, jdg, ctx, dflags)
+      pure $ HoleJudgment
+        { hj_range = fmap realSrcSpanToRange new_rss
+        , hj_jdg = jdg
+        , hj_ctx = ctx
+        , hj_dflags = dflags
+        , hj_hole_sort = holeSortFor mp
+        }
+
 
+holeSortFor :: Maybe T.Text -> HoleSort
+holeSortFor = maybe Hole Metaprogram
 
 
 mkJudgementAndContext
@@ -285,8 +309,12 @@ 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
+        occ <- (either (const Nothing) (Just . occName) =<<)
+             . listToMaybe
+             . S.toList
+             . M.keysSet
+             $ nodeIdentifiers info
+        guard $ isHole occ
         pure (unsafeCopyAge r $ nodeSpan ast', ty)
 
 
@@ -543,5 +571,28 @@ 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 $ MetaprogramSyntax mp
+    let anns = addAnnotationsForPretty [] x mempty
+    modifyAnnsT $ mappend anns
+    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
new file mode 100644
index 0000000000..37e8581928
--- /dev/null
+++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/Metaprogram.hs
@@ -0,0 +1,90 @@
+{-# LANGUAGE DuplicateRecordFields #-}
+{-# LANGUAGE OverloadedStrings     #-}
+
+{-# LANGUAGE NoMonoLocalBinds  #-}
+{-# LANGUAGE RankNTypes #-}
+
+module Wingman.LanguageServer.Metaprogram
+  ( hoverProvider
+  ) where
+
+import           Control.Applicative (empty)
+import           Control.Monad
+import           Control.Monad.Trans
+import           Control.Monad.Trans.Maybe
+import           Data.List (find)
+import           Data.Maybe
+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 (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.Judgements.SYB (metaprogramQ)
+import           Wingman.Metaprogramming.Parser (attempt_it)
+import           Wingman.LanguageServer
+import           Wingman.Types
+
+
+------------------------------------------------------------------------------
+-- | Provide the "empty case completion" code lens
+hoverProvider :: PluginMethodHandler IdeState TextDocumentHover
+hoverProvider state plId (HoverParams (TextDocumentIdentifier uri) (unsafeMkCurrent -> pos) _)
+  | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do
+      let loc = fmap (realSrcLocSpan . positionToRealSrcLoc nfp) pos
+
+      cfg <- getTacticConfig plId
+      liftIO $ fromMaybeT (Right Nothing) $ do
+        -- guard $ hasFeature FeatureEmptyCase $ cfg_feature_set cfg
+
+        holes <- getMetaprogramsAtSpan state nfp $ RealSrcSpan $ unTrack loc
+
+        fmap (Right . Just) $
+          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
+              pure $ Hover
+                { _contents = HoverContents
+                            $ MarkupContent MkMarkdown
+                            $ 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
+
+
+getMetaprogramsAtSpan
+    :: IdeState
+    -> NormalizedFilePath
+    -> SrcSpan
+    -> MaybeT IO [(Tracked 'Current RealSrcSpan, T.Text)]
+getMetaprogramsAtSpan state nfp ss = do
+    let stale a = runStaleIde "getMetaprogramsAtSpan" state nfp a
+
+    TrackedStale tcg tcg_map <- fmap (fmap tmrTypechecked) $ stale TypeCheck
+
+    let scrutinees = traverse (metaprogramQ ss . 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
+
+
diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs
index 1c205d8bab..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   #-}
 
@@ -7,14 +8,13 @@ module Wingman.LanguageServer.TacticProviders
   , tcCommandId
   , TacticParams (..)
   , TacticProviderData (..)
+  , useNameFromHypothesis
   ) 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
@@ -29,28 +29,31 @@ 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
 import           Wingman.Judgements
+import           Wingman.Machinery (useNameFromHypothesis)
+import           Wingman.Metaprogramming.Parser (parseMetaprogram)
 import           Wingman.Tactics
 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
 
 
 ------------------------------------------------------------------------------
@@ -66,6 +69,8 @@ tacticKind HomomorphismLambdaCase = "homomorphicLambdaCase"
 tacticKind DestructAll            = "splitFuncArgs"
 tacticKind UseDataCon             = "useConstructor"
 tacticKind Refine                 = "refine"
+tacticKind BeginMetaprogram       = "beginMetaprogram"
+tacticKind RunMetaprogram         = "runMetaprogram"
 
 
 ------------------------------------------------------------------------------
@@ -82,6 +87,8 @@ tacticPreferred HomomorphismLambdaCase = False
 tacticPreferred DestructAll            = True
 tacticPreferred UseDataCon             = True
 tacticPreferred Refine                 = True
+tacticPreferred BeginMetaprogram       = False
+tacticPreferred RunMetaprogram         = True
 
 
 mkTacticKind :: TacticCommand -> CodeActionKind
@@ -93,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
@@ -136,8 +153,28 @@ commandProvider UseDataCon =
           . occName
           $ dataConName dcon
 commandProvider Refine =
+  requireHoleSort (== Hole) $
   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
 
 
 ------------------------------------------------------------------------------
@@ -153,6 +190,7 @@ type TacticProvider
      = TacticProviderData
     -> IO [Command |? CodeAction]
 
+
 data TacticProviderData = TacticProviderData
   { tpd_dflags :: DynFlags
   , tpd_config :: Config
@@ -160,6 +198,7 @@ data TacticProviderData = TacticProviderData
   , tpd_uri    :: Uri
   , tpd_range  :: Tracked 'Current Range
   , tpd_jdg    :: Judgement
+  , tpd_hole_sort :: HoleSort
   }
 
 
@@ -182,6 +221,19 @@ requireFeature f tp tpd =
     False -> pure []
 
 
+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
 -- predicate holds for the goal.
@@ -245,18 +297,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 34dcb449c6..d0f5368e47 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
@@ -298,3 +299,19 @@ 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
+
+------------------------------------------------------------------------------
+-- | 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/Lexer.hs b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Lexer.hs
new file mode 100644
index 0000000000..fb396029a4
--- /dev/null
+++ b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Lexer.hs
@@ -0,0 +1,70 @@
+{-# LANGUAGE DataKinds         #-}
+{-# LANGUAGE LambdaCase        #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE TypeApplications  #-}
+
+module Wingman.Metaprogramming.Lexer where
+
+import           Control.Applicative
+import           Control.Monad
+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
+
+
+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
+
+ichar :: Parser Char
+ichar = P.alphaNumChar <|> P.char '_' <|> P.char '\''
+
+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 "}")
+
+parens :: Parser a -> Parser a
+parens = P.between (symbol "(") (symbol ")")
+
+identifier :: Text -> Parser ()
+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 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 (ichar <|> P.char '-')
+    pure $ T.pack (c:cs)
+
+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..c9f26aa10a
--- /dev/null
+++ b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
@@ -0,0 +1,101 @@
+{-# 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.Functor
+import qualified Data.Text as T
+import qualified Refinery.Tactic as R
+import qualified Text.Megaparsec as P
+import           Wingman.Auto
+import           Wingman.Machinery (useNameFromHypothesis)
+import           Wingman.Metaprogramming.Lexer
+import           Wingman.Metaprogramming.ProofState (proofState, layout)
+import           Wingman.Tactics
+import           Wingman.Types
+
+
+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)
+
+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
+        []    -> 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
+    , nullary   "application" application
+    , unary_occ "apply" $ useNameFromHypothesis apply
+    , nullary   "split" split
+    , unary_occ "ctor" userSplit
+    , nullary   "obvious" obvious
+    , nullary   "auto" auto
+    , nullary   "sorry" sorry
+    ]
+
+
+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)
+      ]
+    ]
+
+
+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 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 $ 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/Metaprogramming/ProofState.hs b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/ProofState.hs
new file mode 100644
index 0000000000..4bfa95cec8
--- /dev/null
+++ b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/ProofState.hs
@@ -0,0 +1,113 @@
+{-# LANGUAGE NamedFieldPuns    #-}
+{-# LANGUAGE OverloadedStrings #-}
+
+module Wingman.Metaprogramming.ProofState where
+
+import           Data.Bool (bool)
+import           Data.Functor ((<&>))
+import qualified Data.Text as T
+import           Data.Text.Prettyprint.Doc
+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 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 #-}
+
+
+data Ann
+  = Goal
+  | Hypoth
+  | Status
+  deriving (Eq, Ord, Show, Enum, Bounded)
+
+forceMarkdownNewlines :: String -> String
+forceMarkdownNewlines = unlines . fmap (<> "  ") . lines
+
+layout :: Doc Ann -> String
+layout
+  = forceMarkdownNewlines
+  . T.unpack
+  . renderSimplyDecorated id
+    renderAnn
+    renderUnann
+  . layoutPretty (LayoutOptions $ AvailablePerLine 80 0.6)
+
+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
+    $ ( annotate Status
+      . countFinished "goals accomplished 🎉" "goal"
+      $ length rtr_subgoals
+      )
+    : pretty sectionSeparator
+    : fmap prettySubgoal rtr_subgoals
+
+
+prettySubgoal :: Judgement -> Doc Ann
+prettySubgoal 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 hy =
+  vsep $ 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)
+
+textSpaces :: Int -> T.Text
+textSpaces n = T.replicate n $ T.singleton ' '
+
+
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs b/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs
index 935d8d6736..9f0c0ecce3 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
@@ -20,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
@@ -33,9 +33,11 @@ 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
 
@@ -59,40 +61,31 @@ descriptor plId = (defaultPluginDescriptor plId)
   , pluginHandlers = mconcat
       [ mkPluginHandler STextDocumentCodeAction codeActionProvider
       , mkPluginHandler STextDocumentCodeLens codeLensProvider
+      , mkPluginHandler STextDocumentHover hoverProvider
       ]
   , pluginRules = wingmanRules plId
   , pluginConfigDescriptor =
       defaultConfigDescriptor {configCustomConfig = mkCustomConfig properties}
-  , pluginModifyDynflags = mempty
-      { dynFlagsModifyGlobal = 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
       cfg <- getTacticConfig plId
       liftIO $ fromMaybeT (Right $ List []) $ do
-        (_, jdg, _, 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 []
@@ -107,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
@@ -115,19 +111,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 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
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..868a040570
--- /dev/null
+++ b/plugins/hls-tactics-plugin/src/Wingman/StaticPlugin.hs
@@ -0,0 +1,96 @@
+{-# LANGUAGE CPP #-}
+
+module Wingman.StaticPlugin
+  ( staticPlugin
+  , metaprogramHoleName
+  , pattern WingmanMetaprogram
+  , pattern MetaprogramSyntax
+  ) where
+
+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 = mempty
+  { dynFlagsModifyGlobal =
+      \df -> allowEmptyCaseButWithWarning
+           $ df
+#if __GLASGOW_HASKELL__ >= 808
+             { staticPlugins = staticPlugins df <> [metaprogrammingPlugin] }
+  , dynFlagsModifyParser = enableQuasiQuotes
+#endif
+  }
+
+
+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
+
+
+#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
+
+metaprogramHoleName :: OccName
+metaprogramHoleName = mkVarOcc "_$metaprogram"
+
+
+mkMetaprogram :: SrcSpan -> FastString -> HsExpr GhcPs
+mkMetaprogram ss mp =
+  HsSCC noExtField MetaprogramSourceText (StringLiteral NoSourceText mp)
+    $ L ss
+    $ HsVar noExtField
+    $ L ss
+    $ mkRdrUnqual
+    $ metaprogramHoleName
+
+
+addMetaprogrammingSyntax :: Data a => a -> a
+addMetaprogrammingSyntax =
+  everywhere $ mkT $ \case
+    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 noExtField $
+        HsQuasiQuote
+          noExtField
+          (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 429931f631..6f3d36354b 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
@@ -10,6 +12,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 ()
@@ -34,6 +37,8 @@ import           Wingman.Judgements
 import           Wingman.Machinery
 import           Wingman.Naming
 import           Wingman.Types
+import OccName (mkVarOcc)
+import Wingman.StaticPlugin (pattern MetaprogramSyntax)
 
 
 ------------------------------------------------------------------------------
@@ -93,17 +98,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
@@ -213,6 +227,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.
@@ -255,6 +272,24 @@ 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
+
+
+------------------------------------------------------------------------------
+-- | Sorry leaves a hole in its extract
+sorry :: TacticsM ()
+sorry = exact $ var' $ mkVarOcc "_"
+
+
+------------------------------------------------------------------------------
+-- | Sorry leaves a hole in its extract
+metaprogram :: TacticsM ()
+metaprogram = exact $ MetaprogramSyntax ""
+
 
 ------------------------------------------------------------------------------
 -- | Allow the given tactic to proceed if and only if it introduces holes that
@@ -402,4 +437,3 @@ applyByName name = do
       True  -> apply hi
       False -> empty
 
-
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Types.hs b/plugins/hls-tactics-plugin/src/Wingman/Types.hs
index 1494336562..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)
 
 
 ------------------------------------------------------------------------------
@@ -56,6 +58,8 @@ data TacticCommand
   | DestructAll
   | UseDataCon
   | Refine
+  | BeginMetaprogram
+  | RunMetaprogram
   deriving (Eq, Ord, Show, Enum, Bounded)
 
 -- | Generate a title for the command.
@@ -72,6 +76,8 @@ 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"
+    go RunMetaprogram _         = "Run custom tactic"
 
 
 ------------------------------------------------------------------------------
@@ -476,6 +482,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
@@ -502,3 +509,15 @@ instance Show UserFacingMessage where
   show NothingToDo             = "Nothing to do"
   show (InfrastructureError t) = "Internal error: " <> T.unpack t
 
+
+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
+  }
+
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..bc42de54a1
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs
@@ -0,0 +1,36 @@
+{-# LANGUAGE CPP                   #-}
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE DuplicateRecordFields #-}
+{-# LANGUAGE OverloadedStrings     #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE ViewPatterns          #-}
+
+module CodeAction.RunMetaprogramSpec where
+
+import  Utils
+import  Test.Hspec
+import  Wingman.Types
+
+
+spec :: Spec
+spec = do
+  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"
+    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)