Type classes in GADTs

[Jason Dagit]

On Wed, Oct 29, 2008 at 10:20 PM, C Rodrigues <red5_2 at hotmail.com> wrote:
>
> I discovered that closed type classes can be implicitly defined using GADTs  The GADT value itself acts like a class dictionary.  However, GHC (6.83) doesn't know anything about these type classes, and it won't infer any class memberships.  In the example below, an instance of Eq is not recognized.
>
> So is this within the domain of GHC's type inference, not something it shoud infer, or a bug?
>
> {-# OPTIONS_GHC -XTypeFamilies -XGADTs -XEmptyDataDecls #-}
> module CaseAnalysisOnGADTs where
>
> -- Commutative and associative operators.
> data CAOp a where
>    Sum    :: CAOp Int
>    Disj   :: CAOp Bool
>    Concat :: CAOp String

I guess when you write something like this the type checker doesn't
look at the closed set of types that 'a' can take on.  I don't know
why that would be a problem in your example, but if we did this:

data CAOp a where
   Sum :: CAOp Int
   Disj  :: CAOP Bool
   Concat :: CAOp String
   Weird :: Show a => CAOp a

Now we have a problem, because the set of types for is { Int, Bool,
String, forall a. Show a => a}.  It's not a closed set anymore.  And I
think, but I'm just making this up, that the above set of type must be
hard to reason about.  I think it would essentially be:

data Show a => CAOp a where ...

And GHC won't allow that, presumably for a good reason.  Neat example,
and I hope someone sheds more light on this.

By the way, since you mention ghc6.8.3, does that mean some other
version of GHC permits noEvidenceOfEq to type check?  I tried 6.6.1
but that didn't accept it either.

Jason