Re: GADTs and functional dependencies

On Tue, Sep 23, 2008 at 9:36 AM, Wolfgang Jeltsch wrote:

Am Dienstag, 23. September 2008 18:19 schrieben Sie:

...

On Tue, Sep 23, 2008 at 6:07 PM, Wolfgang Jeltsch

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:

bear in mind that the only instance you defined is

instance Class () ()

which doesn't involve your GADT at all.

This is correct. (It's only a trimmed-down example, after all.)

...

Maybe you meant something like:

instance Class (GADT a) ()

No, I didn't.

...

Moreover, your fun cannot typecheck, regardless of using MPTC or GADTs. The unit constructor, (), has type () and not b.

Pattern matching against the data constructor GADT specializes a to (). Since Class uses a functional dependency, it is clear that b has to be (). So it should typecheck. At least, I want it to. ;-)

I'm re-reading what you said after my first reply. I'm inserting types in places that may not be valid in Haskell... You're saying that the types should be like this: fun :: (Class a b) => GADT a -> b fun (GADT :: GADT ()) = () So, now I'm more inclined to agree with you than before. And suppose we added this: data GADT a where GADT :: GADT () GADT2 :: GADT String Now I would expect this: fun :: (Class a b) => GADT a -> b fun (GADT :: GADT ()) = () fun (GADT2 :: GADT String) = -- I can't put anything here till I add more instances of Class Now, I'm too confused about how this should work. Jason