Type classes in GADTs
Jason Dagit
dagit at codersbase.com
Thu Oct 30 03:01:41 EDT 2008
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
More information about the Glasgow-haskell-users
mailing list