On Tue, Sep 23, 2008 at 1:44 PM, Chris Kuklewicz <haskell@list.mightyreason.com> wrote:
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 <dave@zednenem.com> <http://www.eyrie.org/~zednenem/>