未知値の周りは無検査ではない
Unknownの素通しは「未解決の値の周りは無検査」という意味ではない。値が無くても宣言型どうしを照合する別経路の検査が走るため、静的近似が本当に確定できない窓は見かけより狭い。
値なしで走る検査
値が未解決の参照に対しては、参照元属性のスキーマ型をアクセスパス(.field / [idx])に沿って絞り込み、代入先の型へ方向付きの代入可能性で照合する、宣言型ベースの項レベル検査が別経路で走る。この判定は公称識別の包摂に加えて長さ・値域の区間の包含まで見るため、篩型のうち決定可能な断片については宣言レベルで含意(部分型)検査が成立しており、role_arn = role.role_nameのような型違いの参照は値なしで弾ける。
スタックを跨ぐupstream_state参照にも同種の検査がある。型の供給源はstateファイルではなく上流の設定ディレクトリで、そのexports宣言を静的にパースし、export名の存在・宣言型と参照位置の期待型の照合・for / フィールドアクセス / 添字の形状をそれぞれ値なしで検査する。stateのexports自体は型なしのJSON値だが、スタック境界の型付けは設定側の宣言が担う、という構図である。
なおこの検査の被覆には実装上の欠落が確認されている。検査対象は属性のトップレベルに現れた参照だけで、リストや構造体の要素に埋まった同じ型違いの参照は素通りする(carina#2786)。またパース時に値が解決できた参照は具体値へ置換されて出自が消えるため、この検査自体に到達しない(carina#3450)。いずれも設計上の窓ではなく修正可能な欠落である。
真に残る窓は二つだけ
(a) 値依存の篩所属。 参照元の宣言型が代入先の篩より粗い場合(例:宣言上はただのStringを、長さ・パターン付きの型が期待される場所へ補間して渡す場合)、最終値が篩を満たすかは宣言型から決定できない。そして値が確定して代入された後も、Carina自身はどの経路でも再検査しない。代入の時刻は二通りあり、上流stateの値はplan時(ただし検証ステップの後)、リソース出力はapply時だが、どちらの代入点にも検証経路がなく、最終判定はプロバイダAPIのエラーに委ねられる。
(b) 宣言型のない上流exportへの参照。 上流のexports宣言に型注釈がなく推論でも型が取れない場合、比較対象が存在せず型検査はスキップされる。型を書いた境界は検査され、書かなかった所だけ穴が開く。
一方、for変数由来のUnknownなどは型が構文から決まるので窓の外である。
根拠の確度
「Unknownの窓」の範囲は探索中に二度訂正されている。未解決参照への宣言型検査が存在すること、上流参照の型供給源がstateではなく設定ディレクトリであることが、いずれも後から判明した。