diff --git a/cabal.project b/cabal.project
index 45ef601d1f..a7b601076d 100644
--- a/cabal.project
+++ b/cabal.project
@@ -20,6 +20,6 @@ package ghcide
 
 write-ghc-environment-files: never
 
-index-state: 2020-09-23T17:24:43Z
+index-state: 2020-09-30T21:52:43Z
 
 allow-newer: data-tree-print:base
diff --git a/ghcide b/ghcide
index b279afbce7..0bfce3114c 160000
--- a/ghcide
+++ b/ghcide
@@ -1 +1 @@
-Subproject commit b279afbce74ef691a47159314e0b7023b2f7074a
+Subproject commit 0bfce3114c28bd00f7bf5729c32ec0f23a8d8854
diff --git a/haskell-language-server.cabal b/haskell-language-server.cabal
index 46a48386ce..e49e1a5451 100644
--- a/haskell-language-server.cabal
+++ b/haskell-language-server.cabal
@@ -80,7 +80,7 @@ library
 executable haskell-language-server
   import:           agpl, common-deps
   main-is:          Main.hs
-  hs-source-dirs:   exe plugins/default/src
+  hs-source-dirs:   exe plugins/default/src plugins/tactics/src
   other-modules:
     Ide.Plugin.Eval
     Ide.Plugin.Example
@@ -93,9 +93,17 @@ executable haskell-language-server
     Ide.Plugin.Retrie
     Ide.Plugin.StylishHaskell
     Ide.Plugin.Tactic
-    Ide.Plugin.Tactic.Types
+    Ide.Plugin.Tactic.CodeGen
+    Ide.Plugin.Tactic.Context
+    Ide.Plugin.Tactic.Debug
+    Ide.Plugin.Tactic.GHC
+    Ide.Plugin.Tactic.Judgements
     Ide.Plugin.Tactic.Machinery
+    Ide.Plugin.Tactic.Naming
+    Ide.Plugin.Tactic.Range
     Ide.Plugin.Tactic.Tactics
+    Ide.Plugin.Tactic.Types
+    Ide.Plugin.Tactic.TestTypes
     Ide.TreeTransform
 
   ghc-options:
@@ -147,8 +155,9 @@ executable haskell-language-server
     , transformers
     , unordered-containers
     , ghc-source-gen
-    , refinery
+    , refinery                 >=0.2.0.0
     , ghc-exactprint
+    , fingertree
 
   if flag(agpl)
     build-depends: brittany
@@ -237,7 +246,8 @@ test-suite func-test
     , tasty-golden
     , tasty-rerun
 
-  hs-source-dirs:     test/functional plugins/default/src
+  hs-source-dirs:     test/functional plugins/tactics/src
+
   main-is:            Main.hs
   other-modules:
     Command
@@ -258,7 +268,7 @@ test-suite func-test
     Symbol
     TypeDefinition
     Tactic
-    Ide.Plugin.Tactic.Types
+    Ide.Plugin.Tactic.TestTypes
 
   ghc-options:
     -Wall -Wno-name-shadowing -threaded -rtsopts -with-rtsopts=-N
diff --git a/plugins/default/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/default/src/Ide/Plugin/Tactic/Machinery.hs
deleted file mode 100644
index 51ef83e6cd..0000000000
--- a/plugins/default/src/Ide/Plugin/Tactic/Machinery.hs
+++ /dev/null
@@ -1,264 +0,0 @@
-{-# LANGUAGE DeriveGeneric         #-}
-{-# LANGUAGE FlexibleContexts      #-}
-{-# LANGUAGE FlexibleInstances     #-}
-{-# LANGUAGE MonoLocalBinds        #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE TypeSynonymInstances  #-}
-{-# LANGUAGE ViewPatterns          #-}
-{-# LANGUAGE ViewPatterns          #-}
-
-module Ide.Plugin.Tactic.Machinery where
-
-import           Control.Monad.State (get, modify, evalStateT)
-import           Data.Char
-import           Data.Function
-import           Data.List
-import           Data.Map (Map)
-import qualified Data.Map as M
-import           Data.Traversable
-import           DataCon
-import           Development.IDE.GHC.Compat
-import           Development.IDE.Types.Location
-import           DynFlags (unsafeGlobalDynFlags)
-import qualified FastString as FS
-import           GHC.Generics
-import           GHC.SourceGen.Overloaded
-import Development.IDE.Spans.LocalBindings
-import           Name
-import           Outputable hiding ((<>))
-import           Refinery.Tactic
-import           TcType
-import           Type
-import           TysWiredIn (listTyCon, pairTyCon, intTyCon, floatTyCon, doubleTyCon, charTyCon)
-import Data.Maybe
-import SrcLoc
-
-
-------------------------------------------------------------------------------
--- | Orphan instance for producing holes when attempting to solve tactics.
-instance MonadExtract (LHsExpr GhcPs) ProvableM where
-  hole = pure $ noLoc $ HsVar noExtField $ noLoc $ Unqual $ mkVarOcc "_"
-
-
-------------------------------------------------------------------------------
--- | A wrapper around 'Type' which supports equality and ordering.
-newtype CType = CType { unCType :: Type }
-
-instance Eq CType where
-  (==) = eqType `on` unCType
-
-instance Ord CType where
-  compare = nonDetCmpType `on` unCType
-
-
-------------------------------------------------------------------------------
--- | Given a 'SrcSpan' and a 'Bindings', create a hypothesis.
-hypothesisFromBindings :: RealSrcSpan -> Bindings -> Map OccName CType
-hypothesisFromBindings span bs = buildHypothesis (getLocalScope bs span)
-
-
-------------------------------------------------------------------------------
--- | Convert a @Set Id@ into a hypothesis.
-buildHypothesis :: [(Name, Maybe Type)] -> Map OccName CType
-buildHypothesis
-  = M.fromList
-  . mapMaybe go
-  where
-    go (n, t)
-      | Just ty <- t
-      , isAlpha . head . occNameString $ occ = Just (occ, CType ty)
-      | otherwise = Nothing
-      where
-        occ = occName n
-
-
-------------------------------------------------------------------------------
--- | The current bindings and goal for a hole to be filled by refinery.
-data Judgement = Judgement
-  { jHypothesis :: Map OccName CType
-  , jGoal       :: CType
-  }
-  deriving (Eq, Ord, Generic)
-
-
-------------------------------------------------------------------------------
--- | Reasons a tactic might fail.
-data TacticError
-  = UndefinedHypothesis OccName
-  | GoalMismatch String CType
-  | UnsolvedSubgoals [Judgement]
-  | NoProgress
-
-instance Show TacticError where
-    show (UndefinedHypothesis name) =
-      occNameString name <> " is not available in the hypothesis."
-    show (GoalMismatch tac (CType typ)) =
-      mconcat
-        [ "The tactic "
-        , tac
-        , " doesn't apply to goal type "
-        , unsafeRender typ
-        ]
-    show (UnsolvedSubgoals _) =
-      "There were unsolved subgoals"
-    show NoProgress =
-      "Unable to make progress"
-
-
-type ProvableM = ProvableT Judgement (Either TacticError)
-type TacticsM = TacticT Judgement (LHsExpr GhcPs) ProvableM
-type RuleM    = RuleT Judgement (LHsExpr GhcPs) ProvableM
-type Rule     = RuleM (LHsExpr GhcPs)
-
-
-------------------------------------------------------------------------------
--- | Produce a subgoal that must be solved before we can solve the original
--- goal.
-newSubgoal
-    :: Map OccName CType  -- ^ Available bindings
-    -> CType              -- ^ Sub-goal type
-    -> RuleM (LHsExpr GhcPs)
-newSubgoal hy g = subgoal =<< newJudgement hy g
-
-
-------------------------------------------------------------------------------
--- | Create a new judgment
-newJudgement
-    ::  Monad m
-    => Map OccName CType  -- ^ Available bindings
-    -> CType              -- ^ Sub-goal type
-    -> m Judgement
-newJudgement hy g = do
-  pure $ Judgement hy g
-
-
-------------------------------------------------------------------------------
--- | Produce a unique, good name for a type.
-mkGoodName
-    :: [OccName]  -- ^ Bindings in scope; used to ensure we don't shadow anything
-    -> Type       -- ^ The type to produce a name for
-    -> OccName
-mkGoodName in_scope t =
-  let tn = mkTyName t
-   in mkVarOcc $ case elem (mkVarOcc tn) in_scope of
-        True -> tn ++ show (length in_scope)
-        False -> tn
-
-
-------------------------------------------------------------------------------
--- | Like 'mkGoodName' but creates several apart names.
-mkManyGoodNames
-  :: (Traversable t, Monad m)
-  => M.Map OccName a
-  -> t Type
-  -> m (t OccName)
-mkManyGoodNames hy args =
-  flip evalStateT (getInScope hy) $ for args $ \at -> do
-    in_scope <- Control.Monad.State.get
-    let n = mkGoodName in_scope at
-    modify (n :)
-    pure n
-
-
-------------------------------------------------------------------------------
--- | Use type information to create a reasonable name.
-mkTyName :: Type -> String
--- eg. mkTyName (a -> B) = "fab"
-mkTyName (tcSplitFunTys -> ([a@(isFunTy -> False)], b))
-  = "f" ++ mkTyName a ++ mkTyName b
--- eg. mkTyName (a -> b -> C) = "f_C"
-mkTyName (tcSplitFunTys -> ((_:_), b))
-  = "f_" ++ mkTyName b
--- eg. mkTyName (Either A B) = "eab"
-mkTyName (splitTyConApp_maybe -> Just (c, args))
-  = mkTyConName c ++ foldMap mkTyName args
--- eg. mkTyName a = "a"
-mkTyName (getTyVar_maybe-> Just tv)
-  = occNameString $ occName tv
--- eg. mkTyName (forall x. y) = "y"
-mkTyName (tcSplitSigmaTy-> ((_:_), _, t))
-  = mkTyName t
-mkTyName _ = "x"
-
-
-------------------------------------------------------------------------------
--- | Is this a function type?
-isFunction :: Type -> Bool
-isFunction (tcSplitFunTys -> ((_:_), _)) = True
-isFunction _ = False
-
-------------------------------------------------------------------------------
--- | Is this an algebraic type?
-algebraicTyCon :: Type -> Maybe TyCon
-algebraicTyCon (splitTyConApp_maybe -> Just (tycon, _))
-  | tycon == intTyCon    = Nothing
-  | tycon == floatTyCon  = Nothing
-  | tycon == doubleTyCon = Nothing
-  | tycon == charTyCon   = Nothing
-  | tycon == funTyCon    = Nothing
-  | otherwise = Just tycon
-algebraicTyCon _ = Nothing
-
-
-------------------------------------------------------------------------------
--- | Get a good name for a type constructor.
-mkTyConName :: TyCon -> String
-mkTyConName tc
-  | tc == listTyCon = "l_"
-  | tc == pairTyCon = "p_"
-  | otherwise = fmap toLower . take 1 . occNameString $ getOccName tc
-
-
-------------------------------------------------------------------------------
--- | Attempt to generate a term of the right type using in-scope bindings, and
--- a given tactic.
-runTactic
-    :: Judgement
-    -> TacticsM ()       -- ^ Tactic to use
-    -> Either TacticError (LHsExpr GhcPs)
-runTactic jdg t
-  = fmap (fst)
-  . runProvableT
-  $ runTacticT t jdg
-
-
-------------------------------------------------------------------------------
--- | Which names are in scope?
-getInScope :: Map OccName a -> [OccName]
-getInScope = M.keys
-
-
-------------------------------------------------------------------------------
--- | Construct a data con with subgoals for each field.
-buildDataCon
-    :: Map OccName CType  -- ^ In-scope bindings
-    -> DataCon            -- ^ The data con to build
-    -> [Type]             -- ^ Type arguments for the data con
-    -> RuleM (LHsExpr GhcPs)
-buildDataCon hy dc apps = do
-  let args = dataConInstArgTys dc apps
-  sgs <- traverse (newSubgoal hy . CType) args
-  pure
-    . noLoc
-    . foldl' (@@)
-        (HsVar noExtField $ noLoc $ Unqual $ nameOccName $ dataConName dc)
-    $ fmap unLoc sgs
-
-
-------------------------------------------------------------------------------
--- | Convert a DAML compiler Range to a GHC SrcSpan
--- TODO(sandy): this doesn't belong here
-rangeToSrcSpan :: String -> Range -> SrcSpan
-rangeToSrcSpan file range = RealSrcSpan $ rangeToRealSrcSpan file range
-
-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))
-
-------------------------------------------------------------------------------
--- | Print something
-unsafeRender :: Outputable a => a -> String
-unsafeRender = showSDoc unsafeGlobalDynFlags . ppr
-
diff --git a/plugins/default/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/default/src/Ide/Plugin/Tactic/Tactics.hs
deleted file mode 100644
index a86e668568..0000000000
--- a/plugins/default/src/Ide/Plugin/Tactic/Tactics.hs
+++ /dev/null
@@ -1,180 +0,0 @@
-{-# LANGUAGE DeriveGeneric         #-}
-{-# LANGUAGE FlexibleInstances     #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE TypeSynonymInstances  #-}
-{-# LANGUAGE ViewPatterns          #-}
-
-module Ide.Plugin.Tactic.Tactics
-  ( module Ide.Plugin.Tactic.Tactics
-  , runTactic
-  ) where
-
-import           Control.Monad.Except (throwError)
-import           Data.List
-import qualified Data.Map as M
-import           Data.Traversable
-import           DataCon
-import           Development.IDE.GHC.Compat
-import           GHC.Exts
-import           GHC.SourceGen.Binds
-import           GHC.SourceGen.Expr
-import           GHC.SourceGen.Overloaded
-import           GHC.SourceGen.Pat
-import           Ide.Plugin.Tactic.Machinery
-import           Name
-import           Refinery.Tactic
-import           TcType
-import           Type hiding (Var)
-
-
-------------------------------------------------------------------------------
--- | Like 'var', but works over standard GHC 'OccName's.
-var' :: Var a => OccName -> a
-var' = var . fromString . occNameString
-
-------------------------------------------------------------------------------
--- | Like 'bvar', but works over standard GHC 'OccName's.
-bvar' :: BVar a => OccName -> a
-bvar' = bvar . fromString . occNameString
-
-
-------------------------------------------------------------------------------
--- | Use something in the hypothesis to fill the hole.
-assumption :: TacticsM ()
-assumption = rule $ \(Judgement hy g) ->
-  case find ((== g) . snd) $ toList hy of
-    Just (v, _) -> pure $ noLoc $ var' v
-    Nothing -> throwError $ GoalMismatch "assumption" g
-
-
-------------------------------------------------------------------------------
--- | Introduce a lambda.
-intro :: TacticsM ()
-intro = rule $ \(Judgement hy g) ->
-  case splitFunTy_maybe $ unCType g of
-    Just (a, b) -> do
-      v <- pure $ mkGoodName (getInScope hy) a
-      sg <- newSubgoal (M.singleton v (CType a) <> hy) $ CType b
-      pure $ noLoc $ lambda [bvar' v] $ unLoc sg
-    _ -> throwError $ GoalMismatch "intro" g
-
-------------------------------------------------------------------------------
--- | Introduce a lambda binding every variable.
-intros :: TacticsM ()
-intros = rule $ \(Judgement hy g) ->
-  case tcSplitFunTys $ unCType g of
-    ([], _) -> throwError $ GoalMismatch "intro" g
-    (as, b) -> do
-      vs <- mkManyGoodNames hy as
-      sg <- newSubgoal (M.fromList (zip vs $ fmap CType as) <> hy) $ CType b
-      pure
-        . noLoc
-        . lambda (fmap bvar' vs)
-        $ unLoc sg
-
-
-------------------------------------------------------------------------------
--- | Combinator for performign case splitting, and running sub-rules on the
--- resulting matches.
-destruct' :: (DataCon -> Judgement -> Rule) -> OccName -> TacticsM ()
-destruct' f term = rule $ \(Judgement hy g) -> do
-  case find ((== term) . fst) $ toList hy of
-    Nothing -> throwError $ UndefinedHypothesis term
-    Just (_, t) ->
-      case splitTyConApp_maybe $ unCType t of
-        Nothing -> throwError $ GoalMismatch "destruct" g
-        Just (tc, apps) -> do
-          fmap noLoc
-              $ case' (var' term)
-              <$> do
-            for (tyConDataCons tc) $ \dc -> do
-              let args = dataConInstArgTys dc apps
-              names <- mkManyGoodNames hy args
-
-              let pat :: Pat GhcPs
-                  pat = conP (fromString $ occNameString $ nameOccName $ dataConName dc)
-                      $ fmap bvar' names
-
-              j <- newJudgement (M.fromList (zip names (fmap CType args)) <> hy) g
-              sg <- f dc j
-              pure $ match [pat] $ unLoc sg
-
-
-------------------------------------------------------------------------------
--- | Case split, and leave holes in the matches.
-destruct :: OccName -> TacticsM ()
-destruct = destruct' $ const subgoal
-
-
-------------------------------------------------------------------------------
--- | Case split, using the same data constructor in the matches.
-homo :: OccName -> TacticsM ()
-homo = destruct' $ \dc (Judgement hy (CType g)) ->
-  buildDataCon hy dc (snd $ splitAppTys g)
-
-
-------------------------------------------------------------------------------
--- | Ensure a tactic produces no subgoals. Useful when working with
--- backtracking.
-solve :: TacticsM () -> TacticsM  ()
-solve t = t >> throwError NoProgress
-
-
-------------------------------------------------------------------------------
--- | Apply a function from the hypothesis.
-apply :: TacticsM ()
-apply = rule $ \(Judgement hy g) -> do
-  case find ((== Just g) . fmap (CType . snd) . splitFunTy_maybe . unCType . snd) $ toList hy of
-    Just (func, CType ty) -> do
-      let (args, _) = splitFunTys ty
-      sgs <- traverse (newSubgoal hy . CType) args
-      pure . noLoc
-           . foldl' (@@) (var' func)
-           $ fmap unLoc sgs
-    Nothing -> throwError $ GoalMismatch "apply" g
-
-
-------------------------------------------------------------------------------
--- | Introduce a data constructor, splitting a goal into the datacon's
--- constituent sub-goals.
-split :: TacticsM ()
-split = rule $ \(Judgement hy g) ->
-  case splitTyConApp_maybe $ unCType g of
-    Just (tc, apps) ->
-      case tyConDataCons tc of
-        [dc] -> buildDataCon hy dc apps
-        _ -> throwError $ GoalMismatch "split" g
-    Nothing -> throwError $ GoalMismatch "split" g
-
-
-------------------------------------------------------------------------------
--- | Run 'one' many times.
-deepen :: Int -> TacticsM ()
-deepen 0 = pure ()
-deepen depth = do
-  one
-  deepen $ depth - 1
-
-
-------------------------------------------------------------------------------
--- | Automatically solve a goal.
-auto :: TacticsM ()
-auto = (intro >> auto)
-   <!> (assumption >> auto)
-   <!> (split >> auto)
-   <!> (apply >> auto)
-   <!> pure ()
-
-
-------------------------------------------------------------------------------
--- | Run a tactic, and subsequently apply auto if it completes. If not, just
--- run the first tactic, leaving its subgoals as holes.
-autoIfPossible :: TacticsM () -> TacticsM ()
-autoIfPossible t = (t >> solve auto) <!> t
-
-
-------------------------------------------------------------------------------
--- | Do one obvious thing.
-one :: TacticsM ()
-one = intro <!> assumption <!> split <!> apply <!> pure ()
-
diff --git a/plugins/default/src/Ide/Plugin/Tactic.hs b/plugins/tactics/src/Ide/Plugin/Tactic.hs
similarity index 72%
rename from plugins/default/src/Ide/Plugin/Tactic.hs
rename to plugins/tactics/src/Ide/Plugin/Tactic.hs
index 6629a29471..199cc1a609 100644
--- a/plugins/default/src/Ide/Plugin/Tactic.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic.hs
@@ -1,10 +1,11 @@
-{-# LANGUAGE DeriveAnyClass    #-}
-{-# LANGUAGE DeriveGeneric     #-}
-{-# LANGUAGE LambdaCase        #-}
-{-# LANGUAGE OverloadedStrings #-}
-{-# LANGUAGE TupleSections     #-}
-{-# LANGUAGE TypeApplications  #-}
-{-# LANGUAGE ViewPatterns      #-}
+{-# LANGUAGE DeriveAnyClass      #-}
+{-# LANGUAGE DeriveGeneric       #-}
+{-# LANGUAGE LambdaCase          #-}
+{-# LANGUAGE OverloadedStrings   #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TupleSections       #-}
+{-# LANGUAGE TypeApplications    #-}
+{-# LANGUAGE ViewPatterns        #-}
 
 -- | A plugin that uses tactics to synthesize code
 module Ide.Plugin.Tactic
@@ -13,14 +14,15 @@ module Ide.Plugin.Tactic
   , TacticCommand (..)
   ) where
 
+import           Control.Arrow
 import           Control.Monad
 import           Control.Monad.Trans
 import           Control.Monad.Trans.Maybe
 import           Data.Aeson
 import           Data.Coerce
 import qualified Data.Map as M
-import qualified Data.Set as S
 import           Data.Maybe
+import qualified Data.Set as S
 import qualified Data.Text as T
 import           Data.Traversable
 import           Development.IDE.Core.PositionMapping
@@ -29,20 +31,25 @@ 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.Util (hscEnv)
+import           Development.IDE.Spans.LocalBindings (getDefiningBindings)
 import           Development.Shake (Action)
+import           DynFlags (xopt)
+import qualified FastString
 import           GHC.Generics (Generic)
-import           HscTypes (hsc_dflags)
+import           GHC.LanguageExtensions.Type (Extension (LambdaCase))
 import           Ide.Plugin (mkLspCommand)
-import           Ide.Plugin.Tactic.Machinery
+import           Ide.Plugin.Tactic.Context
+import           Ide.Plugin.Tactic.GHC
+import           Ide.Plugin.Tactic.Judgements
+import           Ide.Plugin.Tactic.Range
 import           Ide.Plugin.Tactic.Tactics
+import           Ide.Plugin.Tactic.TestTypes
 import           Ide.Plugin.Tactic.Types
 import           Ide.TreeTransform (transform, graft, useAnnotatedSource)
 import           Ide.Types
 import           Language.Haskell.LSP.Core (clientCapabilities)
 import           Language.Haskell.LSP.Types
 import           OccName
-import qualified FastString
 
 
 descriptor :: PluginId -> PluginDescriptor
@@ -53,22 +60,17 @@ descriptor plId = (defaultPluginDescriptor plId)
               (tcCommandId tc)
               (tacticDesc $ tcCommandName tc)
               (tacticCmd $ commandTactic tc))
-              enabledTactics
+              [minBound .. maxBound]
     , pluginCodeActionProvider = Just codeActionProvider
     }
 
 tacticDesc :: T.Text -> T.Text
 tacticDesc name = "fill the hole using the " <> name <> " tactic"
 
-------------------------------------------------------------------------------
-
-enabledTactics :: [TacticCommand]
-enabledTactics = [Intros, Destruct, Homomorphism]
-
 ------------------------------------------------------------------------------
 -- | A 'TacticProvider' is a way of giving context-sensitive actions to the LS
 -- UI.
-type TacticProvider = PluginId -> Uri -> Range -> Judgement -> IO [CAResult]
+type TacticProvider = DynFlags -> PluginId -> Uri -> Range -> Judgement -> IO [CAResult]
 
 
 ------------------------------------------------------------------------------
@@ -87,10 +89,6 @@ tcCommandName = T.pack . show
 -- 'filterGoalType' and 'filterBindingType' for the nitty gritty.
 commandProvider :: TacticCommand -> TacticProvider
 commandProvider Auto  = provide Auto ""
-commandProvider Split = provide Split ""
-commandProvider Intro =
-  filterGoalType isFunction $
-    provide Intro ""
 commandProvider Intros =
   filterGoalType isFunction $
     provide Intros ""
@@ -100,17 +98,25 @@ commandProvider Destruct =
 commandProvider Homomorphism =
   filterBindingType homoFilter $ \occ _ ->
     provide Homomorphism $ T.pack $ occNameString occ
+commandProvider DestructLambdaCase =
+  requireExtension LambdaCase $
+    filterGoalType (isJust . lambdaCaseable) $
+      provide DestructLambdaCase ""
+commandProvider HomomorphismLambdaCase =
+  requireExtension LambdaCase $
+    filterGoalType ((== Just True) . lambdaCaseable) $
+      provide HomomorphismLambdaCase ""
 
 
 ------------------------------------------------------------------------------
 -- | A mapping from tactic commands to actual tactics for refinery.
 commandTactic :: TacticCommand -> OccName -> TacticsM ()
 commandTactic Auto         = const auto
-commandTactic Split        = const split
-commandTactic Intro        = const intro
 commandTactic Intros       = const intros
 commandTactic Destruct     = destruct
 commandTactic Homomorphism = homo
+commandTactic DestructLambdaCase     = const destructLambdaCase
+commandTactic HomomorphismLambdaCase = const homoLambdaCase
 
 
 ------------------------------------------------------------------------------
@@ -137,13 +143,14 @@ codeActionProvider :: CodeActionProvider
 codeActionProvider _conf state plId (TextDocumentIdentifier uri) range _ctx
   | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri =
       fromMaybeT (Right $ List []) $ do
-        (_, span, jdg) <- MaybeT $ judgementForHole state nfp range
+        (_, jdg, _, dflags) <- judgementForHole state nfp range
         actions <- lift $
           -- This foldMap is over the function monoid.
-          foldMap commandProvider enabledTactics
+          foldMap commandProvider [minBound .. maxBound]
+            dflags
             plId
             uri
-            span
+            range
             jdg
         pure $ Right $ List actions
 codeActionProvider _ _ _ _ _ _ = pure $ Right $ codeActions []
@@ -157,7 +164,7 @@ codeActions = List . fmap CACodeAction
 -- | Terminal constructor for providing context-sensitive tactics. Tactics
 -- given by 'provide' are always available.
 provide :: TacticCommand -> T.Text -> TacticProvider
-provide tc name plId uri range _ = do
+provide tc name _ plId uri range _ = do
   let title = tacticTitle tc name
       params = TacticParams { file = uri , range = range , var_name = name }
   cmd <- mkLspCommand plId (tcCommandId tc) title (Just [toJSON params])
@@ -168,13 +175,23 @@ provide tc name plId uri range _ = do
     $ Just cmd
 
 
+------------------------------------------------------------------------------
+-- | Restrict a 'TacticProvider', making sure it appears only when the given
+-- predicate holds for the goal.
+requireExtension :: Extension -> TacticProvider -> TacticProvider
+requireExtension ext tp dflags plId uri range jdg =
+  case xopt ext dflags of
+    True  -> tp dflags plId uri range jdg
+    False -> pure []
+
+
 ------------------------------------------------------------------------------
 -- | Restrict a 'TacticProvider', making sure it appears only when the given
 -- predicate holds for the goal.
 filterGoalType :: (Type -> Bool) -> TacticProvider -> TacticProvider
-filterGoalType p tp plId uri range jdg@(Judgement _ (CType g)) =
-  case p g of
-    True  -> tp plId uri range jdg
+filterGoalType p tp dflags plId uri range jdg =
+  case p $ unCType $ jGoal jdg of
+    True  -> tp dflags plId uri range jdg
     False -> pure []
 
 
@@ -185,11 +202,13 @@ filterBindingType
     :: (Type -> Type -> Bool)  -- ^ Goal and then binding types.
     -> (OccName -> Type -> TacticProvider)
     -> TacticProvider
-filterBindingType p tp plId uri range jdg@(Judgement hys (CType g)) =
-  fmap join $ for (M.toList hys) $ \(occ, CType ty) ->
-    case p g ty of
-      True  -> tp occ ty plId uri range jdg
-      False -> pure []
+filterBindingType p tp dflags plId uri range jdg =
+  let hy = jHypothesis jdg
+      g  = jGoal jdg
+   in fmap join $ for (M.toList hy) $ \(occ, CType ty) ->
+        case p (unCType g) ty of
+          True  -> tp occ ty dflags plId uri range jdg
+          False -> pure []
 
 
 data TacticParams = TacticParams
@@ -207,13 +226,18 @@ judgementForHole
     :: IdeState
     -> NormalizedFilePath
     -> Range
-    -> IO (Maybe (PositionMapping, Range, Judgement))
-judgementForHole state nfp range = runMaybeT $ do
+    -> MaybeT IO (Range, Judgement, Context, DynFlags)
+judgementForHole state nfp range = do
   (asts, amapping) <- MaybeT $ runIde state $ useWithStale GetHieAst nfp
   range' <- liftMaybe $ fromCurrentRange amapping range
 
   (binds, _) <- MaybeT $ runIde state $ useWithStale GetBindings nfp
 
+  -- Ok to use the stale 'ModIface', since all we need is its 'DynFlags'
+  -- which don't change very often.
+  (modsum, _) <- MaybeT $ runIde state $ useWithStale GetModSummaryWithoutTimestamps nfp
+  let dflags = ms_hspp_opts modsum
+
   (rss, goal) <- liftMaybe $ join $ listToMaybe $ M.elems $ flip M.mapWithKey (getAsts $ hieAst asts) $ \fs ast ->
       case selectSmallestContaining (rangeToRealSrcSpan (FastString.unpackFS fs) range') ast of
         Nothing -> Nothing
@@ -224,22 +248,25 @@ judgementForHole state nfp range = runMaybeT $ do
           pure (nodeSpan ast', ty)
 
   resulting_range <- liftMaybe $ toCurrentRange amapping $ realSrcSpanToRange rss
+  (tcmod, _) <- MaybeT $ runIde state $ useWithStale TypeCheck nfp
+  let tcg = fst $ tm_internals_ $ tmrModule tcmod
+      ctx = mkContext
+              (mapMaybe (sequenceA . (occName *** coerce))
+                $ getDefiningBindings binds rss)
+              tcg
+      hyps = hypothesisFromBindings rss binds
+  pure (resulting_range, mkFirstJudgement hyps goal, ctx, dflags)
 
-  let hyps = hypothesisFromBindings rss binds
-  pure (amapping, resulting_range, Judgement hyps $ CType goal)
 
 
 tacticCmd :: (OccName -> TacticsM ()) -> CommandFunction TacticParams
 tacticCmd tac lf state (TacticParams uri range var_name)
   | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri =
       fromMaybeT (Right Null, Nothing) $ do
-        (pos, _, jdg) <- MaybeT $ judgementForHole state nfp range
-        -- Ok to use the stale 'ModIface', since all we need is its 'DynFlags'
-        -- which don't change very often.
-        (hscenv, _) <- MaybeT $ runIde state $ useWithStale GhcSession nfp
-        let dflags = hsc_dflags $ hscEnv hscenv
+        (range', jdg, ctx, dflags) <- judgementForHole state nfp range
+        let span = rangeToRealSrcSpan (fromNormalizedFilePath nfp) range'
         pm <- MaybeT $ useAnnotatedSource "tacticsCmd" state nfp
-        case runTactic jdg
+        case runTactic ctx jdg
               $ tac
               $ mkVarOcc
               $ T.unpack var_name of
@@ -248,10 +275,8 @@ tacticCmd tac lf state (TacticParams uri range var_name)
               $ Left
               $ ResponseError InvalidRequest (T.pack $ show err) Nothing
           Right res -> do
-            range' <- liftMaybe $ toCurrentRange pos range
-            let span = rangeToSrcSpan (fromNormalizedFilePath nfp) range'
-                g = graft span res
-            let response = transform dflags (clientCapabilities lf) uri g pm
+            let g = graft (RealSrcSpan span) res
+                response = transform dflags (clientCapabilities lf) uri g pm
             pure $ case response of
                Right res -> (Right Null , Just (WorkspaceApplyEdit, ApplyWorkspaceEditParams res))
                Left err -> (Left $ ResponseError InternalError (T.pack err) Nothing, Nothing)
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
new file mode 100644
index 0000000000..1f1f3ea449
--- /dev/null
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
@@ -0,0 +1,105 @@
+{-# LANGUAGE FlexibleContexts #-}
+module Ide.Plugin.Tactic.CodeGen where
+
+import Control.Monad.Except
+import Data.List
+import Data.Traversable
+import DataCon
+import Development.IDE.GHC.Compat
+import GHC.Exts
+import GHC.SourceGen.Binds
+import GHC.SourceGen.Expr
+import GHC.SourceGen.Overloaded
+import GHC.SourceGen.Pat
+import Ide.Plugin.Tactic.Judgements
+import Ide.Plugin.Tactic.Machinery
+import Ide.Plugin.Tactic.Naming
+import Ide.Plugin.Tactic.Types
+import Name
+import Type hiding (Var)
+
+
+destructMatches
+    :: (DataCon -> Judgement -> Rule)
+       -- ^ How to construct each match
+    -> (Judgement -> Judgement)
+       -- ^ How to derive each match judgement
+    -> CType
+       -- ^ Type being destructed
+    -> Judgement
+    -> RuleM [RawMatch]
+destructMatches f f2 t jdg = do
+  let hy = jHypothesis jdg
+      g  = jGoal jdg
+  case splitTyConApp_maybe $ unCType t of
+    Nothing -> throwError $ GoalMismatch "destruct" g
+    Just (tc, apps) -> do
+      let dcs = tyConDataCons tc
+      case dcs of
+        [] -> throwError $ GoalMismatch "destruct" g
+        _ -> for dcs $ \dc -> do
+          let args = dataConInstArgTys dc apps
+          names <- mkManyGoodNames hy args
+
+          let pat :: Pat GhcPs
+              pat = conP (fromString $ occNameString $ nameOccName $ dataConName dc)
+                  $ fmap bvar' names
+              j = f2
+                $ introducingPat (zip names $ coerce args)
+                $ withNewGoal g jdg
+          sg <- f dc j
+          pure $ match [pat] $ unLoc sg
+
+
+------------------------------------------------------------------------------
+-- | Combinator for performing case splitting, and running sub-rules on the
+-- resulting matches.
+destruct' :: (DataCon -> Judgement -> Rule) -> OccName -> Judgement -> Rule
+destruct' f term jdg = do
+  let hy = jHypothesis jdg
+  case find ((== term) . fst) $ toList hy of
+    Nothing -> throwError $ UndefinedHypothesis term
+    Just (_, t) ->
+      fmap noLoc $ case' (var' term) <$>
+        destructMatches f (destructing term) t jdg
+
+
+------------------------------------------------------------------------------
+-- | Combinator for performign case splitting, and running sub-rules on the
+-- resulting matches.
+destructLambdaCase' :: (DataCon -> Judgement -> Rule) -> Judgement -> Rule
+destructLambdaCase' f jdg = do
+  let g  = jGoal jdg
+  case splitFunTy_maybe (unCType g) of
+    Just (arg, _) | isAlgType arg ->
+      fmap noLoc $ lambdaCase <$>
+        destructMatches f id (CType arg) jdg
+    _ -> throwError $ GoalMismatch "destructLambdaCase'" g
+
+
+------------------------------------------------------------------------------
+-- | Construct a data con with subgoals for each field.
+buildDataCon
+    :: Judgement
+    -> DataCon            -- ^ The data con to build
+    -> [Type]             -- ^ Type arguments for the data con
+    -> RuleM (LHsExpr GhcPs)
+buildDataCon jdg dc apps = do
+  let args = dataConInstArgTys dc apps
+  sgs <- traverse (newSubgoal . flip withNewGoal jdg . CType) args
+  pure
+    . noLoc
+    . foldl' (@@)
+        (HsVar noExtField $ noLoc $ Unqual $ nameOccName $ dataConName dc)
+    $ fmap unLoc sgs
+
+
+------------------------------------------------------------------------------
+-- | Like 'var', but works over standard GHC 'OccName's.
+var' :: Var a => OccName -> a
+var' = var . fromString . occNameString
+
+------------------------------------------------------------------------------
+-- | Like 'bvar', but works over standard GHC 'OccName's.
+bvar' :: BVar a => OccName -> a
+bvar' = bvar . fromString . occNameString
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Context.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Context.hs
new file mode 100644
index 0000000000..f1cccae928
--- /dev/null
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Context.hs
@@ -0,0 +1,42 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE LambdaCase       #-}
+
+module Ide.Plugin.Tactic.Context where
+
+import Bag
+import Control.Arrow
+import Control.Monad.Reader
+import Development.IDE.GHC.Compat
+import Ide.Plugin.Tactic.Types
+import OccName
+import TcRnTypes
+
+
+mkContext :: [(OccName, CType)] -> TcGblEnv -> Context
+mkContext locals
+  = Context locals
+  . fmap splitId
+  . (getFunBindId =<<)
+  . fmap unLoc
+  . bagToList
+  . tcg_binds
+
+
+splitId :: Id -> (OccName, CType)
+splitId = occName &&& CType . idType
+
+
+getFunBindId :: HsBindLR GhcTc GhcTc -> [Id]
+getFunBindId (AbsBinds _ _ _ abes _ _ _)
+  = abes >>= \case
+      ABE _ poly _ _ _ -> pure poly
+      _ -> []
+getFunBindId _ = []
+
+
+getCurrentDefinitions :: MonadReader Context m => m [OccName]
+getCurrentDefinitions = asks $ fmap fst . ctxDefiningFuncs
+
+getModuleHypothesis :: MonadReader Context m => m [(OccName, CType)]
+getModuleHypothesis = asks ctxModuleFuncs
+
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Debug.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Debug.hs
new file mode 100644
index 0000000000..6d1053c2c6
--- /dev/null
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Debug.hs
@@ -0,0 +1,20 @@
+module Ide.Plugin.Tactic.Debug
+  ( unsafeRender
+  , unsafeRender'
+  , traceM
+  , traceShowId
+  , trace
+  ) where
+
+import Debug.Trace
+import DynFlags (unsafeGlobalDynFlags)
+import Outputable
+
+------------------------------------------------------------------------------
+-- | Print something
+unsafeRender :: Outputable a => a -> String
+unsafeRender = unsafeRender' . ppr
+
+unsafeRender' :: SDoc -> String
+unsafeRender' = showSDoc unsafeGlobalDynFlags
+
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
new file mode 100644
index 0000000000..9d1c34851b
--- /dev/null
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
@@ -0,0 +1,69 @@
+{-# LANGUAGE ViewPatterns #-}
+
+module Ide.Plugin.Tactic.GHC where
+
+import Data.Maybe (isJust)
+import TcType
+import TyCoRep
+import TyCon
+import Type
+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
+                                                -- this is only used for
+                                                -- e.g., FlexibleContexts
+tcTyVar_maybe (TyVarTy v)   = Just v
+tcTyVar_maybe _             = Nothing
+
+
+instantiateType :: Type -> ([TyVar], Type)
+instantiateType t = do
+  let vs  = tyCoVarsOfTypeList t
+      vs' = fmap cloneTyVar vs
+      subst = foldr (\(v,t) a -> extendTCvSubst a v $ TyVarTy t) emptyTCvSubst
+            $ zip vs vs'
+   in (vs', substTy subst t)
+
+
+cloneTyVar :: TyVar -> TyVar
+cloneTyVar t =
+  let uniq = getUnique t
+      some_magic_number = 49
+   in setVarUnique t $ deriveUnique uniq some_magic_number
+
+
+------------------------------------------------------------------------------
+-- | Is this a function type?
+isFunction :: Type -> Bool
+isFunction (tcSplitFunTys -> ((_:_), _)) = True
+isFunction _ = False
+
+------------------------------------------------------------------------------
+-- | Is this an algebraic type?
+algebraicTyCon :: Type -> Maybe TyCon
+algebraicTyCon (splitTyConApp_maybe -> Just (tycon, _))
+  | tycon == intTyCon    = Nothing
+  | tycon == floatTyCon  = Nothing
+  | tycon == doubleTyCon = Nothing
+  | tycon == charTyCon   = Nothing
+  | tycon == funTyCon    = Nothing
+  | otherwise = Just tycon
+algebraicTyCon _ = Nothing
+
+------------------------------------------------------------------------------
+-- | Can ths type be lambda-cased?
+--
+-- Return: 'Nothing' if no
+--         @Just False@ if it can't be homomorphic
+--         @Just True@ if it can
+lambdaCaseable :: Type -> Maybe Bool
+lambdaCaseable (splitFunTy_maybe -> Just (arg, res))
+  | isJust (algebraicTyCon arg)
+  = Just $ isJust $ algebraicTyCon res
+lambdaCaseable _ = Nothing
+
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
new file mode 100644
index 0000000000..51c1cef988
--- /dev/null
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
@@ -0,0 +1,89 @@
+{-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE ViewPatterns    #-}
+
+module Ide.Plugin.Tactic.Judgements where
+
+import           Data.Char
+import           Data.Coerce
+import           Data.Map (Map)
+import qualified Data.Map as M
+import           Data.Maybe
+import qualified Data.Set as S
+import           Development.IDE.Spans.LocalBindings
+import           Ide.Plugin.Tactic.Types
+import           OccName
+import           SrcLoc
+import           Type
+
+
+------------------------------------------------------------------------------
+-- | Given a 'SrcSpan' and a 'Bindings', create a hypothesis.
+hypothesisFromBindings :: RealSrcSpan -> Bindings -> Map OccName CType
+hypothesisFromBindings span bs = buildHypothesis $ getLocalScope bs span
+
+------------------------------------------------------------------------------
+-- | Convert a @Set Id@ into a hypothesis.
+buildHypothesis :: [(Name, Maybe Type)] -> Map OccName CType
+buildHypothesis
+  = M.fromList
+  . mapMaybe go
+  where
+    go (occName -> occ, t)
+      | Just ty <- t
+      , isAlpha . head . occNameString $ occ = Just (occ, CType ty)
+      | otherwise = Nothing
+
+
+hasDestructed :: Judgement -> OccName -> Bool
+hasDestructed j n = S.member n $ _jDestructed j
+
+destructing :: OccName -> Judgement -> Judgement
+destructing n jdg@Judgement{..} = jdg
+  { _jDestructed = _jDestructed <> S.singleton n
+  }
+
+withNewGoal :: a -> Judgement' a -> Judgement' a
+withNewGoal t jdg = jdg
+  { _jGoal = t
+  }
+
+introducing :: [(OccName, a)] -> Judgement' a -> Judgement' a
+introducing ns jdg@Judgement{..} = jdg
+  { _jHypothesis = M.fromList ns <> _jHypothesis
+  }
+
+------------------------------------------------------------------------------
+-- | Pattern vals are currently tracked in jHypothesis, with an extra piece of data sitting around in jPatternVals.
+introducingPat :: [(OccName, a)] -> Judgement' a -> Judgement' a
+introducingPat ns jdg@Judgement{..} = jdg
+  { _jHypothesis  = M.fromList ns <> _jHypothesis
+  , _jPatternVals = S.fromList (fmap fst ns) <> _jPatternVals
+  }
+
+
+disallowing :: [OccName] -> Judgement' a -> Judgement' a
+disallowing ns jdg@Judgement{..} = jdg
+  { _jHypothesis = M.withoutKeys _jHypothesis $ S.fromList ns
+  }
+
+jHypothesis :: Judgement' a -> Map OccName a
+jHypothesis = _jHypothesis
+
+
+------------------------------------------------------------------------------
+-- | Only the hypothesis members which are pattern vals
+jPatHypothesis :: Judgement' a -> Map OccName a
+jPatHypothesis jdg
+  = M.restrictKeys (jHypothesis jdg) $ _jPatternVals jdg
+
+
+jGoal :: Judgement' a -> a
+jGoal = _jGoal
+
+
+substJdg :: TCvSubst -> Judgement -> Judgement
+substJdg subst = fmap $ coerce . substTy subst . coerce
+
+mkFirstJudgement :: M.Map OccName CType -> Type -> Judgement' CType
+mkFirstJudgement hy = Judgement hy mempty mempty . CType
+
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
new file mode 100644
index 0000000000..65885324c0
--- /dev/null
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
@@ -0,0 +1,144 @@
+{-# LANGUAGE DeriveFunctor         #-}
+{-# LANGUAGE DeriveGeneric         #-}
+{-# LANGUAGE DerivingStrategies    #-}
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE LambdaCase            #-}
+{-# LANGUAGE MonoLocalBinds        #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE RecordWildCards       #-}
+{-# LANGUAGE TypeSynonymInstances  #-}
+{-# LANGUAGE ViewPatterns          #-}
+{-# LANGUAGE ViewPatterns          #-}
+{-# OPTIONS_GHC -fno-warn-orphans  #-}
+
+module Ide.Plugin.Tactic.Machinery
+  ( module Ide.Plugin.Tactic.Machinery
+  ) where
+
+import           Control.Applicative
+import           Control.Monad.Except (throwError)
+import           Control.Monad.Reader
+import           Control.Monad.State (gets, modify)
+import           Data.Coerce
+import           Data.Either
+import           Data.List (intercalate, sortBy)
+import           Data.Ord (comparing, Down(..))
+import qualified Data.Set as S
+import           Development.IDE.GHC.Compat
+import           Ide.Plugin.Tactic.Judgements
+import           Ide.Plugin.Tactic.Types
+import           Refinery.ProofState
+import           Refinery.Tactic
+import           Refinery.Tactic.Internal
+import           TcType
+import           Type
+import           Unify
+
+
+substCTy :: TCvSubst -> CType -> CType
+substCTy subst = coerce . substTy subst . coerce
+
+
+------------------------------------------------------------------------------
+-- | Produce a subgoal that must be solved before we can solve the original
+-- goal.
+newSubgoal
+    :: Judgement
+    -> RuleM (LHsExpr GhcPs)
+newSubgoal j = do
+    unifier <- gets ts_unifier
+    subgoal $ substJdg unifier j
+
+
+------------------------------------------------------------------------------
+-- | Attempt to generate a term of the right type using in-scope bindings, and
+-- a given tactic.
+runTactic
+    :: Context
+    -> Judgement
+    -> TacticsM ()       -- ^ Tactic to use
+    -> Either [TacticError] (LHsExpr GhcPs)
+runTactic ctx jdg t =
+    let skolems = tyCoVarsOfTypeWellScoped $ unCType $ jGoal jdg
+        tacticState = mempty { ts_skolems = skolems }
+    in case partitionEithers
+          . flip runReader ctx
+          . unExtractM
+          $ runTacticTWithState t jdg tacticState of
+      (errs, []) -> Left $ errs
+      (_, solns) -> do
+        -- TODO(sandy): remove this trace sometime
+        traceM $ intercalate "\n" $ fmap (unsafeRender . fst) $ solns
+        case sortBy (comparing $ Down . uncurry scoreSolution . snd) solns of
+          (res : _) -> Right $ fst res
+          -- guaranteed to not be empty
+          _ -> Left []
+
+
+scoreSolution :: TacticState -> [Judgement] -> Int
+scoreSolution TacticState{..} holes
+  -- TODO(sandy): should this be linear?
+  = S.size ts_used_vals - length holes * 5
+
+
+runTacticTWithState
+    :: (MonadExtract ext m)
+    => TacticT jdg ext err s m ()
+    -> jdg
+    -> s
+    -> m [Either err (ext, (s, [jdg]))]
+runTacticTWithState t j s = proofs' s $ fmap snd $ proofState t j
+
+
+proofs'
+    :: (MonadExtract ext m)
+    => s
+    -> ProofStateT ext ext err s m goal
+    -> m [(Either err (ext, (s, [goal])))]
+proofs' s p = go s [] p
+    where
+      go s goals (Subgoal goal k) = do
+         h <- hole
+         (go s (goals ++ [goal]) $ k h)
+      go s goals (Effect m) = go s goals =<< m
+      go s goals (Stateful f) =
+          let (s', p) = f s
+          in go s' goals p
+      go s goals (Alt p1 p2) = liftA2 (<>) (go s goals p1) (go s goals p2)
+      go s goals (Interleave p1 p2) = liftA2 (interleave) (go s goals p1) (go s goals p2)
+      go _ _ Empty = pure []
+      go _ _ (Failure err) = pure [throwError err]
+      go s goals (Axiom ext) = pure [Right (ext, (s, goals))]
+
+
+------------------------------------------------------------------------------
+-- | We need to make sure that we don't try to unify any skolems.
+-- To see why, consider the case:
+--
+-- uhh :: (Int -> Int) -> a
+-- uhh f = _
+--
+-- If we were to apply 'f', then we would try to unify 'Int' and 'a'.
+-- This is fine from the perspective of 'tcUnifyTy', but will cause obvious
+-- type errors in our use case. Therefore, we need to ensure that our
+-- 'TCvSubst' doesn't try to unify skolems.
+checkSkolemUnification :: CType -> CType -> TCvSubst -> RuleM ()
+checkSkolemUnification t1 t2 subst = do
+    skolems <- gets ts_skolems
+    unless (all (flip notElemTCvSubst subst) skolems) $
+      throwError (UnificationError t1 t2)
+
+
+------------------------------------------------------------------------------
+-- | Attempt to unify two types.
+unify :: CType -- ^ The goal type
+      -> CType -- ^ The type we are trying unify the goal type with
+      -> RuleM ()
+unify goal inst =
+    case tcUnifyTy (unCType inst) (unCType goal) of
+      Just subst -> do
+          checkSkolemUnification inst goal subst
+          modify (\s -> s { ts_unifier = unionTCvSubst subst (ts_unifier s) })
+      Nothing -> throwError (UnificationError inst goal)
+
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Naming.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Naming.hs
new file mode 100644
index 0000000000..5426701106
--- /dev/null
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Naming.hs
@@ -0,0 +1,93 @@
+{-# LANGUAGE ViewPatterns #-}
+
+module Ide.Plugin.Tactic.Naming where
+
+import           Control.Monad.State.Strict
+import           Data.Bool (bool)
+import           Data.Char
+import           Data.Map (Map)
+import qualified Data.Map as M
+import           Data.Traversable
+import           Name
+import           TcType
+import           TyCon
+import           Type
+import           TysWiredIn (listTyCon, pairTyCon, unitTyCon)
+
+
+------------------------------------------------------------------------------
+-- | Use type information to create a reasonable name.
+mkTyName :: Type -> String
+-- eg. mkTyName (a -> B) = "fab"
+mkTyName (tcSplitFunTys -> ([a@(isFunTy -> False)], b))
+  = "f" ++ mkTyName a ++ mkTyName b
+-- eg. mkTyName (a -> b -> C) = "f_C"
+mkTyName (tcSplitFunTys -> ((_:_), b))
+  = "f_" ++ mkTyName b
+-- eg. mkTyName (Either A B) = "eab"
+mkTyName (splitTyConApp_maybe -> Just (c, args))
+  = mkTyConName c ++ foldMap mkTyName args
+-- eg. mkTyName a = "a"
+mkTyName (getTyVar_maybe -> Just tv)
+  = occNameString $ occName tv
+-- eg. mkTyName (forall x. y) = "y"
+mkTyName (tcSplitSigmaTy -> ((_:_), _, t))
+  = mkTyName t
+mkTyName _ = "x"
+
+
+------------------------------------------------------------------------------
+-- | Get a good name for a type constructor.
+mkTyConName :: TyCon -> String
+mkTyConName tc
+  | tc == listTyCon = "l_"
+  | tc == pairTyCon = "p_"
+  | tc == unitTyCon = "unit"
+  | otherwise
+      = take 1
+      . fmap toLower
+      . filterReplace isSymbol      's'
+      . filterReplace isPunctuation 'p'
+      . occNameString
+      $ getOccName tc
+
+
+------------------------------------------------------------------------------
+-- | Maybe replace an element in the list if the predicate matches
+filterReplace :: (a -> Bool) -> a -> [a] -> [a]
+filterReplace f r = fmap (\a -> bool a r $ f a)
+
+
+------------------------------------------------------------------------------
+-- | Produce a unique, good name for a type.
+mkGoodName
+    :: [OccName]  -- ^ Bindings in scope; used to ensure we don't shadow anything
+    -> Type       -- ^ The type to produce a name for
+    -> OccName
+mkGoodName in_scope t =
+  let tn = mkTyName t
+   in mkVarOcc $ case elem (mkVarOcc tn) in_scope of
+        True -> tn ++ show (length in_scope)
+        False -> tn
+
+
+------------------------------------------------------------------------------
+-- | Like 'mkGoodName' but creates several apart names.
+mkManyGoodNames
+  :: (Traversable t, Monad m)
+  => M.Map OccName a
+  -> t Type
+  -> m (t OccName)
+mkManyGoodNames hy args =
+  flip evalStateT (getInScope hy) $ for args $ \at -> do
+    in_scope <- get
+    let n = mkGoodName in_scope at
+    modify (n :)
+    pure n
+
+
+------------------------------------------------------------------------------
+-- | Which names are in scope?
+getInScope :: Map OccName a -> [OccName]
+getInScope = M.keys
+
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Range.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Range.hs
new file mode 100644
index 0000000000..9bf5c17d54
--- /dev/null
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Range.hs
@@ -0,0 +1,18 @@
+module Ide.Plugin.Tactic.Range where
+
+import qualified FastString as FS
+import           Development.IDE.Types.Location
+import           SrcLoc
+
+------------------------------------------------------------------------------
+-- | Convert a DAML compiler Range to a GHC SrcSpan
+-- TODO(sandy): this doesn't belong here
+rangeToSrcSpan :: String -> Range -> SrcSpan
+rangeToSrcSpan file range = RealSrcSpan $ rangeToRealSrcSpan file range
+
+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))
+
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
new file mode 100644
index 0000000000..89cb181275
--- /dev/null
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -0,0 +1,228 @@
+{-# LANGUAGE DeriveGeneric         #-}
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeSynonymInstances  #-}
+{-# LANGUAGE ViewPatterns          #-}
+
+module Ide.Plugin.Tactic.Tactics
+  ( module Ide.Plugin.Tactic.Tactics
+  , runTactic
+  ) where
+
+import           Control.Applicative
+import           Control.Monad.Except (throwError)
+import           Control.Monad.State.Class
+import           Control.Monad.State.Strict (StateT(..), runStateT)
+import           Data.Function
+import           Data.List
+import qualified Data.Map as M
+import           Data.Maybe
+import qualified Data.Set as S
+import           Development.IDE.GHC.Compat
+import           GHC.Exts
+import           GHC.SourceGen.Expr
+import           GHC.SourceGen.Overloaded
+import           Ide.Plugin.Tactic.CodeGen
+import           Ide.Plugin.Tactic.Context
+import           Ide.Plugin.Tactic.GHC
+import           Ide.Plugin.Tactic.Judgements
+import           Ide.Plugin.Tactic.Machinery
+import           Ide.Plugin.Tactic.Naming
+import           Ide.Plugin.Tactic.Types
+import           Refinery.Tactic
+import           Refinery.Tactic.Internal
+import           TcType
+import           Type hiding (Var)
+
+
+
+------------------------------------------------------------------------------
+-- | Use something in the hypothesis to fill the hole.
+-- TODO(sandy): deprecate this
+assumption :: TacticsM ()
+assumption = rule $ \jdg -> do
+  let hy = jHypothesis jdg
+      g  = jGoal jdg
+  case find ((== g) . snd) $ toList hy of
+    Just (v, _) -> pure $ noLoc $ var' v
+    Nothing -> throwError $ GoalMismatch "assumption" g
+
+
+------------------------------------------------------------------------------
+-- | Use something named in the hypothesis to fill the hole.
+assume :: OccName -> TacticsM ()
+assume name = rule $ \jdg -> do
+  let g  = jGoal jdg
+  case M.lookup name $ jHypothesis jdg of
+    Just ty ->
+      case ty == jGoal jdg of
+        True  -> do
+          useOccName jdg name
+          pure $ noLoc $ var' name
+        False -> throwError $ GoalMismatch "assume" g
+    Nothing -> throwError $ UndefinedHypothesis name
+
+
+useOccName :: MonadState TacticState m => Judgement -> OccName -> m ()
+useOccName jdg name =
+  case M.lookup name $ jHypothesis jdg of
+    Just{}  -> modify $ withUsedVals $ S.insert name
+    Nothing -> pure ()
+
+
+------------------------------------------------------------------------------
+-- | Introduce a lambda.
+intro :: TacticsM ()
+intro = rule $ \jdg -> do
+  let hy = jHypothesis jdg
+      g  = jGoal jdg
+  case splitFunTy_maybe $ unCType g of
+    Just (a, b) -> do
+      v <- pure $ mkGoodName (getInScope hy) a
+      let jdg' = introducing [(v, CType a)] $ withNewGoal (CType b) jdg
+      sg <- newSubgoal jdg'
+      pure $ noLoc $ lambda [bvar' v] $ unLoc sg
+    _ -> throwError $ GoalMismatch "intro" g
+
+
+------------------------------------------------------------------------------
+-- | Introduce a lambda binding every variable.
+intros :: TacticsM ()
+intros = rule $ \jdg -> do
+  let hy = jHypothesis jdg
+      g  = jGoal jdg
+  case tcSplitFunTys $ unCType g of
+    ([], _) -> throwError $ GoalMismatch "intro" g
+    (as, b) -> do
+      vs <- mkManyGoodNames hy as
+      let jdg' = introducing (zip vs $ coerce as) $ withNewGoal (CType b) jdg
+      sg <- newSubgoal jdg'
+      pure
+        . noLoc
+        . lambda (fmap bvar' vs)
+        $ unLoc sg
+
+
+------------------------------------------------------------------------------
+-- | Case split, and leave holes in the matches.
+destruct :: OccName -> TacticsM ()
+destruct name = do
+  jdg <- goal
+  case hasDestructed jdg name of
+    True -> throwError $ AlreadyDestructed name
+    False -> rule $ \jdg -> destruct' (const subgoal) name jdg
+
+
+------------------------------------------------------------------------------
+-- | Case split, using the same data constructor in the matches.
+homo :: OccName -> TacticsM ()
+homo = rule . destruct' (\dc jdg ->
+  buildDataCon jdg dc $ snd $ splitAppTys $ unCType $ jGoal jdg)
+
+
+------------------------------------------------------------------------------
+-- | LambdaCase split, and leave holes in the matches.
+destructLambdaCase :: TacticsM ()
+destructLambdaCase = rule $ destructLambdaCase' (const subgoal)
+
+
+------------------------------------------------------------------------------
+-- | LambdaCase split, using the same data constructor in the matches.
+homoLambdaCase :: TacticsM ()
+homoLambdaCase = rule $ destructLambdaCase' (\dc jdg ->
+  buildDataCon jdg dc $ snd $ splitAppTys $ unCType $ jGoal jdg)
+
+
+apply' :: OccName -> TacticsM ()
+apply' func = rule $ \jdg -> do
+  let hy = jHypothesis jdg
+      g  = jGoal jdg
+  case M.lookup func hy of
+    Just (CType ty) -> do
+        let (args, ret) = splitFunTys ty
+        unify g (CType ret)
+        sgs <- traverse (newSubgoal . flip withNewGoal jdg . CType) args
+        pure . noLoc
+             . foldl' (@@) (var' func)
+             $ fmap unLoc sgs
+    Nothing -> throwError $ GoalMismatch "apply" g
+
+
+------------------------------------------------------------------------------
+-- | Choose between each of the goal's data constructors.
+split :: TacticsM ()
+split = do
+  jdg <- goal
+  let g = jGoal jdg
+  case splitTyConApp_maybe $ unCType g of
+    Nothing -> throwError $ GoalMismatch "getGoalTyCon" g
+    Just (tc, _) -> do
+      let dcs = tyConDataCons tc
+      choice $ fmap splitDataCon dcs
+
+
+------------------------------------------------------------------------------
+-- | Attempt to instantiate the given data constructor to solve the goal.
+splitDataCon :: DataCon -> TacticsM ()
+splitDataCon dc = rule $ \jdg -> do
+  let g = jGoal jdg
+  case splitTyConApp_maybe $ unCType g of
+    Just (tc, apps) -> do
+      case elem dc $ tyConDataCons tc of
+        True -> buildDataCon jdg dc apps
+        False -> throwError $ IncorrectDataCon dc
+    Nothing -> throwError $ GoalMismatch "splitDataCon" g
+
+
+------------------------------------------------------------------------------
+-- | @matching f@ takes a function from a judgement to a @Tactic@, and
+-- then applies the resulting @Tactic@.
+matching :: (Judgement -> TacticsM ()) -> TacticsM ()
+matching f = TacticT $ StateT $ \s -> runStateT (unTacticT $ f s) s
+
+
+attemptOn :: (Judgement -> [a]) -> (a -> TacticsM ()) -> TacticsM ()
+attemptOn getNames tac = matching (choice . fmap (\s -> tac s) . getNames)
+
+
+------------------------------------------------------------------------------
+-- | Automatically solve a goal.
+auto :: TacticsM ()
+auto = do
+  current <- getCurrentDefinitions
+  TacticT $ StateT $ \jdg ->
+    runStateT (unTacticT $ auto' 5) $ disallowing current jdg
+
+auto' :: Int -> TacticsM ()
+auto' 0 = throwError NoProgress
+auto' n = do
+  let loop = auto' (n - 1)
+  intros <|> many_ intro
+  choice
+    [ attemptOn functionNames $ \fname -> do
+        apply' fname
+        loop
+    , attemptOn algebraicNames $ \aname -> do
+        progress ((==) `on` jGoal) NoProgress (destruct aname)
+        loop
+    , split >> loop
+    , attemptOn allNames $ \name -> do
+        assume name
+        loop
+    ]
+
+
+functionNames :: Judgement -> [OccName]
+functionNames  =
+  M.keys . M.filter (isFunction . unCType) . jHypothesis
+
+
+algebraicNames :: Judgement -> [OccName]
+algebraicNames =
+  M.keys . M.filter (isJust . algebraicTyCon . unCType) . jHypothesis
+
+
+allNames :: Judgement -> [OccName]
+allNames = M.keys . jHypothesis
+
diff --git a/plugins/default/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/TestTypes.hs
similarity index 72%
rename from plugins/default/src/Ide/Plugin/Tactic/Types.hs
rename to plugins/tactics/src/Ide/Plugin/Tactic/TestTypes.hs
index 5d0ae4042c..2ea4b8d06c 100644
--- a/plugins/default/src/Ide/Plugin/Tactic/Types.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/TestTypes.hs
@@ -1,8 +1,6 @@
 {-# LANGUAGE OverloadedStrings #-}
-module Ide.Plugin.Tactic.Types
-  ( tacticTitle
-  , TacticCommand (..)
-  ) where
+
+module Ide.Plugin.Tactic.TestTypes where
 
 import qualified Data.Text as T
 
@@ -12,18 +10,18 @@ import qualified Data.Text as T
 -- editor via 'commandProvider'.
 data TacticCommand
   = Auto
-  | Split
-  | Intro
   | Intros
   | Destruct
   | Homomorphism
+  | DestructLambdaCase
+  | HomomorphismLambdaCase
   deriving (Eq, Ord, Show, Enum, Bounded)
 
 -- | Generate a title for the command.
 tacticTitle :: TacticCommand -> T.Text -> T.Text
-tacticTitle Auto _ = "Auto"
-tacticTitle Split _ = "Auto"
-tacticTitle Intro _ = "Intro"
+tacticTitle Auto _ = "Attempt to fill hole"
 tacticTitle Intros _ = "Introduce lambda"
 tacticTitle Destruct var = "Case split on " <> var
 tacticTitle Homomorphism var = "Homomorphic case split on " <> var
+tacticTitle DestructLambdaCase _ = "Lambda case split"
+tacticTitle HomomorphismLambdaCase _ = "Homomorphic lambda case split"
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
new file mode 100644
index 0000000000..291d732fad
--- /dev/null
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
@@ -0,0 +1,149 @@
+{-# LANGUAGE DeriveFunctor                  #-}
+{-# LANGUAGE DeriveGeneric                  #-}
+{-# LANGUAGE DerivingStrategies             #-}
+{-# LANGUAGE FlexibleInstances              #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving     #-}
+{-# LANGUAGE MultiParamTypeClasses          #-}
+{-# LANGUAGE TypeSynonymInstances           #-}
+
+module Ide.Plugin.Tactic.Types
+  ( module Ide.Plugin.Tactic.Types
+  , module Ide.Plugin.Tactic.Debug
+  , OccName
+  , Name
+  , Type
+  , TyVar
+  , Span
+  , Range
+  ) where
+
+import Control.Monad.Reader
+import Data.Function
+import Data.Map (Map)
+import Data.Set (Set)
+import Development.IDE.GHC.Compat
+import Development.IDE.Types.Location
+import GHC.Generics
+import Ide.Plugin.Tactic.Debug
+import OccName
+import Refinery.Tactic
+import Type
+
+
+------------------------------------------------------------------------------
+-- | A wrapper around 'Type' which supports equality and ordering.
+newtype CType = CType { unCType :: Type }
+
+instance Eq CType where
+  (==) = eqType `on` unCType
+
+instance Ord CType where
+  compare = nonDetCmpType `on` unCType
+
+
+------------------------------------------------------------------------------
+data TacticState = TacticState
+    { ts_skolems   :: !([TyVar])
+    , ts_unifier   :: !(TCvSubst)
+    , ts_used_vals :: !(Set OccName)
+    }
+
+instance Semigroup TacticState where
+  TacticState a1 b1 c1 <> TacticState a2 b2 c2
+    = TacticState
+        (a1 <> a2)
+        (unionTCvSubst b1 b2)
+        (c1 <> c2)
+
+instance Monoid TacticState where
+  mempty = TacticState mempty emptyTCvSubst mempty
+
+
+withUsedVals :: (Set OccName -> Set OccName) -> TacticState -> TacticState
+withUsedVals f ts = ts
+  { ts_used_vals = f $ ts_used_vals ts
+  }
+
+
+------------------------------------------------------------------------------
+-- | The current bindings and goal for a hole to be filled by refinery.
+data Judgement' a = Judgement
+  { _jHypothesis  :: !(Map OccName a)
+  , _jDestructed  :: !(Set OccName)
+    -- ^ These should align with keys of _jHypothesis
+  , _jPatternVals :: !(Set OccName)
+    -- ^ These should align with keys of _jHypothesis
+  , _jGoal        :: !(a)
+  }
+  deriving stock (Eq, Ord, Generic, Functor)
+
+type Judgement = Judgement' CType
+
+
+newtype ExtractM a = ExtractM { unExtractM :: Reader Context a }
+    deriving (Functor, Applicative, Monad, MonadReader Context)
+
+------------------------------------------------------------------------------
+-- | Orphan instance for producing holes when attempting to solve tactics.
+instance MonadExtract (LHsExpr GhcPs) ExtractM where
+  hole = pure $ noLoc $ HsVar noExtField $ noLoc $ Unqual $ mkVarOcc "_"
+
+
+------------------------------------------------------------------------------
+-- | Reasons a tactic might fail.
+data TacticError
+  = UndefinedHypothesis OccName
+  | GoalMismatch String CType
+  | UnsolvedSubgoals [Judgement]
+  | UnificationError CType CType
+  | NoProgress
+  | NoApplicableTactic
+  | AlreadyDestructed OccName
+  | IncorrectDataCon DataCon
+  deriving stock (Eq)
+
+instance Show TacticError where
+    show (UndefinedHypothesis name) =
+      occNameString name <> " is not available in the hypothesis."
+    show (GoalMismatch tac (CType typ)) =
+      mconcat
+        [ "The tactic "
+        , tac
+        , " doesn't apply to goal type "
+        , unsafeRender typ
+        ]
+    show (UnsolvedSubgoals _) =
+      "There were unsolved subgoals"
+    show (UnificationError (CType t1) (CType t2)) =
+        mconcat
+          [ "Could not unify "
+          , unsafeRender t1
+          , " and "
+          , unsafeRender t2
+          ]
+    show NoProgress =
+      "Unable to make progress"
+    show NoApplicableTactic =
+      "No tactic could be applied"
+    show (AlreadyDestructed name) =
+      "Already destructed " <> unsafeRender name
+    show (IncorrectDataCon dcon) =
+      "Data con doesn't align with goal type (" <> unsafeRender dcon <> ")"
+
+
+------------------------------------------------------------------------------
+type TacticsM  = TacticT Judgement (LHsExpr GhcPs) TacticError TacticState ExtractM
+type RuleM     = RuleT Judgement (LHsExpr GhcPs) TacticError TacticState ExtractM
+type Rule      = RuleM (LHsExpr GhcPs)
+
+
+------------------------------------------------------------------------------
+-- | The Reader context of tactics and rules
+data Context = Context
+  { ctxDefiningFuncs :: [(OccName, CType)]
+    -- ^ The functions currently being defined
+  , ctxModuleFuncs :: [(OccName, CType)]
+    -- ^ Everything defined in the current module
+  }
+  deriving stock (Eq, Ord)
+
diff --git a/plugins/default/src/Ide/TreeTransform.hs b/plugins/tactics/src/Ide/TreeTransform.hs
similarity index 99%
rename from plugins/default/src/Ide/TreeTransform.hs
rename to plugins/tactics/src/Ide/TreeTransform.hs
index 996c552c43..012426de68 100644
--- a/plugins/default/src/Ide/TreeTransform.hs
+++ b/plugins/tactics/src/Ide/TreeTransform.hs
@@ -26,7 +26,6 @@ import           Language.Haskell.LSP.Types
 import           Language.Haskell.LSP.Types.Capabilities (ClientCapabilities)
 import           Outputable
 import           Retrie.ExactPrint hiding (parseExpr)
-import           Text.Regex.TDFA.Text()
 
 
 ------------------------------------------------------------------------------
diff --git a/stack-8.10.1.yaml b/stack-8.10.1.yaml
index 1fe0cba806..d198452493 100644
--- a/stack-8.10.1.yaml
+++ b/stack-8.10.1.yaml
@@ -20,7 +20,7 @@ extra-deps:
 - HsYAML-aeson-0.2.0.0@rev:2
 - monad-dijkstra-0.1.1.2
 - opentelemetry-0.4.2
-- refinery-0.1.0.0
+- refinery-0.2.0.0
 - retrie-0.1.1.1
 - stylish-haskell-0.11.0.3
 - semigroups-0.18.5
diff --git a/stack-8.10.2.yaml b/stack-8.10.2.yaml
index ea835fd350..a917a40fe9 100644
--- a/stack-8.10.2.yaml
+++ b/stack-8.10.2.yaml
@@ -21,7 +21,7 @@ extra-deps:
 - HsYAML-aeson-0.2.0.0@rev:2
 - monad-dijkstra-0.1.1.2
 - opentelemetry-0.4.2
-- refinery-0.1.0.0
+- refinery-0.2.0.0
 - retrie-0.1.1.1
 - stylish-haskell-0.11.0.3
 - semigroups-0.18.5
diff --git a/stack-8.6.4.yaml b/stack-8.6.4.yaml
index edd214620a..116d7619c0 100644
--- a/stack-8.6.4.yaml
+++ b/stack-8.6.4.yaml
@@ -46,7 +46,7 @@ extra-deps:
 - ormolu-0.1.2.0
 - parser-combinators-1.2.1
 - primitive-0.7.1.0
-- refinery-0.1.0.0
+- refinery-0.2.0.0
 - regex-base-0.94.0.0
 - regex-pcre-builtin-0.95.1.1.8.43
 - regex-tdfa-1.3.1.0
diff --git a/stack-8.6.5.yaml b/stack-8.6.5.yaml
index 1092a77489..65e1e14ee4 100644
--- a/stack-8.6.5.yaml
+++ b/stack-8.6.5.yaml
@@ -45,7 +45,7 @@ extra-deps:
 - ormolu-0.1.2.0
 - parser-combinators-1.2.1
 - primitive-0.7.1.0
-- refinery-0.1.0.0
+- refinery-0.2.0.0
 - regex-base-0.94.0.0
 - regex-pcre-builtin-0.95.1.1.8.43
 - regex-tdfa-1.3.1.0
diff --git a/stack-8.8.2.yaml b/stack-8.8.2.yaml
index 6c71cdfd59..2b2308268d 100644
--- a/stack-8.8.2.yaml
+++ b/stack-8.8.2.yaml
@@ -38,7 +38,7 @@ extra-deps:
 - monad-dijkstra-0.1.1.2
 - opentelemetry-0.4.2
 - ormolu-0.1.2.0
-- refinery-0.1.0.0
+- refinery-0.2.0.0
 - retrie-0.1.1.1
 - semigroups-0.18.5
 # - github: wz1000/shake
diff --git a/stack-8.8.3.yaml b/stack-8.8.3.yaml
index c63e172e69..30a7c72bb3 100644
--- a/stack-8.8.3.yaml
+++ b/stack-8.8.3.yaml
@@ -29,7 +29,7 @@ extra-deps:
 - ilist-0.3.1.0
 - lsp-test-0.11.0.5
 - monad-dijkstra-0.1.1.2
-- refinery-0.1.0.0
+- refinery-0.2.0.0
 - retrie-0.1.1.1
 - semigroups-0.18.5
 # - github: wz1000/shake
diff --git a/stack-8.8.4.yaml b/stack-8.8.4.yaml
index 63fde601f3..10bc12c58d 100644
--- a/stack-8.8.4.yaml
+++ b/stack-8.8.4.yaml
@@ -32,7 +32,7 @@ extra-deps:
 - ilist-0.3.1.0
 - lsp-test-0.11.0.5
 - monad-dijkstra-0.1.1.2
-- refinery-0.1.0.0
+- refinery-0.2.0.0
 - retrie-0.1.1.1
 - semigroups-0.18.5
 - stylish-haskell-0.11.0.3
diff --git a/stack.yaml b/stack.yaml
index 1092a77489..65e1e14ee4 100644
--- a/stack.yaml
+++ b/stack.yaml
@@ -45,7 +45,7 @@ extra-deps:
 - ormolu-0.1.2.0
 - parser-combinators-1.2.1
 - primitive-0.7.1.0
-- refinery-0.1.0.0
+- refinery-0.2.0.0
 - regex-base-0.94.0.0
 - regex-pcre-builtin-0.95.1.1.8.43
 - regex-tdfa-1.3.1.0
diff --git a/test/functional/Tactic.hs b/test/functional/Tactic.hs
index 6045f09730..e770ad8a41 100644
--- a/test/functional/Tactic.hs
+++ b/test/functional/Tactic.hs
@@ -8,21 +8,22 @@ module Tactic
   )
 where
 
-import Data.Foldable
-import Data.Text (Text)
+import           Control.Applicative.Combinators ( skipManyTill )
+import           Control.Monad.IO.Class
+import           Data.Foldable
+import           Data.Maybe
+import           Data.Text (Text)
 import qualified Data.Text as T
-import           Control.Monad.IO.Class         ( MonadIO(liftIO) )
+import qualified Data.Text.IO as T
+import           Ide.Plugin.Tactic.TestTypes
 import           Language.Haskell.LSP.Test
-import           Language.Haskell.LSP.Types     ( Position(..)
-                                                , Range(..)
-                                                , CAResult(..)
-                                                , CodeAction(..)
-                                                )
+import           Language.Haskell.LSP.Types (ApplyWorkspaceEditRequest, Position(..) , Range(..) , CAResult(..) , CodeAction(..))
 import           Test.Hls.Util
 import           Test.Tasty
 import           Test.Tasty.HUnit
-import Data.Maybe (mapMaybe)
-import Ide.Plugin.Tactic.Types (tacticTitle, TacticCommand (..))
+import           System.FilePath
+import System.Directory (doesFileExist)
+import Control.Monad (unless)
 
 
 ------------------------------------------------------------------------------
@@ -68,6 +69,30 @@ tests = testGroup
       "T2.hs" 8 8
       [ (not, Intros, "")
       ]
+  , mkTest
+      "Produces (homomorphic) lambdacase code actions"
+      "T3.hs" 4 24
+      [ (id, HomomorphismLambdaCase, "")
+      , (id, DestructLambdaCase, "")
+      ]
+  , mkTest
+      "Produces lambdacase code actions"
+      "T3.hs" 7 13
+      [ (id, DestructLambdaCase, "")
+      ]
+  , mkTest
+      "Doesn't suggest lambdacase without -XLambdaCase"
+      "T2.hs" 11 25
+      [ (not, DestructLambdaCase, "")
+      ]
+  , goldenTest "GoldenIntros.hs"            2 8  Intros ""
+  , goldenTest "GoldenEitherAuto.hs"        2 11 Auto   ""
+  , goldenTest "GoldenJoinCont.hs"          4 12 Auto   ""
+  , goldenTest "GoldenIdentityFunctor.hs"   3 11 Auto   ""
+  , goldenTest "GoldenIdTypeFam.hs"         7 11 Auto   ""
+  , goldenTest "GoldenEitherHomomorphic.hs" 2 15 Auto ""
+  , goldenTest "GoldenNote.hs"              2 8  Auto ""
+  , goldenTest "GoldenPureList.hs"          2 12 Auto ""
   ]
 
 
@@ -96,6 +121,26 @@ mkTest name fp line col ts =
         f (elem title titles)
           @? ("Expected a code action with title " <> T.unpack title)
 
+
+goldenTest :: FilePath -> Int -> Int -> TacticCommand -> Text -> TestTree
+goldenTest input line col tc occ =
+  testCase (input <> " (golden)") $ do
+    runSession hieCommand fullCaps tacticPath $ do
+      doc <- openDoc input "haskell"
+      actions <- getCodeActions doc $ pointRange line col
+      Just (CACodeAction (CodeAction {_command = Just c}))
+        <- pure $ find ((== Just (tacticTitle tc occ)) . codeActionTitle) actions
+      executeCommand c
+      _resp :: ApplyWorkspaceEditRequest <- skipManyTill anyMessage message
+      edited <- documentContents doc
+      let expected_name = tacticPath </> input <.> "expected"
+      -- 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 @?= expected
+
+
 tacticPath :: FilePath
 tacticPath = "test/testdata/tactic"
 
diff --git a/test/testdata/tactic/GoldenEitherAuto.hs b/test/testdata/tactic/GoldenEitherAuto.hs
new file mode 100644
index 0000000000..eb34cd8209
--- /dev/null
+++ b/test/testdata/tactic/GoldenEitherAuto.hs
@@ -0,0 +1,2 @@
+either' :: (a -> c) -> (b -> c) -> Either a b -> c
+either' = _
diff --git a/test/testdata/tactic/GoldenEitherAuto.hs.expected b/test/testdata/tactic/GoldenEitherAuto.hs.expected
new file mode 100644
index 0000000000..10d633470c
--- /dev/null
+++ b/test/testdata/tactic/GoldenEitherAuto.hs.expected
@@ -0,0 +1,5 @@
+either' :: (a -> c) -> (b -> c) -> Either a b -> c
+either' = (\ fac fbc eab
+   -> case eab of
+        (Left a) -> fac a
+        (Right b) -> fbc b)
diff --git a/test/testdata/tactic/GoldenEitherHomomorphic.hs b/test/testdata/tactic/GoldenEitherHomomorphic.hs
new file mode 100644
index 0000000000..dee865d1a2
--- /dev/null
+++ b/test/testdata/tactic/GoldenEitherHomomorphic.hs
@@ -0,0 +1,2 @@
+eitherSplit :: a -> Either (a -> b) (a -> c) -> Either b c
+eitherSplit = _
diff --git a/test/testdata/tactic/GoldenEitherHomomorphic.hs.expected b/test/testdata/tactic/GoldenEitherHomomorphic.hs.expected
new file mode 100644
index 0000000000..8276908d71
--- /dev/null
+++ b/test/testdata/tactic/GoldenEitherHomomorphic.hs.expected
@@ -0,0 +1,5 @@
+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))
diff --git a/test/testdata/tactic/GoldenIdTypeFam.hs b/test/testdata/tactic/GoldenIdTypeFam.hs
new file mode 100644
index 0000000000..be8903fec0
--- /dev/null
+++ b/test/testdata/tactic/GoldenIdTypeFam.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE TypeFamilies #-}
+
+type family TyFam
+type instance TyFam = Int
+
+tyblah' :: TyFam -> Int
+tyblah' = _
diff --git a/test/testdata/tactic/GoldenIdTypeFam.hs.expected b/test/testdata/tactic/GoldenIdTypeFam.hs.expected
new file mode 100644
index 0000000000..ad5697334e
--- /dev/null
+++ b/test/testdata/tactic/GoldenIdTypeFam.hs.expected
@@ -0,0 +1,7 @@
+{-# LANGUAGE TypeFamilies #-}
+
+type family TyFam
+type instance TyFam = Int
+
+tyblah' :: TyFam -> Int
+tyblah' = (\ i -> i)
diff --git a/test/testdata/tactic/GoldenIdentityFunctor.hs b/test/testdata/tactic/GoldenIdentityFunctor.hs
new file mode 100644
index 0000000000..6d1de50992
--- /dev/null
+++ b/test/testdata/tactic/GoldenIdentityFunctor.hs
@@ -0,0 +1,3 @@
+data Ident a = Ident a
+instance Functor Ident where
+   fmap = _
diff --git a/test/testdata/tactic/GoldenIdentityFunctor.hs.expected b/test/testdata/tactic/GoldenIdentityFunctor.hs.expected
new file mode 100644
index 0000000000..fa0a8b629b
--- /dev/null
+++ b/test/testdata/tactic/GoldenIdentityFunctor.hs.expected
@@ -0,0 +1,3 @@
+data Ident a = Ident a
+instance Functor Ident where
+   fmap = (\ fab ia -> case ia of { (Ident a) -> Ident (fab a) })
diff --git a/test/testdata/tactic/GoldenIntros.hs b/test/testdata/tactic/GoldenIntros.hs
new file mode 100644
index 0000000000..5b4e6e241f
--- /dev/null
+++ b/test/testdata/tactic/GoldenIntros.hs
@@ -0,0 +1,2 @@
+blah :: Int -> Bool -> (a -> b) -> String -> Int
+blah = _
diff --git a/test/testdata/tactic/GoldenIntros.hs.expected b/test/testdata/tactic/GoldenIntros.hs.expected
new file mode 100644
index 0000000000..26d8599e4e
--- /dev/null
+++ b/test/testdata/tactic/GoldenIntros.hs.expected
@@ -0,0 +1,2 @@
+blah :: Int -> Bool -> (a -> b) -> String -> Int
+blah = (\ i b fab l_c -> _)
diff --git a/test/testdata/tactic/GoldenJoinCont.hs b/test/testdata/tactic/GoldenJoinCont.hs
new file mode 100644
index 0000000000..a0cdb05da6
--- /dev/null
+++ b/test/testdata/tactic/GoldenJoinCont.hs
@@ -0,0 +1,4 @@
+type Cont r a = ((a -> r) -> r)
+
+joinCont :: Show a => (a -> c) -> (b -> c) -> Either a b -> (c -> d) -> d
+joinCont = _
diff --git a/test/testdata/tactic/GoldenJoinCont.hs.expected b/test/testdata/tactic/GoldenJoinCont.hs.expected
new file mode 100644
index 0000000000..306591b32c
--- /dev/null
+++ b/test/testdata/tactic/GoldenJoinCont.hs.expected
@@ -0,0 +1,7 @@
+type Cont r a = ((a -> r) -> r)
+
+joinCont :: Show a => (a -> c) -> (b -> c) -> Either a b -> (c -> d) -> d
+joinCont = (\ fac fbc eab fcd
+   -> case eab of
+        (Left a) -> fcd (fac a)
+        (Right b) -> fcd (fbc b))
diff --git a/test/testdata/tactic/GoldenNote.hs b/test/testdata/tactic/GoldenNote.hs
new file mode 100644
index 0000000000..c9e0c820e4
--- /dev/null
+++ b/test/testdata/tactic/GoldenNote.hs
@@ -0,0 +1,2 @@
+note :: e -> Maybe a -> Either e a
+note = _
diff --git a/test/testdata/tactic/GoldenNote.hs.expected b/test/testdata/tactic/GoldenNote.hs.expected
new file mode 100644
index 0000000000..47a9bd6d92
--- /dev/null
+++ b/test/testdata/tactic/GoldenNote.hs.expected
@@ -0,0 +1,5 @@
+note :: e -> Maybe a -> Either e a
+note = (\ e ma
+   -> case ma of
+        Nothing -> Left e
+        (Just a) -> Right a)
diff --git a/test/testdata/tactic/GoldenPureList.hs b/test/testdata/tactic/GoldenPureList.hs
new file mode 100644
index 0000000000..3a3293b4ec
--- /dev/null
+++ b/test/testdata/tactic/GoldenPureList.hs
@@ -0,0 +1,2 @@
+pureList :: a -> [a]
+pureList = _
diff --git a/test/testdata/tactic/GoldenPureList.hs.expected b/test/testdata/tactic/GoldenPureList.hs.expected
new file mode 100644
index 0000000000..9410eea557
--- /dev/null
+++ b/test/testdata/tactic/GoldenPureList.hs.expected
@@ -0,0 +1,2 @@
+pureList :: a -> [a]
+pureList = (\ a -> (:) a [])
diff --git a/test/testdata/tactic/T2.hs b/test/testdata/tactic/T2.hs
index a81756abbb..20b1644a8f 100644
--- a/test/testdata/tactic/T2.hs
+++ b/test/testdata/tactic/T2.hs
@@ -7,3 +7,6 @@ global = True
 foo :: Int
 foo  = _
 
+dontSuggestLambdaCase :: Either a b -> Int
+dontSuggestLambdaCase = _
+
diff --git a/test/testdata/tactic/T3.hs b/test/testdata/tactic/T3.hs
new file mode 100644
index 0000000000..1bb42a9b02
--- /dev/null
+++ b/test/testdata/tactic/T3.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE LambdaCase #-}
+
+suggestHomomorphicLC :: Either a b -> Either a b
+suggestHomomorphicLC = _
+
+suggestLC :: Either a b -> Int
+suggestLC = _
+
diff --git a/test/testdata/tactic/hie.yaml b/test/testdata/tactic/hie.yaml
index c95f6c9a09..7aa4f9e0ad 100644
--- a/test/testdata/tactic/hie.yaml
+++ b/test/testdata/tactic/hie.yaml
@@ -1 +1 @@
-cradle: {direct: {arguments: ["T1", "T2"]}}
+cradle: {direct: {arguments: ["T1", "T2", "T3"]}}