Merge pull request #3314 from dunhamsteve/issue-3313

[ fix ] auto search returns no solution instead of ambiguous solution #3313

src/Core/AutoSearch.idr

@@ -142,6 +142,7 @@ anyOne fc env top [elab]
     = catch elab $
          \case
            err@(CantSolveGoal _ _ _ _ _) => throw err
+           err@(AmbiguousSearch _ _ _ _) => throw err
            _ => throw $ CantSolveGoal fc (gamma !(get Ctxt)) [] top Nothing
 anyOne fc env top (elab :: elabs)
     = tryUnify elab (anyOne fc env top elabs)

tests/idris2/error/error028/Issue3313.idr

@@ -0,0 +1,5 @@
+data Expr : Type -> Type where
+    Add : (Integral n) => n -> n -> Expr n
+
+eval : (Integral n) => Expr n -> n
+eval (Add x y) = x + y

tests/idris2/error/error028/expected

@@ -0,0 +1,15 @@
+1/1: Building Issue3313 (Issue3313.idr)
+Error: While processing right hand side of eval. Multiple solutions found in search of:
+    Integral n
+
+Issue3313:5:18--5:23
+ 1 | data Expr : Type -> Type where
+ 2 |     Add : (Integral n) => n -> n -> Expr n
+ 3 | 
+ 4 | eval : (Integral n) => Expr n -> n
+ 5 | eval (Add x y) = x + y
+                      ^^^^^
+
+Possible correct results:
+    conArg (implicitly bound at Issue3313:5:1--5:23)
+    conArg (implicitly bound at Issue3313:5:1--5:23)

tests/idris2/error/error028/run

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