Refine should either do intros or split, not both (#1842)

* Refine should either do intros or split, not both

* Empty commit for CI

* Another commit for CI

Author: isovector

plugins/hls-tactics-plugin/src/Wingman/Tactics.hs

@@ -381,10 +381,7 @@ localTactic t f = do
 
 
 refine :: TacticsM ()
-refine = do
-  try' intros
-  try' splitSingle
-  try' intros
+refine = intros <%> splitSingle
 
 
 auto' :: Int -> TacticsM ()

plugins/hls-tactics-plugin/test/CodeAction/RefineSpec.hs

@@ -13,11 +13,11 @@ spec = do
   let refineTest = goldenTest Refine ""
 
   describe "golden" $ do
-    refineTest 2 8 "RefineIntro"
-    refineTest 2 8 "RefineCon"
-    refineTest 4 8 "RefineReader"
-    refineTest 8 8 "RefineGADT"
+    refineTest  2  8 "RefineIntro"
+    refineTest  2  8 "RefineCon"
+    refineTest  4 10 "RefineReader"
+    refineTest  8 10 "RefineGADT"
 
   describe "messages" $ do
-    mkShowMessageTest allFeatures Refine "" 2 8 "MessageForallA" NothingToDo
+    mkShowMessageTest allFeatures Refine "" 2 8 "MessageForallA" TacticErrors
 

plugins/hls-tactics-plugin/test/golden/RefineGADT.expected.hs

@@ -5,5 +5,5 @@ data GADT a where
   Two :: GADT Bool
 
 test :: z -> GADT Int
-test z = One (\ b -> _)
+test z = One _
 

plugins/hls-tactics-plugin/test/golden/RefineGADT.hs

@@ -5,5 +5,5 @@ data GADT a where
   Two :: GADT Bool
 
 test :: z -> GADT Int
-test = _
+test z = _
 

plugins/hls-tactics-plugin/test/golden/RefineReader.expected.hs

@@ -1,5 +1,5 @@
 newtype Reader r a = Reader (r -> a)
 
 test :: b -> Reader r a
-test b = Reader (\ r -> _)
+test b = Reader _
 

plugins/hls-tactics-plugin/test/golden/RefineReader.hs

@@ -1,5 +1,5 @@
 newtype Reader r a = Reader (r -> a)
 
 test :: b -> Reader r a
-test = _
+test b = _