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

[dunhamsteve]

Description

This fixes #3313, where auto search reports no solution instead of an ambiguous solution.

The root cause it that the AmbiguousSearch error is caught and then re-emitted as CantSolveGoal.

Prior to this change the code:

data Expr : Type -> Type where
    Add : (Integral n) => n -> n -> Expr n

eval : (Integral n) => Expr n -> n
eval (Add x y) = x + y

reports

1/1: Building src.Issue3313 (src/Issue3313.idr)
Error: While processing right hand side of eval. Can't find an implementation for Num n.

src.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
                      ^^^^^

and after the change it reports

1/1: Building Issue3313 (src/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)

[andrevidela]

Looks good to me

[gallais]

Ideally we'd want the bounds on these implicitly introduced names to be tighter so that one points to eval and one points to Add instead of both pointing to the whole LHS.