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:1-34
• 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 no-op, though I suspect I'm missing some context!
Environment
- GHC version used: 8.6.5, 8.8.1, 8.10