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

Question

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?

Answer 1

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.

Answer 2

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.