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