静的解析 (static analysis)

Hikari の静的解析は、評価を開始する前にソースを検査して問題を報告する。次の層から成る。

前提: 型注釈の文法・実行時照合は language-spec.md §17、エラーの三層モデルは同 §16。型検査が診断と併せて出す型消去の証明（実行時照合を外してよい注釈位置の判定）が何を約束するかは language-spec.md §17、その判定規則は ../internals/type-erasure.md。各コマンド（hikari check / hikari build / LSP ほか）の挙動は hikari-command.md。

本書で繰り返す用語

型検査（§2〜§3）は一貫して次の方針を採る。個別の規則ではこの語彙を前提に簡潔に書く。

• 健全 (sound): 報告する診断はすべて正しい。すなわち 誤検出（false positive）を出さない。
• 不完全 (incomplete): 静的に確定しない箇所は見逃す（false negative を許容）。
• 漸進的 (gradual): 型が確定しない箇所は動的に扱い、実行時照合に委ねる。
• 「到達すれば確実に panic」: その箇所が実行されれば必ず language-spec.md §16.2 の型的 panic になると静的に確定できること。規則が立つ 2 つの根拠の一方で、もう一方が下記の契約系（§2.4）。
• 契約系: 到達してもその地点では panic しないが、宣言された型・述語・網羅性という契約に反する箇所を実行前に塞ぐ診断。破れが現れるのは後続の読み出し・await・呼び出しで、その地点に実行時 backstop が無いこともある（§2.4）。
• 素通し: 静的に確定しない箇所を検査から外して通すこと。各規則の「素通し条件」がその一覧で、これが誤検出ゼロを担保する。
• backstop: gradual 境界（明示的に書いた Any）と、静的型が確定しない受信者で、実行時照合（language-spec.md §17 冒頭）が逸脱を捕捉すること。静的に閉じた領域では検査が先に報告するため、backstop が初めて働くのは gradual 境界を跨いだ逸脱に限られる。
• Any / Unknown: Any は言語の型（任意の値を受ける gradual top）。Unknown は「静的型を確定できなかった」内部状態で、型としては露出しない（hover に出ないだけ）。どちらが絡む照合も素通しする。

1. 構文層の一括検査（実行開始前）

実行（hikari <file> / hikari build）と LSP 診断の前に、entry ファイルを起点とした到達可能な全モジュールを一括で構文検査する。構文層のみを対象とし、1 件でも見つかれば実行を開始しない（exit 1）。

静的エラーとして検出するもの

• 構文エラー: entry および import 先の各ファイルのパースエラー。
• 動的 import — import <対象> := "path" の := 右辺が文字列リテラルでないもの（変数・文字列補間 "${...}"・bare 識別子・任意式）— もパーサーが弾く。リテラル限定によりモジュールグラフを実行前に静的確定できる。
• import の配置: import は宣言形（type / enum と同型）で、ファイルトップレベルの宣言位置にのみ書ける。関数本体・入れ子リテラル内部の import はパーサーが構文エラーにする（配置は文法で担保。別途の placement 検査は持たない）。
• type / enum の配置: 宣言であり式ではない（language-spec.md §1.5）。文/スロット宣言の位置（body 領域・slot-list 領域。import と違い入れ子リテラル内も可）にのみ書け、式の位置（部分式・:= / = の右辺・引数）に現れるとパーサーが構文エラーにする。
• ファイルレベルの構造（language-spec.md §13.1）。ファイル全体が 1 つの slot-list 領域なので、次の 2 つを弾く。
• (a) ファイルレベルの |: 領域を分けるパイプはファイルには現れない（入れ子リテラルの | は従来どおり）。パーサーが構文エラーにする
• (b) 既定値を持たないトップレベルのスロット宣言（name: Type だけの形）: ファイルオブジェクトはロードで完成するため、未束縛スロットを埋める呼び出し側が居ない（analyze で検出）
• import 先不在: import リテラルが解決したパスにファイルが無い場合（analyze で検出。これだけは構文層でなく解決層の検査）。language-spec.md §16.1 の「ファイル不在 = 回復可能エラー」は fs.read 等プログラムが明示的に行う I/O への指針であり、モジュール解決には適用しない（欠落モジュールはロード時の静的エラーである）。
• 未知の標準ライブラリモジュール: import <対象> := "std:<name>" の <name> が std/index.md に無い場合（analyze で検出）。解決層の静的エラーで、回復可能にはしない。
• third-party パッケージ解決の失敗: import <対象> := "pkg:<alias>" で次のいずれか（analyze で検出）。解決層の静的エラー。
• (a) その .hika を含むパッケージにマニフェストが無い
• (b) <alias> がマニフェストの deps に無い
• (c) 解決先がキャッシュに未取得（この場合は取得コマンド hikari get の実行を案内する）
• 詳細は packages.md。
• export の不正（language-spec.md §13.2、analyze で検出）。次のいずれも静的エラー。
• (a) export { ... } の要素に bare 識別子以外（変数・文字列・補間・任意式）が含まれる
• (b) 列挙した名前がトップレベル member として未定義
• (c) 同一ファイルに export が 2 個以上存在
• (d) export の列挙内に同名の重複
• (e) export がファイルトップレベル以外（入れ子リテラルの内部）に出現
• 空の名前リスト export {} はエラーではない — 「何も公開しない」と名乗る形である（language-spec.md §13.2）。(a) は要素の綴りを見る規則なので、要素が 0 個のリストは当たらない。

検出しないもの（従来どおり panic / 回復可能）

• 未定義参照・arity 不一致 → panic（language-spec.md §16.2）。型不一致も実行時 panic だが、hikari check / LSP はこれに加えて「到達すれば確実に型不一致 panic になる」箇所を実行前に検出する（§2）。
• 循環 import → 実行時に検出（language-spec.md §13.4）。静的検査はグラフを 1 度だけ辿って終了し、循環自体は報告しない。

REPL は対象外: 行単位評価のため一括構文検査は行わない（import のリテラル制約はパース時に常に効く）。

2. 静的型検査

2.1 検査の保証と適用範囲

型注釈の照合は実行時に走る（language-spec.md §17 冒頭）が、静的検査はそれに加えて、実行前に型の不一致と契約違反を検出する。照合は language-spec.md §17.4 の表に従い、静的に分かる型同士で行う。

本節の検査は全実行系に無条件で適用する — hikari <path>（ファイル実行）・hikari eval・hikari test・hikari build・REPL・LSP・hikari check のいずれも同じ水準で検査し、診断が 1 件でもあれば評価・生成を行わない（exit code は §1 / hikari-command.md §5.5・check.md と同じ。0=クリーン、1=型/構文エラー）。水準を下げる手段は無い — 一部の規則だけを外す入口も、ファイル単位で有効・無効を切り替える header 属性（language-spec.md §13.1）も持たない。検査は 1 つで、書き手から見て切り替わる段は無い。

検査の保証

保証は次の 2 本立てである。

(1) 健全・不完全・誤検出ゼロ: 報告する診断はすべて正しく、静的に確定しない箇所は素通しする（漸進的型付け）。各規則の「素通し条件」がその一覧で、素通しした逸脱は実行時照合が backstop になる。

(2) class b の健全性: 検査が診断ゼロで通れば、チェッカーが具体型（非 Any・非 Unknown）を割り当てた各評価点で値が実行時にその型と整合し、Any を経由しない領域では language-spec.md §16.2 の型的 panic（型不一致・no such slot/method・arity 不一致・未定義参照）が起きない。Any 境界の逸脱は実行時照合が backstop。判定原則は「imprecision（Any に倒す箇所）は塞がず、unsoundness（具体型を assert して受理したのに backstop も無く panic しうる箇所）だけを塞ぐ」。可変状態（可変スロットと std の可変な器）についてこの基準を成立させるのは §2.10 で、その分担は同節「可変状態と健全性」に集約する。

規則が立つ 2 つの根拠

個々の規則は次のどちらかを根拠に立つ。本書は規則ごとにどちらであるかを書く。

• 「到達すれば確実に panic」: その箇所が実行されれば必ず language-spec.md §16.2 の型的 panic になると静的に確定できる。実行時に同じ地点で現れる不一致を実行前に見せるもので、§2.4 の注釈照合・§2.7 のメンバー解決のうち値が後から slot を増やせない型の受信者・§2.8 の演算子と適用がこの群にあたる。
• 契約系: 到達してもその地点では panic しない。破れが現れるのは後続の読み出し・await・呼び出しであり、そこに実行時 backstop が無いこともある。§2.5 の Any 規律・§2.6 の宣言型の契約・§2.7 のメンバー解決のうち record の受信者・§2.9 の収束と網羅性・§2.10 の可変状態・§2.11 の refinement がこの群で、class b の健全性はここが支える。

分類は診断の重大度も適用範囲も変えない（どちらも Error で、どちらも全実行系にかかる。§5）。違うのは素通し条件の引き方だけである — 「到達すれば確実に panic」の規則は実行時にその地点で落ちる形だけを対象にし、契約系の規則は実行時照合が素通しする位置（Future の payload・結果型を宣言しない関数値・可変な器への書き込みの引数など）にも及ぶ。どちらの群も誤検出ゼロは共通の要件で、確定しない箇所は素通しする。

規則の分類は診断の文面には現れない — 検査は常にこの水準で走るため、書き手に示すべき区別が無いからである（language-spec.md 由来の語彙以外のメタ参照を診断に入れないのと同じ方針）。

2.2 静的型の決め方（ローカル推論）

リテラル・リスト・tuple・data オブジェクト・関数リテラル（パラメーター型と結果型）からボトムアップに型を求め、関数本体内では immutable 束縛（:=）と mutable ローカル（=）の推論型を参照する。各構文の扱いを以下に示す。

束縛・代入・アスクリプション

• mutable ローカル（=）: 確立が型を決め、再代入は型を変えない。確立とは未束縛・型なし（前方参照プレースホルダー）・既存型 Unknown の名前への代入で、そこで右辺の推論型（注釈があればその型）を採る。以降の x = v はその型のまま — v の型がどうであれ x の静的型は動かない。
• 理由: 可変ローカルは「同じ型の値を入れ替える入れ物」である。§2.10「可変ローカルの型安定性」が型変更再代入を禁じているので、再代入で型が動くのはおおむねその規則の違反時だけであり、違反を根拠に型を狭めても得るものが無い。確立時の型を保てば、名前の型はその名前の生涯を通じて 1 つに定まる。
• 例外がひとつある。§2.10 が「既確立型を照合の前に広げる」位置では、違反でない正当な再代入でも実際の型は動く。 同節が Never を wildcard として扱い、単一タグを親 enum へ持ち上げるためで、そこでは代入が通ったうえで確立時の型（List(Never) / 単一タグ）が残る。実際の値より広い型ではなく狭いままなので誤検出にはならないが、その分の見逃しが残る。

take := { ss: List(String) | ss.length! }
mutable xs := []   # List(Never) で確立
xs = [1, 2]        # §2.10 は Never を wildcard として通す。型は List(Never) のまま
take(xs)           # 要素型が確定していないので報告しない（見逃し）

確立時に型を確定させたい書き手は注釈を書けばよい（xs: List(String) = []）。

• 帰結として分岐の合流が要らない。枝で再代入されても型が動かないので、if / when / match / while / loop / conduit の枝を跨いで合流すべき型が無い。
• 枝内の := シャドウ・match のアームパターン束縛は外側変数を変えない別束縛である（language-spec.md §6.1）。これは確立の場所が違うだけなので、上の規則から自動的に従う。
• スコープチェーンを遡る更新（language-spec.md §6.1）も同じく型を変えない。確立時に右辺型が静的に不明なら、その名前は型不明のままである。
• 精度は下がる側である（再代入後の狭い型を採らない）が、誤検出は増えない — 静的型が確立時の型より広くなることはないためである。両枝で型を変えた後の読み出し（x = 0 の後両枝で x = "a" / x = "b" として x + 1）は、その形が §2.10 の型変更再代入として代入の位置で報告される。

関数リテラルのパラメーター型・結果型

パラメーター型は各スロットの宣言型を採り、宣言が無い位置は内部名注釈（language-spec.md §17.3 form 2）が関数型ならそのパラメーター型で補う（結果型の gap-filling と対称。両方あればスロットの宣言型を優先する）。補完は内部名注釈のパラメーター数がスロット数と一致するときだけ行う。いずれも無ければ Any。この補完により、値のシグネチャが実行時の構造照合（language-spec.md §17.4）と同じ宣言集合から組まれ、§2.6「inner-name 型と slot/結果型の整合」 / §2.6「関数型注釈と実体シグネチャの整合」の当たりがパラメーター位置でも実行時と揃う。

結果型は language-spec.md §17.3 の結果型注釈（本体末尾アスクリプション・内部名注釈・束縛注釈）があればそれを最優先で採り、無ければ本体末尾式から推論する — パラメーターをその宣言型（無型は Any）で本体スコープに束縛し、先行する immutable ローカル束縛（:=）を畳み込んでから末尾式を型付けする（例: {row: Int, col: Int | esc + "...${row}..."} は esc が String なら結果型 String）。

• 早期 return を含む関数: 末尾式の型と本体中の各 return e 引数 e の型を join して結果型を解く（末尾自体が return e なら fall-through が無いため末尾は数えず return 集合だけ join）。多値 return(a, b) はタプル型。? 演算子の失敗 bail も同じ脱出経路として失敗 variant 型（Result は Err(E)・Option は None、いずれも成功要素は未制約）を寄与する（language-spec.md §16.5）。全経路同型ならその型、割れれば Any、1 つでも型不明なら Unknown（language-spec.md §18.2 のとおり if / when / while / cond などビルトインブロック内 return は外側関数から脱出するため本体の脱出経路に含まれる）。
• 値として格納された関数リテラルの return は除外: slot デフォルト name := {…}・:= / = 束縛の右辺に現れる {…} の本体内 return は外側関数の結果に寄与しない — それらは構築時に実行されず、呼ばれたときその関数自身の境界で取り出される（language-spec.md §18.2）。除外は健全（格納関数の body は外側の評価では走らない）。これにより { inner self, edit := {… return … |} … |} のように関数スロット（メソッド）を束ねたデータオブジェクトを返す関数の結果型が、メソッド内 return との join で Any に潰れず、その record 形に確定する。
• ユーザー定義高階関数へ引数として渡したブロック内の return（本来はそのブロックから脱出し当該関数の結果に寄与しない）はビルトイン制御構文と区別が付かないため依然含めるが、join は余分な型を Any に倒すだけで誤検出を生まない（過剰帰属側は健全）。例: { inner self | when (c) { return false }\ntrue } は return false と末尾 true がともに Bool で結果型 Bool。
• 再帰関数・前方参照（最小不動点）: 前方参照シード（body 領域・slot-list 領域・関数本体のローカル束縛とも）は宣言の AST を控え、参照時にオンデマンドで型解決する。対象は RHS が関数リテラルの宣言だけ — 関数本体は定義時に評価されないため、後方定義の参照が実行時にも正当な唯一の形で、その型の先読みは健全。解決中の再参照（自己再帰・相互再帰の循環）は「パラメーターは宣言どおり・結果 Never」のプレースホルダー関数型に解ける。Never は join の恒等元（§3.3）なので base 経路の型だけが結果へ寄与し、単一パスの最小不動点として結果型が収束する — 値を返しうる経路は必ず有限の呼び出し連鎖の先で非再帰式に行き着くため、base 経路の join が全返却値を覆う。
• 例: f := { n: Int | if(n <= 0, { "done" }, { f(n - 1) }) } は String。相互再帰 is_even / is_odd・ローカル再帰・base case を早期 return で返し末尾が自己呼び出しの形も同様に解ける。
• Never 被演算子の演算・メンバー参照・メソッド呼び出し・関数適用・? は Never を伝播する（値を生まない式の派生も値を生まない）。これにより n * fact(n - 1) のような自己呼び出しの変換式も base 枝の型に収束する。
• 値を返す経路が自己呼び出ししかない関数の結果型は Never（発散）に解ける。再帰呼び出しの実引数はプレースホルダーのパラメーター型（束縛注釈があればその契約）で照合される。
• 束縛注釈が関数型に解ける宣言は、解決中の再参照もその契約型で見る（結果も宣言どおり）。

データオブジェクト・メソッド・要素アクセス

• データオブジェクトの record 型: body 無し・名前 slots のオブジェクトリテラル（{ x: T, y := e |}）は各 slot 型（注釈→デフォルト推論→Any）から成る record 型に推論する。inner-name 付き（{ inner self, x := e |}）でも値自身は同じ record 形（slot から組むか、内部名注釈 { inner self: T | … } があれば T）に確定し、その内部名 self も同じ record 型で本体スコープへ束縛する。これにより inner-name オブジェクトを返す関数（make := { initial | { inner self, … |} }）の結果型が具体 record に解ける。オブジェクトは要素の並びを持たないので（language-spec.md §2.1）、o.0 のような添字アクセスはそもそも解決しない。
• 修飾タグの値: Name.Tag（Name が enum 型値束縛に帰着する形。language-spec.md §17.4）は、payload 無しのタグならそのタグ型そのもの、payload 付きなら payload 型を引数に取る構築子の関数型に推論する。適用 Name.Tag(args) の結果はタグ型。タグはフラット束縛されないので、スロット分解 { Circle } := Shape と修飾形が同じ型を得る（型付けの単一情報源は同じ表）。
• 原始型メソッド（型メソッド）の呼び出し recv.method(args):
• 単相メソッド（戻り型がレシーバーの型ラベルだけで一意）は直接推論（27.to_char() → String、"hi".to_int() → Option(Int)、xs.length() → Int）。
• 多相メソッド（map / first / unwrap / fold / and_then など戻り型が要素型・ペイロード型・ブロック結果型に依存）は §3 の単一化で解く。copy / flatten のように戻り型がレシーバー型そのもの・その入れ子要素型になるものはレシーバー型から直接導く。
• シグネチャを収録しないメソッド（each — block 内の break が任意型で escape しうる）とレシーバー型が確定しない呼び出しは型不明。
• 呼ばずに書いた型メソッド recv.method（language-spec.md §3.10 の「受け手を束縛した値」）は関数型に推論する。シグネチャの receiver をレシーバーの実型と単一化し、残る引数から戻り型への関数型を採る（"hi".length → {| Int }、[1, 2].contains → { Int | Bool }）。引数を取らないメソッドは 0 引数の関数型で、明示 kick m! で走る。受け手のスロットが同名を持てば型メソッドより先にスロットが解決するので、record 受け手はフィールド型が勝つ。実引数の照合は呼び出し形の規則（上記）が担う — 束縛済みメソッドの関数型を汎用の引数照合へ流すと、要素型に依存する引数（List(a).contains(a)）まで照合対象に入って誤検出になる。
• 列挙軸のブロック取りメソッドにブロックリテラルを渡すとき: レシーバーの要素型が分かればブロックの要素パラメーターを要素型で束縛する（List(Int) / Range / Bytes の要素は Int、String の要素は長さ 1 の String、Option(T) の payload は T）。これでブロック本体のローカル推論と hover が要素型を見られる。
• 対象: ブロックのパラメーターで要素そのものを受け取るメソッドに限る — 反復（each / map / filter / flat_map）・述語（find / any / all / count / take_while / drop_while / partition）・射影と比較（sort_by / min_by / max_by / fold / sort_with）、および Option の map / filter / and_then。
• 位置規則: 単一パラメーターのブロックは第 1 パラメーターが要素。fold は (acc, 要素) で、累積パラメーターには先頭引数（初期値）の型を束縛する。sort_with は比較する 2 要素を受けるので両パラメーターが要素型。
• 対象外: or_else / unwrap_or_else のようにブロックが引数を取らない thunk であるもの（書き手がパラメーターを書いても要素は渡らないため、束縛すると誤った型が付く）と、Result / Ordering のブロック取りメソッド（要素型が一意に定まらず、map_err のようにブロックが payload でなくエラー型を受けるものがある）。レシーバーの要素型が確定しない場合も束縛せず型不明のまま置く（保守側）。
• paren 形 recv.method(a, b) と juxtaposition 形 recv.method a b は同じ method call として平坦化し、全引数が揃った呼び出しでだけ要素型を流す。反復メソッド自体の戻り型は §3 の単一化で解く。

注釈の無いブロックパラメーターへ型を流す

注釈の無いブロックパラメーターの静的型には出所が 2 つある。要素型のシード（上記「列挙軸のブロック取りメソッド」）と、呼び先が宣言するブロックパラメーターの型である。どちらも根拠は同じ — 実行時にその型の値が確実にその位置へ渡ることが、呼び先の型から分かる。

後者は次の規則で流す。

• 完全適用のときだけ引く。 部分適用や arity 不一致では、i 番目の実引数がどのパラメーターに当たるかが確定しない。
• 呼び先の関数型のパラメーター i が関数型であり、そのパラメーター型が宣言されているとき、その型を i 番目の実引数のブロックのパラメーターへ位置順に流す。
• 注釈・デフォルトを持つパラメーターは上書きしない。 書き手が書いた型が常に勝つ。
• 素通し条件（型を作らない側へ倒す）: ブロックパラメーターの宣言型が Unknown・明示的な Any・型変数・Never に解ける位置。呼び先が型を述べていない位置であり、そこへ根拠の無い具体型を作ると誤検出を招く。prelude と std の高階関数の多くは型変数のシグネチャを持つので、この素通しが規模を決める。
• 要素型のシードが取れる呼び出しでは、そちらを使う。 受け手の実際の型から計算する分具体的である。
• 流すのは宣言型そのもので、refinement 型（language-spec.md §17.7）を基底へ潰さない。潰すと、その値を再び同じ refinement の位置へ渡したときに述語を証明できず refinement-not-proven を誤って報告する。

これが無いと、シグネチャに Borrowed(…) と書いてあってもその型が書き手の未注釈パラメーターへ届かず、§2.14「借用は保存できない」の判定が丸ごと素通しになる。

• record/object のフィールドアクセス recv.field: recv の静的型が record/object 型でフィールド field を持つとき、そのフィールド型を採る。フィールドが関数型で呼び出される（recv.field(args)）ときは §3 の単一化で結果型を解く。宣言に無いフィールドへのアクセスは §2.7 が no-such-member として報告する（宣言したメンバー集合が受け手から触れる範囲である。language-spec.md §17.2）。型としては Any（gradual top）を採り、推論はそのまま続ける — 報告済みの 1 件から連鎖して別の規則が鳴るのを避けるためで、値が宣言に無いスロットを持ちうること（幅構造型。同 §17.2）とも整合する。
• 要素アクセス recv.N と整数キーの動的アクセス recv.[i]（language-spec.md §7.4 / §3.10）: recv が要素型を一意に持つ列のときその要素型を採る — String の要素は長さ 1 の String、Bytes / Range の要素は Int、List(T) の要素は T。添字に依らず一定なので N / i が定数でなくても確定する。Tuple は要素ごとに型が異なるため、添字が静的に定数の整数のときだけその位置の要素型を採る。動的アクセス recv.[k] のキー k が静的に Int と分からない場合は型不明。これにより ch := s.0 の後 ch.code() → Int のように要素アクセスの連鎖が解ける。

import 先モジュールの型

いずれも record 型として扱い、mod.member(args) の戻り型まで §3 の単一化で解ける。循環 import・解決不能な import は Any。record 型の組み方は import 種別で分かれる。

• 相対 import（import mod := "path.hika"）: import 先ファイルのトップレベル slot 束縛から成る record 型（各 slot 型は import 先を本規則で推論）。分解 import import { a, b } := "..." も各名前を対応 slot 型で束縛する。import 先に export { n1, … }（language-spec.md §13.2）があれば record 型は列挙した名前（exported member 集合）だけに絞る。exported でない slot への mod.x（§2.7）や分解 import（§2.7）は、exported member 集合に無い名前として no such slot を報告する。
• third-party（pkg:）: pkg:<alias> は相手パッケージの入口 .hika に解決される（packages.md）ので、入口ファイルから相対 import と同じく record 型を組む。未取得（キャッシュ不在）は Any。
• 標準ライブラリ（std:）: 多くがネイティブ実装で .hika ソースを持たないため、処理系が保持する構造化型シグネチャ（std 各書のメンバー表に対応）から record 型を組む（例: import t := "std:time" で t.of({…}) → Result(Instant)、(t.of({…})).unwrap! → Instant）。
• std:time の不透明型 Instant / Date / Time / Duration は名目型として推論語彙に加える。これらは std:time が export する型メンバー（§13 のモジュール型 export と同機構）で、t.Instant と修飾参照するか import { Instant } := "std:time" で取り出して型注釈に書ける（x: t.Instant・mk: {Int | t.Duration}）。
• 不透明性は保たれる — 参照できるのは名目型名だけで、内部表現へのアクセスはコンストラクターとメソッド経由に限られ、match inst { Instant(ms) => … } のようなペイロード分解はできない。推論器内部では各々固有の型メソッド表を持ち inst.year! → Int・inst.add(dur) → Instant・a.diff(b) → Duration のように戻り型を解く。
• std:http/client の Response・std:random の Generator は record/object 値ゆえ record 型扱い（専用の名目型は設けない）。曜日タグ（t.Monday 等）は Weekday を表す Variant 値。
• メンバー関数のパラメーター型は各書のメンバー表（hover に出るシグネチャ）を単一情報源とする。 実引数の照合（§2.5「呼び出しの引数型」）はこの型に対して行われるので、メンバー表が実装より狭いと正当な呼び出しを弾く。不透明型のメソッドも同じ表で照合する（c.write(42) → argument 1 of write expects Bytes, got Int）— 受け手がモジュール関数か不透明ハンドルかで検査の有無が割れない。ただし型引数を持つ器（Array / InsertionMap / ScratchMap / SortedMap / OrderedSet）だけは要素型を join で解く近似なので、キーを取る口（get / remove / contains）を照合すると型の違うキーで引ける器（引き当ては ==）を弾く。器で照合するのは §2.10 の書き込みの口（set / push / update）に限る。多相なメンバーは Any ではなく型変数で書く — List(Any) は可変コンテナー位置の不変性（§2.10）により List(Cell) を受け付けないので、要素型を問わないなら List(a) と書く。パラメーター型を解決できないメンバーは照合を丸ごと素通しする（誤検出ゼロ）。

Any（gradual top）の伝播と確定不能式

• Any の伝播: 受信者・被演算子が Any の派生操作はすべて Any を結果とする — フィールド参照 any.field・位置/動的アクセス any.N / any.[k]・型メソッド呼び出し any.method(args)・算術/連結演算 any + x 等。Any はあらゆる操作を受理する gradual top なので、その結果も Any であって Unknown ではない（報告もしない）。これにより結果型が Any の関数戻り値（layout(…)）のフィールドを連鎖して引く箇所が Unknown に落ちず素通しする。
• 例外: String 連結 +: 片辺が String と確定すれば、もう片辺が Any でも結果は String。String の + は連結専用で非 String との + は panic（language-spec.md §7.2）するため、到達すれば確実に String だから（アスクリプションと同型の漸進的精緻化）。これにより無型パラメーターとの連結（"note not found: " + id — id は Any）が String に解け、Err("…" + id) の payload が Any に倒れない。数値算術（- * / % および両辺非 String の +）は引き続き Any を伝播する。
• 短絡演算子の値は常に Bool: && / || は両辺 Bool 必須でスロット上書き不可（§2.8）のため、式が値を生めばその値は確実に Bool（さもなくば実行時 panic）— 被演算子の型に依らず Bool に確定する（== / != の常時 Bool、String 連結の精緻化と同じ論法）。左辺は短絡に関わらず必ず評価されるため左辺が Never（発散）なら式も Never。右辺の Never は左辺の短絡で回避されうるため伝播しない。
• 原始スカラーの中置 matches の値は Bool: v matches T は universal method matches に落ち、受け手が同名スロットを持てば結果は上書きされうる（値型は確定不能）。受け手が確定原始スカラー（Int/Float/String/Bool/Bytes/Range）ならスロットを持てない閉じた型で、組込 matches が確実に Bool を返す（順序比較の精緻化と同じ論法）。右辺は型コンテキスト（language-spec.md §17.1）なので結果型に関わらない。
• 原始スカラーの順序比較の値は Bool: < / <= / > / >= は universal method compare に落ち一般には上書きされうる（値型は確定不能）が、両辺が確定原始スカラーで妥当な同型組合せ（§2.8。Int/Float/String/Bool の同型）なら compare スロットを持てない閉じた型で組込比較に落ち、式が値を生めば確実に Bool（== / && の常時 Bool と同じ論法）。妥当でない組合せは実行時 panic（§2.8 で報告）のため値を生まず対象外、非原始・Any・Unknown が絡む辺は確定不能のまま。
• レコード更新 + の値は合成 record 型: 両辺が record 型なら結果はフィールドを右勝ちでマージした record 型に確定する（language-spec.md §7.4.1、値の合成と同じ右勝ち規則。左のうち右に無い名前→右の全名前の順、同名は右の型で上書き）。到達すれば結果値はそのフィールド集合を確実に持つため（r + { field := v |} のレコード更新の精緻化）。片辺が Any なら結果も Any（§2.2 冒頭）、List 同士は要素 join の List（既存）。
• 上の 2 規則で解けないオブジェクト合成 + の値は Any: 両辺が合成できるオブジェクト形（関数・record・List）でありながら record 同士でも List 同士でもない + は、関数の合成（language-spec.md §7.4.1）が典型である。合成した値は「値が埋まったスロット」と「未束縛スロット」が同居し、body は片側から継承する — 関数型（引数と結果しか持たない）にも record 型（フィールドしか持たない）にも書き下せない。型語彙で言える最も近い型として Any（gradual top）を採る。「値ではあるが形は記述できない」ことの表明であり、Unknown（まだ解いていない）とは区別する。合成でない +（数値・String・非オブジェクト）は従来どおり。
• 確定できない式: 一般の関数呼び出しの結果・多相メソッド・（Any でない受信者で）フィールドを確定できないメンバーアクセス・演算子の不明な組合せ・右辺型が静的に不明な mutable ローカルなどは型不明として扱い、不明が絡む照合は素通しする。

2.3 条件による型の絞り込み（フロー絞り込み）

if / when / while の条件に書いた matches テストと比較述語から、その条件が真である枝の中でだけ主語の静的型を絞る。v が Any でも if (v matches Int) { … } の中では Int として型付けされ、Int に無いメソッドの呼び出しが §2.7 で報告される。絞り込みは枝の子スコープへの上書きとして実装し、型システムには交差型・差集合型を導入しない。

• 対象の枝: if の then 枝・if の else 枝・when / while の本体。then 枝と when / while 本体では条件が真、else 枝では条件が偽と分かっている。if は else を省いた 2 引数形も対象で、その場合は then 枝だけを絞り込む（綴りの違いで絞り込みの有無が割れると、§2.11「境界の証明義務」がそれを「証明できない」として鳴らす）。枝がサンクリテラルでない（変数経由で本体が見えない）場合は対象外（保守側）。
• 対象の主語: 裸の識別子に束縛されたもの。r.field のような path は対象外。絞り込んだ型が古びる原因は「枝の実行中に主語が別の値へ差し替わる」ことだけなので、それが起きないと確証できる束縛だけを主語にする。
• 再代入されない束縛（immutable）は無条件に対象。:= 宣言・bare 必須スロット（＝パラメーター）・match の アームパターン束縛（値コンストラクターの payload Some(x)、レコードパターンのスロット { code }、型付き束縛 name: T、およびタプル要素に入れ子で現れるそれら。prelude.md §8.4）が該当する。差し替えが言語仕様上起きないため無効化の機構が要らない（language-spec.md §6.1）。
• 可変ローカル（=）は、その名前を所有するフレーム本体の入れ子リテラル（サンク・関数リテラル）のどこにもその名前への代入が無いときだけ対象。枝の本体はフレーム本体から見て入れ子リテラルなので、この 1 つの条件が「枝の中で直接代入される」形と「枝の中で呼んだクロージャがスコープチェインを遡って書き換える」形（language-spec.md §6.1）の両方を塞ぐ。フレーム本体の文の位置にある代入（v = a の後に if (v matches Int) { … } と続く形）は枝の実行中には走らないので、絞り込みを妨げない。複合代入（v += 1）と分解代入も代入として数える。
• 条件の分解: v matches T と v.matches(T) の両記法、および下記の比較述語を葉とし、&& は両辺の事実の和（同名で型が食い違う組は到達不能な枝なのでどちらにも絞らず落とす。ただし落とすのは真に交わらない型の組だけで、refinement の事実とその基底型の事実が同名に立つ組は refinement が基底型の部分型なので〔language-spec.md §17.7〕refinement を採る — if (v matches Int && v > 0) の v は refinement { v: Int | v > 0 } になる）、|| は両辺に共通する名前だけを残して和型（OneOf）へ持ち上げ、.not()（postfix 短縮 .not! を含む）は極性を反転する。否定の内側ではド・モルガンにより && と || の扱いが入れ替わる。述語 T が静的に型値へ解決できない場合はその葉から事実を作らない（保守側）。
• 比較述語の葉: 比較式のうち、両辺が決定可能断片の算術式へ落ち、そこに現れる自由な識別子がただひとつであるものを葉とし、その識別子を主語として「主語は refinement { 主語名: 基底 | その条件 } に一致する」という正の事実を生む（language-spec.md §17.7。基底は分岐前の主語の静的型）。断片の算術は変数・length!・整数リテラルを項とし、+ / - / 定数倍の * / 定数除数の / と % で組み立てたものである。x > 0 / x.length! > 0 に加え x + 1 > 0 / x * 2 <= 10 / x % 2 == 0 / x / 3 > 1 が葉になる。自由な識別子が 2 つ以上ある比較は葉にしない（x > y）— 絞り込み先の refinement は自由変数を持てないため、単一変数に閉じた条件だけが述語になれる。

述語スロット名には主語の名前をそのまま使う — 条件の原文がそのまま述語の原文になり、診断に出たとき書き手が書いた条件と読み比べられる。同じ名前に複数の事実が立てば述語の論理積へまとめるので、x: Int に対する if (x > 0 && x < 10) は refinement { x: Int | x > 0 && x < 10 } の 1 つになる（主語名がスロット名を兼ねるため述語は自由変数を持たない。language-spec.md §17.7）。否定も同じ枠で閉じる — 極性が負のときは比較を反転してやはり正の事実にする（x > 0 の否定は x <= 0）。差集合型が無くても refinement としてそのまま書けるので、下の「否定の事実による差し引き」の制約（閉じた union に限る）は比較述語の葉には及ばず、else 枝でも絞り込みが健全に効く。主語の静的型が基底として確定しないとき、定数側がまとめられないとき、述語が language-spec.md §17.7 の決定可能断片の外に出るときは、その葉から事実を作らない（保守側）。

比較の葉は両辺が断片の算術式へ落ちることを要求するので、String / Bool 定数との比較（s == "x" / b == true）は算術式にならず葉にならない — 断片としては書ける形（language-spec.md §17.7 の未解釈定数）だが、絞り込みは受けない（見逃し側）。

自由な識別子が 2 つの比較は「関係の事実」になる。 i < xs.length! のように両辺が断片の算術式へ落ち、そこに現れる自由な識別子がちょうど 2 つである比較は、型に落とさない事実として枝の中に持つ。上の単一変数の葉が主語の静的型を refinement で上書きするのに対し、こちらはどの名前の型も変えない — 変えられないからである（refinement の述語は自由変数を持てない。language-spec.md §17.7）。

値を型に載せるのではなく、解析の環境に置く。 i の型は Int のまま、xs の型は List(T) のままである。したがって Inspect（language-spec.md §17.4）にもホバーにも現れない。関係の事実を読むのは §2.11 の証明義務だけで、そこでは他の材料と同じ連言の一部になる。判定手続きは項を場所ごとに独立した未解釈の定数として扱う（language-spec.md §17.7）ので、項が別々の名前に根ざしていても線形系の上では同じ扱いである。

3 つ以上は葉にしない。 材料が増えるほど判定の句が増え、断片の判定が打ち切りにかかりやすくなる。2 つに限るのは添字の上限（i < xs.length!）と下限が 2 項で書ける形だからで、必要が出たときに広げる。

Float の比較は葉になる。 片辺が Float リテラルまたは Float の定数式（language-spec.md §17.7 の「Float の定数式」。1 つの定数へまとめられる形）で、他辺が単一の識別子である比較 6 種（< / <= / > / >= / == / !=）を葉とし、その識別子を主語として refinement { 主語名: Float | その条件 } の正の事実を生む。上の整数の葉と違い算術式は許さない — 変数を含む Float 算術は断片外だからである（language-spec.md §17.7）。Float の順序は §9.4 の全順序で、-0.0 と 0.0 は別の値である。したがって f != 0.0 は f が -0.0 であることを排除しない — 両方を除くには f != 0.0 && f != -0.0 と書く（&& は事実の和なので、この形は 1 つの述語へまとめられる）。

定数はどちらの辺に書いてもよい — 0 < x は x > 0 へ演算子を鏡映して正準化する。綴りの違いで絞り込みの有無が割れると、§2.11「境界の証明義務」がそれを「証明できない」として鳴らしてしまい、書き手には直しようが無い。

主語に x.length! を許すのは、length! が断片の組込 measure（language-spec.md §17.7）で、主語そのものではなくその測度だけを制約するためである。NonEmpty := refinement { s: String | s.length! > 0 } のような型は、これが無いと断片内の絞り込みが 1 つも存在しなくなる。

• String のメソッド述語の葉: 条件が s.contains("@") / s.starts_with("https://") / s.ends_with(".com")（引数は文字列リテラル）のときも同じ枠で正の事実を生む。主語の分岐前の型が String に確定するときに限る — 同名のメソッドは List（要素の等値）・Bytes（部分バイト列）・Range（算術判定）にもあり意味が違うので、型を見ずに部分列として解釈すると誤った事実を立ててしまう（断片の側の同じ制約は language-spec.md §17.7）。極性が負のときは .not() を付けた原文に揃える（s.contains("@").not()）。引数が空文字列の述語は恒真なので事実を生まない。

• 裸の Bool 変数と is_empty! の葉: 条件が裸の Bool 識別子そのもの（if (b) { … }。主語の分岐前の型が Bool に確定するときに限る）か、x.is_empty! のときも同じ枠で正の事実を生む。どちらも決定可能断片が受理する述語の綴り（前者は b == true、後者は length! == 0 へ正規化される。language-spec.md §17.7）であり、比較で書いた条件（s.length! > 0）と相互に証明できる。

• match アーム主語の絞り込み: match v { … } の主語が上の「対象の主語」を満たす裸の識別子であるとき、各アームの body で主語そのものを絞る。主語が式や path のときは対象外（保守側）。レコードパターンへ絞るときは下記「幅と封印」に従い封印マークを落とす。
• 正の事実: そのアームのパターンが型値へ解決できるときに立てる。パターンが複数（OR パターン）のアーム からは立てない — 正の事実としては和型に持ち上げないと健全でないためである（保守側）。catch-all アーム（_・裸の識別子）も正の事実を持たない。
• 否定の事実: アーム N の body では、アーム 1..N−1 のうちガードを持たない アームのパターンを否定として立てる。アーム N に到達したことが意味するのは「先行アームがすべて外れた」ではなく「先行アームの（パターン ∧ ガード）がすべて偽だった」である。ガード付きアームは「パターンは当たったがガードが偽だった」経路でこのアームへ落ちてくるので、そのパターンを否定にすると健全でない（match v { String | c => … ; _ => … } の _ 側の v は、c が偽なら String でありうる）。網羅性の判定（§2.9「closed variant の match に網羅性を要求」「到達しえないアーム・冗長な catch-all」）が「ガード付きアームは非貢献」と扱うのと同じ規律である。ガードを持たない OR パターンのアームは、全パターンをそのまま否定に使える。否定の差し引きは下記の条件（閉じた union・排他型）にそのまま従うので、record・List(T)・Option(T) の選択肢は差し引かない。
• アームガード: pattern | guard => body の guard が真であることは body の中で分かっているので、条件と同じ分解で正の事実を立てる。主語はアームパターンが束縛した名前でも外側の名前でもよい。パターンが立てた事実と同名に立つ場合は述語の論理積へまとめる。
• 絞り込み先の基底との整合: 比較述語の制約は整数領域の意味論で解釈されるため、載せてよい基底は制約の中身で決まる。Int 基底には変数の線形制約・剰余類制約を、String / Bytes / List 基底には length! だけを主語にした制約を、String 基底にはさらにメソッド述語（contains / starts_with / ends_with）を、Bool 基底には裸の Bool 変数が生む真偽定数との等価比較を載せる。これ以外の組（Any 基底に v > 0 を載せる等 — 値が Float 0.5 のとき「v >= 1」がエラーになる）では絞り込まない（保守側）。
• 事実の極性: 葉は極性に応じて正の事実（「主語は T に一致する」）と否定の事実（「主語は T に一致しない」）のどちらかを生む。正の事実は絞り込み先の型として使い、否定の事実は下の差し引きにかける。同じ名前に正と否定が同時に付く場合は正を採り（正の方が強い）、正の事実と同じ型の否定が同時に立つ組（v matches Int && (v matches Int).not()）は到達不能なのでその名前を落とす。
• 正の事実に使える型: 正の事実の型として使えるのは、実行時の型テストがその型への所属を決める型に限る。照合が真を返しても値がその型に属するとは限らない位置を構造のどこかに含む型は、正の事実として使わない。決めないと定めている位置は次の 3 つである。
• 関数型 — 宣言の無い引数・結果位置は素通しする（language-spec.md §17.4 の照合表）。f matches {Int | Int} は無注釈の関数にも真を返す。
• Future(T) の payload — await 前に検査しない（同表）。v matches Future(Int) はどの Future にも真を返す。
• 型変数 — 無境界のものは実行時に消去され Any と同じ挙動になる（同 §17.2）。境界付きのものが実行時に確定するのは境界のメンバーであって型変数そのものではない。

これらの位置を主張する型で絞り込むと、検査が実行時に確かめられていない型を主張することになる。さらに型消去の判定（language-spec.md §17）がその位置を「確実に成功する」と見て実行時照合まで外すため、砦も残らない。ジェネリック型の遅延適用（Tree(Int)）は型引数と展開先の両方をこの基準で見て、展開を辿りきれない形は使わない側へ倒す。否定の事実にはこの制限が要らない — 下の差し引きの条件（選択肢と述語がいずれも「値が高々ひとつにしか一致しない型」）が既にこれらの型を除いている。

• 正の事実の適用（交わりの代用）: 正の事実の適用は本来「分岐前の型との交わり」であって置き換えではない — 型システムに交差型を導入しないので置き換えで代用するが、置き換えは分岐前の型が持っていた情報を落としうる。そこで確実に狭める組にだけ適用し、それ以外はその正の事実を使わない（保守側）。確実に狭めるのは次の組だけで、これ以外はすべて据え置く。
• 分岐前の型と同一。
• 分岐前の型が閉じた union で、正の事実の型がその選択肢の部分集合。
• 分岐前の型が Any。
• record 同士 — 分岐前の型の各フィールドが正の事実の型にもあり、その型も確実に狭い。matches は record を幅で照合するので、フィールドが増える方が狭い型になる（正の事実の型の側にフィールドが増えるのは可）。
• 同じ型コンストラクターの共変コンテナー（List(T) / Option(T) / Result(T, E) / tuple）— 要素ごとに確実に狭い。
• 分岐前の型が refinement のときは、上のいずれかに加えて正の事実の型がその述語を含意すること。

この定義の帰結として、Any への「絞り込み」、v: Int に union 別名 OneOf(Int, String) を当てる形、分岐前の型が refinement のときに述語を持たない素の型名（Int）を当てる形は、いずれも狭めないので使わない。record 同士・Variant タグ同士のようにどちらが狭いとも言えない組も据え置く — どちらを採っても相手側の情報を落とすので、分岐前の型を保つ方が情報を失わない。正の事実を使わない場合も、同じ名前に立つ否定の事実や比較述語の制約は通常どおり適用され、分岐前の型に据え置くのは名前に何も適用できなかったときだけである。

• 否定の事実による差し引き: 否定の事実は、分岐前の型が閉じた union（OneOf(...)） であり、かつ union の各選択肢と述語がいずれも「値が高々ひとつにしか一致しない型」であるときに限り、一致する選択肢を union から取り除く形で絞り込む。この条件を満たすのは原始型（Int / Float / String / Bool / Bytes / Range）・Unit・同じ enum に属する Variant タグ（タグ同一性は所属 enum を含む。language-spec.md §17.4）で、いずれも「値はどれかひとつのタグ・原始型に属する」ため差し引きが健全に定義できる。if (v matches Int) { … } { … } で v: OneOf(Int, String) なら else 枝の v は String になる。record・List(T)・Option(T) のような幅や要素で重なりうる型は選択肢にも述語にも許さない（例えば空リストは List(Int) にも List(String) にも一致するため、取り除くと健全でない）。取り除いた結果が空になる（＝その枝が到達不能）場合と、取り除ける選択肢が無い場合は絞り込まず分岐前の型に据え置く（保守側）。
• ガード節（フロー感応）: 枝が確実に脱出する分岐文の後では、その分岐を通過したことが事実になる。when (x <= 0) { return 0 } の後続の文では x > 0 が成り立つ。これは枝の子スコープではなく、同じ body のそれ以降の兄弟文への上書きになる。次をすべて満たすときだけ事実を立てる。
• 文の形 — 式文が when (cond) { … }・2 引数 if (cond) { … }・3 引数 if (cond) { … } { … } のいずれかで、枝がサンクリテラルであること。while は本体が 0 回実行されうるので対象外。
• 確実に脱出する枝があること — その枝の全経路が return で脱出する。1 経路でも脱出しないなら事実を立てない（保守側）。両方の枝が脱出する形は以降が到達不能なので、やはり事実を立てない。? bail は数えない — postfix ? が脱出するのは被演算子が失敗 variant のときだけで、成功なら中身に開いて後続へ進む（language-spec.md §16.5）ので「必ず脱出する」にならない（脱出しうる箇所を集める §2.6「宣言結果型と全脱出経路の整合」とはここが逆向きである）。この判定自体は枝の末尾文だけを見る保守的なもので、when / while / match の末尾は辿らない — match の全アームが return で脱出する形を末尾に置いても、それだけでは「全経路脱出」と数えない（見逃し側）。
• 主語 — 上の「対象の主語」を満たすこと。
• 無効化 — 次の 3 つで事実を落とす。いずれも可変ローカルにだけ効く条件で、immutable な束縛は言語仕様上代入の対象になれないため無効化が要らない。上の可変ローカルの条件（入れ子リテラルに代入が無いこと）は「枝の実行中に走らない」ことを根拠に文位置の代入を許していたが、フロー感応ではその前提が成り立たないので、これらを足して代入の全経路を覆う。
• ガード以降の兄弟文にその名前への文位置の代入があれば、その代入位置以降は落とす。
• 枝の内側の代入でも落とす。 match のアームや if / when の枝の中でその名前へ代入したら、そのフレームに載っている事実を全部落とす（内側の 1 枚だけではない）。枝が走るかどうかは静的に決まらないので、走ったかもしれない代入の後で古い事実を使ってはいけない。落とす向きは事実を減らす側なので診断は増えない。
• 入れ子リテラルの本体には持ち込まない。フロー感応な事実が有効なのは、それを立てたフレームの直線的な文の並びの中だけである — 入れ子リテラルは値として格納されうるので、その本体が走るのは事実を古びさせる代入より後でありうる（when (x > 0) { return 0 } の後に g := {| … x … } と書き、さらに後で x = 5 して g() を呼ぶ形）。

立てる極性は脱出した枝の反対側である — when (c) { return … } と if (c) { return … } は負（c が偽）、if (c) { … } { return … } は正。3 引数形を含めるのは、除くと if (c) { return 1 } と if (c) { return 1 } { } で絞り込みの有無が割れるためである（綴りの違いで割れると§2.11「境界の証明義務」が書き手に直しようの無い診断を出す）。

• 適用先: 枝の本体スコープに絞り込み後の型で束縛を上書きする。効くのはチェッカーの逐次診断（枝内の文の型照合）である。枝の外へは持ち出さない — 可変ローカルの型は確立時に決まって動かないので（§2.2）、枝を跨いで型を運ぶ機構そのものが無い。
• 幅と封印: matches は record を幅構造型として照合する（宣言に無いスロットを持つ値でも真。language-spec.md §2.4）ため、record 述語へ絞り込むときは封印マーク（Sealed）を落とす。封印を持ち込むと枝内の正当なスロットアクセスが契約外アクセス（§2.7「封印契約に対する契約外アクセス（importer 側）」）として誤検出になる。
• 絞り込み先が分岐前の型と確実に非整合な場合（その枝が到達不能）は、絞り込まず分岐前の型に据え置く（保守側）。枝内で同名のスロット・:= を宣言していれば、そちらのシャドウが素直に勝つ。

将来枠

次は絞り込まない。絞り込みそのものはいずれも見逃し側（誤検出を出さない）に倒れるので、対応範囲が広がるまでは静的型が分岐前のまま据え置かれるだけである。

• path 主語: r.field のような path を主語とする条件は対象外。path は受信者が別名で参照されうる（s := r の後 s.field = …）ほか、枝の中で呼んだ任意の関数からも書き換えられるため、「枝の実行中に差し替わらない」ことを確証するには別名解析と呼び出し先の副作用解析が要る。
• 可変ローカル: 上記「対象の主語」の条件を満たすものだけが対象。入れ子リテラルのどこかで代入される名前は、その代入が枝の実行中に走るかを問わず絞り込まない（呼び出しの有無までは追わない）。
• 比較述語以外の Bool 式: 葉になるのは上記が列挙した形（比較述語・裸の Bool 変数・is_empty!・String のメソッド述語）に限る。それ以外は対象外 — ユーザー関数の呼び出しを含む述語、refinement_opaque が要る断片外の述語（非線形項・Float 算術）、path を主語とする述語、自由な識別子が 2 つ以上ある比較（x > y。単一変数に閉じた refinement で表せない）がこれにあたる。

§2.11「境界の証明義務」では極性が反転する。同項は「述語の充足を証明できない」ことを診断にするので、§2.3 が事実を記録しなかった形は「材料が足りない」＝診断になる。そのため同項は安全網を持つ — 境界へ渡る式が、その境界を支配する if / when / while の条件に現れる名前を含むなら報告しない（支配する条件の定義と、網が反証を抑止しないことは §2.11）。本節の対応範囲が広がるほど、この安全網に頼る箇所は減る。

2.4 型注釈と値の照合

型注釈位置に来る値と、注釈そのものを検査する。いずれも「到達すれば確実に panic」を根拠とする。

型注釈と値の不一致

v の静的型が確定し、注釈型と確実に非互換のとき報告する。

• 型注釈つき束縛 x: T := v / x: T = v。
• 型注釈つき分解 a: T, … := tup（タプル要素位置が確定）/ { x: T } := rec（record フィールド型が確定）。
• 型が静的に分かる関数への完全適用 f(args) の引数（f := {a: T | …} のような注釈付きパラメーター）。
• タグの値コンストラクターへの完全適用 Circle(arg) の payload（宣言 payload 型を引数型とみなす）。Circle("hello") のようなリテラル違反を検出する。修飾形 Shape.Circle(arg)（受信者が enum 型値束縛と確定するとき）も同じ payload 型で検査する。実行時は構築時 panic（language-spec.md §17.4）が backstop。
• 所属 enum が違う同名タグ。タグの同定はタグ名だけでなく所属 enumを含む（language-spec.md §17.4 のタグ namespace 分離）ので、enum A := OneOf(Tag(Int), …) の位置に別の enum B := Tag(Int) のタグを置いた形は実行時照合が確実に落とす。
• 双方の所属が判明して食い違うときだけ報告する。片側でも所属が分からなければ素通しする（誤検出ゼロ）。組込の Option / Result / Ordering / Control のタグは所属を持たない規約なので、この判定にかからない。
• 分岐合流の整合判定（§3.4 の consistent）が親 enum 型とタグの対に対して既に同じ線引きを使っている。同じ食い違いが位置によって別の答えにならないよう、判定の形を揃える。
• スロットのデフォルト確定 {x: T := d |}（mutable 前置の可変スロットも同じ）。
• 注釈位置に確実に型でない値が来る場合（追跡可能な範囲で）。
• レコードリテラルの宣言フィールド欠落 p: { x: Int, y: Int |} := { x := 1 |}。宣言型が record で、値がデータオブジェクトリテラル（body も inner-name も持たない { … |}）のとき、宣言フィールドに対応するスロットがリテラルに無ければ報告する。実行時照合（language-spec.md §17.5）はスロットが読めない時点で失敗するので、到達すれば確実に panic する。
• リテラルだからこそ断定できる: record 型は幅構造型なので、型の側のフィールド一覧は値が持つスロットの一覧ではない。一方リテラルのスロット集合は構文でそのまま決まり、body も inner-name も無い以上後から増えない。型同士の照合が欠落を保守側に扱うのに対し、ここは確実な不一致として断定できる。
• universal method 名は除く（apply_when / compare / copy / inspect / matches / reference_equals）。組込ベースラインが自前スロットより先に効く（language-spec.md §17.5）ため、スロットが無くても照合は通りうる。
• スロットはあるが既定値式を持たない形（{ x: Int |} のようなパラメータースロット）は対象外とする（保守側の見逃し）。
• 本判定は既存のリテラルの構文形への降下（宣言型が record・リスト・タプル・variant payload のとき、値が対応するリテラルなら内側の式へ降りて要素ごとに照合する経路）の一部である。降下は §2.11「境界の証明義務」・§2.10「可変コンテナー位置の不変性」・§2.10「可変な器への書き込みの要素型照合」が共有するので、欠落の照合もそれらへ同時に効く。
• 診断は既存の型不一致（type-mismatch）として、注釈位置に宣言型と値の静的型を並べて出す。フィールド型の食い違いと同じ形で、欠落だけ別の語彙にはしない。

型注釈位置の未定義型名・非型式

型注釈位置（束縛・スロット・分解・結果型アスクリプション expr: T）に次が来る場合、到達すれば確実に実行時エラーになるため報告する。文言は実行時の型評価と一致させる。

型位置に書いた [...] はここへ来ない — 角括弧は List のリテラルであって型位置には現れないので、静的検査より手前で構文解析が brackets are not a type; for a list write List(T), for a record write { name: T |} と断る（language-spec.md §17.2）。

型位置の {} に書いたエントリも同じく手前で断る。 型位置のエントリは name: 型 と bare 識別子で尽きる（language-spec.md §17.2）ので、既定値つきスロット（name := 型 / 可変スロット mutable name := 型）は slot defaults are not a type entry; for a field write { name: T |}、structural 型の名前でない位置エントリ（{ 1 |}）は a bare type entry must be a name; for a field write { name: T |} と断る。断らないと型欄が空のまま検査を素通りし、hikari check は通るのに走らせると落ちる（型を引く位置で止まる）。関数型（{ … | 結果型 }）の位置エントリはパラメーター型なので名前に限らず、List(Int) も { Int | Int } も書ける。

• 未定義の型名（スコープに束縛の無い大文字始まりの参照）— undefined: <name>
• enum の payload の型名は走査の終わりに判定する。 宣言はファイルを上から辿る途中で読むので、その時点では import が解けていないことがある（enum P := OneOf(Rep(Html)) の Html を後段の import が供給する形）。そこで断ると正しいコードを undefined と呼ぶことになるので、走査を終えてから解き直し、なお解けないものだけを報告する。名前でない型式（型変数・適用形）は断じない
• 型になり得ない式（数値・文字列リテラル・演算子式など）— not a valid type expression
• モジュールが公開しない型メンバー参照 mod.Name（下記「モジュール型メンバーの解決」）
• 非構造型への埋め込み（{ Int |}）— {...} 形の bare 大文字エントリは埋め込みで、
  取り込む先は構造型でなければならない。
  <name> is not a structural type; cannot embed; for a list of <name>, write List(<name>)
• function 型で名前付きと位置を混ぜた slot-list（{ x: Int, String | Int }）—
  位置エントリとスロットは別の列に載るので、混在した綴りは書いた順を保てない
  （language-spec.md §17.3）。関数型のパラメーター名は照合に参加しない
  ので、混在を許して並び順の規則を読者に負わせるより書けなくする方が安い。
  function type mixes positional and named parameters; write all positional ({ Int, String | R }) or all named ({ a: Int, b: String | R })

結果型を持つ形だけが対象である — 結果型の無い { Ord, x: Int |} は record 型で、
bare 大文字は埋め込み（上記）であって位置パラメーターではない。

報告するのは構造型ではあり得ないと確定した型（原始型・Unit・List(T)・タプル・
関数型・Option / Result / Future / OneOf・Ordering / Control）に限る。基底が
構造型になり得る形（refinement・多重度・効果・名目型・ジェネリック宣言・遅延適用）と、
静的な解決が実行時の型値と一対一に対応しない形（Any / Never・型変数・タグ）は
「型名の解決順」の誤検出ゼロ優先に従って素通しし、実行時の照合を後ろ盾にする。

モジュール型メンバーの解決

型注釈位置の mod.Name は、mod がモジュールを丸ごと束縛した名前（別名連鎖 m2 := m1
も辿る）に帰着し、import が解決できてモジュール record を組めるとき、Name をそのモジュール
の型メンバー集合から引く。引けなければ undefined: mod.Name を報告する。

モジュールの型メンバー集合は静的に閉じる。相対 import・third-party（pkg:）は import 先の
トップレベル型宣言で、std: は処理系が持つ型メンバー表で確定し、どちらも別の視点がより
多くの型を宣言していることが無い（§2.7「存在しないメソッド／スロット」の import 先
モジュールと同じ根拠）。集合に無い綴りは到達すれば必ず実行時に失敗する。

• std: も対象。§2.7 が std: 名前空間の値メンバー検査を当面見送るのとは別で、
  こちらは型メンバー表そのものが権威なので閉じた集合として扱える。
• 値スロットにある名前は素通し。Name が型メンバーに無くても公開スロット（値）にある
  ときは報告しない（decimal.Ceiling のような Variant 値を型位置に書いた形）。上記
  「型名の解決順」の「型と確定できなければ Unknown」に従い、誤検出ゼロを優先する。
• 素通し条件: §2.7「存在しないメソッド／スロット」の import 先モジュールと同じ —
  循環 import・解決不能な import（既に Any）・mutable 束縛・関数引数/戻り値経由の
  import 値。受信者がモジュール束縛に帰着しない recv.Name（一般の record など）も対象外。

型名の解決順

型位置の識別子は、追跡済みスコープを先に引き、束縛が無いときだけ prelude の型語彙へフォールバックする。

• スコープに束縛がある: その束縛が型値（type / enum 定義・型値を束ねた名前）ならその型を採る。確実に型でないと断定できるときだけ not-a-type を報告し、型と確定できなければ Unknown（素通し）。
• スコープに束縛が無い: prelude が束縛する型語彙（Int / String / List / Error 等）として解決する。

型名は予約語ではなく prelude 束縛の普通の値（language-spec.md §1.2.1・§17.2）なので、書き手が同名を束縛すればそちらが勝つ。type Error := {code: Int |} を書いたファイルの e: Error はその定義を指す。

型語彙の固定セットを先に見てはならない。実行時の注釈は普通の式として評価され、スコープの束縛が勝つ（language-spec.md §17）。静的検査が固定セットを優先すると、同じ注釈が静的検査と実行時で別の型を意味してしまう。しかも型消去（language-spec.md §17）が「証明済み」として実行時照合を外した位置ではその食い違いが表に出ないため、単なる不一致では済まず健全性の穴になる。解決順は実行時と一致していなければならない。

素通し: スコープに束縛はあるが型と確定できない大文字名（型不明の値束縛など）は素通しする（実行時に評価され得るため未定義ではない）。小文字始まりの bare 名は型変数（language-spec.md §17.2）なので対象外。型注釈位置に限った例外であり、値位置の未定義参照は §2.13 が扱う。

型構築子そのものを値位置で束ねた名前（MyList := List）は型値束縛として扱い、以後 MyList(Int) はユーザー定義のジェネリック type と同じ型適用の経路で List(Int) に解ける。型は値（language-spec.md §17.2）なので、実行時も構築子の値を束ねた名前へ型引数を当てられる — prelude の構築子をユーザー定義と別扱いにしないだけである。対象は引数 1 個ちょうどのテンプレートで表せる構築子（List / Option / Future / Type）に限る。Result（1 個または 2 個）と OneOf（可変長）は単一のパラメーター列を持つテンプレートで表せないため対象外で、束ねた名前は型不明のまま（実行時照合が backstop）。同名を書き手が束縛していれば上記「型名の解決順」どおりそちらが勝つ。

型注釈位置の型適用 Name(T)（ジェネリック type / enum のインスタンス化）は宣言のテンプレートへ型引数を代入して解決する。再帰ジェネリック enum（enum Tree(a) := OneOf(Leaf(a), Node(Tree(a), Tree(a)))、language-spec.md §17.4）は実行時と同じ規則で解決する — 宣言中の自己参照 Tree(a) は遅延型適用のまま保持し（無限展開しない）、使用サイトの Tree(Int) は 1 段だけ展開したテンプレートに解く。これにより注釈と値の照合（§2.4）・closed variant の match 網羅性（§3 — 判定時に遅延適用を 1 段ずつ展開）が非再帰ジェネリック enum と同水準で働く。

型構築子の型引数の個数

型引数の個数が宣言と食い違う型適用は type-arity-mismatch を報告する。ジェネリック type / enum の宣言に対してだけでなく、型引数を 1 つも取らない宣言（type P := { a: Int |} に対する P(Int)。実行時の型適用が必ず止める形である）にも、prelude が束縛する型構築子のうち arity が固定のもの——List(T) / Option(T) / Future(T) / Type(T)（いずれも 1 個）・Result(T) と Result(T, E)（1 個または 2 個）・多重度型 AtMostOnce(T) / ExactlyOnce(T) / Borrowed(T) / Consuming(F)（いずれも 1 個。§2.14）・EffectConduit(F)（1 個。§2.15）——にも同じ判定を行う。Effect(T, …) は効果ラベルの個数が可変なので本判定の対象外で、第 1 引数を欠く Effect() だけを type-arity-mismatch とする。個数が合わない適用は実行時の型適用が必ずエラーにするので「到達すれば確実に panic」に当たる。ただし書き手が prelude の構築子と同じ綴りを構築子でない型で覆った形（type List := { n: Int |} を書いた後の x: List(Int)）は対象外である — 注釈の側は実行時も prelude の構築子として解ける（止まるのは値の照合であって型式の評価ではない）ので、断つと実行時に通る注釈を静的に拒むことになる。

可変長の OneOf は対象外。OneOf(A, B, …) は最小 2 個で上限が無いため、個数だけからは不一致を確定できない。引数 0〜1 個の形は実行時にエラーになるが、固定 arity と同じ「N 個ちょうど」の判定に載らないので誤検出ゼロを優先して素通しする（実行時が backstop）。

判定は §2.4 の解決順に従う。書き手が同名を束縛していれば（type List(a, b) := (a, b)）そちらが勝ち、その宣言の arity で判定する。宣言が使用より後ろにある形（前方参照）はその時点で宣言の型引数が分からないので、prelude の arity では判定せず素通しする — 実行時は書き手の宣言が勝つため、prelude の個数で報告すると宣言の位置が使用より後ろというだけで誤検出になる。

2.5 型注釈の規律（暗黙 Any の禁止）

暗黙の Any（型を書かず推論・省略で Any になる位置）は禁止し、Any を意図するなら明示せよ — この 1 つの思想を、名前付き関数の結果型・パラメーター型・値束縛の 3 位置へ適用する。いずれも契約系の診断で、暗黙 Any コンテナーは実行時に panic せず（Any 境界には実行時照合の backstop がある）、class b の健全性を超えた方針上の規律である。

暗黙・明示 Any の許可マトリクス

「明示」と認める書式は位置ごとに定める。下表に許否をまとめる（✓ 許容 / ✗ 禁止）。

「明示」と認める書式が位置で異なる理由: Any を許すのは、書き手が明示的に動的型を選んだと確信できる書式に限るためである。

• パラメーターは値に直接付くインライン注釈 x: Any を意図的なオプトインとみなし、別置きの関数型注釈に埋もれた Any（{Any | R}）は「型を書き忘れた／確定させていない」扱いで拒否する。
• 結果型は逆に、関数の型シグネチャを宣言する束縛注釈・内部名注釈の Any を「戻り値が動的である」という契約宣言として認め、戻り値そのものを Any へ上書きする body 末尾アスクリプション : Any（top 型への無意味な値強制で静的精度を捨てるだけ）は拒否する。
• 値束縛は束縛名の型注釈 x: Any := を唯一の明示位置として認める。

パラメーターと結果型で「インライン注釈 ↔ シグネチャ注釈」の許否が反転している点に注意（本節「名前付き関数のパラメーター型」脚注）。

名前付き関数の結果型

名前に束縛された関数値（body 非空の {…}）の結果型について、暗黙の Any を禁止し、Any を意図するなら型シグネチャで明示させる。本節「名前付き関数のパラメーター型」（パラメーター）・本節「値束縛の型」（値束縛）と同じ「暗黙 Any を書かせない」思想を結果型へ適用したもので、許否は上表に要約する。

• 暗黙 Any の禁止（省略して推論がネスト Any に到達）: 結果型注釈（language-spec.md §17.3 の 3 形）を省略し、本体推論の結果型（§2）がネスト位置に Any（gradual top）を含むとき型エラーを報告する。ネスト位置の Never（ボトム型）も同じく報告する — 本節「値束縛の型」が局所束縛の Never を許すのに対し、関数シグネチャは呼び手への文書なので {| List(Never) }（空リストをそのまま返す）や {| Option(Never) }（None をそのまま返す）は要素型を確定させていない。bare な top-level Never（panic だけの発散関数）は対象外で、これは bare な top-level Any を対象外とするのと対称である。診断は推論された結果型をそのまま文面に載せる。判定は本節「値束縛の型」と共通で、List(Any)・Option(Any)・Future(Any)・Result の成功型・タプル/record の要素・enum 適用の型引数などに Any を含む場合を指す。書き手には具体型の付与か、下記の明示オプトインを促す。
• bare な top-level Any は対象外（本節「値束縛の型」と対称）: 結果型そのものが Any に等しいだけ（ネスト位置の Any を含まない）のときは報告しない。これは Any パラメーターや明示 : Any ローカルが結果へ流れた透過的な帰結で、本節「値束縛の型」が bare top-level Any 束縛を対象外とするのと揃える。分岐が gradual に整合しつつ Any へ吸収されて結果型が top-level Any に倒れるケース（language-spec.md の load_notes 型）も、ネスト Any を残さないため本規則では素通しする（join が結果を top へ collapse するため、実装上も吸収された List(Any) を top-level Any と区別できない）。
• 明示オプトイン（束縛注釈・内部名注釈）: 結果型を束縛注釈 f: {P… | Any} := … または内部名注釈 { inner self: {P… | Any} | … } で Any と宣言する場合は許容する（戻り値が動的であるという契約宣言）。結果型は宣言どおり Any として扱い、呼び出し結果は素通しする（実行時意味と整合・誤検出ゼロ）。
• 明示だが禁止（body 末尾アスクリプション）: body 末尾アスクリプション { … | expr: Any } で結果型を Any にすることは禁止し、型エラーを報告する。戻り値そのものを top 型へ強制する無意味な値上書き（静的精度を捨てるだけで契約宣言ではない）ため、明示オプトインと認めない。
• 具体型・型変数は従来どおり: 結果型を具体型で宣言・推論できれば§2.6「結果型の越境利用」の越境照合に使う。推論結果が Unknown（静的に確定不能。§2.2）のときは素通しする。結果型が型変数の場合は Any ではないため許容する。
• 他規則との重複回避（二重報告の抑止）:
• 分岐が確実に割れるケースは合流結果が top-level Any に倒れる（ネスト Any ではない）ため本規則は発火せず、§2.9「分岐の結果型に収束を要求」が「分岐結果型の非収束」として報告する。
• ?（失敗 bail）が絡む関数の結果収束は§2.9「分岐の結果型に収束を要求」の check_result_converge が担当するため、本規則は ? を含む本体を素通しする（局所推論では bail の成功型が Any へ倒れ偽陽性になりうるため）。
• パラメーター型が確定しない関数は本節「名前付き関数のパラメーター型」が報告するため、本規則はパラメーター型が確定した関数の結果型のみ検査する（無型パラメーター由来の結果 Any を二重報告しない）。

• 対象: トップレベル／ローカルの束縛 name := <関数> / name: T := <関数>、およびスロットのデフォルトが関数の場合（メソッド・演算子スロットを含む）。
• 対象外: 名前に束縛されないインライン関数（if(c, {a}, {b}) の then/else、map({x | …}) 等の引数ブロック）、body を省略したデータオブジェクト（結果型がスロット宣言から導出でき、注釈を要求する理由が無い）。

名前付き関数のパラメーター型

本節「名前付き関数の結果型」と同じ対象（名前に束縛された body 非空の関数）の各パラメーターは、型が静的に確定しなければならない。確定する条件は次のいずれか。

• インライン注釈 x: T が付く
• 束縛注釈・内部名注釈で宣言した関数型の対応位置（同インデックス）が Any でない具体型を与える
• デフォルト式 x := <expr> の型が静的に推論できる
• インライン注釈・関数型注釈位置・デフォルト式が型変数を与える（Any と異なり同一性を追跡できるため確定とみなす）

いずれでも確定しないパラメーターには型エラーを報告する。これにより結果型だけ宣言してパラメーターが無型の関数（add := { inner self: {Int}, x, y | x + y }）や、関数型注釈位置で Any を与えたパラメーター（f: {Any | String} := {x | x} の x）も検出する。_（捨て変数）パラメーターと slot-list 内の type / enum スロットは対象外。

インライン : Any は動的型へのオプトイン: パラメーターに明示したインライン注釈 x: Any は必須化を充足する（型エラーにしない）。真に動的な型付けを意図する場合のオプトインとして許す（多相な関数は型変数 x: a で書くことが推奨される。language-spec.md §17.2）。一方、無注釈の bare パラメーターと関数型注釈位置の Any は「型を書き忘れた／確定させていない」扱いで検出する。

: Any の許否は書き手が Any を明示的に選んだと確信できる書式か否かで分ける。パラメーターはインライン注釈 x: Any を明示オプトインと認め、関数型注釈位置の Any を拒否する。結果型は逆に、束縛注釈・内部名注釈が宣言する Any を認め、body 末尾アスクリプション : Any を拒否する（本節「名前付き関数の結果型」）。位置ごとの許否は §3 冒頭の「暗黙・明示 Any の許可マトリクス」に要約する。

値束縛の型

本節の前 2 項が関数シグネチャの暗黙 Any を禁じるのと同じ思想を値束縛へ広げる。型注釈の無い束縛の推論型がコンテナー／payload のネスト位置に Any（gradual top）を含むとき、binding '<name>' requires an explicit type を報告する。型注釈（hdrs: List(String) := …）で要素型を確定させれば解消する。

• 対象: 型注釈の無い束縛 — := 宣言（トップレベル／ローカル）、可変 = の確立（未束縛からの初回代入。再代入は§2.10「可変ローカルの型安定性」が担当）、名前／位置の分解束縛の各要素。
• ネスト Any の判定: 束縛型を再帰的に辿り、次のネスト位置に Any が現れれば真とする — List / Option / Future の要素、Result の成功型、Tuple の各要素、Record の各フィールド、enum 適用（TypeApp / TypeVariant）の型引数、OneOf の各 alt。Any（gradual top）に到達したら真。
• 見ない位置（誤検出ゼロ）:
• 関数型（Func）: パラメーター・結果型は本節の前 2 項と §2.6「結果型の越境利用」の管轄のため辿らない（結果型の暗黙 Any は本節「名前付き関数の結果型」が検査する）。
• Result のエラー型 E: Ok(5) は Result(Int)（E は未制約、§3.4）で、E の未制約は don't-care のため辿らない。これにより Ok(5) を誤検出しない。
• bare な top-level Any 単体: 分岐割れ由来の Any は§2.9「分岐の結果型に収束を要求」、インライン : Any は明示 opt-in（本節「名前付き関数のパラメーター型」）が既に管轄するため、束縛型そのものが Any に等しいだけのケースは本規則の対象外（二重報告を避ける）。ネスト位置に Any を含むときのみ報告する。
• Unknown（型不明）: 静的に型を確定できない束縛（無型関数の呼び出し結果など）は Unknown で素通しする（§2.2）。
• 捕捉例: xs := [1, "x"]（混在で要素の join が Any）。
• 非捕捉例: Some(5)（Option(Int)）、Ok(5)（Result(Int)）、[1, 2]（List(Int)）、無型関数の呼び出し結果（Unknown）、関数値（本節の前 2 項と §2.6「結果型の越境利用」の管轄）、_ 破棄束縛、型注釈付き束縛。不在・空の構築も対象外 — xs := []（List(Never)）、x := None（Option(Never)）、x := Err("e")（Result(Never, String)）、a, b := (None, 5) の a、x := { items := [] |}（Record の List(Never) フィールド）。
• Never を報告しない理由: 不在・空の位置は「動的な値が入っている」（Any）のではなく値が入っていない。実行時もこれらをどの要素型とも整合と扱う（None matches Option(Int) / [] matches List(Int) はいずれも真）ため、Any として報告するのは実行時より悲観的で、しかも悲観の向きが誤っている。Never は注釈照合で全型の部分型、join の恒等元（全深度）として振る舞うので、宣言型への代入も他経路との合流も従来どおり通る。
• 健全性の位置づけ: 暗黙 Any コンテナーは実行時に panic せず（Any 境界には実行時照合の backstop がある）、本規則は class b の健全性を超えた方針上の規律である（§2.1）。
• 対象外（見送り）: object リテラル内の slot デフォルト（{ items := [] |} を直接引数へ渡す等、名前束縛を経由しない位置）。無注釈の外側束縛は本規則が Record フィールド再帰で束縛レベルで捕捉し、アスクリプション付き（{...}: T）はフィールド型が契約から確定するため、slot デフォルト単体の追加検査は冗長かつ誤検出の恐れがある。

2.6 宣言した型を契約として使う

書き手が宣言した型（language-spec.md §17.3 の結果型注釈・内部名注釈・関数型注釈）を、値の使用地点まで運んで照合する。宣言結果型と全脱出経路の整合だけは「到達すれば確実に panic」を根拠とし、残りは契約系である。

結果型の越境利用

完全適用 f(args) の結果型を、language-spec.md §17.3 で宣言された結果型（§2.5「名前付き関数の結果型」により明示は具体型または型変数に限られる）か、宣言が無ければ本体末尾式から推論した結果型（§2.2）から確定できる。これを使って x: T := f(args)（変数・分解束縛）の照合を行う（結果型 String の関数を x: Int := f(…) に束縛 → 型エラー）。型変数を含む結果型は呼び出し位置で引数型に単一化して確定する（id(5) → Int）。

結果型が宣言も推論もできない関数（本体末尾が静的に不明・早期 return を含み末尾と return 経路の join が割れる等）の呼び出し結果は Any＝素通しのまま。早期 return を含んでも全経路が同型に join できれば §2.2 のとおり結果型が確定し越境照合の対象になる。無型パラメーターの関数は結果 Any に倒れて素通しするが、§2.5「名前付き関数のパラメーター型」がパラメーター型を必須化するため無型パラメーター関数自体を別途報告し、越境対象の関数は本体スコープのパラメーター型が契約上確定する。

本体適合は best-effort: 関数本体の結果が宣言結果型に適合するかは、本体の結果型が静的に確定するときだけ照合する（確定しない箇所は素通し）。宣言した関数型のパラメーター型は本体スコープへ伝播し末尾式の型付けに使う — f: {Int | String} := {x | x} の本体 x は Int と確定し宣言結果 String と非互換＝検出する（実行時は arity のみ照合しパラメーター型を保証しないので、この伝播は静的検査だけが持つ精度である）。本体結果型の推論はローカル（本体末尾式）に留まり、呼び出し越境を伴う完全推論は将来段階。可変ローカルは確立時の型で参照する（§2.2 のとおり再代入で型は動かない）。本規則の健全性は「宣言結果型（契約）に対して誤検出を出さない」基準で、契約に反する本体の見逃しは許容し実行時照合が backstop。

宣言結果型と全脱出経路の整合

宣言結果型（language-spec.md §17.3 の 3 形）を持つ関数について、末尾式に到達する値だけでなく、return と ? の失敗 bail で脱出する値も宣言結果型と照合し、確実に非整合な経路を type mismatch: return value expects … として報告する。実行時は 3 形とも脱出値を宣言結果型で照合する（§17.3「照合は全脱出経路に及ぶ」）ため、本規則は「到達すれば確実に panic する不一致」を実行前に見せる位置づけである。

when cond { return Err(e) } の早期 bail は ? の下地になる定型（language-spec.md §16.5）で、ここが未検査だと Result(T, E) の E を宣言しても脱出経路だけが契約から漏れる。

• 見る脱出経路: 本体の文に直接現れる return / 引数位置の式に現れる return（現フレームで評価される）、builtin 制御構文（if / when / while）と conduit{…} / loop{…} 関数のブロック引数の中の return、match / subjectless match のアーム body の中の return、ブロックを取る組込メソッドのブロック引数の中の return（下記）、? の失敗 bail（失敗 variant の種別とエラー型 E のみを寄与し、成功要素は gradual top として制約しない — §3.4 と同じ扱い）。
• ブロックを取る組込メソッドのブロックも脱出経路: xs.each { x | when … { return Some(x) } } は Option を返す探索の慣用（prelude.md §8）で、ブロック内の return は外側関数から脱出する（language-spec.md §18.2 の「透過は制御構造に限らない」）。レシーバーの推論型が組込型に確定し、かつメソッドがその型のブロック取りメソッドであるときだけ辿る（List / String / Bytes / Range の反復・述語メソッドと、Option / Result / Ordering のブロック取りメソッド）。Future のメソッドは対象外 — ブロックが別フローで遅延起動されるため脱出が成立しない。網羅ではなく実行時挙動を確認した名前の集合に限り、集合と実装のドリフトは回帰テストが固定する。ブロックのパラメーターはレシーバーの要素型（§3 の反復メソッドのシードと同じ出所）で束縛して本体を型付けする — 束縛しなければ return x が型不明になり脱出経路として見えない。要素型が確定しない位置・位置規則に当たらないパラメーター（fold の accumulator 等）は型不明のまま置き、その return は素通しする。
• 末尾式が分岐のときは枝ごとに照合する: 末尾値を join してから照合すると枝ごとの具体型が失われる（join が Any へ倒れる）ため、if / when / match の葉を個別に突き合わせる。末尾値そのものの照合は本節「結果型の越境利用」の越境照合と body 末尾アスクリプションの静的照合が担うので、本規則はそこが素通しした「join で消えた枝」だけを補う（二重報告を避ける）。
• 辿らない経路（誤検出ゼロ）: 不透過なユーザー高階関数へ渡したブロック内の return（そのブロック自身が関数境界なので外側の結果型に寄与しない。language-spec.md §18.2）、レシーバー型が確定しない／集合に無いメソッド呼び出しのブロック（同名のユーザー定義メソッドは透過でないため、確定しない受信者を透過とみなすと誤検出になる。Future のメソッドも同様に対象外）、値として格納される関数リテラル（構築時には評価されない）。
• 素通しする宣言結果型: Any・型変数・Unit — 実行時の照合が素通しする位置と揃える（§17.4）。宣言結果型が Result(T)（≡ Result(T, Error)）なら E は確定しているので Err payload も照合する。
• 非捕捉例: 宣言結果型に適合する早期 return、結果型を宣言しない／Any と宣言した関数、不透過な高階関数のブロック内 return。

捕捉例（いずれも到達すれば実行時 panic する）:

# 成功型 T を破る return（body 末尾アスクリプションで宣言）
f := { b: Bool |
  when b { return Ok("s") }
  Ok(1): Result(Int, String)
}

# 明示したエラー型 E を破る return
g := { b: Bool |
  when b { return Err(error("io_error", "x")) }
  Ok(1): Result(Int, String)
}

# 末尾式の片方の枝だけが E を破る（join では Result(Any) に潰れて見えない）
h: { Bool | Result(Int, String) } := { b |
  if b { Err("boom") } { Err(error("io_error", "x")) }
}

inner-name 型と slot/結果型の整合

リテラルが inner-name 型注釈 { inner self: T | … }（language-spec.md §17.3）を持ち T が型値へ解決できるとき、self（＝値自身）についての 2 つの独立した表明 — inner-name 型 T と、値が自前に宣言する slot 型・結果型 — が矛盾すれば報告する。

結果型の照合は body 末尾アスクリプションだけでなく、宣言が無いときの本体推論結果（§2.2）とも行う（double := { inner self:{Int|String}, x:Int | x+x } は本体推論結果 Int と T の結果 String の非整合を定義時に検出）。inner-name の関数型注釈が宣言する結果型は §17.3/§17.4 のとおり呼出時に実行時強制されるため、この矛盾は実行前の本規則に加え実行時 panic としても顕在化する（double(3) は panic）。一方 inner-name のパラメーター型とrecord 型は引き続き実行時に評価されないため、それらの矛盾は §2.9 の 3 規則と同じく契約系の診断にとどまる（inner-name のパラメーター型・record 型を値の構造照合に用いる段階が将来入れば、実行時にも現れうる）。

• 種別不一致: T が関数型なのに値がデータオブジェクト（body 無し）、または T が非関数型なのに値が関数（body 有り）→ 報告。
• 関数の場合（body 有り・T = {P… | R}）: 宣言スロット数 ≠ T のパラメーター数なら報告（arity 不一致）。各位置のスロット宣言型 Sᵢ と T の Pᵢ が確実に非整合なら報告。宣言結果型（body 末尾アスクリプション）または宣言が無ければ本体推論結果と T の結果 R が確実に非整合なら報告。
• データオブジェクトの場合（body 無し・T = record 型）: 同名フィールドで、T のフィールド型とスロット宣言型が確実に非整合なら報告。
• 誤検出ゼロ: いずれも両辺が静的に解決でき gradual 整合性 consistent（§3。Any・型変数・Unknown は wildcard）で確実に非整合なときのみ報告。片方でも未解決・注釈無しなら素通し。T が型値へ解決できないときも素通し。

関数型注釈と実体シグネチャの整合

関数型注釈（パラメーター型が関数型 {P… | R}、または束縛注釈が関数型）を受ける関数値については、その値の静的に確定したシグネチャ（各スロット宣言型・宣言/推論した結果型）と注釈が確実に非整合なら報告する。パラメーター・結果を gradual 整合性 consistent（§3）で照合し、確実な非整合の対があるときだけ報告する。§17.2 の higher-rank 非対応と整合し変性は取らない（不変照合）。

• 根拠と穴: language-spec.md §17.4 の実行時照合（match_func）は、関数値が結果型注釈を宣言しないとき結果照合を素通しする。そのため無注釈結果の関数（bad := {n: Int | "s"}）を関数型注釈 {Int | Int} に束縛・引数渡ししても束縛地点では panic せず、後続の値使用（bad(…) の結果を Int として使う箇所）で初めて panic する。本規則はこの実体シグネチャの非整合を実行前に報告して塞ぐ。
• 注釈照合には足さない: 束縛地点で即 panic しない照合を §2.4 の注釈照合（「到達すれば確実に panic」枠）に足すと誤検出になるため、本規則は独立した契約系の診断として置く。
• 引数位置に直接書かれた関数リテラルは、結果型を宣言しないとき結果位置を照合しない: if / while など透過的な制御構文ブロックへ渡るサンクは、内部の return / break / continue が呼び出し元へ透過的に脱出する（language-spec.md §18.2）ため、§2 の推論が拾うのは脱出値の型でありサンク自身の結果型とは限らない（x := if (c) {1} {return "oops"} の else 枝は {| String} と推論される）。よってこの場合だけ結果位置を不変照合から外す。結果型を宣言している（form 2 内部名注釈 / form 3 body 末尾アスクリプション）リテラルはその宣言が値自身の表明であり脱出値型に汚染されないため、通常どおり照合する。パラメーター型はどちらの場合も値自身の宣言なので常に照合する。
• 素通し条件: シグネチャが静的に確定しない（宣言も内部名注釈も無いスロット・結果型が推論不能）位置・arity 不一致・Any/型変数/Unknown が絡む対。スロットが無注釈でも内部名注釈がパラメーター型を宣言していれば §2.2 の補完でシグネチャが確定するため、f: {String | Int} := { inner self: {Int | Int}, x | 0 } のような束縛注釈と内部名注釈の食い違いも本規則が報告する。渡す関数が無名または結果型省略で該当位置が Any になり静的に拒否できないケースは、関数型の呼出時強制（language-spec.md §17.4）が実行時 backstop。

2.7 メンバー・メソッドの解決

受信者に対して名前が解決できるかを検査する。根拠は受信者の型で 2 つに分かれる — 値が後から slot を増やせない型（原始スカラー・variant・enum・List / Tuple・std: の不透明型・import 先モジュール）は「到達すれば確実に panic」、record は契約系である。record を契約系に置くのは、宣言に無い名前を持つ値が渡ってくることがある（幅サブタイプ。language-spec.md §17.2）ため到達しても panic するとは限らないからで、それでも報告するのは宣言したメンバー集合が受け手から触れる範囲である（同 §17.2）ことによる。

存在しないメソッド／スロット

recv.name（メンバー参照・型メソッド呼び出し recv.name(args) の両方）で、recv の静的型がメソッド集合の閉じた型に確定し、name がその型に解決できるどの名前（型メソッド・universal method matches / compare / inspect・演算子メソッド + ほか language-spec.md §8.1）にも該当しないとき、no such slot or method: name を報告する。

中置演算子形（recv op arg。op は演算子表 language-spec.md §8.3 の項目）にも同じ規則を適用する。中置は recv.op(arg) の糖衣なので判定は dot 形と同一で、素通し条件（Any・型不明・関数・無境界の型変数の受信者）も変わらない。

補足: 原始スカラー・variant・不透明型は実行時も同じ no such slot or method に落ちる。hikari check は一律に no such slot or method として報告する。

record の受信者（幅構造型）: 宣言スロット・埋め込みが取り込んだエントリ（language-spec.md §17.5）・record に効く組込メソッド（universal / 演算子・names / values / has_name ほか language-spec.md §8.1）のいずれにも解決しない名前を報告する。注釈の位置は問わない — パラメーター・束縛・export のいずれで宣言しても同じに読む。

閉じる根拠は宣言である。 受信者の型が record であることではなく、書き手がその型で受けると宣言したことが根拠なので、宣言に帰着しない受信者は素通しする。宣言に帰着するのは次の 2 つで、どちらでもない受信者（可変束縛・注釈の無い束縛・推論だけで組んだ record）は対象外である。

• 名前の付いた型（type Rec := { … |}）に確定する受信者。別名は書かれた綴りでしか付かないので、その型で受けている時点で宣言がある（関数の戻り値経由でも同じ）
• 注釈された名前の受信者（o: { a: Int |} のパラメーター・p: T := v の束縛）。無名の record をその場で書いた形がこれで、型の側には手かかりが残らない
• enum の payload を受けた名前（match e { Tag(p) => p.name } の p）。型は enum E := OneOf(Tag(T)) の宣言が書いており、注釈された名前と同じ資格で閉じる。T をその場に書いた無名の record（Tag({ a: Int |})）でも同じである

封印契約型（language-spec.md §17.6）の受信者だけは、実行時封印という裏付けを持ち強制の水準が違うので、下記「封印契約に対する契約外アクセス（importer 側）」が別コードで扱う。

以下は値が後から slot を増やせない型で、こちらは「到達すれば確実に panic」に乗る。

• 原始スカラー（Int / Float / Bool / String / Bytes / Range）と variant（Option / Result / Ordering）: 型から閉じたメソッド集合が一意に決まる。
• ユーザー定義 enum の値（enum E := OneOf(…) の E に確定する受信者。組込タグの型も同じ）: variant の値はスロットを 1 つも持たないので、解決するのは組込メソッドだけである。ここは所属で絞らない — v.is_some は名前としては解決し、実行系がタグを見たところで「Option ではない」と断る。それは領域のエラーであってメンバー解決のエラーではないので、静的にも同じ線で分ける。したがって報告するのは、組込メソッド（型メソッド表のいずれかのラベルにある綴り・universal method・演算子メソッド）のどれでもない名前だけである（e.kind / e.col のような、record だった頃の綴りがこれにあたる）。enum 名前空間の受信者（E.Tag の E）は上記「enum 型値のタグ member」が別に扱う。無名の型集合（OneOf(Int, String) のように tag でない選択肢を並べた union）は対象外である — あれは「どれかの型の値」であって variant ではないので、絞り込む前の受信者を報告すると誤検出になる（§2.5）。
• enum 型値のタグ member: enum Name := OneOf(Tag1(…), …) で束縛された Name 自身（language-spec.md §17.4）。Name は宣言済みタグ名の集合を slot に持つ閉じた名前空間なので、Name.Tag の Tag が universal method にもいずれの宣言タグ名にも該当しなければ報告する（Color.Foo で Color に Foo タグが無ければ検出）。受信者が Name そのもの（enum 定義で束縛された名前、または immutable 別名連鎖）に帰着する場合に限る。prelude の Option / Result / Ordering も同機構で Option.Some 等のタグ member を持つ（これは Name.Tag のタグ側の検査。上記 variant 検査は値そのものへのメソッド呼び出しで別軸）。
• std: の不透明型（std:time の Instant / Date / Time / Duration）: 内部表現を露出しない名目型で、型ごとにメソッド集合が閉じて一意に決まる。
• List / Tuple（Unit を含む — () は空タプルではなく Unit だが同じメソッド集合を持つ）: 型からメソッド集合が一意に決まる。受信者の由来は問わない — 変数・関数戻り値・注釈・パラメーター経由でも検査する。名前スロットを持つ List 値は作れないためである: 実行時は名前スロットへの代入を cannot assign slot on List / cannot assign slot on Tuple で拒み、リテラルの側も位置要素と名前スロットの混在を構文エラー（a slot-list takes only slot declarations）にする。
• 代入先の位置は 1 度しか鳴らさない: xs.foo = 9 のような代入先は本項が受け持ち、§2.10 の no such slot は重ねない。名前が組込メソッドとして解決する形（c.length = 9）だけはそちらが受け持つ。
• import 先モジュール（相対 import import mod := "path.hika" / third-party import mod := "pkg:…"）: import 先のファイルオブジェクトのトップレベル slot は宣言時に決まり（language-spec.md §13.1 — slot 生成はトップレベル slot-list 宣言時のみ）、幅構造型の record と違って別の視点がより多くのスロットを宣言していることも無いので、メンバー集合が静的に閉じる。受信者が import で丸ごと束縛した名前（別名連鎖 m2 := m1 も辿る）に帰着し、import が解決でき record 型を組めるとき、name が import 先トップレベル slot にも universal method にも該当しなければ報告する（mod.member(args) の呼び出し形も同様）。
• 公開メンバーはトップレベルに直接並ぶ束縛である（language-spec.md §13.1）。入れ子ブロックで auto-vivify した名前はそのフレームのローカルで slot にならない。export があればそのリストがさらに絞る（language-spec.md §13.2）。
• enum は Name だけを公開メンバーとして export する（language-spec.md §17.4。タグはフラット束縛せず Name の下に置かれる）。import 側では mod.E（型メンバー兼タグ名前空間）だけが解決し、各タグは mod.E.A と連鎖参照する（未知タグ mod.E.Foo の検出は上記「enum 型値のタグ member」と同規則）。
• 素通し条件: 循環 import・解決不能な import（既に Any）・mutable 束縛・関数引数/戻り値経由の import 値（closed 保証が切れる）。
• std: モジュールもメンバー集合が構造化シグネチャ（§2.2「import 先モジュールの型」）で閉じるため原理的には同様に検査でき、その不透明型（Instant 等）は既に本節の対象。ただし std: 名前空間オブジェクト自体のメンバー検査は当面行わない（見逃しは許容）。

対象外: 関数・Any・型不明・型変数（境界を持たないもの）の受信者、および数値スロット（t.0）。境界付き型変数の受信者は、境界が record または既知の不透明型に解けるならその境界を基底とみなして本項を適用する（language-spec.md §17.8「境界に無い名前は型エラーである」）。封印契約型（export { name: T }、language-spec.md §17.6）に確定した受信者は、強制の水準が違うため（実行時封印を持つ）、本項ではなく本節「封印契約に対する契約外アクセス（importer 側）」が扱う。

封印契約に対する契約外アクセス（importer 側）

export { name: T }（language-spec.md §13.2・§17.6）で公開した名前は 封印契約 を持つ。受信者 recv の静的型がこの封印契約型に確定するとき、recv.name / recv.name(args) の name が、契約の閉じたメンバー集合（§17.6）にも universal method（matches / compare / inspect ほか language-spec.md §8.1）にも該当しなければ、no such slot or method: name を報告する。

中置演算子形（recv op arg。op は演算子表 language-spec.md §8.3 の項目）にも同じ規則を適用する（§2.7 と同一）。

• 「存在しないメソッド／スロット」との関係: 判定語彙・報告文言は共通（no such slot or method: name）で、根拠もどちらも契約系である。異なるのは強制の水準だけ — 封印契約型は契約外スロットを実行時にも到達不能にする封印（下記）を持ち、一般の record は静的な層だけで強制する。コードを分けているのはこの水準差を診断の側で区別できるようにするためで、報告文言に両者を区別する語は含めない。
• 素通し条件: 受信者の静的型が Any・型不明・関数に確定するとき。一般の record は素通しではない — 上記「存在しないメソッド／スロット」が no-such-member として報告する。(x: Any).name のように Any を経由した契約外アクセスも静的には素通しするが、契約型が record 型に確定する export については実行時封印（language-spec.md §17.6）が到達不能化する backstop になる。契約型が関数型のときはその適用結果に実行時封印が及ばないため、Any 経由の契約外アクセスは静的にも実行時にも塞がらない。

封印契約の契約外・未使用スロット（定義側）

対象は 型注釈束縛 name: T := <リテラル>（language-spec.md §17.6。export { name: T } の name に限らず、非 exported な通常の型注釈束縛も含む）で、次の 3 条件をすべて満たすものである。

1. 値が スロット集合の確定する（§2.10）オブジェクトリテラルに帰着する。
2. 契約 T が閉じたメンバー集合（§17.6）へ静的に解決できる（Any・未確定でない）。
3. エスケープ安全条件（後述）を満たす。

これら 3 条件を満たす型注釈束縛について、そのリテラルの宣言スロットのうち次の両方を満たすものを sealed export slot '<name>' is never used として報告する。

• 契約 T の閉じたメンバー集合（§17.6）に無い（契約外）。
• 定義ファイル内で参照 0（値読み出しをカウント。束縛名・スロット名・代入先は数えない。lint.md の unused と同じ数え方）。スロットは obj.slot という外部 API の形でも読まれうるので、recv.name のドット越し読み出しも受信者の型を問わず参照として数える（見逃し側）。

オブジェクト自身の body 内から参照されるスロット（例: メソッド deposit が読む balance）は参照 > 0 のため対象外。破棄子 _・型注釈付きスロットの扱いは既存 unused（lint.md）の保守方針を踏襲する。

エスケープ安全条件: export { name: T } は値が必ず封印契約の型 T としてのみ外へ出るため、契約外は importer から到達不能と保証される（本節「封印契約に対する契約外アクセス（importer 側）」）。非 exported な型注釈束縛にはこの保証が無く、値が型無し（Any）位置で外へ漏れると、他ファイルからの契約外アクセスを見落として偽陽性になりうる。これを避けるため、非 exported な型注釈束縛は追加で次を満たす場合に限り契約起点にする。

束縛名 name の参照箇所すべてで name が メンバーアクセスの受信者（name.member / name.member(args)）としてのみ現れ、バラの値（関数引数・戻り値・他束縛の右辺・リテラル要素等）として一度も現れないこと。

この条件下では値はファイル外へバラで渡らず、契約外サブスロットは in-file の name.sub 読み以外から到達不能になるため健全である。条件を満たさない束縛（バラ値として使われうる）は素通しする（見逃し許容）。export { name: T } 経由の契約起点（本節「封印契約の契約外・未使用スロット（定義側）」の元々の対象）はエスケープ安全条件の判定対象に含めない（封印契約そのものが到達不能を保証するため）。

• なぜ typecheck か: 契約外か否かの判定に封印契約の型情報を要するため、型を見ない lint ではなく typecheck の診断とする。lint の unused がオブジェクトのスロットを一律対象外とする（lint.md）のを、封印契約という静的な閉包を使って一部だけ健全に覆す位置付けになる。
• 素通し条件: 値が スロット集合の確定する（§2.10）リテラルに直接帰着しない場合（mutable 再代入・関数戻り値経由など）。契約 T 自体が Any・未確定に倒れる場合。非 exported な型注釈束縛でエスケープ安全条件を満たさない場合。値が型注釈束縛に流れない場合（型注釈の無い export { name }・export 自体が無く型注釈も無いファイル）。

分解 import の未 export 名

スロット分解 import { a, b, … } := "…"（language-spec.md §13.2）で、解決済みの import 先モジュール（closed record）に帰着するとき、各分解名が import 先のトップレベル slot（値・型メンバーとも）に無ければ、実行時に確実にエラー（no such slot）になるため報告する。enum は Name のみがトップレベル slot で、各タグは Name の下の member なので分解 import では直接引けない。

これは export が公開を絞ったファイルから未列挙の名前を import { x } := "…" で受けるエラーを、実行前に捕捉する。循環・解決不能な import は素通し。

タプル分解の要素数と分解元

タプル分解 a, b := expr（language-spec.md §6.3）で、右辺が静的に確定するとき、到達すれば確実に実行時エラーになる 2 つの形を報告する。スロット分解 { a, b } := expr のどの名前が取れるかは本項の対象外である（右辺の静的型が record に確定するなら §2.7「存在しないメソッド／スロット」が宣言に無い名前を報告し、import 先モジュールからの分解は本節「分解 import の未 export 名」が扱い、スロットそのものの有無は次項が扱う）。

• 要素数不一致: 右辺の静的型がタプルに確定するとき、左辺の名前の個数（破棄子 _ も 1 個と数える）とタプルの要素数が違えば destructure arity mismatch: N names, M values を報告する。実行時の要素数厳密一致（language-spec.md §6.3）を先取りするもので、文面も実行時と同じである。
• Sequence でない右辺: 右辺の静的型が Sequence（language-spec.md §17.5）を実装しない型に確定するとき destructure source has no positional axis: <型> を報告する。対象はオブジェクト（record・関数）・原始スカラーの Int / Float / Bool・Unit・variant（Option / Result / Ordering / Control とユーザー定義 enum のタグ型）・std: の不透明型・Future である。オブジェクトが一律ここに入るのは、要素の並びを持つのが List・タプル・String・Bytes・range に限られるためである（同 §2.1）。

素通し: 長さが静的に決まらない右辺（List・String・Bytes・Range）は要素数を検査しない — いずれも Sequence は実装するので、上の 2 つ目の対象にもならない。Any・型変数・Never・OneOf・refinement 型、および型が確定しない右辺は両方とも素通しする。

スロット分解の対象

スロット分解 { a, b } := expr はスロットから取る。どの名前が取れるかは record が幅構造型のため閉じない（上記）が、スロットを持ちうるかは型から言い切れる位置がある。右辺の静的型がスロットを持たない型に確定するとき destructure source has no name slots: <型> を報告する。対象は Tuple・Unit・List・原始スカラー（Int / Float / Bool / String / Bytes / Range）である。

スロット分解は universal method を引かない（{ length } := [1, 2, 3] は実行時エラー）ので、これらの型ではどの名前も取れない。

素通し: record（幅構造型）・関数・std: の不透明型・OneOf・型構築子・Any・型変数・Never・refinement 型、および型が確定しない右辺。不透明型と OneOf を外すのは、それらの綴りが型値としても書かれうるためである（{ Circle, Rect } := Shape は enum タグの bare 化。language-spec.md §6.3）。

copy-and-update overlay の未知キー

overlay 付き複製 recv.copy(overlay)（language-spec.md §9.5）で、recv がスロット集合の確定するオブジェクト値に帰着し overlay がオブジェクトリテラルに帰着するとき、到達すれば確実に実行時エラーになる overlay を報告する。実行時に language-spec.md §9.5 の overlay 適用が出すエラーを先取りする（判定は §2.10 と共有）。

• overlay のキー（スロット名）が受け手 recv のスロット集合に無いとき、copy: no such slot: <name> を報告する（未知キーをソース順にすべて報告）。受け手のスロット集合は closed リテラルの宣言スロットから確定し、実行時の権威集合（§9.5）と一致する。

素通し: 受け手 recv は §2.10 と同じ判定（①オブジェクトリテラルに直接帰着、または②それを immutable 束縛した名前）に限る。受け手が copy スロットを持つ（copy を上書き、§9.5。override は overlay を任意に解釈しうる）ときは overlay 意味論が静的に閉じないため素通し。注釈付き record・関数引数/戻り値・import 越境の受け手、overlay が変数・body/inner-name/destructure 混じり・型/enum スロットを含むリテラルの場合も素通し。

ブロックリテラルへの Sequence メソッド

recv.name の recv が本体付きリテラル（{ params | body } / { body }）で、name が Sequence（language-spec.md §17.5）のメソッド（each / map / filter / fold / length ほか）のとき sequence method on a block literal: name … を報告する。オブジェクトは要素の並びを持たない（同 §2.1）ので、この綴りは到達すれば必ず失敗する。

この形は並置形のブロック実引数に後置 .name を続けたとき生まれる。. は並置より強く結びつく（language-spec.md §8.1）ので、xs.filter { p | … }.each { p | … } は xs.filter({ p | … }.each)({ p | … }) と解釈され、.each は filter の結果ではなくブロック自身に係る。each の型は意図的に Unknown（block 内の break が任意の値で脱出しうるため）なので照合は素通しし、実行時に述語が () を返して落ちる。意図した連鎖はグルーピング括弧 (xs.filter { … }).each { … } か、結果を名前に束縛してから続ける形で書く。

報告しない:

• List リテラル（[1, 2, 3]）— 本物の Sequence であり、.each は 1, 2, 3 を巡る。
• 本体の無いリテラル（record）— 受け手がブロックではないので、本規則ではなく §2.7 の未知スロット検査が扱う。
• スロットを見るメソッド（names / values / has_name）— オブジェクトで意味を持つ（{ a := 1 | body }.names! は ["a"]、パラメーターだけの { p | body }.names! は ["p"]）。
• universal method（copy / inspect ほか）・演算子メソッド糖衣・Sequence に無い名前（{ body }.fork! のような大域関数の後置形）。

既定値の中の inner-name

スロットの既定値式はリテラル評価時に宣言順で 1 回だけ走る（language-spec.md §12）。その最中のオブジェクトは半端なので、inner-name ({ inner self, … |} の self) から読めるのはその位置より上で宣言したスロットだけである。それ以外の読みを inner-name-in-default として報告する。

報告するのは inner-name の出現が既定値式の中に直接あるときに限る。読みの側だけを見ても足りない — 裸の出現が残ると、半端なオブジェクトが名前を通り抜けて同じ穴が開く。

inner_bound は出現そのものを報告する。 inner_bound (language-spec.md §4.2.1) が指すのは束縛を写した自分だが、既定値の評価時点では束縛がまだ始まっていない — inner-name のように「上で宣言した兄弟だけは読める」という逃げ道が無く、読める値が 1 つも無い。したがって dot の受け手かどうかを問わず、既定値式の中の出現を inner-bound-in-default として報告する（inner bound name 'b' is not available in a slot default）。

inner_bound では既定値の外も報告する。 inner_bound は束縛が 1 つも始まっていない時点の名前なので、初期化済みかどうかに関わらず読める値が無い。対象はスロット destructure の右辺（{ p } := b）と型注釈（x: b・{ p: b } := …）の 2 つで、それぞれ inner bound name 'b' is not available in a destructure source / … in a type annotation を報告する。

報告しない条件のうち inner_bound にも及ぶのは、body 領域・既定値が作る関数リテラルの中・内側で隠されているときの 3 つである。隠されているかは束縛の綴りで見る — 走査に現れたリテラルがその名前をスロット・inner-name・inner_bound のどれかで宣言していれば、その内側の出現は別のものを指すので降りない（内側のリテラルが b を宣言していれば報告しない）。

報告しない:

• body 領域（{ … | body } の body）と、既定値が作る関数リテラルの中（get := {| self.x }）。どちらも既定値の評価より後に走るので inner-name は完成したオブジェクトを指す。走査は入れ子のオブジェクトリテラルで止まる。
• inner-name が内側で隠されているとき（入れ子のリテラルが同じ名前を inner に取る・同名のローカルが手前にある）。受け手はその literal の inner-name ではない。

原始型メソッドの引数型

recv.method(args) の実引数が、レシーバーの型パラメーターに依らず一意に決まるパラメーター型と確実に非互換なとき type mismatch: argument N of <method> expects … , got … を報告する。対象は String.slice(Int, Int) / String.contains(String) / String.starts_with(String) / String.replace(String, String) / String.split(String) / List.join(String) / Bytes.slice(Int, Int) / Range.step(Int) など、引数型が固定のメソッド（実装上の出所は原始型メソッドの引数型表）。paren 形と juxtaposition 形（recv.method a b）の両方を平坦化して照合する。

これらのメソッドは実行時に引数型を厳格に検証して panic する（"abc".slice("x", 2) は String.slice: start must be Int）ため、§2 の「到達すれば確実に panic する不一致」に当たる。

報告しない:

• 要素型・payload 型に依存する引数（List.contains(x) の x / Option.or(default)）— 引数型がレシーバーの型パラメーターで決まるため引数型表に収録されない。これらは実行時にも型を検証せず panic しない（[1, 2].contains("s") は false）ので、本項の対象外で正しい。ただし std の可変な器（Array / ScratchMap）への書き込みは受け手の型引数が定める要素型を後続の読み出しがそのまま信用するため、§2.10「可変な器への書き込みの要素型照合」が契約系の診断として別途照合する（読み出しは確実に panic するので健全性に効く）。contains / or のような非破壊メソッドにこの問題は無い。総称パラメーターの型変数が受け手と引数で割れる場合（x: Option(Int) に x.or("s")）を診断するかは将来課題 — §3.1 の「単一化は結果型の推論だけに使い診断を出さない」方針の例外を増やすかの判断が要る。
• ブロックを取るメソッド（map / fold / sort_by）— 同じ理由で引数型表に収録されない。
• レシーバー型が不明・Any・Never のとき、実引数型が不明・Any・型変数・Never のとき、引数数が表と合わないとき（arity 側の責務）。

2.8 演算子と適用

両辺・実引数の型から、到達すれば確実に panic する演算と適用を検出する。

演算子の型不一致（二項算術）

+ / - / * / / / % で、両辺の静的型がともに原始スカラーに確定し、その組合せが実行時に確実に演算子未定義 panic（operator '<op>' not defined for …、language-spec.md §7.1〜§7.2）になるとき報告する。

妥当な組合せは次だけで、それ以外の原始スカラー同士（混合 Int/Float・String を含む非 +・Bool/Bytes/Range の算術など）はすべて報告する。

• 健全性の根拠: 原始スカラーは演算子スロットを持てない閉じた型なので、左辺が原始スカラーの算術は必ず組込中置（language-spec.md §8.1）に落ち、上記以外は確実に panic。暗黙の Int/Float 変換は行わない（language-spec.md §7.1）ため 1 + 1.0 も対象。
• 素通し条件: どちらかの辺が Any・Unknown・型変数、または原始スカラー以外（record・object・List 等 — 演算子スロットでオーバーロードされうる、+ でオブジェクトマージ／List 連結になる）。== / !=（全値で定義され panic しない）は対象外。順序比較・短絡は §2.8 / §2.8。

順序比較の型不一致

< / <= / > / >= で、両辺の静的型がともに原始スカラーに確定し、その組合せが実行時に確実に panicするとき報告する。

妥当な組合せは同型の Int / Float / String / Bool（Int < Int・"a" < "b"・true < false）だけ。それ以外の原始スカラー同士はすべて報告する — 混合（Int/Float・Int/String）は cross-type で panic、Bytes / Range は同型でも順序を持たず（compare が not comparable）panic する。

• 健全性の根拠: 順序比較は universal method left.compare(right)（language-spec.md §8.1）に落ち、原始スカラーは compare スロットを上書きできない閉じた型なので、組込 compare の妥当な組合せ以外は確実に panic。1 < 1.0 も対象（暗黙変換なし）。
• 素通し条件: どちらかの辺が Any・Unknown・型変数、または原始スカラー以外（compare スロットでオーバーロードされうる object 等）。

短絡の型不一致

&& / || で、左辺の静的型が Bool 以外の原始スカラーに確定するとき、確実に実行時エラー（operator '<op>' requires Bool, got …、language-spec.md §9.3）になるため報告する（1 && x・"a" || y）。

• 健全性の根拠: && / || は両辺 Bool 必須でスロット上書き不可（operator-slot に落ちず先に短絡評価される）であり、左辺は短絡に関わらず必ず評価されるため Bool 以外なら確実に panic。
• 右辺は見ない: 右辺は短絡で評価されないことがある（&& は左 false、|| は左 true で右を見ない）ため、Bool 以外でも確実な panic とは言えず報告しない（見逃し許容）。
• 素通し条件: 左辺が Any・Unknown・型変数・原始スカラー以外。

関数でない値への適用

適用 f a / f(a) / 明示的 kick f! の呼び先の静的型が、原始スカラー（Int / Float / String / Bool / Bytes / Range）または Unit に確定するとき、確実に実行時エラー（not a function: <型>）になるため報告する。

• 健全性の根拠: これらは閉じた型で、スロットを 1 つも持てない。呼び出しは引数をスロットへ束縛してから本体評価か部分適用かを決める（language-spec.md §3.6）ので、スロットを持てない値は呼び先になれない。演算子の判定（上記）が「演算子スロットを上書きできない」ことに乗っているのと同じ根拠である。
• 引数の数には依らない: 引数ゼロの明示的 kick x! も、値適用 x 1 も、束縛する先が無いことは同じである。
• 覆いは剥がしてから見る: 効果型 Effect(T, L)（§2.15）と多重度型 Borrowed(T) 等（§2.14）は基底を包むだけなので、剥がした先が原始スカラーまたは Unit なら報告する。実引数の照合と arity の判定が基底で行われるのと同じ扱いである。
• 呼び先が適用そのものなら見ない: カリー適用の途中（(f 1) 2 の f 1）の型は関数の最終結果型で来るので、残りのパラメーターを持つ関数型としては引けない。そこを呼び先として判定すると正当な部分適用が「関数でない値」に見えるため、素通しする（見逃し側）。
• 素通し条件: 呼び先の型が Any・Unknown・型変数・Never のいずれか、または原始スカラー・Unit 以外の型。List や record・object は呼び先になれる（body を持つリテラルは関数、持たないリテラルは派生する）ので対象外で、List への値適用が「束縛できる未束縛スロットが無い」で落ちることは見逃す（判定の根拠が別なので、そちらは arity 側の話である）。

完全適用の arity 超過

型が静的に分かる関数への適用 f(args) で、パラメーター数が 2 以上に確定し引数数がそれを超過するとき、確実に実行時 arity panic（language-spec.md §16.2）になるため報告する。

• 健全性の根拠: 超過引数は束縛できるスロットが無く panic する。パラメーター 1 個への超過は tuple 畳み込み（language-spec.md §7.4）で単一タプル束縛に帰着するため対象外（型不一致側が backstop）。
• 引数が 1 個以上ある不足は報告しない: 引数数 < パラメーター数はカリー適用やデフォルト充足で正当な部分適用でありうるため。2 引数以上の不一致な不足が panic するケース（f := {x:Int,y:Int,z:Int|…}; f(1, 2)）は見逃す（false negative は許容）。引数が 1 つも無い形だけは別で、下記「引数ゼロの明示的 kick に必須スロットが残る」が見る — そちらは部分適用にならないので確実な panic である。
• 素通し条件: 関数型が静的に確定しない呼び出し・パラメーター 1 個の関数・引数数が一致か不足の呼び出し。デフォルトスロット持ち関数も宣言パラメーター数で判定し、超過のみ報告。

引数ゼロの明示的 kick に必須スロットが残る

引数を 1 つも持たない適用 f() / f! で、呼び先の未束縛スロットに既定値を持たないものが残ると確定するとき、確実に実行時 arity panic（language-spec.md §16.2）になるため報告する。文面は実行時と同じ missing required arguments、コードは arity-mismatch である。

• 健全性の根拠: 引数ゼロの適用は明示的 kick であって部分適用ではない（language-spec.md §3.6）。未束縛スロットへ既定値を補完してその場で本体を走らせる形なので、埋める値の無いスロットが 1 つでも残れば必ず止まる。実引数が 1 つでもある呼び出しは既定値を見ずに部分適用へ倒れるので、この規則の対象外である。
• 個数は数えない: 文面が「N 個足りない」と言わないのは実行時と同じ理由で、既定値を持つスロットまで「足りない」と数えてしまうためである。足りないのは「既定値の無い未束縛スロット」であって引数の個数ではない。
• 既定値の有無を引ける位置に限る: 関数型はどのスロットが既定値を持つかを運ばない（{ a: Int | … } と { a := 1 | … } はどちらも 1 パラメーターの関数型になる）ので、型だけからは判定できない。引けるのは次の 2 つで、どちらでもなければ素通しする。
• 呼び先が確実に関数リテラルへ帰着するとき（リテラルを直接呼ぶ形と、リテラルへ不変束縛した裸の名前）。そのリテラルの値スロット宣言を読む。ただし関数型のパラメーター数がそのリテラルの値スロット数と一致するときだけである — 食い違うのは部分適用で既にいくつか束縛済みの形であり（f := { a: Int, b := 2 | … } の f(1) は { Any | … } になる）、残りスロットの既定値の有無をリテラルの並びから決められない。
• 呼び先が std のメンバーのとき。std のメンバーは既定値を持たない（std/index.md）ので、パラメーターが 1 つでもあれば必ず止まる。カタログは既定値を表す綴りそのものを持たないため、この前提は綴りの約束ではなく構造で保たれる。
• 素通し条件: 実引数が 1 つ以上ある呼び出し・パラメーター 0 個の関数・呼び先の型が関数に確定しない位置・上記 2 つのどちらでも既定値の有無を引けない位置（不透過な高階パラメーター・部分適用の結果を受けた名前など）。本体を持たないリテラル（構築子）の C() も関数型にならないので対象外で、実行時が backstop である。

値コンストラクターパターンの payload 個数

match の値コンストラクターパターン Tag(pat…)（修飾形 Name.Tag(pat…) を含む。prelude.md §8.4）で、Tag の payload 個数が宣言から確定し、書かれたサブパターンの個数がそれと食い違うとき報告する。コードは arity-mismatch である — 引数数の不一致そのものなので、パターン専用の言い方は作らない（§2.15 のハンドラーの操作スロットと同じ扱い）。

• 健全性の根拠: タグの payload 個数は enum 宣言（prelude の Option / Result を含む）が決めるので、個数の合わないパターンは照合に入る前に必ずエラーになる。個数を通すと payload の無い位置を読みに行き、書いたエラーとは無関係な診断（添字が範囲外）になるため、照合より先に個数を見る。
• 無引数 bare タグは対象外: Tag（括弧なし）は payload を持つタグに対してもタグ判別だけを行い一致する（同 §8.4）。個数の不一致ではないので報告しない。
• 入れ子も対象: payload 位置の型がまた closed variant に確定するなら、その位置のサブパターンにも同じ判定を行う（Ok(Some(a, b))）。
• タプル要素位置も対象: タプルパターンの要素は再帰照合される（prelude.md §8.4）ので、そこに置いた値コンストラクターにも同じ判定を行う（(Some(a, b), 2)）。要素の型は列の型が持つ。判定は主語の型から辿るので、照合対象がタプルで closed variant に確定しない match でもかかる。
• 素通し条件: 列の型が確定しないとき・列の型が closed variant に確定しないとき・タグがその列の宣言タグ集合に無いとき・タプルパターンの要素数が列のタプル型と食い違うとき（タプルの個数不一致は本判定の管轄でない）。ガード付きアームも対象である — ガードは照合が済んでから評価されるので、個数のエラーはガードの真偽に依らず現れる。

2.9 分岐の収束と網羅性

分岐が型として収束すること、match が closed variant を過不足なく覆うことを要求する。いずれも契約系の診断である。

分岐の結果型に収束を要求

§3 は if 分岐・match アームの結果型が割れた場合、合流結果を Any に倒して推論を続ける（漸進的な挙動）。本規則はそれとは別に、分岐が確実に割れるときエラーを報告する。§2.5「名前付き関数の結果型」の「暗黙 Any を結果型に許さない」を分岐合流まで広げたものである。

• 対象: 完全適用された if cond {then} {else} の then/else サンク結果型、match subject { arms }（subjectful / subjectless 両形）の各アーム body（=> の右）末尾式型。部分適用（if (c) のみ等）や分岐構文でない呼び出しは対象外。when（片枝で false 側が Unit）/ while（戻り値が break(value) で任意化）は「分岐が割れた」のではなく構造的に Any になるため対象外。match で catch-all（_ => body）が無いときの実行時 Unit フォールスルーは見ない（明示アーム body 同士だけを比較する）。
• 関数結果の合流も対象（return / ? bail）: §2.2 のとおり関数結果型は末尾式の fall-through 値と本体中の各 return e 引数型（および ? の失敗 bail 型。language-spec.md §16.5）を join して解く。? の失敗 bail が寄与するのは失敗 variant 型（脱出する値は Err / None で成功 payload を持たないため、Result は Err(E)〔成功要素は未制約〕、Option は None）。すなわち bail の成功 payload 型は関数の成功型を制約しない（Err の E だけが関数結果へ流れる）。これにより Ok 型の異なる逐次 ?（§16.5 の process 例）も末尾値と収束する。本規則はこの合流位置にも収束判定を掛け、確実に割れる脱出経路を報告する（同一関数で return None と return Err(…) を混ぜる、? を Result / Option 非返却の関数で使い末尾値と bail 種別が割れる等）。判定は下記 consistency と同一で、Option と Result は別種として非整合、Unknown / Any / 型変数は wildcard。bail の成功要素を Any として寄与するため、種別（Option vs Result、bail vs 末尾）の違いだけが収束判定に効き、成功 payload 型の違いは割れと断じない。
• 合流を判定する境界は「呼び出しで入るユーザー関数」だけ: return / ? は最寄りのユーザー関数境界から脱出するが、if / when / while / 反復メソッド（each）のブロックと conduit 関数（language-spec.md §18.2 / §18.3）は透過で、そこは境界にならない。よって引数位置に現れたブロックそれ自体には収束判定を掛けない — 掛けるとブロックの末尾値（典型的には Unit）と bail の失敗 variant が割れて偽陽性になる（while {…} { v := f()? … } 等）。ブロック内の脱出型は、外側の関数の合流（? / return の走査は引数位置のブロックへ入る）が引き続き見る。呼び先ごとの透過判定は行わないため、不透過なユーザー高階関数に渡したブロック単体の割れは見逃す（見逃し側＝誤検出ゼロ）。
• 判定は gradual な型整合性（consistency）で行う: Any・型変数・Unknown アームは任意の型と整合する wildcard とみなし、確実に非整合なアームの対があるときだけ報告する。if c {1} {"a"}（Int と String）は報告するが、if c {Some(1)} {None}（Option(Int) と Option(Any)）や if c {1} {f(x)}（片側が Any / 型不明）は報告しない。
• Variant（タグ）同士は整合扱い: 異なるタグ（Circle(…) と Rect(…)）は同一 enum に属しうるため割れと断じない（合流結果は §3 のとおり同一 enum なら親 enum 型に持ち上がり、そうでなければ Any。後者は型エラーではない）。record 同士も幅構造型で共通の幅型を持ちうるため整合扱い。親 enum 型とその所属タグの対も整合扱い（タグ値は親 enum 型の値なので割れではない）。双方の所属 enum 名が判明して食い違うときだけ確実な非整合として報告する。
• Result はエラー型 E も見る: 成功型 T と同じく E の対にも整合性を掛ける。E は §3.4 の join で確実に割れると Any に倒れ、その Any はネスト位置なので§2.5「値束縛の型」が辿らない（同規則が E を don't-care として除外している）ため、E の割れはどの規則からも見えなくなる。ここで見ることで、割れは Any に倒しつつ本規則が報告するという二段構えが E にも及ぶ。未制約な E（Ok(5) のように E を確定させない構築。内部表現では不在）は確定情報が無いので Unknown と同じ wildcard 扱いで、割れと断じない。
• g: {Int | Result(Int)} のもとで if (c) { g(1) } { Err("boom") } は報告する（Error と String が確実に非整合）。
• if (c) { Ok(()) } { Err("x") } は報告しない（Ok(()) の E が未制約）。
• ファイルルートは対象外（discard コンテキスト）: ファイルレベルの暗黙リテラル（language-spec.md §13.1）の結果合流には収束判定を掛けない。ファイルの「結果値」は誰も受け取らず、プロセスは終了コードだけを返すためである（language-spec.md §17.4 が宣言結果型 Unit を discard コンテキストとして結果照合から外すのと同じ理屈）。これによりトップレベルに達した ? の失敗 bail（language-spec.md §16.5・hikari-command.md §5.4 が定める挙動）が書ける — println("x") の Unit と bail の Result が合流する形は割れではなく、実行時に exit code 1 として現れる。関数の中の合流は従来どおり判定する。
• 推論精度は変えない: 判定は分岐収束の診断専用で、§3 の join の精度は変えない。診断を出すだけで、合流型自体は引き続き Any に倒す。

closed variant の match に網羅性を要求

language-spec.md §16.4 は「網羅性は言語として静的に保証しない」（受け手が未知 kind 用 default 分岐を持つ慣習）とするが、本規則は match subject { arms } の照合対象の型が closed variant に確定し、覆われないタグが確実に存在し、catch-all が無いとき被覆漏れを報告する。非網羅 match は実行時に panic せず ()（unit）にフォールスルーする（prelude.md §8.4）ため「到達すれば確実に panic」には乗らず、本節「分岐の結果型に収束を要求」と同じ契約系の診断である。

• ガード付きアームは網羅に貢献しない: pattern | guard => body はガードが実行時に偽になりうるため、そのパターンがあるタグを完全に覆っても覆ったとみなさない。全タグ列挙でもいずれかがガード付きなら網羅未達。subjectless match（アーム頭が Bool 述語）は closed variant の照合対象を持たないため対象外。
• closed variant と必要タグ集合: prelude の Option(T) → {Some, None}、Result(T, E) → {Ok, Err}（E を変えてもタグ集合は不変）、ユーザー定義 enum（全 alt が Variant の OneOf、language-spec.md §17.4）→ 宣言した各タグ名。単一タグ enum（alt 1 個）はそのタグだけが必要。
• タグを覆うパターン: 値コンストラクターパターン Tag(自明な束縛…)（payload が全て小文字 bare 束縛または _）と無引数 bare タグ Tag（prelude.md §8.4）がそのタグを完全に覆う。修飾コンストラクターパターン Name.Tag(…) / 修飾 bare タグ Name.Tag（language-spec.md §17.4）も同じ被覆規則で bare 形と等価に数える。OR（positional 複数列挙）は各 positional を見る。複数アームにまたがる被覆も合算する。
• 修飾形は所属 enum の一致を要する: Name.Tag の Name が照合対象と異なる enum に解決できるとき（照合対象が Color の match に Auth.None が紛れる等）、タグ名が同じでも被覆に数えない。この場合は保守側に倒すのではなく、被覆しないと確定した上で網羅性判定を続行する（他に当該タグを覆うアームが無ければ通常どおり非網羅を報告）。
• 入れ子サブパターンの被覆（行列 usefulness による判定）: payload に自明でないサブパターン（入れ子の値コンストラクター・素の値・レコード等）を持つ Tag(…) はそのタグを部分的にしか覆わない（Ok(Some(x)) は Ok(None) を覆わない）。判定は payload 位置の相関を保ったまま行い、payload 位置が closed variant なら内側タグの被覆漏れを内側まで見る。非 variant 位置（Int / String 等）は無限型として wildcard でのみ覆われるとみなす。これにより Ok(Some(x)) / Ok(None) / Err(e) を網羅、Ok(Some(x)) / Err(e) を非網羅（Ok(None) 漏れ）と判定する。witness は欠落した値の形で示す（whole-tag 欠落は None / Some(_)、入れ子欠落は Ok(None) / Some(Some(_))。無限型位置は _ で描画）。
• 健全性: ある位置でタグ T（または非 variant 位置の T ならざる値）を覆うアームが無ければその値はどのアームにも一致しないので、報告は常に正しい。複数アームの被覆は合算する（Some(0) / Some(x) は Some(x) の wildcard が Some を完全被覆 → None だけ報告）。
• 直積の隙間を捕捉: 多 payload タグ（Rect(a, b)）は各 payload を独立に見ないため直積の隙間（Rect(Some(x), 0) / Rect(None, y) が Rect(Some(_), _) を漏らす類）を検出する。非 variant 位置を無限型として扱う帰結として、リテラル payload だけでタグを覆う match（Some(0) / None）は Some(_) 欠落として非網羅になる。
• gradual 列は隙間を主張しない: payload 位置の型が Any / 型変数 / 不明のとき、その列は列挙できないのでどのパターンも通す（隙間として報告しない。誤検出ゼロ）。これも診断のための便宜であって覆う証明ではない — 下記「保守側被覆は診断のための便宜」と同じく、結果型が実行時 Unit フォールスルーを混ぜるかどうかの判定には数えない。Result(Any) の Ok(Some(x)) は Ok(5) を覆わないので、数えるとその値が () へ落ちる経路の照合まで消える。
• 入れ子位置の修飾タグも所属 enum を照合: 上記「修飾形は所属 enum の一致を要する」は payload 位置にも及ぶ。行列の各列は型を持ち回るため、入れ子の修飾タグ（Ok(Auth.None)）も列の型（Ok の payload 型）の所属 enum と照合し、異なる enum の同名タグは被覆に数えない。受信者を enum 型値へ解決できない修飾形は従来どおり保守側で被覆扱い。この保守側被覆は診断のための便宜であって、覆うことの証明ではない — 報告を増やさないために覆い扱いへ倒しているだけなので、match の結果型が実行時 Unit フォールスルー（prelude.md §8.4）を混ぜるかどうかの判定では覆いに数えない（この判定は型消去（language-spec.md §17）が消してよい位置を決める材料になるので、覆いを過大に数えると実行時に () が通る経路の照合まで消える）。
• catch-all: _ => body または Any 型パターンがあれば常に網羅とみなす。
• payload 位置の型付き束縛は、列を覆うと確かめられるときだけ完全被覆: Tag(name: T) の T がその位置の payload 型の全値を覆うと確かめられるとき（T が Any・payload 型と型等価・payload 型の値が T へ確実に一致すると型消去（language-spec.md §17）の判定が言う組）は wildcard と同じ完全被覆に数える。確かめられないときは列挙不能とし、その match は網羅性も冗長性も報告しない（保守側）。Circle(r: Pos) は述語を外れた Circle(0) を覆わないので完全被覆にできず、かといって Circle(_) 欠落と報告すると誤検出になるためである。覆うと確かめられる形（Ok(v: Int)）まで列挙不能へ倒してはならない — そちらは他のタグの被覆漏れを報告できなくなる。アーム頭に書いた同じ綴りがAny 以外を列挙不能として扱う（下記「素通し条件」）のに対し、payload 位置は列の型が引ける分ここまで精密にできる。
• 素通し条件: 照合対象の型が closed variant に確定しないとき（Unknown / Any / 型変数 / 非 Variant を含む OneOf / 展開不能な遅延型適用）は報告しない。再帰ジェネリック enum の遅延型適用（§2.4）は判定時に 1 段ずつ展開して closed variant として扱う。また「特定タグの被覆」とも catch-all とも分類できないパターン（一般のレコードパターン・素値パターン・型パターン等）が 1 つでも混じる場合は保守側で報告しない。これにより Option / Result / enum のタグだけで構成された明快な match に限って網羅性を強制する。
• 「Option を T の所で未開封使用」は §2.4 で既出: 未開封の Option(T) / Result(T) を要素 T が要る位置（型注釈つき束縛・型付き関数引数・タプル/record 分解）に置くエラーは、§2.4 の照合が既に検出する（x: Int := Some(1) は型不一致）。本規則（網羅性）の対象外。

到達しえないアーム・冗長な catch-all

本節「closed variant の match に網羅性を要求」の網羅性（被覆漏れ＝下からの不足）と対をなす、被覆過剰（上からの冗長）の収束系診断。match subject { arms } の照合対象の型が closed variant に確定するとき、確実に評価されない次のアームを報告する。match はパターンを上から試して最初の一致で確定し、catch-all は全アームが外れた後に最初の 1 つだけが使われる（prelude.md §8.4）ため以下は死アームである（ガード付きアームはガードが偽になりうるため、それより後ろのアームを死アームとは断じない）。

• 全値一致パターンより後ろのアーム: 先行アームが全値に一致する（Any 型パターン、型付き束縛 name: Any）と、それ以降のアームは到達しない。
• 2 つ目以降の catch-all: catch-all は最初の 1 つだけが使われるため、2 つ目以降の _ => body は到達しない。
• 先行アームで完全被覆されたタグ: あるタグ T を完全に覆うアーム（bare タグ T / payload 全 wildcard の T(_…)、または修飾形 Name.T / Name.T(_…)）より後ろに現れ、OR の全 positional が被覆済みタグだけのアームは到達しない（Some(x) => … Some(0) => … の 2 つ目）。
• 冗長な catch-all（不要 default）: closed variant の全タグが catch-all 以外のアームで完全被覆されているとき、catch-all は決して評価されない冗長アーム（Some(x) => … None => … _ => 0 の _ => 0）。網羅済みを whole-tag 完全被覆（各タグを payload 全 wildcard で覆うアームがあること）で確かめてから報告する。
• 健全性: 本節の「完全被覆」は payload を wildcard で覆う whole-tag 被覆に限って数える。これは意図的に保守側で、入れ子の部分被覆だけで網羅が成り立つ場合は catch-all を冗長と断じない（見逃す）。列挙不能なパターンが紛れても、到達不能の根拠を「先行する全値一致」「2 つ目以降の default」「先行する whole-tag 被覆」に限るため過剰報告は生じない。照合対象の型が closed variant に確定しないときは何も報告しない。

== / compare スロットの本体は中断しない

== / compare の名前で宣言されたスロットの本体が中断するとき報告する（language-spec.md §9.1・§9.4）。

• 判定は §2.15 の効果推論が担い、診断は undeclared-effect である。 これらのスロットは結果型に Susp（language-spec.md §17.9）を許さないので、中断は宣言との食い違いとして §2.15「宣言との照合」の定義側に落ちる。専用の診断コードは持たない。
• 効果は呼び先まで辿るので、判定はスロット本体に直に書かれた ! / sleep / wait_any に限らない。
• 見るのは Susp だけである。 compare / == は効果を持たない（prelude.md §17.6）が、他のラベルまで一度に締めると本規則が咎める範囲を越える。
• なぜ規則にするか: 等価と順序は式のどこにでも現れる。中断しうると a == b を含む式がすべて中断点になり、実行形が呼び出し規約に乗る。規則を置くことで、比較は受け手の種別に依らず中断しないと言い切れる。
• 中断を伴う比較が要るなら、比較の結果を先に求めてから sort_by / sort_with（prelude.md §6）へ明示コンパレーターとして渡す。そちらは呼び出しなので中断してよい。

導出形が定まっている演算子はスロットにできない

!= < <= > >= の名前でスロットを宣言したとき報告する（language-spec.md §9.1・§9.4）。位置はスロット宣言。

• なぜ規則にするか: != は == の否定として、< <= > >= は compare の結果から導かれる。実行系はその綴りのスロットを参照しないので、宣言しても期待どおりには動かない。黙って無視すると書いた人はエラーに気づけないため、定義した地点で止める。
• 代わりに何を書くか: < <= > >= の代わりに compare を、!= の代わりに ==（または compare）を定義する。導出はそこから走る。
• 算術（+ - * / % **）は対象外。 language-spec.md §8.1 が受け手の同名スロットによる差し替えを明示的に認めている。- は単項が negate からの導出を持つが（§8.6）、- という綴りのスロット自体は二項の減算として正当なので報告しない — 宣言だけを見て単項を差し替えるつもりだったかは判別できず、報告すれば正しい二項の宣言を誤検出することになる。

== と compare の同居は禁止

1 つのオブジェクトリテラルが == スロットと compare スロットを両方持つとき報告する（language-spec.md §9.4）。位置はオブジェクトリテラル — 悪いのはどちらか一方のスロットではなく、2 つを同居させたリテラルそのものである。

• なぜ規則にするか: == は compare から導出されるため、両方を書けると等価と順序がずれた受け手を作れてしまう。§9.4 が「一貫性を構造的に保証する」と述べているのはこの禁止のことで、黙ってどちらかを選ぶのではなく禁じる。
• 単独の定義は正当。 == だけ・compare だけを持つ受け手は引き続き書ける。禁じるのは同居だけである。
• 判定は 1 つのリテラルのスロット集合で閉じる。 別々のリテラルが片方ずつ持つ形は同居ではない。
• 禁止は静的検査が持つ。 実行の手前で塞ぐので、同居した受け手がどの実行系にも届かない。

OR パターンは全枝で同じ名前を束縛する

OR（カンマ区切りのパターン列、prelude.md §8.4）の各枝が違う名前を束縛するアームを報告する。どの枝が当たっても body から見える名前が同じでなければ、body は自分が読める名前を静的に決められない。

• 対象: match subject { arms } の subjectful アームで、OR の枝が 2 つ以上あるもの。枝ごとに「その枝が一致したとき body へ入る名前の集合」を求め、集合が全枝で一致しなければ報告する。
• 名前を集める位置: レコードパターンの field（{ a } / { a := v } / { a: T }）・値コンストラクターパターンの payload 位置にある小文字始まりの bare 識別子（Some(x)）・型付き束縛（name: T）。_ は束縛しないので数えない。
• 束縛の無い枝同士は制約を受けない。 0, 1, 2 / None, Empty のようにどの枝も何も束縛しない形は「全枝で一致」である（空集合同士）。
• 値つきスロット name := v も束縛である（prelude.md §8.4。{ a := 1 } => a は 1 を返す）。束縛を body で読まない分岐でも規則はかかる — 読むかどうかで規則が変わると、body を書き換えただけでパターンが合法になったり違法になったりする。値で振り分けたいだけなら アームを分ける（{ a := 1 } => … と { b := 2 } => …）。
• 診断はアームの位置に出す。 報告文は不足している名前を挙げる（variable 'b' is not bound in all patterns と同型）。
• 機能を削るのではなく未定義の穴を塞ぐ規則である — 現状この形は、当たった枝によって body の名前参照が実行時 undefined になったりならなかったりする。

2.10 代入と可変状態

代入が実行時に成立するか（前 2 項。「到達すれば確実に panic」）と、代入と伸長が静的型を裏切らないか（後 4 項。契約系）を検査する。後者が class b の健全性を可変状態について成立させる分担は、末尾の「可変状態と健全性」に集約する。

slot 代入

slot アクセスへの代入 recv.x := v / recv.x = v（および動的アクセス recv.[k] := v / = v、language-spec.md §3.10）で、到達すれば確実に失敗する代入を報告する。

• 要素（数値プロパティ recv.0 / 整数リテラルキー recv.[0]）への代入は、受け手に関わらず常に不変（language-spec.md §7.4 — List・タプル・String・Bytes・range はいずれも要素を差し替えられない）なので、shape を解決せず常に報告する（cannot assign to immutable positional slot）。
• スロットへの :=（recv.x := v）は、受け手に関わらず常にエラーである（language-spec.md §6.2 — スロット集合はリテラル宣言時に固定されるので、:= が成立する受け手は存在しない）。要素への代入と同じく shape を解決せず常に報告する（cannot add slot ':='）。受け手の静的型がメソッド集合の閉じた型（§2.7）に確定して同じ位置に no such slot or method が積まれていても、:= ではスロットを足せないことの方が具体的なので本項が残す（2 度鳴らさない）。素通しにはできない — 落とす側に := の受け口が無いので、黙った位置は内部エラーで止まる。
• スロットへの = は、recv がスロット集合の確定するオブジェクト値（§2.10）に帰着するとき、実行時 language-spec.md §6.2 の規則どおり次を報告する。

「スロット集合が確定する」範囲

record は幅構造型であり、宣言された型が挙げるより多くのスロットを値が持ちうる（注釈付き record パラメーター・戻り値・import 越境の値は、別の視点が具体型で宣言したスロットを持っているかもしれない）。そのためスロットの検査は受信者が次のいずれかに帰着する場合に限る。スロット集合がリテラル宣言時に固定される（language-spec.md §2.4）ことは、この制約を解かない — 固定されるのはその値のスロット集合であって、静的型が値のスロット集合を言い当てられるようになるわけではない。

§2.7 がメンバー解決を宣言集合に閉じることは、この範囲を広げない。 あちらが定めるのは触れてよい名前であって、値がどのスロットを持つかではない。実行時に確実にエラーになると断じるには後者が要るので、受信者の帰着先は上記に限ったままである。

1. データオブジェクトリテラル（{…|}）に直接帰着、または
2. それを immutable 束縛（:= / immutable slot） した名前（別名連鎖 b := a も辿る）。

immutable 束縛なら値はそのリテラルに固定されるため健全。素通し: mutable ローカル（=、後で別の値に再代入されうる）・注釈付き束縛・関数引数/戻り値・import 越境。この制限がかかるのは受け手が record でありうるからで、静的型がメソッド集合の閉じた型に確定する受け手（§2.7 の List / Tuple ほか）はそちらが由来を問わずに検査する。

動的アクセスのキー recv.[k] は要素の並び専用（Int キー、language-spec.md §3.10）で、k が静的に定数（整数リテラル、またはそれへの immutable 束縛名）のときだけ解決する。非定数キーは素通し。

束縛の重複と immutable への代入

ローカル束縛（language-spec.md §6.1）のうち、スコープの構造だけで
確実に成立しないと分かるものを報告する。値の型も受け手の shape も要らないので、上の slot
代入と違って「スロット集合が確定する」のような制限はかからない。

外側スコープの同名は衝突ではない（language-spec.md §6.1）。別の
オブジェクトリテラルの同名を結果として隠すのは正当なので、重複の判定は同一スコープに
限る。slot-list 領域と body 領域は同じリテラルに属するので
（language-spec.md §13.1）、両者にまたがる同名は重複である。

スコープチェインには prelude が含まれる。 prelude の束縛は最外スコープの immutable 束縛
なので（language-spec.md §6.1）、println = f / max = 0 は表の 3 行目に
当たり cannot assign to immutable binding: name を報告する。prelude 名だけの特別規則では
なく、x := 1 の後の x = 2 と同じ行である。prelude は利用者のトップレベルより外側の
スコープに置くので、if := 5 / mutable max := 0 のような被覆は 1 行目の重複判定にかからない —
同じスコープへ混ぜると正当な被覆が再宣言に見えるため、鎖を 1 段挟んで別スコープにしておく
必要がある。

破棄子 _ は環境に入らないため対象外 — 同一スコープで何度でも書けて、_ = expr は表の
4 行目（束縛が見つからない）にも当たらない（language-spec.md §6.1）。

素通し: スコープ模型で束縛の有無を確実に判定できない位置（§2.13 と同じ範囲 — 判定
不能な前方参照・動的 import 越境）。

可変ローカルの型安定性

可変ローカル x（body 内の mutable x := … 宣言）が既に確定した具体型 T を持つとき、再代入 x = v の v の静的型が T に収まらないと確定できるなら報告する。判定は §2.4 の注釈位置と同じ方向のあるもの（T の位置に v を入れて確実に panic するか）を使う — 代入が問うのは「T と重なるか」ではなく「T に収まるか」だからである。対称な重なり判定を使うと T が record 型のときスロットの型も幅も自由に差し替えられてしまう（o.r = { mutable x := "s" |} が o.r の宣言型 { x: Int |} に対して通ってしまう）。mutable x := 0（Int 確立）の後 x = "a" を型変更として検出し、注釈付き確立 mutable x: Int := 0 の後の無注釈 x = "a" も同様に塞ぐ。受け手を伴うスロット代入 recv.name = v は本節「スロット代入の型安定性」が担当する — 本規則は名前の scope 探索が本体で、そちらは受け手型の解決が本体である。

• 健全性の位置づけ: 型変更再代入はその地点で panic しない（language-spec.md §6.1 のとおり = は可変な束縛の更新として許容）。捕捉するのはその後の読み出しであり、mutable x := 0 の後 x = "a" を許すと x + 1 が確実に panic する。本規則は本節の残る 3 規則と対で class b の健全性を成立させる（下記「可変状態と健全性」）。
• 確立 vs 再代入: x が宣言直後で型なし（前方参照プレースホルダー）・既存型 Unknown のときは確立とみなし検査せず記録する。以降の = が検査対象。違反を報告しても新しい右辺型は記録しない — §2.2 のとおり再代入は確立済みの型を変えないためで、右辺型に乗り換えると違反 1 つを根拠に以降の照合の基準が動いて診断が連鎖する。
• スコープ探索: 型安定性は契約系の診断なので、クロージャが捕捉した外側可変ローカルへの型変更再代入も違反として報告する（前方参照の読み飛ばしを行わず、捕捉した外側の束縛まで辿るスコープ探索）。既確立の具体型を持つ可変スロット（{ mutable x := 0 | …}）の body 内 = 再代入も同様に検査する。
• 素通し条件: 既存型か右辺型のいずれかが未確定（Any・Unknown・型変数）。実束縛がまだ無い（確立）ときも素通し。
• 既確立型は照合の前に広げる: 既確立型は多くの場合値 1 個から推論した型であり、位置の型としては狭すぎることがある（書き手が注釈したスロット型でも、{ c: Red |} のように単一タグに絞った形は同じく狭い）。次の 2 種類の位置を広げてから方向のある判定に掛ける。広げるのは照合のためだけで、診断の文面には元の既確立型を出す。辿るのはコンテナーの内側（List / Option / Result / Future の要素・tuple の要素・record のフィールド）までで、union の候補と関数型の引数・結果へは降りない — そこに単一タグの既確立型が直に現れる形は実際上作れないので、降りない側（報告する側）に倒して機構を小さく保つ。
• Never は wildcard として扱う — 空リテラル [] 由来の未制約な位置である（mutable x := [] の List(Never)）。広げないと mutable x := [] の後の x = [1] が誤検出になる。
• enum のタグはその親 enum 型へ持ち上げる — mutable c := Red が確立するのは「Color のどれか」であってタグ Red そのものではない（§3.4 の join が同一 enum のタグを親へ持ち上げるのと同じ向き）。広げないと c = Green や親 enum 型を返す呼び出しの代入が誤検出になる。親 OneOf を持たない単一タグ enum はタグ自身が enum 型なので広げない。無関係な型への代入（c = "s"）は広げても報告し続ける。

スロット代入の型安定性

スロット代入 recv.name = v で受け手 recv の静的型が record でスロット name に確定した具体型 T を持つとき、v の静的型が T に収まらないと確定できるなら報告する。判定は本節「可変ローカルの型安定性」と同じ方向のあるもので、§2.4 の注釈位置・本節「可変な器への書き込みの要素型照合」と揃える — 同じ式の可否が位置によって食い違わないことが要件である。本節「可変ローカルの型安定性」が可変ローカルについて行う検査をメンバー経路へ広げたもので、o := { x = 1 |} の後の o.x = "s" を型変更として検出する。

• 受け手の型は静的型そのものを使う。したがって推論 record（o.x = "s"）・inner-name 型（self.x = "s"）・宣言パラメーター型（{ r: { x: Int |} | r.x = "s" }）の三経路を一様に覆う。受け手の値のスロット集合が確定する（§2.10）かは問わない — §2.10 が「slot が存在するか・代入してよいか」を値の shape で見るのに対し、本規則は「その slot の型を変えていないか」を型で見る別軸の検査である。
• 健全性の位置づけ: 型変更代入はその地点で panic しない（language-spec.md §6.2 のとおり可変スロットへの = は正当）。捕捉するのはその後の読み出しで、o.x = "s" を許すと o.x + 1 が演算子の型不一致で確実に panic し、p: { x: Int |} := o は束縛地点の実行時照合で panic する。本規則は本節「可変コンテナー位置の不変性」と対でこれを塞ぐ。
• 素通し条件: 受け手の静的型が record でない・スロット name を持たない・スロット型が未確定（Any・Unknown・型変数）・右辺型が未確定。動的アクセス recv.[k] はキーが静的な定数文字列に解決できるときだけ対象とする（§2.10「動的アクセスのキー」と同じ判定）。スロット型を照合の前に広げる規約も本節「可変ローカルの型安定性」と共通である（Never は wildcard・enum のタグは親 enum 型へ）。
• 動的な要素アクセスは対象外: recv.[k] は Int キーで Sequence の要素を引く形しか無く（language-spec.md §3.10）、要素は不変なので代入経路そのものが存在しない。スロットの動的キーは言語から撤去されており、キーで引く辞書は std:map が型の付いた値として提供する。
• := と不正な = は対象外: スロットへの :=・存在しない slot への =・immutable スロットへの = は §2.10 が既に報告する。本規則が見るのは正当な可変スロット代入だけである。

可変コンテナー位置の不変性

型注釈位置（束縛・パラメーター・分解・スロット既定値・アスクリプション・宣言結果型）で宣言型と静的型を並行に辿り、可変コンテナーの位置で両者の型が等しくないなら報告する。可変コンテナーの位置とは次の 2 つで、いずれも実行時に中身を差し替えられる。

• record 型のフィールド（language-spec.md §17.2）。可変スロット（mutable）は再代入で別型の値を持てる
• std の可変な器の型引数 — std:array の Array(e) の e（set / push / update が要素を差し替える。std/array.md §3）と std:map の ScratchMap(k, v) の k / v（set / update がキーと値を書き込む。std/map.md §3.1）

したがって record は幅部分型を持ち深さ部分型を持たない — { x: Int, y: Int |} の値は { x: Int |} の位置に通るが（幅。スロットは実行時に減らせない）、{ x: Int |} の値は { x: Any |} の位置に通らない（深さ）。

• なぜ代入地点の検査では足りないか: 本節の型安定性の 2 規則と「可変な器への書き込みの要素型照合」は受け手の静的型に対して代入を検査する。同一オブジェクトに広狭 2 つの静的視点が同時に存在できると、狭い視点では違反である代入が広い視点では正当になり、どちらの地点にも報告できる違反が無い（可変な器を共変に扱ったときに生じる不健全性そのものである）。不変性はこの 2 視点の同時存在そのものを禁じる。
• 不変にしない位置: Option / Result / Future の payload、tuple の要素、List(T) の要素型、そして std の不変な器 SortedMap(k, v) / InsertionMap(k, v) / OrderedSet(e) の型引数。いずれも構築後に中身を差し替える手段が無いので共変で健全であり、従来どおり §2 の照合に委ねる（language-spec.md §7.4 のとおり List・タプルはいずれも不変である）。
• 素通し条件（wildcard）: 静的型側が Any・Never・型変数・Unknown。Never は空リテラル [] 由来の要素型・None 由来の payload 型で、値を持たないので差し替えの起点にならない。宣言型側の Any は素通ししない — { x: Any |} / List(Any) の位置へ狭い型の値を通すことがこの穴の本体だからである。ここだけは他の規則の「未確定は素通し」と非対称になる。
• wildcard の素通しは型の深さを問わない: 可変コンテナー位置の型を突き合わせるとき、静的型側の wildcard はその型のどの位置に現れても素通しさせる。{ drop_idx: Option(Int) |} の位置に { drop_idx: Option(Never) |}（None を置いた record）を渡す形は、フィールド型を丸ごと比べると食い違うが、食い違っているのは値を持たない Never の位置だけなので報告しない。上の素通し条件を型の最外周にだけ掛けると、この形が誤検出になる。
• 入れ子の Any はここで gradual 境界になる: { p: Patch |} の位置に静的型 { p: Any |} の値（{ mutable p := … |}）を渡す形も上の素通しにかかり、報告しない。この位置には広狭 2 視点が残る（{ p: Any |} 側から Patch でない値を書き込める）が、Any を経由した領域は language-spec.md §17 の健全性保証の適用外である。暗黙に入り込むことはない — 入れ子位置の Any は§2.5「値束縛の型」が型注釈を要求するため（record スロット既定値の { p: Any |} も対象）、そこへ到達するには書き手が Any を明示している。欄の型を確定させればこの素通しは消える。
• refinement は基底で比べる: 述語の充足は§2.11「境界の証明義務」の証明義務が担うので、本規則は refinement を基底型へ降ろして比較する。
• 実行時照合より厳しい: 実行時の matches（language-spec.md §17.4）は record を幅構造型として照合し、フィールド型も部分型で通す。本規則はそれより狭く受理するので、実行時なら通る値を静的に拒む場合がある。契約系の診断として実行時照合より狭く受理するもので、実行時照合そのものは不変である。
• Any を書けば逃げられる: 幅の広い引数を受けたい関数は、フィールド型・要素型ではなくその位置全体を Any にする（{ r: Any | … }）。record の一部フィールドだけ動的にしたい設計は本規則の下では表現できず、そのフィールドを持つ record 型を分けるか位置全体を Any にするかの選択になる。
• 入れ子は辿る: 不変にする位置は可変コンテナーに限るが、そこへ到達するためには不変でない位置も辿る。Option({ x: Any |}) の位置に Option({ x: Int |}) を渡す形は、Option の payload を通って record フィールドに至るので報告する。辿る対象は Option / Result / Future の payload・tuple の要素・List の要素・record のフィールド・union（OneOf）の候補・タグ付きデータ（enum）の payload・関数型の引数と結果（下記）である。union とタグ payload を落とすと、そこを一段挟むだけで穴が復活する（Option で書けば報告されるのに enum で書くと通る、という食い違いになる）。
• union の候補は「すべての候補が食い違うときだけ」報告する: 宣言型が OneOf(A, B) で静的型がその候補のいずれかに収まる値のとき、実行時の照合は候補を順に試して 1 本でも通れば成功する（language-spec.md §17.4）ため、どの候補で束縛されるかは静的に決まらない。したがって照合が通りうる候補のすべてで可変コンテナー位置が食い違うときにだけ報告する。1 本でも食い違わない候補があれば、実行時はそちらで束縛されうるので報告しない（誤検出ゼロ）。
• 自己参照の候補は数に入れない: 宣言型が自己参照 union（type U := OneOf({ x: Any |}, U)）のとき、候補 U は同じ照合へ戻るだけで「食い違わなかった」ことにならない。食い違わない候補として数えると、他のどの候補が食い違っても報告が落ちる。候補が 1 つも残らないときは材料がゼロなので報告しない（誤検出ゼロ側）。
• 関数型の内側も辿る（結果位置に例外あり）: 宣言型が関数型のときは引数型・結果型へ降り、その中の可変コンテナー位置を検査する。{| { x: Any |} } の位置に {| { x: Int |} } を返す関数を渡すと、呼び出し結果を通して同じ値に広い視点が立つためである。例外は結果位置に限る — 渡す値が結果型を宣言しないインライン関数リテラルのとき、結果位置へは降りない。if / while に渡すサンクがこの形で、その「結果型」は内部の脱出値から拾ったものでサンク自身の表明ではないので、降りると誤検出になる。引数型位置はこの例外の対象外で常に辿る — §2.6「関数型注釈と実体シグネチャの整合」が「パラメーター型はどちらの場合も値自身の宣言なので常に照合する」としているのと同じ理由である。インラインサンクの分岐合流が record フィールドを広げた場合は、合流結果が Any を含むので§2.5「値束縛の型」が型注釈を要求し、書き手が Any を明示した時点で gradual 境界になる。
• その位置で構築するリテラルは対象外: p: { x: Any |} := { x := 1 |} は報告しない。宣言型が record・リストのとき検査はリテラルの構文形へ降り、フィールド／要素ごとに宣言型と突き合わせる（§2 の注釈位置と共通の降下）。降りた先の位置はそのリテラルが所有する新しいスロットであり、他の視点が同時に立ちようがないので不変性は要らない。既存の値を置いた位置（識別子・呼び出しの結果）では降下できないので不変性が効く。リテラルの中に既存の値を置いた形（xs: List({ x: Any \|}) := [rec]）は要素位置で rec に当たるので報告する。

可変な器への書き込みの要素型照合

std の可変な器（std:array の Array(e)、std:map の ScratchMap(k, v)）へ書き込むメソッド — Array の set / push / update、ScratchMap の set / update — の実引数の静的型が、受け手の型引数が定める要素型と確実に非整合なら報告する。根拠は契約系である — これらのメソッドは実行時に引数型を検証せず panic しないため「到達すれば確実に panic」には乗らず、破れが現れるのは後続の get / frozen の読み出しである。受け手の静的型は書き込みで動かない（Array(Int) のハンドルは "s" を書き込んでも Array(Int) のまま）ので、ここを開けたままにすると get が Int と主張する位置へ String が届く。

• 照合は型注釈位置とまったく同じ判断を下す: 書き込む実引数を、その要素型を宣言型とする注釈位置と同じ経路で照合する（構文形への降下を含む）。update はブロックの結果型を要素型に対して照合する。
• 素通し条件: 受け手が Array / ScratchMap と確定しない・要素型が未確定（Any・Unknown・型変数）・引数型が未確定。
• 不変な器（SortedMap / InsertionMap / OrderedSet）の insert / merge は対象外である。 新値を返すので受け手の静的型が動かず、引数の型が受け手の型引数と割れた呼び出しの結果型は §3.1 の単一化に従って Any 側へ倒れる（診断は出さない）。倒れた先は Any 境界なので class b の健全性は破れない。

可変状態と健全性

本節の型安定性・不変性・可変な器への書き込みの 4 規則は §2.1 の class b の健全性を成立させるために不可欠である。Hikari の可変状態は次の 2 つで尽きるため、この 2 行を塞げば「具体型を割り当てた評価点で値が型と整合する」が全域で成り立つ。

スロットの追加は可変状態ではない — スロット集合はリテラル宣言時に固定され、後から増えない（language-spec.md §2.4）。実行時のキーでスロットへ書く手段も無い（同 §3.10 の動的アクセスは要素の並び専用）。したがって「スロットの追加」「非定数キーの動的スロット書き込み」はいずれも塞ぐべき経路として存在しない。キーで引く辞書は std:map が担い、不変な値（SortedMap / InsertionMap）はここでいう可変状態に当たらず、可変なハンドル（ScratchMap）は表の 2 行目が塞ぐ。

代入の検査（型安定性の 2 規則と「可変な器への書き込みの要素型照合」）と不変性（「可変コンテナー位置の不変性」）は片方だけでは足りない — 前者だけなら広い視点を経由した代入が漏れ、後者だけなら単一の視点内での型変更代入が漏れる。

2.11 refinement 型の証明義務

refinement 型（language-spec.md §17.7）についての契約系の診断。境界での述語充足を実行前に証明させ、その証明が可能な形で述語が書かれているかを見る。

境界の証明義務

refinement 型（language-spec.md §17.7）が要求される境界へ流れ込む値について、述語の充足を実行前に証明できなければ cannot prove refinement predicate for '<name>' を報告する。実行時は同じ境界で述語が評価され、偽なら型不一致 panic になる（§17.7）ため、本規則はその実行時契約を実行前に見せる位置づけである。

「証明できない」で鳴る規則である（「述語が偽だと証明できた」ではない）。判定手続きは過小近似で、真だが手の届かない述語も「導けない」に落ちる — 本規則は §2.5 の Any 規律と同じ契約系の診断で、そこを書き手に明示のオプトインで埋めさせる。型の側のオプトインが refinement_opaque、値の側が式アスクリプション（下記「解消の道」）である。ただし「証明できなかった」の原因が書き手にどうにもできないものであってはならないので、下記の素通し条件がそれを切り分ける。

• 対象の境界: 宣言型が refinement 型に確定する境界。language-spec.md §17.7 の実行時照合地点 7 つのうち、式アスクリプションを除く 6 つである — 束縛注釈・分解束縛・パラメーター束縛（実引数とデフォルト）・スロットのデフォルト確定・関数型注釈の呼出時強制（実引数と宣言結果型）・enum の payload 構築。式アスクリプションから証明義務を外すのは、そこが本規則のオプトインの書式（下記「解消の道」）だからである。義務を外すだけで検査を外すのではない: アスクリプション境界でも「証明可能に偽」は報告する（下記）。
• 証明の材料: リテラルと定数、フロー絞り込み（§2.3）で得た事実、および関数契約（language-spec.md §17.4 の畳み込み結果）が与える refinement。材料の連言 P から述語 Q への含意を、P ∧ ¬Q の充足不能性として決定可能断片の中で判定する。定数リテラル（整数・文字列・真偽・Float）はその値が主張する事実（整数はその値そのもの、文字列は値と length!）を材料に加え、List リテラルは自分の length! を加える（[10, 20, 30] は length! == 3）。要素の値には触れない。

材料は弱くなる方向にしか倒さない — 材料 P を実際より強くすると偽の証明ができてしまうので、値について分かることが無い箇所は材料に入れない。この不変条件を守ったうえで、次の 4 つが材料を広げる。

• 定数束縛を経由した値: 再代入されない束縛（:=）に整数定数が入っているとき、その定数を材料に加える（n := 5 の後の p: Pos := n）。別名の連鎖（m := n）も辿り、値式そのものが定数式（2 + 3）のときも同じである。Float の定数束縛も同じ線引きで材料になる（Y := 4.0 の後の f(Y - 1.0)）。再代入されうる名前・スロット・パラメーターは追わない（束縛時の値が境界に届く保証が無い）。
• レコードの場所の材料（§17.7 のフィールドパス）: 境界へ直書きされたレコードリテラルのスロットへ降り、各スロットの値が主張する事実を場所ごとの材料に加える（{minLength := 3, name := "hello" |} は f.minLength == 3 と f.name.length! == 5 を与える）。辿るのは := で宣言された immutable スロットだけである — 可変性は shallow（language-spec.md §6.1）なので、= の mutable スロットは境界を通った後に中身が変わりうる。レコードを := 宣言した名前に束縛して渡した形（src := {…} の後の x: T := src）も同じ条件で辿る。
• 位置分解の要素: 分解束縛（a: Pos, b: Pos := (3, 4)）の右辺がタプルリテラルで要素数が名前の数と合うとき、各名前の境界へその位置の内側の式を材料として結び付ける。変数を経由した右辺と要素数の合わない右辺には対応を付けない。名前分解（{ x } := r）は位置ではなく名前で取るので対象外である。
• 境界へ渡る式の算術: 値式が整数の加算・減算・乗算（と単項マイナス）で組まれているとき、各項の材料から区間を伝播させ、得られた上下限を材料に加える（p: Pos に対する take(p + 1) は p >= 1 から p + 1 >= 2 を導く）。区間は実際の値集合を含む側にしか動かさないので、得られる材料は常に実際より弱い。除算・剰余・変数同士の積（非線形）・Float の算術は区間を作らない。

これらは証明にだけ使い、反証には使わない。下記「証明可能に偽」の判定は直書きの定数リテラル（レコードリテラルを含む）と静的型が運ぶ refinement だけを材料にする — 証明の材料が増えれば「証明できない」は減るが、反証の材料が増えると診断は増える方向にも動きうるためである。

• 素通し条件（誤検出ゼロ）: 次のいずれかに当たる境界では報告しない。
• 宣言側の述語が厳密でないとき — refinement_opaque（証明対象外の gradual 境界）と、決定可能断片の外にある述語がこれにあたる。後者は境界をどう直しても証明が通らないので、原因のある定義地点で本節「述語の断片適合」だけが報告する（二重報告の抑止）。
• 値の静的型が Unknown（型不明） に倒れるとき（§2.5「値束縛の型」と同じ切り分け）。Never（発散位置。§3.3）も同様で、値が流れ込まないため義務を課さない。
• 基底型の照合が既に落ちているとき（§2.4 の型不一致として報告済み。そこへ述語の話を重ねても書き手の助けにならない）。
• 目標の refinement が型変数の実体化で入ったとき。多相な関数のパラメーター型が型変数のとき、カリー化した部分適用の途中で別の実引数がその型変数を refinement 型に束縛することがある（if (c) { take(x) } { 0 } では then 枝の結果 Pos が if のシグネチャの型変数を束縛し、else 枝が { Pos } の境界へ渡るように見える）。この位置の Pos は書き手が宣言した契約ではなく単一化の結果で、実行時の契約 wrapper も型変数には述語を持たないので照合しない。書き手が明示的に書いた refinement は型変数を経由しないので従来どおり目標である。
• 安全網: 境界へ渡る式が、その境界を支配する条件で検査されている名前を含むとき。値式に現れる識別子のいずれかが、境界を字句的に囲む枝の条件か、同じ body でその位置より手前に書かれた分岐文の条件（when (x <= 0) { return 0 } のようなガード節）に現れるなら報告しない。書き手が条件で検査しているのにチェッカーが材料にできなかった箇所は絞り込みで直しようが無いので、ここで止める。条件と境界の間でその名前を束縛し直すか代入すると、条件はもうその名前について何も語っていないので覆いは外れる（when (b != 0) { b = 0; a / b } は報告する）。網は反証を抑止しない — 述語を満たしえないと証明できる境界は網に関係なく報告する（下記「アスクリプション境界では「証明可能に偽」だけを報告する」）。さもないとその報告が網の裏から破れる。§2.3 の対応範囲が広がるほど、この安全網に頼る箇所は減る。
• Any は報告する: 値の静的型が Any（gradual top）に確定するときは、述語の証明材料が無いため refinement boundary '<name>' receives an Any value を報告する。Unknown（確定できていない）と Any（動的だと確定している）を分ける点は §2.5「値束縛の型」と同じである。
• 判定手続きの強さは処理系の構成に依る: 断片の内外は構文だけで決まる（本節「述語の断片適合」）が、断片内の述語を実際に導けるかは判定手続きの完全性に依る。外部 SMT solver を有効にした構成では導ける範囲が広がり、本規則の「証明できない」の報告は減る。逆に下記「証明可能に偽」の報告は増えうる — そこは実行時に到達すれば必ず型不一致 panic になる箇所なので、増える方向は §2.1 の class b の健全性の側に働く。既定の構成（外部 solver 無し）でも健全性は同じで、差は導ける範囲だけである。
• 解消の道: 式アスクリプション（language-spec.md §17.1）で refinement 型に確定させる — f(v: Pos) と書けば静的型が Pos になり本規則を満たす。アスクリプションは式の評価地点で実行時照合される（language-spec.md §17 冒頭）ので健全性は保たれ、「ここは実行時検査に委ねる」という判断がソースに現れる。refinement_opaque が型の側のオプトインであるのに対し、こちらは値の側の同じ層のオプトインになる。
• 文面は述語と逃げ道を載せる: 本規則は「真だが証明できない」コードにも鳴る設計なので、期待型が type で名付けられていても述語の原文を添え（expected Pos (v > 0)）、上の解消の道を一文で示す。畳み込んだ契約は論理積として並べる。
• アスクリプション境界では「証明可能に偽」だけを報告する: アスクリプションは本規則のオプトインの書式なので証明義務は課さないが、材料と述語が両立しないことを証明できた場合（take(0: Pos) / q := (0: Pos)）は refinement predicate cannot hold here を報告する。そこは実行時に必ず型不一致 panic になる箇所で、見逃すと §2.1 の class b の健全性の反例になる。判定は「材料の連言と述語の論理積が充足不能」であることで、材料が定数リテラルでも refinement でもない値は判定できないので報告しない。フロー絞り込み（§2.3）が立てた事実は静的型として運ばれるため反証の材料でもある（when (x > 0) { return 0 } の後の take(x) は x <= 0 と Pos が両立しないので報告する）。
• 捕捉例・非捕捉例: p: Pos := 0 のように材料から述語の充足が否定されるもの、材料が足りず含意を示せないもの、値の静的型が Any のものを報告する。値の静的型が同じ基底の refinement で、その述語が宣言側の述語を含意するとき（Pos の値を refinement { v: Int | v >= 0 } の境界へ渡す）は証明成功として報告しない。
• 宣言型の内側へは値の構文形に沿って降りる: 宣言型が refinement を内側に持つとき（List(Pos) / Option(Pos) / { x: Pos |} / { Int | Pos }）、値が対応する構文形で書かれていれば、その構成要素ごとに本規則を再適用する。対象はコンテナーのリテラル（リスト・タプル・レコード）、variant 構築子の payload（Some(x) / Ok(x) / Err(x) とユーザー定義 enum のタグ）、および関数リテラルの結果位置（{ Int | Pos } の境界へ渡したサンクの脱出経路。§2.6「宣言結果型と全脱出経路の整合」と同じ収集器で全脱出点を集める）である。

降りる先へは内側の式をそのまま渡す — 型だけを見て降りてはならない。take(Some(5)) の Some(5) の静的型は Option(Int) なので、型木だけを並行に辿ると正しいコードに「証明できない」が鳴る。内側の式（5）を材料として渡せば定数証明もフロー絞り込みも安全網も要素位置で同じように効く。

関数の結果位置は、実行時に契約が挿さる境界にだけ降りる。 結果位置は他の位置と違い、境界に着いた値がそのまま照合されるのではなく、呼出時強制の契約（language-spec.md §17.4）が挿さって初めて照合される。降りるのは束縛注釈（h: { Int | Pos } := …）・代入注釈・実引数を受けるパラメーター注釈で、コンテナー要素・構築子 payload・enum タグの payload のように値として格納される位置は対象外である（そこでも関数は普通に呼ばれるが、契約が挿さらないので結果が宣言型と照合されない）。引数数と本体の形は問わない — 契約は呼出しごとに実返り値を照合するので、零引数サンクも同じである。スロット既定値へは降りない — 呼べば契約が挿さるが、そのオブジェクトが呼ばれるかどうかが静的に決まらないためで、見逃し側に置いて実行時照合を backstop にする。

• 構文形が無いときは宣言型と静的型を並行に辿る: 値が対応する構文形で書かれていない（変数経由でコンテナーや payload の中身が見えない）ときは、宣言型と値の静的型の型木を並行に辿り、対応する位置の refinement について本規則を適用する。o: Option(Int) を Option(Pos) の境界へ渡す形がこれにあたる。上の構文形による降下を先に試し、それが効かない位置だけこの経路に落ちる — 構文形があるときに型木を見ると take(Some(5)) が誤検出になるため、順序は逆にできない。

この経路には内側の式が無いので、材料は型が運ぶ述語だけである。素通し条件は外側の境界と同じものが位置ごとに効く。

Future の payload は辿らない。 実行時の Future 照合は payload-blind（await 前は payload が無い）なので、Future(Int) を Future(Pos) の境界へ渡しても述語は評価されない。ここで証明義務を課すと、実行時に決して破れないコードに「証明できない」が鳴る（payload の型そのものの不一致は §2.12「Future payload の照合」が見る）。

関数型では変位に従う — 結果位置は共変なので宣言型の述語を目標に、パラメーター位置は反変なので向きを反転して（実際の側の述語を目標に）判定する。{ Pos | Int } の境界へ { Int | Int } を渡すのは「より広く受ける関数」なので報告しない。

• 現段階で見ていない境界（見逃し。将来枠）: 宣言結果型を関数宣言の側から見ること（内部名注釈と本体末尾アスクリプションが宣言する結果型。上の降下は境界へ渡された関数値を見るものなので、リテラル自身が結果型を宣言する 2 形は届かない）、呼ばれるオブジェクトのスロット既定値、原始型メソッドの引数（§2.7 の引数型表を通る経路）、および union の選択肢に埋もれた refinement（f: OneOf(Pos, String) := 0。どの選択肢に照合されるかが静的に決まらない）。型木の並行走査は同じ形の対だけを辿るので、片側が OneOf や型変数で構造が食い違う位置も素通しする。材料の側では、区間に落ちない算術（除算・剰余・非線形項・Float の算術）と、項同士の関係（take(x - y) で x > y が分かっている形）を見ない。いずれも見逃し側で、実行時照合が backstop になる。

述語の断片適合

refinement（opaque でない方）の述語が決定可能断片（language-spec.md §17.7）の外の式を含むとき refinement predicate of '<name>' is outside the decidable fragment を報告する（<name> は type Name := refinement { … } で名付けた型名。無名の refinement リテラルは正準表示を載せる）。判定は型値を構築する地点（type の右辺など）で行い、1 つの refinement リテラルにつき高々 1 件を報告する。

• 断片は whitelist: 断片内と判定するのは §17.7 が列挙した形だけで、そこに無い式はすべて断片外＝本規則のトリガーである。断片外の代表例はユーザー関数の呼び出し・断片に無い組込メソッド（s.split("@") など）・要素アクセス（xs.0 / t.1）・非線形項（変数同士の積・変数を除数に置く除算）・0 除算・変数を含む Float 算術だが、この 6 つは列挙ではない。
• 判定は構文と基底型の構造で行う: 式の形だけで決まる部分は型解決を通さずに厳密に判定でき、構造に依る部分は解決できなければ断片外へ倒す（安全側。断片内と誤って受けると偽の証明を作りうる）。診断の位置は refinement キーワード — 書き手が直す対象はそこから始まる型式そのものだからである。
• 基底型に依る 4 点: 断片の定義のうち次の 4 点は基底型に依る（§17.7）。
• 裸の述語変数が述語本体になれるのは基底型が Bool のときだけ。 refinement { n: Int | n } はこの条件を外すので断片外であり、本規則は真の欠陥を名指しして報告する（a bare slot variable is a predicate only when the base type is Bool）。
• contains / starts_with / ends_with が断片内になるのは基底型が String のときだけ。 同名のメソッドが List / Bytes / Range にもあり意味が違うためである。
• 組込 measure（length! / is_empty!）が断片内なのは、基底型が長さを持つ（String / List / Bytes）ときだけ。 measure は「0 以上」の公理を持つので、Int 基底の v.length! >= 0 を受理すると恒真として証明でき、実行時には length が無くて panic する地点の照合が消去（language-spec.md §17）で落ちる。
• フィールドパスの領域は、基底型がその位置に宣言した型で決まる。
• 解決してはじめて分かる形: 別名（type I := Int の I）や修飾名で書いた基底型は構文の走査では断定できないので、上の 4 点と場所（フィールドパス）の判定は型解決の後に行い、定義地点で報告する。構文の走査が既に断片外と判定した述語はここで重ねない。 断片外へ倒れた述語は本節「境界の証明義務」の証明対象から外れて境界では素通しになるので、定義地点で鳴らさないとどこでも何も鳴らないまま実行時照合だけが残る。
• 解消の道: 述語を断片内に収めるか、refinement_opaque に書き換えて「実行時検査に委ねる」と明示する。後者は本節「境界の証明義務」の証明対象からも外れる。
• 報告は定義地点のファイルで行う: 本規則は検査対象のファイルに書かれた refinement リテラルだけを見る。import 先で定義された断片外の refinement は、そのファイル自身を検査したときに報告される。importer 側では「境界の証明義務」が「目標が厳密でない」として素通しするので、どちらのファイルも検査しなければ診断は出ない（見逃し側。実行時照合が backstop）。
• refinement_opaque の述語は本規則の対象外（明示オプトイン）。断片外の述語も実行時には普通に評価され、照合として機能する。

述語の閉じ

refinement / refinement_opaque の述語が自分のスロット以外の名前を参照するとき refinement predicate of '<name>' references the free variable '<var>' を報告する。位置は自由変数そのもので、書き手が消す対象がそこだからである。

• 両方の綴りが対象である。 閉じていることは断片へ入るための条件ではなく refinement 全体の要件（language-spec.md §17.7）で、refinement_opaque は判定を実行時へ送る綴りであって自由変数を許す綴りではない。上の「述語の断片適合」が opaque を対象外にするのとは線引きが違う。
• 自由変数があるときは断片の診断を重ねない。 閉じていないことが根本原因なので、1 つの refinement リテラルにつき本規則だけが報告する。
• 報告しないと内部エラーへ到達できる。 実行系は閉じていない述語を落とせず、そこは「静的検査が通した入力では起きない」不変条件として書かれている。

除数の非ゼロ義務

/ と % の除数の位置について、値が 0 でないことを実行前に証明できなければ cannot prove divisor is non-zero を報告する（divisor-not-proven）。ゼロ除算は実行時エラー（language-spec.md §7.1・§16.2 のバグ層）なので、本規則はその実行時契約を実行前に見せる位置づけであり、上の「境界の証明義務」と同じ契約系である。

判定は上の「境界の証明義務」をそのまま使う。 目標の述語を除数の静的型に応じて処理系が組み、材料・判定手続き・素通し条件のすべてを共有する — 新しい判定手続きは持たない。目標は次の 2 つである。

• 除数が Int のとき: v != 0
• 除数が Float のとき: v != 0.0 && v != -0.0。-0.0 での除算も実行時エラーであり、Float の -0.0 と 0.0 は §9.4 の全順序では別の値なので、片方だけでは足りない

解消の道も同じである。 上流で除数の宣言型を絞る（d: NonZero := …）か、式アスクリプションで実行時へ委ねる（a / (d: NonZero)）。NonZero / NonZeroFloat は prelude が持つ（prelude.md）。条件で検査する形（if (d != 0) { a / d }）は §2.3 の比較述語の葉が事実を立てるので、注釈を書かずに証明が通る。

• 対象は除数だけである。 被除数には義務を課さない（値に関わらずゼロ除算は起きない）。
• ** の負指数は対象外。同じ実行時エラーの族だが、被検査項が指数で述語も v >= 0 と違う（language-spec.md §7.1 のローカル節）。
• 素通し条件は上と共通。除数の静的型が Unknown・Never に倒れる位置、基底型の照合が既に落ちている位置、および安全網（除数の式に現れる名前がその位置を支配する条件で検査されているとき）で報告しない。

添字の範囲義務

要素アクセス（recv.[i] / recv.N。language-spec.md §3.2・§3.10）について、添字が受け手の範囲に収まることを実行前に証明できなければ cannot prove index is in range を報告する（index-not-proven）。範囲外は実行時エラー（同 §3.10・§16.2 のバグ層）なので、上の 2 つと同じ契約系である。

判定は「境界の証明義務」をそのまま使う。 目標は i >= 0 && i < recv.length! で、材料・判定手続き・素通し条件を共有する。目標が 2 つの名前にまたがる点だけが上の 2 つと違い、そこは §2.3 の関係の事実が材料を供給する。

• 対象の受け手: 静的型が長さを持つと確定し（List / String / Bytes）、かつ受け手が裸の識別子であるもの。場所（o.xs）を外すのは §2.3「対象の主語」と同じ理由で、可変スロットなら中身が変わりうるからである。Range は要素数が静的に決まらないので対象外である。
• 受け手の長さについての事実が材料に無い位置は素通しする。 上限（i < recv.length!）を導くには recv.length! そのものについての事実が要る。ところが述語は自由変数を持てない（language-spec.md §17.7）ので、「引数 b の長さは at + 4 以上」という契約は型として書けない。書き手に直す道が無い位置で鳴らさないのは素通し条件そのものなので、ここは義務を課さず実行時エラーに委ねる。
• 長さの事実が立つのはリテラルの受け手である（[10, 20, 30] を := で束ねた名前は length! == 3）。定数添字はその場で決着し、位置アクセス recv.N もこの経路で見る。
• 解消の道は 2 つ。条件で検査する（if (i < xs.length!) { xs.[i] }。§2.3 の関係の事実が立つ）・範囲を生む形から引く（下記）。
• range の要素は上下限を運ぶ。range(a, b) を要素を 1 つずつ配る組込メソッド（map / each / filter / any / all / find / count / flat_map）へ渡した位置では、ブロックの第 1 スロットに a <= v && v < b の関係の事実を立てる。定石の range(0, xs.length!).map { i | xs.[i] } がこれで通る。運ぶのは組込の反復メソッドへ直に渡した形だけで、range を名前に束ねてから渡した形・ユーザー関数へ渡した形は対象外である（受け手の実装が要素をどう配るか分からない）。第 1 スロットが要素でない fold も外れる。
• 素通し条件は上と共通。受け手の静的型が Unknown・Never に倒れる位置、基底型の照合が既に落ちている位置、および安全網（添字の式に現れる名前がその位置を支配する条件で検査されているとき）で報告しない。

2.12 Future

Future のブロックは別フローで遅延起動され、payload は await 前に照合されない。この 2 つの性質から 2 つの診断が立つ。

Future ブロック内の脱出

レシーバー型が Future に確定する .map / .and_then のブロック本体に、外側関数から確実に脱出する return または ? bail があれば return is not allowed in a Future block: the block runs after the outer function has returned を報告する（? は bail (?) is not allowed in …）。

Future のブロックは別フローで遅延起動され、評価される時点で外側の関数は既に戻っているため脱出が成立しない。実行時は制御値を素通しせず panic にする（language-spec.md §18.2 / prelude.md §9.6）ので、到達すれば確実に panic する不一致として §2 の対象になる。

脱出点の収集は §2.6「宣言結果型と全脱出経路の整合」（宣言結果型を全脱出経路で照合）が使う収集器と同一で、制御透過な経路だけを辿る — if / when / while のブロック、match のアーム body、conduit{…} / loop{…} 関数のブロック引数、レシーバー型が確定する反復メソッドのブロック。

報告しない:

• レシーバー型が Future に確定しないとき（Any / Unknown 経由）
• 不透過なユーザー高階関数へ渡したブロック内の return — その return はブロック自身の関数境界で取り出されるため Future ブロックからは脱出せず、panic に至らない
• 値として格納される関数リテラル内の return — 構築時には評価されない
• break / continue — 字句的に囲うループとの関係が別軸（language-spec.md §18.1）のため静的には扱わない。実行時 panic が backstop

§2.6「宣言結果型と全脱出経路の整合」が Future ブロックを脱出経路に数えないこととは両立する — 「脱出が成立しない」という同じ事実から、§2.6「宣言結果型と全脱出経路の整合」は「宣言結果型に寄与しない」を、本規則は「書いてはならない」を導く。

Future payload の照合

typed 位置（束縛・パラメーター・分解・本体結果型）に流れる値の静的型が Future(U)、宣言型が Future(T) で、consistent(T, U)（Any・型変数・Unknown は wildcard）が確実に false なら報告する。入れ子（List(Future(String)) 等）も辿る。

• 契約系である根拠: 実行時照合（language-spec.md §17.4）は Future を payload-blind で照合する（await 前は payload が存在しないため Future か否かのみ）。ゆえに x: Future(String) := fork({42}) は束縛地点で panic せず、「到達すれば確実に panic」としては報告できない（誤検出になる）。Option/Result は実行時に payload を照合するので同じ照合が「確実に panic」の枠に収まる（§17.4）が、Future は収まらない。本規則は §2.6「関数型注釈と実体シグネチャの整合」と同様、「束縛地点で即 panic しないが後続の await 使用で確実に panic する非整合」を実行前に塞ぐ契約系の診断としてこれを行う。
• 誤検出ゼロ: consistent が確実に非整合の対のみ報告。payload 型が静的に不明な Future（無型ソース由来）は素通し。

2.13 値位置の未定義参照

構文層（§1）は値位置の未定義参照を検出しない。本節は値位置の識別子参照でどのスコープ（prelude・トップレベル・ローカル・destructure 束縛・import member・inner-name・型変数）にも束縛が無いものを undefined: <name> として報告する（到達すれば確実に language-spec.md §16.2 の undefined panic）。破棄子 _・型コンテキストの bare 小文字（型変数、language-spec.md §17.2）は対象外。スコープ模型で束縛の有無を確実に判定できないケース（動的 import 越境など）は素通しし、実行時 panic に委ねる。

前方参照は位置で分かれる。 同じ文列の後方で宣言される名前を即時評価の位置で参照する形（println(later) の後に later := 1）は、その宣言文がまだ走っていないことが確実なので報告する。リテラル本体からの参照（f := {| later } の後に later := 1）は本体が宣言の時点では走らないので対象外で、相互再帰もこちらに入る。外側に同じ綴りの束縛があるときも対象外である — スロットの既定値や x := x の右辺は外側の束縛を指す。書き込みの対象（x = v の x）は値位置の出現ではないので、これも対象外である。

match の bare 識別子パターンも値位置である。 パターンの裸の識別子は束縛ではなく素の値パターン（prelude.md §8.4）なので、同じ規律で見る — enum に無いタグを書いた形（match c { Purple => … }）や、名前 destructure をせずに書いた bare タグはここで報告する。payload 位置の bare 識別子は対象外である（あちらは束縛で、解決できない構築子パターンのアームでは payload の名前を未定義と断じない）。

2.14 多重度型の消費追跡

多重度型（language-spec.md §17.8）についての診断。同節が型語彙・部分型関係・複製と捕獲・実行時の扱いを定めるのに対し、本節はどう検査するかを定める — 何を追跡し、どの操作が値を消費し、消費済みの値への出現・消費状態の割れ・未消費をどう報告するかである。

多重度は実行時に何も照合しない（§17.8）ため、本節の診断はいずれも「到達すれば確実に panic」には乗らず、宣言した型が課す契約の破れを実行前に塞ぐ契約系（§2.1）である。本節が報告する 14 種は §5 に出どころ §2.14 として並び、同節の規則に従いすべて Error である。never-consumed も Warning ではない — ExactlyOnce は書き手が宣言した契約なので、Warning にすると「宣言したのに守らなくてよい型」ができてしまう。

本節が繰り返し使う前提を先に置く。個別の規則ではこれを前提に簡潔に書く。

• 消費追跡は名前のフロー状態である。 対象は裸の識別子で、名前ごとの状態は生存 / 消費済みの 2 値である。
• 借用は消費状態を持たない（Borrowed(T) は多重度型ではない。§17.8）。借用についての診断（下記「借用は保存できない」「借用したレシーバーでの Consuming 呼び出しを禁じる」）は式の形と静的型だけで決まり、フロー解析を要さない。その分対象も裸の識別子に限らず式へ広がる。
• 移譲と複製は別である。 別フローで走り起動が高々 1 回のブロックへの捕獲は所有権の移譲で、親側が消費済みになるので値へ届く経路が増えない。copy は複製で、親側に元の値が残るので経路が 2 本になる。この違いが「捕獲は許すが copy は禁じる」の根拠である（§17.8「複製と別フローへの捕獲」）。
• 決められない位置は見逃し側へ倒す。 消費とも借用とも判定できない位置で消費と決めれば借用だった使用が use-after-consume に、借用と決めれば移った義務が never-consumed になり、倒すべき向きが診断ごとに逆になる。誤検出ゼロを優先し、各規則の「素通し条件」がその一覧である。包みの内側と値の構造をたどる走査の深さの上限も同じで、予算を使い切った位置は追跡対象にせず、禁じる判定では禁じる側へ倒す。

追跡の対象と消費する操作

追跡するのは、静的型が AtMostOnce(T) / ExactlyOnce(T) に解ける裸の識別子だけである。束縛（:=・mutable := による mutable ローカルの宣言・パラメーター束縛・分解束縛・match のアームパターン束縛）が作る名前が対象である。名前を作るのは宣言だけなので（language-spec.md §6.1）、= による再代入は追跡対象へ載せ直さず、消費のマークだけを落とす。

アームは排他なので、アームが束縛した名前の追跡はそのアームの中だけで有効である。兄弟のアームにも match の後ろにも持ち出さない（下記「分岐は消費状態の収束を要求する」）。

消費する操作は次のとおりである。

これ以外の出現はすべて借用である。消費後の出現は、借用であってもエラーになる（use-after-consume）。報告には消費が起きた地点を位置で添える。

f := fs.open("a.txt")!.unwrap_or_else { e | panic(e.message) }
a := f.read_at(0, 4096)!     # 借用
b := f.read_at(4096, 4096)!  # 借用（何度でもよい）
f.close()!                   # 消費
f.sync()!                    # エラー: use-after-consume

ExactlyOnce の値を関数へ渡した場合、消費義務は呼び先へ移る — 呼び先ではパラメーターの宣言型が ExactlyOnce(T) なので同じ規則がその本体にかかり、呼び出し側には義務が残らない。

引数位置が消費になるのは、受け側のパラメーターの型が具体型に解けたときだけである。 呼び先の関数型そのものが引けない位置（不透過なユーザー定義高階関数・部分適用・arity 不一致）と、パラメーターの型が Unknown・明示的に書いた Any・型変数・Never に倒れる位置は「不明」とし、消費状態は動かさず、その名前を消費義務の判定から外す。ただし組込型メソッドの実引数は「不明」ではなく禁止である（下記「規律が届かないパラメーターへ多重度型の値を渡せない」）。

捕獲を 1 回の消費とみなせるのは、ブロックが別フローで走り、かつ起動が高々 1 回のときに限る。 spawn / fork（prelude.md §9.1 / §9.9）と Future の map / and_then（同 §9.6）がこれを満たす。std:parallel の map / filter / fold（std/parallel.md）は別フローで走るが fn を要素ごとに起動するので満たさず、下記「ブロックの起動回数」の起動回数が不明な側として扱う。fork も借用にはできない — 協調フローで親子が同時には走らないが、子が消費の後に走る可能性を静的に排除できないためである。

移譲が使えるのは追跡対象の値に限る。 追跡の外にある構造に入った多重度型の値の捕獲は下記「複製と別フローへの捕獲の禁止」が塞ぐ。spawn は静的に移譲と判定した捕獲について複製も非 Copyable 検査も行わない（prelude.md §9.9）。

本節は借用の行き先を追わない。 安全性が「借用したレシーバーでは Consuming メソッドを呼べない」の 1 本で立つ（§17.8）ため、借用が呼び先から漏れて生き延びても、そこから消費は起こせない。

自己参照（inner-name。language-spec.md §4.2）は、そのメソッド本体における受け手の扱いに一致させる — Consuming メソッドの本体では所有、それ以外の本体では借用。放置すると受け手の規律を迂回できるためである。

分岐は消費状態の収束を要求する

分岐の枝で消費状態が割れたとき、使用地点ではなく分岐そのものを報告する（divergent-consumption）。§2.9「分岐の結果型に収束を要求」と同じ立て付けで、書き手は両枝で消費を揃えるか、どちらの枝でも消費しないことで解消できる。

if (c) { f.close()! } { () }   # エラー: divergent-consumption
f.read_at(0, 10)!

割れを報告するのは ExactlyOnce だけである。 AtMostOnce は使い残しを咎めない（language-spec.md §17.8）ので、分岐では報告せず合流点の状態を消費済みへ寄せ、その後で使われたときにだけ use-after-consume を報告する。ExactlyOnce では寄せられない — 消費していない枝が持つ消費義務を、寄せると黙って帳消しにしてしまうためである。

Never に倒れる枝（return / break / continue / panic）は合流に寄与しない。 その枝は合流点に到達しないためで、§3.3 が Never を分岐合流の恒等元として扱うのとまったく同じ規則である。

t := begin_txn()                                 # t の静的型は ExactlyOnce(Txn)
when (invalid(row)) {
  t.rollback()
  return Err(error("bad_row", "invalid row"))    # 発散する枝。合流に寄与しない
}
t.exec("UPDATE …")                               # 借用
t.commit()                                       # 合流後、t は生存している

ブロックの起動回数

Hikari の制御構造は予約語ではなく prelude 束縛の普通の関数（philosophy.md §2.2）なので、反復駆動とユーザー定義高階関数は構文上どちらも「ブロックを渡す呼び出し」である。したがって外側の値を消費できるかは、ループかどうかではなくそのブロック位置が高々 1 回しか起動されないと仕様が定めているかで決める。

「高々 1 回」の側は次の表で全部である。この表に無いブロック位置は prelude・std・ユーザー定義のいずれであっても「不明」へ倒す。一覧がこの向きに閉じているので、ブロックを取る関数・メソッドが将来増えても健全性は保たれる。

これらの位置では外側の値の消費を許す。分岐の枝と match のアーム body は上記の収束規則で合流し、残りは 0 回か 1 回なので合流点で状態が割れない。

表のほかに、宣言で開く行が 1 つある。 呼び先の関数型が引け、ブロックが現れた実引数に対応するパラメーターの宣言型が ExactlyOnce（基底が関数型）に解けるなら、そのブロック位置も「高々 1 回」である（language-spec.md §17.8「ブロックの起動回数を宣言する」）。db.transaction と構造が同じ自前の bracket（with_conn(pool) { c | … }）がこれで書ける。その宣言は呼び先の本体で本節自身が検証する — ブロックを 1 度も呼ばなければ never-consumed、2 度呼べば use-after-consume になる。

AtMostOnce と Borrowed は開かない。 AtMostOnce は 0 回の可能性を残すので、開くと起動されなかった経路でも義務が果たされたことになる。Borrowed は消費義務を持たないので起動回数について何も述べていない。

残りはすべて起動回数が不明（0〜n 回）で、外側の値の消費を禁じる（consume-in-unknown-arity-block）。代表を挙げる。

別フローで走り、かつ起動が高々 1 回のブロック（spawn / fork・Future の map / and_then）だけはこの軸に乗らない — 起動を待たず、捕獲の時点で消費になる（上記「追跡の対象と消費する操作」）。

借用はどのブロック位置でも自由である。 実用上のループはほぼ借用なので、制限が刺さる場面は限られる。パラメーターを取る std の bracket は、そのパラメーターを Borrowed(T) で宣言する — ブロックがハンドルを消費できず bracket 自身の後始末が壊れないようにするためである（std/array.md）。

f := fs.open_rw("log")!.unwrap_or_else { e | panic(e.message) }
xs.each { x | f.write_at(0, x)! }     # 借用。何周でもよい
f.close()!                            # 消費はループの外

xs.each { x | f.close()! }            # エラー: consume-in-unknown-arity-block

xs.each { x |
  g := fs.open(x)!.unwrap_or_else { e | panic(e.message) }
  g.close()!                          # ブロック内で束縛しブロック内で消費 — 通る
}

break / continue による運び出しの禁止

多重度型の値を break / continue の実引数に置くことを escape-of-multiplicity-value として報告する。 break value はループ式全体の戻り値を value にする（prelude.md §8.5）ので、値はループの外へ出て同じ関数の中に残る。return と違い関数の外へ出ないので消費ではなく、かといって追跡はループのスコープで切れるため、外へ出た値が規律の外で生き延びる。

ExactlyOnce の消費義務

義務を果たす期限はその値を束縛したスコープの終わりで、全脱出経路（break / continue / return / ? の bail。§2.6「宣言結果型と全脱出経路の整合」と同じ経路列挙）で消費されていなければ never-consumed を報告する。

xs.each { x |
  t := begin_txn()                    # t の静的型は ExactlyOnce(Txn)
  t.exec("insert …")
}                                     # エラー: never-consumed（どの脱出経路でも t が消費されない）

トップレベル束縛にも同じ期限がかかる。 そのスコープの終わりはファイル評価の終わりなので、そこまでに消費されなければ never-consumed になる。多重度型の値は export できない（下記「モジュール境界とトップレベル束縛」）ので、義務がファイルの外へ出ることはない。

panic 経路には義務を課さない（そこでプログラムが終了するため。language-spec.md §16.2）。Hikari はスコープ離脱フックを持たないので、未消費の値が自動で消費されることはない。

包みは多重度を伝播する

失敗しうるコンストラクターはすべて包みを通る（fs.open は Future(Result(File)) を返す）ため、包みが多重度を継承しないと主要な入口が丸ごと追跡の外に出る。線引きは個別のコンテナー名ではなく構造で決める。

• 伝播する（包み自体を 1 つの追跡対象にでき、中身を出す形をその包みの消費として記録できる）: enum の variant payload・タプル・Future・List。Option / Result は組込 enum（language-spec.md §17.4）なので、この規則はそれらを特例にせずユーザー定義 enum も自動的に含む。Future はタグを持たないが「0 か 1 個を包み取り出しが 1 回きり」の側なので同じ扱いとする。
• 伝播しない（上記 4 つ以外のすべて）: record（スロットが := か = かを問わない）がこれにあたる。名前フィールドのパスを主語にすると別名（p := o の後の p.h と o.h）で漏れ、差し替え（o.h = f2）で誤検出になるためである（§17.8「規律を課さないと決めたもの」）。

中身が多重度型なら包み自体を追跡対象とし、取り出し（unwrap_or_else / ? / ! / 分解束縛 / 要素アクセス p.0）を消費とする。伝播しない側は「入れたら追跡終了」で、そこから先はハンドル側の実行時の封印が捕捉する（close 後はどのメソッドを呼んでも実行時エラーになる。std/fs.md ほか）。封印は型注釈の照合ではないので §2 冒頭の backstop とは別の機構だが、静的に諦めた経路を実行時に捕まえる役どころは同じである。本節で「実行時の封印」と書くのは以下すべてこの機構を指す。

r := fs.open("a.txt")!
a := r.unwrap_or_else { e | panic(e.message) }
b := r.unwrap_or_else { e | panic(e.message) }   # エラー: use-after-consume（r は 1 度目で消費済み）

効果の層はこの線の外である。 線を引いているのは器についてであり、Effect(T, …) は器ではない（language-spec.md §17.9）。効果の層を挟んだ位置に在るのは基底の値そのものなので義務はそのまま届き、Effect(ExactlyOnce(T), …) を結果型に宣言した関数の返り値を束縛した名前は追跡対象になる。層と包みが重なる Effect(Future(Result(File)), Fs, Susp) も同じである。

List が伝播する側なのは、追跡するのが器であって要素ではないからである。 要素は恒久的に対象外のまま（§17.8「規律を課さないと決めたもの」）で、追跡対象に載るのは器を束縛した裸の識別子 1 つである。器を外すと、器から取り出すたびに新しい追跡対象が生まれる一方で器の側からは何も減らないため、1 つの資源に対して独立に果たせる義務が人数分できる。タプルと違って長さが静的でないので、取り出しは器ごと 1 回きりになる — 複数の要素を扱うなら借用で回す（下記「器の中身を所有で受けるブロック」）か、(要素, 残り) を返す形で取り出す（hit, rest := xs.partition { l: Borrowed(Lease) | … } は器を消費して 2 つの器を返す）。

要素アクセスを消費とするのは、下記「素通し条件」の「裸の識別子でない主語」に対する例外である。例外の対象はタプルの要素・variant payload・List の要素に限る。

器の中身を所有で受けるブロック

追跡対象の List を受け手とする組込メソッドが、その要素を器の外へ出す形は器の消費である。 組込型メソッドは呼び先の関数型が引けない（上記「追跡の対象と消費する操作」）ので、呼び出しそのものからは借用か消費かが決まらない。しかし外へ出したかどうかは型から決まるので、判定はそこに置く。次の 2 つのどちらかに当たる呼び出しが器の消費である。

• 結果型が多重度を運ぶ。 xs.first! は Option(Lease) を返すので要素を器の外へ出している。運ばないもの（xs.count! の Int・xs.is_empty! の Bool）は器を覗いただけなので消費ではない。
• 実引数のブロックが、パラメーターを所有の多重度型で宣言している。 xs.each { e: Lease | … } の e は書き手が所有で受けると書いた位置で、そのブロックは要素の消費義務を引き受ける。Borrowed で受けるブロック（xs.each { e: Borrowed(Lease) | … }）は消費状態を持たないので器を消費せず、何度書いてもよい。

列挙ではなく型で決めるのは、std に List のメソッドが増えても穴が開かないようにするためである。

xs := [l]                              # l: Lease（ExactlyOnce）
xs.each { e: Borrowed(Lease) | e.ping() }   # 通る（借用は器を消費しない）
a := xs.0                              # 器の消費。a が追跡対象になる
b := xs.0                              # エラー: use-after-consume（xs は 1 度目で消費済み）

関数値へ閉じ込める経路を塞ぐ

メソッドはスロットに入った普通の関数なので値として取り出せるが、取り出した時点で受け手との関連が切れて追跡が終わる。取り出した関数値はコンテナーにも別フローにも別モジュールにも渡せるので、多重度型のメソッドは呼び出し形（f.close() / f.close!）でのみ使えるとする。Consuming メソッドの取り出しは cannot-extract-consuming、非 Consuming メソッドの取り出しは受け手への借用を保存する形なので cannot-bind-borrowed である。

引数側は事情が違う。auto-curry（language-spec.md §3.6）で作った部分適用は何度でも適用できるので、素朴には「値は 1 回消費されたことになっているのに本体は呼ばれた回数だけ走る」ことになる。これは結果の側に多重度を載せることで解ける — 追跡対象の実引数を埋めた部分適用の結果は多重度型になり（language-spec.md §17.8「関数値の多重度」）、その関数値を呼ぶことが上の表のとおり消費だからである。2 回呼べば use-after-consume、ExactlyOnce を埋めて 1 度も呼ばなければ never-consumed になる。部分適用のための専用の規律は要らない。

• 載せる多重度は「強い方が勝つ」。 埋めた実引数（および包みの内側）に ExactlyOnce が 1 つでもあれば結果は ExactlyOnce、無く AtMostOnce だけなら AtMostOnce である。弱めると「ちょうど 1 回消費する」義務が、結果を呼ばないことで消えてしまう。
• 借用の引数は多重度を載せない。 借用は消費できないので果たすべき義務が無い。
• 部分適用そのものは消費ではない。 本体が走らない（§3.6）ので資源も使われず、回数の規律は結果の側へ移る。呼び先が既に多重度型なら、そこへの部分適用の結果もその多重度を引き継ぐ — これにより多段の部分適用（u3(l) の後の p(1)）でも義務が落ちない。
• 明示的 kick（use(f)! / use(f)()）は部分適用ではないので報告しない。 未束縛スロットへ既定値が入るのは明示的 kick に固有の意味論なので（§3.6）、残りのスロットが既定値を持つならその呼び出しで本体がちょうど 1 回走り、多重度型の値もちょうど 1 回消費される。残りのスロットに既定値が無い形は到達すれば実行時の arity panic であり、そちらは arity 不一致の管轄に留まる。

規律が届かないパラメーターへ多重度型の値を渡せない

実引数に、静的型が多重度型に解ける裸の識別子を置いたとき、渡した先にその多重度が届かないなら pass-of-multiplicity-value として報告する。 届かない位置は 3 つあり、どれも渡した先に規律を課す先が無いという 1 つの理由の現れである。

• 受け手が std の不透明ハンドルに解けるメソッド呼び出しの実引数。 組込型メソッドは呼び先の関数型が引けないので（上記「追跡の対象と消費する操作」）、渡した値が消費されたのか借用されたのかを判定する材料が無い。素通しにすると呼び手側でもその名前が生きたままになり、渡した先（コレクションの中）と呼び手の両方から同じ資源へ届く経路ができる。language-spec.md §17.8 が「コレクション要素は恒久的に対象外」と定めている以上、入った先で拾い直す道は無い。
• 呼び先の関数型は引けるが、対応するパラメーターの宣言型が多重度型に解けない位置。 型の照合は多重度の層を剥がして基底同士で行う（§17.8）ので、この形は型としては通る。渡すこと自体は消費として記録されるため呼び手の側の名前は使えなくなるが、受け側の名前が追跡対象にならない — その中では同じ資源を何度でも使える。
• 呼び先の関数型は引けるが、対応するパラメーターの宣言型が型変数に解ける位置。 型変数にはスロットも多重度も無いので規律を課す先が無く（§17.8「基底に型変数を置く」）、消費とも借用とも決められないので呼び手の側の名前まで生きたまま残る。境界の有無は問わない — 境界は確定できる型を絞るだけで、多重度の規律を課す先を作らないからである。

2 つ目は狙って書かなくても起きる。基底型そのもので受ける形だけでなく、構造的に狭い record 注釈でも幅部分型で落ちる。基底が record のユーザー定義多重度型には実行時の封印が無い（§17.8「規律が届かない位置」）ため、素通しにすると実行時にも捕まらない。

type Lease := ExactlyOnce({ ping: {| Int }, done: Consuming({| Unit }) |})

peek := { x: { ping: {| Int } |} | (x.ping(), x.ping()) }

l: Lease := new_lease()
n := peek(l)                  # エラー: pass-of-multiplicity-value

逃げ道はパラメーターの宣言型である。 多重度型で受ければ規律はそのまま続き（{ x: Lease | … }）、基底に型変数を置く形（{ x: AtMostOnce(a) | … }。§17.8「基底に型変数を置く」）でも続く。触るだけなら借用で受ける（{ x: Borrowed(Lease) | … }）。Hikari 側のコンテナーへ入れる形は本規則の対象ではなく、入れることが消費として記録される。

dup := { x: a | (x, x) }
h := m.insertion.scratch()

h.set("a", lease)             # エラー: pass-of-multiplicity-value（組込型メソッド）
p, q := dup(lease)            # エラー: pass-of-multiplicity-value（型変数）
box := { mutable held := lease |}   # 通る（コンテナーリテラルへ入れる形は消費として記録される）

対象外の形が 4 つある。

• タグ構築子の実引数。 Ok(x) / Err(x) やユーザー定義 enum の variant 構築子は payload 型が型変数だが、包みが多重度を伝播する（上記「包みは多重度を伝播する」）ので規律が消えない。3 つ目が対象にするのは、包みを作らない普通の関数の型変数パラメーターだけである。
• 緩い向き。 多重度を持たない値を多重度型のパラメーターへ渡す形と、ExactlyOnce の値を AtMostOnce のパラメーターへ渡す形（§17.8「多重度型の部分型関係」）は、受け側の規律が同じか強まるだけである。禁じるのは規律が消える向きだけである。
• 素通し条件 — パラメーターの宣言型が Unknown / Any / Never に解ける位置。明示的に書いた Any は gradual 境界なので書き手の選択として通す。型変数はここに入らない — 決められないことは同じだが、Any と違って基底に型変数を置けば規律を通せるためである。
• 多重度型を含む構造を渡す形。 対象は静的型が多重度型そのものに解ける裸の識別子だけで、record に入れてから渡す形は追跡がすでに切れている。そちらは下記「複製と別フローへの捕獲の禁止」が別フローへの捕獲について塞ぐ。List に入れてから渡す形は器が追跡対象なので、渡すことはその器の消費として記録される。

基底が境界の無い型変数の値のメンバーは参照できない

静的型が多重度型に解け、その基底が境界の無い型変数である値へのメンバー参照を cannot-call-on-type-variable-base として報告する。 呼び出し形（x.done()）も取り出し（r := x.done）も対象である。型変数にスロットが無いので、そのメンバーが Consuming かどうかを引く先が無く、消費とも借用とも決められない。

close_it := { x: ExactlyOnce(a) | x.commit() }   # エラー: cannot-call-on-type-variable-base

素通しにできない。 境界を持たない型変数にはメンバーを数え上げる先が無いので、この位置のメンバー参照は型検査を一つも受けていない — 存在しないメンバー（x.nonexistent()）でも no-such-member が出ない（§2.7）。素通しにすると、ExactlyOnce の義務がその名前から静かに消える。

逃げ道は 2 つある。 基底を具体型で書く（{ x: Lease | x.done() }）か、基底の型変数へ interface 境界を付ける。境界がメンバーを数え上げられるときは報告しない — 境界が（多重度の層を剥がしたのち）record または既知の不透明型に解けるなら Consuming を引く先ができる（§17.8「基底の型変数へ境界を付ける」）。そのときメンバーの解決は境界を基底とみなして行い、境界の宣言に無い名前は具体 record 基底のときと同じく no-such-member になる（§2.7）。閉じた union や原始型のようにメンバーを列挙できない境界では報告する側のままで、条件は「境界が付いていること」ではなく「境界がメンバーを数え上げられること」である。

Borrowed(a) は対象外である。 Borrowed は多重度型ではなく消費義務を持たないので、メンバーが解けなくても消える義務が無い。

借用は保存できない

language-spec.md §17.8「借用は保存できない」の表の各行を cannot-bind-borrowed として報告する。

• 対象は静的型が Borrowed(T) に解ける式である。裸の識別子に限らず、借用を返すメソッドの呼び出し（a.set(0, 1)）もアスクリプションもその位置に現れればかかる。基底 T が多重度型かどうかは問わない。
• 例外は 1 つ — 連鎖のルートが名前を持たない所有の式のとき（arr.array(2, 0).set(0, 1) の arr.array(2, 0)）は報告しない。 借用の式から受け手の連鎖を遡り、借用でなくなった地点の式をルートとする。ルートが識別子なら報告する（その名前が資源を持ったまま 2 本目の経路になる）。ルートまで遡っても借用のままなら所有者は式の外に居るので報告する。ルートがそれ以外（その場で作られ名前に束縛されていない所有の式）のときだけ、その資源へ届く経路が連鎖そのものしか無いので見逃し側へ倒す（§17.8「例外 — 連鎖のルートが名前を持たない所有の式のとき」）。
• 「関数の結果」の行は、宣言結果型があり、それが Borrowed(…) でないときだけ報告する。 宣言が無い結果型では報告しない — 結果型を宣言せず Borrowed(T) を返す連鎖メソッドの正当な形を巻き込まないためである。
• 「別フローへの捕獲」の行は名前だけを見る。 捕獲されるのはブロックが参照する外側の名前なので、この位置には式の形が無い。

呼び先が宣言するブロックパラメーターの型は、注釈の無いブロックパラメーターへ流す。 これにより std:array の arr.build や std:map の m.insertion.build のようにブロックパラメーターを借用として宣言するメソッドでは、書き手が { h | … } と注釈無しで書いても借用の規律が働く。詳しくは §2.2「注釈の無いブロックパラメーターへ型を流す」。

借用したレシーバーでの Consuming 呼び出しを禁じる

language-spec.md §17.8「安全性は 1 本の規則で立つ」— 借用したレシーバーでは Consuming メソッドを呼べない — を cannot-consume-borrowed として報告する。借用が漏れて生き延びても閉じられないことが、借用を region なしで安全にしている土台である。

• 対象は静的型が Borrowed(T) に解ける式をレシーバーに、Consuming で宣言されたスロットをメソッドとして呼ぶ形（h.close() / h.close! の dot 形と h close() / h close の中置形の両方）。裸の識別子に限らず、a.set(0, 1).frozen() のように借用を返すメソッドの結果をそのままレシーバーにした形も含む。
• 報告しない条件（いずれも見逃し側へ倒す）。
• 受け手の基底が record にも std の不透明ハンドル型にも解けない（多重度が両者以外を包む形。Borrowed(AtMostOnce(Int)) 等）。std の不透明ハンドル（arr.Array / fs.File ほか）は record ではないがメソッドの一覧を持つので、そこから Consuming かどうかを引く（§17.8「可変ホスト資源はすべて多重度を持つ」）。
• 受け手の連鎖のルートが名前を持たない所有の式である（arr.array(2, 0).set(0, 1).frozen()）。借用が漏れて生き延びる先が無いためで、上記「借用は保存できない」の例外と同じ判定である。
• その名前のスロットが宣言されていない（universal method・打鍵エラー）。
• スロットの型が Consuming(F) と確定しない（型を持たないメソッドフィールド { ping |} の bare 形）。
• 受け手が借用でない（所有 AtMostOnce / ExactlyOnce のレシーバーでの Consuming 呼び出しは正当な消費である）。

show := { h: Borrowed(Handle) | h.close() }   # エラー: cannot-consume-borrowed

複製と別フローへの捕獲の禁止

§17.8「複製と別フローへの捕獲」が静的な型エラーと定める次の 2 つを、affine-not-copyable として報告する。2 つは対象の範囲が違う（移譲と複製の違い。本節冒頭の前提）。

• copy — 多重度型の値と、それをスロット・要素に持つあらゆる構造（上記「包みは多重度を伝播する」で伝播する包みも含む）。
• 別フローで走るブロックへの捕獲 — 多重度型の値を伝播しない構造（伝播する 4 つ以外のすべて。record）に入れた形だけ。捕獲を許せるのは捕獲が消費として記録される値だけで、伝播しない構造へ入れた時点で追跡が切れ、そこから先の捕獲では親側が値を使い続けられる。

捕獲側は「別フローで走るブロック」という性質で決める — 起動回数は問わない。禁じる向きなので、起動が高々 1 回の spawn / fork / Future のメソッドも、要素ごとに起動する std:parallel の map / filter / fold（std/parallel.md）も等しく対象になる。移譲を許す側の性質はこれより狭く「別フローで走り、かつ起動が高々 1 回」であることに注意する（上記「追跡の対象と消費する操作」）。

実行時の失敗はどちらの禁止も肩代わりしない。 実行時の matches Copyable も copy のディスパッチも spawn の非 Copyable 捕獲 panic も基底型の判定でしかないので（§17.8・prelude.md §9.9）、基底型が record である多重度型（type Txn := ExactlyOnce({ … |}) の形）を含む構造はそのまま複製・捕獲されて通ってしまう。ユーザー定義型には std ハンドルのような実行時の封印も無い。本規則だけが塞ぐ。

r := fs.open("a.txt")!        # Result(File)。伝播する包みなので追跡対象
spawn {| consume(r) }        # 通る（移譲。r はここで消費済みになる）

o := { mutable h := f |}      # record は伝播しない。ここで f の追跡は終わる
spawn {| o.use() }           # エラー: affine-not-copyable
p := o.copy!                  # エラー: affine-not-copyable（複製はどの構造でも不可）

状態の引き渡し口へ置く値

std が状態をブロックへ引き渡す口として定める位置（std/http/server.md §13 の serve の設定レコードの state）に、多重度型の値を含むが自身は追跡対象でない値（多重度型そのものでも、多重度を伝播する包みでもない値）を置いたら state-not-owned を報告する。

理由は所有が 2 つになることである。そこへ置いた値が多重度型でなければ、置くこと自体が消費として記録されない（上記「包みは多重度を伝播する」）。すると呼び手の手元に同じ構造が残り、そこから抜き出した資源と引き渡した先の資源が同じ実体を指す。引き渡した先は後から走るので、上記「複製と別フローへの捕獲の禁止」が捕獲について述べたのと同じ危険がここに開く。置いた値が多重度型なら、置くことが消費になって呼び手の側の名前が使えなくなる。多重度型を 1 つも含まない値は対象外である。

serve({ port := 8080, state := { mutable held := [lease] |} |}, handler)!  # エラー: state-not-owned
serve({ port := 8080, state := 0 |}, handler)!                    # 通る（多重度型を含まない）

モジュール境界とトップレベル束縛

export した名前の静的型が多重度型に解けるなら export-of-multiplicity-value を報告する。型と関数（結果型が多重度型のものを含む）の export は従来どおり許す — 型値の静的型は Type(T)（language-spec.md §17.4.1）なので該当しない。

理由は 2 つある。importer 側は追跡できない（m.conn は path アクセスなので下記の素通し条件に当たり、しかも複数のファイルが import すれば同じ値へ複数の経路から届く）。ExactlyOnce は義務の持ち主が決まらない — export した値はファイル評価の終わりを越えて importer へ渡るので、定義側でその終わりを期限にすると誤検出になる。

export が無いファイルは全トップレベル束縛を公開する（language-spec.md §13.2）ので、多重度型の値をトップレベルに束縛すればこの診断が立つ。単体で走らせるプログラムがそうしたいときは export {} と名乗る — 公開面が空になるので本項の対象が無くなり、消費の期限は上記「ExactlyOnce の消費義務」のとおりファイル評価の終わりのまま残る。

ファイル内のトップレベル束縛は追跡する。 ユーザー定義関数の本体は「起動回数が不明なブロック」（上記）なので、その中で外側の値を消費するのは consume-in-unknown-arity-block になる。したがってトップレベル束縛を消費できるのはトップレベルの文列だけで、そこは 1 回だけ順に評価されるため追跡できる。

conn := sqlite.open(url)!.unwrap_or_else { e | panic(e.message) }   # トップレベル束縛
shutdown := {| conn.close()! }                                     # エラー: consume-in-unknown-arity-block

Consuming の宣言位置

Consuming(F) を書ける位置の制限（language-spec.md §17.8）に反する宣言を consuming-on-non-multiplicity として報告する。他の診断と違い使用地点のフロー解析ではなく型宣言の検査なので、追跡が 1 つも走らないファイルでも効く。

判定は書かれた位置の構文だけで決まる。 許すのは 2 つで、どちらも多重度型構築子（AtMostOnce / ExactlyOnce）の直接の基底に書いたものである — record のスロットと、そこへ型変数を書いたときその場で添えた境界 record のスロット（§17.8「基底の型変数へ境界を付ける」）である。それ以外の位置に現れた Consuming(F) はすべて報告する。境界を名前で書いた形が 2 つ目に当たらないのは、そう書かれた名前が Consuming を持つことがそもそもありえないからである — その名前を宣言する側が 1 つ目に当たらず報告される。

素通し条件（誤検出ゼロ）

次のいずれかに当たる位置では追跡しない。

• 静的型が Unknown / Any に倒れる束縛と、gradual 境界（明示的に書いた Any）を経由した値。
• 裸の識別子でない主語（o.field.close() のような path、コレクションの要素そのもの）。タプルの要素・variant payload・List の要素は例外で、上記「包みは多重度を伝播する」のとおり取り出しを器の消費として追跡する（主語になるのは器であって要素ではない）。path とコレクション要素を対象にしないのは、同じ型のスロットへの差し替えが通る（§2.10）以上「消費済み」と記憶したパスの使用が差し替え後に誤検出になり、コンテナーは自由に別名が作れるので追っても漏れるためである。
• record のスロットを経由して同じ資源へ 2 度届く形（r := { held := l |} の後の r.held を 2 度）。record は伝播しない側なので器が主語にならず、取り出すたびに独立した追跡対象が生まれる。List はこの形も塞ぐが、record は塞がない。
• 静的型が型変数に解ける位置（§17.8「基底に型変数を置く」）。多重度型の値をそこへ渡す形は上記「規律が届かないパラメーターへ多重度型の値を渡せない」が禁じるので、素通しが残るのは gradual 境界を経由して届いた値だけである。
• Never（発散位置。§3.3）。値が流れ込まないため追跡する対象が無い。

素通しした逸脱は、std:fs などのハンドルが持つ既存の実行時の封印が捕捉する（§17.8）。

本節の判定は純粋なフロー解析であり、外部 SMT solver の有無に影響されない — §2.11「境界の証明義務」の報告が構成によって増減するのとは違い、同じソースなら構成に依らず同じ診断が出る。

REPL では追跡が効かない

REPL は検査を 1 行単位で行うため、行をまたぐ越境照合は対象外である（repl.md）。消費追跡は本質的に行をまたぐ（f := fs.open(…) と f.close()! と f.sync()! は別の行になる）ので、REPL では消費の追跡も never-consumed も効かない。実行時の封印が捕捉する。

2.15 効果の推論と検査

関数が起こす効果（language-spec.md §17.9）を推論し、宣言と食い違う位置を報告する。効果は注釈が無くても本体から決まるため、本節は §2.5 の Any 規律や §2.6 の宣言型と違って「注釈を書いた箇所だけ」を対象にしない — 書き手が効果を一切書いていないコードでも、純粋を宣言した位置へ効果を持つ関数を渡せば報告する。

効果の決め方

• 葉は組込だけである。 効果を生むのは prelude / std の組込呼び出しに限られ、どの組込がどのラベルを持つかは prelude.md と std 各書のメンバー表を単一情報源とする。ユーザーコードは葉を持たない。
• 関数の効果は本体で起こる効果の和集合である。 分岐・ループ・match のアームはすべて和に寄与し、到達可能性は問わない（実行されうる位置に書かれていれば計上する）。
• 効果は呼び出し地点に帰属する。 fork(block) / spawn(block) はその地点で block の効果を計上するので、f! が同じ効果を二重に計上することはない。! そのものは中断点なので Susp を足す。
• EffectConduit を宣言したパラメーターの効果を加える。 その位置に渡された値の効果が、呼び出し地点の効果に入る。宣言が無いパラメーターの効果は加えない（渡されたブロックは呼ばれないかもしれないため、加えると誤検出になる）。
• 呼び先を定義へ辿れない位置は宣言された型から採る。 効果は本体から決まるが、呼び出しの戻り値へ束縛した関数値や、パラメーターで受け取った record のスロットに置かれた関数のように、本体へ辿り着けない位置がある。そこでは書き手が型に書いた効果が唯一の出どころなので、宣言型が関数型ならその結果型の効果集合を採る。採るのは Mut を除く 7 ラベルである（下記「素通し条件」）。EffectConduit(F) は自分では効果を宣言しない（language-spec.md §17.9）ので、この経路でも効果を持たない。
• 再帰は最小不動点で解く。 §2.2 が結果型の再帰を扱うのと同じ枠に乗せ、初期値を空集合として増加方向へ収束させる。効果集合は有限（8 種）なので必ず停止する。

import 先モジュールの効果は §2.2「import 先モジュールの型」の経路で決まる — 相対 import と pkg: は import 先ファイルを本規則で推論し、std: は処理系が保持する構造化型シグネチャから採る。循環 import・解決不能な import は §2.2 のとおり Any に倒れ、効果も不明として素通しする。

宣言との照合

契約系の規則である（§2.1）。破れが現れるのは宣言した位置ではなく、その関数を純粋だと信じた呼び出し側だからである。

• 定義側: 結果型を宣言した関数の宣言効果集合が本体の効果を包含しないとき undeclared-effect を報告する。判定は 3 形（束縛注釈・内部名注釈・body 末尾アスクリプション、language-spec.md §17.3）すべてにかかる。
• 使用側: 引数位置・束縛位置で、渡す値の効果が宣言型の許す効果集合に収まらないとき effect-mismatch を報告する。効果集合の部分型は上向きにだけ緩む（language-spec.md §17.9）ので、判定は「収まるか」という方向のあるものであり、§2.4 の注釈照合・§2.10 の型安定性と同じ向きを使う。

apply_twice: { { Int | Int }, Int | Int } := { f, x | f(f(x)) }

apply_twice({ n | n + 1 }, 3)               # 通る
apply_twice({ n | println(n); n + 1 }, 3)   # effect-mismatch

渡す値の効果は 3 つの出どころから採り、この順に引く。 (1) 値が帰着するリテラルの
本体、(2) 書き手がその値に書いた型注釈、(3) 値が import 先のメンバーそのものである
ときの境界の要約（§2.15）。(3) が要るのは、別ファイルのメンバーが
(1) も (2) も持たないためである — 本体は境界の向こうにあり、lib.member という綴りは
注釈を置く場所を持たない。出どころで答えが変わってはならない — 同じ嘘が同一ファイル
なら報告され、値を別ファイルへ移すだけで黙るなら、検査は綴りを問うていることになる。

(2) からは Mut を採らない。型は「どのフレームが持つ可変状態か」を述べないので、
帰属を決められる (1) と (3) だけがそのラベルを運ぶ（§2.15
「Mut の判定」）。透過を宣言したメンバー（EffectConduit）は (3) の対象外である —
透過は「渡された値の効果が通る」という宣言であって、それ自身が効果を持つとは限らない。

宣言時の形の検査

いずれも書かれた位置の構文だけで決まり、型の解決を要さない。

基底が解決できない位置（型変数・解決できない名前）では報告しない。Consuming の位置制限（§2.14「Consuming の宣言位置」）と同じ保守側の引き方である。

Mut の判定とスコープ吸収

Mut は「自分の呼び出しフレームの外にある可変状態への書き込み」である（language-spec.md §17.9）。判定に要る解析は本書に揃っている。

• ローカル束縛への代入: §2.10「束縛の重複と immutable への代入」がスコープチェインを遡る探索を持つ。代入先が自フレームで見つかれば Mut を起こさず、外側で見つかれば起こす。
• スロット代入 recv.name = v: §2.10「スロット集合が確定する」の判定を使う。受け手が自フレームのリテラルに帰着するなら Mut を起こさず、そうでなければ起こす。判定できない受け手は起こす側に倒す（純粋と誤って言わないため。本節は誤検出ゼロを保つので、Mut を過剰に付けても診断にはならず、純粋を宣言した位置で初めて報告される）。

スコープ吸収: EffectConduit なブロック引数を取る関数が、そのブロックへ Borrowed(T) を貸し出しており、かつブロック内の可変操作がすべて「貸し出された借用」か「ブロック内で生まれた束縛」に解決するなら、そのブロックの Mut はその関数の外へ出ない。判定は上の 2 つと同じスコープ解析で決まる。

吸収が成立しない形は診断ではなく、単に Mut が外へ出るだけである。

mutable counter := 0
r := arr.build(3, 0) { a |
  counter = counter + 1      # 貸し出された借用でもブロック内の束縛でもない
  a.set(0, 1)
}
# 吸収されず、この式は Mut を持つ

ハンドラーの検査

検査は 3 段で進む。操作スロット名から扱うラベルを決め、ブロックの効果推論からそのラベルの操作を集め、両者を突き合わせる。

• 操作スロット名の解決。操作スロット名は操作の素の名前（修飾を落とした末尾の識別子。fs.read なら read）である。どの操作も指さない操作スロット名は unknown-effect-operation を報告する。操作は宣言であって導出ではない — prelude と std が操作として宣言したものだけが操作であり、効果を持つかどうかからは決まらない（language-spec.md §17.9）。ブロックが実際に起こした操作の控えは網羅と引数個数にだけ使い、操作スロット名が操作を指すかの判定には使わない。
• 扱うラベルの決定。解決できた操作スロット名が指す操作のラベルを集めた和が、そのハンドラーの扱うラベル集合になる。素の名前が複数のラベルにまたがるとき、その 1 つの操作スロットが両方を受け、両方のラベルが扱われたものとする。
• 網羅の検査。扱うラベル L について、ブロックが起こす L の操作に操作スロットが無ければ non-exhaustive-handler を報告する。対象はブロックが実際に起こす操作であり、L の全操作ではない（language-spec.md §17.9）。部分ハンドルを持たないという規律は「起こしている L の操作を一部だけ扱う形が無い」ことを指す。

• 操作スロットの引数個数。操作 op: { P… | Effect(R, L) } に対し操作スロットの型は { P…, AtMostOnce({ R | a }) | a } なので、スロット数は操作のパラメーター数 + 1（継続）でなければならない。合わなければ arity-mismatch を報告する — 引数数の不一致そのものなので、ハンドラー専用の言い方は作らない。不透明型のメソッドは受け手も操作のパラメーターに数える（a.set(i, v) の操作スロットは受け手・i・v・継続の 4 スロット）。パラメーター数を引けるのは prelude の組込・std のメンバー・不透明型のメソッドである（相対 import と pkg: のモジュールメンバーはそもそも操作になれないので、操作スロット名の解決の段で落ちる）。素の名前が複数の口にまたがって数が食い違うとき（fs.read と net.read）も素通しする — 1 つの操作スロットが両方を受ける以上、要求できる数が無いためである。

扱ったラベルでも、名前を持たない葉が起こした分は残る。 ハンドラーが横取りできるのは操作スロットで名指した操作だけなので、未完了 Future への ! が足す Susp・素の代入が足す Mut・操作として宣言されていない std メンバー・不透明型メソッド・相対 import と pkg: のモジュールメンバーが足すラベルは handle 式の効果に残る。差し引くと「起こるのに宣言されていない」形が静かに通ってしまう。

したがって網羅の検査もそれらの操作スロットを要求しない。 要求に応えて書いた操作スロットは受理されず、受理されても実行時に効かないので、要求すること自体がエラーだからである。

ブロックの効果が素通し条件（下記）で計算できないとき、網羅の検査は行わない — 起こす操作が分からない位置で網羅を要求すると、判定できないことを違反として報告することになる。

handle 式の効果は「ブロックの効果から扱うラベルを除いたもの」と「ハンドラー本体自身の効果」の和である。

継続についての診断は本節が持たない。 継続は AtMostOnce（language-spec.md §17.9）なので、二重の再開・コンテナーへの格納・別フローへの捕獲・copy はいずれも §2.14 の消費追跡がそのまま報告する（use-after-consume / affine-not-copyable / cannot-bind-borrowed）。継続を呼ばない形は AtMostOnce の使い残しなので報告しない。

素通し条件

• gradual 境界（明示的な Any）を経由した値。本体が見えないので効果を計算できず、関数型注釈の呼出時強制（language-spec.md §17.4）も効果を強制できない（実行時に照合する対象が無い）。
• 型変数に倒れるブロックパラメーター。呼び先の宣言型が Any や型変数の位置には、効果を言う情報がそもそも無い。
• 循環 import・解決不能な import（上記）。
• 値として届いた関数が宣言する Mut。Mut は「自分の呼び出しフレームの外にある可変状態への書き込み」なので、同じ書き込みが見る側によって効果になったりならなかったりする。型に書かれた Mut は書いた側のフレームから見た言い分にすぎず、呼び出し元のフレームが書き込み先を所有していればそこで吸収される — 外側の可変ローカルを書き換える内部名の関数がその形で、内側の型では Mut でも外側の関数は純粋である。所有者を辿れるのは定義へ届いた経路だけなので、宣言型から採るのは残り 7 ラベルに限る。
• 部分適用の連鎖の先で呼ぶ形（f(a)(b)）。並置の段が部分適用なのか戻り値の呼び出しなのかは綴りから決まらないので、宣言型の結果を採ると部分適用の段で効果を先取りすることになる。

したがって保証はこう述べられる — 明示的な Any を一つも書かないプログラムでは、効果を宣言していない位置に効果を持つ関数が入らない（Mut と上の 2 つを除く）。§2.1 の class b の健全性と同じ形の系である。

実行時は肩代わりしない

効果の型は実行時に照合しない（language-spec.md §17.9）ため、塞ぐのは静的検査だけである。多重度型が copy の禁止について同じ非対称を持つ（§2.14）のと同じで、素通しした位置を実行時の失敗が捕まえることはない。

2.16 検出しないもの（将来段階・対象外）

次は検出しない。

• 呼び出し越境を伴う本体結果型の完全推論（将来段階）。現状は本体末尾式・可変ローカル（§2.2 のとおり確立時の型）・再帰を含む関数呼び出し結果の越境照合まで行う（呼び出し先の結果型は宣言〔束縛注釈／inner-name／body 末尾アスクリプション〕または本体推論〔再帰は §2.2 の最小不動点〕から確定し、x: T := f(args) を照合する。無型パラメーターの関数は結果 Any で保守的に素通し）。
• ループ本体の発散推論（while (true) { … } などを Never と判定する）は対象外 — 将来段階ではない。本体が実際に発散するかの判定は停止性問題を伴い、誤検出ゼロを保ったまま一般には決定できない。推論は保守側（Unknown / Unit）に倒す。
• フロー絞り込み（§2.3）の未対応範囲（将来段階）。範囲は §2.3「将来枠」が挙げる。そこが §2.11「境界の証明義務」で極性を反転させること（絞り込みの側では見逃しで済む形が証明義務の側では診断になるので、安全網がそこで報告を止める）は §2.11「素通し条件（誤検出ゼロ）」が書く。
• Future(T) payload を「到達すれば確実に panic」として照合すること（対象外 — 将来段階ではない）。実行時の注釈照合は Future の payload を検査せず（x: Future(String) := fork({ 42 }) は束縛時に panic しない）、その根拠が成立しないため原理的に報告できない。payload の照合は契約系の §2.12「Future payload の照合」が担う。

値位置の未定義参照は §2.13 が、型注釈位置の未定義型名は §2.4 が扱う。arity 不一致のうち超過は §2.8 が検出し、不足（部分適用）は正当。

• matches の右辺に置いた型でない値（1 matches f。f は関数値）は対象外 — 将来段階ではない。右辺は型式だけでなく型値を運ぶ普通の値も取り（T := Int の T・パラメーター t: Any・型値を返す呼び出し）、照合は実行時にその値を読む（language-spec.md §17.4）。静的型で切り分けられない — タグ述語（c matches Circle、§17.4 の照合表）の Circle は値コンストラクターなので静的型は関数であり、f と同じ種別に見える。関数を断れば正当なタグ述語を断つことになるので、ここは実行時の照合が backstop である。

3. 多相な組込シグネチャと単一化による結果型推論

組込関数（if など）と一部の原始型メソッド（map / filter / first / last / fold / unwrap など）、および std のコレクション（Array(e) / SortedMap(k, v) / InsertionMap(k, v) / ScratchMap(k, v) / OrderedSet(e)。std/array.md §3・std/map.md §4.2・std/set.md §3.1 のシグネチャ表）のメソッドは、結果型が引数やレシーバーの要素型に依存する多相な型を持つ。静的型検査はこれらの結果型を「型変数」と「単一化」で推論する。

3.1 単一化の基本方針

• 型変数は推論器の内部表現であり、ユーザーは型コンテキストの bare 小文字で記述できる（language-spec.md §17.2）。記述された型変数は内部生成の型変数と同じ単一化・代入で扱う。
• 単一化は結果型を推論するためだけに使い、不一致を見つけても診断は出さない。分岐や引数の型が割れた場合は結果型を Any に、手がかりが無い場合は Unknown に倒す。この振る舞いは分岐合成（join）と同じで、新たな型エラーを生まない。
• 型不明・Any の実引数が流れる型変数は Any へ束縛する: 実型が Unknown / Any の位置に現れた型変数は Any に束縛し、既存・後続の束縛とは join で拡げる。無制約のまま素通しすると、同じ変数を別の既知実引数が束縛したとき動的な位置の寄与が消え、結果が既知側の型で確定して「実行時に他の値も流れうる式」への誤検出の種になる（§2 誤検出ゼロ）。例: 初期値 0 とブロック結果が型不明な fold の結果は Int に確定せず Any。実型が Never（発散・再帰の解決中プレースホルダー）の束縛は join の恒等元として他経路の型に収束する（§3.3）。
• 多相メソッドの呼び出し形は paren / juxtaposition のどちらでも同じに扱う: recv.method(a, b) と recv.method a b（AST 上は連鎖 CallExpression）を平坦化して同一の method call として単一化する。引数不足の場合は部分適用とみなし、残余 params を持つ関数型（未解決の型変数は残したまま）を返す — これにより .fold "" のような単独の部分適用も後続の適用や curried 用法で正しく型付けされる（完全適用時にだけ未解決変数を Any に倒す）。

3.2 境界付き型変数の診断（単一化の例外）

境界付き型変数（language-spec.md §17.2）だけは単一化の例外として診断を出す。境界には閉じた union（type set 境界）と構造的 interface（interface 境界）の 2 種があり、いずれも呼び出しの単一化で違反が確実な呼び出しを §2 で報告する。

• ① 同型分裂: 境界付き型変数が静的に確定した複数の型に割れるとき報告する。
• 例: sum(1, 2.0)（type set 境界 a: Number が Int と Float に割れる）、min(1, 2.0)（interface 境界 a: Comparable でも Int/Float は rigid なので割れる）。
• interface 境界では、確定 member が rigid な型（原始型・Unit・名目 opaque＝静的型が実行時型を一意に決める種）のときだけ報告する — record/list/tuple/variant/function は幅部分型ゆえ静的型が異なっても実行時に一致しうるため素通しする。
• rigid ガードは interface 境界にのみ適用する — type set 境界は member が閉じた union の alt に確定し、異なる alt（enum を境界にした a: Shape の異なるタグ等）は実行時に確実に割れるため無条件に報告する。
• ② 非充足: 確定型が境界を満たさないとき報告する。
• type set 境界: 確定型が境界のメンバーでない（math.abs("a") — String は Number のメンバーでない）。
• interface 境界: 確定型が interface を確実に満たさない（describe(5) — describe := {x: a: Drawable | …} に対し Int は draw に応答せず slot も生やせない）。判定は tri-state（満たす／満たさない／不明）で、record 型・function 型がエントリを静的に持たない場合や Any/Unknown/型変数は「不明」として素通しする。名目 opaque はカタログの表にそのメソッドがあるかで閉じる（Instant / SortedMap / OrderedSet は compare を持つので Comparable を満たし、File は満たさない）。
• 受け手の型引数への適用: std のコレクションのシグネチャが受け手の型引数に境界を置くとき（SortedMap((k: Comparable), v) の k・OrderedSet((e: Comparable)) の e）、その型変数を引数に取るメソッドの呼び出しは受け手の型引数を②で判定し、type-mismatch: receiver of insert expects SortedMap((k: Comparable), v), got SortedMap(List(Int), String) の形で報告する。型変数を引数に取らないメソッド（length / keys）は見ない（std/map.md §4.2・std/set.md §3.1）。
• いずれも当該実引数の型が静的に確定しているときだけ報告する（Unknown / Any / 未解決を含む場合は素通し）。実行時単一化（language-spec.md §17.2）が backstop。

3.3 Never（ボトム型）の扱い

Never（language-spec.md §17.2、panic / exit の結果型や return / break / continue の式位置の型など発散位置の型）は全型の部分型で、join の恒等元として働く — join(T, Never) = join(Never, T) = T（全深度）。これにより発散アームを含む分岐が他方の具体型へ精密に解ける。

• if (c) { 1 } { panic("x") } は Int。
• if (c) { v } { return d } の結果型は v の型に解ける。return(v) の引数 v の型は別途関数結果型の収束へ寄与する（§18.2 の return、§16.5 の ?）。
• gradual 整合性 consistent（§2.9「分岐の結果型に収束を要求」）でも Never は Any・型変数と同じく全型と整合する wildcard で、発散アームは分岐の割れと断じない。
• 代入照合では Never 値（actual）は任意の宣言型に代入可（Never <: ∀T）。逆に宣言型が Never で値が確定した非 Never 具体型なら確実な不一致として報告する（「返らないと表明した位置が値を返す」）。
• 発散と見るのは prelude の束縛のままの綴りだけである。 return / break / continue は予約語ではなく prelude 束縛なので（language-spec.md §18.1 の「名前として引ける」）、書き手が同名を宣言すればそちらが勝ち、実行時もその束縛を呼ぶ。覆われた綴りの呼び出しは普通の呼び出しで、式位置の型はその束縛の結果型である。綴りだけで Never と決めてはならない — Never は全型の部分型なので、その位置の型不一致がまるごと黙る。

3.4 分岐合成 join（gradual meet）

完全一致ならその型。それ以外は以下。

• 同種のジェネリックコンテナー（List / Option / Result / Future / Tuple）は要素ごとに再帰合流し、より精密な分岐へ寄せる — コンテナー内部では Any と Result の未制約な E（Ok(5) のように E を確定させない構築の E）を identity とみなし他方の確定型を採る。宣言された Result(T) ≡ Result(T, Error) は E が Error に確定しているので未制約ではなく、identity にはならない。
• if (c) { Ok(()) } { Err("x") } は Result(Unit, String)（Ok(()) の Result(Unit, _) と Err("x") の Result(_, String) を合流）。
• if (c) { Some(1) } { None } は Option(Int)。
• if (c) { [1] } { [] } は List(Int)。
• map / and_then / or_else / map_err はエラー型を結果へ運ぶ — map はレシーバーの E、and_then はレシーバーと同じ E、or_else と map_err は写し先の E。E を確定させられない構築（Ok(5)）だけが未制約のまま残る。
• 同一 enum に属する異なるタグの Variant 同士は親 enum 型へ持ち上げる — enum ParseError := OneOf(Empty, NotANumber(String), TooBig) のもとで match の各 Err 分岐（Err(Empty) / Err(TooBig) / Err(NotANumber(s))）を合流するとエラー型は ParseError に解け、Ok(7) と合わせた match 全体は Result(Int, ParseError) になる（language-spec.md §17.4）。所属 enum が分からない・異なる enum 同士・親が複数候補ある場合は Any に倒す。
• 同じタグ同士の Variant は payload を要素ごとに再帰合流する — タグ名・所属 enum・arity がすべて一致するときだけ働き、一致しなければ Any に倒す。親 enum 型への持ち上げを先に試すので、これが効くのは主に親 OneOf を持たない単一タグ enum（OneOf(A) ≡ A の退化。language-spec.md §17.4）である。enum Box(a) := Wrap(a) のもとで if (c) { Wrap(1) } { Wrap("s") } は Wrap(Any) になる（Any に倒さない）。Wrap(Any) は両分岐の値を覆うので上界として正しく、タグと arity が分かっている分だけ Any より精密である。所属 enum を一致条件に含めるのは、異なる enum の同名タグを混同しないため（§17.4 のタグ namespace 分離）。
• record 同士は共通スロットの交差へ合流する（幅合流）— 両者が持つ名前のフィールドだけを残し、各フィールド型を再帰合流する。if (c) { {x := 1, y := "s" |} } { {x := 2, w := true |} } は { x: Int |}。共通スロットの型が割れたら、そのフィールドは残したまま型を Any にする — 到達すれば値は必ずそのスロットを持つので、幅の情報は捨てない。共通スロットが 1 つも無ければ Any に倒す（空 record 型は実行時に全ての値と一致するため、合流結果としては Any より狭く名乗れない）。フィールド順は左辺の順に従う。
• 片側がメソッド契約フィールド（型を持たない bare フィールド。language-spec.md §17.5 の構造的 interface）なら合流結果も bare フィールドになり、静的照合は実行時判定に委ねる（保守側）。
• 共通スロットの片側が Any なら結果の型も Any にする（幅は残すが型は狭めない）— {x: Int |} と {x: Any |} の合流は {x: Any |}。同種コンテナーの要素合流（List / Option 等、上記参照）は Any を identity とみなして他方の確定型を採るが、record のフィールドではその正当化が効かない。要素側の Any は「未制約」（None / [] のような構築時の多相変数由来）が支配的なのに対し、record のフィールドの Any は動的な値そのものから来るため、片側だけの型でスロットを確定させると実行時に正当なプログラム（if (c) { {x := dyn |} } { {x := 1 |} } の .x を String へ代入する等）を誤検出する。Any を素通しする漸進性の原則に従い、型は Any のまま残す。
• 宣言された閉じた union へ吸収する（包含）— 片方の選択肢集合が他方に含まれるとき、広い方の型を採る。単体の型は 1 要素の集合とみなすので、OneOf(Int, String) と Int の合流は OneOf(Int, String)、Number と Int の合流は Number になる。同一 enum のタグ持ち上げと同じ規則の別の入口で、合流結果は必ずどちらかの枝に既に現れていた型になる（推論が宣言されていない union を合成することはない）。選択肢が互いに含まれない union 同士は Any に倒す。
• refinement 型（language-spec.md §17.7）同士は含意で合流する — 同一基底で片方の述語がもう片方を含意すると証明できたなら、含意される側（広い方）を採る（それが両方の上位型である）。互いに含意する組では、枝の順に依らず選言標準形の節数が少ない方（同数なら原子数、それも同数なら正準形の辞書順）を残す — 含意の判定手続きは前提の節数に反比例する予算を持つため、綴りの選び方が枝の順に依ると下流の証明の成否まで順に依ってしまう。型等価な組（原文が一致する組）はその型のまま。どちらの向きも証明できない異なる組・基底型が異なる組・断片外（refinement_opaque）を含む異なる組、および refinement と非 refinement の組は基底型へ持ち上げる（Any に倒すと§2.5「値束縛の型」が無関係な注釈を要求してしまう）。含意の判定は過小近似なので「証明できない」は常に基底型へ倒れ、合流が実際より狭い型を作ることはない。
• ただし上の宣言された閉じた union への吸収を先に試す — Sign := OneOf(Pos, Neg) のように union の選択肢そのものが refinement のとき、Sign とその選択肢 Pos の合流は Sign になる（先に基底へ剥がすと Int と Sign の組になり Any へ倒れてしまう）。どちらも union でない refinement 同士の合流には干渉しない。
• consistent もこの吸収に追従する — union とその選択肢を分岐の両枝に置いた Pos と Sign は整合とみなし、§2.9「分岐の結果型に収束を要求」は報告しない（合流型が Sign になるとおり、両枝は実際に収束している）。この非対称は refinement 固有ではなく Int と OneOf(Int, String) でも起きたもので、join を緩めるのではなく consistent を join に揃える向きで解消した。consistent は §2.9 の分岐の収束と到達しえないアームの判定・§2.6「inner-name 型と slot/結果型の整合」・§2.12「Future payload の照合」が共有する（§2.10 の型安定性の 2 規則は方向のある判定を使うので consistent を共有しない。union の選択肢への正当な代入 x: OneOf(Int, String) = 1 の後の x = "s" は、宣言型の選択肢に収まるので方向のある判定でも通る）。判定は誤検出ゼロ側に倒し、かつ対称に保つ — 片方が union なら他方がその選択肢のいずれかと整合すれば整合、双方が union ならどちらかの向きで「一方の全選択肢が他方のいずれかの選択肢と整合する」が成り立てば整合とし、分からない組は整合扱いにする。片方向だけで判定すると consistent が対称性を失い、§2.9「分岐の結果型に収束を要求」の可否が分岐の枝の順に依ってしまう（if (c) { a } { b } と if (c) { b } { a } で答えが変わる）。join が綴りの選択を枝の順に依らせないのと同じ要件である。
• 覆いの型構築子は剥がして基底同士で合流する — 効果型（language-spec.md §17.9）と多重度型（§17.8）はどちらも値の型そのものではなく、型の照合はその層を剥がして基底同士で行うからである。refinement は含意を先に試し、導けなければ基底へ落とす（上記）。同じ覆い同士は型等価なのでその型のまま残るので、剥がす対象は層の有無か基底が食い違う組だけである。剥がさないと合流が Any へ倒れ、その先の照合がまるごと素通しになる（AtMostOnce(Int) を返す呼び出しと 2 を並べた [mk(), 2] の要素型が List(Any) になり、List(String) への代入が黙る）。
• トップレベル（コンテナーの外）の Any は保つ — if (c) { 1 } { dynamic } は Any のまま（全体が動的な分岐を不用意に精密化しない）。合流できない異種・確実に割れるスカラー要素は Any に倒し、どちらかが Unknown なら Unknown。
• 同じ join を if / when / match の枝で再代入された可変ローカルの合流点併合にも使う（§2.2）。分岐の結果値だけでなく枝を跨ぐ可変ローカルの型も合流点で join し、割れれば Any に倒す。
• 例: if (c) { "a" } { "b" } → String。[1, 2].map({ x | x.to_char() }) → List(String)。if (c) { 1 } { "a" } → Any（§2.9「分岐の結果型に収束を要求」がこの分岐をエラー報告するが、合流型自体は Any のまま）。