Functional dependencies, principal types, and decidable type checking

[Manuel M T Chakravarty]

Assume the following type class declarations with functional
dependencies:

> {-# 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)

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

Again, in GHCi,

> *FDs> let bar x = foo ((x::Int, x), (x, x))
> *FDs> :t bar
> bar :: Int -> ()

(which by itself is bizarre), but it also accepts

> bar :: Int -> c
> bar x = foo ((x::Int, x), (x, x))
 
For those who expected GHC to diverge during type checking with the
above class declaration, console yourself by knowing that Hugs (Feb'05)
does diverge...well, it invokes the emergency break:

> Hugs.Base> :l FDs
> ERROR "./FDs.hs" -
> *** The type checker has reached the cutoff limit while trying to
> *** determine whether:
> ***     C (Int,Int) (Int,Int) a
> *** can be deduced from:
> ***     ()
> *** This may indicate that the problem is undecidable.  However,
> *** you may still try to increase the cutoff limit using the -c
> *** option and then try again.  (The current setting is -c40)

Manuel