Hi Iavor, Thanks much for the explanation.

Before this experiment with FDs, I was using a type family. I tried switching to FDs, because I wanted the compiler to know that the family is injective in order to assist type-checking. Can we declare type families to be injective? Now I see that I ran into a similar problem almost two years ago: http://haskell.1045720.n5.nabble.com/Injective-type-families-td3385084.html. I guess the answer is still "no", judging by this ticket: http://hackage.haskell.org/trac/ghc/ticket/6018 . -- Conal On Tue, Dec 25, 2012 at 6:47 PM, Iavor Diatchki <iavor.diatc...@gmail.com>wrote: > Hello Conal, > > GHC implementation of functional dependencies is incomplete: it will use > functional dependencies during type inference (i.e., to determine the > values of free type variables), but it will not use them in proofs, which > is what is needed in examples like the one you posted. The reason some > proving is needed is that the compiler needs to figure out that for each > instantiation of the type `ta` and `tb` will be the same (which, of course, > follows directly from the FD on the class). > > As far as I understand, the reason that GHC does not construct such proofs > is that it can't express them in its internal proof language (System FC). > It seems to me that it should be fairly straight-forward to extend FC to > support this sort of proof, but I have not been able to convince folks that > this is the case. I could elaborate, if there's interest. > > In the mean time, the way forward would probably be to express the > dependency using type families, which I find tends to be more verbose but, > at present, is better supported in GHC. > > Cheers, > -Iavor > PS: cc-ing the GHC users' list, as there was some talk of closing the > ghc-bugs list, but I am not sure if the transition happened yet. > > > > > > On Tue, Dec 25, 2012 at 6:15 PM, Conal Elliott <co...@conal.net> wrote: > >> I ran into a simple falure with functional dependencies (in GHC 7.4.1): >> >> > class Foo a ta | a -> ta >> > >> > foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool >> > foo = (==) >> >> I expected that the `a -> ta` functional dependency would suffice to >> prove that `ta ~ tb`, but >> >> Pixie/Bug1.hs:9:7: >> Could not deduce (ta ~ tb) >> from the context (Foo a ta, Foo a tb, Eq ta) >> bound by the type signature for >> foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> >> Bool >> at Pixie/Bug1.hs:9:1-10 >> `ta' is a rigid type variable bound by >> the type signature for >> foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool >> at Pixie/Bug1.hs:9:1 >> `tb' is a rigid type variable bound by >> the type signature for >> foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool >> at Pixie/Bug1.hs:9:1 >> Expected type: ta -> tb -> Bool >> Actual type: ta -> ta -> Bool >> In the expression: (==) >> In an equation for `foo': foo = (==) >> Failed, modules loaded: none. >> >> Any insights about what's going wrong here? >> >> -- Conal >> >> _______________________________________________ >> Glasgow-haskell-bugs mailing list >> Glasgow-haskell-bugs@haskell.org >> http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs >> >> >

_______________________________________________ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs