Can adding a constraint cause other constraints to go out of scope?

Question

Consider the following code, which typechecks:

module Scratch where

import GHC.Exts

ensure :: forall c x. c => x -> x
ensure = id

type Eq2 t = (forall x y. (Eq x, Eq y) => Eq (t x y) :: Constraint)

foo :: forall t a.
  ( Eq2 t
  , Eq a
  ) => ()
foo = ensure @(Eq (a `t` a)) ()

foo isn't doing anything useful here, but let's imagine it's doing some important business that requires an Eq (t a a) instance. The compiler is able to take the (Eq2 t, Eq a) constraints and elaborate an Eq (t a a) dictionary, so the constraint is discharged and everything works.

Now suppose we want foo to do some additional work that depends on an instance of the following rather convoluted class:

-- some class
class (forall ob x y. (SomeConstraint t ~ ob, ob x, ob y) => ob (t x y)) =>
  SomeClass t
  where
  type SomeConstraint t :: * -> Constraint

foo' :: forall t a.
  ( Eq2 t
  , Eq a
  , SomeClass t -- <- the extra constraint
  ) => ()
foo' = ensure @(Eq (a `t` a)) ()

Note that in the body of foo' we're still demanding only what we did in foo: an Eq (t a a) constraint. Moreover we haven't removed or modified the constraints the compiler used to elaborate an instance of Eq (t a a) in foo; we still demand (Eq2 t, Eq a) in addition to the new constraint. So I would expect foo' to typecheck as well.

Unfortunately, it looks like what actually happens is that the compiler forgets how to elaborate Eq (t a a). Here is the error we get in the body of foo':

    • Could not deduce (Eq (t a a)) arising from a use of ‘ensure’
      from the context: (Eq2 t, Eq a, SomeClass t)
        bound by the type signature for:
                   foo' :: forall (t :: * -> * -> *) a.
                           (Eq2 t, Eq a, SomeClass t) =>
                           ()

Given that the compiler can "deduce Eq (t a a)" just fine "from the context (Eq2 t, Eq a)", I don't understand why the richer context (Eq2 t, Eq a, SomeClass t) causes Eq (t a a) to become unavailable.

Is this a bug, or am I just doing something wrong? In either case, is there some workaround for this?

Answer 1

It's not really a bug; it's expected. In the definition of foo, the context has

1. forall x y. (Eq x, Eq y) => Eq (t x y) (i.e. Eq2 t)
2. Eq a
3. SomeClass t
4. forall ob x y. (SomeConstraint t ~ ob, ob x, ob y) => ob (t x y) (from the "closure of the superclass relation over" SomeClass t)

We want Eq (t a a). Well, from the context, there are two axioms whose heads match: (1) with x ~ a, y ~ a and (2) with ob ~ Eq, x ~ a, y ~ a. There is doubt; GHC rejects. (Note that since SomeConstraint t ~ ob is only in the hypothesis of (4), it gets completely ignored; choosing instances pays attention only to instance heads.)

The obvious way forward is to remove (4) from the superclasses of SomeClass. How? Split the quantification from the actual instance "head":

class ob (t x y) => SomeClassSuper ob t x y where
instance ob (t x y) => SomeClassSuper ob t x y where
class (forall ob x y. (SomeConstraint t ~ ob, ob x, ob y) => SomeClassSuper ob t x y) => SomeClass t where
  type SomeConstraint t :: * -> Constraint

This is what your forall ob. _ => forall x y. _ => _ trick basically did, except this doesn't rely on a bug (your syntax is not allowed). Now, (4) becomes forall ob x y. (SomeConstraint t ~ ob, ob x, ob y) => SomeClassSuper ob t x y. Because this is not actually a constraint of the form Class args..., it doesn't have superclasses, so GHC doesn't search upwards and find the all-powerful forall ob x y. ob (t x y) head that ruins everything. Now the only instance capable of discharging Eq (t a a) is (1), so we use it.

GHC does search the "superclasses" of the new (4) when it absolutely needs to; the User's Guide actually makes this feature out to be an extension to the base rules above, which come from the original paper. That is, forall ob x y. (SomeConstraint t ~ ob, ob x, ob y) => ob (t x y) is still available, but it is considered after all the "true" superclasses in the context (since it isn't actually the superclass of anything).

import Data.Kind

ensure :: forall c x. c => ()
ensure = ()

type Eq2 t = (forall x y. (Eq x, Eq y) => Eq (t x y) :: Constraint)

-- fine
foo :: forall t a. (Eq2 t, Eq a) => ()
foo = ensure @(Eq (t a a))

class ob (t x y) => SomeClassSuper ob t x y where
instance ob (t x y) => SomeClassSuper ob t x y where
class (forall ob x y. (SomeConstraint t ~ ob, ob x, ob y) => SomeClassSuper ob t x y) => SomeClass t where
  type SomeConstraint t :: * -> Constraint

-- also fine
bar :: forall t a. (Eq2 t, Eq a, SomeClass t) => ()
bar = ensure @(Eq (t a a))

-- also also fine
qux :: forall t a. (Eq2 t, Eq a, SomeConstraint t a, SomeClass t) => ()
qux = ensure @(SomeConstraint t (t a a))

You might argue that, in accordance with the open world policy, GHC should backtrack in the face of "incoherence" (such as the overlap between (1) and the original (4)), since quantified constraints can manufacture "incoherence" while there is no actual incoherence and we'd like your code to "just work". That's a perfectly valid want, but GHC is currently being conservative and just giving up instead of backtracking for reasons of performance, simplicity, and predictability.