Haskell用GADT实现Lambda转DeBrujin索引出现非穷尽模式错误

你遇到的非穷尽模式报错是拼写失误直接导致的：

• 你定义LambdaTerm的App构造器对应的处理分支时，把函数名transform拼写成了transfrom（字母s和f顺序写反）
• 这就导致实际生效的transform函数只覆盖了Var、Abs两个构造器的处理逻辑，App的处理逻辑被归属到了另一个完全不相关、从未被调用的transfrom函数中
• 当你调用transform [] t1时，t1是App构造的项，匹配不到transform的任何分支，就触发了非穷尽模式异常

把拼错的函数名改对即可，额外的类型标注也可以省略，GADT的类型推导可自动处理对应逻辑：

transform e (App t1 t2) = AppI trans1 trans2
  where
    trans1 = transform e t1
    trans2 = transform e t2

修复后调用transform [] t1即可正确输出(λ.0)(y)，和你预设的t1'结构完全一致。

内容的提问来源于stack exchange，提问作者flyingsheep