Agda类型系统回归问题：非函数类型应用错误报告优化

在Agda 2.5.4版本中，类型系统在处理非函数类型的应用时出现了一个错误报告退步的问题。这个问题最初由开发者plt-amy在测试中发现并报告，随后由核心开发者andreasabel快速定位并修复。

问题背景

考虑以下Agda代码示例：

open import Agda.Builtin.Nat

record T : Set where
  field
    f : Nat → Nat

foo : T
foo .T.f = suc

test : Nat
test = foo 123

在Agda 2.5.3版本中，类型检查器能够正确地识别出类型错误，并给出合理的错误信息：

T should be a function type, but it isn't
when checking that 123 is a valid argument to a function of type T

然而，从2.5.4版本开始，错误信息变得不直观：

T !=< Nat of type Set
when checking that the inferred type of an application
  T
matches the expected type
  Nat

技术分析

这个问题的本质在于类型检查器在处理函数应用时的逻辑变化。在2.5.4版本中，当检查一个非函数类型的应用时（如将参数123应用于记录类型T），类型检查器没有正确地验证参数数量与函数类型的匹配性。

核心问题出现在Application.hs模块中，具体是在处理函数应用类型检查时，没有充分验证参数数量与目标类型的匹配。正确的做法应该是实现一个"telViewExactly"函数，严格检查可见参数的数量是否与目标类型的要求完全匹配。

修复方案

修复方案主要包括以下改进：

1. 在类型检查过程中增加对参数数量的严格验证
2. 确保在参数数量不匹配时，能够提前终止检查并给出合理的错误信息
3. 恢复2.5.3版本中直观的错误报告行为

修复的核心思想是：在类型检查过程中，如果发现目标类型不是函数类型或者参数数量不匹配，应该立即报错，而不是继续尝试进行类型匹配检查。

潜在风险

开发者andreasabel指出，这个问题可能存在更严重的变体。例如，在某些情况下，对错误目标类型的检查可能会导致元变量的实例化，进而产生更加晦涩难懂的错误信息。这提示我们在类型系统实现中需要特别注意边界条件的处理。

结论

这个问题的快速修复展示了Agda开发团队对用户体验的重视。通过恢复直观的错误信息，可以帮助开发者更快地定位和修复代码中的类型错误。同时，这个案例也提醒我们，在类型系统实现中，参数数量验证是一个需要特别注意的关键环节。

对于Agda用户来说，这个修复意味着在2.5.4及以后版本中，当错误地将非函数类型作为函数应用时，将重新获得清晰明确的错误提示，这大大提升了开发体验。