Agda性能回归分析：--save-metas选项导致的类型检查效率下降

在Agda 2.7.0版本中，开发者发现了一个显著的性能退化问题。当使用该版本进行类型检查时，某些原本在Agda 2.6.5中能够快速完成的证明过程变得异常缓慢。经过深入调查，发现问题根源在于默认启用的--save-metas选项。

问题现象

在测试案例中，一个简单的自反性证明在Agda 2.7.0中需要数秒才能完成类型检查，而在2.6.5版本中几乎是瞬时完成的。这个证明涉及的目标类型虽然结构清晰，但包含了一些嵌套的函数应用和等式推理。

技术分析

通过二分法定位，最终确定问题源于2f09379734a5a7ed080032866901c5436d67df03提交，该提交将--save-metas设为默认选项。--save-metas选项原本的设计目的是保留未解决的元变量，而不是在类型检查过程中即时展开它们。

进一步测试表明：

1. 使用--no-save-metas选项时，性能问题消失
2. 问题不仅出现在当前测试案例，在其他代码库(TypeTopology)也有类似报告
3. 标准库和立方类型测试中未发现明显性能下降

深层原因

--save-metas选项的核心问题是它改变了Agda处理元变量的策略。在默认情况下，Agda会尝试即时展开元变量，这虽然可能增加编译时间，但能减少最终代码中的间接引用。而启用--save-metas后：

1. 更多的元变量被保留在接口文件中
2. 类型检查时需要处理更多的间接引用
3. 对于某些复杂的依赖类型，这会导致显著的性能下降

解决方案

考虑到实际影响，开发团队决定：

1. 在#7452中恢复--no-save-metas为默认选项
2. 将--save-metas保留为可选功能
3. 未来考虑更智能的元变量处理策略，而不是简单的全保留或全展开

经验教训

这个案例展示了编译器选项默认值改变可能带来的深远影响。特别是：

1. 性能影响可能高度依赖于代码模式
2. 基准测试需要覆盖多样化的代码库
3. 编译器优化有时需要在即时性能和最终代码质量间权衡

对于Agda用户来说，如果遇到意外的性能下降，检查--save-metas选项的状态是一个值得尝试的排查方向。