Type classes in GADTs

C Rodrigues red5_2 at hotmail.com
Thu Oct 30 01:20:43 EDT 2008

I discovered that closed type classes can be implicitly defined using GADTs.  The GADT value itself acts like a class dictionary.  However, GHC (6.8.3) 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

{- For any non-bottom value of type 'CAOp a', the value will have type
-- CAOp Int, CAOp Bool, or CAOp String.  Int, Bool, and String are all
-- members of Eq.  Therefore, if we have a non-bottom value of type
-- 'CAOp a' then 'a' is a member of Eq.

data D a = D !(CAOp a) (a, a)

-- However, GHC won't figure this out.

noEvidenceOfEq :: D a -> Bool
noEvidenceOfEq (D op (e1, e2)) = e1 == e2 -- Error, no instance (Eq a)

-- Unless you force it to do case analysis on constructors.

evidenceOfEq :: CAOp a -> a -> a -> Bool
evidenceOfEq Sum    = (==)
evidenceOfEq Disj   = (==)
evidenceOfEq Concat = (==)

-- Then you can use the result from that, but GHC still won't
-- recognize it as an Eq instance.

useEvidenceOfEq :: D a -> Bool
useEvidenceOfEq (D op (e1, e2)) = evidenceOfEq op e1 e2
You live life beyond your PC. So now Windows goes beyond your PC.

More information about the Glasgow-haskell-users mailing list