Possible bug with GADTs?
Below, please find a snippet from a program I'm working on, and the error it produces. I was told in #haskell that this was "pretty suspect" and could conceivably be a ghc bug. So I'm reporting it here. I'd also be grateful for workarounds. This is on ghc 6.12.1.20100203, but if people can't reproduce it I'll install a newer one; I'm just not eager to do that because of course it means rebuilding quite a lot of things. {-# LANGUAGE GADTs #-} module Foo where data TemplateValue t where TemplateList :: [a] -> TemplateValue [a] instance (Eq a) => Eq (TemplateValue a) where (==) (TemplateList a) (TemplateList b) = (==) a b Foo.hs:7:45: Could not deduce (Eq a1) from the context (a ~ [a2]) arising from a use of `==' at Foo.hs:7:45-52 Possible fix: add (Eq a1) to the context of the constructor `TemplateList' In the expression: (==) a b In the definition of `==': == (TemplateList a) (TemplateList b) = (==) a b In the instance declaration for `Eq (TemplateValue a)' -- Dan Knapp "An infallible method of conciliating a tiger is to allow oneself to be devoured." (Konrad Adenauer)
It looks to me as though that wouldn't be expected to work because 'a' and 't' are different type variables... which seems to be essentially what the error msg is saying... ...am I missing something? --Ben On 17 Aug 2010, at 19:54, Dan Knapp wrote:
Below, please find a snippet from a program I'm working on, and the error it produces. I was told in #haskell that this was "pretty suspect" and could conceivably be a ghc bug. So I'm reporting it here. I'd also be grateful for workarounds. This is on ghc 6.12.1.20100203, but if people can't reproduce it I'll install a newer one; I'm just not eager to do that because of course it means rebuilding quite a lot of things.
{-# LANGUAGE GADTs #-} module Foo where
data TemplateValue t where TemplateList :: [a] -> TemplateValue [a] instance (Eq a) => Eq (TemplateValue a) where (==) (TemplateList a) (TemplateList b) = (==) a b
Foo.hs:7:45: Could not deduce (Eq a1) from the context (a ~ [a2]) arising from a use of `==' at Foo.hs:7:45-52 Possible fix: add (Eq a1) to the context of the constructor `TemplateList' In the expression: (==) a b In the definition of `==': == (TemplateList a) (TemplateList b) = (==) a b In the instance declaration for `Eq (TemplateValue a)'
-- Dan Knapp "An infallible method of conciliating a tiger is to allow oneself to be devoured." (Konrad Adenauer) _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Thinking about this a bit more, and renaming some of the variables: {-# LANGUAGE GADTs #-} module Foo where data TemplateValue t where TemplateList :: [x] -> TemplateValue [x] instance (Eq a) => Eq (TemplateValue a) where (==) (TemplateList b) (TemplateList c) = (==) b c -- here we have a == [x] Could not deduce (Eq x) from the context (a ~ [x1]) It looks as though it has decided to use the (instance Eq x => Eq [x]) instance, and hence is searching for Eq x (which can't be deduced) rather than using the (Eq a / Eq [x]) directly. So, I guess that's an interesting question why that happens... --Ben On 17 Aug 2010, at 20:04, Ben Moseley wrote:
It looks to me as though that wouldn't be expected to work because 'a' and 't' are different type variables... which seems to be essentially what the error msg is saying...
...am I missing something?
--Ben
On 17 Aug 2010, at 19:54, Dan Knapp wrote:
Below, please find a snippet from a program I'm working on, and the error it produces. I was told in #haskell that this was "pretty suspect" and could conceivably be a ghc bug. So I'm reporting it here. I'd also be grateful for workarounds. This is on ghc 6.12.1.20100203, but if people can't reproduce it I'll install a newer one; I'm just not eager to do that because of course it means rebuilding quite a lot of things.
{-# LANGUAGE GADTs #-} module Foo where
data TemplateValue t where TemplateList :: [a] -> TemplateValue [a] instance (Eq a) => Eq (TemplateValue a) where (==) (TemplateList a) (TemplateList b) = (==) a b
Foo.hs:7:45: Could not deduce (Eq a1) from the context (a ~ [a2]) arising from a use of `==' at Foo.hs:7:45-52 Possible fix: add (Eq a1) to the context of the constructor `TemplateList' In the expression: (==) a b In the definition of `==': == (TemplateList a) (TemplateList b) = (==) a b In the instance declaration for `Eq (TemplateValue a)'
-- Dan Knapp "An infallible method of conciliating a tiger is to allow oneself to be devoured." (Konrad Adenauer) _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1 On 08/17/2010 03:22 PM, Ben Moseley wrote:
{-# LANGUAGE GADTs #-} module Foo where
data TemplateValue t where TemplateList :: [x] -> TemplateValue [x]
instance (Eq a) => Eq (TemplateValue a) where (==) (TemplateList b) (TemplateList c) = (==) b c -- here we have a == [x]
Could not deduce (Eq x) from the context (a ~ [x1])
It looks as though it has decided to use the (instance Eq x => Eq [x]) instance, and hence is searching for Eq x (which can't be deduced) rather than using the (Eq a / Eq [x]) directly. So, I guess that's an interesting question why that happens...
Hm... isn't that a case of overlapping and/or incoherent instances? -----BEGIN PGP SIGNATURE----- Version: GnuPG v1.4.10 (GNU/Linux) Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/ iEYEARECAAYFAkxrXlgACgkQIn7hlCsL25USIQCfZ2cZXlZJZxVLI/m4pWkfA4+f 18EAnjIsecXNpJNbYUyfIPs7uTgoNi5M =8tG5 -----END PGP SIGNATURE-----
| {-# LANGUAGE GADTs #-} | module Foo where | | data TemplateValue t where | TemplateList :: [x] -> TemplateValue [x] | | instance (Eq b) => Eq (TemplateValue b) where | (==) (TemplateList p) (TemplateList q) = (==) p q A good example. Yes, GHC 6.12 fails on this and will always fail because its type checker is inadequate. I'm hard at work [today] on the new typechecker, which compiles it just fine. Here's the reasoning (I have done a bit of renaming). * The TemplateList constructor really has type TemplateList :: forall a. forall x. (a~[x]) => [x] -> TemplateValue a * So in the pattern match we have (Eq b) available from the instance header TemplateList p :: TemplateValue b x is a skolem, existentially bound by the pattern p :: [x] b ~ [x] available from the pattern match * On the RHS we find we need (Eq [x]). * So the constraint problem we have is (Eq b, b~[x]) => Eq [x] ["Given" => "Wanted"] Can we prove this? From the two given constraints we can see that we also have Eq [x], and that certainly proves Eq [x]. Nevertheless, it's a bit delicate. If we didn't notice all the consequences of the "given" constraints, we might use the top-level Eq a => Eq [a] instance to solve the wanted Eq [x]. And now we need Eq x, which *isn't* a consequence of (Eq b, b~[x]). Still, there is a unique proof, and GHC (now) finds it. It'll all be in 6.16. Simon
Wow, I didn't seriously expect it was a real bug. This is my first
time finding a confirmed compiler bug. Thanks for the response!
On Wed, Aug 18, 2010 at 2:49 AM, Simon Peyton-Jones
| {-# LANGUAGE GADTs #-} | module Foo where | | data TemplateValue t where | TemplateList :: [x] -> TemplateValue [x] | | instance (Eq b) => Eq (TemplateValue b) where | (==) (TemplateList p) (TemplateList q) = (==) p q
A good example. Yes, GHC 6.12 fails on this and will always fail because its type checker is inadequate. I'm hard at work [today] on the new typechecker, which compiles it just fine.
Here's the reasoning (I have done a bit of renaming).
* The TemplateList constructor really has type TemplateList :: forall a. forall x. (a~[x]) => [x] -> TemplateValue a
* So in the pattern match we have (Eq b) available from the instance header TemplateList p :: TemplateValue b x is a skolem, existentially bound by the pattern p :: [x] b ~ [x] available from the pattern match
* On the RHS we find we need (Eq [x]).
* So the constraint problem we have is (Eq b, b~[x]) => Eq [x] ["Given" => "Wanted"] Can we prove this? From the two given constraints we can see that we also have Eq [x], and that certainly proves Eq [x].
Nevertheless, it's a bit delicate. If we didn't notice all the consequences of the "given" constraints, we might use the top-level Eq a => Eq [a] instance to solve the wanted Eq [x]. And now we need Eq x, which *isn't* a consequence of (Eq b, b~[x]).
Still, there is a unique proof, and GHC (now) finds it. It'll all be in 6.16.
Simon
-- Dan Knapp "An infallible method of conciliating a tiger is to allow oneself to be devoured." (Konrad Adenauer)
On Tue, Aug 17, 2010 at 8:54 PM, Dan Knapp
Below, please find a snippet from a program I'm working on, and the error it produces. I was told in #haskell that this was "pretty suspect" and could conceivably be a ghc bug. So I'm reporting it here. I'd also be grateful for workarounds. [...]
I've just found a fairly simple one: make instance resolution happen where the equality constraints are not in scope. {-# LANGUAGE GADTs #-} data TemplateValue a where TemplateList :: [a] -> TemplateValue [a] instance Eq a => Eq (TemplateValue a) where (==) = eqBy (==) eqBy :: (a -> a -> Bool) -> TemplateValue a -> TemplateValue a -> Bool eqBy (==) (TemplateList xs) (TemplateList ys) = xs == ys I've also found that, surprisingly at this point, the following typechecks: eq :: Eq a => TemplateValue a -> Bool eq (TemplateList xs) = xs == xs
participants (5)
-
Andrea Vezzosi -
Ben Moseley -
Brandon S Allbery KF8NH -
Dan Knapp -
Simon Peyton-Jones