diff --git a/ghcide/src/Development/IDE/GHC/ExactPrint.hs b/ghcide/src/Development/IDE/GHC/ExactPrint.hs
index a8e7a7638f..4e038aced3 100644
--- a/ghcide/src/Development/IDE/GHC/ExactPrint.hs
+++ b/ghcide/src/Development/IDE/GHC/ExactPrint.hs
@@ -1,9 +1,11 @@
-{-# LANGUAGE CPP #-}
+{-# LANGUAGE CPP                #-}
 {-# LANGUAGE DerivingStrategies #-}
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE OverloadedStrings #-}
-{-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE GADTs              #-}
+{-# LANGUAGE OverloadedStrings  #-}
+{-# LANGUAGE RankNTypes         #-}
+{-# LANGUAGE TypeFamilies       #-}
+
+{- HLINT ignore "Use zipFrom" -}
 
 module Development.IDE.GHC.ExactPrint
     ( Graft(..),
@@ -15,6 +17,8 @@ module Development.IDE.GHC.ExactPrint
       hoistGraft,
       graftWithM,
       graftWithSmallestM,
+      graftSmallestDecls,
+      graftSmallestDeclsWithM,
       transform,
       transformM,
       useAnnotatedSource,
@@ -60,9 +64,17 @@ import Language.LSP.Types.Capabilities (ClientCapabilities)
 import Outputable (Outputable, ppr, showSDoc)
 import Retrie.ExactPrint hiding (parseDecl, parseExpr, parsePattern, parseType)
 import Parser (parseIdentifier)
+import Data.Traversable (for)
+import Data.Foldable (Foldable(fold))
+import Data.Bool (bool)
 #if __GLASGOW_HASKELL__ == 808
 import Control.Arrow
 #endif
+#if __GLASGOW_HASKELL__ > 808
+import Bag (listToBag)
+import ErrUtils (mkErrMsg)
+import Outputable (text, neverQualify)
+#endif
 
 
 ------------------------------------------------------------------------------
@@ -202,6 +214,7 @@ graftWithoutParentheses dst val = Graft $ \dflags a -> do
             )
             a
 
+
 ------------------------------------------------------------------------------
 
 graftWithM ::
@@ -271,6 +284,44 @@ graftDecls dst decs0 = Graft $ \dflags a -> do
             | otherwise = DL.singleton (L src e) <> go rest
     modifyDeclsT (pure . DL.toList . go) a
 
+graftSmallestDecls ::
+    forall a.
+    (HasDecls a) =>
+    SrcSpan ->
+    [LHsDecl GhcPs] ->
+    Graft (Either String) a
+graftSmallestDecls dst decs0 = Graft $ \dflags a -> do
+    decs <- forM decs0 $ \decl -> do
+        (anns, decl') <- annotateDecl dflags decl
+        modifyAnnsT $ mappend anns
+        pure decl'
+    let go [] = DL.empty
+        go (L src e : rest)
+            | dst `isSubspanOf` src = DL.fromList decs <> DL.fromList rest
+            | otherwise = DL.singleton (L src e) <> go rest
+    modifyDeclsT (pure . DL.toList . go) a
+
+graftSmallestDeclsWithM ::
+    forall a.
+    (HasDecls a) =>
+    SrcSpan ->
+    (LHsDecl GhcPs -> TransformT (Either String) (Maybe [LHsDecl GhcPs])) ->
+    Graft (Either String) a
+graftSmallestDeclsWithM dst toDecls = Graft $ \dflags a -> do
+    let go [] = pure DL.empty
+        go (e@(L src _) : rest)
+            | dst `isSubspanOf` src = toDecls e >>= \case
+                Just decs0 -> do
+                    decs <- forM decs0 $ \decl -> do
+                        (anns, decl') <-
+                            annotateDecl dflags decl
+                        modifyAnnsT $ mappend anns
+                        pure decl'
+                    pure $ DL.fromList decs <> DL.fromList rest
+                Nothing -> (DL.singleton e <>) <$> go rest
+            | otherwise = (DL.singleton e <>) <$> go rest
+    modifyDeclsT (fmap DL.toList . go) a
+
 graftDeclsWithM ::
     forall a m.
     (HasDecls a, Fail.MonadFail m) =>
@@ -355,12 +406,37 @@ annotate dflags ast = do
 
 -- | Given an 'LHsDecl', compute its exactprint annotations.
 annotateDecl :: DynFlags -> LHsDecl GhcPs -> TransformT (Either String) (Anns, LHsDecl GhcPs)
+-- The 'parseDecl' function fails to parse 'FunBind' 'ValD's which contain
+-- multiple matches. To work around this, we split the single
+-- 'FunBind'-of-multiple-'Match'es into multiple 'FunBind's-of-one-'Match',
+-- and then merge them all back together.
+annotateDecl dflags
+            (L src (
+                ValD ext fb@FunBind
+                  { fun_matches = mg@MG { mg_alts = L alt_src alts@(_:_)}
+                  })) = do
+    let set_matches matches =
+          ValD ext fb { fun_matches = mg { mg_alts = L alt_src matches }}
+
+    (anns', alts') <- fmap unzip $ for (zip [0..] alts) $ \(ix :: Int, alt) -> do
+      uniq <- show <$> uniqueSrcSpanT
+      let rendered = render dflags $ set_matches [alt]
+      lift (mapLeft show $ parseDecl dflags uniq rendered) >>= \case
+        (ann, L _ (ValD _ FunBind { fun_matches = MG { mg_alts = L _ [alt']}}))
+           -> pure (bool id (setPrecedingLines alt' 1 0) (ix /= 0) ann, alt')
+        _ ->  lift $ Left "annotateDecl: didn't parse a single FunBind match"
+
+    let expr' = L src $ set_matches alts'
+        anns'' = setPrecedingLines expr' 1 0 $ fold anns'
+
+    pure (anns'', expr')
 annotateDecl dflags ast = do
     uniq <- show <$> uniqueSrcSpanT
     let rendered = render dflags ast
     (anns, expr') <- lift $ mapLeft show $ parseDecl dflags uniq rendered
     let anns' = setPrecedingLines expr' 1 0 anns
     pure (anns', expr')
+
 ------------------------------------------------------------------------------
 
 -- | Print out something 'Outputable'.
diff --git a/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal b/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal
index 71914280be..113380f3eb 100644
--- a/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal
+++ b/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal
@@ -24,6 +24,7 @@ library
   exposed-modules:
     Ide.Plugin.Tactic
     Ide.Plugin.Tactic.Auto
+    Ide.Plugin.Tactic.CaseSplit
     Ide.Plugin.Tactic.CodeGen
     Ide.Plugin.Tactic.CodeGen.Utils
     Ide.Plugin.Tactic.Context
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
index 74bba3f52c..8fd10c326d 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
@@ -6,6 +6,7 @@
 {-# LANGUAGE OverloadedStrings   #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TupleSections       #-}
+{-# LANGUAGE TypeApplications    #-}
 {-# LANGUAGE ViewPatterns        #-}
 
 -- | A plugin that uses tactics to synthesize code
@@ -15,6 +16,7 @@ module Ide.Plugin.Tactic
   , TacticCommand (..)
   ) where
 
+import           Bag (listToBag, bagToList)
 import           Control.Arrow
 import           Control.Monad
 import           Control.Monad.Error.Class (MonadError(throwError))
@@ -23,10 +25,10 @@ import           Control.Monad.Trans.Maybe
 import           Data.Aeson
 import           Data.Bool (bool)
 import           Data.Coerce
+import           Data.Data (Data)
 import           Data.Functor ((<&>))
 import           Data.Generics.Aliases (mkQ)
 import           Data.Generics.Schemes (everything)
-import           Data.List
 import           Data.Map (Map)
 import qualified Data.Map as M
 import           Data.Maybe
@@ -40,15 +42,14 @@ import           Development.IDE.Core.Service (runAction)
 import           Development.IDE.Core.Shake (useWithStale, IdeState (..))
 import           Development.IDE.GHC.Compat
 import           Development.IDE.GHC.Error (realSrcSpanToRange)
-import           Development.IDE.GHC.ExactPrint (graft, transform, useAnnotatedSource, maybeParensAST)
-import           Development.IDE.GHC.ExactPrint (graftWithoutParentheses)
+import           Development.IDE.GHC.ExactPrint
 import           Development.IDE.Spans.LocalBindings (getDefiningBindings)
 import           Development.Shake (Action)
-import           DynFlags (xopt)
 import qualified FastString
 import           GHC.Generics (Generic)
 import           GHC.LanguageExtensions.Type (Extension (LambdaCase))
 import           Ide.Plugin.Tactic.Auto
+import           Ide.Plugin.Tactic.CaseSplit
 import           Ide.Plugin.Tactic.Context
 import           Ide.Plugin.Tactic.GHC
 import           Ide.Plugin.Tactic.Judgements
@@ -61,6 +62,7 @@ import           Ide.Types
 import           Language.LSP.Server
 import           Language.LSP.Types
 import           OccName
+import           Prelude hiding (span)
 import           Refinery.Tactic (goal)
 import           SrcLoc (containsSpan)
 import           System.Timeout
@@ -193,7 +195,7 @@ codeActions = List . fmap InR
 provide :: TacticCommand -> T.Text -> TacticProvider
 provide tc name _ plId uri range _ = do
   let title = tacticTitle tc name
-      params = TacticParams { file = uri , range = range , var_name = name }
+      params = TacticParams { tp_file = uri , tp_range = range , tp_var_name = name }
       cmd = mkLspCommand plId (tcCommandId tc) title (Just [toJSON params])
   pure
     $ pure
@@ -240,9 +242,9 @@ filterBindingType p tp dflags plId uri range jdg =
 
 
 data TacticParams = TacticParams
-    { file :: Uri -- ^ Uri of the file to fill the hole in
-    , range :: Range -- ^ The range of the hole
-    , var_name :: T.Text
+    { tp_file :: Uri -- ^ Uri of the file to fill the hole in
+    , tp_range :: Range -- ^ The range of the hole
+    , tp_var_name :: T.Text
     }
   deriving (Show, Eq, Generic, ToJSON, FromJSON)
 
@@ -268,7 +270,7 @@ judgementForHole state nfp range = do
 
   case asts of
     (HAR _ hf _ _ kind) -> do
-      (rss, goal) <- liftMaybe $ join $ listToMaybe $ M.elems $ flip M.mapWithKey (getAsts hf) $ \fs ast ->
+      (rss, g) <- liftMaybe $ join $ listToMaybe $ M.elems $ flip M.mapWithKey (getAsts hf) $ \fs ast ->
           case selectSmallestContaining (rangeToRealSrcSpan (FastString.unpackFS fs) range') ast of
             Nothing -> Nothing
             Just ast' -> do
@@ -290,14 +292,14 @@ judgementForHole state nfp range = do
                    $ hypothesisFromBindings rss binds
           cls_hy = contextMethodHypothesis ctx
       case kind of
-        HieFromDisk hf' ->
+        HieFromDisk _hf' ->
           fail "Need a fresh hie file"
         HieFresh ->
           pure ( resulting_range
                , mkFirstJudgement
                    (local_hy <> cls_hy)
                    (isRhsHole rss tcs)
-                   goal
+                   g
                , ctx
                , dflags
                )
@@ -319,29 +321,15 @@ tacticCmd tac state (TacticParams uri range var_name)
         (range', jdg, ctx, dflags) <- judgementForHole state nfp range
         let span = rangeToRealSrcSpan (fromNormalizedFilePath nfp) range'
         pm <- MaybeT $ useAnnotatedSource "tacticsCmd" state nfp
-        x <- lift $ timeout 2e8 $
-          case runTactic ctx jdg
-                $ tac
-                $ mkVarOcc
-                $ T.unpack var_name of
+
+        x <- lift $ timeout 2e8 $ pure $
+          case runTactic ctx jdg $ tac $ mkVarOcc $ T.unpack var_name of
             Left err ->
-              pure $ Left
-                   $ ResponseError InvalidRequest (T.pack $ show err) Nothing
-            Right rtr -> do
-              traceMX "solns" $ rtr_other_solns rtr
-              traceMX "simplified" $ rtr_extract rtr
-              let g = graftWithoutParentheses (RealSrcSpan span)
-                      -- Parenthesize the extract iff we're not in a top level hole
-                    $ bool maybeParensAST id (_jIsTopHole jdg)
-                    $ rtr_extract rtr
-                  response = transform dflags clientCapabilities uri g pm
-              pure $ case response of
-                Right res -> Right $ Just res
-                Left err -> Left $ ResponseError InternalError (T.pack err) Nothing
-        pure $ case x of
-          Just y -> y
-          Nothing -> Left
-                   $ ResponseError InvalidRequest "timed out" Nothing
+              Left $ mkErr InvalidRequest $ T.pack $ show err
+            Right rtr ->
+              mkWorkspaceEdits rtr jdg span ctx dflags clientCapabilities uri pm
+        pure $ joinNote (mkErr InvalidRequest "timed out") x
+
       case res of
         Left err -> pure $ Left err
         Right medit -> do
@@ -349,12 +337,127 @@ tacticCmd tac state (TacticParams uri range var_name)
             sendRequest SWorkspaceApplyEdit (ApplyWorkspaceEditParams Nothing edit) (\_ -> pure ())
           pure $ Right Null
 tacticCmd _ _ _ =
-  pure $ Left $ ResponseError InvalidRequest (T.pack "Bad URI") Nothing
+  pure $ Left $ mkErr InvalidRequest "Bad URI"
+
+mkErr :: ErrorCode -> T.Text -> ResponseError
+mkErr code err = ResponseError code err Nothing
+
+
+joinNote :: e -> Maybe (Either e a) -> Either e a
+joinNote e Nothing = Left e
+joinNote _ (Just a) = a
+
+
+------------------------------------------------------------------------------
+-- | Turn a 'RunTacticResults' into concrete edits to make in the source
+-- document.
+mkWorkspaceEdits rtr jdg span ctx dflags clientCapabilities uri pm = do
+  let g = graftHole jdg (RealSrcSpan span) ctx rtr
+      response = transform dflags clientCapabilities uri g pm
+   in case response of
+        Right res -> Right $ Just res
+        Left err -> Left $ mkErr InternalError $ T.pack err
+
+
+------------------------------------------------------------------------------
+-- | Graft a 'RunTacticResults' into the correct place in an AST. Correctly
+-- deals with top-level holes, in which we might need to fiddle with the
+-- 'Match's that bind variables.
+graftHole
+  :: Judgement' a2
+  -> SrcSpan
+  -> Context
+  -> RunTacticResults
+  -> Graft (Either String) ParsedSource
+graftHole jdg span ctx rtr
+  | _jIsTopHole jdg
+      = graftSmallestDeclsWithM span
+      $ graftDecl span
+      $ \pats ->
+        splitToDecl (fst $ last $ ctxDefiningFuncs ctx)
+      $ iterateSplit
+      $ mkFirstAgda (fmap unXPat pats)
+      $ unLoc
+      $ rtr_extract rtr
+graftHole jdg span _ rtr
+  = graftWithoutParentheses span
+    -- Parenthesize the extract iff we're not in a top level hole
+  $ bool maybeParensAST id (_jIsTopHole jdg)
+  $ rtr_extract rtr
+
+
+------------------------------------------------------------------------------
+-- | Merge in the 'Match'es of a 'FunBind' into a 'HsDecl'. Used to perform
+-- agda-style case splitting in which we need to separate one 'Match' into
+-- many, without affecting any matches which might exist but don't need to be
+-- split.
+mergeFunBindMatches
+    :: ([Pat GhcPs] -> LHsDecl GhcPs)
+    -> SrcSpan
+    -> HsBind GhcPs
+    -> Either String (HsBind GhcPs)
+mergeFunBindMatches make_decl span (fb@FunBind {fun_matches = mg@MG {mg_alts = L alts_src alts}}) =
+  pure $
+    fb
+      { fun_matches = mg
+        { mg_alts = L alts_src $ do
+            alt@(L alt_src match) <- alts
+            case span `isSubspanOf` alt_src of
+              True -> do
+                let pats = fmap fromPatCompatPs $ m_pats match
+                    (L _ (ValD _ (FunBind {fun_matches = MG {mg_alts = L _ to_add}}))) =
+                        make_decl pats
+                to_add
+              False -> pure alt
+        }
+      }
+mergeFunBindMatches _ _ _ = Left "mergeFunBindMatches: called on something that isnt a funbind"
+
+
+noteT :: String -> TransformT (Either String) a
+noteT = lift . Left
+
+------------------------------------------------------------------------------
+-- | Helper function to route 'mergeFunBindMatches' into the right place in an
+-- AST --- correctly dealing with inserting into instance declarations.
+graftDecl
+    :: SrcSpan
+    -> ([Pat GhcPs] -> LHsDecl GhcPs)
+    -> LHsDecl GhcPs
+    -> TransformT (Either String) (Maybe [LHsDecl GhcPs])
+graftDecl span
+    make_decl
+    (L src (ValD ext fb))
+  = either noteT (pure . Just . pure . L src . ValD ext) $
+      mergeFunBindMatches make_decl span fb
+-- TODO(sandy): add another case for default methods in class definitions
+graftDecl span
+    make_decl
+    (L src (InstD ext cid@ClsInstD{cid_inst = cidi@ClsInstDecl{cid_sigs = _sigs, cid_binds = binds}}))
+  = do
+      binds' <-
+        for (bagToList binds) $ \b@(L bsrc bind) -> do
+          case bind of
+            fb@FunBind{}
+              | span `isSubspanOf` bsrc -> either noteT (pure . L bsrc) $ mergeFunBindMatches make_decl span fb
+            _ -> pure b
+
+      pure $ Just $ pure $ L src $ InstD ext $ cid
+        { cid_inst = cidi
+          { cid_binds = listToBag binds'
+          }
+        }
+graftDecl span _ x = do
+  traceMX "biggest" $ unsafeRender $ locateBiggest @(Match GhcPs (LHsExpr GhcPs)) span x
+  traceMX "first" $ unsafeRender $ locateFirst @(Match GhcPs (LHsExpr GhcPs)) x
+  noteT "graftDecl: don't know about this AST form"
+
 
 
 fromMaybeT :: Functor m => a -> MaybeT m a -> m a
 fromMaybeT def = fmap (fromMaybe def) . runMaybeT
 
+
 liftMaybe :: Monad m => Maybe a -> MaybeT m a
 liftMaybe a = MaybeT $ pure a
 
@@ -389,7 +492,16 @@ getRhsPosVals rss tcs
   ) tcs
 
 
+locateBiggest :: (Data r, Data a) => SrcSpan -> a -> Maybe r
+locateBiggest ss x = getFirst $ everything (<>)
+  ( mkQ mempty $ \case
+    L span r | ss `isSubspanOf` span -> pure r
+    _ -> mempty
+  )x
+
+locateFirst :: (Data r, Data a) => a -> Maybe r
+locateFirst x = getFirst $ everything (<>)
+  ( mkQ mempty $ \case
+    r -> pure r
+  ) x
 
--- TODO(sandy): Make this more robust
-isHole :: OccName -> Bool
-isHole = isPrefixOf "_" . occNameString
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/CaseSplit.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/CaseSplit.hs
new file mode 100644
index 0000000000..04d0f9bb12
--- /dev/null
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/CaseSplit.hs
@@ -0,0 +1,84 @@
+{-# LANGUAGE LambdaCase          #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications    #-}
+{-# LANGUAGE ViewPatterns        #-}
+
+module Ide.Plugin.Tactic.CaseSplit
+  ( mkFirstAgda
+  , iterateSplit
+  , splitToDecl
+  ) where
+
+import           Control.Lens
+import           Data.Bool (bool)
+import           Data.Data
+import           Data.Generics
+import           Data.Set (Set)
+import qualified Data.Set as S
+import           Development.IDE.GHC.Compat
+import           GHC.Exts (IsString(fromString))
+import           GHC.SourceGen (funBinds, match, wildP)
+import           Ide.Plugin.Tactic.GHC
+import           Ide.Plugin.Tactic.Types
+import           OccName
+
+
+
+------------------------------------------------------------------------------
+-- | Construct an 'AgdaMatch' from patterns in scope (should be the LHS of the
+-- match) and a body.
+mkFirstAgda :: [Pat GhcPs] -> HsExpr GhcPs -> AgdaMatch
+mkFirstAgda pats (Lambda pats' body) = mkFirstAgda (pats <> pats') body
+mkFirstAgda pats body = AgdaMatch pats body
+
+
+------------------------------------------------------------------------------
+-- | Transform an 'AgdaMatch' whose body is a case over a bound pattern, by
+-- splitting it into multiple matches: one for each alternative of the case.
+agdaSplit :: AgdaMatch -> [AgdaMatch]
+agdaSplit (AgdaMatch pats (Case (HsVar _ (L _ var)) matches)) = do
+  (i, pat) <- zip [id @Int 0 ..] pats
+  case pat of
+    VarPat _ (L _ patname) | eqRdrName patname var -> do
+      (case_pat, body) <- matches
+      -- TODO(sandy): use an at pattern if necessary
+      pure $ AgdaMatch (pats & ix i .~ case_pat) body
+    _ -> []
+agdaSplit x = [x]
+
+
+------------------------------------------------------------------------------
+-- | Replace unused bound patterns with wild patterns.
+wildify :: AgdaMatch -> AgdaMatch
+wildify (AgdaMatch pats body) =
+  let make_wild = bool id (wildifyT (allOccNames body)) $ not $ containsHole body
+   in AgdaMatch (make_wild pats) body
+
+
+------------------------------------------------------------------------------
+-- | Helper function for 'wildify'.
+wildifyT :: Data a => Set OccName -> a -> a
+wildifyT (S.map occNameString -> used) = everywhere $ mkT $ \case
+  VarPat _ (L _ var) | S.notMember (occNameString $ occName var) used -> wildP
+  (x :: Pat GhcPs) -> x
+
+
+------------------------------------------------------------------------------
+-- | Construct an 'HsDecl' from a set of 'AgdaMatch'es.
+splitToDecl
+    :: OccName  -- ^ The name of the function
+    -> [AgdaMatch]
+    -> LHsDecl GhcPs
+splitToDecl name ams = noLoc $ funBinds (fromString . occNameString . occName $ name) $ do
+  AgdaMatch pats body <- ams
+  pure $ match pats body
+
+
+------------------------------------------------------------------------------
+-- | Sometimes 'agdaSplit' exposes another opportunity to do 'agdaSplit'. This
+-- function runs it a few times, hoping it will find a fixpoint.
+iterateSplit :: AgdaMatch -> [AgdaMatch]
+iterateSplit am =
+  let iterated = iterate (agdaSplit =<<) $ pure am
+   in fmap wildify . head . drop 5 $ iterated
+
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Debug.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Debug.hs
index 6c528da4e3..f32562cc2e 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Debug.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Debug.hs
@@ -11,6 +11,7 @@ module Ide.Plugin.Tactic.Debug
   , traceX
   , traceIdX
   , traceMX
+  , traceFX
   ) where
 
 import Control.DeepSeq
@@ -53,3 +54,6 @@ traceX str a = trace (mappend ("!!!" <> str <> ": ") $ show a)
 traceIdX :: (Show a) => String -> a -> a
 traceIdX str a = trace (mappend ("!!!" <> str <> ": ") $ show a) a
 
+traceFX :: String -> (a -> String) -> a -> a
+traceFX str f a = trace (mappend ("!!!" <> str <> ": ") $ f a) a
+
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
index e7c473e471..a3efa75a6b 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
@@ -1,17 +1,26 @@
-{-# LANGUAGE CPP              #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE PatternSynonyms  #-}
-{-# LANGUAGE ViewPatterns     #-}
+{-# LANGUAGE CPP                 #-}
+{-# LANGUAGE FlexibleContexts    #-}
+{-# LANGUAGE LambdaCase          #-}
+{-# LANGUAGE OverloadedStrings   #-}
+{-# LANGUAGE PatternSynonyms     #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications    #-}
+{-# LANGUAGE ViewPatterns        #-}
 
 module Ide.Plugin.Tactic.GHC where
 
 import           Control.Monad.State
+import           Data.Function (on)
+import           Data.List (isPrefixOf)
 import qualified Data.Map as M
 import           Data.Maybe (isJust)
+import           Data.Set (Set)
+import qualified Data.Set as S
 import           Data.Traversable
 import           DataCon
 import           Development.IDE.GHC.Compat
-import           Generics.SYB (mkT, everywhere)
+import           GHC.SourceGen (match, case', lambda)
+import           Generics.SYB (mkQ, everything, listify, Data, mkT, everywhere)
 import           Ide.Plugin.Tactic.Types
 import           OccName
 import           TcType
@@ -21,6 +30,7 @@ import           TysWiredIn (intTyCon, floatTyCon, doubleTyCon, charTyCon)
 import           Unique
 import           Var
 
+
 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
@@ -112,6 +122,102 @@ algebraicTyCon (splitTyConApp_maybe -> Just (tycon, _))
   | otherwise = Just tycon
 algebraicTyCon _ = Nothing
 
+
+------------------------------------------------------------------------------
+-- | We can't compare 'RdrName' for equality directly. Instead, compare them by
+-- their 'OccName's.
+eqRdrName :: RdrName -> RdrName -> Bool
+eqRdrName = (==) `on` occNameString . occName
+
+
+------------------------------------------------------------------------------
+-- | Does this thing contain any references to 'HsVar's with the given
+-- 'RdrName'?
+containsHsVar :: Data a => RdrName -> a -> Bool
+containsHsVar name x = not $ null $ listify (
+  \case
+    ((HsVar _ (L _ a)) :: HsExpr GhcPs) | eqRdrName a name -> True
+    _ -> False
+  ) x
+
+
+------------------------------------------------------------------------------
+-- | Does this thing contain any holes?
+containsHole :: Data a => a -> Bool
+containsHole x = not $ null $ listify (
+  \case
+    ((HsVar _ (L _ name)) :: HsExpr GhcPs) -> isHole $ occName name
+    _ -> False
+  ) x
+
+
+------------------------------------------------------------------------------
+-- | Check if an 'OccName' is a hole
+isHole :: OccName -> Bool
+-- TODO(sandy): Make this more robust
+isHole = isPrefixOf "_" . occNameString
+
+
+------------------------------------------------------------------------------
+-- | Get all of the referenced occnames.
+allOccNames :: Data a => a -> Set OccName
+allOccNames = everything (<>) $ mkQ mempty $ \case
+    a -> S.singleton a
+
+
+
+
+------------------------------------------------------------------------------
+-- | A pattern over the otherwise (extremely) messy AST for lambdas.
+pattern Lambda :: [Pat GhcPs] -> HsExpr GhcPs -> HsExpr GhcPs
+pattern Lambda pats body <-
+  HsLam _
+    (MG {mg_alts = L _ [L _
+      (Match { m_pats = fmap fromPatCompatPs -> pats
+             , m_grhss = UnguardedRHSs body
+             })]})
+  where
+    -- If there are no patterns to bind, just stick in the body
+    Lambda [] body   = body
+    Lambda pats body = lambda pats body
+
+
+------------------------------------------------------------------------------
+-- | A GRHS that caontains no guards.
+pattern UnguardedRHSs :: HsExpr GhcPs -> GRHSs GhcPs (LHsExpr GhcPs)
+pattern UnguardedRHSs body <-
+  GRHSs {grhssGRHSs = [L _ (GRHS _ [] (L _ body))]}
+
+
+------------------------------------------------------------------------------
+-- | A match with a single pattern. Case matches are always 'SinglePatMatch'es.
+pattern SinglePatMatch :: Pat GhcPs -> HsExpr GhcPs -> Match GhcPs (LHsExpr GhcPs)
+pattern SinglePatMatch pat body <-
+  Match { m_pats = [fromPatCompatPs -> pat]
+        , m_grhss = UnguardedRHSs body
+        }
+
+
+------------------------------------------------------------------------------
+-- | Helper function for defining the 'Case' pattern.
+unpackMatches :: [Match GhcPs (LHsExpr GhcPs)] -> Maybe [(Pat GhcPs, HsExpr GhcPs)]
+unpackMatches [] = Just []
+unpackMatches (SinglePatMatch pat body : matches) =
+  (:) <$> pure (pat, body) <*> unpackMatches matches
+unpackMatches _ = Nothing
+
+
+------------------------------------------------------------------------------
+-- | A pattern over the otherwise (extremely) messy AST for lambdas.
+pattern Case :: HsExpr GhcPs -> [(Pat GhcPs, HsExpr GhcPs)] -> HsExpr GhcPs
+pattern Case scrutinee matches <-
+  HsCase _ (L _ scrutinee)
+    (MG {mg_alts = L _ (fmap unLoc -> unpackMatches -> Just matches)})
+  where
+    Case scrutinee matches =
+      case' scrutinee $ fmap (\(pat, body) -> match [pat] body) matches
+
+
 ------------------------------------------------------------------------------
 -- | Can ths type be lambda-cased?
 --
@@ -170,3 +276,17 @@ dataConExTys = DataCon.dataConExTyCoVars
 #else
 dataConExTys = DataCon.dataConExTyVars
 #endif
+
+
+------------------------------------------------------------------------------
+-- | In GHC 8.8, sometimes patterns are wrapped in 'XPat'.
+-- The nitty gritty details are explained at
+-- https://blog.shaynefletcher.org/2020/03/ghc-haskell-pats-and-lpats.html
+--
+-- We need to remove these in order to succesfull find patterns.
+unXPat :: Pat GhcPs -> Pat GhcPs
+#if __GLASGOW_HASKELL__ == 808
+unXPat (XPat (L _ pat)) = unXPat pat
+#endif
+unXPat pat = pat
+
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Simplify.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Simplify.hs
index c125d50876..2f5e5a4e0d 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Simplify.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Simplify.hs
@@ -8,17 +8,14 @@ module Ide.Plugin.Tactic.Simplify
   ( simplify
   ) where
 
-import Data.Data (Data)
-import Data.Generics (everywhere, somewhere, something, listify, extT, mkT, GenericT, mkQ)
+import Data.Generics (everywhere, mkT, GenericT)
 import Data.List.Extra (unsnoc)
-import Data.Maybe (isJust)
 import Data.Monoid (Endo (..))
 import Development.IDE.GHC.Compat
-import GHC.Exts (fromString)
-import GHC.SourceGen (var, op)
+import GHC.SourceGen (var)
 import GHC.SourceGen.Expr (lambda)
 import Ide.Plugin.Tactic.CodeGen.Utils
-import Ide.Plugin.Tactic.GHC (fromPatCompatPs)
+import Ide.Plugin.Tactic.GHC (fromPatCompatPs, containsHsVar)
 
 
 ------------------------------------------------------------------------------
@@ -57,17 +54,6 @@ foldEndo :: Foldable t => t (a -> a) -> a -> a
 foldEndo = appEndo . foldMap Endo
 
 
-------------------------------------------------------------------------------
--- | Does this thing contain any references to 'HsVar's with the given
--- 'RdrName'?
-containsHsVar :: Data a => RdrName -> a -> Bool
-containsHsVar name x = not $ null $ listify (
-  \case
-    ((HsVar _ (L _ a)) :: HsExpr GhcPs) | a == name -> True
-    _ -> False
-  ) x
-
-
 ------------------------------------------------------------------------------
 -- | Perform an eta reduction. For example, transforms @\x -> (f g) x@ into
 -- @f g@.
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs
index 0929d461d4..1c38cd15b2 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs
@@ -72,6 +72,9 @@ instance Show Class where
 instance Show (HsExpr GhcPs) where
   show  = unsafeRender
 
+instance Show (Pat GhcPs) where
+  show  = unsafeRender
+
 
 ------------------------------------------------------------------------------
 data TacticState = TacticState
@@ -372,3 +375,11 @@ data RunTacticResults = RunTacticResults
   , rtr_extract     :: LHsExpr GhcPs
   , rtr_other_solns :: [(Trace, LHsExpr GhcPs)]
   } deriving Show
+
+
+data AgdaMatch = AgdaMatch
+  { amPats :: [Pat GhcPs]
+  , amBody :: HsExpr GhcPs
+  }
+  deriving (Show)
+
diff --git a/test/testdata/tactic/FmapBoth.hs.expected b/test/testdata/tactic/FmapBoth.hs.expected
index 3160676e8f..825b00ebea 100644
--- a/test/testdata/tactic/FmapBoth.hs.expected
+++ b/test/testdata/tactic/FmapBoth.hs.expected
@@ -1,4 +1,3 @@
 fmapBoth :: (Functor f, Functor g) => (a -> b) -> (f a, g a) -> (f b, g b)
-fmapBoth = \ fab p_faga
-  -> case p_faga of { (fa, ga) -> (fmap fab fa, fmap fab ga) }
+fmapBoth fab (fa, ga) = (fmap fab fa, fmap fab ga)
 
diff --git a/test/testdata/tactic/GoldenApplicativeThen.hs.expected b/test/testdata/tactic/GoldenApplicativeThen.hs.expected
deleted file mode 100644
index fc7816581b..0000000000
--- a/test/testdata/tactic/GoldenApplicativeThen.hs.expected
+++ /dev/null
@@ -1,2 +0,0 @@
-useThen :: Applicative f => f Int -> f a -> f a
-useThen = (\ x x8 -> (*>) x x8)
diff --git a/test/testdata/tactic/GoldenArbitrary.hs.expected b/test/testdata/tactic/GoldenArbitrary.hs.expected
index 1d533bef3f..6f7af5c3fd 100644
--- a/test/testdata/tactic/GoldenArbitrary.hs.expected
+++ b/test/testdata/tactic/GoldenArbitrary.hs.expected
@@ -22,31 +22,32 @@ data Obj
 
 
 arbitrary :: Gen Obj
-arbitrary = let
-              terminal
-                = [(Square <$> arbitrary) <*> arbitrary, Circle <$> arbitrary,
-                   Polygon <$> arbitrary, pure Empty, pure Full]
-            in
-              sized
-                $ (\ n
-                     -> case n <= 1 of
-                          True -> oneof terminal
-                          False
-                            -> oneof
-                                 $ ([(Rotate2 <$> arbitrary) <*> scale (subtract 1) arbitrary,
-                                     Complement <$> scale (subtract 1) arbitrary,
-                                     (UnionR <$> arbitrary) <*> scale (subtract 1) arbitrary,
-                                     ((DifferenceR <$> arbitrary) <*> scale (flip div 2) arbitrary)
-                                       <*> scale (flip div 2) arbitrary,
-                                     (IntersectR <$> arbitrary) <*> scale (subtract 1) arbitrary,
-                                     ((Translate <$> arbitrary) <*> arbitrary)
-                                       <*> scale (subtract 1) arbitrary,
-                                     ((Scale <$> arbitrary) <*> arbitrary)
-                                       <*> scale (subtract 1) arbitrary,
-                                     ((Mirror <$> arbitrary) <*> arbitrary)
-                                       <*> scale (subtract 1) arbitrary,
-                                     (Outset <$> arbitrary) <*> scale (subtract 1) arbitrary,
-                                     (Shell <$> arbitrary) <*> scale (subtract 1) arbitrary,
-                                     (WithRounding <$> arbitrary) <*> scale (subtract 1) arbitrary]
-                                      <> terminal))
+arbitrary
+  = let
+      terminal
+        = [(Square <$> arbitrary) <*> arbitrary, Circle <$> arbitrary,
+           Polygon <$> arbitrary, pure Empty, pure Full]
+    in
+      sized
+        $ (\ n
+             -> case n <= 1 of
+                  True -> oneof terminal
+                  False
+                    -> oneof
+                         $ ([(Rotate2 <$> arbitrary) <*> scale (subtract 1) arbitrary,
+                             Complement <$> scale (subtract 1) arbitrary,
+                             (UnionR <$> arbitrary) <*> scale (subtract 1) arbitrary,
+                             ((DifferenceR <$> arbitrary) <*> scale (flip div 2) arbitrary)
+                               <*> scale (flip div 2) arbitrary,
+                             (IntersectR <$> arbitrary) <*> scale (subtract 1) arbitrary,
+                             ((Translate <$> arbitrary) <*> arbitrary)
+                               <*> scale (subtract 1) arbitrary,
+                             ((Scale <$> arbitrary) <*> arbitrary)
+                               <*> scale (subtract 1) arbitrary,
+                             ((Mirror <$> arbitrary) <*> arbitrary)
+                               <*> scale (subtract 1) arbitrary,
+                             (Outset <$> arbitrary) <*> scale (subtract 1) arbitrary,
+                             (Shell <$> arbitrary) <*> scale (subtract 1) arbitrary,
+                             (WithRounding <$> arbitrary) <*> scale (subtract 1) arbitrary]
+                              <> terminal))
 
diff --git a/test/testdata/tactic/GoldenBigTuple.hs.expected b/test/testdata/tactic/GoldenBigTuple.hs.expected
index c750f48356..1e7ccecde4 100644
--- a/test/testdata/tactic/GoldenBigTuple.hs.expected
+++ b/test/testdata/tactic/GoldenBigTuple.hs.expected
@@ -1,4 +1,4 @@
 -- There used to be a bug where we were unable to perform a nested split. The
 -- more serious regression test of this is 'AutoTupleSpec'.
 bigTuple :: (a, b, c, d) -> (a, b, (c, d))
-bigTuple = \ pabcd -> case pabcd of { (a, b, c, d) -> (a, b, (c, d)) }
+bigTuple (a, b, c, d) = (a, b, (c, d))
diff --git a/test/testdata/tactic/GoldenEitherAuto.hs.expected b/test/testdata/tactic/GoldenEitherAuto.hs.expected
index 833c250f0b..f7756898e0 100644
--- a/test/testdata/tactic/GoldenEitherAuto.hs.expected
+++ b/test/testdata/tactic/GoldenEitherAuto.hs.expected
@@ -1,5 +1,3 @@
 either' :: (a -> c) -> (b -> c) -> Either a b -> c
-either' = \ fac fbc eab
-  -> case eab of
-       (Left a) -> fac a
-       (Right b) -> fbc b
+either' fac _ (Left a) = fac a
+either' _ fbc (Right b) = fbc b
diff --git a/test/testdata/tactic/GoldenEitherHomomorphic.hs.expected b/test/testdata/tactic/GoldenEitherHomomorphic.hs.expected
index af8e10f357..c18f2ec476 100644
--- a/test/testdata/tactic/GoldenEitherHomomorphic.hs.expected
+++ b/test/testdata/tactic/GoldenEitherHomomorphic.hs.expected
@@ -1,5 +1,3 @@
 eitherSplit :: a -> Either (a -> b) (a -> c) -> Either b c
-eitherSplit = \ a efabfac
-  -> case efabfac of
-       (Left fab) -> Left (fab a)
-       (Right fac) -> Right (fac a)
+eitherSplit a (Left fab) = Left (fab a)
+eitherSplit a (Right fac) = Right (fac a)
diff --git a/test/testdata/tactic/GoldenFmapTree.hs.expected b/test/testdata/tactic/GoldenFmapTree.hs.expected
index ed608dcbbd..64eef825fa 100644
--- a/test/testdata/tactic/GoldenFmapTree.hs.expected
+++ b/test/testdata/tactic/GoldenFmapTree.hs.expected
@@ -1,7 +1,4 @@
 data Tree a = Leaf a | Branch (Tree a) (Tree a)
-
 instance Functor Tree where
-   fmap = \ fab ta
-     -> case ta of
-          (Leaf a) -> Leaf (fab a)
-          (Branch ta2 ta3) -> Branch (fmap fab ta2) (fmap fab ta3)
+  fmap fab (Leaf a) = Leaf (fab a)
+  fmap fab (Branch ta2 ta3) = Branch (fmap fab ta2) (fmap fab ta3)
diff --git a/test/testdata/tactic/GoldenFoldr.hs.expected b/test/testdata/tactic/GoldenFoldr.hs.expected
index e043416a4d..4e98d0c50e 100644
--- a/test/testdata/tactic/GoldenFoldr.hs.expected
+++ b/test/testdata/tactic/GoldenFoldr.hs.expected
@@ -1,5 +1,3 @@
 foldr2 :: (a -> b -> b) -> b -> [a] -> b
-foldr2 = \ f_b b l_a
-  -> case l_a of
-       [] -> b
-       (a : l_a4) -> f_b a (foldr2 f_b b l_a4)
+foldr2 _ b [] = b
+foldr2 f_b b (a : l_a4) = f_b a (foldr2 f_b b l_a4)
diff --git a/test/testdata/tactic/GoldenFromMaybe.hs.expected b/test/testdata/tactic/GoldenFromMaybe.hs.expected
index 7d08d130e5..90f8edcb79 100644
--- a/test/testdata/tactic/GoldenFromMaybe.hs.expected
+++ b/test/testdata/tactic/GoldenFromMaybe.hs.expected
@@ -1,5 +1,3 @@
 fromMaybe :: a -> Maybe a -> a
-fromMaybe = \ a ma
-  -> case ma of
-       Nothing -> a
-       (Just a2) -> a2
+fromMaybe a Nothing = a
+fromMaybe _ (Just a2) = a2
diff --git a/test/testdata/tactic/GoldenGADTDestruct.hs.expected b/test/testdata/tactic/GoldenGADTDestruct.hs.expected
index fe8d1a8bd8..7f9975ba33 100644
--- a/test/testdata/tactic/GoldenGADTDestruct.hs.expected
+++ b/test/testdata/tactic/GoldenGADTDestruct.hs.expected
@@ -4,4 +4,4 @@ data CtxGADT where
   MkCtxGADT :: (Show a, Eq a) => a -> CtxGADT
 
 ctxGADT :: CtxGADT -> String
-ctxGADT gadt = case gadt of { (MkCtxGADT a) -> _ }
+ctxGADT (MkCtxGADT a) = _
diff --git a/test/testdata/tactic/GoldenGADTDestructCoercion.hs.expected b/test/testdata/tactic/GoldenGADTDestructCoercion.hs.expected
index e3a3e4ed80..57aab53bb4 100644
--- a/test/testdata/tactic/GoldenGADTDestructCoercion.hs.expected
+++ b/test/testdata/tactic/GoldenGADTDestructCoercion.hs.expected
@@ -5,4 +5,4 @@ data E a b where
   E :: forall a b. (b ~ a, Ord a) => b -> E a [a]
 
 ctxGADT :: E a b -> String
-ctxGADT gadt = case gadt of { (E b) -> _ }
+ctxGADT (E b) = _
diff --git a/test/testdata/tactic/GoldenIdentityFunctor.hs.expected b/test/testdata/tactic/GoldenIdentityFunctor.hs.expected
index 91d1e22d3d..757bc8347a 100644
--- a/test/testdata/tactic/GoldenIdentityFunctor.hs.expected
+++ b/test/testdata/tactic/GoldenIdentityFunctor.hs.expected
@@ -1,3 +1,3 @@
 data Ident a = Ident a
 instance Functor Ident where
-   fmap = \ fab ia -> case ia of { (Ident a) -> Ident (fab a) }
+  fmap fab (Ident a) = Ident (fab a)
diff --git a/test/testdata/tactic/GoldenIntros.hs.expected b/test/testdata/tactic/GoldenIntros.hs.expected
index 8da62d6b9b..23eadc5edc 100644
--- a/test/testdata/tactic/GoldenIntros.hs.expected
+++ b/test/testdata/tactic/GoldenIntros.hs.expected
@@ -1,2 +1,2 @@
 blah :: Int -> Bool -> (a -> b) -> String -> Int
-blah = \ i b fab l_c -> _
+blah i b fab l_c = _
diff --git a/test/testdata/tactic/GoldenJoinCont.hs.expected b/test/testdata/tactic/GoldenJoinCont.hs.expected
index 7397859c4d..042675ab0b 100644
--- a/test/testdata/tactic/GoldenJoinCont.hs.expected
+++ b/test/testdata/tactic/GoldenJoinCont.hs.expected
@@ -1,4 +1,4 @@
 type Cont r a = ((a -> r) -> r)
 
 joinCont :: Cont r (Cont r a) -> Cont r a
-joinCont = \ f_r far -> f_r (\ f_r2 -> f_r2 far)
+joinCont f_r far = f_r (\ f_r2 -> f_r2 far)
diff --git a/test/testdata/tactic/GoldenListFmap.hs.expected b/test/testdata/tactic/GoldenListFmap.hs.expected
index 7ff6fabfce..4a0af02b09 100644
--- a/test/testdata/tactic/GoldenListFmap.hs.expected
+++ b/test/testdata/tactic/GoldenListFmap.hs.expected
@@ -1,5 +1,3 @@
 fmapList :: (a -> b) -> [a] -> [b]
-fmapList = \ fab l_a
-  -> case l_a of
-       [] -> []
-       (a : l_a3) -> fab a : fmapList fab l_a3
+fmapList _ [] = []
+fmapList fab (a : l_a3) = fab a : fmapList fab l_a3
diff --git a/test/testdata/tactic/GoldenNote.hs.expected b/test/testdata/tactic/GoldenNote.hs.expected
index 420ce242a0..99bc0cd6d0 100644
--- a/test/testdata/tactic/GoldenNote.hs.expected
+++ b/test/testdata/tactic/GoldenNote.hs.expected
@@ -1,5 +1,3 @@
 note :: e -> Maybe a -> Either e a
-note = \ e ma
-  -> case ma of
-       Nothing -> Left e
-       (Just a) -> Right a
+note e Nothing = Left e
+note _ (Just a) = Right a
diff --git a/test/testdata/tactic/GoldenPureList.hs.expected b/test/testdata/tactic/GoldenPureList.hs.expected
index fc5bcdc2a3..8f2bc80ea7 100644
--- a/test/testdata/tactic/GoldenPureList.hs.expected
+++ b/test/testdata/tactic/GoldenPureList.hs.expected
@@ -1,2 +1,2 @@
 pureList :: a -> [a]
-pureList = \ a -> a : []
+pureList a = a : []
diff --git a/test/testdata/tactic/GoldenSafeHead.hs.expected b/test/testdata/tactic/GoldenSafeHead.hs.expected
index 194b8922c0..7f8f73e5b7 100644
--- a/test/testdata/tactic/GoldenSafeHead.hs.expected
+++ b/test/testdata/tactic/GoldenSafeHead.hs.expected
@@ -1,5 +1,3 @@
 safeHead :: [x] -> Maybe x
-safeHead = \ l_x
-  -> case l_x of
-       [] -> Nothing
-       (x : l_x2) -> Just x
+safeHead [] = Nothing
+safeHead (x : _) = Just x
diff --git a/test/testdata/tactic/GoldenShowCompose.hs.expected b/test/testdata/tactic/GoldenShowCompose.hs.expected
index 8152b5a0ae..d8a78b3017 100644
--- a/test/testdata/tactic/GoldenShowCompose.hs.expected
+++ b/test/testdata/tactic/GoldenShowCompose.hs.expected
@@ -1,2 +1,2 @@
 showCompose :: Show a => (b -> a) -> b -> String
-showCompose = \ fba -> show . fba
+showCompose fba = show . fba
diff --git a/test/testdata/tactic/GoldenShowMapChar.hs.expected b/test/testdata/tactic/GoldenShowMapChar.hs.expected
index d4cb942825..22ab0bec15 100644
--- a/test/testdata/tactic/GoldenShowMapChar.hs.expected
+++ b/test/testdata/tactic/GoldenShowMapChar.hs.expected
@@ -1,2 +1,2 @@
 test :: Show a => a -> (String -> b) -> b
-test = \ a fl_cb -> fl_cb (show a)
+test a fl_cb = fl_cb (show a)
diff --git a/test/testdata/tactic/GoldenSwap.hs.expected b/test/testdata/tactic/GoldenSwap.hs.expected
index 2560c15acb..e09cb3800a 100644
--- a/test/testdata/tactic/GoldenSwap.hs.expected
+++ b/test/testdata/tactic/GoldenSwap.hs.expected
@@ -1,2 +1,2 @@
 swap :: (a, b) -> (b, a)
-swap = \ p_ab -> case p_ab of { (a, b) -> (b, a) }
+swap (a, b) = (b, a)
diff --git a/test/testdata/tactic/GoldenSwapMany.hs.expected b/test/testdata/tactic/GoldenSwapMany.hs.expected
index aaffc2d873..1d2bc0a605 100644
--- a/test/testdata/tactic/GoldenSwapMany.hs.expected
+++ b/test/testdata/tactic/GoldenSwapMany.hs.expected
@@ -1,2 +1,2 @@
 swapMany :: (a, b, c, d, e) -> (e, d, c, b, a)
-swapMany = \ pabcde -> case pabcde of { (a, b, c, d, e) -> (e, d, c, b, a) }
+swapMany (a, b, c, d, e) = (e, d, c, b, a)
diff --git a/test/testdata/tactic/RecordCon.hs.expected b/test/testdata/tactic/RecordCon.hs.expected
index 235efbdbfa..9abb0ff3f9 100644
--- a/test/testdata/tactic/RecordCon.hs.expected
+++ b/test/testdata/tactic/RecordCon.hs.expected
@@ -4,6 +4,6 @@ data MyRecord a = Record
     }
 
 blah :: (a -> Int) -> a -> MyRecord a
-blah = \ fai a -> Record {field1 = a, field2 = fai a}
+blah fai a = Record {field1 = a, field2 = fai a}