証明木

トレイトソルバー自体は、ゴールが成立するかどうかと必要な制約のみを返しますが、その証明を試みる過程で何が起きたかも知りたい場合があります。トレイトソルバーは通常、コンパイラーの他の部分からはブラックボックスとして扱われるべきですが、その内部を完全に無視することはできないため、そのためのインターフェイスとして「証明木」を提供しています。これを使用するには、ProofTreeVisitor トレイトを実装します。例については既存の実装を参照してください。特に重要な用途として、coherence エラーに対するクレート間の曖昧性の原因、トレイトソルバーのエラー改善、および クロージャーシグネチャの先行推論の計算があります。

証明木の計算

トレイトソルバーは Canonicalization を使用し、ネストされた各ゴールに対して完全に独立した InferCtxt を使用します。診断と rustdoc の auto-traits はどちらも、「ネストされたゴールの中を見る」処理を正しく扱う必要があります。Vec<Vec<?x>>: Debug のようなゴールが与えられた場合、これを exists<T0> Vec<Vec<T0>>: Debug に正規化し、そのゴールを Vec<Vec<?0>>: Debug としてインスタンス化し、ネストされたゴール Vec<?0>: Debug を取得し、これを正規化して exists<T0> Vec<T0>: Debug を取得し、これを Vec<?0>: Debug としてインスタンス化します。その結果、曖昧な ?0: Debug ゴールがネストされます。

証明木は、ProofTreeBuilder を検索グラフに渡すことで計算します。これは、トレイトソルバーの評価ステップを木に変換します。推論変数またはプレースホルダーを使用する任意のデータを保存する際、そのデータは、この計算中に作成されたすべての未制約の推論変数のリストとともに正規化されます。この CanonicalState はその後、証明木をたどる際に親の推論コンテキストでインスタンス化され、推論変数のリストを使用して、この評価中に作成されたすべての正規化された値を接続します。

ソルバーのデバッグ

以前は、ソルバー実装のデバッグにも証明木を使おうとしていました。これには、プログラムから解析する場合とは異なる設計要件があります。トレイトソルバーをデバッグする推奨方法は、tracing を使用することです。トレイトソルバーは、その一般的な「形状」には debug トレーシングレベルのみを使用し、追加の詳細には trace を使用します。したがって、RUSTC_LOG=rustc_next_trait_solver=debug によって大まかな概要が得られ、より正確な情報が必要な場合は RUSTC_LOG=rustc_next_trait_solver=trace を使用できます。