hikari 静的解析 (static analysis)

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

節	層	対象	いつ走るか
§1	構文層の一括検査	パースエラー・import 解決	実行前・LSP 診断前（常時）
§2	静的型検査	「到達すれば確実に型的 panic」になる箇所	`hikari check` / LSP
§3	strict 型検査	§2 に契約系診断を上乗せ	`--strict` 指定時
§4	単一化による結果型推論	§2/§3 の基盤（多相な結果型を解く）	型検査中
§5	末尾位置マーキング	TCO 用の末尾呼び出し検出	パース直後

前提: 型注釈の文法・実行時照合は language-spec.md §17、エラーの三層モデルは同 §16。各コマンド（hikari check / hikari build / LSP ほか）の挙動は hikari-command.md。

本書で繰り返す用語

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

健全 (sound): 報告する診断はすべて正しい。すなわち 誤検出（false positive）を出さない。
不完全 (incomplete): 静的に確定しない箇所は見逃す（false negative を許容）。
漸進的 (gradual): 型が確定しない箇所は動的に扱い、実行時照合に委ねる。
「到達すれば確実に panic」: その箇所が実行されれば必ず language-spec.md §16.2 の型的 panic になると静的に確定できること。§2 が検出するのはこの条件を満たす箇所だけ。
素通し: 静的に確定しない箇所を検査から外して通すこと。各規則の「素通し条件」がその一覧で、これが誤検出ゼロを担保する。
backstop: 静的に見逃しても、実行時照合（language-spec.md §17 冒頭）が最終的に捕捉すること。
`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 と違い入れ子リテラル内も可）にのみ書け、式の位置（部分式・:= / = の右辺・引数）に現れるとパーサが構文エラーにする。
import 先不在: import リテラルが解決したパスにファイルが無い場合（analyze で検出。これだけは構文層でなく解決層の検査）。language-spec.md §16.1 の「ファイル不在 = 回復可能エラー」は fs.read 等プログラムが明示的に行う I/O への指針であり、モジュール解決には適用しない（Go / Rust / ES modules と同様、欠落モジュールはロード時の静的エラー）。
未知の標準ライブラリモジュール: import <対象> := "std:<name>" の <name> が std/index.md に無い場合（analyze で検出）。解決層の静的エラーで、回復可能にはしない。ただし jsgen 専用モジュール（hikari build-js でのみ有効な std: 名。js-backend.md §2.3・§2.4）は既知の名前として受理し、この誤検出を出さない（インタプリタ実行時に別途 hikari build-js 専用である旨のエラーになる）。
`std:ffi/js` の束縛形・member（js-backend.md §1、std/js.md）: 上記の jsgen 専用モジュールとして受理されるが、次の 2 点を追加で検査する（解決層の静的エラー）。

分解束縛の拒否: import [call, get] := "std:ffi/js" のように名前空間束縛（import js := "std:ffi/js"）以外の形は静的エラー（std/js.md §3）。
未知 member: std:ffi/js を束縛した名前への member 参照（js.<name>）で <name> が定義済み 11 member（std/js.md §1）のいずれにも該当しなければ静的エラー。他の std: モジュール（§2.3 の一般則）と異なり、std:ffi/js は member 集合が言語仕様で完全に閉じているため通常モードでも検査する。

third-party パッケージ解決の失敗: import <対象> := "pkg:<alias>" で次のいずれか（analyze で検出）。解決層の静的エラー。

(a) その .hikari を含むパッケージにマニフェストが無い
(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 が body 領域（| 後、または 0-pipe #{hikari} の本体全体）または入れ子リテラルに出現

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

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

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

2. 静的型検査（`hikari check` / LSP）

型注釈の照合は実行時に走る（language-spec.md §17 冒頭）が、hikari check と LSP 診断はそれに加えて、実行前に型不一致を健全に検出する。検出するのは「到達すれば確実に型的 panic になる」ことが静的に確定する型不一致だけで、確定しない箇所は素通しする（漸進的型付け）。したがって誤検出は出さず、見逃しは許容する。実行時照合が backstop。

--strict はこの §2 の検査に加えて class b の健全性（Any-free 領域で §16.2 の型的 panic を起こさない）を保証する（§3・ADR 0070）。

照合は language-spec.md §17.4 の表に従い、静的に判る型同士で行う。

2.1 型注釈と値の不一致

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。
スロットのデフォルト確定 {x: T := d |}。
注釈位置に確実に型でない値が来る場合（追跡可能な範囲で）。

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

型注釈位置（束縛・スロット・分解・結果型アスクリプション expr: T）に次が来る場合、到達すれば確実に実行時エラー（undefined: <name> / not a valid type expression）になるため報告する。

未定義の型名（スコープに束縛の無い大文字始まりの参照）
型になり得ない式（数値・文字列リテラル・演算子式など）

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

型注釈位置の型適用 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.1）・closed variant の match 網羅性（§3 — 判定時に遅延適用を 1 段ずつ展開）が非再帰ジェネリック enum と同水準で働く。

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

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

中置メソッド呼び出し形（並置 dispatch recv name / recv name(args)、language-spec.md §8.1）にも同じ規則を適用する。閉じた型は関数ではないので実行時にこの並置はメソッド dispatch にしかならず、識別子のリテラル名がそのままメソッド名に使われる。素通し条件（Any・型不明・open object・関数・一般 record の受信者）は dot 形と同一。

補足: 原始スカラー・variant・不透明型は実行時も同じ no such slot or method に落ちる。閉じたリスト/タプルリテラルの並置は body-empty 関数への適用に帰着するため実行時の語句は別（undefined / スロット束縛不能）になりうるが、同位置で確実にエラーになる点は同じで、hikari check は一律に no such slot or method として報告する。

対象は値が後から slot を増やせない型に限る。

原始スカラー（Int / Float / Bool / String / Bytes / Range）と variant（Option / Result / Ordering）: 型から閉じたメソッド集合が一意に決まる。
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`: extensible（open object、language-spec.md §2.4）が静的には同じ型に推論されつつ実行時に名前スロットを持てる（x: List(Int) := extensible[] のあと x.foo := 1 が成立）ため、受信者が閉じたリテラル（非 extensible の […] リスト・タプル (…)）に直接帰着する場合に限り検査する。変数・関数戻り値・注釈経由の受信者は open object かもしれないため素通し。
import 先モジュール（相対 import import mod := "path.hikari" / third-party import mod := "pkg:…"）: import 先のファイルオブジェクトは closed（language-spec.md §13.1 — ファイルレベルの暗黙リテラルは closed で extensible 適用不可、slot 生成はトップレベル slot-list 宣言時のみ）なので、一般の record（幅構造型）と異なりメンバ集合が静的に閉じる。受信者が `import` で丸ごと束縛した名前（別名連鎖 m2 := m1 も辿る）に帰着し、import が解決でき record 型を組めるとき、name が import 先トップレベル slot にも universal method にも該当しなければ報告する（mod.member(args) の呼び出し形も同様）。

公開メンバは slot-list 領域の束縛のみ。body 領域の値束縛（name := expr）は最外側フレームのローカルで slot にならない（0-pipe #{hikari} は全体が body のため公開 slot 0 個 — mod.x は実行時に no such slot/method）。
`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.15「import 先モジュールの型」）で閉じるため原理的には同様に検査でき、その不透明型（Instant 等）は既に本節の対象。ただし std: 名前空間オブジェクト自体のメンバ検査は当面行わない（見逃しは許容）。例外は `std:ffi/js`（§1 の追加検査）で、member 集合が固定 11 個に閉じているため通常モードでも未知 member を検査する。

対象外: 一般の record（幅構造型 — 宣言に無いフィールドを持ちうる。上記 import 先モジュールのような closed 確定の受信者を除く）・関数・open object・Any・型不明の受信者、および数値スロット（t.0）。封印契約型（export [name: T]、language-spec.md §17.6）に確定した受信者は、実行時 backstop を持たない（Stage 1）ため本節（通常モード）ではなく §3 規則 (11) の --strict 限定診断で扱う。

2.4 分解 import の未 export 名

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

これは 0-pipe #{hikari}（全体が body 領域＝公開 slot 0 個）を import [x] := "script.hikari" で受ける典型的な誤りを実行前に捕捉する。循環・解決不能な import は素通し。

2.5 slot 代入

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

位置スロット（数値プロパティ recv.0 / 整数リテラルキー recv.[0]）への代入は、受け手に関わらず常に immutable（language-spec.md §7.4）なので、shape を解決せず常に報告する（cannot assign to immutable positional slot）。
名前スロットは、recv が確実に closed なオブジェクト値（§2.6）に帰着するとき、実行時 language-spec.md §6.2 の規則どおり次を報告する。

式	状況	エラー
`recv.x := v`	closed object は slot 追加不可	`cannot add slot ':='`
`recv.x = v`	`x` が存在しない slot	`no such slot`
`recv.x = v`	`x` が既存の immutable slot	`cannot assign to immutable slot`
`recv.x = v`	`x` が既存の mutable slot	（正当・報告しない）

2.6 「確実に closed」の範囲

language-spec.md §2.4 のとおり object の open / closed は実行時の値の性質であり、静的には一般に判定できない（注釈付き record パラメータ・戻り値・import 越境の値は extensible（open）かもしれない）。そのため名前スロットの検査は受信者が次のいずれかに帰着する場合に限る。

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

ブラケット形 […] の名前スロット解釈は brace 形と共通で既定 closed（language-spec.md §2.1.1）なので、last := [ col := -1, row := -1 ] のような純名前スロットのブラケットリテラルも対象。位置要素を含むリテラル（[1, 2] / [1, col := -1]）は brace 形と同様に対象外（shape を確定させない保守側の見逃し）。

immutable 束縛なら値は不変でその closed リテラルに固定されるため健全。素通し: mutable ローカル（=、後で open 値に再代入されうる）・注釈付き束縛・関数引数/戻り値・import 越境。これは §2.3 の List / Tuple メソッド検査（閉じたリテラルにのみ働く）と同じ保守戦略。

動的アクセスのキー recv.[k] は k が静的に定数（文字列/整数リテラル、またはそれらへの immutable 束縛名）のときだけ解決する。非定数キーは素通し。

2.7 copy-and-update overlay の未知キー

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

overlay のキー（名前スロット名）が受け手 recv の名前スロット集合に無いとき、copy: no such slot: <name> を報告する（未知キーをソース順にすべて報告）。受け手の名前スロット集合は closed リテラルの宣言スロットから確定し、実行時の権威集合（§9.5）と一致する。
overlay が位置スロットを含むとき、copy overlay must have only name slots (no positional slots) を報告する。実行時は位置スロット検査が未知キー検査より先に走る（§9.5）ため、この 1 件のみ報告し未知キーは報告しない。

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

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

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

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

組合せ	対象演算子
`Int <op> Int`	`+` `-` `*` `/` `%`
`Float <op> Float`	`+` `-` `*` `/` `%`
`String + String`	`+` のみ

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

2.9 順序比較の型不一致

< / <= / > / >= で、両辺の静的型がともに原始スカラーに確定し、その組合せが実行時に確実に 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 等）。

2.10 短絡の型不一致

&& / || で、左辺の静的型が 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・型変数・原始スカラー以外。

2.11 完全適用の arity 超過

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

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

2.12〜2.15 静的型の決め方（ローカル推論）

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

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

mutable ローカル（`=`）: 直前の代入（同一スコープの直線的フロー）の右辺型を採る。加えて `if`（両枝）/ `when` / `match` の枝で再代入された可変ローカルは、枝合流点で各経路の型を `join` して確定する（フロー感応な局所推論）。

各経路は、再代入したなら再代入後の型、しなければ分岐前の型を寄与する。when の false 側・catch-all 無しの非網羅 match の Unit フォールスルーは分岐前の型を経路に含める。
全経路が一致すればその型に精緻化し、割れれば Any、いずれかが型不明なら Unknown（健全側）。
枝内の `:=` シャドウ・`match` の arm パターン束縛は外側変数を変えない別束縛として合流から除外する（怠ると外側変数を誤って narrow し誤検出になる）。
`while` はフォールスルー合流で追跡（本体を分岐前型で 1 回畳み、join(本体再代入型, 分岐前型) を採る。ループは 0 回以上実行ゆえ分岐前型を必ず経路に含める）。単一パスで健全 — 本体型が分岐前型と一致すれば安定、割れれば Any に倒れる（全反復の上界）。
`loop` / `conduit`（自己再帰/制御透過）とスコープチェーンを遡る更新（language-spec.md §6.1）は追跡せず分岐前の型に留める（保守側）。右辺型が静的に不明な mutable ローカルは型不明。
この枝合流は結果型推論だけでなくチェッカの逐次診断（分岐後の文の型照合）にも用いる。

式アスクリプション `expr: T`（language-spec.md §17 冒頭・§17.1）: 内側式の推論型に依らず注釈型 `T` を採る。評価地点で T へ実照合され一致しなければ確実に panic（§16.2）するため、到達すれば静的型は T で、束縛注釈 x: T := v と同じ健全性を持つ。これにより後置した結果型が後続束縛へ伝播する（vrows := build_vrows(0): List(VRow) の vrows は List(VRow)）。T が型として解決できない場合は Unknown（素通し）。

関数の結果型を宣言する正しい形は language-spec.md §17.3 の 3 形（束縛注釈 f: {… | T} := {…} ／内部名注釈／body 末尾アスクリプション {… | expr: T}）。関数値の外側に後置した {…}: T は「関数値そのものを T に照合する」式アスクリプションであり結果型宣言ではない。

代入族の文の値型: 束縛・代入（:= / = / スロット代入 / 分解代入 / 複合代入）は文としての値型が `Unit`（language-spec.md §6.1）。よって関数本体の末尾式が代入族の文なら結果型は Unit に確定し、右辺型が静的に不明でも Any に倒れない。これは束縛が変数の型を記録する動作とは別軸 — 記録するのは変数の型、文自体の値型は Unit。

2.13 関数リテラルの結果型

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 の恒等元（§4.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（発散）に解ける。再帰呼び出しの実引数はプレースホルダのパラメータ型（束縛注釈があればその契約）で照合される。
束縛注釈が関数型に解ける宣言は、解決中の再参照もその契約型で見る（結果も宣言どおり）。

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

データオブジェクトの 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 に解ける。位置要素を持つデータオブジェクト（{ 1, 2 | }）は record 形に収まらないため確定しない。
原始型メソッド（型メソッド）の呼び出し recv.method(args):

単相メソッド（戻り型がレシーバの型ラベルだけで一意）は直接推論（27.to_char() → String、"hi".to_int() → Option(Int)、xs.length() → Int）。
多相メソッド（map / first / unwrap / fold / and_then など戻り型が要素型・ペイロード型・ブロック結果型に依存）は §4 の単一化で解く。copy / flatten のように戻り型がレシーバ型そのもの・その入れ子要素型になるものはレシーバ型から直接導く。
シグネチャを収録しないメソッド（each — block 内の break が任意型で escape しうる）とレシーバ型が確定しない呼び出しは型不明。

位置軸の反復メソッド（each / map / filter / fold）にブロックリテラルを渡すとき: レシーバの要素型が判ればブロックの要素パラメータを要素型で束縛する（List(Int) / Range / Bytes の要素は Int、String の要素は長さ 1 の String）。fold は加えて先頭引数（初期値）の型を累積パラメータに束縛する。これでブロック本体のローカル推論と hover が要素型を見られる。

paren 形 recv.method(a, b) と juxtaposition 形 recv.method a b（AST 上は ((recv.method a) b) の連鎖 CallExpression）は同じ method call として平坦化。シードは全引数が揃った最外の呼び出しでだけ流し、連鎖の中間段（recv.method a 単体）は素通しする。反復メソッド自体の戻り型は §4 の単一化で解く。

record/object のフィールドアクセス recv.field: recv の静的型が record/object 型でフィールド field を持つとき、そのフィールド型を採る。フィールドが関数型で呼び出される（recv.field(args)）ときは §4 の単一化で結果型を解く。record 型は幅構造型（宣言フィールドは下限で、値は宣言に無いスロットを持ちうる。language-spec.md §2.4）なので、宣言に無いフィールドへのアクセスは Any（gradual top）とする。
位置スロットアクセス 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 のように要素アクセスの連鎖が解ける。

2.15 import 先モジュールの型

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

相対 import（import mod := "path.hikari"）: 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.3）や分解 import（§2.4）は、exported member 集合に無い名前として no such slot を報告する。
third-party（`pkg:`）: pkg:<alias> は相手パッケージの入口 .hikari に解決される（packages.md）ので、入口ファイルから相対 import と同じく record 型を組む。未取得（キャッシュ不在）は Any。
標準ライブラリ（`std:`）: Go ネイティブ実装で .hikari ソースを持たないため、処理系が保持する構造化型シグネチャ（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 値。

2.16 `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.10）のため、式が値を生めばその値は確実に `Bool`（さもなくば実行時 panic）— 被演算子の型に依らず Bool に確定する（== / != の常時 Bool、String 連結の精緻化と同じ論法）。左辺は短絡に関わらず必ず評価されるため左辺が Never（発散）なら式も Never。右辺の Never は左辺の短絡で回避されうるため伝播しない。
原始スカラーの順序比較の値は `Bool`: < / <= / > / >= は universal method compare に落ち一般には上書きされうる（値型は確定不能）が、両辺が確定原始スカラーで妥当な同型組合せ（§2.9。Int/Float/String/Bool の同型）なら compare スロットを持てない閉じた型で組込比較に落ち、式が値を生めば確実に `Bool`（== / && の常時 Bool と同じ論法）。妥当でない組合せは実行時 panic（§2.9 で報告）のため値を生まず対象外、非原始・Any・Unknown が絡む辺は確定不能のまま。
レコード更新 `+` の値は合成 record 型: 両辺が record 型なら結果はフィールドを右勝ちでマージした record 型に確定する（language-spec.md §7.4.1、値の合成と同じ右勝ち規則。左のうち右に無い名前→右の全名前の順、同名は右の型で上書き）。到達すれば結果値はそのフィールド集合を確実に持つため（r + { field := v |} のレコード更新の精緻化）。片辺が Any なら結果も Any（§2.16 冒頭）、List 同士は要素 join の List（既存）。
確定できない式: 一般の関数呼び出しの結果・多相メソッド・（Any でない受信者で）フィールドを確定できないメンバアクセス・演算子の不明な組合せ・右辺型が静的に不明な mutable ローカルなどは型不明として扱い、不明が絡む照合は素通しする。

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

次は検出しない。

呼び出し越境を伴う本体結果型の完全推論（将来段階）。現状は本体末尾式・分岐合流した可変ローカル・再帰を含む関数呼び出し結果の越境照合まで行う（呼び出し先の結果型は宣言〔束縛注釈／inner-name／body 末尾アスクリプション〕または本体推論〔再帰は §2.13 の最小不動点〕から確定し、x: T := f(args) を通常モードでも照合する。無型パラメータの関数は結果 Any で保守的に素通し）。残るのは loop / conduit の反復合流・発散推論（language-spec-future.md「型注釈の残課題」）など推論器が Unknown に倒す特殊フロー。
Future(T) payload の通常モード照合（対象外 — 将来段階ではない）。実行時の注釈照合は Future の payload を検査せず（x: Future(String) := fork({ 42 }) は束縛時に panic しない）、「到達すれば確実に panic」が成立しないため通常モードでは原理的に報告できない。payload の照合は strict の規則 (10) が担う（§3）。

値位置の未定義参照は §1 のとおり通常モードでは実行時 panic のまま（型注釈位置の未定義型名のみ §2.2 で静的検出）。ただし --strict は値位置の未定義参照も静的検出する（§3）。arity 不一致のうち超過は §2.11 で通常モードでも検出し、不足（部分適用）は正当。通常モードの hikari run / hikari build には strict 規則を適用しない（実行時照合が backstop）。hikari run --strict / hikari check --strict は strict 規則を上乗せする（§3）。

3. strict 型検査モード（`--strict`）

--strict を付けた hikari <path> --strict（ファイル実行）と hikari check --strict は、§2 の健全・漸進的な検査に以下の追加規則を上乗せした strict モードで検査する。hikari <path> --strict は診断が 1 件でもあれば評価せず停止する（exit code は §1 / hikari-command.md §5・check.md と同じ。0=クリーン、1=型/構文エラー）。

フラグ無し（通常モード）の挙動は不変 — hikari <path> は型検査せず実行し、hikari check は §2 の検査のみを行う。

strict の健全性基準（class b）: strict モードは §2 の「健全・不完全・誤検出ゼロ」に加えて class b の健全性を満たす — --strict が診断ゼロで通れば、チェッカが具体型（非 Any・非 Unknown）を割り当てた各評価点で値が実行時にその型と整合し、`Any` を経由しない領域では [language-spec.md](language-spec.md) §16.2 の型的 panic（型不一致・no such slot/method・arity 不一致・未定義参照）が起きない。Any 境界の逸脱は実行時照合が backstop。判定原則は「imprecision（Any に倒す箇所）は塞がず、unsoundness（具体型を assert して受理したのに backstop も無く panic しうる箇所）だけを塞ぐ」。設計判断は ADR 0070。

規則 (1)〜(3) と規則 (13) は「明示された型を検査に使う／型注釈を要求する」系（規則 (1)(2)(13) は暗黙 Any を書かせない方針、規則 (3) は宣言型の越境利用）、規則 (4)〜(12) は「到達すれば確実に panic」に乗らないが契約に反する箇所を実行前に塞ぐ収束系・契約系の診断である。

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

規則 (1)(2)(13) の暗黙 Any 規律は一貫した思想に立つ — 暗黙の `Any`（型を書かず推論・省略で `Any` になる位置）は禁止し、`Any` を意図するなら明示せよ。ただし「明示」と認める書式は位置ごとに定める。下表に許否をまとめる（✓ 許容 / ✗ 禁止）。

位置	暗黙 `Any`	明示オプトインと認める書式	明示だが認めない書式
パラメータ型（規則 (2)）	✗ 禁止（bare `x`）	✓ インライン注釈 `x: Any`	✗ 関数型注釈位置 `{Any \| R}`
結果型（規則 (1)）	✗ 禁止（省略して推論がネスト位置に `Any` を含む）	✓ 束縛注釈 `f: {P \| Any} := …` ・内部名注釈 `{ inner self: {P \| Any} \| … }`	✗ body 末尾アスクリプション `{ … \| expr: Any }`
値束縛の型（規則 (13)）	✗ 禁止（無注釈で推論型が `Any` を含む）	✓ 束縛注釈 `x: Any := …`	—

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

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

パラメータと結果型で「インライン注釈 ↔ シグネチャ注釈」の許否が反転している点に注意（規則 (2) 脚注）。

規則 (1) 名前付き関数の結果型の暗黙 `Any` を禁止（明示 `Any` はオプトインで許容）

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

暗黙 `Any` の禁止（省略して推論がネスト `Any` に到達）: 結果型注釈（language-spec.md §17.3 の 3 形）を省略し、本体推論の結果型（§2）がネスト位置に `Any`（gradual top）を含むとき型エラーを報告する。判定は規則 (13) の containsImplicitAny と共通で、List(Any)・Option(Any)・Future(Any)・Result の成功型・タプル/record の要素・enum 適用の型引数などに Any を含む場合を指す。空 [] / extensible[] を返す関数（List(Any)）がこれに当たる。書き手には具体型の付与か、下記の明示オプトインを促す。
bare な top-level `Any` は対象外（規則 (13) と対称）: 結果型そのものが Any に等しいだけ（ネスト位置の Any を含まない）のときは報告しない。これは Any パラメータや明示 : Any ローカルが結果へ流れた透過的な帰結で、規則 (13) が 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 型へ強制する無意味な値上書き（静的精度を捨てるだけで契約宣言ではない）ため、明示オプトインと認めない。
具体型・型変数は従来どおり: 結果型を具体型で宣言・推論できれば規則 (3) の越境照合に使う。推論結果が Unknown（静的に確定不能。§2.16）のときは素通しする。結果型が型変数の場合は Any ではないため許容する。
他規則との重複回避（二重報告の抑止）:

分岐が確実に割れるケースは合流結果が top-level Any に倒れる（ネスト Any ではない）ため本規則は発火せず、規則 (4) が「分岐結果型の非収束」として報告する。
?（失敗 bail）が絡む関数の結果収束は規則 (4) の checkResultConverge が担当するため、本規則は ? を含む本体を素通しする（局所推論では bail の成功型が Any へ倒れ偽陽性になりうるため）。
パラメータ型が確定しない関数は規則 (2) が報告するため、本規則はパラメータ型が確定した関数の結果型のみ検査する（無型パラメータ由来の結果 Any を二重報告しない）。

対象: トップレベル／ローカルの束縛 name := <関数> / name: T := <関数>、および名前スロットのデフォルトが関数の場合（メソッド・演算子スロットを含む）。
対象外: 名前に束縛されないインライン関数（if(c, {a}, {b}) の then/else、map({x | …}) 等の引数ブロック）、body 空のデータオブジェクト（結果型を持たない）。

規則 (2) 名前付き関数のパラメータ型を必須化

規則 (1) と同じ対象（名前に束縛された 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 を拒否する（規則 (1)）。位置ごとの許否は §3 冒頭の「暗黙・明示 Any の許可マトリクス」に要約する。

規則 (3) 宣言/推論された結果型を契約として越境利用

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

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

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

規則 (4) 分岐の結果型に収束を要求

§4 は if 分岐・match アームの結果型が割れた場合に合流結果を Any に倒して素通しする（通常モードの漸進的挙動）が、strict モードでは分岐が確実に割れるときエラーを報告する。規則 (1) の「暗黙 Any を結果型に許さない」を分岐合流まで広げたもので、参照言語（Haskell / Rust / F#）が分岐に同一型を要求するのと揃う。

対象: 完全適用された if cond {then} {else} の then/else サンク結果型、match subject { arms }（subjectful / subjectless 両形）の各 arm body（=> の右）末尾式型。部分適用（if (c) のみ等）や分岐構文でない呼び出しは対象外。when（片腕で false 側が Unit）/ while（戻り値が break(value) で任意化）は「分岐が割れた」のではなく構造的に Any になるため対象外。match で catch-all（_ => body）が無いときの実行時 Unit フォールスルーは見ない（明示 arm body 同士だけを比較する）。
関数結果の合流も対象（`return` / `?` bail）: §2 のとおり関数結果型は末尾式の fall-through 値と本体中の各 return e 引数型（および ? の失敗 bail 型。language-spec.md §16.5）を join して解く。? の失敗 bail が寄与するのは失敗 variant 型（脱出する値は Err / None で成功 payload を持たないため、Result は Err(E)〔成功要素は未制約〕、Option は None）。すなわち bail の成功 payload 型は関数の成功型を制約しない（Rust の ? と同じく Err の E だけが関数結果へ流れる）。これにより Ok 型の異なる逐次 ?（§16.5 の process 例）も末尾値と収束する。strict はこの合流位置にも収束判定を掛け、確実に割れる脱出経路を報告する（同一関数で 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 に属しうるため割れと断じない（合流結果は §4 のとおり同一 enum なら親 enum 型に持ち上がり、そうでなければ Any。後者は型エラーではない）。record 同士も幅構造型で共通の幅型を持ちうるため整合扱い。親 `enum` 型とその所属タグの対も整合扱い（タグ値は親 enum 型の値なので割れではない）。双方の所属 enum 名が判明して食い違うときだけ確実な非整合として報告する。
推論精度は変えない: 判定は分岐収束の診断専用で、§4 の join の精度は変えない。strict は収束診断を上乗せするだけで、合流型自体は引き続き Any に倒す。

規則 (5) closed variant の `match` に網羅性を要求

§2 と language-spec.md §16.4 は「網羅性は静的に保証しない」（受け手が未知 kind 用 default 分岐を持つ慣習）が、strict モードでは match subject { arms } のスクルティニ型が closed variant に確定し、覆われないタグが確実に存在し、catch-all が無いとき被覆漏れを報告する。非網羅 match は実行時に panic せず ()（unit）にフォールスルーする（prelude.md §8.4）ため §2 の「到達すれば確実に panic」には乗らず、規則 (4) と同じ strict が上乗せする収束系の診断（参照言語 Haskell / Rust / F# の網羅性検査と揃う）。

ガード付き arm は網羅に貢献しない: pattern | guard => body はガードが実行時に偽になりうるため、そのパターンがあるタグを完全に覆っても覆ったとみなさない（Rust ほか主流と同じ）。全タグ列挙でもいずれかがガード付きなら網羅未達。subjectless match（arm 頭が 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 が紛れる等）、タグ名が同じでも被覆に数えない。この場合は保守側に倒すのではなく、被覆しないと確定した上で網羅性判定を続行する（他に当該タグを覆う arm が無ければ通常どおり非網羅を報告）。

入れ子サブパターンの被覆（行列 usefulness による判定）: payload に自明でないサブパターン（入れ子の値コンストラクタ・素の値・レコード等）を持つ Tag(…) はそのタグを部分的にしか覆わない（Ok(Some(x)) は Ok(None) を覆わない）。判定は Maranget 流の行列 usefulness（各アームのパターンを列ベクトルとする行列を、先頭列の型で特殊化 / default 分解しながら再帰する witness 生成）で行う。あるタグへ特殊化するとその payload 型列が新たな列として展開され、位置間の相関を保ったまま（各 payload 位置を joint に）被覆を判定する。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(_))。無限型位置は _ で描画）。

健全性: witness 生成は「網羅なら witness を出さない」を保証する。ある位置でタグ 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(_) 欠落として非網羅になる。
入れ子位置の修飾タグも所属 `enum` を照合: 上記「修飾形は所属 enum の一致を要する」は payload 位置にも及ぶ。行列の各列は型を持ち回るため、入れ子の修飾タグ（Ok(Auth.None)）も列の型（Ok の payload 型）の所属 enum と照合し、異なる enum の同名タグは被覆に数えない。受信者を enum 型値へ解決できない修飾形は従来どおり保守側で被覆扱い。

catch-all: _ => body または Any 型パターンがあれば常に網羅とみなす。
素通し条件: スクルティニ型が closed variant に確定しないとき（Unknown / Any / 型変数 / 非 Variant を含む OneOf / 展開不能な遅延型適用）は報告しない。再帰ジェネリック enum の遅延型適用（§2.2）は判定時に 1 段ずつ展開して closed variant として扱う。また「特定タグの被覆」とも catch-all とも分類できないパターン（一般のレコードパターン・素値パターン・型パターン等）が 1 つでも混じる場合は保守側で報告しない。これにより Option / Result / enum のタグだけで構成された明快な match に限って網羅性を強制する。
「Option を T の所で未開封使用」は §2 で既出: 未開封の Option(T) / Result(T) を要素 T が要る位置（型注釈つき束縛・型付き関数引数・タプル/record 分解）に置く誤りは、§2 の照合が通常モードで既に検出する（x: Int := Some(1) は型不一致）。本規則（網羅性）の対象外。

規則 (6) closed variant の `match` で到達しえない arm・冗長な catch-all を報告

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

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

規則 (7) inner-name 型と slot/結果型の整合

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

結果型の照合は body 末尾アスクリプションだけでなく、宣言が無いときの本体推論結果（§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 型は引き続き実行時に評価されないため、それらの矛盾は規則 (4)〜(6) と同じく strict が上乗せする契約系の診断にとどまる（将来 inner-name のパラメータ型・record 型を値の構造照合に用いる段階〔language-spec-future.md〕が入れば実行時にも現れうる）。

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

規則 (8) 関数型注釈と実体シグネチャの整合

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

根拠と穴: language-spec.md §17.4 の実行時照合（funcSignatureMatches）は、関数値が結果型注釈を宣言しないとき結果照合を素通しする。そのため無注釈結果の関数（bad := {n: Int | "s"}）を関数型注釈 {Int | Int} に束縛・引数渡ししても束縛地点では panic せず、後続の値使用（bad(…) の結果を Int として使う箇所）で初めて panic する。strict はこの実体シグネチャの非整合を実行前に報告して塞ぐ。
通常モード不変: 本規則は strict 専用。束縛地点で即 panic しない照合を通常モードの assignable（「到達すれば確実に panic」枠）に足すと誤検出になるため、規則 (4)〜(7) と同種の strict 契約診断として上乗せする。
素通し条件: シグネチャが静的に確定しない（無注釈スロット・結果型が推論不能）位置・位置スロット混在・arity 不一致・Any/型変数/Unknown が絡む対。渡す関数が無名または結果型省略で該当位置が Any になり静的に拒否できないケースは、関数型の呼出時強制（language-spec.md §17.4・language-spec-future.md）が実行時 backstop。

規則 (9) 可変ローカルの型安定性

strict モードは、可変ローカル x（body 内の = 束縛）が既に確定した具体型 T を持つとき、再代入 x = v の v の静的型が T と確実に非整合（gradual consistent）なら報告する。x = 0（Int 確立）のあと x = "a" を型変更として検出し、注釈付き確立 x: Int = 0 のあとの無注釈 x = "a" も同様に塞ぐ（Rust の let mut / F# の型安定な可変束縛と揃える）。

健全性の位置づけ: 型変更再代入は実行時に panic しない（language-spec.md §6.1 のとおり = は再束縛で許容）ため、本規則は class b 健全性を超えた方針上の規律。規則 (4)〜(8) と同種の strict 契約診断として上乗せし、通常モードの意味論・診断は不変。
確立 vs 再代入: x が未束縛・型なし（前方参照プレースホルダ）・既存型 Unknown のときは確立とみなし検査せず記録する。以降の = が検査対象。違反を報告したうえで下流検査のため新しい右辺型を記録する（実行時挙動に合わせる）。
スコープ探索: 型安定性は方針検査なので、クロージャが捕捉した外側可変ローカルへの型変更再代入も違反として報告する（forwardOnly を読み飛ばすフル scope 探索 lookupValue）。これは §2.12 の分岐合流（同一フレーム限定）とは別軸。既確立の具体型を持つ可変スロット（{x = 0 | …}）の body 内 = 再代入も同様に検査する。
素通し条件: 既存型か右辺型のいずれかが未確定（Any・Unknown・型変数）。実束縛がまだ無い（確立）ときも素通し。

規則 (10) Future payload の照合

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

strict 限定の根拠: 実行時照合（language-spec.md §17.4）は Future を payload-blind で照合する（await 前は payload が存在しないため Future か否かのみ）。ゆえに x: Future(String) := fork({42}) は束縛地点で panic せず、通常モードで報告すると誤検出になる。Option/Result は実行時に payload を照合するため通常モードでも payload 照合が健全（§17.4）だが、Future はできない。strict は規則 (8) と同様「束縛地点で即 panic しないが後続の await 使用で確実に panic する非整合」を実行前に塞ぐ契約診断としてこれを行う。
誤検出ゼロ: consistent が確実に非整合の対のみ報告。payload 型が静的に不明な Future（無型ソース由来）は素通し。通常モードは完全に不変。

規則 (11) 封印契約に対する契約外アクセス（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 in strict mode を報告する。

中置メソッド呼び出し形（並置 dispatch recv name / recv name(args)）にも同じ規則を適用する（§2.3 と同一の並置規則）。

§2.3 との関係: 本規則は §2.3「存在しないメソッド／スロット」の対象を封印契約型の受信者へ広げたものであり、判定語彙・報告文言は共通（no such slot or method: name）。異なるのは強制レベルだけ — 封印契約型の契約外スロットは Stage 1 の実行時には値に物理的に残るため、§2.3 の対象（原始スカラー・variant・enum・std: 不透明型・閉じたリテラル・import 先モジュール）のように「到達すれば確実に panic」とは言えない。ランタイム backstop が無いぶん、本規則は --strict の契約系診断（本節）に置き、報告文言に in strict mode を含めて通常モードの §2.3 診断と区別する。
素通し条件: 受信者の静的型が Any・型不明・封印契約でない一般の record（幅構造型。language-spec.md §2.4）・open object・関数に確定するとき。(x: Any).name のように `Any` を経由した契約外アクセスも同様に素通しする（Stage 2 の実行時封印まで塞がない設計上の穴。language-spec-future.md §20）。

規則 (12) 封印契約の契約外・未使用スロット（定義側）

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

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

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

契約 T の閉じたメンバ集合（§17.6）に無い（契約外）。
定義ファイル内で参照 0（値読み出しをカウント。束縛名・スロット名・代入先は数えない。lint.md の unused と同じ数え方）。ただしローカル束縛用の unused と異なり、スロットは obj.slot という外部 API の形でも読まれ得るため、recv.name のドット越し読み出しも（受信者の型を問わず保守的に）参照として数える。誤検出ゼロを優先する結果として、この一部が見逃し（本来報告すべき未使用スロットの不検出）につながることは許容する。

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

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

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

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

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

規則 (13) 暗黙的 Any を含む束縛を禁止（型注釈を要求）

規則 (1)(2) が関数シグネチャの暗黙 Any を禁じるのと同じ思想を値束縛へ広げる。strict モードは、型注釈の無い束縛の推論型がコンテナ／payload のネスト位置に `Any`（gradual top）を含むとき、binding '<name>' requires an explicit type in strict mode を報告する。型注釈（hdrs: List(String) := extensible[]）で要素型を確定させれば解消する。参照言語（Haskell / Rust / F#）が空コンテナに要素型の推論／注釈を要求するのと揃う。

extensible[]（空 open object、language-spec.md §2.4）は要素型が確定せず List(Any) に推論され、以後の push や要素読み出しで Any が伝播する。これを実行前に塞ぎ、書き手に要素型の明示を促す。

対象: 型注釈の無い束縛 — := 宣言（トップレベル／ローカル）、可変 = の確立（未束縛からの初回代入。再代入は規則 (9) が担当）、名前／位置の分解束縛の各要素。
判定 `containsImplicitAny`: 束縛型を再帰的に辿り、次のネスト位置に Any が現れれば真とする — List / Option / Future の要素、Result の成功型、Tuple の各要素、Record の各フィールド、enum 適用（TypeApp / TypeVariant）の型引数、OneOf の各 alt。Any（gradual top）に到達したら真。
見ない位置（誤検出ゼロ）:

関数型（Func）: パラメータ・結果型は規則 (1)〜(3) の管轄のため辿らない（結果型の暗黙 Any は規則 (1) が検査する）。
`Result` のエラー型 `E`: Ok(5) は Result(Int)（E は未制約既定 Error、§4.4）で、E の未制約は don't-care のため辿らない。これにより Ok(5) を誤検出しない。
bare な top-level `Any` 単体: 分岐割れ由来の Any は規則 (4)、インライン : Any は明示 opt-in（規則 (2)）が既に管轄するため、束縛型そのものが Any に等しいだけのケースは本規則の対象外（二重報告を避ける）。ネスト位置に Any を含むときのみ報告する。
Unknown（型不明）: 静的に型を確定できない束縛（無型関数の呼び出し結果など）は Unknown で素通しする（§2.16）。

捕捉例: hdrs := extensible[] / xs := []（List(Any)）、x := None（Option(Any)）、x := Err("e")（Result(Any, String) の成功型）、(a, b) := (None, 5) の a、x := { items := [] |}（Record の List(Any) フィールド）。
非捕捉例: Some(5)（Option(Int)）、Ok(5)（Result(Int)）、extensible[1, 2]（List(Int)）、無型関数の呼び出し結果（Unknown）、関数値（規則 (1)〜(3)）、_ 破棄束縛、型注釈付き束縛。
健全性の位置づけ: 暗黙 Any コンテナは実行時に panic せず（Any 境界には実行時照合の backstop がある）、本規則は class b 健全性を超えた方針上の規律である。規則 (1)(2) の「暗黙 Any を書かせない」を値束縛へ広げた strict 専用診断で、通常モードの意味論・診断は不変。
対象外（見送り）: object リテラル内の slot デフォルト（{ items := [] |} を直接引数へ渡す等、名前束縛を経由しない位置）。無注釈の外側束縛は本規則が Record フィールド再帰で束縛レベルで捕捉し、アスクリプション付き（{...}: T）はフィールド型が契約から確定するため、slot デフォルト単体の追加検査は冗長かつ誤検出の恐れがある。

値位置 undefined 参照の strict 検出

§1/§2 は「値位置の未定義参照は実行時 panic のまま」（型注釈位置の未定義型名のみ §2.2 で静的検出）とするが、strict モードは値位置の識別子参照でどのスコープ（prelude・トップレベル・ローカル・destructure 束縛・import member・inner-name・型変数）にも束縛が無いものを undefined: <name> として報告する（到達すれば確実に language-spec.md §16.2 の undefined panic）。破棄子 _・型コンテキストの bare 小文字（型変数、language-spec.md §17.2）は対象外。スコープ模型で束縛の有無を確実に判定できないケース（判定不能な前方参照・動的 import 越境など）は素通しする。通常モードは従来どおり実行時 panic のまま。

strict の適用範囲

strict 型検査は hikari <path> --strict / hikari check --strict / hikari build --strict / hikari lsp --strict で適用する。いずれも実効 strict はファイル単位で決まり「CLI --strict」OR「entry header の strict 属性」（language-spec.md §13.1）の論理和（hikari-command.md §5.5・check.md「strict 型検査」）。通常モード（フラグ無し・header に strict 無し）の hikari <path> / hikari build は本モードを適用せず、実行時照合を backstop とする（§2 末）。

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

組込関数（if など）と一部の原始型メソッド（map / filter / first / last / fold / unwrap など）は、結果型が引数やレシーバの要素型に依存する多相な型を持つ。静的型検査はこれらの結果型を「型変数」と「単一化」で推論する。

4.1 単一化の基本方針

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

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

境界付き型変数（[language-spec.md](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/型変数は「不明」として素通しする。

いずれも当該実引数の型が静的に確定しているときだけ報告する（Unknown / Any / 未解決を含む場合は素通し）。実行時単一化（language-spec.md §17.2）が backstop。

4.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（従来 Any に倒れていた）。
if (c) { v } { return d } の結果型は v の型に解ける（従来は Unknown で型が付かなかった）。return(v) の引数 v の型は別途関数結果型の収束へ寄与する（§18.2 の return、§16.5 の ?）。
gradual 整合性 consistent（規則 (4)）でも Never は Any・型変数と同じく全型と整合する wildcard で、発散アームは分岐の割れと断じない。
代入照合では Never 値（actual）は任意の宣言型に代入可（Never <: ∀T）。逆に宣言型が Never で値が確定した非 Never 具体型なら確実な不一致として報告する（「返らないと表明した位置が値を返す」）。

4.4 分岐合成 `join`（gradual meet）

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

同種のジェネリックコンテナ（List / Option / Result / Future / Tuple）は要素ごとに再帰合流し、より精密な分岐へ寄せる — コンテナ内部では Any と Result の既定エラー（Elem2 を省いた Result(T) ≡ Result(T, Error) の未制約な E）を 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)。

同一 `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 に倒す。
トップレベル（コンテナの外）の Any は保つ — if (c) { 1 } { dynamic } は Any のまま（全体が動的な分岐を不用意に精密化しない）。合流できない異種・確実に割れるスカラー要素は Any に倒し、どちらかが Unknown なら Unknown。
同じ join を `if` / `when` / `match` の枝で再代入された可変ローカルの合流点併合にも使う（§2.12）。分岐の結果値だけでなく枝を跨ぐ可変ローカルの型も合流点で join し、割れれば Any に倒す。
例: if (c) { "a" } { "b" } → String。[1, 2].map({ x | x.to_char() }) → List(String)。if (c) { 1 } { "a" } → Any（通常モード。strict はこの分岐を規則 (4) でエラー報告するが合流型自体は Any のまま）。

4.5 `if` / `match` の結果型

`if` の結果型は then/else サンクの結果型の join で解く（match と同じ分岐合成）。if は組込関数だが curried 適用（((if cond) {then}) {else}）を汎用の単一化に通すと最初の分岐で多相結果が確定し、2 つ目の分岐が前者へ単一化されて相補的な variant 分岐（Ok / Err）が Any に倒れるため、match と揃えて専用に join で合流させる。どちらかのサンク結果が未解決なら Unknown 扱い。
`match` の結果型も同じ分岐合成で解く。各 arm pattern => body の body 末尾式型の join で、全 arm が同一の確定型ならその型、割れれば Any、1 つでも未解決なら Unknown。arm のパターンが束縛する名前（レコードパターンのスロット・値コンストラクタの payload）は body スコープへ型つきで束縛し、さらに末尾式より前のローカル束縛（`m := …` / `m = …`）を畳み込んでから末尾式を推論する。よって match x { Circle(r) => r … } のように payload を返す body も、Ok(data) => m := extensible[] … m のように局所束縛を返す body も解ける。例: match weekday { Sat => "weekend" Sun => "weekend" _ => "weekday" } は String。

subjectful でスクルティニが closed variant に網羅していると静的に確証できず（非網羅、または `List` 等）catch-all が無いときは、実行時の Unit フォールスルー（prelude.md §8.4）を含めて join(result, Unit) する（subjectless の Unit 算入と同じ健全側）。これにより非網羅 match の推論結果型が具体型に確定せず Any/Unit に倒れ、下流照合の backstop 領域へ移る。網羅と静的に確証できる closed variant match（全タグ被覆または catch-all あり）は具体型を保つ。
値コンストラクタ payload の型は、コンストラクタの結果型をスクルティニ（subject）の型と単一化して確定する — ユーザ定義 enum のタグだけでなく prelude の variant コンストラクタ（Some / Ok / Err）も対象。例: xs: Option(Int) を match xs { Some(x) => x, None => 0 } で受けると payload x は Int、結果型は Int。Result(T, E) の Ok(v) は v を T に、Err(e) は e を E に単一化する（既定の Result(Int) ≡ Result(Int, Error) では e は Error）。スクルティニ型が不明・単一化が不発なら宣言 payload 型のまま（解けない型変数は Any）。

subjectless `match` の結果型も同じ分岐合成。各 arm body 末尾式型の join で、全 arm 同型なら確定・割れれば Any・1 つでも未解決なら Unknown（アーム body 内の先行ローカル束縛も畳み込む）。ただし catch-all（`_ => body`）が無い subjectless match はどの述語も真でないとき実行時に Unit を返すため Unit も join に含める。例: grade := {n: Int | match { n >= 90 => "A" … _ => "F" }} は catch-all 有りで全 arm String のため String、_ を除くと String と Unit の join で Any。
同じ単一化はユーザ定義スロットの呼び出しにも使う。レシーバの静的型が record/object でフィールドが関数型のとき（util.repeat(s, n)・import 先モジュールの関数。§2.14/§2.15）、フィールドの関数型へ実引数を適用して結果型を解く。

5. 末尾位置マーキング（TCO）

評価器の末尾呼び出し最適化（language-spec.md §18.5）のため、各関数リテラル本体を走査し、末尾位置の self 完全適用呼び出しを静的にマークする。マークは型検査とは独立で、実行時のトランポリン（language-spec.md §18.5）が参照する。設計判断は ADR 0048。

このマーキングはパース直後の純粋パス（ast.MarkTailCalls、parser.ParseProgram が呼ぶ）として実装する。§2 / §4 の静的型検査は entry モジュールにしか走らないが、prelude（prelude.hikari）と import 先モジュールは別経路でパースされて評価器へ渡るため、全経路が通るパーサ直後に置くことで prelude の self-host ドライバ（stop_at 等）も一様にマークされる。パース後・評価前の単一スレッド実行なので fork との競合は無い。

末尾位置の判定は language-spec.md §18.5 の再帰的定義に従う。関数本体の最後の文の式を末尾位置とし、末尾位置の if / when / match の各分岐 body 末尾式・conduit / loop 本体末尾式へ伝播する（条件・subject・ガード・非末尾の文は末尾でない）。この位置集合は §2 / §4 が return 脱出経路の収集で走査する制御構文と同一で、末尾位置マーキングはその精緻化（結果へ流れる ∧ 以降評価が残らない ∧ self 完全適用）である。
self の同定: 呼び出しの callee が inner-name（inner 宣言。§4.2）を指し、完全適用（部分適用でない）である CallExpression をマークする。
健全性は保守側: 判定は unshadowed な標準制御構文（if / when / match と conduit / loop）を前提とし、判定できない構文（rebind・ユーザ定義の非透過高階関数）を通した位置はマークしない。過剰マークは避ける（マークは実行時に TailCall 制御値を末尾位置でのみ発行させるため、非末尾位置を誤ってマークすると制御値が値位置へ漏れる）。未マークはスタックにフォールバックするだけで結果は正しい（定数スタック保証を失うのみ）。この前提集合は §18.1 / §18.2 の透過が同じく標準制御構文を前提とするのと同一。
lint への再利用: 同じ末尾位置マーキングを hikari lint の non-tail-recur ルール（lint.md「ルール」）が再利用する。loop 関数の反復ドライバ（lexically 内側の inner-name 自己再帰）の self 完全適用のうち末尾マークが付かないものを「TCO が効かず深い反復でスタックを消費する」書き方の問題として警告する。トリガを loop に限るのは、非末尾の自己再帰が一般には正常（fact / fib 等）で一律警告が誤検出になるため（ADR 0048 D5）。