diff --git a/cabal.project b/cabal.project
index 4d956fc5bd..5db0d1cd23 100644
--- a/cabal.project
+++ b/cabal.project
@@ -20,6 +20,6 @@ package ghcide
 
 write-ghc-environment-files: never
 
-index-state: 2020-09-09T00:00:00Z
+index-state: 2020-09-16T00:00:00Z
 
 allow-newer: data-tree-print:base
diff --git a/exe/Main.hs b/exe/Main.hs
index dfecd730ad..c6911722db 100644
--- a/exe/Main.hs
+++ b/exe/Main.hs
@@ -20,6 +20,7 @@ import Ide.Plugin.ImportLens              as ImportLens
 import Ide.Plugin.Ormolu                  as Ormolu
 import Ide.Plugin.StylishHaskell          as StylishHaskell
 import Ide.Plugin.Retrie                  as Retrie
+import Ide.Plugin.Tactic                  as Tactic
 #if AGPL
 import Ide.Plugin.Brittany                as Brittany
 #endif
@@ -45,6 +46,9 @@ idePlugins includeExamples = pluginDescToIdePlugins allPlugins
       , Pragmas.descriptor  "pragmas"
       , Floskell.descriptor "floskell"
       , Fourmolu.descriptor "fourmolu"
+      , Tactic.descriptor "tactic"
+      -- , genericDescriptor     "generic"
+      -- , ghcmodDescriptor      "ghcmod"
       , Ormolu.descriptor   "ormolu"
       , StylishHaskell.descriptor "stylish-haskell"
       , Retrie.descriptor "retrie"
diff --git a/ghcide b/ghcide
index 008d4db3ff..bfe35e60cc 160000
--- a/ghcide
+++ b/ghcide
@@ -1 +1 @@
-Subproject commit 008d4db3ff3a8a3635bf3ac709d0df593f456d0a
+Subproject commit bfe35e60cc5c5cf2a2bb73ca80d6b089c3ae5731
diff --git a/haskell-language-server.cabal b/haskell-language-server.cabal
index 8ead3a824c..46a48386ce 100644
--- a/haskell-language-server.cabal
+++ b/haskell-language-server.cabal
@@ -92,6 +92,11 @@ executable haskell-language-server
     Ide.Plugin.Pragmas
     Ide.Plugin.Retrie
     Ide.Plugin.StylishHaskell
+    Ide.Plugin.Tactic
+    Ide.Plugin.Tactic.Types
+    Ide.Plugin.Tactic.Machinery
+    Ide.Plugin.Tactic.Tactics
+    Ide.TreeTransform
 
   ghc-options:
     -threaded -Wall -Wno-name-shadowing -Wredundant-constraints
@@ -123,13 +128,27 @@ executable haskell-language-server
     , ormolu                   ^>=0.1.2
     , regex-tdfa
     , retrie                   >=0.1.1.0
+    , hslogger
+    , optparse-applicative
+    , haskell-lsp              ^>=0.22
+    , hls-plugin-api
+    , lens
+    , mtl
+    , ormolu                   ^>=0.1.2
+    , regex-tdfa
+    , retrie                   >=0.1.1.0
     , safe-exceptions
     , shake                    >=0.17.5
     , stylish-haskell          ^>=0.11
     , temporary
+    , text
+    , syb
     , time
     , transformers
     , unordered-containers
+    , ghc-source-gen
+    , refinery
+    , ghc-exactprint
 
   if flag(agpl)
     build-depends: brittany
@@ -218,7 +237,7 @@ test-suite func-test
     , tasty-golden
     , tasty-rerun
 
-  hs-source-dirs:     test/functional
+  hs-source-dirs:     test/functional plugins/default/src
   main-is:            Main.hs
   other-modules:
     Command
@@ -238,6 +257,8 @@ test-suite func-test
     Rename
     Symbol
     TypeDefinition
+    Tactic
+    Ide.Plugin.Tactic.Types
 
   ghc-options:
     -Wall -Wno-name-shadowing -threaded -rtsopts -with-rtsopts=-N
diff --git a/plugins/default/src/Ide/Plugin/Tactic.hs b/plugins/default/src/Ide/Plugin/Tactic.hs
new file mode 100644
index 0000000000..6629a29471
--- /dev/null
+++ b/plugins/default/src/Ide/Plugin/Tactic.hs
@@ -0,0 +1,269 @@
+{-# LANGUAGE DeriveAnyClass    #-}
+{-# LANGUAGE DeriveGeneric     #-}
+{-# LANGUAGE LambdaCase        #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE TupleSections     #-}
+{-# LANGUAGE TypeApplications  #-}
+{-# LANGUAGE ViewPatterns      #-}
+
+-- | A plugin that uses tactics to synthesize code
+module Ide.Plugin.Tactic
+  ( descriptor
+  , tacticTitle
+  , TacticCommand (..)
+  ) where
+
+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.Text as T
+import           Data.Traversable
+import           Development.IDE.Core.PositionMapping
+import           Development.IDE.Core.RuleTypes
+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.Shake (Action)
+import           GHC.Generics (Generic)
+import           HscTypes (hsc_dflags)
+import           Ide.Plugin (mkLspCommand)
+import           Ide.Plugin.Tactic.Machinery
+import           Ide.Plugin.Tactic.Tactics
+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
+descriptor plId = (defaultPluginDescriptor plId)
+    { pluginCommands
+        = fmap (\tc ->
+            PluginCommand
+              (tcCommandId tc)
+              (tacticDesc $ tcCommandName tc)
+              (tacticCmd $ commandTactic tc))
+              enabledTactics
+    , 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]
+
+
+------------------------------------------------------------------------------
+-- | Construct a 'CommandId'
+tcCommandId :: TacticCommand -> CommandId
+tcCommandId c = coerce $ T.pack $ "tactics" <> show c <> "Command"
+
+
+------------------------------------------------------------------------------
+-- | The name of the command for the LS.
+tcCommandName :: TacticCommand -> T.Text
+tcCommandName = T.pack . show
+
+------------------------------------------------------------------------------
+-- | Mapping from tactic commands to their contextual providers. See 'provide',
+-- '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 ""
+commandProvider Destruct =
+  filterBindingType destructFilter $ \occ _ ->
+    provide Destruct $ T.pack $ occNameString occ
+commandProvider Homomorphism =
+  filterBindingType homoFilter $ \occ _ ->
+    provide Homomorphism $ T.pack $ occNameString occ
+
+
+------------------------------------------------------------------------------
+-- | 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
+
+
+------------------------------------------------------------------------------
+-- | We should show homos only when the goal type is the same as the binding
+-- type, and that both are usual algebraic types.
+homoFilter :: Type -> Type -> Bool
+homoFilter (algebraicTyCon -> Just t1) (algebraicTyCon -> Just t2) = t1 == t2
+homoFilter _ _ = False
+
+
+------------------------------------------------------------------------------
+-- | We should show destruct for bindings only when those bindings have usual
+-- algebraic types.
+destructFilter :: Type -> Type -> Bool
+destructFilter _ (algebraicTyCon -> Just _) = True
+destructFilter _ _ = False
+
+
+runIde :: IdeState -> Action a -> IO a
+runIde state = runAction "tactic" state
+
+
+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
+        actions <- lift $
+          -- This foldMap is over the function monoid.
+          foldMap commandProvider enabledTactics
+            plId
+            uri
+            span
+            jdg
+        pure $ Right $ List actions
+codeActionProvider _ _ _ _ _ _ = pure $ Right $ codeActions []
+
+
+codeActions :: [CodeAction] -> List CAResult
+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
+  let title = tacticTitle tc name
+      params = TacticParams { file = uri , range = range , var_name = name }
+  cmd <- mkLspCommand plId (tcCommandId tc) title (Just [toJSON params])
+  pure
+    $ pure
+    $ CACodeAction
+    $ CodeAction title (Just CodeActionQuickFix) Nothing Nothing
+    $ Just cmd
+
+
+------------------------------------------------------------------------------
+-- | 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
+    False -> pure []
+
+
+------------------------------------------------------------------------------
+-- | Multiply a 'TacticProvider' for each binding, making sure it appears only
+-- when the given predicate holds over the goal and binding types.
+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 []
+
+
+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
+    }
+  deriving (Show, Eq, Generic, ToJSON, FromJSON)
+
+
+------------------------------------------------------------------------------
+-- | Find the last typechecked module, and find the most specific span, as well
+-- as the judgement at the given range.
+judgementForHole
+    :: IdeState
+    -> NormalizedFilePath
+    -> Range
+    -> IO (Maybe (PositionMapping, Range, Judgement))
+judgementForHole state nfp range = runMaybeT $ do
+  (asts, amapping) <- MaybeT $ runIde state $ useWithStale GetHieAst nfp
+  range' <- liftMaybe $ fromCurrentRange amapping range
+
+  (binds, _) <- MaybeT $ runIde state $ useWithStale GetBindings nfp
+
+  (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
+        Just ast' -> do
+          let info = nodeInfo ast'
+          ty <- listToMaybe $ nodeType info
+          guard $ ("HsUnboundVar","HsExpr") `S.member` nodeAnnotations info
+          pure (nodeSpan ast', ty)
+
+  resulting_range <- liftMaybe $ toCurrentRange amapping $ realSrcSpanToRange rss
+
+  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
+        pm <- MaybeT $ useAnnotatedSource "tacticsCmd" state nfp
+        case runTactic jdg
+              $ tac
+              $ mkVarOcc
+              $ T.unpack var_name of
+          Left err ->
+            pure $ (, Nothing)
+              $ 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
+            pure $ case response of
+               Right res -> (Right Null , Just (WorkspaceApplyEdit, ApplyWorkspaceEditParams res))
+               Left err -> (Left $ ResponseError InternalError (T.pack err) Nothing, Nothing)
+tacticCmd _ _ _ _ =
+  pure ( Left $ ResponseError InvalidRequest (T.pack "Bad URI") Nothing
+       , Nothing
+       )
+
+
+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
+
diff --git a/plugins/default/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/default/src/Ide/Plugin/Tactic/Machinery.hs
new file mode 100644
index 0000000000..51ef83e6cd
--- /dev/null
+++ b/plugins/default/src/Ide/Plugin/Tactic/Machinery.hs
@@ -0,0 +1,264 @@
+{-# 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
new file mode 100644
index 0000000000..a86e668568
--- /dev/null
+++ b/plugins/default/src/Ide/Plugin/Tactic/Tactics.hs
@@ -0,0 +1,180 @@
+{-# 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/Types.hs b/plugins/default/src/Ide/Plugin/Tactic/Types.hs
new file mode 100644
index 0000000000..5d0ae4042c
--- /dev/null
+++ b/plugins/default/src/Ide/Plugin/Tactic/Types.hs
@@ -0,0 +1,29 @@
+{-# LANGUAGE OverloadedStrings #-}
+module Ide.Plugin.Tactic.Types
+  ( tacticTitle
+  , TacticCommand (..)
+  ) where
+
+import qualified Data.Text as T
+
+------------------------------------------------------------------------------
+-- | The list of tactics exposed to the outside world. These are attached to
+-- actual tactics via 'commandTactic' and are contextually provided to the
+-- editor via 'commandProvider'.
+data TacticCommand
+  = Auto
+  | Split
+  | Intro
+  | Intros
+  | Destruct
+  | Homomorphism
+  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 Intros _ = "Introduce lambda"
+tacticTitle Destruct var = "Case split on " <> var
+tacticTitle Homomorphism var = "Homomorphic case split on " <> var
diff --git a/plugins/default/src/Ide/TreeTransform.hs b/plugins/default/src/Ide/TreeTransform.hs
new file mode 100644
index 0000000000..996c552c43
--- /dev/null
+++ b/plugins/default/src/Ide/TreeTransform.hs
@@ -0,0 +1,124 @@
+{-# LANGUAGE LambdaCase          #-}
+{-# LANGUAGE NamedFieldPuns      #-}
+{-# LANGUAGE OverloadedStrings   #-}
+{-# LANGUAGE RecordWildCards     #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module Ide.TreeTransform
+  ( Graft, graft, transform, useAnnotatedSource
+  ) where
+
+import           BasicTypes (appPrec)
+import           Control.Monad
+import           Control.Monad.Trans.Class
+import qualified Data.Text as T
+import           Debug.Trace
+import           Development.IDE.Core.RuleTypes
+import           Development.IDE.Core.Rules
+import           Development.IDE.Core.Shake
+import           Development.IDE.GHC.Compat  hiding (parseExpr)
+import           Development.IDE.Types.Location
+import           Generics.SYB
+import           Ide.PluginUtils
+import           Language.Haskell.GHC.ExactPrint
+import           Language.Haskell.GHC.ExactPrint.Parsers
+import           Language.Haskell.LSP.Types
+import           Language.Haskell.LSP.Types.Capabilities (ClientCapabilities)
+import           Outputable
+import           Retrie.ExactPrint hiding (parseExpr)
+import           Text.Regex.TDFA.Text()
+
+
+------------------------------------------------------------------------------
+-- | Get the latest version of the annotated parse source.
+useAnnotatedSource
+    :: String
+    -> IdeState
+    -> NormalizedFilePath
+    -> IO (Maybe (Annotated ParsedSource))
+useAnnotatedSource herald state nfp = do
+  pm <- runAction herald state $ use GetParsedModule nfp
+  pure $ fmap fixAnns pm
+
+
+------------------------------------------------------------------------------
+-- | A transformation for grafting source trees together. Use the semigroup
+-- instance to combine 'Graft's, and run them via 'transform'.
+newtype Graft a = Graft
+  { runGraft :: DynFlags -> a -> TransformT (Either String) a
+  }
+
+instance Semigroup (Graft a) where
+  Graft a <> Graft b = Graft $ \dflags -> a dflags >=> b dflags
+
+instance Monoid (Graft a) where
+  mempty = Graft $ const pure
+
+
+------------------------------------------------------------------------------
+-- | Convert a 'Graft' into a 'WorkspaceEdit'.
+transform
+    :: DynFlags
+    -> ClientCapabilities
+    -> Uri
+    -> Graft ParsedSource
+    -> Annotated ParsedSource
+    -> Either String WorkspaceEdit
+transform dflags ccs uri f a = do
+  let src = printA a
+  a' <- transformA a $ runGraft f dflags
+  let res = printA a'
+  pure $ diffText ccs (uri, T.pack src) (T.pack res) IncludeDeletions
+
+
+------------------------------------------------------------------------------
+-- | Construct a 'Graft', replacing the node at the given 'SrcSpan' with the
+-- given 'LHSExpr'. The node at that position must already be a 'LHsExpr', or
+-- this is a no-op.
+graft
+    :: forall a
+     . Data a
+    => SrcSpan
+    -> LHsExpr GhcPs
+    -> Graft a
+graft dst val = Graft $ \dflags a -> do
+  (anns, val') <- annotate dflags $ parenthesize val
+  modifyAnnsT $ mappend anns
+  pure $ everywhere'
+    ( mkT $
+        \case
+          (L src _ :: LHsExpr GhcPs) | src == dst -> val'
+          l -> l
+    ) a
+
+
+------------------------------------------------------------------------------
+-- | Dark magic I stole from retrie. No idea what it does.
+fixAnns :: ParsedModule -> Annotated ParsedSource
+fixAnns ParsedModule {..} =
+  let ranns = relativiseApiAnns pm_parsed_source pm_annotations
+   in unsafeMkA pm_parsed_source ranns 0
+
+
+------------------------------------------------------------------------------
+-- | Given an 'LHSExpr', compute its exactprint annotations.
+annotate :: DynFlags -> LHsExpr GhcPs -> TransformT (Either String) (Anns, LHsExpr GhcPs)
+annotate dflags expr = do
+  uniq <- show <$> uniqueSrcSpanT
+  let rendered = traceId $ render dflags expr
+  (anns, expr') <- lift $ either (Left . show) Right $ parseExpr dflags uniq rendered
+  let anns' = setPrecedingLines expr' 0 1 anns
+  pure (anns', expr')
+
+
+------------------------------------------------------------------------------
+-- | Print out something 'Outputable'.
+render :: Outputable a => DynFlags -> a -> String
+render dflags = showSDoc dflags . ppr
+
+
+------------------------------------------------------------------------------
+-- | Put parentheses around an expression if required.
+parenthesize :: LHsExpr GhcPs -> LHsExpr GhcPs
+parenthesize = parenthesizeHsExpr appPrec
+
diff --git a/stack-8.10.1.yaml b/stack-8.10.1.yaml
index 888d60fcf8..483e9dd060 100644
--- a/stack-8.10.1.yaml
+++ b/stack-8.10.1.yaml
@@ -20,10 +20,14 @@ 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
 - retrie-0.1.1.1
 - stylish-haskell-0.11.0.3
 - semigroups-0.18.5
 - temporary-1.2.1.1
+- implicit-hie-cradle-0.2.0.0
+- implicit-hie-0.1.1.0
+- hie-bios-0.7.1
 
 flags:
   haskell-language-server:
diff --git a/stack-8.10.2.yaml b/stack-8.10.2.yaml
index 24f8f1168e..348a1afae3 100644
--- a/stack-8.10.2.yaml
+++ b/stack-8.10.2.yaml
@@ -21,10 +21,14 @@ 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
 - retrie-0.1.1.1
 - stylish-haskell-0.11.0.3
 - semigroups-0.18.5
 - temporary-1.2.1.1
+- implicit-hie-cradle-0.2.0.0
+- implicit-hie-0.1.1.0
+- hie-bios-0.7.1
 
 flags:
   haskell-language-server:
diff --git a/stack-8.6.4.yaml b/stack-8.6.4.yaml
index 33c7463533..f501b90af4 100644
--- a/stack-8.6.4.yaml
+++ b/stack-8.6.4.yaml
@@ -28,6 +28,7 @@ extra-deps:
 - ghc-exactprint-0.6.2
 - ghc-lib-parser-8.10.1.20200523
 - ghc-lib-parser-ex-8.10.0.4
+- ghc-source-gen-0.4.0.0
 - haddock-api-2.22.0@rev:1
 - haddock-library-1.8.0
 - haskell-lsp-0.22.0.0
@@ -45,6 +46,7 @@ extra-deps:
 - ormolu-0.1.2.0
 - parser-combinators-1.2.1
 - primitive-0.7.1.0
+- refinery-0.1.0.0
 - regex-base-0.94.0.0
 - regex-pcre-builtin-0.95.1.1.8.43
 - regex-tdfa-1.3.1.0
@@ -58,6 +60,8 @@ extra-deps:
 - these-1.1.1.1
 - type-equality-1
 - topograph-1
+- implicit-hie-cradle-0.2.0.0
+- implicit-hie-0.1.1.0
 
 flags:
   haskell-language-server:
diff --git a/stack-8.6.5.yaml b/stack-8.6.5.yaml
index 0a3e7dd963..48f52f1bcc 100644
--- a/stack-8.6.5.yaml
+++ b/stack-8.6.5.yaml
@@ -25,8 +25,9 @@ extra-deps:
 # - ghcide-0.1.0
 - ghc-check-0.5.0.1
 - ghc-exactprint-0.6.2
-- ghc-lib-parser-8.10.1.20200523
-- ghc-lib-parser-ex-8.10.0.4
+- ghc-lib-parser-8.10.2.20200808
+- ghc-lib-parser-ex-8.10.0.16
+- ghc-source-gen-0.4.0.0
 - haddock-api-2.22.0@rev:1
 - haddock-library-1.8.0
 - haskell-lsp-0.22.0.0
@@ -44,6 +45,7 @@ extra-deps:
 - ormolu-0.1.2.0
 - parser-combinators-1.2.1
 - primitive-0.7.1.0
+- refinery-0.1.0.0
 - regex-base-0.94.0.0
 - regex-pcre-builtin-0.95.1.1.8.43
 - regex-tdfa-1.3.1.0
@@ -57,6 +59,8 @@ extra-deps:
 - these-1.1.1.1
 - type-equality-1
 - topograph-1
+- implicit-hie-cradle-0.2.0.0
+- implicit-hie-0.1.1.0
 
 flags:
   haskell-language-server:
diff --git a/stack-8.8.2.yaml b/stack-8.8.2.yaml
index b6f531b938..60b183aee1 100644
--- a/stack-8.8.2.yaml
+++ b/stack-8.8.2.yaml
@@ -28,7 +28,6 @@ extra-deps:
 - haskell-lsp-0.22.0.0
 - haskell-lsp-types-0.22.0.0
 - haskell-src-exts-1.21.1
-- hie-bios-0.7.1
 - hlint-2.2.8
 - hoogle-5.0.17.11
 - hsimport-0.11.0
@@ -39,6 +38,7 @@ extra-deps:
 - monad-dijkstra-0.1.1.2
 - opentelemetry-0.4.2
 - ormolu-0.1.2.0
+- refinery-0.1.0.0
 - retrie-0.1.1.1
 - semigroups-0.18.5
 # - github: wz1000/shake
@@ -46,6 +46,9 @@ extra-deps:
 - stylish-haskell-0.11.0.3
 - temporary-1.2.1.1
 - these-1.1.1.1
+- implicit-hie-cradle-0.2.0.0
+- implicit-hie-0.1.1.0
+- hie-bios-0.7.1
 
 flags:
   haskell-language-server:
diff --git a/stack-8.8.3.yaml b/stack-8.8.3.yaml
index ffff979c59..0765b96059 100644
--- a/stack-8.8.3.yaml
+++ b/stack-8.8.3.yaml
@@ -22,7 +22,6 @@ extra-deps:
 - fourmolu-0.1.0.0@rev:1
 # - ghcide-0.1.0
 - haskell-src-exts-1.21.1
-- hie-bios-0.7.1
 - hlint-2.2.8
 - HsYAML-aeson-0.2.0.0@rev:2
 - hoogle-5.0.17.11
@@ -30,12 +29,16 @@ extra-deps:
 - ilist-0.3.1.0
 - lsp-test-0.11.0.5
 - monad-dijkstra-0.1.1.2
+- refinery-0.1.0.0
 - retrie-0.1.1.1
 - semigroups-0.18.5
 # - github: wz1000/shake
 #   commit: fb3859dca2e54d1bbb2c873e68ed225fa179fbef
 - stylish-haskell-0.11.0.3
 - temporary-1.2.1.1
+- implicit-hie-cradle-0.2.0.0
+- implicit-hie-0.1.1.0
+- hie-bios-0.7.1
 
 flags:
   haskell-language-server:
diff --git a/stack-8.8.4.yaml b/stack-8.8.4.yaml
index 9234ceaeb9..1543ee1a8f 100644
--- a/stack-8.8.4.yaml
+++ b/stack-8.8.4.yaml
@@ -32,12 +32,16 @@ extra-deps:
 - ilist-0.3.1.0
 - lsp-test-0.11.0.5
 - monad-dijkstra-0.1.1.2
+- refinery-0.1.0.0
 - retrie-0.1.1.1
 - semigroups-0.18.5
 - stylish-haskell-0.11.0.3
 # - github: wz1000/shake
 #   commit: fb3859dca2e54d1bbb2c873e68ed225fa179fbef
 - temporary-1.2.1.1
+- ghc-exactprint-0.6.3.2
+- implicit-hie-cradle-0.2.0.0
+- implicit-hie-0.1.1.0
 
 flags:
   haskell-language-server:
diff --git a/stack.yaml b/stack.yaml
index 0a3e7dd963..48f52f1bcc 100644
--- a/stack.yaml
+++ b/stack.yaml
@@ -25,8 +25,9 @@ extra-deps:
 # - ghcide-0.1.0
 - ghc-check-0.5.0.1
 - ghc-exactprint-0.6.2
-- ghc-lib-parser-8.10.1.20200523
-- ghc-lib-parser-ex-8.10.0.4
+- ghc-lib-parser-8.10.2.20200808
+- ghc-lib-parser-ex-8.10.0.16
+- ghc-source-gen-0.4.0.0
 - haddock-api-2.22.0@rev:1
 - haddock-library-1.8.0
 - haskell-lsp-0.22.0.0
@@ -44,6 +45,7 @@ extra-deps:
 - ormolu-0.1.2.0
 - parser-combinators-1.2.1
 - primitive-0.7.1.0
+- refinery-0.1.0.0
 - regex-base-0.94.0.0
 - regex-pcre-builtin-0.95.1.1.8.43
 - regex-tdfa-1.3.1.0
@@ -57,6 +59,8 @@ extra-deps:
 - these-1.1.1.1
 - type-equality-1
 - topograph-1
+- implicit-hie-cradle-0.2.0.0
+- implicit-hie-0.1.1.0
 
 flags:
   haskell-language-server:
diff --git a/test/functional/Main.hs b/test/functional/Main.hs
index 328a0e502f..d499adc3f5 100644
--- a/test/functional/Main.hs
+++ b/test/functional/Main.hs
@@ -21,6 +21,7 @@ import Progress
 import Reference
 import Rename
 import Symbol
+import Tactic
 import TypeDefinition
 
 main :: IO ()
@@ -48,5 +49,6 @@ main =
         , Reference.tests
         , Rename.tests
         , Symbol.tests
+        , Tactic.tests
         , TypeDefinition.tests
         ]
diff --git a/test/functional/Tactic.hs b/test/functional/Tactic.hs
new file mode 100644
index 0000000000..17ca8e3843
--- /dev/null
+++ b/test/functional/Tactic.hs
@@ -0,0 +1,106 @@
+{-# LANGUAGE NamedFieldPuns      #-}
+{-# LANGUAGE OverloadedStrings   #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE ViewPatterns        #-}
+
+module Tactic
+  ( tests
+  )
+where
+
+import Data.Foldable
+import Data.Text (Text)
+import qualified Data.Text as T
+import           Control.Monad.IO.Class         ( MonadIO(liftIO) )
+import           Language.Haskell.LSP.Test
+import           Language.Haskell.LSP.Types     ( 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 (..))
+
+
+------------------------------------------------------------------------------
+-- | Get a range at the given line and column corresponding to having nothing
+-- selected.
+--
+-- NB: These coordinates are in "file space", ie, 1-indexed.
+pointRange :: Int -> Int -> Range
+pointRange
+  (subtract 1 -> line)
+  (subtract 1 -> col) =
+    Range (Position line col) (Position line $ col + 1)
+
+
+------------------------------------------------------------------------------
+-- | Get the title of a code action.
+codeActionTitle :: CAResult -> Maybe Text
+codeActionTitle CACommand{} = Nothing
+codeActionTitle (CACodeAction(CodeAction title _ _ _ _)) = Just title
+
+
+tests :: TestTree
+tests = testGroup
+  "tactic"
+  [ mkTest
+      "Produces intros code action"
+      "T1.hs" 2 14
+      [ (id, Intros, "")
+      ]
+  , mkTest
+      "Produces destruct and homomorphism code actions"
+      "T2.hs" 2 21
+      [ (id, Destruct, "eab")
+      , (id, Homomorphism, "eab")
+      ]
+  , mkTest
+      "Can destruct globals"
+      "T2.hs" 8 8
+      [ (id, Destruct, "global")
+      ]
+  , mkTest
+      "Won't suggest homomorphism on the wrong type"
+      "T2.hs" 8 8
+      [ (not, Homomorphism, "global")
+      ]
+  , mkTest
+      "Won't suggest intros on the wrong type"
+      "T2.hs" 8 8
+      [ (not, Intros, "")
+      ]
+  ]
+
+
+------------------------------------------------------------------------------
+-- | Make a tactic unit test.
+mkTest
+    :: Foldable t
+    => String  -- ^ The test name
+    -> FilePath  -- ^ The file to load
+    -> Int  -- ^ Cursor line
+    -> Int  -- ^ Cursor columnn
+    -> t ( Bool -> Bool   -- Use 'not' for actions that shouldnt be present
+         , TacticCommand  -- An expected command ...
+         , Text           -- ... for this variable
+         ) -- ^ A collection of (un)expected code actions.
+    -> TestTree
+mkTest name fp line col ts =
+  testCase name $ do
+  runSession hieCommand fullCaps tacticPath $ do
+    doc <- openDoc fp "haskell"
+    actions <- getCodeActions doc $ pointRange line col
+    let titles = mapMaybe codeActionTitle actions
+    for_ ts $ \(f, tc, var) -> do
+      let title = tacticTitle tc var
+      liftIO $
+        f (elem title titles)
+          @? ("Expected a code action with title " <> T.unpack title)
+
+tacticPath :: FilePath
+tacticPath = "test/testdata/tactic"
+
diff --git a/test/testdata/tactic/T1.hs b/test/testdata/tactic/T1.hs
new file mode 100644
index 0000000000..7ab382d69f
--- /dev/null
+++ b/test/testdata/tactic/T1.hs
@@ -0,0 +1,3 @@
+fmapEither :: (a -> b) -> Either c a -> Either c b
+fmapEither = _lalala
+
diff --git a/test/testdata/tactic/T2.hs b/test/testdata/tactic/T2.hs
new file mode 100644
index 0000000000..a81756abbb
--- /dev/null
+++ b/test/testdata/tactic/T2.hs
@@ -0,0 +1,9 @@
+eitherFmap :: (a -> b) -> Either e a -> Either e b
+eitherFmap fa eab = _
+
+global :: Bool
+global = True
+
+foo :: Int
+foo  = _
+
diff --git a/test/testdata/tactic/hie.yaml b/test/testdata/tactic/hie.yaml
new file mode 100644
index 0000000000..c95f6c9a09
--- /dev/null
+++ b/test/testdata/tactic/hie.yaml
@@ -0,0 +1 @@
+cradle: {direct: {arguments: ["T1", "T2"]}}
diff --git a/test/testdata/tactic/test.cabal b/test/testdata/tactic/test.cabal
new file mode 100644
index 0000000000..845edafa26
--- /dev/null
+++ b/test/testdata/tactic/test.cabal
@@ -0,0 +1,17 @@
+name:                test
+version:             0.1.0.0
+-- synopsis:
+-- description:
+license:             BSD3
+author:              Author name here
+maintainer:          example@example.com
+copyright:           2017 Author name here
+category:            Web
+build-type:          Simple
+cabal-version:       >=1.10
+
+library
+  exposed-modules:     T1, T2
+  build-depends:       base >= 4.7 && < 5
+  default-language:    Haskell2010
+  ghc-options:         -Wall -fwarn-unused-imports