正如年初的 Types Team 公告帖子 中所宣布的，Types Team 已经开始重新实现 rustc 的 trait solver。这次重构类似于 Chalk，但利用过去几年积累的经验，直接集成到现有代码库中。与 Chalk 不同的是，新的 trait solver 的唯一目标是取代现有实现。我们正在单独进行 a-mir-formality 中的类型系统形式化工作。自该公告发布以来已经过去了半年，这符合 我们路线图 的第一步。

通过重新实现 rustc 的 trait solver，我们能够修复现有实现中的许多微妙 bug 和低效率问题。这应该会带来更快的编译速度和更少的 bug。新的 trait solver 实现还应该解除许多未来更改的阻碍，最显著的是围绕隐式约束 (implied bounds) 和协同归纳 (coinduction) 的改动。例如，它将允许我们移除 当前对 GATs 的许多限制，并修复许多长期存在的不健全 (unsound) 问题，例如 #25860。一些不健全问题将在稳定化时得到修复，而其他问题则需要后续的额外工作。新的 solver 还将启用或极大地简化其他仍在实验中的类型系统扩展，例如 泛型 const 表达式 和 非生命周期绑定。

现状

新的 trait solver 实现可以在 nightly 版本上通过使用 rustc 标志 -Ztrait-solver=next 进行测试。如果只想在一致性检查 (coherence checking) 中使用新的实现，可以使用 -Ztrait-solver=next-coherence。请参阅 其跟踪 issue 中新 trait solver 的当前实现进度。

现在我们已经到了一个阶段，当 feature flag 启用时，我们完全依赖于新的实现。这是一个重要的步骤，因为我们之前仍然依赖旧的 solver 进行 “深度范化 (deep normalization)” 和 “选择 (selection)”。使用新的 trait solver 时，许多 crate 和我们现有的大多数回归测试都能成功编译。

虽然还有大量不常见的 bug，我们目前有两个主要的失败原因

首先，新的 solver 对 impl Trait 采用了稍微不同的方法。对于嵌套的返回位置 impl trait 的情况，例如 fn foo() -> impl Trait<Assoc = impl Sized>，其实现仍然存在问题。研究这种新方法帮助我们发现了现有实现的问题，这使得我们能够在 type_alias_impl_trait 功能稳定化之前完善其设计。

其次，隐式 Unsize 强制转换 (coercion) 的类型推断，例如将 Box<String> 转换为 Box<dyn Display>，依赖于现有 trait solver 的实现细节。我们最近开始在这里模拟现有行为，并在接下来的几周内修复由此导致的大部分剩余问题。

展望未来

在修复当前未解决的问题后，我们计划逐步将 rustc 的部分功能迁移到新的 trait solver 实现，首先在一致性检查 (coherence) 中使用它。我们预计在今年年底将一致性检查迁移到新的实现。将函数的类型检查迁移到新的 trait solver 实现将更具挑战性。这将是最后一个使用旧实现的地方。我们预计在 2024 年更改默认设置，可能会依赖新的 edition 来帮助迁移。

一个主要的挑战将是“不完备性 (incompleteness)”。我们将不完备性作为一个技术术语，用于描述类型系统不必要地指导类型推断的情况。不完备性允许原本模棱两可的代码能够编译，但它也使得 trait 系统依赖于顺序，并可能导致不正确和奇怪的错误。考虑以下示例

fn impl_trait() -> impl Into<u32> {
    0u16
}

fn main() {
    // There are two possible types for `x`:
    // - `u32` by using the "alias bound" of `impl Into<u32>`
    // - `impl Into<u32>`, i.e. `u16`, by using `impl<T> From<T> for T`
    //
    // We infer the type of `x` to be `u32` even though this is not
    // strictly necessary and can even lead to surprising errors.
    let x = impl_trait().into();
    println!("{}", std::mem::size_of_val(&x));
}

我们如何以及何时进行这种推断跳跃，与旧的 trait solver 实现密切相关，这不是我们希望或甚至能够直接复制的东西。我们必须弄清楚如何在将规则适应新实现的同时，尽可能地保持现有行为。这个问题有多复杂，只有在解决更大的问题并开始在启用新实现的情况下运行 crater 时才会显现出来。

另一个主要的障碍将是错误诊断 (error diagnostics)。我们目前依赖旧 trait solver 实现的许多内部细节来向用户发出可操作且有用的错误。这些诊断信息是通过依赖和绕过这些内部细节逐步改进的。我们无法在新 trait solver 实现中简单地重用它们。我们的目标是可选地发出“证明树 (proof trees)”，这是一种 trait 求解过程的内存表示。我们打算在这些证明树之上提供一个简化的 API，然后用于诊断。