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