GADTs and functional dependencies

[David Menendez]

On Tue, Sep 23, 2008 at 1:44 PM, Chris Kuklewicz
<haskell at list.mightyreason.com> wrote:
> You cannot create a normal function "fun".  You can make a type class
> function
>
> fun :: Class a b => GADT a -> b
>
>> data GADT a where
>>     GADT :: GADT ()
>>     GADT2 :: GADT String
>>
>> -- fun1 :: GADT () -> () -- infers type
>> fun1 g = case g of
>>           (GADT :: GADT ()) -> ()
>>
>> -- fun2 :: GADT String -> Bool -- infers type
>> fun2 g = case g of
>>           (GADT2 :: GADT String) -> True
>>
>> -- "fun" cannot type check.  The type of 'g' cannot be both "GADT ()" and
>> "GADT String"
>> -- This is because "fun" is not a member of type class.
>> {- fun g = case g of
>>           (GADT :: GADT ()) -> ()
>>           (GADT2 :: GADT String) -> True
>> -}

It may be that fun cannot type check, but surely it isn't for the
reason you've given.

data Rep a where
    Unit :: Rep ()
    Int :: Rep Int

zero :: Rep a -> a
zero r = case r of
    Unit -> ()
    Int -> 0

The type of r is "both" Rep () and Rep Int. No type class needed.

If I had to guess, I'd say the original problem is that any
specialization triggered by the functional dependency happens before
the specialization triggered by pattern matching on the GADT. If I
recall correctly, it is known that GADTs and fundeps don't always work
nicely together.

The example does seem to work if translated to use type families.

type family Fam t :: *
type instance Fam () = ()

data GADT a where
    GADT :: GADT ()

fun :: GADT a -> Fam a
fun GADT = ()

-- 
Dave Menendez <dave at zednenem.com>
<http://www.eyrie.org/~zednenem/>