[Haskell-cafe] Type family signatures

[Ryan Ingram]

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