[Haskell-cafe] checking types with type families

[C. McCann]

On Sat, Jul 3, 2010 at 4:28 PM, Dan Doel <dan.doel at gmail.com> wrote:
> It's potentially not just a violation of intent, but of soundness. The
> following code doesn't actually work, but one could imagine it working:
>
>  class C a b | a -> b
>
>  instance C () a
>
>  -- Theoretically works because C a b, C a c implies that b ~ c
>  --
>  -- GHC says b doesn't match c, though.
>  f :: (C a b, C a c) => a -> (b -> r) -> c -> r
>  f x g y = g y

The funny part is that GHC eventually would decide they match, but not
until after it complains about (g y). For instance, if you do this:

    f :: (C a b, C a c) => a -> (b -> r) -> c -> r
    f x g y = undefined

...and load it into GHCi, it says the type is:

    > :t f
    f :: (C a c) => a -> (c -> r) -> c -> r

As far as I can tell, type variables in scope simultaneously that
"should" be equal because of fundeps will eventually be unified, but
too late to make use of it without using some sort of type class-based
indirection. This can lead to interesting results when combined with
UndecidableInstances. For instance, consider the following:

    class C a b c | a b -> c where
        c :: a -> c -> c
        c = flip const

    instance C () b (c, c)

    f x = (c x ('a', 'b'), c x (True, False))

    g :: (c, c) -> (c, c)
    g = c ()

This works fine: Because "b" remains ambiguous, the "c" parameters
also remain distinct; yet for the same reason, "a" effectively
determines "c" anyway, such that g ends up with the type (forall c.
(c, c) -> (c, c)), rather than something like (forall c. c -> c) or
(forall b c. (C () b c) => c -> c). But if we remove the (seemingly
unused) parameter b from the fundep...

    class C a b c | a -> c where

...GHC now, understandably enough, complains that it can't match Char
with Bool. It will still accept this:

    f x = c x ('a', 'b')
    g x = c x (True, False)

...but not if you add this as well:

    h x = (f x, g x)

Or even this:

    h = (f (), g ())

On the other hand, this is still A-OK:

    f = c () ('a', 'b')
    g = c () (True, False)

    h = (f, g)

Note that all of the above is without venturing into the
OverlappingInstances pit of despair.

I don't know if this is how people expect this stuff to work, but I've
made occasional use of it--introducing a spurious parameter in order
to have a fundep that uniquely determines a polymorphic type. Perhaps
there's a better way to do that?

- C.