Give a canonical ordering for destructing terms in Wingman (#1586)

* Use a canonical ordering when destructing terms

* Fix introducing hypotheses in the wrong order

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

Author: isovector

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

@@ -16,6 +16,7 @@ import           Development.IDE.Spans.LocalBindings
 import           OccName
 import           SrcLoc
 import           Type
+import           Wingman.GHC (algebraicTyCon)
 import           Wingman.Types
 
 
@@ -61,7 +62,10 @@ withNewGoal t = field @"_jGoal" .~ t
 
 
 introduce :: Hypothesis a -> Judgement' a -> Judgement' a
-introduce hy = field @"_jHypothesis" <>~ hy
+-- NOTE(sandy): It's important that we put the new hypothesis terms first,
+-- since 'jAcceptableDestructTargets' will never destruct a pattern that occurs
+-- after a previously-destructed term.
+introduce hy = field @"_jHypothesis" %~ mappend hy
 
 
 ------------------------------------------------------------------------------
@@ -149,7 +153,10 @@ findPositionVal :: Judgement' a -> OccName -> Int -> Maybe OccName
 findPositionVal jdg defn pos = listToMaybe $ do
   -- It's important to inspect the entire hypothesis here, as we need to trace
   -- ancstry through potentially disallowed terms in the hypothesis.
-  (name, hi) <- M.toList $ M.map (overProvenance expandDisallowed) $ hyByName $ jEntireHypothesis jdg
+  (name, hi) <- M.toList
+              $ M.map (overProvenance expandDisallowed)
+              $ hyByName
+              $ jEntireHypothesis jdg
   case hi_provenance hi of
     TopLevelArgPrv defn' pos' _
       | defn == defn'
@@ -238,12 +245,13 @@ patternHypothesis scrutinee dc jdg
   = introduceHypothesis $ \_ pos ->
       PatternMatchPrv $
         PatVal
-            scrutinee
-            (maybe mempty
-                  (\scrut -> S.singleton scrut <> getAncestry jdg scrut)
-                  scrutinee)
-            (Uniquely dc)
-            pos
+          scrutinee
+          (maybe
+              mempty
+              (\scrut -> S.singleton scrut <> getAncestry jdg scrut)
+              scrutinee)
+          (Uniquely dc)
+          pos
 
 
 ------------------------------------------------------------------------------
@@ -285,6 +293,21 @@ jLocalHypothesis
   . jHypothesis
 
 
+------------------------------------------------------------------------------
+-- | Given a judgment, return the hypotheses that are acceptable to destruct.
+--
+-- We use the ordering of the hypothesis for this purpose. Since new bindings
+-- are always inserted at the beginning, we can impose a canonical ordering on
+-- which order to try destructs by what order they are introduced --- stopping
+-- at the first one we've already destructed.
+jAcceptableDestructTargets :: Judgement' CType -> [HyInfo CType]
+jAcceptableDestructTargets
+  = filter (isJust . algebraicTyCon . unCType . hi_type)
+  . takeWhile (not . isAlreadyDestructed . hi_provenance)
+  . unHypothesis
+  . jEntireHypothesis
+
+
 ------------------------------------------------------------------------------
 -- | If we're in a top hole, the name of the defining function.
 isTopHole :: Context -> Judgement' a -> Maybe OccName
@@ -391,6 +414,12 @@ isDisallowed :: Provenance -> Bool
 isDisallowed DisallowedPrv{} = True
 isDisallowed _               = False
 
+------------------------------------------------------------------------------
+-- | Has this term already been disallowed?
+isAlreadyDestructed :: Provenance -> Bool
+isAlreadyDestructed (DisallowedPrv AlreadyDestructed _) = True
+isAlreadyDestructed _ = False
+
 
 ------------------------------------------------------------------------------
 -- | Eliminates 'DisallowedPrv' provenances.

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

@@ -358,9 +358,7 @@ overFunctions =
 
 overAlgebraicTerms :: (HyInfo CType -> TacticsM ()) -> TacticsM ()
 overAlgebraicTerms =
-  attemptOn $ filter (isJust . algebraicTyCon . unCType . hi_type)
-            . unHypothesis
-            . jHypothesis
+  attemptOn jAcceptableDestructTargets
 
 
 allNames :: Judgement -> Set OccName

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

@@ -261,6 +261,10 @@ instance Uniquable a => Ord (Uniquely a) where
   compare = nonDetCmpUnique `on` getUnique . getViaUnique
 
 
+-- NOTE(sandy): The usage of list here is mostly for convenience, but if it's
+-- ever changed, make sure to correspondingly update
+-- 'jAcceptableDestructTargets' so that it correctly identifies newly
+-- introduced terms.
 newtype Hypothesis a = Hypothesis
   { unHypothesis :: [HyInfo a]
   }