[SOLVED] How to deal with "Error: Multiple solutions found"?

How to deal with "Error: Multiple solutions found"?

I'm trying to build a set datatype.

mutual

  data Set : Type -> Type where
    Nil : Eq a => Set a
    (::) : Eq a => (x : a) -> (s : Set a) -> {auto _ : contains x s = False} -> Set a

  contains : Eq a => a -> Set a -> Bool
  contains x [] = False
  contains x (y :: s) = (x == y) || contains x s

But I have no idea how to deal with this error:

Error: While processing right hand side of contains. Multiple solutions found in search of:
    Eq a

test:9:26--9:32
 5 |     (::) : Eq a => (x : a) -> (s : Set a) -> {auto _ : contains x s = False} -> Set a
 6 |
 7 |   contains : Eq a => a -> Set a -> Bool
 8 |   contains x [] = False
 9 |   contains x (y :: s) = (x == y) || contains x s
                              ^^^^^^

Possible correct results:
    conArg (implicitly bound at test:9:3--9:49)
    conArg (implicitly bound at test:9:3--9:49)

Solution

You have multiple instances of Eq a floating around (one for each set element), so Idris isn't sure which one to use. For example, in contains, there's one from contains : Eq a => and another less obvious one from (y :: s). You can disambiguate with

  contains : Eq a => a -> Set a -> Bool
  contains x [] = False
  contains @{eq} x (y :: s) = ((==) @{eq} x y) || contains @{eq} x s

though it may be better to work out some refactor that doesn't have multiple Eq a, if that's possible.