Quantified constraint doesn't evidence type family instances
Summary
First up, sorry in advance: I'm unsure on the exact vocabulary for this particular problem.
In the below code, I would expect the DC
constraint on eg1
to imply the CC
constraint required for eg0
via the quantified constraint on D
. However, it doesn't seem to be able to do so.
Interestingly, if I change the constraint on eg0
to use the Magic
class (which I created because of the recent restrictions on QC instance heads), everything seems to work happily.
Is this a case of GHC not searching hard enough for the CC
instance? I'm certainly not an expert, but this behaviour feels bizarre to me; my intuition until now would have been to say that CC f x
and Magic f x
are equivalent in all circumstances!
Steps to reproduce
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE UndecidableInstances #}
{# LANGUAGE UndecidableSuperClasses #}
import Data.Kind (Constraint, Type)
class CC f x => Magic f x
instance CC f x => Magic f x
class C (f :: Type > Type) where
type CC f :: Type > Constraint
eg0 :: CC f x => f x > f x  Changing the constraint to `Magic f x => ...` works!
eg0 = id
class (C f, forall x. DC f x => Magic f x) => D (f :: Type > Type) where
type DC f :: Type > Constraint
eg1 :: (D f, DC f x) => f x > f x
eg1 = eg0
• Could not deduce: CC f x arising from a use of ‘eg0’
from the context: (D f, DC f x)
bound by the type signature for:
eg1 :: forall (f :: * > *) x. (D f, DC f x) => f x > f x
at Test.hs:23:134
• In the expression: eg0
In an equation for ‘eg1’: eg1 = eg0
• Relevant bindings include
eg1 :: f x > f x (bound at Test.hs:24:1)

24  eg1 = eg0
 ^^^
Expected behavior
I would expect the aforementioned change to be a noop, though I suspect I'm missing some context!
Environment
 GHC version used: 8.6.5, 8.8.1, 8.10