[Haskell-cafe] Overlapping instances

[Mitchell Rosen]

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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20160224/758ea838/attachment.html>