再配置後に検証がないのは型検査済みIRの不変条件の破壊である
「well-typedなIRだけがバックエンドに渡る」というのがコンパイラの標準的な契約である。しかしapplyの再配置はIRに新しい値を書き込む。すると問いが立つ:再配置で書き込まれた値は、IRが持っていた型(篩)に対して検証されるのか?
Carinaでは長くこの検証が無く、確認済みの実バグだった(carina#3448、2026-10に解決)。
検証はplanの早い段階で一度だけ走っていた。ところが代入の時刻は二通りあり、上流stateの値はその後ろで(plan時に)、リソース出力はapply時に代入される。どちらの代入点にも検証経路がなかった。違反値はplanの表示に現れてさえ検査されず、プロバイダAPIのエラーとしてapplyの途中で初めて顕在化した。
型システムの側から見ると、これは段階を跨ぐ値の篩所属を最終的に誰も検査していなかった、ということである。未解決参照に対しては宣言型ベースの代入可能性検査が別経路で走るが、その検査が粗い型を通した場合 — 例えば宣言上はただのStringを、長さ・パターン付きの型が期待される場所へ補間して渡す場合 — 最終値が篩を満たすかは宣言型からは決定できない。値が確定して代入された後に検査し直さなければ、篩所属は誰も確かめない。
コンパイラの言葉で言えば「型検査済み」というIRの不変条件が再配置で破壊可能である、ということになる。そして修正の縫い目も類比から直ちに出る:各再配置点の直後に、書き込んだ値をその穴の型で検証する。
直し方は類比どおりだった
修正(carina#3825、carina#3846)は、各再配置点の後に検証を置き、さらに検証を通っていない値をプロバイダに渡せない型にした。
- plan: 参照を解決した値を、正規化の前にschemaの制約で検査する。違反はplanエラーになり、どの参照から来た値かも示す。
- apply: applyで初めて分かった属性は、プロバイダに送る直前に検査する。送信用の値(
ProviderReady<T>)は検査付きの関数でしか作れない。 - provider設定: 上流の値を代入した後に検査する(
ProviderReadyConfig)。
信頼境界を越えて入ってきた値を、使う直前に検証する形である(信頼境界を越えるデータは境界で再検証する)。applyまで値が決まらないものをどう扱うかは、hybrid type checkingの「キャストを挿入する」に当たる(判定できない部分型は、拒否も受理もせず実行時の検査に回す)。
この事例は、値ベース検査の「全数」性が何に対する全数なのかも精密化する。全数なのは検証ステップの時点で値が確定しているものに限られる。静的段階で確定する値、ではない — 検証ステップより後にplan時代入される上流state値は、静的段階の値でありながら検査を免れていた。
根拠の確度
修正の内容はPR carina#3825とcarina#3846の説明による。#3846は#3448の筋書き(上流stateの値を補間してS3のバケット名に渡す)をそのまま回帰テストにしている。2026-11-07時点のmainで確認した。