Adventures with Types in Haskell: GADT's: why does the following typechecks?

Question

I'm following this lecture by Simon Peyton-Jones on GADT's. There, the following data-type is declared:

data T a where
  T0 :: Bool -> T Bool
  T1 :: T a

And then the question that is asked is what is the type of the following function:

f x y = case x of
          T0 _ -> True
          T1   -> y

To me, it seems the only possible type is:

f :: T a -> Bool -> Bool

However, the following type:

f :: T a -> a -> a

is also valid! And indeed you could use f as follows:

 f (T1) "hello"

My question is why is the second type signature for f valid?

Answer 1

Normally, to type check

case e of
  K1 ... -> e1
  K2 ... -> e2
  ...

it is required that all the expressions ei share a common type.

This is still true when using GADTs, except that in each branch the constructor provides some type equality equations T ~ T' which are known to hold in that branch. Hence, when checking that all ei share a common type, we no longer require their types to be identical, but only to be equal when the type equations hold.

In particular:

f :: T a -> a -> a
f x y = -- we know x :: T a , y :: a
   case x of
      T0 _ -> -- provides a ~ Bool
              True   -- has type Bool
      T1   -> -- provides a ~ a (useless)
              y      -- has type a

Here we need to check Bool ~ a which would be false in general, but here becomes true because we only need to check this under the provided equality a ~ Bool. And, in such case, it becomes true!

(To be honest, the type system does something slightly different, checking instead if both branches are equal to the type declared in the signature (under their known equalities) -- but let me keep it simple. For GADT pattern matching such a signature is always required in some form.)

Note that this is the whole point of GADTs -- they allow to type-check pattern matches whose branches apparently involve different types.