David is right that the program should be rejected. To be concrete, as he suggests, suppose type instance Fam Int = Bool type instance Fam Char = Bool
Now suppose that 'unwrap' did typecheck. Then we could write: x :: Fam Int x = GADT 3 True y :: (Char, Bool) y = unwrap x Voila! We started with an Int (3), and managed to return it as the first component of a pair of type (Char,Bool). Ryan's explanation of the type checking process is accurate, but I agree that the error message is horrible. Dimitrios and I are working on a better version of the type checker that will say something more helpful, like Cannot deduce (a ~ a1) from (Fam a ~ Fam a1) which is a lot more useful. Nice example, thank you. Simon | -----Original Message----- | From: haskell-cafe-boun...@haskell.org [mailto:haskell-cafe-boun...@haskell.org] On | Behalf Of Ryan Ingram | Sent: 18 August 2009 21:56 | To: Thomas van Noort | Cc: Haskell Cafe | Subject: Re: [Haskell-cafe] Type family signatures | | On Mon, Aug 17, 2009 at 12:12 AM, Thomas van Noort<tho...@cs.ru.nl> wrote: | > Somehow I didn't receive David's mail, but his explanation makes a lot of | > sense. I'm still wondering how this results in a type error involving rigid | > type variables. | | "rigid" type means the type has been specified by the programmer somehow. | | Desugaring your code a bit, we get: | | GADT :: forall a b. (b ~ Fam a) => a -> b -> GADT b | | Notice that this is an existential type that partially hides "a"; all | we know about "a" after unwrapping this type is that (Fam a ~ b). | | unwrap :: forall a b. (b ~ Fam a) => GADT b -> (a,b) | unwrap (GADT x y) = (x,y) | | So, the type signature of unwrap fixes "a" and "b" to be supplied by | the caller. Then the pattern match on GADT needs a type variable for | the existential, so a new "a1" is invented. These are rigid because | they cannot be further refined by the typechecker; the typechecker | cannot unify them with other types, like "a1 ~ Int", or "a1 ~ a". | | An example of a non-rigid variable occurs type-checking this expression: | | foo x = x + (1 :: Int) | | During type-checking/inference, there is a point where the type environment is: | | (+) :: forall a. Num a => a -> a -> a | | b :: *, non-rigid | x :: b | | c :: *, non-rigid | foo :: b -> c | | Then (+) gets instantiated at Int and forces "b" and "c" to be Int. | | In your case, during the typechecking of unwrap, we have: | | unwrap :: forall a b. (b ~ Fam a) => GADT b -> (a,b) | a :: *, rigid | b :: *, rigid | (b ~ Fam a) | | -- From the pattern match on GADT: | a1 :: *, rigid | x :: a1 | y :: b | (b ~ Fam a1) | | Now the typechecker wants to unify "a" and "a1", and it cannot, | because they are rigid. If one of them was still open, we could unify | it with the other. | | The type equalities give us (Fam a ~ Fam a1), but that does not give | us (a ~ a1). If Fam was a data type or data family, we would know it | is injective and be able to derive (a ~ a1), but it is a type family, | so we are stuck. | | -- ryan | _______________________________________________ | Haskell-Cafe mailing list | Haskell-Cafe@haskell.org | http://www.haskell.org/mailman/listinfo/haskell-cafe _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe