
#15974: QuantifiedConstraints: Spurious error involving superclass constraints -------------------------------------+------------------------------------- Reporter: lexi.lambda | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.6.3 Component: Compiler | Version: 8.6.2 Resolution: invalid | Keywords: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by lexi.lambda): * status: new => closed * resolution: => invalid Comment: I discovered #14831, which is superficially related to this ticket, but I think the issues are actually distinct. The issue in that ticket is that GHC has //two different// options for solving a constraint, and it picks the wrong one. After reading some of the discussion there, however, I think I understand what’s going on in this ticket, and I don’t think it’s an issue with GHC making the wrong choice, but rather GHC having only one choice to make. In the program in the ticket, GHC is performing the following steps: 1. GHC attempts to solve the superclass constraint `A (X f)` when declaring the `B (X f)` instance. 2. Since the only way to get there is through the instance declaration for `A (X f)`, it then tries to solve the (quantified) instance context, `forall a. A a => A (f a)`. 3. GHC then attempts to solve `A (f a)`, assuming it has `A a`, and it only has one path to get there, which is through `B (f a)` (via the superclass relationship). 4. It then tries to solve `B a`, since that is the quantified context of `B (f a)`, and it gets stuck. This suggests a fix: add `forall a. A a => A (f a)` to the instance context for `B (X f)`. And indeed, the following declaration is accepted! {{{#!hs instance (forall a. A a => A (f a), forall a. B a => B (f a)) => B (X f) }}} This is unintuitive to me, since when I write, say, `Eq` and `Ord` instance on a datatype, I merely write them like {{{#!hs instance Eq a => Eq (List a) instance Ord a => Ord (List a) }}} not like {{{#!hs instance Eq a => Eq (List a) instance (Eq a, Ord a) => Ord (List a) }}} …but this works out only because `Ord a` entails `Eq a`. In this case, `forall a. B a => B (f a)` does **not** actually entail `forall a. A a => A (f a)`, so I guess this is not actually a bug. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15974#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler