Functional dependencies, principal types, and decidable type checking

[Iavor Diatchki]

Hi,

On Apr 3, 2005 7:33 AM, Manuel M T Chakravarty <chak at cse.unsw.edu.au> wrote:
> 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
This seems reasonable.


> but GHC is also happy to accept the more general type
> 
> > bar :: a -> c
> > bar x = foo ((x, x), (x, x))

It seems that GHC 6.4 has a new "feature" where it is creating
recursive dictionaries (which is sometimes useful).   Here is a
simpler example of the same behavior:
> {-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}
> 
> class T a where t :: a
> instance T a => T a where t = t
> 
> f :: Int
> f = t
GHC accepts this which means that it managed to discharge the
constraint "T Int", and the only way it could have done this is by
creating a recursive (in this case bottom) dicitionary.

> > *FDs> let bar x = foo ((x::Int, x), (x, x))
> > *FDs> :t bar
> > bar :: Int -> ()
This looks like a bug to me.

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

I think this is what GHC used to do, and indeed seems quite
reasonable.  I guess one could be more lazy in the context reduction
(like GHC did in the first example), and only diverge if the function
is actually used.

I think that if an implementation creates recursive dictionaries it
may be nice to have some sort of a "progress" check to avoid creating
completely undefined dictionaries.  I suspect implementing such a
thing may be tricky though.

-Iavor