[Haskellcafe] Type family signatures
Simon PeytonJones
simonpj at microsoft.com
Wed Aug 19 05:19:27 EDT 2009
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: haskellcafebounces at haskell.org [mailto:haskellcafebounces at haskell.org] On
 Behalf Of Ryan Ingram
 Sent: 18 August 2009 21:56
 To: Thomas van Noort
 Cc: Haskell Cafe
 Subject: Re: [Haskellcafe] Type family signatures

 On Mon, Aug 17, 2009 at 12:12 AM, Thomas van Noort<thomas at 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 nonrigid variable occurs typechecking this expression:

 foo x = x + (1 :: Int)

 During typechecking/inference, there is a point where the type environment is:

 (+) :: forall a. Num a => a > a > a

 b :: *, nonrigid
 x :: b

 c :: *, nonrigid
 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
 _______________________________________________
 HaskellCafe mailing list
 HaskellCafe at haskell.org
 http://www.haskell.org/mailman/listinfo/haskellcafe
More information about the HaskellCafe
mailing list