TypeFamilies vs. FunctionalDependencies & type-level recursion

[Dan Doel]

Sorry about the double send, David. I forgot to switch to reply-all in
the gmail interface.

On Tue, Jun 14, 2011 at 11:49 AM,
<dm-list-haskell-prime at scs.stanford.edu> wrote:
> You absolutely still can use FunctionalDependencies to determine type
> equality in GHC 7.  For example, I just verified the code below with
> GHC 7.02:
>
> *Main> typeEq True False
> HTrue
> *Main> typeEq (1 :: Int) (2 :: Int)
> HTrue
> *Main> typeEq (1 :: Int) False
> HFalse
>
> As always, you have to make sure one of the overlapping instances is
> more specific than the other, which you can do by substituting a
> parameter c for HFalse in the false case and fixing c to HFalse using
> another class like TypeCast in the context.  (As contexts play no role
> in instance selection, they don't make the instance any more
> specific.)
>
> While I don't have convenient access to GHC 6 right this second, I'm
> pretty sure there has been no change for a while, as the HList paper
> discussed this topic in 2004.

Okay. I don't really write a lot of code like this, so maybe I missed
the quirks.

In that case, HList has been relying on broken behavior of fundeps for
7 years. :) Because the instance:

   instance TypeEq a b c

violates the functional dependency, by declaring:

   instance TypeEq Int Int Int
   instance TypeEq Int Int Char
   instance TypeEq Int Int Double
   ...
   instance TypeEq Int Char Int
   instance TypeEq Int Char Char
   ...

and adding the constraint doesn't actually affect which instances are
being declared, it just adds a constraint requirement for when any of
the instances are used. It appears I was wrong, though. GHC doesn't
actually fix the instance for such fundeps, and the following compiles
and runs fine:

   class C a b | a -> b where
     foo :: a -> b
     foo = error "Yo dawg."

   instance C a b where

   bar :: Int
   bar = foo "x"

   baz :: Char
   baz = foo "x"

so we're using an instance C String Int and an instance C String Char
despite the fact that there's a functional dependency from the first
argument to the second.

-- Dan