[ fix ] Make searching in pairs to not cause ambiguity when there isn't (#3366)

* [ test ] Move wrongly placed test

* [ cleanup ] Remove one unused argument

* [ refactor ] Support normalisation inside the proof modification fun

* [ fix ] Normalise `fst`s and `snd`s and remove duplicates in autosearch

src/Core/AutoSearch.idr

@@ -181,7 +181,7 @@ exactlyOne fc env top target [elab]
            _ => throw $ CantSolveGoal fc (gamma !(get Ctxt)) [] top Nothing
 exactlyOne {vars} fc env top target all
     = do elabs <- successful all
-         case rights elabs of
+         case nubBy ((==) `on` fst) $ rights elabs of
               [(res, defs, ust)] =>
                     do put UST ust
                        put Ctxt defs
@@ -270,7 +270,7 @@ searchLocalWith : {vars : _} ->
 searchLocalWith {vars} fc rigc defaults trying depth def top env (prf, ty) target
     = do defs <- get Ctxt
          nty <- nf defs env ty
-         findPos defs prf id nty target
+         findPos defs pure nty target
   where
     clearEnvType : {idx : Nat} -> (0 p : IsVar nm idx vs) ->
                    FC -> Env Term vs -> Env Term vs
@@ -283,14 +283,15 @@ searchLocalWith {vars} fc rigc defaults trying depth def top env (prf, ty) targe
         = clearEnvType p fc env
     clearEnv _ env = env
 
-    findDirect : Defs -> Term vars ->
+    findDirect : Defs ->
-                 (Term vars -> Term vars) ->
+                 (Term vars -> Core (Term vars)) ->
                  NF vars ->  -- local's type
                  (target : NF vars) ->
                  Core (Term vars)
-    findDirect defs p f ty target
+    findDirect defs f ty target
         = do (args, appTy) <- mkArgs fc rigc env ty
-             logTermNF "auto" 10 "Trying" env (f prf)
+             fprf <- f prf
+             logTermNF "auto" 10 "Trying" env fprf
              logNF "auto" 10 "Type" env ty
              logNF "auto" 10 "For target" env target
              ures <- unify inTerm fc env target appTy
@@ -299,7 +300,7 @@ searchLocalWith {vars} fc rigc defaults trying depth def top env (prf, ty) targe
              -- We can only use the local if its type is not an unsolved hole
              if !(usableLocal fc defaults env ty)
                 then do
-                   let candidate = apply fc (f prf) (map metaApp args)
+                   let candidate = apply fc fprf (map metaApp args)
                    logTermNF "auto" 10 "Local var candidate " env candidate
                    -- Clear the local from the environment to avoid getting
                    -- into a loop repeatedly applying it
@@ -312,13 +313,13 @@ searchLocalWith {vars} fc rigc defaults trying depth def top env (prf, ty) targe
                 else do logNF "auto" 10 "Can't use " env ty
                         throw (CantSolveGoal fc (gamma defs) [] top Nothing)
 
-    findPos : Defs -> Term vars ->
+    findPos : Defs ->
-              (Term vars -> Term vars) ->
+              (Term vars -> Core (Term vars)) ->
               NF vars ->  -- local's type
               (target : NF vars) ->
               Core (Term vars)
-    findPos defs p f nty@(NTCon pfc pn _ _ [(_, xty), (_, yty)]) target
+    findPos defs f nty@(NTCon pfc pn _ _ [(_, xty), (_, yty)]) target
-        = tryUnifyUnambig (findDirect defs prf f nty target) $
+        = tryUnifyUnambig (findDirect defs f nty target) $
              do fname <- maybe (throw (CantSolveGoal fc (gamma defs) [] top Nothing))
                                pure
                                !fstName
@@ -331,22 +332,22 @@ searchLocalWith {vars} fc rigc defaults trying depth def top env (prf, ty) targe
                            ytytm <- quote empty env yty
                            exactlyOne fc env top target
                             [(do xtynf <- evalClosure defs xty
-                                 findPos defs p
+                                 findPos defs
-                                     (\arg => apply fc (Ref fc Func fname)
+                                     (\arg => normalise defs env $ apply fc (Ref fc Func fname)
                                                         [xtytm,
                                                          ytytm,
-                                                         f arg])
+                                                         !(f arg)])
                                      xtynf target),
                              (do ytynf <- evalClosure defs yty
-                                 findPos defs p
+                                 findPos defs
-                                     (\arg => apply fc (Ref fc Func sname)
+                                     (\arg => normalise defs env $ apply fc (Ref fc Func sname)
                                                         [xtytm,
                                                          ytytm,
-                                                         f arg])
+                                                         !(f arg)])
                                      ytynf target)]
                    else throw (CantSolveGoal fc (gamma defs) [] top Nothing)
-    findPos defs p f nty target
+    findPos defs f nty target
-        = findDirect defs p f nty target
+        = findDirect defs f nty target
 
 searchLocalVars : {vars : _} ->
                   {auto c : Ref Ctxt Defs} ->

tests/idris2/interface/interface033/PairErroneouslyFound.idr

@@ -0,0 +1,40 @@
+data X = MkX
+
+useX : X => Nat
+
+v : (X, String)
+
+f : Nat
+f = do
+  let (x, _) = v
+  useX
+
+f' : Nat
+f' = do
+  let xx = v
+  useX
+
+g : Nat
+g = do
+  let xx@(x, _) = v
+  useX
+
+g' : Monad m => m Nat
+g' = do
+  (x, _) <- pure v
+  pure useX
+
+g'' : Monad m => m Nat
+g'' = do
+  xx@(x, _) <- pure v
+  pure useX
+
+data Y = MkY
+
+failing "Multiple solutions found"
+  bad1 : X => Y => X => Nat
+  bad1 = useX
+
+failing "Multiple solutions found"
+  bad2 : (X, Y) => X => Nat
+  bad2 = useX

tests/idris2/interface/interface033/expected

@@ -0,0 +1 @@
+1/1: Building PairErroneouslyFound (PairErroneouslyFound.idr)

tests/idris2/interface/interface033/run

@@ -0,0 +1,3 @@
+. ../../../testutils.sh
+
+check PairErroneouslyFound.idr