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, just as they do this one instance FD Int Bool g :: FD Int b => ... The problem is that the implementation technique for FDs used by GHC and Hugs (global unification) isn't up to the job. 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. Simon | -----Original Message----- | From: Claus Reinke [mailto:[EMAIL PROTECTED] | Sent: 24 September 2008 19:27 | To: Simon Peyton-Jones; glasgow-haskell-users@haskell.org | Subject: Re: GADTs and functional dependencies | | >> This has never worked with fundeps, because it involves a *local* type | equality (one that holds | >> in some places and not others) and my implementation of fundeps is | fundamentally based on | >> *global* equality. Prior to GADTs that was fine! | | Actually, how does that relate to reasoning under assumptions? | | class FD a b | a -> b | | f :: (FD t1 t2, FD t1 t3) => .. | f = .. | | There is no instance of 'FD', so no equalities can be derived from there | outside of 'f', and no equalities should be derived globally from instances | that are only local hypotheses in 'f' . But inside 'f', we assume that those | two 'FD' instances exist, so we should assume 't2 ~ t3' to the right of | the implication. | | Isn't that decidedly local? | Claus | |
_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
