Functional dependencies, principal types, and decidable type checking

[Manuel M T Chakravarty]

Iavor Diatchki wrote:
> 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.

It is reasonable in so far as it is a valid typing, but Haskell
(including FDs) comes with the promise of type inference determining
principal (as in most general) types.

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

We know

  a -> c   <=   (C (a, a) (a, a) c) => a -> c

where <= is the "is more or as general as" relation, but due to GHCi's
answer to ":t bar", it must also be true that

  (C (a, a) (a, a) c) => a -> c   <=   a -> c

To check whether that relation holds, we need to know the set of
satisfiable instances of the predicate "C (a, a) (a, a) c" under the
given instance declaration.  It seems as if we get infinite inference
trees here.

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

Yes, *but* you have given GHC -fallow-undecidable-instances!!  My
examples doesn't require that.

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

This only happens when the functional dependency "a b -> c" is used in
the class declaration.  I think what is happening is that the type
variable that was to the right of the error is "zonk"ed (in error) after
type checking.

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

I am actually a bit worried about the type theory of this all.
Recursive dictionaries sounds like a cool idea, but what does it mean in
terms of typing derivations?  Moreover, how does that combine with
improving substitutions, such as those used in the implementation of
functional dependencies?

Manuel