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.