## GHC does not use quantified constraint from transitive superclass

## Summary

GHC sometimes does not choose to use a quantified constraint made available by a superclass, and I am not sure why. The program typechecks if a type annotation is added to give the instance search a hint. Here’s a small program that reproduces the issue:

```
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE TypeFamilies #-}
module Sandbox where
type family F a
class C1 a
class (forall c. C1 c) => C2 a
class (forall b. (b ~ F a) => C2 a) => C3 a
data Dict c = c => Dict
foo :: forall a. C3 a => Dict (C1 a)
foo = Dict
bar :: forall a. C3 a => Dict (C1 a)
bar = Dict :: C2 a => Dict (C1 a)
```

The definition of `foo`

is rejected with the following error:

```
error:
• Could not deduce (C1 a) arising from a use of ‘Dict’
from the context: C3 a
bound by the type signature for:
foo :: forall a. C3 a => Dict (C1 a)
Possible fix:
add (C1 a) to the context of
the type signature for:
foo :: forall a. C3 a => Dict (C1 a)
• In the expression: Dict
In an equation for ‘foo’: foo = Dict
```

However, `bar`

is accepted, as GHC successfully solves the `C2 a`

constraint using the quantified superclass of `C3`

, then proceeds to use the quantified superclass of `C2`

to solve `C1 a`

.

What’s especially strange to me about this program is that the problem goes away if either constraint is non-quantified *or* if the type family is removed from the context of `C3`

’s superclass. The second of those two conditions makes it sound like maybe this is related to #15347, but I don’t think it is. That issue is about equalities in quantified heads, while this involves an equality in a quantified instance context, and equalities in instance contexts are entirely legal.

I think `foo`

should typecheck, but if it can’t for some reason I don’t understand, I’d prefer it at least fail with a more helpful error message.

## Environment

- GHC version used: 8.8.1