Fundeps and type equality

[Iavor Diatchki]

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 <conal at 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20121225/175fa942/attachment.htm>