Less aggressive refine tactic (#1475)

* Use try' everywhere

* Make refine much less aggressive

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

Author: isovector

plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/KnownStrategies.hs

@@ -5,7 +5,7 @@ module Ide.Plugin.Tactic.KnownStrategies where
 import           Control.Monad.Error.Class
 import           Ide.Plugin.Tactic.Context                    (getCurrentDefinitions)
 import           Ide.Plugin.Tactic.KnownStrategies.QuickCheck (deriveArbitrary)
-import           Ide.Plugin.Tactic.Machinery                  (tracing)
+import           Ide.Plugin.Tactic.Machinery                  (tracing, try')
 import           Ide.Plugin.Tactic.Tactics
 import           Ide.Plugin.Tactic.Types
 import           OccName                                      (mkVarOcc)
@@ -29,7 +29,7 @@ known name t = do
 
 deriveFmap :: TacticsM ()
 deriveFmap = do
-  try intros
+  try' intros
   overAlgebraicTerms homo
   choice
     [ overFunctions apply >> auto' 2

plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Machinery.hs

@@ -272,3 +272,16 @@ requireConcreteHole m = do
     0 -> m
     _ -> throwError TooPolymorphic
 
+
+------------------------------------------------------------------------------
+-- | The 'try' that comes in refinery 0.3 causes unnecessary backtracking and
+-- balloons the search space. This thing just tries it, but doesn't backtrack
+-- if it fails.
+--
+-- TODO(sandy): Remove this when we upgrade to 0.4
+try'
+    :: Functor m
+    => TacticT jdg ext err s m ()
+    -> TacticT jdg ext err s m ()
+try' t = commit t $ pure ()
+

plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs

@@ -309,21 +309,17 @@ localTactic t f = do
 
 
 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
+refine = do
+  try' intros
+  try' splitSingle
+  try' intros
 
 
 auto' :: Int -> TacticsM ()
 auto' 0 = throwError NoProgress
 auto' n = do
   let loop = auto' (n - 1)
-  try intros
+  try' intros
   choice
     [ overFunctions $ \fname -> do
         apply fname

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

@@ -1,3 +1,3 @@
 test :: ((), (b, c), d)
-test = ((), (_, _), _)
+test = (_, _, _)