diff --git a/plugins/hls-tactics-plugin/COMMANDS.md b/plugins/hls-tactics-plugin/COMMANDS.md
index 3405f664c1..be3cc59b39 100644
--- a/plugins/hls-tactics-plugin/COMMANDS.md
+++ b/plugins/hls-tactics-plugin/COMMANDS.md
@@ -23,6 +23,7 @@ running  `application` will produce:
 ```haskell
 f (_ :: a)
 ```
+
 ## apply
 
 arguments: single reference.  
@@ -46,6 +47,7 @@ running  `apply f` will produce:
 ```haskell
 f (_ :: a)
 ```
+
 ## assume
 
 arguments: single reference.  
@@ -69,6 +71,7 @@ running  `assume some_a_val` will produce:
 ```haskell
 some_a_val
 ```
+
 ## assumption
 
 arguments: none.  
@@ -92,6 +95,7 @@ running  `assumption` will produce:
 ```haskell
 some_a_val
 ```
+
 ## auto
 
 arguments: none.  
@@ -116,6 +120,7 @@ running  `auto` will produce:
 ```haskell
 g . f
 ```
+
 ## binary
 
 arguments: none.  
@@ -139,6 +144,7 @@ running  `binary` will produce:
 ```haskell
 (_3 :: a -> a -> Int) (_1 :: a) (_2 :: a)
 ```
+
 ## cata
 
 arguments: single reference.  
@@ -168,6 +174,7 @@ case x of
         a2_c = f a2
      in _
 ```
+
 ## collapse
 
 arguments: none.  
@@ -193,6 +200,7 @@ running  `collapse` will produce:
 ```haskell
 (_ :: a -> a -> a -> a) a1 a2 a3
 ```
+
 ## ctor
 
 arguments: single reference.  
@@ -214,6 +222,7 @@ running  `ctor Just` will produce:
 ```haskell
 Just (_ :: a)
 ```
+
 ## destruct
 
 arguments: single reference.  
@@ -239,6 +248,7 @@ case a of
   False -> _
   True -> _
 ```
+
 ## destruct_all
 
 arguments: none.  
@@ -271,6 +281,7 @@ case a of
     Nothing -> _
     Just i -> _
 ```
+
 ## homo
 
 arguments: single reference.  
@@ -298,6 +309,7 @@ case e of
   Left a -> Left (_ :: x)
   Right b -> Right (_ :: y)
 ```
+
 ## intro
 
 arguments: single binding.  
@@ -319,6 +331,7 @@ running  `intro aye` will produce:
 ```haskell
 \aye -> (_ :: b -> c -> d)
 ```
+
 ## intros
 
 arguments: varadic binding.  
@@ -368,6 +381,29 @@ running  `intros x y z w` will produce:
 ```haskell
 \x y z -> (_ :: d)
 ```
+
+## nested
+
+arguments: single reference.  
+non-deterministic.
+
+> Nest the given function (in module scope) with itself arbitrarily many times. NOTE: The resulting function is necessarily unsaturated, so you will likely need `with_arg` to use this tactic in a saturated context.
+
+
+### Example
+
+Given:
+
+```haskell
+_ :: [(Int, Either Bool a)] -> [(Int, Either Bool b)]
+```
+
+running  `nested fmap` will produce:
+
+```haskell
+fmap (fmap (fmap _))
+```
+
 ## obvious
 
 arguments: none.  
@@ -389,6 +425,7 @@ running  `obvious` will produce:
 ```haskell
 []
 ```
+
 ## pointwise
 
 arguments: tactic.  
@@ -412,6 +449,7 @@ running  `pointwise (use mappend)` will produce:
 ```haskell
 mappend _ _
 ```
+
 ## recursion
 
 arguments: none.  
@@ -435,6 +473,7 @@ running  `recursion` will produce:
 ```haskell
 foo (_ :: Int) (_ :: b)
 ```
+
 ## sorry
 
 arguments: none.  
@@ -456,6 +495,7 @@ running  `sorry` will produce:
 ```haskell
 _ :: b
 ```
+
 ## split
 
 arguments: none.  
@@ -477,6 +517,38 @@ running  `split` will produce:
 ```haskell
 Right (_ :: b)
 ```
+
+## try
+
+arguments: tactic.  
+non-deterministic.
+
+> Simultaneously run and do not run a tactic. Subsequent tactics will bind on both states.
+
+
+### Example
+
+Given:
+
+```haskell
+f :: a -> b
+
+_ :: b
+```
+
+running  `try (apply f)` will produce:
+
+```haskell
+-- BOTH of:
+
+f (_ :: a)
+
+-- and
+
+_ :: b
+
+```
+
 ## unary
 
 arguments: none.  
@@ -500,6 +572,7 @@ running  `unary` will produce:
 ```haskell
 (_2 :: a -> Int) (_1 :: a)
 ```
+
 ## use
 
 arguments: single reference.  
@@ -523,3 +596,28 @@ running  `use isSpace` will produce:
 ```haskell
 isSpace (_ :: Char)
 ```
+
+## with_arg
+
+arguments: none.  
+deterministic.
+
+> Fill the current goal with a function application. This can be useful when you'd like to fill in the argument before the function, or when you'd like to use a non-saturated function in a saturated context.
+
+
+### Example
+
+> Where `a` is a new unifiable type variable.
+
+Given:
+
+```haskell
+_ :: r
+```
+
+running  `with_arg` will produce:
+
+```haskell
+(_2 :: a -> r) (_1 :: a)
+```
+
diff --git a/plugins/hls-tactics-plugin/src/Wingman/GHC.hs b/plugins/hls-tactics-plugin/src/Wingman/GHC.hs
index d39ed21587..da4a5e6642 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/GHC.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/GHC.hs
@@ -113,7 +113,7 @@ freshTyvars t = do
         case M.lookup tv reps of
           Just tv' -> tv'
           Nothing  -> tv
-      ) t
+      ) $ snd $ tcSplitForAllTys t
 
 
 ------------------------------------------------------------------------------
diff --git a/plugins/hls-tactics-plugin/src/Wingman/KnownStrategies.hs b/plugins/hls-tactics-plugin/src/Wingman/KnownStrategies.hs
index 913fcd5799..b158f3364a 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/KnownStrategies.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/KnownStrategies.hs
@@ -35,7 +35,7 @@ deriveFmap = do
   try intros
   overAlgebraicTerms homo
   choice
-    [ overFunctions apply >> auto' 2
+    [ overFunctions (apply Saturated) >> auto' 2
     , assumption
     , recursion
     ]
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
index 61fe043442..1025d07218 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
@@ -188,7 +188,7 @@ commands =
 
   , command "apply" Deterministic (Ref One)
       "Apply the given function from *local* scope."
-      (pure . useNameFromHypothesis apply)
+      (pure . useNameFromHypothesis (apply Saturated))
       [ Example
           Nothing
           ["f"]
@@ -295,7 +295,7 @@ commands =
       "Fill the current hole with a call to the defining function."
       ( pure $
           fmap listToMaybe getCurrentDefinitions >>= \case
-            Just (self, _) -> useNameFromContext apply self
+            Just (self, _) -> useNameFromContext (apply Saturated) self
             Nothing -> E.throwError $ TacticPanic "no defining function"
       )
       [ Example
@@ -308,13 +308,7 @@ commands =
 
   , command "use" Deterministic (Ref One)
       "Apply the given function from *module* scope."
-      ( \occ -> pure $ do
-          ctx <- ask
-          ty <- case lookupNameInContext occ ctx of
-            Just ty -> pure ty
-            Nothing -> CType <$> getOccNameType occ
-          apply $ createImportedHyInfo occ ty
-      )
+      (pure . use Saturated)
       [ Example
           (Just "`import Data.Char (isSpace)`")
           ["isSpace"]
@@ -354,6 +348,44 @@ commands =
           "(_ :: a -> a -> a -> a) a1 a2 a3"
       ]
 
+  , command "try" Nondeterministic Tactic
+      "Simultaneously run and do not run a tactic. Subsequent tactics will bind on both states."
+      (pure . R.try)
+      [ Example
+          Nothing
+          ["(apply f)"]
+          [ EHI "f" "a -> b"
+          ]
+          (Just "b")
+          $ T.pack $ unlines
+            [ "-- BOTH of:\n"
+            , "f (_ :: a)"
+            , "\n-- and\n"
+            , "_ :: b"
+            ]
+      ]
+
+  , command "nested" Nondeterministic (Ref One)
+      "Nest the given function (in module scope) with itself arbitrarily many times. NOTE: The resulting function is necessarily unsaturated, so you will likely need `with_arg` to use this tactic in a saturated context."
+      (pure . nested)
+      [ Example
+          Nothing
+          ["fmap"]
+          []
+          (Just "[(Int, Either Bool a)] -> [(Int, Either Bool b)]")
+          "fmap (fmap (fmap _))"
+      ]
+
+  , command "with_arg" Deterministic Nullary
+      "Fill the current goal with a function application. This can be useful when you'd like to fill in the argument before the function, or when you'd like to use a non-saturated function in a saturated context."
+      (pure with_arg)
+      [ Example
+          (Just "Where `a` is a new unifiable type variable.")
+          []
+          []
+          (Just "r")
+          "(_2 :: a -> r) (_1 :: a)"
+      ]
   ]
 
 
@@ -369,14 +401,9 @@ oneTactic =
 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.InfixR (symbol "|"   $> (R.<%>) )]
     , [ P.InfixL (symbol ";"   $> (>>))
       , P.InfixL (symbol ","   $> bindOne)
       ]
@@ -426,7 +453,7 @@ parseMetaprogram
 -- | Automatically generate the metaprogram command reference.
 writeDocumentation :: IO ()
 writeDocumentation =
-  writeFile "plugins/hls-tactics-plugin/COMMANDS.md" $
+  writeFile "COMMANDS.md" $
     unlines
       [ "# Wingman Metaprogram Command Reference"
       , ""
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser/Documentation.hs b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser/Documentation.hs
index 632c5cad1a..b63dea6f08 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser/Documentation.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser/Documentation.hs
@@ -150,6 +150,7 @@ prettyCommand (MC name syn det desc _ exs) = vsep
   , ">" <+> align (pretty desc)
   , mempty
   , vsep $ fmap (prettyExample name) exs
+  , mempty
   ]
 
 
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs
index be831c4287..b4df0940fc 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs
@@ -19,6 +19,7 @@ import           Data.Foldable
 import           Data.Functor ((<&>))
 import           Data.Generics.Labels ()
 import           Data.List
+import           Data.List.Extra (dropEnd, takeEnd)
 import qualified Data.Map as M
 import           Data.Maybe
 import           Data.Set (Set)
@@ -69,6 +70,18 @@ assume name = rule $ \jdg -> do
     Nothing -> throwError $ UndefinedHypothesis name
 
 
+------------------------------------------------------------------------------
+-- | Like 'apply', but uses an 'OccName' available in the context
+-- or the module
+use :: Saturation -> OccName -> TacticsM ()
+use sat occ = do
+  ctx <- ask
+  ty <- case lookupNameInContext occ ctx of
+    Just ty -> pure ty
+    Nothing -> CType <$> getOccNameType occ
+  apply sat $ createImportedHyInfo occ ty
+
+
 recursion :: TacticsM ()
 -- TODO(sandy): This tactic doesn't fire for the @AutoThetaFix@ golden test,
 -- presumably due to running afoul of 'requireConcreteHole'. Look into this!
@@ -90,7 +103,7 @@ recursion = requireConcreteHole $ tracing "recursion" $ do
 
     let hy' = recursiveHypothesis defs
     ctx <- ask
-    localTactic (apply $ HyInfo name RecursivePrv ty) (introduce ctx hy')
+    localTactic (apply Saturated $ HyInfo name RecursivePrv ty) (introduce ctx hy')
       <@> fmap (localTactic assumption . filterPosition name) [0..]
 
 
@@ -214,30 +227,39 @@ homoLambdaCase =
         $ jGoal jdg
 
 
-apply :: HyInfo CType -> TacticsM ()
-apply hi = tracing ("apply' " <> show (hi_name hi)) $ do
+data Saturation = Unsaturated Int
+  deriving (Eq, Ord, Show)
+
+pattern Saturated :: Saturation
+pattern Saturated = Unsaturated 0
+
+
+apply :: Saturation -> HyInfo CType -> TacticsM ()
+apply (Unsaturated n) hi = tracing ("apply' " <> show (hi_name hi)) $ do
   jdg <- goal
   let g  = jGoal jdg
       ty = unCType $ hi_type hi
       func = hi_name hi
   ty' <- freshTyvars ty
-  let (_, _, args, ret) = tacticsSplitFunTy ty'
+  let (_, _, all_args, ret) = tacticsSplitFunTy ty'
+      saturated_args = dropEnd n all_args
+      unsaturated_args = takeEnd n all_args
   rule $ \jdg -> do
-    unify g (CType ret)
+    unify g (CType $ mkFunTys' unsaturated_args ret)
     ext
         <- fmap unzipTrace
         $ traverse ( newSubgoal
                     . blacklistingDestruct
                     . flip withNewGoal jdg
                     . CType
-                    ) args
+                    ) saturated_args
     pure $
       ext
         & #syn_used_vals %~ S.insert func
         & #syn_val       %~ mkApply func . fmap unLoc
 
 application :: TacticsM ()
-application = overFunctions apply
+application = overFunctions $ apply Saturated
 
 
 ------------------------------------------------------------------------------
@@ -402,7 +424,7 @@ auto' n = do
   try intros
   choice
     [ overFunctions $ \fname -> do
-        requireConcreteHole $ apply fname
+        requireConcreteHole $ apply Saturated fname
         loop
     , overAlgebraicTerms $ \aname -> do
         destructAuto aname
@@ -433,7 +455,7 @@ applyMethod cls df method_name = do
     Just method -> do
       let (_, apps) = splitAppTys df
       let ty = piResultTys (idType method) apps
-      apply $ HyInfo method_name (ClassMethodPrv $ Uniquely cls) $ CType ty
+      apply Saturated $ HyInfo method_name (ClassMethodPrv $ Uniquely cls) $ CType ty
     Nothing -> throwError $ NotInScope method_name
 
 
@@ -442,7 +464,7 @@ applyByName name = do
   g <- goal
   choice $ (unHypothesis (jHypothesis g)) <&> \hi ->
     case hi_name hi == name of
-      True  -> apply hi
+      True  -> apply Saturated hi
       False -> empty
 
 
@@ -485,7 +507,7 @@ nary n =
 self :: TacticsM ()
 self =
   fmap listToMaybe getCurrentDefinitions >>= \case
-    Just (self, _) -> useNameFromContext apply self
+    Just (self, _) -> useNameFromContext (apply Saturated) self
     Nothing -> throwError $ TacticPanic "no defining function"
 
 
@@ -514,6 +536,30 @@ cata hi = do
       $ Hypothesis unifiable_diff
 
 
+------------------------------------------------------------------------------
+-- | Deeply nest an unsaturated function onto itself
+nested :: OccName -> TacticsM ()
+nested = deepening . use (Unsaturated 1)
+
+
+------------------------------------------------------------------------------
+-- | Repeatedly bind a tactic on its first hole
+deep :: Int -> TacticsM () -> TacticsM ()
+deep 0 _ = pure ()
+deep n t = foldr1 bindOne $ replicate n t
+
+
+------------------------------------------------------------------------------
+-- | Try 'deep' for arbitrary depths.
+deepening :: TacticsM () -> TacticsM ()
+deepening t =
+  asum $ fmap (flip deep t) [0 .. 100]
+
+
+bindOne :: TacticsM a -> TacticsM a -> TacticsM a
+bindOne t t1 = t <@> [t1]
+
+
 collapse :: TacticsM ()
 collapse = do
   g <- goal
@@ -523,6 +569,15 @@ collapse = do
     _    -> nary (length terms) <@> fmap (assume . hi_name) terms
 
 
+with_arg :: TacticsM ()
+with_arg = rule $ \jdg -> do
+  let g = jGoal jdg
+  fresh_ty <- freshTyvars $ mkInvForAllTys [alphaTyVar] alphaTy
+  a <- newSubgoal $ withNewGoal (CType fresh_ty) jdg
+  f <- newSubgoal $ withNewGoal (coerce mkFunTys' [fresh_ty] g) jdg
+  pure $ fmap noLoc $ (@@) <$> fmap unLoc f <*> fmap unLoc a
+
+
 ------------------------------------------------------------------------------
 -- | Determine the difference in hypothesis due to running a tactic. Also, it
 -- runs the tactic.
diff --git a/plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs b/plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs
index e6ec079562..03efe5c266 100644
--- a/plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs
+++ b/plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs
@@ -36,3 +36,6 @@ spec = do
     metaTest 10 32 "MetaCataAST"
     metaTest  6 46 "MetaPointwise"
     metaTest  4 28 "MetaUseSymbol"
+    metaTest  7 53 "MetaDeepOf"
+    metaTest  2 34 "MetaWithArg"
+
diff --git a/plugins/hls-tactics-plugin/test/golden/MetaDeepOf.expected.hs b/plugins/hls-tactics-plugin/test/golden/MetaDeepOf.expected.hs
new file mode 100644
index 0000000000..90216da0a2
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/MetaDeepOf.expected.hs
@@ -0,0 +1,8 @@
+whats_it_deep_of
+    :: (a -> a)
+    -> [(Int, Either Bool (Maybe [a]))]
+    -> [(Int, Either Bool (Maybe [a]))]
+-- The assumption here is necessary to tie-break in favor of the longest
+-- nesting of fmaps.
+whats_it_deep_of f = fmap (fmap (fmap (fmap (fmap f))))
+
diff --git a/plugins/hls-tactics-plugin/test/golden/MetaDeepOf.hs b/plugins/hls-tactics-plugin/test/golden/MetaDeepOf.hs
new file mode 100644
index 0000000000..3afcdcc4e1
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/MetaDeepOf.hs
@@ -0,0 +1,8 @@
+whats_it_deep_of
+    :: (a -> a)
+    -> [(Int, Either Bool (Maybe [a]))]
+    -> [(Int, Either Bool (Maybe [a]))]
+-- The assumption here is necessary to tie-break in favor of the longest
+-- nesting of fmaps.
+whats_it_deep_of f = [wingman| nested fmap, assumption |]
+
diff --git a/plugins/hls-tactics-plugin/test/golden/MetaTry.hs b/plugins/hls-tactics-plugin/test/golden/MetaTry.hs
index d92c4a5763..582189bcbc 100644
--- a/plugins/hls-tactics-plugin/test/golden/MetaTry.hs
+++ b/plugins/hls-tactics-plugin/test/golden/MetaTry.hs
@@ -1,2 +1,2 @@
 foo :: a -> (b, a)
-foo a = [wingman| split; try assumption |]
+foo a = [wingman| split; try (assumption) |]
diff --git a/plugins/hls-tactics-plugin/test/golden/MetaWithArg.expected.hs b/plugins/hls-tactics-plugin/test/golden/MetaWithArg.expected.hs
new file mode 100644
index 0000000000..4110ddcbb4
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/MetaWithArg.expected.hs
@@ -0,0 +1,2 @@
+wat :: a -> b
+wat a = _ a
diff --git a/plugins/hls-tactics-plugin/test/golden/MetaWithArg.hs b/plugins/hls-tactics-plugin/test/golden/MetaWithArg.hs
new file mode 100644
index 0000000000..75c6ab0445
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/MetaWithArg.hs
@@ -0,0 +1,2 @@
+wat :: a -> b
+wat a = [wingman| with_arg, assumption |]