GADTs and functional dependencies

[Wolfgang Jeltsch]

Am Dienstag, 23. September 2008 18:19 schrieben Sie:
> On Tue, Sep 23, 2008 at 6:07 PM, 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:
>
> 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.  ;-) 

Best wishes,
Wolfgang