GADTs and functional dependencies

[Jason Dagit]

On Tue, Sep 23, 2008 at 9:07 AM, Wolfgang Jeltsch
<g9ks157k at acme.softbase.org> wrote:
> Hello,
>
> please consider the following code:
>
>> {-# LANGUAGE GADTs, MultiParamTypeClasses, FunctionalDependencies #-}
>>
>> data GADT a where
>>
>>     GADT :: GADT ()
>>
>> class Class a b | a -> b
>>
>> instance Class () ()
>>
>> fun :: (Class a b) => GADT a -> b
>> fun GADT = ()
>
> I'd expect this to work but unfortunately, using GHC 6.8.2, it fails with the
> following message:
>
>> FDGADT.hs:12:11:
>>     Couldn't match expected type `b' against inferred type `()'
>>       `b' is a rigid type variable bound by
>>           the type signature for `fun' at FDGADT.hs:11:16
>>     In the expression: ()
>>     In the definition of `fun': fun GADT = ()
>
> What's the reason for this?  Is there a workaround?  Does this work in 6.8.3
> or 6.10.1?

There is one workaround that I can think of.  Use a data type to get
the level of polymorphism you need.

You could create a data type to hold b and return that instead of the naked b.

data Any where
  Any :: a -> Any

Now you could say,
fun :: GADT a -> Any

If you go with this existential solution you'll probably want to add
type class constraints to the 'a' in Any so that you can recover
enough about the type to use the value later.

Jason