Why GADT/existential data constructors cannot be used in lazy patterns?

With "normal" data, you can skip checking the constructor during pattern-matching, on the understanding that when you try to use the data from the pattern, it might turn out to not exist, thus throwing an exception at you.

With a GADT, the type signature potentially changes depending on which constructor is present. We need to know about types at compile-time; it's no good not checking the constructor until you need the values. If you do, you might have a type mismatch error. And that, potentially, means your program crashing with a segmentation fault (or worse). Haskell programs should never segfault.

Consider

data EQ a b where
  Refl :: EQ a a

If we could define

transport :: Eq a b -> a -> b
transport ~Refl a = a

then we could have

transport undefined :: a -> b

and thus acquire

transport undefined True = True :: Int -> Int

and then a crash, rather than the more graceful failure you get when trying to head-normalise the undefined.

GADT data represent evidence about types, so bogus GADT data threaten type safety. It is necessary to be strict with them to validate that evidence: you can't trust unevaluated computations in the presence of bottom.