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

There are two cases in the definition of f and both match your second type signature:

T0 _ -> True

Here your argument was of type T Bool and your result is a Bool. So this matches your type signature for a ~ Bool.

T1 ->  y

Here your argument was of type T a and your result is y, which is of type a. So this matches the signature for any a.

To understand why this is type safe, just ask yourself the following question: Is there any way that you could call f, such that the result wouldn't match the type signature? Like could you get back anything other than an a if you passed in a T a and a a?

And the answer is: No, there isn't. If you passed in a T0 (meaning a is Bool), you'll get back a Bool. If you passed in a T1 you'll get back the second argument, which is guaranteed to be of type a as well. If you try to call it like f (T1 :: T Int) "notAnInt", it won't compile because the types don't match. In other words: Any application of the function that matches the type signature will produce the correct result type according to the signature. Therefore f is type safe.