Today, I got a compiler error when trying to use a lazy pattern when matching on an existential GADT constructor:
An existential or GADT data constructor cannot be used inside a lazy (~) pattern
Why is that limitation? What "bad" stuff could happen, if it were allowed?
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.
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.
