再配置後に検証がないのは型検査済みIRの不変条件の破壊である
「well-typedなIRだけがバックエンドに渡る」というのがコンパイラの標準的な契約である。しかしapplyの再配置はIRに新しい値を書き込む。すると問いが立つ:再配置で書き込まれた値は、IRが持っていた型(篩)に対して検証されるのか?
答えは否で、これは確認済みの実バグである(carina#3448)。
検証はplanの早い段階で一度だけ走る。ところが代入の時刻は二通りあり、上流stateの値はその後ろで(plan時に)、リソース出力はapply時に代入される。どちらの代入点にも検証経路がない。違反値はplanの表示に現れてさえ検査されず、プロバイダAPIのエラーとしてapplyの途中で初めて顕在化する。
型システムの側から見ると、これは段階を跨ぐ値の篩所属を最終的に誰も検査していない、ということである。未解決参照に対しては宣言型ベースの代入可能性検査が別経路で走るが、その検査が粗い型を通した場合 — 例えば宣言上はただのStringを、長さ・パターン付きの型が期待される場所へ補間して渡す場合 — 最終値が篩を満たすかは宣言型からは決定できない。値が確定して代入された後も、Carina自身はどの経路でも再検査しない。
コンパイラの言葉で言えば「型検査済み」というIRの不変条件が再配置で破壊可能である、ということになる。そして修正の縫い目も類比から直ちに出る:各再配置点の直後に、書き込んだ値をその穴の型で検証する。
この事例は、値ベース検査の「全数」性が何に対する全数なのかも精密化する。全数なのは検証ステップの時点で値が確定しているものに限られる。静的段階で確定する値、ではない — 検証ステップより後にplan時代入される上流state値は、静的段階の値でありながら検査を免れている。