diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
index 011315dd8b..a936838f0a 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
@@ -144,6 +144,7 @@ mkWorkspaceEdits
     -> Either ResponseError (Maybe WorkspaceEdit)
 mkWorkspaceEdits span dflags ccs uri pm rtr = do
   for_ (rtr_other_solns rtr) $ traceMX "other solution"
+  traceMX "solution" $ rtr_extract rtr
   let g = graftHole (RealSrcSpan span) rtr
       response = transform dflags ccs uri g pm
    in case response of
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/FeatureSet.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/FeatureSet.hs
index 394e688f73..ce2901b7a6 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/FeatureSet.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/FeatureSet.hs
@@ -21,7 +21,9 @@ import qualified Data.Text  as T
 ------------------------------------------------------------------------------
 -- | All the available features. A 'FeatureSet' describes the ones currently
 -- available to the user.
-data Feature = FeatureUseDataCon
+data Feature
+  = FeatureUseDataCon
+  | FeatureRefineHole
   deriving (Eq, Ord, Show, Read, Enum, Bounded)
 
 
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
index e5644cebae..549dd5f4b1 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
@@ -84,11 +84,12 @@ tacticsThetaTy (tcSplitSigmaTy -> (_, theta,  _)) = theta
 ------------------------------------------------------------------------------
 -- | Get the data cons of a type, if it has any.
 tacticsGetDataCons :: Type -> Maybe ([DataCon], [Type])
-tacticsGetDataCons ty =
+tacticsGetDataCons ty | Just _ <- algebraicTyCon ty =
   splitTyConApp_maybe ty <&> \(tc, apps) ->
     ( filter (not . dataConCannotMatch apps) $ tyConDataCons tc
     , apps
     )
+tacticsGetDataCons _ = Nothing
 
 ------------------------------------------------------------------------------
 -- | Instantiate all of the quantified type variables in a type with fresh
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs
index d082e4441f..3ebf91de23 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs
@@ -51,6 +51,7 @@ commandTactic Homomorphism           = useNameFromHypothesis homo
 commandTactic DestructLambdaCase     = const destructLambdaCase
 commandTactic HomomorphismLambdaCase = const homoLambdaCase
 commandTactic UseDataCon             = userSplit
+commandTactic Refine                 = const refine
 
 
 ------------------------------------------------------------------------------
@@ -89,6 +90,9 @@ commandProvider UseDataCon =
           . occNameString
           . occName
           $ dataConName dcon
+commandProvider Refine =
+  requireFeature FeatureRefineHole $
+    provide Refine ""
 
 
 ------------------------------------------------------------------------------
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs
index c85b4104f3..b388a4cee9 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs
@@ -207,6 +207,19 @@ splitAuto = requireConcreteHole $ tracing "split(auto)" $ do
             splitDataCon dc
 
 
+------------------------------------------------------------------------------
+-- | Like 'split', but only works if there is a single matching data
+-- constructor for the goal.
+splitSingle :: TacticsM ()
+splitSingle = tracing "splitSingle" $ do
+  jdg <- goal
+  let g = jGoal jdg
+  case tacticsGetDataCons $ unCType g of
+    Just ([dc], _) -> do
+      splitDataCon dc
+    _ -> throwError $ GoalMismatch "splitSingle" g
+
+
 ------------------------------------------------------------------------------
 -- | Allow the given tactic to proceed if and only if it introduces holes that
 -- have a different goal than current goal.
@@ -268,6 +281,17 @@ localTactic t f = do
     runStateT (unTacticT t) $ f jdg
 
 
+refine :: TacticsM ()
+refine = go 3
+  where
+    go 0 = pure ()
+    go n = do
+      let try_that_doesnt_suck t = commit t $ pure ()
+      try_that_doesnt_suck intros
+      try_that_doesnt_suck splitSingle
+      go $ n - 1
+
+
 auto' :: Int -> TacticsM ()
 auto' 0 = throwError NoProgress
 auto' n = do
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/TestTypes.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/TestTypes.hs
index 219731fbc2..638fda6311 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/TestTypes.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/TestTypes.hs
@@ -20,6 +20,7 @@ data TacticCommand
   | DestructLambdaCase
   | HomomorphismLambdaCase
   | UseDataCon
+  | Refine
   deriving (Eq, Ord, Show, Enum, Bounded)
 
 -- | Generate a title for the command.
@@ -31,6 +32,7 @@ tacticTitle Homomorphism var         = "Homomorphic case split on " <> var
 tacticTitle DestructLambdaCase _     = "Lambda case split"
 tacticTitle HomomorphismLambdaCase _ = "Homomorphic lambda case split"
 tacticTitle UseDataCon dcon          = "Use constructor " <> dcon
+tacticTitle Refine _                 = "Refine hole"
 
 
 ------------------------------------------------------------------------------
diff --git a/plugins/hls-tactics-plugin/test/GoldenSpec.hs b/plugins/hls-tactics-plugin/test/GoldenSpec.hs
index 5e3fd4b9e5..e7a263814f 100644
--- a/plugins/hls-tactics-plugin/test/GoldenSpec.hs
+++ b/plugins/hls-tactics-plugin/test/GoldenSpec.hs
@@ -105,6 +105,17 @@ spec = do
       useTest "Left"  "UseConLeft.hs"  2 8
       useTest "Right" "UseConRight.hs" 2 8
 
+  -- test via:
+  -- stack test hls-tactics-plugin --test-arguments '--match "Golden/refine/"'
+  describe "refine" $ do
+    let refineTest = mkGoldenTest allFeatures Refine ""
+    describe "golden" $ do
+      refineTest "RefineIntro.hs"  2 8
+      refineTest "RefineCon.hs"    2 8
+      refineTest "RefineReader.hs" 4 8
+      refineTest "RefineGADT.hs"   8 8
+
+
   describe "golden tests" $ do
     let autoTest = mkGoldenTest allFeatures Auto ""
 
diff --git a/plugins/hls-tactics-plugin/test/golden/RefineCon.hs b/plugins/hls-tactics-plugin/test/golden/RefineCon.hs
new file mode 100644
index 0000000000..dc611f6e93
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/RefineCon.hs
@@ -0,0 +1,3 @@
+test :: ((), (b, c), d)
+test = _
+
diff --git a/plugins/hls-tactics-plugin/test/golden/RefineCon.hs.expected b/plugins/hls-tactics-plugin/test/golden/RefineCon.hs.expected
new file mode 100644
index 0000000000..e6e43592a4
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/RefineCon.hs.expected
@@ -0,0 +1,3 @@
+test :: ((), (b, c), d)
+test = ((), (_, _), _)
+
diff --git a/plugins/hls-tactics-plugin/test/golden/RefineGADT.hs b/plugins/hls-tactics-plugin/test/golden/RefineGADT.hs
new file mode 100644
index 0000000000..04fa6ee1a4
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/RefineGADT.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE GADTs #-}
+
+data GADT a where
+  One :: (b -> Int) -> GADT Int
+  Two :: GADT Bool
+
+test :: z -> GADT Int
+test = _
+
diff --git a/plugins/hls-tactics-plugin/test/golden/RefineGADT.hs.expected b/plugins/hls-tactics-plugin/test/golden/RefineGADT.hs.expected
new file mode 100644
index 0000000000..c3c463b2c8
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/RefineGADT.hs.expected
@@ -0,0 +1,9 @@
+{-# LANGUAGE GADTs #-}
+
+data GADT a where
+  One :: (b -> Int) -> GADT Int
+  Two :: GADT Bool
+
+test :: z -> GADT Int
+test z = One (\ b -> _)
+
diff --git a/plugins/hls-tactics-plugin/test/golden/RefineIntro.hs b/plugins/hls-tactics-plugin/test/golden/RefineIntro.hs
new file mode 100644
index 0000000000..afe7524957
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/RefineIntro.hs
@@ -0,0 +1,2 @@
+test :: a -> Either a b
+test = _
diff --git a/plugins/hls-tactics-plugin/test/golden/RefineIntro.hs.expected b/plugins/hls-tactics-plugin/test/golden/RefineIntro.hs.expected
new file mode 100644
index 0000000000..4cacf9e17c
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/RefineIntro.hs.expected
@@ -0,0 +1,2 @@
+test :: a -> Either a b
+test a = _
diff --git a/plugins/hls-tactics-plugin/test/golden/RefineReader.hs b/plugins/hls-tactics-plugin/test/golden/RefineReader.hs
new file mode 100644
index 0000000000..cf4df0cd91
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/RefineReader.hs
@@ -0,0 +1,5 @@
+newtype Reader r a = Reader (r -> a)
+
+test :: b -> Reader r a
+test = _
+
diff --git a/plugins/hls-tactics-plugin/test/golden/RefineReader.hs.expected b/plugins/hls-tactics-plugin/test/golden/RefineReader.hs.expected
new file mode 100644
index 0000000000..570bb31c33
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/RefineReader.hs.expected
@@ -0,0 +1,5 @@
+newtype Reader r a = Reader (r -> a)
+
+test :: b -> Reader r a
+test b = Reader (\ r -> _)
+