Inconsistent error message when finding more than one implementation of an interface

[JavierGelatti]

Context

When more than one implementation of an interface is found, Idris (correctly) generates an error notifying the problem. The error message includes an explanation of the issue.

For example:

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

eval : (Num n) => Expr n -> n
eval (Add x y) = x + y
--               ^^^^^
--               Error marked here

The generated error is:

While processing right hand side of eval. Multiple solutions found in search of:
    Num n

Possible correct results:
    conArg (implicitly bound at <location>)
    conArg (implicitly bound at <location>)

Problem

However, when more than one implementation is indirectly found (i.e. by interface extension), the error message is inconsistent and can be misleading.

Steps to Reproduce

The following is the same code as before, but replacing Num with Integral. Note that the applied function (+) is declared in the Num interface, and Integral extends Num.

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

eval : (Integral n) => Expr n -> n
eval (Add x y) = x + y
--               ^^^^^
--               Error marked here

Expected Behavior

The generated error should explain that more than one instance of Num was found:

While processing right hand side of eval. Multiple solutions found in search of:
    Num n

Possible correct results:
    ...

Knowing the search paths that were used to find the implementations could also be useful.

Observed Behavior

The error message says that it couldn't find an implementation for Num:

While processing right hand side of eval. Can't find an implementation for Num n.

This is not only inconsistent with the first error but can also be misleading because it's equivalent to the error that's generated when no implementation of Num could be found, e.g.:

data Expr : Type -> Type where
    Add : n -> n -> Expr n

eval : Expr n -> n
eval (Add x y) = x + y
--               ^^^^^
-- While processing right hand side of eval.
-- Can't find an implementation for Num n.