GADTs and functional dependencies

[Claus Reinke]

> By "global" I really meant "throughout the scope of the type variable concerned.
>
> Nevertheless, the program you give is rejected, even though the scope is global:
>
>  class FD a b | a -> b
>
>  f :: (FD t1 t2, FD t1 t3) => t1 -> t2 -> t3
>  f x y = y
>
> Both GHC and Hugs erroneously reject the program,

while both GHC and Hugs accept this variation:

    class FD a b | a -> b
    f :: (FD t1 t2, FD t1 t3) => t1 -> t2 -> t3
    f x y = undefined

and infer the type of 'f' to be 'f :: (FD t1 t3) => t1 -> t3 -> t3'.

So they use the FD globally (when checking use of 'f'), but not locally
(when checking the definition of 'f'). Is that interpretation correct, or is
there another bug involved?

> The problem is that the implementation technique for FDs used by GHC and Hugs (global unification) 
> isn't up to the job.

Interesting. When the FD-via-CHR discussion started, I toyed with the
idea of writing an instance inference engine based on CHR (since CHR
happen to be a variant of CPN - Coloured Petri Nets -, I happened to
have an implementation at hand;-). But once I noticed the difficulties of
managing local constraint stores (and exchanging some, but not all inferred
information with the global constraint store), I abandoned the idea.

Ever since then I've been wondering how GHC handles that!-)

>That is what we are fixing with type functions.  I do not know how to fix it for FDs (except by way 
>of translation to TFs) -- at least, not while maintaining a strongly typed intermediate language. 
>This latter constraint is a condition imposed by GHC, but it's one I am strongly committed to.

Since FDs constrain the set of valid instances, I had been wondering
whether one could apply the FD-based refinements/substitutions to the
code obtained (just as they are applied to the class constraints) while
keeping a typed intermediate language.

Claus