On Tue, Sep 23, 2008 at 1:44 PM, Chris Kuklewicz
You cannot create a normal function "fun". You can make a type class function
fun :: Class a b => GADT a -> b
data GADT a where GADT :: GADT () GADT2 :: GADT String
-- fun1 :: GADT () -> () -- infers type fun1 g = case g of (GADT :: GADT ()) -> ()
-- fun2 :: GADT String -> Bool -- infers type fun2 g = case g of (GADT2 :: GADT String) -> True
-- "fun" cannot type check. The type of 'g' cannot be both "GADT ()" and "GADT String" -- This is because "fun" is not a member of type class. {- fun g = case g of (GADT :: GADT ()) -> () (GADT2 :: GADT String) -> True -}
It may be that fun cannot type check, but surely it isn't for the
reason you've given.
data Rep a where
Unit :: Rep ()
Int :: Rep Int
zero :: Rep a -> a
zero r = case r of
Unit -> ()
Int -> 0
The type of r is "both" Rep () and Rep Int. No type class needed.
If I had to guess, I'd say the original problem is that any
specialization triggered by the functional dependency happens before
the specialization triggered by pattern matching on the GADT. If I
recall correctly, it is known that GADTs and fundeps don't always work
nicely together.
The example does seem to work if translated to use type families.
type family Fam t :: *
type instance Fam () = ()
data GADT a where
GADT :: GADT ()
fun :: GADT a -> Fam a
fun GADT = ()
--
Dave Menendez