Type classes in GADTs

[Daniil Elovkov]

Jason Dagit wrote:
> 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 ...
> 

I agree with Jason here. Actually we can think of quite a lot of examples where the type checker _can_ know something what we see as obvious. But that something is a special case of a more general situation which is far less obvious and knowing it may require serious program analysis.

Then, regarding handling some special cases, I think it's a matter of keeping type checker predictable and clean.

In this particular case, handling this situation would require type checker to look at the _values_ of the given datatype, which as I understand Haskell type checker doesn't. If we later add members to CAOp the valid program may become invalid, though the "signature" of CAOp hasn't changed. That doesn't look good. Not all members of CAOp may be exported from a module, that would have to be taken into account as well, probably.

In your example, why not just do

traditionalEvidenceOfEq :: Eq a => D a -> Bool


--
Daniil Elovkov