Split out the attemptWhen combinator

Author: isovector

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

@@ -223,6 +223,16 @@ unify goal inst = do
     Nothing -> throwError (UnificationError inst goal)
 
 
+------------------------------------------------------------------------------
+-- | Prefer the first tactic to the second, if the bool is true. Otherwise, just run the second tactic.
+--
+-- This is useful when you have a clever pruning solution that isn't always
+-- applicable.
+attemptWhen :: TacticsM a -> TacticsM a -> Bool -> TacticsM a
+attemptWhen _  t2 False = t2
+attemptWhen t1 t2 True  = commit t1 t2
+
+
 ------------------------------------------------------------------------------
 -- | Get the class methods of a 'PredType', correctly dealing with
 -- instantiation of quantified class types.

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

@@ -131,14 +131,13 @@ destructOrHomoAuto hi = tracing "destructOrHomoAuto" $ do
   let g  = unCType $ jGoal jdg
       ty = unCType $ hi_type hi
 
-  let do_destruct = rule $ destruct' (const subgoal) hi
-
-  case (splitTyConApp_maybe g, splitTyConApp_maybe ty) of
-    (Just (gtc, apps), Just (tytc, _)) | gtc == tytc ->
-      commit
-        (rule $ destruct' (\dc jdg -> buildDataCon False jdg dc apps) hi)
-        do_destruct
-    _ -> do_destruct
+  attemptWhen
+      (rule $ destruct' (\dc jdg ->
+        buildDataCon False jdg dc $ snd $ splitAppTys g) hi)
+      (rule $ destruct' (const subgoal) hi)
+    $ case (splitTyConApp_maybe g, splitTyConApp_maybe ty) of
+        (Just (gtc, _), Just (tytc, _)) -> gtc == tytc
+        _ -> False
 
 
 ------------------------------------------------------------------------------