[Haskell-cafe] Type family signatures

[Thomas van Noort]

Thank your for this elaborate explanation, you made my day!

Thomas

Ryan Ingram wrote:
> 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 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