<div dir="ltr">Consider this "list membership" typeclass and two overlapping instances:<div><br></div><div><font size="2" face="courier new, monospace">class Elem (x :: k) (xs :: [k])</font></div><div><font size="2" face="courier new, monospace"><br></font></div><div><font size="2" face="courier new, monospace">instance {-# OVERLAPS #-} Elem x (x ': xs)<br>instance {-# OVERLAPS #-} Elem x xs => Elem x (y ': xs)</font><br><br>The inductive style is satisfying, but I'm struggling to understand exactly how GHC can pick one instance over the other.</div><div><br></div><div>How is a constraint like <font face="courier new, monospace">Elem Int [Int]</font><font face="arial, sans-serif"> solved? Certainly the </font><font face="courier new, monospace">Elem x (x ': xs)</font><font face="arial, sans-serif"> instance matches, with </font><font face="courier new, monospace">x = Int</font><font face="arial, sans-serif"> and </font><font face="courier new, monospace">xs = []</font><font face="arial, sans-serif">. But, the second instance is also equally valid with </font><font face="courier new, monospace">x = Int, y = Int, xs = []</font><font face="arial, sans-serif">. Even though <i>if </i>the second instance is chosen, the context cannot be satisfied (no instance for </font><font face="courier new, monospace">Elem x []</font><font face="arial, sans-serif">), 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 </font><font face="courier new, monospace">IncoherentInstances</font><font face="arial, sans-serif">.</font></div><div><font face="arial, sans-serif"><br></font></div><div><font face="arial, sans-serif">Thanks.</font></div></div>