Simon Peyton-Jones wrote:

| > {-# OPTIONS -fglasgow-exts #-} | > | > class C a b c | a b -> c where | > foo :: (a, b) -> c | > | > instance C a a r => C a (b, c) r where | > foo (a, (b, c)) = foo (a, a)

You are already on dodgy ground here, because the instance decl doesn't guarantee that the bit before the => is smaller than the bit after the =>. E.g. context reduction could go: C (Int,Int) (Bool, Bool) r --> C (Int,Int) (Int,Int) r --> C (Int,Int) (Int,Int) r

So [Point 1]: GHC should require -fallow-undecidable-instances if you use repeated type variables before the =>.

Yes, I think that would be a good idea.

| Now, in GHCi (version 6.4), | | > *FDs> let bar x = foo ((x, x), (x, x)) | > *FDs> :t bar | > bar :: (C (a, a) (a, a) c) => a -> c | | but GHC is also happy to accept the more general type | | > bar :: a -> c | > bar x = foo ((x, x), (x, x))

There are two separate things going on here

[Point 2] GHC postpones context reduction until it's forced to do it (except if a single step will eliminate the dictionary altogether). Example:

data T a = T a instance Eq (T a) bar x = [T x] == []

GHC will *infer* bar :: Eq [T a] => a -> Bool, but it will happily *check* bar :: a -> Bool bar x = [T x] == []

The reason for this lazy context reduction is overlapping instances; in principle there might be more instances for Eq [T a] at bar's call site.

But now I look at it again, I think it would be OK to postpone context reduction only if there actually were overlapping instances (right here at bar's defn). That might be a good idea because it'd give less confusing types perhaps.

However, note that the two types are indeed equivalent -- both are more general than the other. It's like saying (Eq Int => t) <= t, and vice versa.

Semantically, I understand that the constraint "C ((x, x), (x, x) a)" does not constrain the two type variables "x" and "a" (and hence, the two types are equivalent), but I don't see how you can derive that with the constraint entailment rules \theta \in P ------------ P ||- \theta P ||- forall a.\theta --------------------- P || [t/a]\theta P || p => \phi P ||- p ------------------------ P ||- \phi which I thought are those underlying GHC's type system.

| Again, in GHCi, | | > *FDs> let bar x = foo ((x::Int, x), (x, x)) | > *FDs> :t bar | > bar :: Int -> () | | (which by itself is bizarre)

This is the first time when the functional dependency plays a role.

...

From bar's right-hand-side we get the constraint (C (Int,Int) (Int,Int) c), and the type (Int -> c). Now GHC tries to decide what to quantify over. Shall we quantify over c? Well, no. GHC never quantifies over type variables that are free in the environment (of course) OR are fixed by functional dependencies from type variables free in the environment. In this case the functional dependencies tell us that since (Int,Int) is obviously completely fixed, then there's no point in quantifying over c.

So bar is not quantified. The constraint (C (Int,Int) (Int,Int) c) is satisfied via the recursive dictionary thing, leaving 'c' completely unconstrained. So GHC chooses c to be (), because it doesn't like to leave programs with completely free type variables.

| but it also accepts | | > bar :: Int -> c | > bar x = foo ((x::Int, x), (x, x))

Here you are *telling* GHC what to quantify over, so the inference of what to quantify doesn't happen.

I accept that this is the process by which GHC computes these types, but it does violate the principal types property, doesn't it? The relation Int -> () <= forall c. Int -> c does not hold. Summary ~~~~~~~ So it seems to me that * MPTCs with recursive dictionary construction seem to require a semantic model of subsumption (as the normal constraint entailment rules would lead to infinite trees). * MPTCs with recursive dictionary construction and FDs break principal types. I guess that's all ok provided GHC enforces the use of -fallow-undecidable-instances for any instances that need recursive dictionaries. Manuel