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?

Sky

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.

Eppes

Simplicity? Where's that? – Smalltime

@Smalltime Simplicity of the compiler implementation in that it doesn't have to become a Prolog interpreter. – Eppes

Answer 2

I think you're running up against the "Reject if in doubt" rule for overlapping axioms. When you bring the SomeClass t constraint into scope, you also introduce the new quantified constraint forall ob x y. (ob x, ob y) => ob (t x y). When it comes time to discharge Eq (t a a), GHC doesn't know whether to use the quantified constraint Eq2 t in foo's signature or the quantified constraint in the SomeClass class, as either one would apply. (As always, GHC doesn't consider SomeConstraint t ~ ob in assessing whether the polymorphic instance applies or not.) There's no mechanism to check that the latter can be "specialized" to the former.

If you delete the Eq2 t constraint from foo:

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

then you'll get an error "Couldn't match type SomeConstraint t with Eq", suggesting that this is exactly how GHC is trying to solve this constraint. (If you remove the SomeConstraint t ~ ob from the class, it'll even typecheck!)

This doesn't solve your problem, but I think it explains what's going on.

Wong

Answer 3

EDIT: This workaround turns out to be a does-not-work-around, because it does not compile in GHC 8.8.3. Mysteriously, the analogous real world program compiles fine in GHC 8.6.5, and even passes a battery of tests, despite the successful compilation being the result of a bug.

---

I found a workaround that involves "breaking up" the quantification in the additional class I'm depending on. So if I make the following change:

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

it makes foo' typecheck.

I still don't really understand why this makes things work, and whether it's somehow coupled to the way I'm quantifying over variables in foo' (in which case it's not really a feasible solution).

Additionally, it still seems to me that it's a bug that the additional SomeClass constraint on foo' (regardless of how SomeClass is defined) would somehow cause the compiler to forget how to build an Eq (t a a) out of the available Eq2 t and Eq a. Is this intuition incorrect?

Additional answers that shed light on these two points are welcome.

Sky

I can't get this to compile. I get "quantified predicate must have a class or type variable head" with GHC 8.8.3 and AllowAmbiguousTypes, ConstraintKinds, KindSignatures, QuantifiedConstraints, RankNTypes, ScopedTypeVariables, TypeApplications, TypeOperators, TypeFamilies. – Wong

Oh, the lack of error message on your GHC version might be this bug, so this "workaround" probably isn't working. – Wong

@K.A.Buhr The entire program compiles and works, so I'm not sure in what sense it wouldn't be working. Do you mean it will fail at runtime? – Sky

I compiled this with 8.6.5, I'll try it with a more recent version of GHC. – Sky