diff --git a/hls-tactics-plugin.cabal b/hls-tactics-plugin.cabal
--- a/hls-tactics-plugin.cabal
+++ b/hls-tactics-plugin.cabal
@@ -1,7 +1,7 @@
 cabal-version:      2.4
 category:           Development
 name:               hls-tactics-plugin
-version:            1.5.0.1
+version:            1.6.0.0
 synopsis:           Wingman plugin for Haskell Language Server
 description:
   Please see the README on GitHub at <https://github.com/haskell/haskell-language-server#readme>
@@ -82,9 +82,9 @@
     , ghc-boot-th
     , ghc-exactprint
     , ghc-source-gen        ^>=0.4.1
-    , ghcide                ^>=1.5.0
+    , ghcide                ^>=1.6
     , hls-graph
-    , hls-plugin-api        >=1.1     && <1.3
+    , hls-plugin-api        ^>=1.3
     , hyphenation
     , lens
     , lsp
@@ -160,7 +160,7 @@
     , ghcide
     , hls-plugin-api
     , hls-tactics-plugin
-    , hls-test-utils      >=1.0 && <1.2
+    , hls-test-utils      ^>=1.2
     , hspec
     , hspec-expectations
     , lens
diff --git a/src/Refinery/Future.hs b/src/Refinery/Future.hs
--- a/src/Refinery/Future.hs
+++ b/src/Refinery/Future.hs
@@ -113,7 +113,7 @@
          -- This would happen when we had a handler that wasn't followed by an error call.
          --     pair >> goal >>= \g -> (handler_ $ \_ -> traceM $ "Handling " <> show g) <|> failure "Error"
          -- We would see the "Handling a" message when solving for b.
-         (go s' (goals ++ [(meta, goal)]) pure $ k h)
+         go s' (goals ++ [(meta, goal)]) pure $ k h
       go s goals handlers (Effect m) = m >>= go s goals handlers
       go s goals handlers (Stateful f) =
           let (s', p) = f s
@@ -121,10 +121,10 @@
       go s goals handlers (Alt p1 p2) =
           unListT $ ListT (go s goals handlers p1) <|> ListT (go s goals handlers p2)
       go s goals handlers (Interleave p1 p2) =
-          interleaveT <$> (go s goals handlers p1) <*> (go s goals handlers p2)
+          interleaveT <$> go s goals handlers p1 <*> go s goals handlers p2
       go s goals handlers (Commit p1 p2) = do
           solns <- force =<< go s goals handlers p1
-          if (any isRight solns) then pure $ ofList solns else go s goals handlers p2
+          if any isRight solns then pure $ ofList solns else go s goals handlers p2
       go _ _ _ Empty = pure Done
       go _ _ handlers (Failure err _) = do
           annErr <- handlers err
diff --git a/src/Wingman/AbstractLSP.hs b/src/Wingman/AbstractLSP.hs
--- a/src/Wingman/AbstractLSP.hs
+++ b/src/Wingman/AbstractLSP.hs
@@ -1,6 +1,5 @@
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE RecordWildCards     #-}
-{-# LANGUAGE StandaloneDeriving  #-}
 
 {-# LANGUAGE NoMonoLocalBinds    #-}
 
@@ -30,6 +29,7 @@
 import           Wingman.AbstractLSP.Types
 import           Wingman.EmptyCase (fromMaybeT)
 import           Wingman.LanguageServer (getTacticConfig, getIdeDynflags, mkWorkspaceEdits, runStaleIde, showLspMessage, mkShowMessageParams)
+import           Wingman.StaticPlugin (enableQuasiQuotes)
 import           Wingman.Types
 
 
@@ -94,12 +94,13 @@
               , _xdata =  Nothing
               } ) $ do
       env@LspEnv{..} <- buildEnv state plId fc
-      let stale a = runStaleIde "runContinuation" state (fc_nfp le_fileContext) a
+      nfp <- getNfp $ fc_uri le_fileContext
+      let stale a = runStaleIde "runContinuation" state nfp a
       args <- fetchTargetArgs @a env
       res <- c_runCommand cont env args fc b
 
       -- This block returns a maybe error.
-      fmap (maybe (Right $ A.Null) Left . coerce . foldMap Last) $
+      fmap (maybe (Right A.Null) Left . coerce . foldMap Last) $
         for res $ \case
           ErrorMessages errs -> do
             traverse_ showUserFacingMessage errs
@@ -110,7 +111,7 @@
           GraftEdit gr -> do
             ccs <- lift getClientCapabilities
             TrackedStale pm _ <- mapMaybeT liftIO $ stale GetAnnotatedParsedSource
-            case mkWorkspaceEdits le_dflags ccs (fc_uri le_fileContext) (unTrack pm) gr of
+            case mkWorkspaceEdits (enableQuasiQuotes le_dflags) ccs (fc_uri le_fileContext) (unTrack pm) gr of
               Left errs ->
                 pure $ Just $ ResponseError
                   { _code    = InternalError
@@ -119,7 +120,7 @@
                   }
               Right edits -> do
                 sendEdits edits
-                pure $ Nothing
+                pure Nothing
 
 
 ------------------------------------------------------------------------------
@@ -152,7 +153,8 @@
     -> MaybeT (LspM Plugin.Config) LspEnv
 buildEnv state plId fc = do
   cfg <- lift $ getTacticConfig plId
-  dflags <- mapMaybeT liftIO $ getIdeDynflags state $ fc_nfp fc
+  nfp <- getNfp $ fc_uri fc
+  dflags <- mapMaybeT liftIO $ getIdeDynflags state nfp
   pure $ LspEnv
     { le_ideState = state
     , le_pluginId = plId
@@ -174,22 +176,19 @@
        )
     -> PluginMethodHandler IdeState TextDocumentCodeAction
 codeActionProvider sort k state plId
-                   (CodeActionParams _ _ (TextDocumentIdentifier uri) range _)
-  | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do
-      fromMaybeT (Right $ List []) $ do
-        let fc = FileContext
-                   { fc_uri   = uri
-                   , fc_nfp   = nfp
-                   , fc_range = Just $ unsafeMkCurrent range
-                   }
-        env <- buildEnv state plId fc
-        args <- fetchTargetArgs @target env
-        actions <- k env args
-        pure
-          $ Right
-          $ List
-          $ fmap (InR . uncurry (makeCodeAction plId fc sort)) actions
-codeActionProvider _ _ _ _ _ = pure $ Right $ List []
+                   (CodeActionParams _ _ (TextDocumentIdentifier uri) range _) = do
+  fromMaybeT (Right $ List []) $ do
+    let fc = FileContext
+                { fc_uri   = uri
+                , fc_range = Just $ unsafeMkCurrent range
+                }
+    env <- buildEnv state plId fc
+    args <- fetchTargetArgs @target env
+    actions <- k env args
+    pure
+      $ Right
+      $ List
+      $ fmap (InR . uncurry (makeCodeAction plId fc sort)) actions
 
 
 ------------------------------------------------------------------------------
@@ -204,12 +203,10 @@
       )
     -> PluginMethodHandler IdeState TextDocumentCodeLens
 codeLensProvider sort k state plId
-                 (CodeLensParams _ _ (TextDocumentIdentifier uri))
-  | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do
+                 (CodeLensParams _ _ (TextDocumentIdentifier uri)) = do
       fromMaybeT (Right $ List []) $ do
         let fc = FileContext
                    { fc_uri   = uri
-                   , fc_nfp   = nfp
                    , fc_range = Nothing
                    }
         env <- buildEnv state plId fc
@@ -219,7 +216,6 @@
           $ Right
           $ List
           $ fmap (uncurry3 $ makeCodeLens plId sort fc) actions
-codeLensProvider _ _ _ _ _ = pure $ Right $ List []
 
 
 ------------------------------------------------------------------------------
diff --git a/src/Wingman/AbstractLSP/TacticActions.hs b/src/Wingman/AbstractLSP/TacticActions.hs
--- a/src/Wingman/AbstractLSP/TacticActions.hs
+++ b/src/Wingman/AbstractLSP/TacticActions.hs
@@ -45,9 +45,10 @@
               }
     )
     $ \LspEnv{..} HoleJudgment{..} FileContext{..} var_name -> do
-        let stale a = runStaleIde "tacticCmd" le_ideState fc_nfp a
+        nfp <- getNfp fc_uri
+        let stale a = runStaleIde "tacticCmd" le_ideState nfp a
 
-        let span = fmap (rangeToRealSrcSpan (fromNormalizedFilePath fc_nfp)) hj_range
+        let span = fmap (rangeToRealSrcSpan (fromNormalizedFilePath nfp)) hj_range
         TrackedStale _ pmmap <- mapMaybeT liftIO $ stale GetAnnotatedParsedSource
         pm_span <- liftMaybe $ mapAgeFrom pmmap span
         IdeOptions{optTesting = IdeTesting isTesting} <-
@@ -161,8 +162,8 @@
   | dst `isSubspanOf` src = do
       L _ dec <- annotateDecl dflags $ make_decl name pats
       case dec of
-        ValD _ (FunBind { fun_matches = MG { mg_alts = L _ alts@(first_match : _)}
-                  }) -> do
+        ValD _ FunBind{ fun_matches = MG { mg_alts = L _ alts@(first_match : _)}
+                      } -> do
           -- For whatever reason, ExactPrint annotates newlines to the ends of
           -- case matches and type signatures, but only allows us to insert
           -- them at the beginning of those things. Thus, we need want to
diff --git a/src/Wingman/AbstractLSP/Types.hs b/src/Wingman/AbstractLSP/Types.hs
--- a/src/Wingman/AbstractLSP/Types.hs
+++ b/src/Wingman/AbstractLSP/Types.hs
@@ -121,7 +121,6 @@
 -- | What file are we looking at, and what bit of it?
 data FileContext = FileContext
   { fc_uri      :: Uri
-  , fc_nfp      :: NormalizedFilePath
   , fc_range    :: Maybe (Tracked 'Current Range)
     -- ^ For code actions, this is 'Just'. For code lenses, you'll get
     -- a 'Nothing' in the request, and a 'Just' in the response.
@@ -129,12 +128,7 @@
   deriving stock (Eq, Ord, Show, Generic)
   deriving anyclass (A.ToJSON, A.FromJSON)
 
-deriving anyclass instance A.ToJSON NormalizedFilePath
-deriving anyclass instance A.ToJSON NormalizedUri
-deriving anyclass instance A.FromJSON NormalizedFilePath
-deriving anyclass instance A.FromJSON NormalizedUri
 
-
 ------------------------------------------------------------------------------
 -- | Everything we need to resolve continuations.
 data LspEnv = LspEnv
@@ -162,10 +156,14 @@
 data HoleTarget = HoleTarget
   deriving stock (Eq, Ord, Show, Enum, Bounded)
 
+getNfp :: Applicative m => Uri -> MaybeT m NormalizedFilePath
+getNfp = MaybeT . pure . uriToNormalizedFilePath . toNormalizedUri
+
 instance IsTarget HoleTarget where
   type TargetArgs HoleTarget = HoleJudgment
   fetchTargetArgs LspEnv{..} = do
     let FileContext{..} = le_fileContext
     range <- MaybeT $ pure fc_range
-    mapMaybeT liftIO $ judgementForHole le_ideState fc_nfp range le_config
+    nfp <- getNfp fc_uri
+    mapMaybeT liftIO $ judgementForHole le_ideState nfp range le_config
 
diff --git a/src/Wingman/CaseSplit.hs b/src/Wingman/CaseSplit.hs
--- a/src/Wingman/CaseSplit.hs
+++ b/src/Wingman/CaseSplit.hs
@@ -105,5 +105,5 @@
 iterateSplit :: AgdaMatch -> [AgdaMatch]
 iterateSplit am =
   let iterated = iterate (agdaSplit =<<) $ pure am
-   in fmap wildify . head . drop 5 $ iterated
+   in fmap wildify . (!! 5) $ iterated
 
diff --git a/src/Wingman/CodeGen.hs b/src/Wingman/CodeGen.hs
--- a/src/Wingman/CodeGen.hs
+++ b/src/Wingman/CodeGen.hs
@@ -1,8 +1,8 @@
+{-# LANGUAGE CPP               #-}
 {-# LANGUAGE FlexibleContexts  #-}
 {-# LANGUAGE OverloadedLabels  #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE TupleSections     #-}
-{-# LANGUAGE TypeApplications  #-}
 
 module Wingman.CodeGen
   ( module Wingman.CodeGen
@@ -57,7 +57,7 @@
     Just (dcs, apps) ->
       fmap unzipTrace $ for dcs $ \dc -> do
         let con = RealDataCon dc
-            ev = concatMap mkEvidence $ dataConInstArgTys dc apps
+            ev = concatMap (mkEvidence . scaledThing) $ dataConInstArgTys dc apps
             -- We explicitly do not need to add the method hypothesis to
             -- #syn_scoped
             method_hy = foldMap evidenceToHypothesis ev
@@ -141,8 +141,7 @@
         in (names', )
          $ ConPatIn (noLoc $ Unqual $ occName $ conLikeName con)
          $ RecCon
-         $ HsRecFields rec_fields
-         $ Nothing
+         $ HsRecFields rec_fields Nothing
   | otherwise =
       (names, ) $ infixifyPatIfNecessary con $
         conP
@@ -186,7 +185,7 @@
       -- ^ Types of arguments to the ConLike with returned type is instantiated with the second argument.
 conLikeInstOrigArgTys' con uniTys =
   let exvars = conLikeExTys con
-   in conLikeInstOrigArgTys con $
+   in fmap scaledThing $ conLikeInstOrigArgTys con $
         uniTys ++ fmap mkTyVarTy exvars
       -- Rationale: At least in GHC <= 8.10, 'dataConInstOrigArgTys'
       -- unifies the second argument with DataCon's universals followed by existentials.
@@ -208,7 +207,7 @@
 
 destruct' :: Bool -> (ConLike -> Judgement -> Rule) -> HyInfo CType -> Judgement -> Rule
 destruct' use_field_puns f hi jdg = do
-  when (isDestructBlacklisted jdg) $ cut -- throwError NoApplicableTactic
+  when (isDestructBlacklisted jdg) cut -- throwError NoApplicableTactic
   let term = hi_name hi
   ext
       <- destructMatches
@@ -227,10 +226,14 @@
 -- resulting matches.
 destructLambdaCase' :: Bool -> (ConLike -> Judgement -> Rule) -> Judgement -> Rule
 destructLambdaCase' use_field_puns f jdg = do
-  when (isDestructBlacklisted jdg) $ cut -- throwError NoApplicableTactic
+  when (isDestructBlacklisted jdg) cut -- throwError NoApplicableTactic
   let g  = jGoal jdg
   case splitFunTy_maybe (unCType g) of
+#if __GLASGOW_HASKELL__ >= 900
+    Just (_multiplicity, arg, _) | isAlgType arg ->
+#else
     Just (arg, _) | isAlgType arg ->
+#endif
       fmap (fmap noLoc lambdaCase) <$>
         destructMatches use_field_puns f Nothing (CType arg) jdg
     _ -> cut -- throwError $ GoalMismatch "destructLambdaCase'" g
@@ -320,12 +323,24 @@
   occexts <- traverse newSubgoal $ fmap snd occjdgs
   ctx     <- ask
   ext     <- newSubgoal
-           $ introduce ctx (userHypothesis $ fmap (second jGoal) occjdgs)
-           $ jdg
+           $ introduce ctx (userHypothesis $ fmap (second jGoal) occjdgs) jdg
   pure $ fmap noLoc $
     let'
       <$> traverse
             (\(occ, ext) -> valBind (occNameToStr occ) <$> fmap unLoc ext)
             (zip (fmap fst occjdgs) occexts)
       <*> fmap unLoc ext
+
+
+------------------------------------------------------------------------------
+-- | Converts a function application into applicative form
+idiomize :: LHsExpr GhcPs -> LHsExpr GhcPs
+idiomize x = noLoc $ case unLoc x of
+  HsApp _ (L _ (HsVar _ (L _ x))) gshgp3 ->
+    op (bvar' $ occName x) "<$>" (unLoc gshgp3)
+  HsApp _ gsigp gshgp3 ->
+    op (unLoc $ idiomize gsigp) "<*>" (unLoc gshgp3)
+  RecordCon _ con flds ->
+    unLoc $ idiomize $ noLoc $ foldl' (@@) (HsVar noExtField con) $ fmap unLoc flds
+  y -> y
 
diff --git a/src/Wingman/Context.hs b/src/Wingman/Context.hs
--- a/src/Wingman/Context.hs
+++ b/src/Wingman/Context.hs
@@ -1,3 +1,5 @@
+{-# LANGUAGE CPP #-}
+
 module Wingman.Context where
 
 import           Control.Arrow
@@ -11,6 +13,10 @@
 import           Wingman.GHC (normalizeType)
 import           Wingman.Judgements.Theta
 import           Wingman.Types
+
+#if __GLASGOW_HASKELL__ >= 900
+import GHC.Tc.Utils.TcType
+#endif
 
 
 mkContext
diff --git a/src/Wingman/Debug.hs b/src/Wingman/Debug.hs
--- a/src/Wingman/Debug.hs
+++ b/src/Wingman/Debug.hs
@@ -17,6 +17,7 @@
 
 import           Control.DeepSeq
 import           Control.Exception
+import           Data.Either (fromRight)
 import qualified Debug.Trace
 import           Development.IDE.GHC.Compat (PlainGhcException, Outputable(..), SDoc, showSDocUnsafe)
 import           System.IO.Unsafe  (unsafePerformIO)
@@ -33,7 +34,7 @@
   -- We might not have unsafeGlobalDynFlags (like during testing), in which
   -- case GHC panics. Instead of crashing, let's just fail to print.
   !res <- try @PlainGhcException $ evaluate $ deepseq z z
-  pure $ either (const "<unsafeRender'>") id res
+  pure $ fromRight "<unsafeRender'>" res
 {-# NOINLINE unsafeRender' #-}
 
 traceMX :: (Monad m, Show a) => String -> a -> m ()
diff --git a/src/Wingman/EmptyCase.hs b/src/Wingman/EmptyCase.hs
--- a/src/Wingman/EmptyCase.hs
+++ b/src/Wingman/EmptyCase.hs
@@ -17,8 +17,7 @@
 import           Data.Monoid
 import qualified Data.Text as T
 import           Data.Traversable
-import           Development.IDE (hscEnv)
-import           Development.IDE (realSrcSpanToRange)
+import           Development.IDE (hscEnv, realSrcSpanToRange)
 import           Development.IDE.Core.RuleTypes
 import           Development.IDE.Core.Shake (IdeState (..))
 import           Development.IDE.Core.UseStale
@@ -51,13 +50,14 @@
   Continuation @EmptyCaseT @EmptyCaseT @WorkspaceEdit EmptyCaseT
     (SynthesizeCodeLens $ \LspEnv{..} _ -> do
       let FileContext{..} = le_fileContext
+      nfp <- getNfp fc_uri
 
-      let stale a = runStaleIde "codeLensProvider" le_ideState fc_nfp a
+      let stale a = runStaleIde "codeLensProvider" le_ideState nfp a
 
       ccs <- lift getClientCapabilities
       TrackedStale pm _ <- mapMaybeT liftIO $ stale GetAnnotatedParsedSource
       TrackedStale binds bind_map <- mapMaybeT liftIO $ stale GetBindings
-      holes <- mapMaybeT liftIO $ emptyCaseScrutinees le_ideState fc_nfp
+      holes <- mapMaybeT liftIO $ emptyCaseScrutinees le_ideState nfp
 
       for holes $ \(ss, ty) -> do
         binds_ss <- liftMaybe $ mapAgeFrom bind_map ss
@@ -81,14 +81,14 @@
           , edits
           )
     )
-  $ (\ _ _ _ we -> pure $ pure $ RawEdit we)
+    (\ _ _ _ we -> pure $ pure $ RawEdit we)
 
 
 scrutinzedType :: EmptyCaseSort Type -> Maybe Type
 scrutinzedType (EmptyCase ty) = pure  ty
 scrutinzedType (EmptyLamCase ty) =
   case tacticsSplitFunTy ty of
-    (_, _, tys, _) -> listToMaybe  tys
+    (_, _, tys, _) -> listToMaybe $ fmap scaledThing tys
 
 
 ------------------------------------------------------------------------------
@@ -115,9 +115,9 @@
     -> Graft (Either String) ParsedSource
 graftMatchGroup ss l =
   hoistGraft (runExcept . runExceptString) $ graftExprWithM ss $ \case
-    L span (HsCase ext scrut mg@_) -> do
+    L span (HsCase ext scrut mg) -> do
       pure $ Just $ L span $ HsCase ext scrut $ mg { mg_alts = l }
-    L span (HsLamCase ext mg@_) -> do
+    L span (HsLamCase ext mg) -> do
       pure $ Just $ L span $ HsLamCase ext $ mg { mg_alts = l }
     (_ :: LHsExpr GhcPs) -> pure Nothing
 
@@ -165,6 +165,6 @@
 emptyCaseQ :: GenericQ [(SrcSpan, EmptyCaseSort (HsExpr GhcTc))]
 emptyCaseQ = everything (<>) $ mkQ mempty $ \case
   L new_span (Case scrutinee []) -> pure (new_span, EmptyCase scrutinee)
-  L new_span (expr@(LamCase [])) -> pure (new_span, EmptyLamCase expr)
+  L new_span expr@(LamCase []) -> pure (new_span, EmptyLamCase expr)
   (_ :: LHsExpr GhcTc) -> mempty
 
diff --git a/src/Wingman/GHC.hs b/src/Wingman/GHC.hs
--- a/src/Wingman/GHC.hs
+++ b/src/Wingman/GHC.hs
@@ -6,6 +6,7 @@
 import           Control.Monad.State
 import           Control.Monad.Trans.Maybe (MaybeT(..))
 import           Data.Bool (bool)
+import           Data.Coerce (coerce)
 import           Data.Function (on)
 import           Data.Functor ((<&>))
 import           Data.List (isPrefixOf)
@@ -21,7 +22,11 @@
 import           Wingman.StaticPlugin (pattern MetaprogramSyntax)
 import           Wingman.Types
 
+#if __GLASGOW_HASKELL__ >= 900
+import GHC.Tc.Utils.TcType
+#endif
 
+
 tcTyVar_maybe :: Type -> Maybe Var
 tcTyVar_maybe ty | Just ty' <- tcView ty = tcTyVar_maybe ty'
 tcTyVar_maybe (CastTy ty _) = tcTyVar_maybe ty  -- look through casts, as
@@ -57,7 +62,7 @@
 ------------------------------------------------------------------------------
 -- | Split a function, also splitting out its quantified variables and theta
 -- context.
-tacticsSplitFunTy :: Type -> ([TyVar], ThetaType, [Type], Type)
+tacticsSplitFunTy :: Type -> ([TyVar], ThetaType, [Scaled Type], Type)
 tacticsSplitFunTy t
   = let (vars, theta, t') = tcSplitNestedSigmaTys t
         (args, res) = tcSplitFunTys t'
@@ -96,10 +101,7 @@
             pure (tv, setTyVarUnique tv uniq)
   pure $
     everywhere
-      (mkT $ \tv ->
-        case M.lookup tv reps of
-          Just tv' -> tv'
-          Nothing  -> tv
+      (mkT $ \tv -> M.findWithDefault tv tv reps
       ) $ snd $ tcSplitForAllTyVars t
 
 
@@ -182,7 +184,11 @@
 
 ------------------------------------------------------------------------------
 -- | Unpack the relevant parts of a 'Match'
+#if __GLASGOW_HASKELL__ >= 900
+pattern AMatch :: HsMatchContext (NoGhcTc GhcPs) -> [Pat GhcPs] -> HsExpr GhcPs -> Match GhcPs (LHsExpr GhcPs)
+#else
 pattern AMatch :: HsMatchContext (NameOrRdrName (IdP GhcPs)) -> [Pat GhcPs] -> HsExpr GhcPs -> Match GhcPs (LHsExpr GhcPs)
+#endif
 pattern AMatch ctx pats body <-
   Match { m_ctxt = ctx
         , m_pats = fmap fromPatCompat -> pats
@@ -193,9 +199,9 @@
 pattern SingleLet :: IdP GhcPs -> [Pat GhcPs] -> HsExpr GhcPs -> HsExpr GhcPs -> HsExpr GhcPs
 pattern SingleLet bind pats val expr <-
   HsLet _
-    (L _ (HsValBinds _
+    (HsValBinds _
       (ValBinds _ (bagToList ->
-        [(L _ (FunBind _ (L _ bind) (MG _ (L _ [L _ (AMatch _ pats val)]) _) _ _))]) _)))
+        [L _ (FunBind {fun_id = (L _ bind), fun_matches = (MG _ (L _ [L _ (AMatch _ pats val)]) _)})]) _))
     (L _ expr)
 
 
@@ -204,7 +210,7 @@
 pattern Lambda :: [Pat GhcPs] -> HsExpr GhcPs -> HsExpr GhcPs
 pattern Lambda pats body <-
   HsLam _
-    (MG {mg_alts = L _ [L _ (AMatch _ pats body) ]})
+    MG {mg_alts = L _ [L _ (AMatch _ pats body) ]}
   where
     -- If there are no patterns to bind, just stick in the body
     Lambda [] body   = body
@@ -232,7 +238,7 @@
 unpackMatches :: PatCompattable p => [Match p (LHsExpr p)] -> Maybe [(Pat p, LHsExpr p)]
 unpackMatches [] = Just []
 unpackMatches (SinglePatMatch pat body : matches) =
-  (:) <$> pure (pat, body) <*> unpackMatches matches
+  ((pat, body):) <$> unpackMatches matches
 unpackMatches _ = Nothing
 
 
@@ -241,14 +247,14 @@
 pattern Case :: PatCompattable p => HsExpr p -> [(Pat p, LHsExpr p)] -> HsExpr p
 pattern Case scrutinee matches <-
   HsCase _ (L _ scrutinee)
-    (MG {mg_alts = L _ (fmap unLoc -> unpackMatches -> Just matches)})
+    MG {mg_alts = L _ (fmap unLoc -> unpackMatches -> Just matches)}
 
 ------------------------------------------------------------------------------
 -- | Like 'Case', but for lambda cases.
 pattern LamCase :: PatCompattable p => [(Pat p, LHsExpr p)] -> HsExpr p
 pattern LamCase matches <-
   HsLamCase _
-    (MG {mg_alts = L _ (fmap unLoc -> unpackMatches -> Just matches)})
+    MG {mg_alts = L _ (fmap unLoc -> unpackMatches -> Just matches)}
 
 
 ------------------------------------------------------------------------------
@@ -258,7 +264,11 @@
 --         @Just False@ if it can't be homomorphic
 --         @Just True@ if it can
 lambdaCaseable :: Type -> Maybe Bool
+#if __GLASGOW_HASKELL__ >= 900
+lambdaCaseable (splitFunTy_maybe -> Just (_multiplicity, arg, res))
+#else
 lambdaCaseable (splitFunTy_maybe -> Just (arg, res))
+#endif
   | isJust (algebraicTyCon arg)
   = Just $ isJust $ algebraicTyCon res
 lambdaCaseable _ = Nothing
@@ -350,12 +360,17 @@
 -- | Like 'tcUnifyTy', but takes a list of skolems to prevent unification of.
 tryUnifyUnivarsButNotSkolems :: Set TyVar -> CType -> CType -> Maybe TCvSubst
 tryUnifyUnivarsButNotSkolems skolems goal inst =
-  case tcUnifyTysFG
-         (bool BindMe Skolem . flip S.member skolems)
-         [unCType inst]
-         [unCType goal] of
-    Unifiable subst -> pure subst
-    _               -> Nothing
+  tryUnifyUnivarsButNotSkolemsMany skolems $ coerce [(goal, inst)]
+
+------------------------------------------------------------------------------
+-- | Like 'tryUnifyUnivarsButNotSkolems', but takes a list
+-- of pairs of types to unify.
+tryUnifyUnivarsButNotSkolemsMany :: Set TyVar -> [(Type, Type)] -> Maybe TCvSubst
+tryUnifyUnivarsButNotSkolemsMany skolems (unzip -> (goal, inst)) =
+  tcUnifyTys
+    (bool BindMe Skolem . flip S.member skolems)
+    inst
+    goal
 
 
 updateSubst :: TCvSubst -> TacticState -> TacticState
diff --git a/src/Wingman/Judgements.hs b/src/Wingman/Judgements.hs
--- a/src/Wingman/Judgements.hs
+++ b/src/Wingman/Judgements.hs
@@ -66,7 +66,13 @@
 withNewGoal :: a -> Judgement' a -> Judgement' a
 withNewGoal t = field @"_jGoal" .~ t
 
+------------------------------------------------------------------------------
+-- | Like 'withNewGoal' but allows you to modify the goal rather than replacing
+-- it.
+withModifiedGoal :: (a -> a) -> Judgement' a -> Judgement' a
+withModifiedGoal f = field @"_jGoal" %~ f
 
+
 ------------------------------------------------------------------------------
 -- | Add some new type equalities to the local judgement.
 withNewCoercions :: [(CType, CType)] -> Judgement -> Judgement
@@ -140,7 +146,7 @@
                    -- otherwise nothing
 hasPositionalAncestry ancestors jdg name
   | not $ null ancestors
-  = case any (== name) ancestors of
+  = case name `elem` ancestors of
       True  -> Just True
       False ->
         case M.lookup name $ jAncestryMap jdg of
@@ -162,8 +168,7 @@
     disallowing reason (M.keysSet $ M.filterWithKey go $ hyByName $ jHypothesis jdg) jdg
   where
     go name _
-      = not
-      . isJust
+      = isNothing
       $ hasPositionalAncestry ancestry jdg name
 
 
@@ -233,14 +238,12 @@
 -- | Return the ancestry of a 'PatVal', or 'mempty' otherwise.
 getAncestry :: Judgement' a -> OccName -> Set OccName
 getAncestry jdg name =
-  case M.lookup name $ jPatHypothesis jdg of
-    Just pv -> pv_ancestry pv
-    Nothing -> mempty
+  maybe mempty pv_ancestry . M.lookup name $ jPatHypothesis jdg
 
 
 jAncestryMap :: Judgement' a -> Map OccName (Set OccName)
 jAncestryMap jdg =
-  flip M.map (jPatHypothesis jdg) pv_ancestry
+  M.map pv_ancestry (jPatHypothesis jdg)
 
 
 provAncestryOf :: Provenance -> Set OccName
@@ -365,9 +368,7 @@
 -- | Are there any top-level function argument bindings in this judgement?
 jHasBoundArgs :: Judgement' a -> Bool
 jHasBoundArgs
-  = not
-  . null
-  . filter (isTopLevel . hi_provenance)
+  = any (isTopLevel . hi_provenance)
   . unHypothesis
   . jLocalHypothesis
 
diff --git a/src/Wingman/Judgements/SYB.hs b/src/Wingman/Judgements/SYB.hs
--- a/src/Wingman/Judgements/SYB.hs
+++ b/src/Wingman/Judgements/SYB.hs
@@ -87,12 +87,12 @@
 
 metaprogramAtQ :: SrcSpan -> GenericQ [(SrcSpan, T.Text)]
 metaprogramAtQ ss = everythingContaining ss $ mkQ mempty $ \case
-  L new_span (WingmanMetaprogram program) -> pure (new_span, T.pack $ unpackFS $ program)
+  L new_span (WingmanMetaprogram program) -> pure (new_span, T.pack $ unpackFS program)
   (_ :: LHsExpr GhcTc) -> mempty
 
 
 metaprogramQ :: GenericQ [(SrcSpan, T.Text)]
 metaprogramQ = everything (<>) $ mkQ mempty $ \case
-  L new_span (WingmanMetaprogram program) -> pure (new_span, T.pack $ unpackFS $ program)
+  L new_span (WingmanMetaprogram program) -> pure (new_span, T.pack $ unpackFS program)
   (_ :: LHsExpr GhcTc) -> mempty
 
diff --git a/src/Wingman/Judgements/Theta.hs b/src/Wingman/Judgements/Theta.hs
--- a/src/Wingman/Judgements/Theta.hs
+++ b/src/Wingman/Judgements/Theta.hs
@@ -26,7 +26,11 @@
 import           Wingman.GHC
 import           Wingman.Types
 
+#if __GLASGOW_HASKELL__ >= 900
+import GHC.Tc.Utils.TcType
+#endif
 
+
 ------------------------------------------------------------------------------
 -- | Something we've learned about the type environment.
 data Evidence
@@ -172,16 +176,32 @@
 ------------------------------------------------------------------------------
 -- | Extract evidence from 'AbsBinds' in scope.
 absBinds ::  SrcSpan -> LHsBindLR GhcTc GhcTc -> [PredType]
+#if __GLASGOW_HASKELL__ >= 900
+absBinds dst (L src (FunBind w _ _ _))
+  | dst `isSubspanOf` src
+  = wrapper w
+absBinds dst (L src (AbsBinds _ _ h _ _ z _))
+#else
 absBinds dst (L src (AbsBinds _ _ h _ _ _ _))
-  | dst `isSubspanOf` src = fmap idType h
+#endif
+  | dst `isSubspanOf` src
+  = fmap idType h
+#if __GLASGOW_HASKELL__ >= 900
+    <> foldMap (absBinds dst) z
+#endif
 absBinds _ _ = []
 
 
 ------------------------------------------------------------------------------
 -- | Extract evidence from 'HsWrapper's in scope
 wrapperBinds ::  SrcSpan -> LHsExpr GhcTc -> [PredType]
+#if __GLASGOW_HASKELL__ >= 900
+wrapperBinds dst (L src (XExpr (WrapExpr (HsWrap h _))))
+#else
 wrapperBinds dst (L src (HsWrap _ h _))
-  | dst `isSubspanOf` src = wrapper h
+#endif
+  | dst `isSubspanOf` src
+  = wrapper h
 wrapperBinds _ _ = []
 
 
@@ -189,14 +209,19 @@
 -- | Extract evidence from the 'ConPatOut's bound in this 'Match'.
 matchBinds :: SrcSpan -> LMatch GhcTc (LHsExpr GhcTc) -> [PredType]
 matchBinds dst (L src (Match _ _ pats _))
-  | dst `isSubspanOf` src = everything (<>) (mkQ mempty patBinds) pats
+  | dst `isSubspanOf` src
+  = everything (<>) (mkQ mempty patBinds) pats
 matchBinds _ _ = []
 
 
 ------------------------------------------------------------------------------
 -- | Extract evidence from a 'ConPatOut'.
 patBinds ::  Pat GhcTc -> [PredType]
+#if __GLASGOW_HASKELL__ >= 900
+patBinds (ConPat{ pat_con_ext = ConPatTc { cpt_dicts = dicts }})
+#else
 patBinds (ConPatOut { pat_dicts = dicts })
+#endif
   = fmap idType dicts
 patBinds _ = []
 
diff --git a/src/Wingman/LanguageServer.hs b/src/Wingman/LanguageServer.hs
--- a/src/Wingman/LanguageServer.hs
+++ b/src/Wingman/LanguageServer.hs
@@ -1,7 +1,6 @@
 {-# LANGUAGE CPP               #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE RankNTypes        #-}
-{-# LANGUAGE TupleSections     #-}
 {-# LANGUAGE TypeFamilies      #-}
 
 {-# LANGUAGE NoMonoLocalBinds  #-}
@@ -230,7 +229,7 @@
 
       -- KnownThings is just the instances in scope. There are no ranges
       -- involved, so it's not crucial to track ages.
-      let henv = untrackedStaleValue $ hscenv
+      let henv = untrackedStaleValue hscenv
       eps <- liftIO $ readIORef $ hsc_EPS $ hscEnv henv
 
       (jdg, ctx) <- liftMaybe $ mkJudgementAndContext cfg g binds new_rss tcg (hscEnv henv) eps
@@ -279,7 +278,7 @@
       evidence = getEvidenceAtHole (fmap (`RealSrcSpan` Nothing) tcg_rss) tcs
       cls_hy = foldMap evidenceToHypothesis evidence
       subst = ts_unifier $ evidenceToSubst evidence defaultTacticState
-  pure $
+  pure
     ( disallowing AlreadyDestructed already_destructed
     $ fmap (CType . substTyAddInScope subst . unCType) $
         mkFirstJudgement
@@ -309,8 +308,8 @@
 
 getSpanAndTypeAtHole
     :: Tracked age Range
-    -> Tracked age (HieASTs b)
-    -> Maybe (Tracked age RealSrcSpan, b)
+    -> Tracked age (HieASTs Type)
+    -> Maybe (Tracked age RealSrcSpan, Type)
 getSpanAndTypeAtHole r@(unTrack -> range) (unTrack -> hf) = do
   join $ listToMaybe $ M.elems $ flip M.mapWithKey (getAsts hf) $ \fs ast ->
     case selectSmallestContaining (rangeToRealSrcSpan (FastString.unpackFS fs) range) ast of
@@ -403,7 +402,11 @@
         (RealDataCon $ tupleDataCon boxity $ length pats)
         tys
           $ zip [0.. ] pats
-    ConPatOut (L _ con) args _ _ _ f _ ->
+#if __GLASGOW_HASKELL__ >= 900
+    ConPat {pat_con = (L _ con), pat_con_ext = ConPatTc {cpt_arg_tys = args}, pat_args = f} ->
+#else
+    ConPatOut {pat_con = (L _ con), pat_arg_tys = args, pat_args = f} ->
+#endif
       case f of
         PrefixCon l_pgt ->
           mkDerivedConHypothesis prov con args $ zip [0..] l_pgt
@@ -564,7 +567,11 @@
                       L span (HsVar _ (L _ name))
                         | isHole (occName name) ->
                             maybeToList $ srcSpanToRange span
+#if __GLASGOW_HASKELL__ >= 900
+                      L span (HsUnboundVar _ occ)
+#else
                       L span (HsUnboundVar _ (TrueExprHole occ))
+#endif
                         | isHole occ ->
                             maybeToList $ srcSpanToRange span
 #if __GLASGOW_HASKELL__ <= 808
diff --git a/src/Wingman/LanguageServer/Metaprogram.hs b/src/Wingman/LanguageServer/Metaprogram.hs
--- a/src/Wingman/LanguageServer/Metaprogram.hs
+++ b/src/Wingman/LanguageServer/Metaprogram.hs
@@ -15,8 +15,7 @@
 import           Data.List (find)
 import           Data.Maybe
 import qualified Data.Text as T
-import           Development.IDE (positionToRealSrcLoc)
-import           Development.IDE (realSrcSpanToRange)
+import           Development.IDE (positionToRealSrcLoc, realSrcSpanToRange)
 import           Development.IDE.Core.Shake (IdeState (..))
 import           Development.IDE.Core.UseStale
 import           Development.IDE.GHC.Compat hiding (empty)
diff --git a/src/Wingman/LanguageServer/TacticProviders.hs b/src/Wingman/LanguageServer/TacticProviders.hs
--- a/src/Wingman/LanguageServer/TacticProviders.hs
+++ b/src/Wingman/LanguageServer/TacticProviders.hs
@@ -1,6 +1,5 @@
 {-# LANGUAGE CPP               #-}
 {-# LANGUAGE OverloadedStrings #-}
-{-# LANGUAGE RecordWildCards   #-}
 {-# OPTIONS_GHC -Wno-orphans #-}
 
 module Wingman.LanguageServer.TacticProviders
@@ -139,8 +138,7 @@
   withConfig $ \cfg ->
     filterTypeProjection
         ( guardLength (<= cfg_max_use_ctor_actions cfg)
-        . fromMaybe []
-        . fmap fst
+        . maybe [] fst
         . tacticsGetDataCons
         ) $ \dcon ->
       provide UseDataCon
@@ -162,10 +160,11 @@
 
 
 requireGHC88OrHigher :: TacticProvider -> TacticProvider
-requireGHC88OrHigher tp tpd =
 #if __GLASGOW_HASKELL__ >= 808
+requireGHC88OrHigher tp tpd =
   tp tpd
 #else
+requireGHC88OrHigher _ _=
   mempty
 #endif
 
@@ -272,7 +271,7 @@
 -- given by 'provide' are always available.
 provide :: TacticCommand -> T.Text -> TacticProvider
 provide tc name _ =
-  pure $ (Metadata (tacticTitle tc name) (mkTacticKind tc) (tacticPreferred tc), name)
+  pure (Metadata (tacticTitle tc name) (mkTacticKind tc) (tacticPreferred tc), name)
 
 
 ------------------------------------------------------------------------------
@@ -296,7 +295,7 @@
 liftLambdaCase :: r -> (Type -> Type -> r) -> Type -> r
 liftLambdaCase nil f t =
   case tacticsSplitFunTy t of
-    (_, _, arg : _, res) -> f res arg
+    (_, _, arg : _, res) -> f res $ scaledThing arg
     _ -> nil
 
 
@@ -314,7 +313,7 @@
 -- usual algebraic types, and when any of their data constructors are records.
 destructPunFilter :: Type -> Type -> Bool
 destructPunFilter _ (algebraicTyCon -> Just tc) =
-  any (not . null . dataConFieldLabels) $ tyConDataCons tc
+  not . all (null . dataConFieldLabels) $ tyConDataCons tc
 destructPunFilter _ _ = False
 
 
diff --git a/src/Wingman/Machinery.hs b/src/Wingman/Machinery.hs
--- a/src/Wingman/Machinery.hs
+++ b/src/Wingman/Machinery.hs
@@ -1,6 +1,6 @@
-{-# LANGUAGE RecordWildCards #-}
-{-# LANGUAGE TupleSections   #-}
-{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE CPP           #-}
+{-# LANGUAGE RankNTypes    #-}
+{-# LANGUAGE TupleSections #-}
 
 module Wingman.Machinery where
 
@@ -18,7 +18,7 @@
 import           Data.Generics.Product (field')
 import           Data.List (sortBy)
 import qualified Data.Map as M
-import           Data.Maybe (mapMaybe, isJust)
+import           Data.Maybe (mapMaybe, isNothing)
 import           Data.Monoid (getSum)
 import           Data.Ord (Down (..), comparing)
 import qualified Data.Set as S
@@ -31,12 +31,20 @@
 import           Refinery.Tactic.Internal
 import           System.Timeout (timeout)
 import           Wingman.Context (getInstance)
-import           Wingman.GHC (tryUnifyUnivarsButNotSkolems, updateSubst, tacticsGetDataCons, freshTyvars)
+import           Wingman.GHC (tryUnifyUnivarsButNotSkolems, updateSubst, tacticsGetDataCons, freshTyvars, tryUnifyUnivarsButNotSkolemsMany)
 import           Wingman.Judgements
 import           Wingman.Simplify (simplify)
 import           Wingman.Types
 
+#if __GLASGOW_HASKELL__ < 900
+import FunDeps (fd_eqs, improveFromInstEnv)
+import Pair (unPair)
+#else
+import GHC.Tc.Instance.FunDeps (fd_eqs, improveFromInstEnv)
+import GHC.Data.Pair (unPair)
+#endif
 
+
 substCTy :: TCvSubst -> CType -> CType
 substCTy subst = coerce . substTy subst . coerce
 
@@ -69,14 +77,14 @@
 
 
 tacticToRule :: Judgement -> TacticsM () -> Rule
-tacticToRule jdg (TacticT tt) = RuleT $ flip execStateT jdg tt >>= flip Subgoal Axiom
+tacticToRule jdg (TacticT tt) = RuleT $ execStateT tt jdg >>= flip Subgoal Axiom
 
 
 consumeChan :: OutChan (Maybe a) -> IO [a]
 consumeChan chan = do
   tryReadChan chan >>= tryRead >>= \case
     Nothing -> pure []
-    Just (Just a) -> (:) <$> pure a <*> consumeChan chan
+    Just (Just a) -> (a:) <$> consumeChan chan
     Just Nothing -> pure []
 
 
@@ -107,7 +115,7 @@
     (in_proofs, out_proofs) <- newChan
     (in_errs, out_errs) <- newChan
     timed_out <-
-      fmap (not. isJust) $ timeout duration $ consume stream $ \case
+      fmap isNothing $ timeout duration $ consume stream $ \case
         Left err -> writeChan in_errs $ Just err
         Right proof -> writeChan in_proofs $ Just proof
     writeChan in_proofs Nothing
@@ -246,6 +254,23 @@
       modify $ updateSubst subst
     Nothing -> cut
 
+------------------------------------------------------------------------------
+-- | Get a substition out of a theta's fundeps
+learnFromFundeps
+    :: ThetaType
+    -> RuleM ()
+learnFromFundeps theta = do
+  inst_envs <- asks ctxInstEnvs
+  skolems <- gets ts_skolems
+  subst <- gets ts_unifier
+  let theta' = substTheta subst theta
+      fundeps = foldMap (foldMap fd_eqs . improveFromInstEnv inst_envs (\_ _ -> ())) theta'
+  case tryUnifyUnivarsButNotSkolemsMany skolems $ fmap unPair fundeps of
+    Just subst ->
+      modify $ updateSubst subst
+    Nothing -> cut
+
+
 cut :: RuleT jdg ext err s m a
 cut = RuleT Empty
 
@@ -342,7 +367,7 @@
 getDefiningType
     :: TacticsM CType
 getDefiningType = do
-  calling_fun_name <- fst . head <$> asks ctxDefiningFuncs
+  calling_fun_name <- asks (fst . head . ctxDefiningFuncs)
   maybe
     (failure $ NotInScope calling_fun_name)
     pure
diff --git a/src/Wingman/Metaprogramming/Lexer.hs b/src/Wingman/Metaprogramming/Lexer.hs
--- a/src/Wingman/Metaprogramming/Lexer.hs
+++ b/src/Wingman/Metaprogramming/Lexer.hs
@@ -1,7 +1,5 @@
 {-# LANGUAGE DataKinds         #-}
-{-# LANGUAGE LambdaCase        #-}
 {-# LANGUAGE OverloadedStrings #-}
-{-# LANGUAGE TypeApplications  #-}
 
 module Wingman.Metaprogramming.Lexer where
 
diff --git a/src/Wingman/Metaprogramming/Parser.hs b/src/Wingman/Metaprogramming/Parser.hs
--- a/src/Wingman/Metaprogramming/Parser.hs
+++ b/src/Wingman/Metaprogramming/Parser.hs
@@ -1,12 +1,12 @@
 {-# 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.Either (fromRight)
 import           Data.Functor
 import           Data.Maybe (listToMaybe)
 import qualified Data.Text as T
@@ -98,6 +98,17 @@
           "\\x y z -> (_ :: d)"
       ]
 
+  , command "idiom" Deterministic Tactic
+      "Lift a tactic into idiom brackets."
+      (pure . idiom)
+      [ Example
+          Nothing
+          ["(apply f)"]
+          [EHI "f" "a -> b -> Int"]
+          (Just "Maybe Int")
+          "f <$> (_ :: Maybe a) <*> (_ :: Maybe b)"
+      ]
+
   , command "intro" Deterministic (Bind One)
       "Construct a lambda expression, binding an argument with the given name."
       (pure . intros' . IntroduceOnlyNamed . pure)
@@ -415,7 +426,7 @@
 
 
 tactic :: Parser (TacticsM ())
-tactic = flip P.makeExprParser operators oneTactic
+tactic = P.makeExprParser oneTactic operators
 
 operators :: [[P.Operator Parser (TacticsM ())]]
 operators =
@@ -473,7 +484,7 @@
 
 parseMetaprogram :: T.Text -> TacticsM ()
 parseMetaprogram
-    = either (const $ pure ()) id
+    = fromRight (pure ())
     . P.runParser tacticProgram "<splice>"
 
 
diff --git a/src/Wingman/Metaprogramming/Parser/Documentation.hs b/src/Wingman/Metaprogramming/Parser/Documentation.hs
--- a/src/Wingman/Metaprogramming/Parser/Documentation.hs
+++ b/src/Wingman/Metaprogramming/Parser/Documentation.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE OverloadedStrings #-}
+{-# OPTIONS_GHC -Wno-deprecations #-}
 
 module Wingman.Metaprogramming.Parser.Documentation where
 
diff --git a/src/Wingman/Metaprogramming/ProofState.hs b/src/Wingman/Metaprogramming/ProofState.hs
--- a/src/Wingman/Metaprogramming/ProofState.hs
+++ b/src/Wingman/Metaprogramming/ProofState.hs
@@ -1,5 +1,7 @@
+{-# LANGUAGE CPP               #-}
 {-# LANGUAGE NamedFieldPuns    #-}
 {-# LANGUAGE OverloadedStrings #-}
+{-# OPTIONS_GHC -Wno-deprecations #-}
 
 module Wingman.Metaprogramming.ProofState where
 
diff --git a/src/Wingman/Naming.hs b/src/Wingman/Naming.hs
--- a/src/Wingman/Naming.hs
+++ b/src/Wingman/Naming.hs
@@ -1,3 +1,5 @@
+{-# LANGUAGE CPP #-}
+
 module Wingman.Naming where
 
 import           Control.Arrow
@@ -18,7 +20,11 @@
 import           Text.Hyphenation (hyphenate, english_US)
 import           Wingman.GHC (tcTyVar_maybe)
 
+#if __GLASGOW_HASKELL__ >= 900
+import GHC.Tc.Utils.TcType
+#endif
 
+
 ------------------------------------------------------------------------------
 -- | A classification of a variable, for which we have specific naming rules.
 -- A variable can have multiple purposes simultaneously.
@@ -38,11 +44,11 @@
 
 pattern IsPredicate :: Type
 pattern IsPredicate <-
-  (tcSplitFunTys -> ([isFunTy -> False], isBoolTy -> True))
+  (tcSplitFunTys -> ([isFunTy . scaledThing -> False], isBoolTy -> True))
 
 pattern IsFunction :: [Type] -> Type -> Type
 pattern IsFunction args res <-
-  (tcSplitFunTys -> (args@(_:_), res))
+  (first (map scaledThing) . tcSplitFunTys -> (args@(_:_), res))
 
 pattern IsString :: Type
 pattern IsString <-
@@ -156,8 +162,7 @@
       = foldMap (fmap toLower . take 1) camels
   | otherwise
       = getStem
-      $ fmap toLower
-      $ name
+      $ fmap toLower name
   where
     occ = getOccName tc
     name = occNameString occ
diff --git a/src/Wingman/Plugin.hs b/src/Wingman/Plugin.hs
--- a/src/Wingman/Plugin.hs
+++ b/src/Wingman/Plugin.hs
@@ -1,6 +1,3 @@
-{-# LANGUAGE OverloadedStrings #-}
-{-# LANGUAGE RecordWildCards #-}
-
 -- | A plugin that uses tactics to synthesize code
 module Wingman.Plugin where
 
diff --git a/src/Wingman/Range.hs b/src/Wingman/Range.hs
--- a/src/Wingman/Range.hs
+++ b/src/Wingman/Range.hs
@@ -19,6 +19,5 @@
 rangeToRealSrcSpan :: String -> Range -> RealSrcSpan
 rangeToRealSrcSpan file (Range (Position startLn startCh) (Position endLn endCh)) =
   mkRealSrcSpan
-    (mkRealSrcLoc (FS.fsLit file) (startLn + 1) (startCh + 1))
-    (mkRealSrcLoc (FS.fsLit file) (endLn + 1) (endCh + 1))
-
+    (mkRealSrcLoc (FS.fsLit file) (fromIntegral $ startLn + 1) (fromIntegral $ startCh + 1))
+    (mkRealSrcLoc (FS.fsLit file) (fromIntegral $ endLn + 1) (fromIntegral $ endCh + 1))
diff --git a/src/Wingman/Simplify.hs b/src/Wingman/Simplify.hs
--- a/src/Wingman/Simplify.hs
+++ b/src/Wingman/Simplify.hs
@@ -19,11 +19,12 @@
 pattern Lambda :: [Pat GhcPs] -> HsExpr GhcPs -> HsExpr GhcPs
 pattern Lambda pats body <-
   HsLam _
-    (MG {mg_alts = L _ [L _
-      (Match { m_pats = fmap fromPatCompat -> pats
-             , m_grhss = GRHSs {grhssGRHSs = [L _ (
+    MG {mg_alts = L _ [L _
+      Match { m_pats = fmap fromPatCompat -> pats
+            , m_grhss = GRHSs {grhssGRHSs = [L _ (
                  GRHS _ [] (L _ body))]}
-             })]})
+            }]
+        }
   where
     -- If there are no patterns to bind, just stick in the body
     Lambda [] body   = body
@@ -35,9 +36,8 @@
 -- | Simlify an expression.
 simplify :: LHsExpr GhcPs -> LHsExpr GhcPs
 simplify
-  = head
-  . drop 3   -- Do three passes; this should be good enough for the limited
-             -- amount of gas we give to auto
+  = (!!3) -- Do three passes; this should be good enough for the limited
+          -- amount of gas we give to auto
   . iterate (everywhere $ foldEndo
     [ simplifyEtaReduce
     , simplifyRemoveParens
@@ -62,7 +62,7 @@
       (HsVar _ (L _ a)) | pat == a ->
     var "id"
   Lambda
-      (unsnoc -> Just (pats, (VarPat _ (L _ pat))))
+      (unsnoc -> Just (pats, VarPat _ (L _ pat)))
       (HsApp _ (L _ f) (L _ (HsVar _ (L _ a))))
       | pat == a
         -- We can only perform this simplifiation if @pat@ is otherwise unused.
@@ -84,8 +84,8 @@
 simplifyCompose :: GenericT
 simplifyCompose = mkT $ \case
   Lambda
-      (unsnoc -> Just (pats, (VarPat _ (L _ pat))))
-      (unroll -> (fs@(_:_), (HsVar _ (L _ a))))
+      (unsnoc -> Just (pats, VarPat _ (L _ pat)))
+      (unroll -> (fs@(_:_), HsVar _ (L _ a)))
       | pat == a
         -- We can only perform this simplifiation if @pat@ is otherwise unused.
       , not (containsHsVar pat fs) ->
diff --git a/src/Wingman/StaticPlugin.hs b/src/Wingman/StaticPlugin.hs
--- a/src/Wingman/StaticPlugin.hs
+++ b/src/Wingman/StaticPlugin.hs
@@ -3,17 +3,26 @@
 module Wingman.StaticPlugin
   ( staticPlugin
   , metaprogramHoleName
+  , enableQuasiQuotes
   , pattern WingmanMetaprogram
   , pattern MetaprogramSyntax
   ) where
 
-import Data.Data
 import Development.IDE.GHC.Compat
 import Development.IDE.GHC.Compat.Util
 import GHC.LanguageExtensions.Type (Extension(EmptyCase, QuasiQuotes))
-import Generics.SYB
+
 import Ide.Types
+
+#if __GLASGOW_HASKELL__ >= 808
+import Data.Data
+import Generics.SYB
+#if __GLASGOW_HASKELL__ >= 900
+import GHC.Driver.Plugins (purePlugin)
+#else
 import Plugins (purePlugin)
+#endif
+#endif
 
 staticPlugin :: DynFlagsModifications
 staticPlugin = mempty
@@ -39,7 +48,6 @@
 pattern MetaprogramSourceText = SourceText "wingman-meta-program"
 
 
-
 pattern WingmanMetaprogram :: FastString -> HsExpr p
 pattern WingmanMetaprogram mp <-
 #if __GLASGOW_HASKELL__ >= 900
@@ -51,7 +59,6 @@
 #endif
 
 
-
 enableQuasiQuotes :: DynFlags -> DynFlags
 enableQuasiQuotes = flip xopt_set QuasiQuotes
 
@@ -75,12 +82,7 @@
         }
     worker :: Monad m => [CommandLineOption] -> ModSummary -> HsParsedModule -> m 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 =
 #if __GLASGOW_HASKELL__ >= 900
@@ -91,9 +93,7 @@
     $ L ss
     $ HsVar noExtField
     $ L ss
-    $ mkRdrUnqual
-    $ metaprogramHoleName
-
+    $ mkRdrUnqual metaprogramHoleName
 
 addMetaprogrammingSyntax :: Data a => a -> a
 addMetaprogrammingSyntax =
@@ -101,7 +101,10 @@
     L ss (MetaprogramSyntax mp) ->
       L ss $ mkMetaprogram ss mp
     (x :: LHsExpr GhcPs) -> x
+#endif
 
+metaprogramHoleName :: OccName
+metaprogramHoleName = mkVarOcc "_$metaprogram"
 
 pattern MetaprogramSyntax :: FastString -> HsExpr GhcPs
 pattern MetaprogramSyntax mp <-
@@ -115,4 +118,3 @@
           (mkRdrUnqual $ mkVarOcc "wingman")
           noSrcSpan
           mp
-
diff --git a/src/Wingman/Tactics.hs b/src/Wingman/Tactics.hs
--- a/src/Wingman/Tactics.hs
+++ b/src/Wingman/Tactics.hs
@@ -8,11 +8,11 @@
 
 import           Control.Applicative (Alternative(empty), (<|>))
 import           Control.Lens ((&), (%~), (<>~))
-import           Control.Monad (filterM)
-import           Control.Monad (unless)
+import           Control.Monad (filterM, unless)
+import           Control.Monad (when)
 import           Control.Monad.Extra (anyM)
 import           Control.Monad.Reader.Class (MonadReader (ask))
-import           Control.Monad.State.Strict (StateT(..), runStateT)
+import           Control.Monad.State.Strict (StateT(..), runStateT, execStateT)
 import           Data.Bool (bool)
 import           Data.Foldable
 import           Data.Functor ((<&>))
@@ -24,7 +24,6 @@
 import           Data.Set (Set)
 import qualified Data.Set as S
 import           Data.Traversable (for)
-import           DataCon
 import           Development.IDE.GHC.Compat hiding (empty)
 import           GHC.Exts
 import           GHC.SourceGen ((@@))
@@ -95,7 +94,7 @@
         -- Make sure that the recursive call contains at least one already-bound
         -- pattern value. This ensures it is structurally smaller, and thus
         -- suggests termination.
-        case (any (flip M.member pat_vals) $ syn_used_vals ext) of
+        case any (flip M.member pat_vals) $ syn_used_vals ext of
           True -> Nothing
           False -> Just UnhelpfulRecursion
 
@@ -132,7 +131,8 @@
   let g  = jGoal jdg
   case tacticsSplitFunTy $ unCType g of
     (_, _, [], _) -> cut -- failure $ GoalMismatch "intros" g
-    (_, _, args, res) -> do
+    (_, _, scaledArgs, res) -> do
+      let args = fmap scaledThing scaledArgs
       ctx <- ask
       let gen_names = mkManyGoodNames (hyNamesInScope $ jEntireHypothesis jdg) args
           occs = case params of
@@ -145,7 +145,7 @@
           bound_occs = fmap fst bindings
           hy' = lambdaHypothesis top_hole bindings
           jdg' = introduce ctx hy'
-               $ withNewGoal (CType $ mkVisFunTys (drop num_occs args) res) jdg
+               $ withNewGoal (CType $ mkVisFunTys (drop num_occs scaledArgs) res) jdg
       ext <- newSubgoal jdg'
       pure $
         ext
@@ -233,7 +233,7 @@
 
   -- Ensure that every data constructor in the domain type is covered in the
   -- codomain; otherwise 'homo' will produce an ill-typed program.
-  case (uncoveredDataCons (coerce $ hi_type hi) (coerce g)) of
+  case uncoveredDataCons (coerce $ hi_type hi) (coerce g) of
     Just uncovered_dcs ->
       unless (S.null uncovered_dcs) $
         failure  $ TacticPanic "Can't cover every datacon in domain"
@@ -243,7 +243,7 @@
     $ destruct'
         False
         (\dc jdg -> buildDataCon False jdg dc $ snd $ splitAppTys $ unCType $ jGoal jdg)
-    $ hi
+        hi
 
 
 ------------------------------------------------------------------------------
@@ -266,7 +266,7 @@
         $ jGoal jdg
 
 
-data Saturation = Unsaturated Int
+newtype Saturation = Unsaturated Int
   deriving (Eq, Ord, Show)
 
 pattern Saturated :: Saturation
@@ -280,17 +280,19 @@
       ty = unCType $ hi_type hi
       func = hi_name hi
   ty' <- freshTyvars ty
-  let (_, _, all_args, ret) = tacticsSplitFunTy ty'
+  let (_, theta, all_args, ret) = tacticsSplitFunTy ty'
       saturated_args = dropEnd n all_args
       unsaturated_args = takeEnd n all_args
   rule $ \jdg -> do
     unify g (CType $ mkVisFunTys unsaturated_args ret)
+    learnFromFundeps theta
     ext
         <- fmap unzipTrace
         $ traverse ( newSubgoal
                     . blacklistingDestruct
                     . flip withNewGoal jdg
                     . CType
+                    . scaledThing
                     ) saturated_args
     pure $
       ext
@@ -443,7 +445,7 @@
 
 
 attemptOn :: (Judgement -> [a]) -> (a -> TacticsM ()) -> TacticsM ()
-attemptOn getNames tac = matching (choice . fmap (\s -> tac s) . getNames)
+attemptOn getNames tac = matching (choice . fmap tac . getNames)
 
 
 localTactic :: TacticsM a -> (Judgement -> Judgement) -> TacticsM a
@@ -501,7 +503,7 @@
 applyByName :: OccName -> TacticsM ()
 applyByName name = do
   g <- goal
-  choice $ (unHypothesis (jHypothesis g)) <&> \hi ->
+  choice $ unHypothesis (jHypothesis g) <&> \hi ->
     case hi_name hi == name of
       True  -> apply Saturated hi
       False -> empty
@@ -524,6 +526,7 @@
                     . blacklistingDestruct
                     . flip withNewGoal jdg
                     . CType
+                    . scaledThing
                     ) args
     app <- newSubgoal . blacklistingDestruct $ withNewGoal (CType ty) jdg
     pure $
@@ -540,7 +543,7 @@
 nary n = do
   a <- newUnivar
   b <- newUnivar
-  applyByType $ mkVisFunTys (replicate n a) b
+  applyByType $ mkVisFunTys (replicate n $ unrestricted a) b
 
 
 self :: TacticsM ()
@@ -558,7 +561,7 @@
 cata hi = do
   (_, _, calling_args, _)
       <- tacticsSplitFunTy . unCType <$> getDefiningType
-  freshened_args <- traverse freshTyvars calling_args
+  freshened_args <- traverse (freshTyvars . scaledThing) calling_args
   diff <- hyDiff $ destruct hi
 
   -- For for every destructed term, check to see if it can unify with any of
@@ -582,8 +585,7 @@
            $ \occ
           -> fmap (occ, )
            $ fmap (<$ jdg)
-           $ fmap CType
-           $ newUnivar
+           $ fmap CType newUnivar
   rule $ nonrecLet occ_tys
 
 
@@ -625,7 +627,7 @@
   let g = jGoal jdg
   fresh_ty <- newUnivar
   a <- newSubgoal $ withNewGoal (CType fresh_ty) jdg
-  f <- newSubgoal $ withNewGoal (coerce mkVisFunTys [fresh_ty] g) jdg
+  f <- newSubgoal $ withNewGoal (coerce mkVisFunTys [unrestricted fresh_ty] g) jdg
   pure $ fmap noLoc $ (@@) <$> fmap unLoc f <*> fmap unLoc a
 
 
@@ -639,4 +641,52 @@
   m
   g' <- unHypothesis . jEntireHypothesis <$> goal
   pure $ Hypothesis $ take (length g' - g_len) g'
+
+
+------------------------------------------------------------------------------
+-- | Attempt to run the given tactic in "idiom bracket" mode. For example, if
+-- the current goal is
+--
+--    (_ :: [r])
+--
+-- then @idiom apply@ will remove the applicative context, resulting in a hole:
+--
+--    (_ :: r)
+--
+-- and then use @apply@ to solve it. Let's say this results in:
+--
+--    (f (_ :: a) (_ :: b))
+--
+-- Finally, @idiom@ lifts this back into the original applicative:
+--
+--    (f <$> (_ :: [a]) <*> (_ :: [b]))
+--
+-- Idiom will fail fast if the current goal doesn't have an applicative
+-- instance.
+idiom :: TacticsM () -> TacticsM ()
+idiom m = do
+  jdg <- goal
+  let hole = unCType $ jGoal jdg
+  when (isFunction hole) $
+    failure $ GoalMismatch "idiom" $ jGoal jdg
+  case splitAppTy_maybe hole of
+    Just (applic, ty) -> do
+      minst <- getKnownInstance (mkClsOcc "Applicative")
+            . pure
+            $ applic
+      case minst of
+        Nothing -> failure $ GoalMismatch "idiom" $ CType applic
+        Just (_, _) -> do
+          rule $ \jdg -> do
+            expr <- subgoalWith (withNewGoal (CType ty) jdg) m
+            case unLoc $ syn_val expr of
+              HsApp{}     -> pure $ fmap idiomize expr
+              RecordCon{} -> pure $ fmap idiomize expr
+              _       -> unsolvable $ GoalMismatch "idiom" $ jGoal jdg
+          rule $ newSubgoal . withModifiedGoal (CType . mkAppTy applic . unCType)
+    Nothing ->
+      failure $ GoalMismatch "idiom" $ jGoal jdg
+
+subgoalWith :: Judgement -> TacticsM () -> RuleM (Synthesized (LHsExpr GhcPs))
+subgoalWith jdg t = RuleT $ flip execStateT jdg $ unTacticT t
 
diff --git a/src/Wingman/Types.hs b/src/Wingman/Types.hs
--- a/src/Wingman/Types.hs
+++ b/src/Wingman/Types.hs
@@ -38,7 +38,6 @@
 import           GHC.Generics
 import           GHC.SourceGen (var)
 import           Refinery.ProofState
-import           Refinery.Tactic
 import           Refinery.Tactic.Internal (TacticT(TacticT), RuleT (RuleT))
 import           System.IO.Unsafe (unsafePerformIO)
 import           Wingman.Debug
@@ -333,12 +332,12 @@
 
 
 instance MonadReader r m => MonadReader r (TacticT jdg ext err s m) where
-  ask = TacticT $ lift $ Effect $ fmap pure ask
+  ask = TacticT $ lift $ Effect $ asks pure
   local f (TacticT m) = TacticT $ Strict.StateT $ \jdg ->
     Effect $ local f $ pure $ Strict.runStateT m jdg
 
 instance MonadReader r m => MonadReader r (RuleT jdg ext err s m) where
-  ask = RuleT $ Effect $ fmap Axiom ask
+  ask = RuleT $ Effect $ asks Axiom
   local f (RuleT m) = RuleT $ Effect $ local f $ pure m
 
 mkMetaHoleName :: Int -> RdrName
@@ -463,7 +462,7 @@
   }
 
 instance Show Context where
-  show (Context {..}) = mconcat
+  show Context{..} = mconcat
     [ "Context "
     , showsPrec 10 ctxDefiningFuncs ""
     , showsPrec 10 ctxModuleFuncs ""
diff --git a/test/AutoTupleSpec.hs b/test/AutoTupleSpec.hs
--- a/test/AutoTupleSpec.hs
+++ b/test/AutoTupleSpec.hs
@@ -7,11 +7,10 @@
 import Control.Monad (replicateM)
 import Control.Monad.State (evalState)
 import Data.Either (isRight)
-import OccName (mkVarOcc)
+import Development.IDE.GHC.Compat.Core ( mkVarOcc, mkBoxedTupleTy )
 import System.IO.Unsafe
 import Test.Hspec
 import Test.QuickCheck
-import TysWiredIn (mkBoxedTupleTy)
 import Wingman.Judgements (mkFirstJudgement)
 import Wingman.Machinery
 import Wingman.Tactics (auto')
diff --git a/test/CodeAction/AutoSpec.hs b/test/CodeAction/AutoSpec.hs
--- a/test/CodeAction/AutoSpec.hs
+++ b/test/CodeAction/AutoSpec.hs
@@ -59,7 +59,7 @@
 
   describe "theta" $ do
     autoTest 12 10 "AutoThetaFix"
-    autoTest  7 20 "AutoThetaRankN"
+    autoTest  7 27 "AutoThetaRankN"
     autoTest  6 10 "AutoThetaGADT"
     autoTest  6  8 "AutoThetaGADTDestruct"
     autoTest  4  8 "AutoThetaEqCtx"
diff --git a/test/CodeAction/RunMetaprogramSpec.hs b/test/CodeAction/RunMetaprogramSpec.hs
--- a/test/CodeAction/RunMetaprogramSpec.hs
+++ b/test/CodeAction/RunMetaprogramSpec.hs
@@ -40,6 +40,10 @@
     metaTest  7 53 "MetaDeepOf"
     metaTest  2 34 "MetaWithArg"
     metaTest  2 18 "MetaLetSimple"
+    metaTest  5  9 "MetaIdiom"
+    metaTest  7  9 "MetaIdiomRecord"
+
+    metaTest 14 10 "MetaFundeps"
 
     metaTest  2 12 "IntrosTooMany"
 
diff --git a/test/ProviderSpec.hs b/test/ProviderSpec.hs
--- a/test/ProviderSpec.hs
+++ b/test/ProviderSpec.hs
@@ -20,3 +20,9 @@
     "T2" 8 8
     [ (not, Intros, "")
     ]
+
+  goldenTestMany "SubsequentTactics"
+    [ InvokeTactic Intros   ""   4  5
+    , InvokeTactic Destruct "du" 4  8
+    , InvokeTactic Auto     ""   4 15
+    ]
diff --git a/test/UnificationSpec.hs b/test/UnificationSpec.hs
--- a/test/UnificationSpec.hs
+++ b/test/UnificationSpec.hs
@@ -1,4 +1,6 @@
+{-# LANGUAGE CPP          #-}
 {-# LANGUAGE ViewPatterns #-}
+
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 
 module UnificationSpec where
@@ -12,13 +14,18 @@
 import qualified Data.Set as S
 import           Data.Traversable
 import           Data.Tuple (swap)
-import           TcType (substTy, tcGetTyVar_maybe)
+import           Development.IDE.GHC.Compat.Core (substTy, mkBoxedTupleTy)
 import           Test.Hspec
 import           Test.QuickCheck
-import           TysWiredIn (mkBoxedTupleTy)
 import           Wingman.GHC
 import           Wingman.Machinery (newUnivar)
 import           Wingman.Types
+
+#if __GLASGOW_HASKELL__ >= 900
+import GHC.Tc.Utils.TcType (tcGetTyVar_maybe)
+#else
+import TcType  (tcGetTyVar_maybe)
+#endif
 
 
 spec :: Spec
diff --git a/test/Utils.hs b/test/Utils.hs
--- a/test/Utils.hs
+++ b/test/Utils.hs
@@ -4,6 +4,7 @@
 {-# LANGUAGE ScopedTypeVariables   #-}
 {-# LANGUAGE TypeOperators         #-}
 {-# LANGUAGE ViewPatterns          #-}
+{-# LANGUAGE RecordWildCards #-}
 
 module Utils where
 
@@ -23,6 +24,7 @@
 import           Ide.Plugin.Tactic as Tactic
 import           Language.LSP.Types
 import           Language.LSP.Types.Lens hiding (actions, applyEdit, capabilities, executeCommand, id, line, message, name, rename, title)
+import qualified Language.LSP.Types.Lens as J
 import           System.Directory (doesFileExist)
 import           System.FilePath
 import           Test.Hls
@@ -42,8 +44,8 @@
 -- NB: These coordinates are in "file space", ie, 1-indexed.
 pointRange :: Int -> Int -> Range
 pointRange
-  (subtract 1 -> line)
-  (subtract 1 -> col) =
+  (subtract 1 -> fromIntegral -> line)
+  (subtract 1 -> fromIntegral -> col) =
     Range (Position line col) (Position line $ col + 1)
 
 
@@ -63,7 +65,7 @@
   runSessionWithServer'
     [plugin]
     def
-    (def { messageTimeout = 5 } )
+    (def { messageTimeout = 20 } )
     fullCaps
     tacticPath
 
@@ -96,40 +98,47 @@
       liftIO $
         (title `elem` titles) `shouldSatisfy` f
 
+data InvokeTactic = InvokeTactic
+  { it_command :: TacticCommand
+  , it_argument :: Text
+  , it_line :: Int
+  , it_col :: Int
+  }
 
+invokeTactic :: TextDocumentIdentifier -> InvokeTactic -> Session ()
+invokeTactic doc InvokeTactic{..} = do
+    -- wait for the entire build to finish, so that Tactics code actions that
+    -- use stale data will get uptodate stuff
+    void waitForDiagnostics
+    void $ waitForTypecheck doc
+    actions <- getCodeActions doc $ pointRange it_line it_col
+    case find ((== Just (tacticTitle it_command it_argument)) . codeActionTitle) actions of
+      Just (InR CodeAction {_command = Just c}) -> do
+          executeCommand c
+          void $ skipManyTill anyMessage $ message SWorkspaceApplyEdit
+      _ -> error $ show actions
 
+
 mkGoldenTest
     :: (Text -> Text -> Assertion)
-    -> TacticCommand
-    -> Text
-    -> Int
-    -> Int
+    -> [InvokeTactic]
     -> FilePath
     -> SpecWith ()
-mkGoldenTest eq tc occ line col input =
+mkGoldenTest eq invocations input =
   it (input <> " (golden)") $ do
     resetGlobalHoleRef
     runSessionForTactics $ do
       doc <- openDoc (input <.> "hs") "haskell"
-      -- wait for diagnostics to start coming
-      void waitForDiagnostics
-      -- wait for the entire build to finish, so that Tactics code actions that
-      -- use stale data will get uptodate stuff
-      void $ waitForTypecheck doc
-      actions <- getCodeActions doc $ pointRange line col
-      case find ((== Just (tacticTitle tc occ)) . codeActionTitle) actions of
-        Just (InR CodeAction {_command = Just c}) -> do
-            executeCommand c
-            _resp <- skipManyTill anyMessage (message SWorkspaceApplyEdit)
-            edited <- documentContents doc
-            let expected_name = input <.> "expected" <.> "hs"
-            -- Write golden tests if they don't already exist
-            liftIO $ (doesFileExist expected_name >>=) $ flip unless $ do
-                T.writeFile expected_name edited
-            expected <- liftIO $ T.readFile expected_name
-            liftIO $ edited `eq` expected
-        _ -> error $ show actions
+      traverse_ (invokeTactic doc) invocations
+      edited <- documentContents doc
+      let expected_name = input <.> "expected" <.> "hs"
+      -- Write golden tests if they don't already exist
+      liftIO $ (doesFileExist expected_name >>=) $ flip unless $ do
+          T.writeFile expected_name edited
+      expected <- liftIO $ T.readFile expected_name
+      liftIO $ edited `eq` expected
 
+
 mkCodeLensTest
     :: FilePath
     -> SpecWith ()
@@ -197,10 +206,13 @@
 
 
 goldenTest :: TacticCommand -> Text -> Int -> Int -> FilePath -> SpecWith ()
-goldenTest = mkGoldenTest shouldBe
+goldenTest tc occ line col = mkGoldenTest shouldBe [InvokeTactic tc occ line col]
 
+goldenTestMany :: FilePath -> [InvokeTactic] -> SpecWith ()
+goldenTestMany = flip $ mkGoldenTest shouldBe
+
 goldenTestNoWhitespace :: TacticCommand -> Text -> Int -> Int -> FilePath -> SpecWith ()
-goldenTestNoWhitespace = mkGoldenTest shouldBeIgnoringSpaces
+goldenTestNoWhitespace tc occ line col = mkGoldenTest shouldBeIgnoringSpaces [InvokeTactic tc occ line col]
 
 
 shouldBeIgnoringSpaces :: Text -> Text -> Assertion
diff --git a/test/golden/AutoThetaRankN.expected.hs b/test/golden/AutoThetaRankN.expected.hs
--- a/test/golden/AutoThetaRankN.expected.hs
+++ b/test/golden/AutoThetaRankN.expected.hs
@@ -4,5 +4,5 @@
 showMe f = f
 
 showedYou :: Int -> String
-showedYou = showMe show
+showedYou = showMe (\x -> show x)
 
diff --git a/test/golden/AutoThetaRankN.hs b/test/golden/AutoThetaRankN.hs
--- a/test/golden/AutoThetaRankN.hs
+++ b/test/golden/AutoThetaRankN.hs
@@ -4,5 +4,5 @@
 showMe f = f
 
 showedYou :: Int -> String
-showedYou = showMe _
+showedYou = showMe (\x -> _)
 
diff --git a/test/golden/MetaFundeps.expected.hs b/test/golden/MetaFundeps.expected.hs
new file mode 100644
--- /dev/null
+++ b/test/golden/MetaFundeps.expected.hs
@@ -0,0 +1,16 @@
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE MultiParamTypeClasses  #-}
+
+class Blah a b | a -> b, b -> a
+instance Blah Int Bool
+
+foo :: Int
+foo = 10
+
+bar :: Blah a b => a -> b
+bar = undefined
+
+qux :: Bool
+qux = bar foo
+
+
diff --git a/test/golden/MetaFundeps.hs b/test/golden/MetaFundeps.hs
new file mode 100644
--- /dev/null
+++ b/test/golden/MetaFundeps.hs
@@ -0,0 +1,16 @@
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE MultiParamTypeClasses  #-}
+
+class Blah a b | a -> b, b -> a
+instance Blah Int Bool
+
+foo :: Int
+foo = 10
+
+bar :: Blah a b => a -> b
+bar = undefined
+
+qux :: Bool
+qux = [wingman| use bar, use foo |]
+
+
diff --git a/test/golden/MetaIdiom.expected.hs b/test/golden/MetaIdiom.expected.hs
new file mode 100644
--- /dev/null
+++ b/test/golden/MetaIdiom.expected.hs
@@ -0,0 +1,6 @@
+foo :: Int -> Int -> Int
+foo = undefined
+
+test :: Maybe Int
+test = (foo <$> _w0) <*> _w1
+
diff --git a/test/golden/MetaIdiom.hs b/test/golden/MetaIdiom.hs
new file mode 100644
--- /dev/null
+++ b/test/golden/MetaIdiom.hs
@@ -0,0 +1,6 @@
+foo :: Int -> Int -> Int
+foo = undefined
+
+test :: Maybe Int
+test = [wingman| idiom (use foo) |]
+
diff --git a/test/golden/MetaIdiomRecord.expected.hs b/test/golden/MetaIdiomRecord.expected.hs
new file mode 100644
--- /dev/null
+++ b/test/golden/MetaIdiomRecord.expected.hs
@@ -0,0 +1,8 @@
+data Rec = Rec
+  { a :: Int
+  , b :: Bool
+  }
+
+test :: Maybe Rec
+test = (Rec <$> _w0) <*> _w1
+
diff --git a/test/golden/MetaIdiomRecord.hs b/test/golden/MetaIdiomRecord.hs
new file mode 100644
--- /dev/null
+++ b/test/golden/MetaIdiomRecord.hs
@@ -0,0 +1,8 @@
+data Rec = Rec
+  { a :: Int
+  , b :: Bool
+  }
+
+test :: Maybe Rec
+test = [wingman| idiom (ctor Rec) |]
+
diff --git a/test/golden/SubsequentTactics.expected.hs b/test/golden/SubsequentTactics.expected.hs
new file mode 100644
--- /dev/null
+++ b/test/golden/SubsequentTactics.expected.hs
@@ -0,0 +1,5 @@
+data Dummy a = Dummy a
+
+f :: Dummy Int -> Int
+f (Dummy n) = n
+
diff --git a/test/golden/SubsequentTactics.hs b/test/golden/SubsequentTactics.hs
new file mode 100644
--- /dev/null
+++ b/test/golden/SubsequentTactics.hs
@@ -0,0 +1,5 @@
+data Dummy a = Dummy a
+
+f :: Dummy Int -> Int
+f = _
+