## #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

Resolution: | → invalid |
---|---|

Status: | new → closed |

### comment:2 follow-up: 3 Changed 10 months ago by

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 Changed 10 months ago by

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.

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 differentoptions 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:

`A (X f)`

when declaring the`B (X f)`

instance.`A (X f)`

, it then tries to solve the (quantified) instance context,`forall a. A a => A (f a)`

.`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).`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!This is unintuitive to me, since when I write, say,

`Eq`

and`Ord`

instance on a datatype, I merely write them likenot like

…but this works out only because

`Ord a`

entails`Eq a`

. In this case,`forall a. B a => B (f a)`

doesnotactually entail`forall a. A a => A (f a)`

, so I guess this is not actually a bug.