今天，当在现有的GADT构造函数上进行匹配时，尝试使用惰性模式时遇到了一个编译器错误:
为什么有这个限制？如果允许的话，会发生什么“坏”的事情？
最佳答案
考虑
data EQ a b where
Refl :: EQ a a
如果我们可以定义
transport :: Eq a b -> a -> b
transport ~Refl a = a
那我们就可以
transport undefined :: a -> b
从而获得
transport undefined True = True :: Int -> Int
然后是崩溃，而不是尝试对
undefined进行头部归一化时遇到的更为平稳的失败。GADT数据代表有关类型的证据，因此虚假的GADT数据威胁到类型安全。必须严格要求他们来验证证据:在存在底部的情况下，您不能相信未经评估的计算。
关于haskell - 为什么不能在惰性模式中使用GADT/现有数据构造函数？，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/14538255/