自从我们上次在类型系统团队更新博客文章中总结我们的进展以来,已经过去半年了。随着下一代 trait 求解器现已在 beta 版中默认用于一致性检查1,是时候进行另一次更新了。下一代 trait 求解器旨在完全取代现有的负责证明 trait 约束、规范化关联类型等的类型系统组件。这应该能修复许多长期存在的(健全性)错误,支持未来的类型系统改进,并提高编译时间。有关更多详细信息,请参阅这篇先前的博客文章。
稳定化在一致性检查中使用新求解器的 FCP 已于四月通过。不幸的是,检查深度递归类型的 auto-trait 约束导致新实现出现指数级膨胀,从而导致 CI 捕获的挂起。修复此挂起需要我们添加一个复杂的缓存优化,以便在保持正确性的同时有效地处理循环2。我们随后合并了稳定化 PR,但在 5 天后回滚了它,因为它导致了nalgebra
中另一个挂起。幸运的是,这次的修复简单得多,这使我们能够在不久后再次稳定化 -Znext-solver=coherence
。
虽然新求解器目前仅用于一致性检查,但这已经消除了一些不一致性和理论上的健全性问题,有关完整摘要,请参阅稳定化报告。如果您遇到任何奇怪的挂起、意外的重叠错误或无用的诊断信息,请在GitHub 上提交 issue。
然后我们将重点再次转移到完全使用新求解器进行自举。我们在这里取得了显著进展,并且能够完整编译 rustc
和 cargo
,使得 try
构建能够成功。我们目前正在调查剩余的编译时间基准测试失败。我们打算开始优化新实现,并测试越来越多的 crate,直到进行完整的crater
运行变得有用。
展望未来
为了解除下一代 trait 求解器稳定化的障碍,我们需要修复多个问题,这些问题也影响了当前实现。这是由于实现之间的细微差异导致新求解器触发了旧求解器避免的错误。新实现工作正确而旧实现不正确的案例不幸地远不如旧实现避免新求解器触发的错误案例那么重要,因为还没有人编写依赖于下一代 trait 求解器行为的代码。
我们还需要投入大量精力改进使用新 trait 求解器时的错误消息。在许多情况下,它们仍然比现状差得多。
我们仍在努力进行首次 crater 运行,并且意识到多个重要问题。我们预计在接下来的几个月内解决大部分问题。因此,虽然我们还没有完全达到 bug 报告有用的阶段,但我们打算很快明确请求对 -Znext-solver=globally
进行测试。要跟踪我们的进展,请查看-Znext-solver
跟踪 issue 或加入我们的 zulip 频道。