Consider this "list membership" typeclass and two overlapping instances:

class Elem (x :: k) (xs :: [k])

instance {-# OVERLAPS #-} Elem x (x ': xs)
instance {-# OVERLAPS #-} Elem x xs => Elem x (y ': xs)

The inductive style is satisfying, but I'm struggling to understand exactly how GHC can pick one instance over the other.

How is a constraint like Elem Int [Int] solved? Certainly the Elem x (x ': xs) instance matches, with x = Int and xs = []. But, the second instance is also equally valid with x = Int, y = Int, xs = []. Even though if the second instance is chosen, the context cannot be satisfied (no instance for Elem x []), it's my understanding that GHC will not backtrack once it picks an instance. And because both instances look valid to me, I don't understand why this code does not require IncoherentInstances.

Thanks.

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe