Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

型システムの不変条件

FIXME: このファイルでは、ソルバーだけでなく、型システム全体の不変条件について説明します

型システムが常に真であることを保証するもの、つまり他の言語や型システムから望まれたり期待されたりする不変条件は数多くあります。残念ながら、そのかなり多くは現在の Rust では成り立ちません。これは設計上の根本的な理由による場合もあれば、バグによる場合もあり、将来変更される可能性があります。

型システムに取り組むとき、また型システムを利用するときに何を仮定できるのかを知っておくことは重要です。そのため、ここではコア型システムの不変条件について、網羅的ではなく非公式なリストを示します。

  • ✅: この不変条件はおおむね成り立ちますが、いくつか奇妙な例外や現在のバグがあります
  • ❌: この不変条件は成り立たず、将来成り立つ可能性も低いです。健全性のために依存してはならず、依存する場合は非常に注意する必要があります

wf(X) は wf(normalize(X)) を含意する ✅

エイリアスを含む型が整形式である場合、そのエイリアスを正規化した後も整形式であるべきです。そうでなければ、これらの型について整形式性を再検査する必要があるため、私たちはこれに依存しています。

これは現在、型システムの健全性の破れにより成り立っていません: #84533。

リージョンを法とした構造的等価性は意味的等価性を含意する ✅

ある型があり、左辺と右辺の両方で任意のリージョンを一意な推論変数に置き換えた後でそれ自身と等価にした場合、結果として構造的に異なる可能性のある型同士は、それでも互いに等しいべきです。

これは、ゴールが HIR typeck で成功した後に MIR borrowck で失敗するのを防ぐために必要です。この不変条件が破られると、MIR typeck は最終的に ICE で失敗します。

ゴールから得られた推論結果を適用しても、その結果は変わらない ❌

TODO: この不変条件は奇妙な形で定式化されており、詳述する必要があります。 だいたいのところ、私はこの検査がソルバーのバグがある場合にのみ失敗するようにしたいです: https://github.com/rust-lang/rust/blob/2ffeb4636b4ae376f716dc4378a7efb37632dc2d/compiler/rustc_trait_selection/src/solve/eval_ctxt.rs#L391-L407。 この検査を再追加して、どこで壊れるかを見るべきです :3

あるゴールを証明する、型を等価にする、その他何らかの処理を行った後、結果として得られた推論制約を適用し、元の操作をやり直した場合、結果は同じであるべきです。

残念ながら、少なくとも新しいソルバーでは、いくつかの厄介な理由によりこれは成り立ちません。

トレイトソルバーは局所的に健全でなければならない ✅

これは、対応する impl が存在しないゴールに対して、決して成功を返してはならないことを意味します。そうしてしまうと、実装されていないにもかかわらずトレイトが実装されていると仮定することになり、実際の健全性の破れにつながる可能性が非常に高くなります。ゴールを証明するために where 境界を使用する場合、impl はそのアイテムのユーザーによって提供されます。

この不変条件は、リージョン制約を検査する場合にのみ成り立ちます。コヒーレンスにおける暗黙の負のオーバーラップ検査ではリージョン制約を検査しないため、この不変条件はそこで破られています。この検査はトレイトソルバーの完全性に依存しているため、現在のリージョン制約検査である InferCtxt::resolve_regions を使用できません。これは、type outlives ゴールの扱いが不完全であるためです。

空の環境において意味的に等しいエイリアスを正規化すると、一意な型になる ✅

エイリアス型/定数の正規化は、一意な結果を持たなければなりません。そうでないと、安全なコードで簡単に transmute を実装できてしまいます。次の関数があるとき、入力型と出力型が常に同じ具象型へ正規化されることを保証しなければなりません。

#![allow(unused)]
fn main() {
fn foo<T: Trait>(
    x: <T as Trait>::Assoc
) -> <T as Trait>::Assoc {
    x
}
}

現在知られている健全性の破れの問題の多くは、最終的にこの不変条件が破られていることに依存しています。しかし、この不変条件なしに健全な型システムを想像することは非常に困難です。したがって問題は、この不変条件が破られていることであり、私たちが誤ってこれに依存していることではありません。

型システムは完全である ❌

型システムは完全ではありません。 不要な推論制約を追加したり、ゴールが成り立ち得るにもかかわらずエラーにしたりすることがよくあります。

  • メソッド選択
  • opaque 型推論
  • type outlives 制約の扱い
  • トレイトソルバーの候補選択中に、Impl 候補よりも ParamEnv 候補を優先すること

ゴールは HIR typeck 以降も結果を保持する ✅

HIR typeck 中に成功したゴールが、MIR borrowck 中に再評価されたときに失敗すると、ICE が発生します。例: #140211。

HIR typeck 中に成功したゴールが、インスタンス化された後に失敗すると、健全性の破れになります。例: #140212。

この制約を維持しながらも、トレイトソルバーにある程度の不完全性を許容しているのは興味深いことです。「許容される不完全性」と、この不変条件を破る振る舞いとを明確に分離する方法があれば望ましいでしょう。

正規化は結果を変えてはならない

この不変条件は、ジェネリックエイリアスの正規化を可能にするために依存されています。これを破ると、容易に健全性の破れにつながる可能性があります。例: #57893。

ゴールはインスタンス化後もオーバーフローする可能性がある

これは、それらが再帰制限に達し始めると起こります。 また、問題のある発散エイリアスもあります。 これらをどのように扱うべきかは明確ではありません :3

空の環境におけるトレイトゴールは、一意な impl によって証明される ✅

空の環境でトレイトゴールが成り立つ場合、そのゴールを証明するために使用される、一意な impl が存在するべきです。それはユーザー定義の場合も組み込みの場合もあります。これは、一意なメソッドや関連アイテムを選択するために必要です。

ただし、いくつかの場合にはこの不変条件を破っています。その一部はバグによるものであり、一部は設計によるものです。

  • marker traits は、関連アイテムを持たないため、オーバーラップが許可されています
  • specialization は、特殊化 impl がその親とオーバーラップすることを許可します
  • 組み込みのトレイトオブジェクトのトレイト実装は、ユーザー定義 impl とオーバーラップすることがあります: #57893

空でない環境で証明できるゴールは、モノモーフィゼーション中にも成り立つ ✅

あるゴールがジェネリック環境で証明できる場合、完全に具象的な型でインスタンス化し、スコープ内に where 句がない状態でも、そのゴールは成り立つべきです。

これは codegen によって仮定されており、codegen はオーバーフローではない曖昧性に遭遇すると ICE します。この不変条件は現在、specialization（#147507）および marker traits（#149502）によって破られています。

コヒーレンスにおける暗黙の負のオーバーラップ検査中、型システムは完全である ✅

オーバーラップ検査の詳細については、Coherence chapter を参照してください。

コヒーレンスにおける暗黙の負のオーバーラップ検査中、 証明可能なゴールに対して決してエラーを返してはなりません。 そうすると、関連アイテムが異なる可能性のあるオーバーラップした impl が許可され、 他の多くの不変条件が破られます。

この不変条件は、私たちが実際に依存しているものであるにもかかわらず、現在さまざまな形で破られています。 これは非常に壊しやすいため、注意する必要があります。

  • エイリアスの一般化
  • サブタイピングバインダー中の一般化（幸い、コヒーレンスでは悪用できません）

トレイト解決は、ライフタイムが異なることに依存してはならない ✅

あるゴールがライフタイムが異なる場合に成り立つなら、そのライフタイムが同じである場合にも成り立たなければなりません。そうでないと、コード生成中にモノモーフィゼーション後エラーが発生したり、不正な vtable による健全性の破綻が生じたりします。

最初に異なるライフタイムでゴールを証明し、それらが後から等しいと制約される場合にも、一貫しない動作が発生する可能性があります。

本体内のトレイト解決は、ライフタイムが等しいことに依存してはならない ✅

トレイトソルバーでリージョンの等価性に依存する場合にも注意が必要です。 これはコード生成に関しては問題ありません。消去されたリージョンはすべて等しいものとして扱うためです。しかし、 HIR から MIR typeck への過程で等価性の情報を失う可能性があります。

これは現在、新しいソルバーでは成り立っていません: trait-system-refactor-initiative#27。

曖昧性を取り除くと、コンパイルできるものが厳密に増える ❌

理想的には、ものごとがコンパイルできるために曖昧性に依存すべきではありません。 そうしないと、将来の改善が破壊的変更になる原因となります。

不完全性 のため、これは成り立っておらず、 推論を改善すると推論の変更が生じ、既存のプロジェクトを壊す可能性があります。

意味的等価性は構造的等価性を含意する ✅

型システムにおいて 2 つの型が等しいということは、それらのジェネリックパラメーターを具体的な 引数でインスタンス化した後に同じ TypeId を持つことを意味しなければなりません。そうでない場合、それらの異なる TypeId を使ってトレイト選択に影響を与えることができます。

コード生成中は構造的等価性を使って型を検索しますが、これは必ずしも健全性の破綻につながるとは限りません

  • 冗長なメソッドコード生成やバックエンドの型チェックエラーが発生する可能性がある？
  • CTFE のアサーションでもこれに依存しています

意味的に異なる型は異なる TypeId を持つ ✅

意味的に異なる 'static 型は、transmute を避けるために異なる TypeId を必要とします。 たとえば for<'a> fn(&'a str) と fn(&'static str) は異なる TypeId を持たなければなりません。

const 項目の評価は決定的である ✅

const 項目の値は型システムに入力され得るため、const 項目の値がすべてのクレートで常に同じであることが重要です。そうでない場合、「等しい」const 引数を持つ関連型が存在し、それゆえ「等しい」関連型であるにもかかわらず、異なるクレートでコード生成中に正規化されたとき、実際には異なる型になってしまう可能性があります。

特に、これは const 関数 には拡張されません。型システムは const 項目 の結果だけを扱うため、const 項目の最終的な値に影響しない限り、const 関数が非決定的であっても実際には問題ありません。