
Oddly, this message was rejected by the system. Trying again.
---------- Forwarded message ----------
From: "David Feuer"
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

I see. I did know about the specificity rule, but somehow it escaped me that the extra y := x substitution required for the second instance to match means that the first instance *is* more specific. Thanks! PS - why do overlapping instances give you hives? Did you mean incoherent instances? On Wednesday, February 24, 2016 at 7:07:54 PM UTC-8, David Feuer wrote:
Oddly, this message was rejected by the system. Trying again. ---------- Forwarded message ---------- From: "David Feuer"
javascript:> Date: Feb 24, 2016 10:04 PM Subject: Re: [Haskell-cafe] Overlapping instances To: "Mitchell Rosen" javascript:> Cc: "Haskell-cafe" javascript:> It's possible that GHC will backtrack with overlapping enabled (I can't remember, and overlapping instances give me hives) but it doesn't have here. The first instance is "more specific" than the second because the type variable x appears twice. On Feb 24, 2016 9:49 PM, "Mitchell Rosen"
javascript:> wrote: 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 Haskel...@haskell.org javascript: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe

No, I refuse to believe that incoherent instances are actually supported.
The documentation must be lying. Overlapping instances are too complicated
for me to really trust. More annoyingly, their existence anywhere violates
some nice properties that would otherwise hold. For instance, from
instance C a => C (Maybe a)
along with
C (Maybe Int)
you'd like to be able to conclude that
C Int
but you can't, because maybe there's a special instance for C (Maybe Int)
somewhere. Overlapping instances also work fairly badly with associated
types.
On Feb 24, 2016 10:12 PM, "Mitchell Rosen"
I see. I did know about the specificity rule, but somehow it escaped me that the extra y := x substitution required for the second instance to match means that the first instance *is* more specific.
Thanks!
PS - why do overlapping instances give you hives? Did you mean incoherent instances?
On Wednesday, February 24, 2016 at 7:07:54 PM UTC-8, David Feuer wrote:
Oddly, this message was rejected by the system. Trying again. ---------- Forwarded message ---------- From: "David Feuer"
Date: Feb 24, 2016 10:04 PM Subject: Re: [Haskell-cafe] Overlapping instances To: "Mitchell Rosen" Cc: "Haskell-cafe" It's possible that GHC will backtrack with overlapping enabled (I can't remember, and overlapping instances give me hives) but it doesn't have here. The first instance is "more specific" than the second because the type variable x appears twice. On Feb 24, 2016 9:49 PM, "Mitchell Rosen"
wrote: 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 Haskel...@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
participants (2)
-
David Feuer
-
Mitchell Rosen