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
