On Fri, Aug 14, 2009 at 12:03 PM, Dan Weston wrote:

But presumably he can use a data family instead of a type family to restore injectivity, at the cost of adding an extra wrapped bottom value and one more layer of value constructor?

Actually, you don't even necessarily pay this penalty, since you can put newtypes into data families.

data family Foo a newtype instance Foo () = UnitFoo Int

You do need to add the constructor wrap/unwrapping in code, but they all get erased after typechecking. -- ryan

On Mon, Aug 17, 2009 at 12:12 AM, Thomas van Noort 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

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-bounces@haskell.org [mailto:haskell-cafe-bounces@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 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