[GHC] #15974: QuantifiedConstraints: Spurious error involving superclass constraints

#15974: QuantifiedConstraints: Spurious error involving superclass constraints -------------------------------------+------------------------------------- Reporter: lexi.lambda | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.3 Component: Compiler | Version: 8.6.2 Keywords: | Operating System: Unknown/Multiple QuantifiedConstraints | Architecture: | Type of failure: GHC rejects Unknown/Multiple | valid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- {{{#!hs {-# LANGUAGE KindSignatures, QuantifiedConstraints, UndecidableInstances #-} }}} Consider the following datatype and two classes: {{{#!hs data X (f :: * -> *) class A a class A a => B a }}} If I create an instance `A (X f)` involving a quantified constraint {{{#!hs instance (forall a. A a => A (f a)) => A (X f) }}} then curiously, the following instance declaration for `B (X f)` is rejected with the accompanying error message: {{{#!hs instance (forall a. B a => B (f a)) => B (X f) }}} {{{ /tmp/qc.hs:11:10: error: • Could not deduce (B a) arising from the superclasses of an instance declaration from the context: forall a. B a => B (f a) bound by the instance declaration at /tmp/qc.hs:11:10-46 or from: A a bound by a quantified context at /tmp/qc.hs:1:1 Possible fix: add (B a) to the context of a quantified context • In the instance declaration for ‘B (X f)’ | 11 | instance (forall a. B a => B (f a)) => B (X f) | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ }}} Notably, if the instance declaration for `A (X f)` is altered to not use a quantified constraint, as in {{{#!hs instance A (f (X f)) => A (X f) }}} or even just {{{#!hs instance A (X f) }}} then the above instance declaration for `B (X f)` is accepted. I see no reason that the `B (X f)` declaration should be rejected, even with the quantified constraint in the instance context for `A (X f)`. The error message complains that the typechecker cannot deduce `B a`, and it even suggests adding `B a` to the context of the quantified constraint, but `B a` is //already// in that context. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15974 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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

#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: | -------------------------------------+------------------------------------- Comment (by simonpj): Great explanation lexi.lambda. I too claim this is not a but. Reason: as you say:
`forall a. B a => B (f a)` does not actually entail `forall a. A a => A (f a)`
So it's not a shortcoming in the implementation (although there are plenty of those). It's just that there is no way to construct evidence for `forall a. A a => A (f a)` from evidence for `forall a. B a => B (f a)` If you agree, would you like to close as invalid? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15974#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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: | -------------------------------------+------------------------------------- Comment (by lexi.lambda):
If you agree, would you like to close as invalid?
Yes, I have already done so, though I appreciate the confirmation that my reasoning was correct. Sorry for the noise! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15974#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC