Functional dependencies, principal types, and decidable typechecking

[Manuel M T Chakravarty]

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