Functional dependencies, principal types, and decidable typechecking

[Simon Peyton-Jones]

Manuel

Your short program tickles a lot of different questions.  Here's an
explanation.

Simon

| Assume the following type class declarations with functional
| dependencies:

Actually much of the behaviour you see happens without fundeps.
 
| > {-# 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 =>.


| 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.


[Point 3]  As Iavor notes, yes, GHC is building recursive dictionaries.
Suppose GHC is trying to find evidence for constraint C from a set of
constraints (with evidence provided) D.  Suppose it finds an instance
decl D' => C which matches C.  Then it tries to prove the constraints
D'.  The new bit is that it adds C to D before trying to prove D'.
That's all!

This is Jolly Useful sometimes.   (See John Hughes's paper about
restricted type synonyms for example.)   It's a bit like infinite data
structures.  ML doesn't let you build them, so there's a static error.
Haskell does, and that is sometimes just what you want; and sometimes
gives you runtime divergence (e.g. take the length of an infinite list).
In the same way, this recursive-dictionary thing is sometimes just what
you want; but sometimes gives you runtime divergence instead of a static
error.


| 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.