diff --git a/plugins/hls-tactics-plugin/src/Wingman/Context.hs b/plugins/hls-tactics-plugin/src/Wingman/Context.hs
index 4ca76efb34..dc28198585 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Context.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Context.hs
@@ -4,7 +4,7 @@ import           Bag
 import           Control.Arrow
 import           Control.Monad.Reader
 import           Data.Foldable.Extra (allM)
-import           Data.Maybe (fromMaybe, isJust)
+import           Data.Maybe (fromMaybe, isJust, mapMaybe)
 import qualified Data.Set as S
 import           Development.IDE.GHC.Compat
 import           GhcPlugins (ExternalPackageState (eps_inst_env), piResultTys)
@@ -27,11 +27,13 @@ mkContext
     -> Context
 mkContext cfg locals tcg eps kt ev = Context
   { ctxDefiningFuncs = locals
-  , ctxModuleFuncs = fmap splitId
-                   . (getFunBindId =<<)
-                   . fmap unLoc
-                   . bagToList
-                   $ tcg_binds tcg
+  , ctxModuleFuncs
+      = fmap splitId
+      . mappend (locallyDefinedMethods tcg)
+      . (getFunBindId =<<)
+      . fmap unLoc
+      . bagToList
+      $ tcg_binds tcg
   , ctxConfig = cfg
   , ctxInstEnvs =
       InstEnvs
@@ -43,6 +45,14 @@ mkContext cfg locals tcg eps kt ev = Context
   }
 
 
+locallyDefinedMethods :: TcGblEnv -> [Id]
+locallyDefinedMethods
+  = foldMap classMethods
+  . mapMaybe tyConClass_maybe
+  . tcg_tcs
+
+
+
 splitId :: Id -> (OccName, CType)
 splitId = occName &&& CType . idType
 
diff --git a/plugins/hls-tactics-plugin/src/Wingman/GHC.hs b/plugins/hls-tactics-plugin/src/Wingman/GHC.hs
index 30ad63bd57..eefadeb003 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/GHC.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/GHC.hs
@@ -73,7 +73,7 @@ isFunction _                                    = True
 -- context.
 tacticsSplitFunTy :: Type -> ([TyVar], ThetaType, [Type], Type)
 tacticsSplitFunTy t
-  = let (vars, theta, t') = tcSplitSigmaTy t
+  = let (vars, theta, t') = tcSplitNestedSigmaTys t
         (args, res) = tcSplitFunTys t'
      in (vars, theta, args, res)
 
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Judgements.hs b/plugins/hls-tactics-plugin/src/Wingman/Judgements.hs
index 27cc02e953..95a7ed6be2 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Judgements.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Judgements.hs
@@ -229,6 +229,7 @@ provAncestryOf (PatternMatchPrv (PatVal mo so _ _)) =
 provAncestryOf (ClassMethodPrv _) = mempty
 provAncestryOf UserPrv = mempty
 provAncestryOf RecursivePrv = mempty
+provAncestryOf ImportPrv = mempty
 provAncestryOf (DisallowedPrv _ p2) = provAncestryOf p2
 
 
diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
index 9c3372a880..c7052a7070 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
@@ -1,6 +1,7 @@
 {-# LANGUAGE CPP               #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE RankNTypes        #-}
+{-# LANGUAGE TupleSections     #-}
 {-# LANGUAGE TypeFamilies      #-}
 
 {-# LANGUAGE NoMonoLocalBinds  #-}
@@ -43,6 +44,7 @@ import           Development.IDE.Spans.LocalBindings (Bindings, getDefiningBindi
 import qualified FastString
 import           GHC.Generics (Generic)
 import           Generics.SYB hiding (Generic)
+import           GhcPlugins (extractModule)
 import           GhcPlugins (tupleDataCon, consDataCon, substTyAddInScope, ExternalPackageState, HscEnv (hsc_EPS), unpackFS)
 import qualified Ide.Plugin.Config as Plugin
 import           Ide.Plugin.Properties
@@ -57,13 +59,14 @@ import           OccName
 import           Prelude hiding (span)
 import           Retrie (transformA)
 import           SrcLoc (containsSpan)
-import           TcRnTypes (tcg_binds, TcGblEnv)
+import           TcRnTypes (tcg_binds, TcGblEnv (tcg_rdr_env))
 import           Wingman.Context
 import           Wingman.FeatureSet
 import           Wingman.GHC
 import           Wingman.Judgements
 import           Wingman.Judgements.SYB (everythingContaining, metaprogramQ)
 import           Wingman.Judgements.Theta
+import           Wingman.Metaprogramming.Lexer (ParserContext(..))
 import           Wingman.Range
 import           Wingman.StaticPlugin (pattern WingmanMetaprogram, pattern MetaprogramSyntax)
 import           Wingman.Types
@@ -576,6 +579,10 @@ mkWorkspaceEdits dflags ccs uri pm g = do
    in first (InfrastructureError . T.pack) response
 
 
+------------------------------------------------------------------------------
+-- | Add ExactPrint annotations to every metaprogram in the source tree.
+-- Usually the ExactPrint module can do this for us, but we've enabled
+-- QuasiQuotes, so the round-trip print/parse journey will crash.
 annotateMetaprograms :: Data a => a -> Transform a
 annotateMetaprograms = everywhereM $ mkM $ \case
   L ss (WingmanMetaprogram mp) -> do
@@ -585,6 +592,9 @@ annotateMetaprograms = everywhereM $ mkM $ \case
     pure x
   (x :: LHsExpr GhcPs) -> pure x
 
+
+------------------------------------------------------------------------------
+-- | Find the source of a tactic metaprogram at the given span.
 getMetaprogramAtSpan
     :: Tracked age SrcSpan
     -> Tracked age TcGblEnv
@@ -596,3 +606,25 @@ getMetaprogramAtSpan (unTrack -> ss)
   . tcg_binds
   . unTrack
 
+
+------------------------------------------------------------------------------
+-- | The metaprogram parser needs the ability to lookup terms from the module
+-- and imports. The 'ParserContext' contains everything we need to find that
+-- stuff.
+getParserState
+    :: IdeState
+    -> NormalizedFilePath
+    -> Context
+    -> MaybeT IO ParserContext
+getParserState state nfp ctx = do
+  let stale a = runStaleIde "getParserState" state nfp a
+
+  TrackedStale (unTrack -> tcmod) _  <- stale TypeCheck
+  TrackedStale (unTrack -> hscenv) _ <- stale GhcSessionDeps
+
+  let tcgblenv = tmrTypechecked tcmod
+      modul = extractModule tcgblenv
+      rdrenv = tcg_rdr_env tcgblenv
+
+  pure $ ParserContext (hscEnv hscenv) rdrenv modul ctx
+
diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/Metaprogram.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/Metaprogram.hs
index 37e8581928..c54d82973f 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/Metaprogram.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/Metaprogram.hs
@@ -10,6 +10,7 @@ module Wingman.LanguageServer.Metaprogram
 
 import           Control.Applicative (empty)
 import           Control.Monad
+import           Control.Monad.Reader (runReaderT)
 import           Control.Monad.Trans
 import           Control.Monad.Trans.Maybe
 import           Data.List (find)
@@ -30,8 +31,8 @@ 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.Metaprogramming.Parser (attempt_it)
 import           Wingman.Types
 
 
@@ -53,12 +54,12 @@ hoverProvider state plId (HoverParams (TextDocumentIdentifier uri) (unsafeMkCurr
             Just (trss, program) -> do
               let tr_range = fmap realSrcSpanToRange trss
               HoleJudgment{hj_jdg=jdg, hj_ctx=ctx} <- judgementForHole state nfp tr_range cfg
+              ps <- getParserState state nfp ctx
+              z <- liftIO $ flip runReaderT ps $ attempt_it ctx jdg $ T.unpack program
               pure $ Hover
                 { _contents = HoverContents
                             $ MarkupContent MkMarkdown
-                            $ either T.pack T.pack
-                            $ attempt_it ctx jdg
-                            $ T.unpack program
+                            $ either T.pack T.pack z
                 , _range = Just $ unTrack tr_range
                 }
             Nothing -> empty
diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs
index 8c23873726..cad31a0107 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs
@@ -34,26 +34,28 @@ import           Wingman.FeatureSet
 import           Wingman.GHC
 import           Wingman.Judgements
 import           Wingman.Machinery (useNameFromHypothesis)
+import           Wingman.Metaprogramming.Lexer (ParserContext)
 import           Wingman.Metaprogramming.Parser (parseMetaprogram)
 import           Wingman.Tactics
 import           Wingman.Types
+import Control.Monad.Reader (runReaderT)
 
 
 ------------------------------------------------------------------------------
 -- | A mapping from tactic commands to actual tactics for refinery.
-commandTactic :: TacticCommand -> T.Text -> TacticsM ()
-commandTactic Auto                   = const auto
-commandTactic Intros                 = const intros
-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 . mkVarOcc . T.unpack
-commandTactic Refine                 = const refine
-commandTactic BeginMetaprogram       = const metaprogram
-commandTactic RunMetaprogram         = parseMetaprogram
+commandTactic :: ParserContext -> TacticCommand -> T.Text -> IO (TacticsM ())
+commandTactic _ Auto                   = pure . const auto
+commandTactic _ Intros                 = pure . const intros
+commandTactic _ Destruct               = pure . useNameFromHypothesis destruct . mkVarOcc . T.unpack
+commandTactic _ DestructPun            = pure . useNameFromHypothesis destructPun . mkVarOcc . T.unpack
+commandTactic _ Homomorphism           = pure . useNameFromHypothesis homo . mkVarOcc . T.unpack
+commandTactic _ DestructLambdaCase     = pure . const destructLambdaCase
+commandTactic _ HomomorphismLambdaCase = pure . const homoLambdaCase
+commandTactic _ DestructAll            = pure . const destructAll
+commandTactic _ UseDataCon             = pure . userSplit . mkVarOcc . T.unpack
+commandTactic _ Refine                 = pure . const refine
+commandTactic _ BeginMetaprogram       = pure . const metaprogram
+commandTactic c RunMetaprogram         = flip runReaderT c . parseMetaprogram
 
 
 ------------------------------------------------------------------------------
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs b/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs
index d0f5368e47..ec6dee3310 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs
@@ -3,6 +3,7 @@
 module Wingman.Machinery where
 
 import           Class (Class (classTyVars))
+import           Control.Applicative (empty)
 import           Control.Lens ((<>~))
 import           Control.Monad.Error.Class
 import           Control.Monad.Reader
@@ -22,13 +23,15 @@ import           Data.Monoid (getSum)
 import           Data.Ord (Down (..), comparing)
 import           Data.Set (Set)
 import qualified Data.Set as S
+import           Development.IDE.Core.Compile (lookupName)
 import           Development.IDE.GHC.Compat
-import           OccName (HasOccName (occName))
+import           GhcPlugins (GlobalRdrElt (gre_name), lookupOccEnv, varType)
+import           OccName (HasOccName (occName), OccEnv)
 import           Refinery.ProofState
 import           Refinery.Tactic
 import           Refinery.Tactic.Internal
 import           TcType
-import           Type
+import           Type (tyCoVarsOfTypeWellScoped, splitTyConApp_maybe)
 import           Unify
 import           Wingman.Judgements
 import           Wingman.Simplify (simplify)
@@ -315,3 +318,52 @@ useNameFromHypothesis f name = do
     Just hi -> f hi
     Nothing -> throwError $ NotInScope name
 
+------------------------------------------------------------------------------
+-- | Lift a function over 'HyInfo's to one that takes an 'OccName' and tries to
+-- look it up in the hypothesis.
+useNameFromContext :: (HyInfo CType -> TacticsM a) -> OccName -> TacticsM a
+useNameFromContext f name = do
+  lookupNameInContext name >>= \case
+    Just ty -> f $ createImportedHyInfo name ty
+    Nothing -> throwError $ NotInScope name
+
+
+------------------------------------------------------------------------------
+-- | Find the type of an 'OccName' that is defined in the current module.
+lookupNameInContext :: MonadReader Context m => OccName -> m (Maybe CType)
+lookupNameInContext name = do
+  ctx <- asks ctxModuleFuncs
+  pure $ case find ((== name) . fst) ctx of
+    Just (_, ty) -> pure ty
+    Nothing      -> empty
+
+
+------------------------------------------------------------------------------
+-- | Build a 'HyInfo' for an imported term.
+createImportedHyInfo :: OccName -> CType -> HyInfo CType
+createImportedHyInfo on ty = HyInfo
+  { hi_name = on
+  , hi_provenance = ImportPrv
+  , hi_type = ty
+  }
+
+
+------------------------------------------------------------------------------
+-- | Lookup the type of any 'OccName' that was imported. Necessarily done in
+-- IO, so we only expose this functionality to the parser. Internal Haskell
+-- code that wants to lookup terms should do it via 'KnownThings'.
+getOccNameType
+    :: HscEnv
+    -> OccEnv [GlobalRdrElt]
+    -> Module
+    -> OccName
+    -> IO (Maybe Type)
+getOccNameType hscenv rdrenv modul occ =
+  case lookupOccEnv rdrenv occ of
+    Just (elt : _) -> do
+      mvar <- lookupName hscenv modul $ gre_name elt
+      pure $ case mvar of
+        Just (AnId v) -> pure $ varType v
+        _ -> Nothing
+    _ -> pure Nothing
+
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Lexer.hs b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Lexer.hs
index fb396029a4..e4d62ca085 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Lexer.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Lexer.hs
@@ -7,16 +7,31 @@ module Wingman.Metaprogramming.Lexer where
 
 import           Control.Applicative
 import           Control.Monad
+import           Control.Monad.Reader (ReaderT)
 import           Data.Text (Text)
 import qualified Data.Text as T
 import           Data.Void
+import           Development.IDE.GHC.Compat (HscEnv, Module)
+import           GhcPlugins (GlobalRdrElt)
 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 (Context)
+
+
+------------------------------------------------------------------------------
+-- | Everything we need in order to call 'Wingman.Machinery.getOccNameType'.
+data ParserContext = ParserContext
+  { ps_hscEnv :: HscEnv
+  , ps_occEnv :: OccEnv [GlobalRdrElt]
+  , ps_module :: Module
+  , ps_context :: Context
+  }
+
+type Parser = P.ParsecT Void Text (ReaderT ParserContext IO)
 
 
-type Parser = P.Parsec Void Text
 
 lineComment :: Parser ()
 lineComment = L.skipLineComment "--"
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
index c9f26aa10a..0eb52007af 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
@@ -7,12 +7,17 @@
 module Wingman.Metaprogramming.Parser where
 
 import qualified Control.Monad.Combinators.Expr as P
+import qualified Control.Monad.Error.Class as E
+import           Control.Monad.Reader (ReaderT, ask, MonadIO (liftIO), asks)
 import           Data.Functor
+import           Data.Maybe (listToMaybe)
 import qualified Data.Text as T
+import           GhcPlugins (occNameString)
 import qualified Refinery.Tactic as R
 import qualified Text.Megaparsec as P
 import           Wingman.Auto
-import           Wingman.Machinery (useNameFromHypothesis)
+import           Wingman.Context (getCurrentDefinitions)
+import           Wingman.Machinery (useNameFromHypothesis, getOccNameType, createImportedHyInfo, useNameFromContext, lookupNameInContext)
 import           Wingman.Metaprogramming.Lexer
 import           Wingman.Metaprogramming.ProofState (proofState, layout)
 import           Wingman.Tactics
@@ -22,12 +27,21 @@ 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)
 
+
+------------------------------------------------------------------------------
+-- | Like 'unary_occ', but runs directly in the 'Parser' monad.
+unary_occM :: T.Text -> (OccName -> Parser (TacticsM ())) -> Parser (TacticsM ())
+unary_occM 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
@@ -45,12 +59,25 @@ oneTactic =
     , unary_occ "destruct" $ useNameFromHypothesis destruct
     , unary_occ "homo" $ useNameFromHypothesis homo
     , nullary   "application" application
+    , unary_occ "apply_module" $ useNameFromContext apply
     , unary_occ "apply" $ useNameFromHypothesis apply
     , nullary   "split" split
     , unary_occ "ctor" userSplit
     , nullary   "obvious" obvious
     , nullary   "auto" auto
     , nullary   "sorry" sorry
+    , nullary   "unary" $ nary 1
+    , nullary   "binary" $ nary 2
+    , nullary   "recursion" $
+        fmap listToMaybe getCurrentDefinitions >>= \case
+          Just (self, _) -> useNameFromContext apply self
+          Nothing -> E.throwError $ TacticPanic "no defining function"
+    , unary_occM "use" $ \occ -> do
+        ctx <- asks ps_context
+        ty <- case lookupNameInContext occ ctx of
+          Just ty -> pure ty
+          Nothing -> CType <$> getOccTy occ
+        pure $ apply $ createImportedHyInfo occ ty
     ]
 
 
@@ -83,19 +110,38 @@ wrapError :: String -> String
 wrapError err = "```\n" <> err <> "\n```\n"
 
 
-attempt_it :: Context -> Judgement -> String -> Either String String
+------------------------------------------------------------------------------
+-- | Attempt to run a metaprogram tactic, returning the proof state, or the
+-- errors.
+attempt_it
+    :: Context
+    -> Judgement
+    -> String
+    -> ReaderT ParserContext IO (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>"
+  P.runParserT tacticProgram "<splice>" (T.pack program) <&> \case
+      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 -> ReaderT ParserContext IO (TacticsM ())
+parseMetaprogram
+    = fmap (either (const $ pure ()) id)
+    . P.runParserT tacticProgram "<splice>"
+
+
+------------------------------------------------------------------------------
+-- | Like 'getOccNameType', but runs in the 'Parser' monad.
+getOccTy :: OccName -> Parser Type
+getOccTy occ = do
+  ParserContext hscenv rdrenv modul _ <- ask
+  mty <- liftIO $ getOccNameType hscenv rdrenv modul occ
+  maybe (fail $ occNameString occ <> " is not in scope") pure mty
 
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs b/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs
index 9f0c0ecce3..95cb965f7f 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs
@@ -40,6 +40,7 @@ import           Wingman.Range
 import           Wingman.StaticPlugin
 import           Wingman.Tactics
 import           Wingman.Types
+import Wingman.Metaprogramming.Lexer (ParserContext)
 
 
 descriptor :: PluginId -> PluginDescriptor IdeState
@@ -50,7 +51,7 @@ descriptor plId = (defaultPluginDescriptor plId)
               PluginCommand
                 (tcCommandId tc)
                 (tacticDesc $ tcCommandName tc)
-                (tacticCmd (commandTactic tc) plId))
+                (tacticCmd (flip commandTactic tc) plId))
                 [minBound .. maxBound]
           , pure $
               PluginCommand
@@ -101,7 +102,7 @@ showUserFacingMessage ufm = do
 
 
 tacticCmd
-    :: (T.Text -> TacticsM ())
+    :: (ParserContext -> T.Text -> IO (TacticsM ()))
     -> PluginId
     -> CommandFunction IdeState TacticParams
 tacticCmd tac pId state (TacticParams uri range var_name)
@@ -115,9 +116,11 @@ tacticCmd tac pId state (TacticParams uri range var_name)
         let span = fmap (rangeToRealSrcSpan (fromNormalizedFilePath nfp)) hj_range
         TrackedStale pm pmmap <- stale GetAnnotatedParsedSource
         pm_span <- liftMaybe $ mapAgeFrom pmmap span
+        pc <- getParserState state nfp hj_ctx
+        t <- liftIO $ tac pc var_name
 
         timingOut (cfg_timeout_seconds cfg * seconds) $ join $
-          case runTactic hj_ctx hj_jdg $ tac var_name of
+          case runTactic hj_ctx hj_jdg t of
             Left _ -> Left TacticErrors
             Right rtr ->
               case rtr_extract rtr of
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs
index 52855e1ffe..ada61855fa 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs
@@ -24,21 +24,23 @@ import qualified Data.Set as S
 import           DataCon
 import           Development.IDE.GHC.Compat
 import           GHC.Exts
+import           GHC.SourceGen ((@@))
 import           GHC.SourceGen.Expr
 import           Name (occNameString, occName)
+import           OccName (mkVarOcc)
 import           Refinery.Tactic
 import           Refinery.Tactic.Internal
 import           TcType
 import           Type hiding (Var)
+import           TysPrim (betaTy, alphaTy, betaTyVar, alphaTyVar)
 import           Wingman.CodeGen
 import           Wingman.Context
 import           Wingman.GHC
 import           Wingman.Judgements
 import           Wingman.Machinery
 import           Wingman.Naming
+import           Wingman.StaticPlugin (pattern MetaprogramSyntax)
 import           Wingman.Types
-import OccName (mkVarOcc)
-import Wingman.StaticPlugin (pattern MetaprogramSyntax)
 
 
 ------------------------------------------------------------------------------
@@ -206,7 +208,7 @@ homoLambdaCase =
 
 
 apply :: HyInfo CType -> TacticsM ()
-apply hi = requireConcreteHole $ tracing ("apply' " <> show (hi_name hi)) $ do
+apply hi = tracing ("apply' " <> show (hi_name hi)) $ do
   jdg <- goal
   let g  = jGoal jdg
       ty = unCType $ hi_type hi
@@ -391,7 +393,7 @@ auto' n = do
   try intros
   choice
     [ overFunctions $ \fname -> do
-        apply fname
+        requireConcreteHole $ apply fname
         loop
     , overAlgebraicTerms $ \aname -> do
         destructAuto aname
@@ -434,3 +436,39 @@ applyByName name = do
       True  -> apply hi
       False -> empty
 
+
+------------------------------------------------------------------------------
+-- | Make a function application where the function being applied itself is
+-- a hole.
+applyByType :: Type -> TacticsM ()
+applyByType ty = tracing ("applyByType " <> show ty) $ do
+  jdg <- goal
+  let g  = jGoal jdg
+  ty' <- freshTyvars ty
+  let (_, _, args, ret) = tacticsSplitFunTy ty'
+  rule $ \jdg -> do
+    unify g (CType ret)
+    app <- newSubgoal . blacklistingDestruct $ withNewGoal (CType ty) jdg
+    ext
+        <- fmap unzipTrace
+        $ traverse ( newSubgoal
+                    . blacklistingDestruct
+                    . flip withNewGoal jdg
+                    . CType
+                    ) args
+    pure $
+      fmap noLoc $
+        foldl' (@@)
+          <$> fmap unLoc app
+          <*> fmap (fmap unLoc) ext
+
+
+------------------------------------------------------------------------------
+-- | Make an n-ary function call of the form
+-- @(_ :: forall a b. a -> a -> b) _ _@.
+nary :: Int -> TacticsM ()
+nary n =
+  applyByType $
+    mkInvForAllTys [alphaTyVar, betaTyVar] $
+      mkFunTys' (replicate n alphaTy) betaTy
+
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Types.hs b/plugins/hls-tactics-plugin/src/Wingman/Types.hs
index 657b6ad4c8..bfea1afe4c 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Types.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Types.hs
@@ -212,6 +212,8 @@ data Provenance
       (Uniquely Class)     -- ^ Class
     -- | A binding explicitly written by the user.
   | UserPrv
+    -- | A binding explicitly imported by the user.
+  | ImportPrv
     -- | The recursive hypothesis. Present only in the context of the recursion
     -- tactic.
   | RecursivePrv
@@ -326,6 +328,7 @@ data TacticError
   | UnhelpfulSplit OccName
   | TooPolymorphic
   | NotInScope OccName
+  | TacticPanic String
   deriving stock (Eq)
 
 instance Show TacticError where
@@ -364,6 +367,8 @@ instance Show TacticError where
       "The tactic isn't applicable because the goal is too polymorphic"
     show (NotInScope name) =
       "Tried to do something with the out of scope name " <> show name
+    show (TacticPanic err) =
+      "PANIC: " <> err
 
 
 ------------------------------------------------------------------------------
diff --git a/plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs b/plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs
index 17750c93ca..e2e6c6cca3 100644
--- a/plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs
+++ b/plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs
@@ -28,4 +28,7 @@ spec = do
     metaTest  2 32 "MetaBindAll"
     metaTest  2 13 "MetaTry"
     metaTest  2 74 "MetaChoice"
+    metaTest  5 40 "MetaUseImport"
+    metaTest  6 31 "MetaUseLocal"
+    metaTest 11 11 "MetaUseMethod"
 
diff --git a/plugins/hls-tactics-plugin/test/golden/MetaUseImport.expected.hs b/plugins/hls-tactics-plugin/test/golden/MetaUseImport.expected.hs
new file mode 100644
index 0000000000..c72f18589c
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/MetaUseImport.expected.hs
@@ -0,0 +1,6 @@
+import Data.Char
+
+
+result :: Char -> Bool
+result = isAlpha
+
diff --git a/plugins/hls-tactics-plugin/test/golden/MetaUseImport.hs b/plugins/hls-tactics-plugin/test/golden/MetaUseImport.hs
new file mode 100644
index 0000000000..87ac26bbcb
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/MetaUseImport.hs
@@ -0,0 +1,6 @@
+import Data.Char
+
+
+result :: Char -> Bool
+result = [wingman| intro c, use isAlpha, assume c |]
+
diff --git a/plugins/hls-tactics-plugin/test/golden/MetaUseLocal.expected.hs b/plugins/hls-tactics-plugin/test/golden/MetaUseLocal.expected.hs
new file mode 100644
index 0000000000..1afee3471a
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/MetaUseLocal.expected.hs
@@ -0,0 +1,7 @@
+test :: Int
+test = 0
+
+
+resolve :: Int
+resolve = test
+
diff --git a/plugins/hls-tactics-plugin/test/golden/MetaUseLocal.hs b/plugins/hls-tactics-plugin/test/golden/MetaUseLocal.hs
new file mode 100644
index 0000000000..0f791818d1
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/MetaUseLocal.hs
@@ -0,0 +1,7 @@
+test :: Int
+test = 0
+
+
+resolve :: Int
+resolve = [wingman| use test |]
+
diff --git a/plugins/hls-tactics-plugin/test/golden/MetaUseMethod.expected.hs b/plugins/hls-tactics-plugin/test/golden/MetaUseMethod.expected.hs
new file mode 100644
index 0000000000..acf46a75a0
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/MetaUseMethod.expected.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE MultiParamTypeClasses #-}
+
+class Test where
+  test :: Int
+
+instance Test where
+  test = 10
+
+
+resolve :: Int
+resolve = test
+
diff --git a/plugins/hls-tactics-plugin/test/golden/MetaUseMethod.hs b/plugins/hls-tactics-plugin/test/golden/MetaUseMethod.hs
new file mode 100644
index 0000000000..4723befd10
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/MetaUseMethod.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE MultiParamTypeClasses #-}
+
+class Test where
+  test :: Int
+
+instance Test where
+  test = 10
+
+
+resolve :: Int
+resolve = [wingman| use test |]
+