TypeFamilies vs. FunctionalDependencies & type-level recursion

[Dan Doel]

On Tue, Jun 14, 2011 at 11:27 AM, Andrea Vezzosi <sanzhiyan at gmail.com> wrote:
>>    class C a b | a -> b
>>    instance C a R
>>    instance C T U
>
> Are you sure that worked before?

80%

> The following still does anyhow:
>
>    data R
>    data T
>    data U
>    class C a b | a -> b
>    instance TypeCast R b => C a b
>    instance TypeCast U b => C T b
>
> In fact this is how IsFunction was implemented in 2005[1], and the
> same transformation appears to work for the Eq class too.
> If we allow TypeFamilies we can use (~) instead of the TypeCast hack,
> fortunately.

So it does.

    instance (b ~ R) => C a b
    instance (b ~ U) => C T b

Which is odd. I don't think there's a way to justify this working.
Either the preconditions are being taken into account, in which case
there is no reason for this to behave differently from:

    instance C a R
    instance C T U

or the preconditions are not being taken into account (which is the
type class way), in which case both of the qualified instances are
illegal, because they declare instances C T b for all b (plus a
constraint on the use), which violates the fundep. I've seen examples
like this before, and I think what GHC ends up doing (now) is fixing
the 'b' to whatever instance it needs first. But I don't think that's
very good behavior.

In this case it happens that it's impossible to use at more than one
instance, but if you accept the instances, you're back to the
questions of type soundness that are only evaded because fundeps don't
actually use all the information they allegedly express.

-- Dan