型システムが難しいのは、健全性が「すべての経路で」を要求するからだ
型システムは難しい、と感じる。Carinaのissue/PRを辿ると、その難しさは規則そのものにはあまり無い。個々の規則は短い — 受け側が合併なら「いずれかに代入可能」、送り側が合併なら「全メンバが代入可能」。難しいのは、健全性が全称命題だということである。
「この型の値は必ずこの検査を通っている」は、すべての経路・すべての段階・すべての表現・すべての境界で成り立って初めて真になる。反例は一箇所あれば足りる。一方でバグ報告は常に一箇所から来て、直すのも一箇所になりやすい。直しは存在命題、要求は全称命題。この非対称が、同じ種類のバグが形を変えて戻ってくる理由になっている。
全称が破れる五つの場所
向き — 同一性と包摂を取り違える
AwsResourceIdを受ける属性にInternetGatewayIdを渡すと拒否された(carina#158)。次に逆向き、一般のArnを特定のIamRoleArnに渡すと拒否された(carina#260)。こちらはiam_role.arnの出力が汎用のArnで型付けされていたのが原因で、issueには「出力をIamRoleArnで型付けし直す」案と「一般から特定への代入を許す」案が並んでいる。後者が不健全であることは、後で#3218が示す。
長さ制約が違うだけのID同士で拒否されたので、String基底のカスタム型を全部相互に互換にした(carina#1796、2026-04-14)。5日後、それがIdentityStoreId → AwsAccountIdの取り違えを通すようになった(carina#2079)。
根は、対称な「互換」で方向のある「代入可能」を判定していたことだった。carina#2091で方向付きのis_assignable_toに置き換えたとき、PRにはこう書かれている。
The existing LSP test
— carina#2091string_based_custom_types_are_compatiblefroze the bug; it is inverted intodistinct_semantic_customs_are_rejected.
試験がバグを仕様として固定していた。そして1か月後、型の同一性を構造化した直後に同じ形の穴がもう一度見つかる(carina#3218)。抽象のaws.Arnが具体のaws.iam.Role.Arnに代入できてしまう — #260で並んでいた二案のうち、採ってはいけない方の挙動である。同日carina#3221で、対称なsame_typeと方向付きのassignable_toが分けられた。
This is essentially Java's array covariance unsoundness, but at the identity-axis level.
— carina#3218
→ 同値関係を方向付き判定に流用すると抽象から具体への代入が漏れる
段階 — 値がまだ無いときの検査
IaCでは値の一部がplan時点で分からない。これを型の外(番兵文字列)に置くと、扱う全箇所が忘れずに処理しなければならない。型の中に入れると、全パターンマッチに波及する。Carinaは「未知」をValue::Unknownに集め(carina#2371)、値の型そのものをConcreteとDeferredに割った(carina#2972)。そのRFCの途中で、一度出した「後段は延期」の判断が撤回されている。
I conflated "validate sub-system has type-level proof" with "the bug class is structurally unrepresentable". They are not the same.
— carina#2972
割った後も穴は残る。検証は参照を解決する前に1回だけ走り、Deferredは素通りする。リテラルなら検査されるのに、同じ値が参照経由で来ると検査されない(carina#3767。2026-09-29に同じ根を持つcarina#3448の重複としてclose)。逆向きの穴もある。パース時の置換で参照がリテラルに化けると出所が消え、String → VpcIdの取り違えが通る。
The same wiring mistake therefore gets two different verdicts depending only on whether the source value happens to be known at parse time.
— carina#3450(open)
型注釈を省略可能にしたOption<TypeExpr>も同じ場所の穴だった。「型が分からない」を型に入れた結果、各消費地点がデフォルトを選ばされ、
the default they all picked is "skip the check entirely", which is unsound.
— carina#2360
→ 「未確定」を表す表現が四つあるのは漸進的型付けの境界が引けていない徴候である / 再配置後に検証がないのは型検査済みIRの不変条件の破壊である / Unknownは二段階の間に開いた窓である
表現 — 同じ値が別の姿で来る
"x"と["x"]、RSA-2048とRSA_2048、属性なしと[]。意味が同じでも表現が違えば、差分は永遠に消えない。IAM条件の単一要素リストをAWSがスカラーに戻すせいで、applyが成功してもplanの差分が残った(carina#2481)。比較器で特例にせず、型レベルの正規形を全層で強制する道が選ばれた。
それでも正規化は片側だけに掛かりやすい。ACM証明書のkey_algorithmを直すためにプロバイダ側へ正規化を足したPR(carina-provider-aws#477)は、マージから1時間半でrevertされた(#480)。本当の原因はcore側の列挙照合が区切り文字を片方向にしか畳んでいなかったことだった(carina#3670)。後に同じ種類がまとめて洗い出されている。
These are one bug class: a comparison where normalization is applied to one side and not the other — which either manufactures a phantom diff or hides a real one.
— carina#3736
境界 — 型が言語をまたぐと消える
WASMプラグインの境界(WIT)を越えられるのはデータだけである。WITに合併型が無かった間、合併はStringに縮退していた(carina#1491)。カスタム型の検証関数は関数ポインタなので越えられず、境界で何もしない検証器に差し替わり、vpc_id = 'test'が通っていた(carina#2354)。型検査が通っていることと、境界の向こうでその型がまだ存在することは別である。
拡張 — 新しい構成子を既存の分岐が知らない
循環スキーマのために参照型Refを足したとき(carina#3340)、懸念はすでに書かれていた — ワイルドカードの腕がRefを黙って受けて型を捨てる。2か月半後、合併のメンバ判定と代入可能性判定がまだRefを知らず、値の検証は通るのに代入検査だけが拒否するという食い違いが見つかった(carina#3757、carina#3762)。
判定器が二系統あるのも同じ構図である。
Risk: fixing one and forgetting the other has already happened repeatedly
— carina#3211(open)
実際、片方では'dev' | 'prod'がInt型の受け側に互換と判定される(carina#2648、open)。
→ 検査器が二系統あるのは設計負債である / 循環スキーマは名前付きμ型で明示展開する / 型名の文字列比較で代入可能性を決めるのは構造を捨てている
緩めても締めても間違える
健全性を守るだけなら全部拒否すればよい。難しさのもう半分は、正しいプログラムを拒否しないこととの綱引きにある。
上の時系列はその振り子だった。名前空間でも同じ往復が起きた。各プロバイダが自前の公称型を持つようにした2日後、aws.AccountIdをawscc.AccountIdに渡すと拒否されることが問題になる。
There is no semantic difference between
— carina#3413aws.AccountIdandawscc.AccountId.
共有する型を4つだけに絞る案はrevertされた(carina#3420)。「何を同じ型と見なすか」は、値の意味で決めるのか出所で決めるのか、という設計判断そのものであり、型検査器の側では決められない。
State ownership belongs in the state layer, not in the type system.
— carina#3420
正規表現の包含のように決定不能な問いも混じる。Carinaは「パターンが違えば保守的に非互換」を選んだ(carina#2218)。これは正しいプログラムの一部を拒否することを、はっきり受け入れた選択である。
解の形は収束している
五つの場所で、修正はだんだん同じ形に寄っていく。一箇所を直すPRが閉じられ、表現を変えて壊れた状態を書けなくするPRに置き換わる。
- 対称な判定を方向付きの判定に置き換える(#2091、#3221)
- 値の型を
Concrete/Deferredに割る(#2972) - 正規化を唯一の関門に移し、それ以外から構築できなくする(carina#3664)
- 透過的な型エイリアスをnewtypeにする(carina#3744)
全称命題を一箇所ずつの修正で守ることはできない。実装言語の型で「すべての経路」を代わりに数えさせるしかない。もう一つの道具は、部分型関係の反射性・推移性・反対称性を性質試験で押さえることで、こちらはまだ無い(carina#3208、open)。
→ typestateで壊れた状態を書けなくする / 部分型関係が公理化されていないと性質の破れを検出できない
根拠の確度
2026-09-29にcarina-rs org配下のissue/PRを検索し、約80件の本文とコメントを読んだ(読んだのはサブエージェントで、要約をもとに書いている)。引用した英文はすべてissue/PR本文にあることを確認済み。「open」と書いたissueの状態は同日にGitHub APIで確認した。
「五つの場所」への分け方と「直しは存在命題、要求は全称命題」という見立ては私の解釈で、issue本文に書かれているわけではない。#3689のように報告者の診断自体が外れていた事例もあり、上の分類に入らない難しさ(症状が型の問題に見えるが原因は別)もある。