Opened 10 months ago

Closed 10 months ago

Last modified 10 months ago

#15974 closed bug (invalid)

QuantifiedConstraints: Spurious error involving superclass constraints

Reported by: lexi.lambda Owned by:
Priority: normal Milestone: 8.6.3
Component: Compiler Version: 8.6.2
Keywords: QuantifiedConstraints Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

{-# LANGUAGE KindSignatures, QuantifiedConstraints, UndecidableInstances #-}

Consider the following datatype and two classes:

data X (f :: * -> *)

class A a
class A a => B a

If I create an instance A (X f) involving a quantified constraint

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:

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

instance A (f (X f)) => A (X f)

or even just

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.

Change History (3)

comment:1 Changed 10 months ago by lexi.lambda

Resolution: invalid
Status: newclosed

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.
  1. 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).
  1. 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).
  1. 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!

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

instance Eq a => Eq (List a)
instance Ord a => Ord (List a)

not like

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.

comment:2 Changed 10 months ago 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?

comment:3 in reply to:  2 Changed 10 months ago 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!

Note: See TracTickets for help on using tickets.