GitLab

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