mie 静的解析 (static analysis)

mie の静的解析は、評価を開始する前にソースを検査して問題を報告する仕組みをまとめる。構文層の一括検査 (§1) と、それに上乗せして実行前に型不一致を健全に検出する静的型検査 (§2)、その strict 拡張 (§3)、結果型推論の基盤となる単一化 (§4) から成る。

型注釈の文法・実行時照合は language-spec.md §17、エラーの三層モデルは同 §16 を前提とする。mie check / mie build / LSP など各コマンドの挙動は mie-command.md を参照。

1. 静的検査 (実行開始前の一括構文検査)

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

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

構文エラー: entry および import 先の各ファイルのパースエラー。動的 import — @import の引数が文字列リテラルでないもの (変数・文字列補間 "${...}"・bare 識別子・任意式) — もここに含まれ、パーサが弾く。リテラル限定によりモジュールグラフを実行前に静的確定できる。
import 先不在: @import リテラルが解決したパスにファイルが無い場合 (analyze で検出。これだけは構文層でなく解決層の検査)。language-spec.md §16.1 の「ファイル不在 = 回復可能エラー」は fs.read 等プログラムが明示的に行う I/O に適用される指針であり、モジュール解決には適用しない (Go / Rust / ES modules と同様、欠落モジュールはロード時の静的エラー)。
未知の標準ライブラリモジュール: @import "std:<name>" の <name> が std/index.md に存在しない場合 (analyze で検出)。import 先不在と同じく解決層の静的エラーであり、回復可能エラーにはしない。
third-party パッケージ解決の失敗: @import "pkg:<alias>" で、(a) その .mie を含むパッケージにマニフェストが無い、(b) <alias> がマニフェストの deps に無い、(c) 解決先がキャッシュに未取得、のいずれか (analyze で検出)。import 先不在と同じ解決層の静的エラーで、回復可能エラーにはしない。未取得 (c) は取得 (mie get) の実行を案内する。詳細は packages.md。

検出しないもの (従来どおり panic / 回復可能):

未定義参照・arity 不一致 → panic (language-spec.md §16.2)。型不一致も実行時 panic だが、mie check / LSP はこれに加えて「到達すれば確実に型不一致 panic になる」箇所を実行前に検出する健全な静的型検査を別レイヤで行う (§2)。確定しない箇所は素通しするため誤検出は出さない。
循環 import → 実行時に検出 (language-spec.md §13.4)。静的検査はグラフを 1 度だけ辿って終了し、循環自体は報告しない。

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

2. 静的型検査 (`mie check` / LSP)

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

検出する型不一致 (照合は language-spec.md §17.4 の表に従い、静的に判る型同士で行う):

型注釈つき束縛 x: T := v / x: T = v で、v の静的型が確定し T と確実に非互換。
型注釈つき分解 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 |}。
注釈位置に確実に型でない値が来る場合（追跡可能な範囲で）。
型注釈位置（束縛・スロット・分解・関数の結果型アスクリプション expr: T）に未定義の型名（スコープに束縛の無い大文字始まりの参照）または型になり得ない式（数値・文字列リテラル・演算子式など）が来る場合。到達すれば確実に実行時エラー（undefined: <name> / not a valid type expression）になるため報告する。スコープに束縛はあるが型と確定できない大文字名（型不明の値束縛など）は素通しする（実行時に評価され得るため未定義ではない）。小文字始まりの bare 名は型変数（language-spec.md §17.2）なので対象外。型注釈位置に限った例外であり、値位置の未定義参照は下記のとおり実行時 panic のまま。

存在しないメソッド／スロットの静的検出: recv.name（メンバ参照と型メソッド呼び出し recv.name(args) の両方）で、recv の静的型がメソッド集合の閉じた型に確定し、name がその型に解決できるどの名前（型メソッド・universal method matches / compare / inspect・演算子メソッド + ほか language-spec.md §8.1）にも該当しないとき、その箇所に到達すれば確実に実行時エラー（no such slot or method）になるため no such slot or method: name を報告する。同じ規則を中置メソッド呼び出し形（並置 dispatch recv name / recv name(args)、language-spec.md §8.1）にも適用する。recv の静的型が下記の閉じた型に確定し、並置される先頭の識別子（メソッド名）がその型に解決できないとき、recv.name と同じく到達すれば確実に実行時エラーになるため no such slot or method: name を報告する。閉じた型は関数ではないので実行時にこの並置はメソッド dispatch にしかならず、識別子のリテラル名がそのままメソッド名に使われる（値ではない）。素通し条件（Any・型不明・open object・関数・一般 record の受信者）は dot 形と同一で誤検出ゼロ。原始スカラー・variant・不透明型では実行時も同じ no such slot or method に落ちるが、閉じたリスト/タプルリテラルの並置は body-empty 関数への適用に帰着するため実行時の語句が別（undefined / スロット束縛不能）になりうる — いずれも同位置で確実にエラーになる点は変わらず、mie check は一律に no such slot or method として報告する。対象は値が後から slot を増やせない型に限る:

原始スカラー（Int / Float / Bool / String / Bytes / Range）と variant（Option / Result / Ordering）: 型から閉じたメソッド集合が一意に決まるため検査する。
enum 型値のタグ member（@enum Name := OneOf(Tag1(…), Tag2(…), …) で束縛された Name 自身。language-spec.md §17.4）: Name は宣言済みタグ名の集合を slot として持つ閉じた名前空間なので、Name.Tag の Tag 部が universal method にもいずれの宣言タグ名にも該当しなければ、到達すれば確実に実行時エラー（no such slot or method）になるため報告する（Color.Foo — Color に Foo タグが無ければ検出）。受信者が Name そのもの（enum 定義で束縛された名前、または immutable 別名連鎖）に帰着する場合に限る。prelude の Option / Result / Ordering も同じ機構で Option.Some 等のタグ member を持つ（上記の variant 検査とは別軸 — こちらは 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 の […] リスト・タプル (…)）に直接帰着する場合に限り検査する。変数・関数戻り値・注釈経由の List / Tuple 受信者は open object かもしれないため素通しする（誤検出ゼロ）。
import 先モジュール（相対 import mod := @import "path.mie" / third-party @import "pkg:…"）: import が返すファイルオブジェクトは closed（language-spec.md §13.1 — ファイルレベルの暗黙リテラルは closed で @ 適用不可、slot 生成はトップレベル slot-list 宣言時のみ）なので、一般の record（幅構造型）と異なりメンバ集合が静的に閉じる。受信者が import 式そのもの、または import 値を immutable 束縛した名前（別名連鎖 m2 := m1 も辿る）に帰着し、かつ import が解決でき record 型を組める（上記「import 先モジュールの型」）とき、name が import 先のトップレベル slot にも universal method にも該当しなければ報告する（mod.member(args) のメソッド呼び出し形も同様）。公開メンバは slot-list 領域の束縛のみで、body 領域の値束縛（name := expr）は最外側フレームのローカルで slot にならない（language-spec.md §13.1。0-pipe #{mie} は全体が body のため公開 slot 0 個 — mod.x は実行時に no such slot/method）。@enum は Name だけを公開メンバとして export する（language-spec.md §17.4 のとおりタグはフラット束縛せず Name の下に住むため）— @enum E := OneOf(A, B) を import したモジュールでは mod.E（型メンバ兼タグ名前空間）だけが解決し、各タグは mod.E.A / mod.E.B と連鎖して参照する（未知タグ mod.E.Foo の静的検出は上記「enum 型値のタグ member」と同じ規則）。素通し条件（誤検出ゼロ）: 循環 import・解決不能な import（既に Any）、mutable 束縛・関数引数/戻り値経由の import 値（closed 保証が切れる）。std: モジュールもメンバ集合が構造化シグネチャ（上記「import 先モジュールの型」）で閉じるため原理的には同様に検査でき、その不透明型（Instant 等）は既に本節の対象。std: 名前空間オブジェクト自体のメンバ検査は当面行わない（見逃しは許容）。
対象外: 一般の record（幅構造型 — 宣言に無いフィールドを持ちうるため、上記 import 先モジュールのような closed と確定する受信者を除く）・関数・open object・Any・型不明の受信者、および数値スロット（t.0）。

分解 import の未 export 名の静的検出: 名前分解 [a, b, …] := @import "…"（language-spec.md §6.3）で、右辺が解決済みの import 先モジュール（上記のとおり closed record）に帰着するとき、各分解名が import 先のトップレベル slot（値・型メンバとも。@enum は Name のみがトップレベル slot で、各タグは Name の下の member であり分解 import では直接引けない）に無ければ、その束縛は実行時に確実にエラー（no such slot）になるため報告する。これは 0-pipe の #{mie}（全体が body 領域＝公開 slot 0 個）を [x] := @import "script.mie" で受ける典型的な誤りを実行前に捕捉する。循環・解決不能な import は素通し（Any）。なお import 値を束縛せず副作用のみで使う形（@import "…" を文として置く・結果を _ で捨てる）は正当な利用であり報告しない。

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 なオブジェクト値に帰着するとき、実行時 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）。既存の mutable slot への = は正当（報告しない）。

「確実に closed」の範囲: language-spec.md §2.4 のとおり object の open / closed は実行時の値の性質であり、静的には一般に判定できない（注釈付き record パラメータ・戻り値・import 越境の値は @extensible（open）かもしれない）。そのため名前スロットの検査は受信者が次のいずれかに帰着する場合に限る: ① 非 @extensible なデータオブジェクトリテラル（{…|} / […]）に直接帰着、または ② それを immutable 束縛（:= / immutable slot） した名前（別名連鎖 b := a も辿る）。ブラケット形 […] も名前スロット name := / = expr の解釈は 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 越境は素通しする（誤検出ゼロ）。これは上記 List / Tuple のメソッド検査（閉じたリテラルにのみ働く）と同じ保守戦略。動的アクセスのキー recv.[k] は k が静的に定数と判るときだけ解決する（文字列/整数リテラル、またはそれらに immutable 束縛した名前）。非定数キーは素通しする。

演算子の型不一致の静的検出: 二項算術演算子 + / - / * / / / % で、両辺の静的型がともに原始スカラー（Int / Float / String / Bool / Bytes / Range）に確定し、その組合せが実行時に確実に演算子未定義の panicになるとき、その式に到達すれば確実に実行時エラー（operator '<op>' not defined for …、language-spec.md §7.1〜§7.2）になるため報告する。妥当な組合せは Int <op> Int（5 演算子すべて）・Float <op> Float（同）・String + String（+ のみ）に限り、それ以外の原始スカラー同士（混合 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 しない）は対象外。順序比較 < / <= / > / >= と短絡 && / || は下記で検出する。

順序比較の型不一致の静的検出: 順序比較演算子 < / <= / > / >= で、両辺の静的型がともに原始スカラーに確定し、その組合せが実行時に確実に panicになるとき、その式に到達すれば確実に実行時エラー（operator '<op>' not defined for …）になるため報告する。妥当な組合せは同型の 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 の妥当な組合せ（同型 Int/Float/String/Bool）以外は実行時に確実に panic する。暗黙の Int/Float 変換は行わない（language-spec.md §7.1）ため 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）・型変数・原始スカラー以外なら素通しする。

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

mutable ローカル (=): 直前の代入 (同一スコープの直線的フロー) の右辺型を採る。分岐合流やスコープチェーンを遡る更新 (language-spec.md §6.1) は追跡せず、その場合は最後に同一スコープで推論した型に留まる (健全側: 見逃しは許容するが誤検出は出さない)。右辺型が静的に不明な mutable ローカルは型不明とする。
式アスクリプション expr: T (language-spec.md §17 冒頭・§17.1): 内側式 expr の推論型に依らず注釈型 T を採る。アスクリプションは評価地点で T へ実照合され、一致しなければ確実に panic する (language-spec.md §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 に照合する」式アスクリプションになる (結果型宣言ではない)。
関数リテラルの結果型: 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.7)。全経路が同型ならその型に確定し、割れれば Any、1 つでも型不明なら Unknown とする (language-spec.md §16.6 のとおり if / when / while / cond などビルトインのブロック内 return は外側関数から脱出するため本体の脱出経路に含まれる)。脱出経路の収集は保守的だが、値として格納された関数リテラル (slot デフォルト name := {…}・:= / = 束縛の右辺に現れる {…}) の本体内 return は除外する — それらは構築時に実行されず、呼ばれたときにその関数自身の境界で取り出される (language-spec.md §16.6) ため外側関数の結果には寄与しないからである (除外は健全: 格納関数の body は外側の評価では走らない)。これにより {self | edit := {… return … |} … |} のように関数スロット (メソッド) を束ねたデータオブジェクトを返す関数の結果型が、メソッド内 return との join で Any に潰れず、その record 形に確定する。一方、ユーザ定義高階関数に引数として渡したブロック内の return (本来はそのブロックから脱出し当該関数の結果には寄与しない) はビルトイン制御構文のブロックと区別が付かないため依然含めるが、join は余分な型を Any に倒すだけで誤検出を生まない (過剰帰属側は健全)。例: {self | when (c) { return false }\ntrue} は return false と末尾 true がともに Bool で結果型 Bool。
代入族の文の値型: 束縛・代入 (:= / = / スロット代入 / 分解代入 / 複合代入) は文としての値型が Unit (language-spec.md §6.1)。したがって関数本体の末尾式が代入族の文なら結果型は Unit に確定し、右辺型が静的に不明でも Any に倒れない。これは束縛が変数の型を後続参照のために記録する動作 (上記 := / =) とは別軸 — 記録するのは変数の型、文自体の値型は Unit である。
データオブジェクトの record 型: body 無し・名前 slots のオブジェクトリテラル ({ x: T, y := e |}) は各 slot 型 (注釈→デフォルト推論→Any) から成る record 型に推論する。inner-name 付き ({self | x := e |}) でも値自身は同じ record 形 (slot から組むか、内部名注釈 {self: T | …} があれば T) に確定し、その内部名 self も同じ record 型で本体スコープへ束縛する。これにより inner-name オブジェクトを返す関数 (make := { initial | { self | … |} }) の結果型が具体 record に解け、Any へ倒れない。位置要素を持つデータオブジェクト ({| 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 単体) は素通しする (要素パラメータ側の位置に来る引数だけを、その CallExpression の Arguments 範囲に対応させてシードする)。反復メソッド自体の戻り型は §4 の単一化で解く。
record/object のフィールドアクセス recv.field: recv の静的型が record/object 型と判りそのフィールド field を持つとき、そのフィールド型を採る。フィールドが関数型で呼び出される (recv.field(args)) ときは §4 の単一化で結果型を解く (原始型メソッドではなくユーザ定義スロットの呼び出し)。record 型は幅構造型 (宣言フィールドは下限で、値は宣言に無いスロットを持ちうる。language-spec.md §2.4) なので、宣言に無いフィールドへのアクセスは型を静的に確定できず Any (gradual top) とする (@type Value := { tag: String |} の値で val.v を引く等)。
位置スロットアクセス recv.N (数値プロパティ) と整数キーの動的アクセス recv.[i] (language-spec.md §7.4 / §3.10): recv の静的型が要素型を一意に持つ列のとき、その要素型を採る — String の要素は長さ 1 の String、Bytes / Range の要素は Int、List(T) の要素は T。これらは添字に依らず要素型が一定なので、N / i が定数でなくても確定する (s.0 も s.[i] も同じ要素型)。Tuple は要素ごとに型が異なるため、添字が静的に定数の整数のときだけその位置の要素型を採る (非定数キーは不明)。動的アクセス recv.[k] のキー k が静的に Int と判らない場合は、List / object の名前スロットアクセスかもしれないため型不明とする (誤検出ゼロ)。これにより ch := s.0 のあと ch.code() → Int のように要素アクセスの連鎖が解ける。
import 先モジュールの型: いずれも record 型として扱い、mod.member(args) の戻り型まで §4 の単一化で解ける。循環 import・解決不能な import は型不明 (Any) に倒す。record 型の組み方は import の種類で分かれる:

相対 import (mod := @import "path.mie"): import 先ファイルのトップレベル slot 束縛から成る record 型 (各 slot 型は import 先を本規則で推論)。分解 import [a, b] := @import "..." も各名前を対応 slot 型で束縛する。
third-party (pkg:): pkg:<alias> は相手パッケージの入口 .mie に解決される (packages.md) ので、その入口ファイルから相対 import と同じく record 型を組む。未取得 (キャッシュ不在) は型不明 (Any)。
標準ライブラリ (std:): Go ネイティブ実装で .mie ソースを持たないため、処理系が保持する構造化型シグネチャ (std 各書のメンバ表に対応) から record 型を組む (例: t := @import "std:time" で t.of({…}) → Result(Instant)、(t.of({…})).unwrap! → Instant)。std:time が返す不透明型 Instant / Date / Time / Duration は名目型として推論語彙に加える。これらは std:time モジュールが export する型メンバー（§13 のモジュール型 export と同じ機構）であり、t := @import "std:time" のもとで t.Instant と修飾参照するか、[Instant] := @import "std:time" で名前を取り出して型注釈に書ける（例: x: t.Instant・mk: {Int | t.Duration}）。不透明性は保たれる — 参照できるのは名目型名だけで、内部表現（内包する int64）へのアクセスは依然コンストラクタとメソッド経由に限られ、@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 値。

Any (gradual top) の伝播: 受信者・被演算子が 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 だからである (§17 のアスクリプション「評価地点で T へ照合され到達すれば確実に T」と同型の漸進的精緻化)。これにより無型パラメータとの連結 ("note not found: " + id — id は Any) が String に解け、Err("…" + id) の payload 型が Any に倒れない。数値算術 (- * / % および両辺非 String の +) は引き続き Any を伝播する (Int + Any は Int+Int 以外 panic だが、漸進的挙動として Any のまま素通しする)。

確定できない式: 一般の関数呼び出しの結果・多相メソッド・(Any でない受信者で) フィールドを確定できないメンバアクセス・演算子の不明な組合せ・右辺型が静的に不明な mutable ローカルなどは型不明として扱い、不明が絡む照合は素通しする。

今回検出しない (将来段階、language-spec-future.md): 次は検出しない。

通常モードでのユーザ定義関数の呼び出し結果の越境照合 (関数の結果型は上記のとおり本体から推論するが、通常モードは呼び出し結果を型不明扱いで素通しする。strict モードは推論・宣言した結果型を使って越境照合する §3)。
分岐合流や呼び出し越境を伴う本体結果型の完全推論 (現状は本体末尾式に限るローカル推論)。
Future(T) の payload・inner-name 型。

値位置の未定義参照と arity 不一致は §1 のとおり実行時 panic のまま（型注釈位置の未定義型名のみ上記の例外として静的検出する）。通常モードの mie run / mie build には適用しない (実行時照合が backstop)。mie run --strict / mie check --strict は本検査に strict 規則を上乗せして適用する (§3)。

3. strict 型検査モード (`--strict`)

--strict を付けた mie <path> --strict (ファイル実行) と mie check --strict は、§2 の健全・漸進的な静的型検査に 6 つの追加規則 を上乗せした strict モードで検査する。mie <path> --strict は診断が 1 件でもあれば 評価せずに停止する (exit code は §1 / mie-command.md §5・§6 と同じ。0=クリーン、1=型/構文エラー)。フラグ無し (通常モード) の挙動は不変 — mie <path> は型検査せず実行し、mie check は §2 の検査のみを行う。

(1) 名前付き関数の結果型に明示 Any を禁止 (省略は許容): 名前に束縛された関数値 (body 非空の {…}) の結果型を language-spec.md §17.3 の 3 形 (束縛注釈／内部名注釈／body 末尾アスクリプション) のいずれかで明示する場合、その結果型を Any にしてはならない — Any は結果型を確定させない (規則 (2) の「Any 注釈は型を確定させない」と対称)。明示された Any 結果型には型エラーを報告する。結果型注釈を省略した場合は許容し、結果型は Any として扱う (呼び出し結果はそれ以上検査されず素通しする — 実行時意味と整合し誤検出ゼロ)。結果型が型変数の場合は Any ではないため許容する（充足）。

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

(2) 名前付き関数のパラメータ型を必須化: (1) と同じ対象 (名前に束縛された body 非空の関数) の各パラメータは、型が静的に確定しなければならない。確定する条件は次のいずれか — インライン注釈 x: T が付く／束縛注釈・内部名注釈で宣言した関数型の対応位置 (同インデックス) が Any でない具体型を与える／デフォルト式 x := <expr> の型が静的に推論できる。インライン注釈・関数型注釈位置・デフォルト式が型変数を与える場合も型は静的に確定したとみなし充足する（Any と異なり同一性を追跡できるため）。いずれでも確定しないパラメータには型エラーを報告する。これにより結果型だけ宣言してパラメータが無型の関数 (例: add := {self: {Int} | x, y | x + y}) や、関数型注釈位置で Any を与えたパラメータ (例: f: {Any | String} := {x | x} の x — 宣言関数型の対応位置が Any) も検出する。_ (捨て変数) パラメータと slot-list 内の @type/@enum スロットは対象外。

インライン : Any は動的型へのオプトイン: パラメータに明示したインライン注釈 x: Any は必須化を充足する (型エラーにしない)。真に動的な型付けを意図する場合のオプトインとして許す（多相な関数は型変数 x: a で書くことが推奨される。language-spec.md §17.2）。一方、無注釈の bare パラメータと関数型注釈位置の Any は「型を書き忘れた／確定させていない」扱いで充足とみなさず検出する (上記)。すなわち : Any の許否はインライン注釈位置に限った非対称であり、書き手が Any を明示的に選んだか否かで分ける。結果型の Any は (1) のとおり明示禁止・省略許容で、こちらと方向が異なる (パラメータは「型を書け、ただし動的なら : Any と明示せよ」、結果型は「省略すれば Any 推論、明示の Any は禁止」)。

(3) 宣言された／推論された結果型を契約として越境利用: §2 は関数呼び出しの結果を「型不明」として素通しするが、strict モードでは完全適用 f(args) の結果型を、language-spec.md §17.3 で宣言された結果型 (規則 (1) により明示は具体型または型変数に限られ、明示 Any は禁止される) か、宣言が無ければ本体末尾式から推論した結果型 (§2) から確定できる。これを使って x: T := f(args) (変数・分解束縛) の照合を行う (例: 結果型 String の関数を x: Int := f(…) に束縛 → 型エラー)。型変数を含む結果型は呼び出し位置で引数型に単一化して確定する（id(5) → Int）。結果型が宣言も推論もできない関数 (本体末尾が静的に不明・早期 return を含み末尾と return 経路の join が割れる等) の呼び出し結果は Any＝素通しのまま (越境照合しない、誤検出ゼロ)。早期 return を含んでも全経路が同型に join できれば §2 のとおり結果型が確定し、越境照合の対象になる。本体推論を越境に使えるのは strict 限定 — strict はパラメータ型を必須化し (規則 2) 呼び出し時に引数型を照合する (checkCall) ため本体スコープのパラメータ型が契約上確定する。通常モードはパラメータ型を保証しないため越境しない。

本体適合は best-effort: 関数本体の結果が宣言した結果型に適合するかは、本体の結果型が静的に確定するときだけ照合する (§2 と同じく確定しない箇所は素通し、誤検出ゼロ)。照合は束縛注釈・内部名注釈・body 末尾アスクリプションのいずれで宣言した結果型でも行う。宣言した関数型のパラメータ型は本体スコープへ伝播し、末尾式の型付けに使う — パラメータ型は契約上確定するため、f: {Int | String} := {x | x} の本体 x は Int と確定し宣言結果 String と非互換＝検出する (このパラメータ伝播は strict 限定。通常モードは実行時に arity のみ照合しパラメータ型を保証しないため伝播しない)。関数呼び出しの結果は規則 (3) のとおり宣言・本体推論した結果型で越境照合する。本体結果型の推論はローカル (本体末尾式に限る) に留まり、分岐合流や呼び出し越境を伴う完全な推論は将来段階。strict モードの健全性は「宣言された結果型 (契約) に対して誤検出を出さない」基準で保つ — 契約に反する本体の見逃し (false negative) は許容し、実行時照合 (language-spec.md §17 冒頭) を 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（=> の右）末尾式型。いずれも分岐の結果（選ばれた body の値）が合流する位置。部分適用 (if (c) のみ等) や分岐構文でない呼び出しは対象外。when (片腕で false 側が Unit) / while (戻り値が break(value) で任意化) は「分岐が割れた」のではなく構造的に Any になるため対象外。@match で catch-all (_ => body) が無いときの実行時 Unit フォールスルーは見ない (明示 arm body 同士だけを比較する — no-match と同じ保守側)。
関数結果の合流も対象 (return / ? bail): §2 のとおり関数結果型は末尾式の fall-through 値と本体中の各 return e 引数型 (および ? 演算子の失敗 bail 型。language-spec.md §16.7) を join して解く。? の失敗 bail が寄与するのは失敗 variant 型 — 脱出する値は Err / None であって成功 payload を持たないため、Result は Err(E) (成功要素は未制約)、Option は None (= 成功要素未制約の Option) を寄与する。すなわち bail の成功 payload 型は関数の成功型を制約しない (Rust の ? と同じく Err の E だけが関数結果へ流れる)。これにより Ok 型の異なる逐次 ? (read()? → parse()? で read の Result(String) と末尾の Result(Cfg)、§16.7 の process 例) も末尾値と収束する。strict モードはこの関数結果の合流位置にも収束判定を掛け、確実に割れる脱出経路をエラーとして報告する — 例: 同一関数で return None (Option) と return Err(…) (Result) を混ぜる、? を Result / Option 非返却の関数で使い末尾値と bail 型 (種別) が割れる。判定は下記 consistency と同一で、Option と Result は別種として非整合、Unknown / Any / 型変数は wildcard (誤検出ゼロ)。bail の成功要素を Any (gradual top) として寄与するため、種別 (Option vs Result、bail vs 末尾) の違いだけが収束判定に効き、成功 payload 型の違いは割れと断じない。
判定は 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 になる。後者は「共通 enum 型を表せない」だけで型エラーではない)。record 同士も幅構造型で共通の幅型を持ちうるため整合扱い。
判定は分岐収束の診断専用で、§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# の網羅性検査と揃う)。通常モードの @match セマンティクスと §2 の「健全・不完全・誤検出ゼロ」「漸進性」は不変。

ガード付き arm は網羅に貢献しない: pattern | guard => body の arm はガードが実行時に偽になりうるため、たとえそのパターンがあるタグを完全に覆っても、そのタグを覆ったとみなさない（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 形と等価に数える（destructure 済みで bare のアームと修飾アームが同一 @match に混在してもタグ単位で合算する）。OR (positional 複数列挙) は各 positional を見る。複数アームにまたがる被覆も合算する。

修飾形は所属 @enum の一致を要する: Name.Tag の Name がスクルティニと異なる @enum に解決できるとき（例: スクルティニが Color の match に Auth.None が紛れる）、タグ名が同じでも被覆に数えない。この場合は「列挙不能で保守側に倒す」のではなく、被覆しないと確定した上で網羅性判定を続行する — 他に当該タグを覆う arm が無ければ通常どおり非網羅を報告する。

入れ子サブパターンの被覆 (再帰判定): payload に自明でないサブパターン（入れ子の値コンストラクタ・素の値・レコード等）を持つ Tag(…) は、そのタグを部分的にしか覆わない（Ok(Some(x)) は Ok(None) を覆わない）。検査は当該 payload 位置の型を辿り、その位置に集めたサブパターン列を同じ網羅性判定で再帰して部分被覆を合算する。payload 位置が closed variant なら内側タグの被覆漏れを内側まで判定し、非 variant 位置（Int 等列挙できない型）は wildcard でのみ覆われるとみなす（保守側）。これにより Ok(Some(x)) => … / Ok(None) => … / Err(e) => … を網羅、Ok(Some(x)) => … / Err(e) => … を非網羅（Ok(None) 漏れ）と判定する。witness は欠落した値の形で示す（whole-tag 欠落は None / Some(_)、入れ子欠落は Ok(None) / Some(Some(_)) など）。

健全性（誤検出ゼロ）: ある payload 位置で「タグ T を覆う行（wildcard か tag T の値コンストラクタ）」が 1 つも無ければ、その位置に T を持つ値はどの行にも一致せず確実に未被覆なので、報告は常に正しい。複数アームにまたがる被覆も合算する（Some(0) => … / Some(x) => … は Some(x) の wildcard が Some を完全被覆 → None だけ報告）。
位置ごとに独立判定（見逃し許容）: 多 payload タグ（Rect(a, b) 等）は各 payload 位置を独立に判定するため、直積の隙間（[Rect(Some(x), 0) | …] [Rect(None, y) | …] が Rect(Some(_), 5) を漏らす類）は見逃す（false negative は許容、過剰報告は出さない）。完全な直積網羅（行列ベースの usefulness 判定）は将来段階。
入れ子位置の修飾タグは所属照合をしない（見逃し許容）: 上記「修飾形は所属 @enum の一致を要する」はトップレベルのスクルティニ位置に限る。payload 位置の修飾タグ（Ok(Auth.None) 等）はタグ名の一致だけで被覆に数え、所属 @enum までは照合しない — 異なる @enum の同名タグが入れ子位置に紛れても見逃す（false negative は許容、過剰報告は出さない）。

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

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

全値一致パターンより後ろの arm: 先行 arm が全値に一致する (Any 型パターン、型付き束縛 name: Any) と、それ以降の arm は到達しない (最初の一致で確定するため死 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 つ目、None => … None => … の 2 つ目)。
冗長な catch-all (不要 default): closed variant の全タグが catch-all 以外の arm で完全被覆されているとき、catch-all (_ => body または Any) は決して評価されない冗長 arm (Some(x) => … None => … _ => 0 の _ => 0)。網羅済みであることを規則 (5) と同じ完全被覆判定で確かめてから報告する。
健全性 (誤検出ゼロ): 「完全被覆」は payload を wildcard で覆う whole-tag 被覆に限って数えるため、規則 (5) の「位置ごと独立判定」が持つ直積の見逃しを引き込まない (入れ子の部分被覆だけで網羅が成り立つ場合は冗長と断じない＝見逃す)。列挙不能なパターン (素値・レコード・型パターン等) が紛れても、到達不能の根拠を「先行する全値一致」「2 つ目以降の default」「先行する whole-tag 被覆」に限るため過剰報告は生じない。スクルティニ型が closed variant に確定しないときは何も報告しない (規則 5 と同じ素通し条件)。

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

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

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

型変数は推論器の内部表現であり、ユーザは型コンテキストの bare 小文字で記述できる（language-spec.md §17.2）。記述された型変数は内部生成の型変数と同じ単一化・代入で扱う。
単一化は結果型を推論するためだけに使い、不一致を見つけても診断は出さない。分岐や引数の型が割れた場合は結果型を Any に、手がかりが無い場合は Unknown に倒す。この振る舞いは分岐合成（join）と同じで、新たな型エラーを生まない。
境界付き型変数（language-spec.md §17.2）だけは単一化の例外として診断を出す: 境界には閉じた union（type set 境界）と構造的 interface（interface 境界）の 2 種があり、いずれも呼び出しの単一化で違反が確実な呼び出しを通常モード（§2）で報告する。

① 同型分裂: 境界付き型変数が静的に確定した複数の型に割れる（sum(1, 2.0) — type set 境界 a: Number が Int と Float に割れる〔language-spec.md §17.2〕、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 の異なるタグ等、member が variant でも）は実行時に確実に割れるため従来どおり無条件に報告する。
② 非充足: type set 境界では確定型が境界のメンバーでない（math.abs("a") — String は Number のメンバーでない）とき、interface 境界では確定型が interface を確実に満たさない（describe(5) — describe := {x: a: Drawable | …} に対し Int は draw に応答するベースラインを持たず slot も生やせない）とき報告する。interface 境界の非充足判定は tri-state（満たす／満たさない／不明）で、record 型・function 型（mie は関数とオブジェクトを単一の {} 表現に統一するため body を持つ値も名前付きスロットを持ちうる）がエントリを静的に持たない場合や Any/Unknown/型変数は「不明」として素通しする（幅部分型・スロット不可視ゆえ実行時に slot を持ちうる）。
いずれも当該実引数の型が静的に確定しているときだけ報告する（Unknown / Any / 未解決を含む場合は素通し — 誤検出ゼロ維持）。実行時単一化（language-spec.md §17.2）が backstop。

多相メソッドの呼び出し形は paren / juxtaposition のどちらでも同じに扱う: recv.method(a, b) と recv.method a b (AST 上は ((recv.method a) b) の連鎖 CallExpression) を平坦化して同一の method call として単一化する。引数不足の場合は部分適用とみなし、残余 params を持つ関数型 (未解決の型変数は残したまま) を返す — これにより .fold "" のような単独の部分適用も後続の適用や curried 用法で正しく型付けされる (完全適用時にだけ未解決変数を Any に倒す)。
Never（ボトム型）の扱い: Never（language-spec.md §17.2、panic/exit の結果型や return/break/continue の式位置の型など発散位置の型）は全型の部分型で、join の恒等元として働く — join(T, Never) = join(Never, T) = T（トップレベル depth 0 を含む全深度）。これにより発散アームを含む分岐が他方の具体型へ精密に解ける: if (c) { 1 } { panic("x") } は Int（従来 Any に倒れていた）。return/break/continue（language-spec.md §16.5・§16.6 の発散する制御フロー）の式位置も Never で、if (c) { v } { return d } の結果型は v の型に解ける（従来は Unknown で型が付かなかった）。return(v) の引数 v の型は別途関数結果型の収束へ寄与する（§16.6 の return、§16.7 の ?）。gradual 整合性 consistent（§3 規則 4 の strict 分岐収束）でも Never は Any・型変数と同じく全型と整合する wildcard で、発散アームは分岐の割れと断じない。代入照合では Never 値（actual）は任意の宣言型に代入可（Never <: ∀T）。逆に宣言型が Never で値が確定した非 Never 具体型なら確実な不一致として報告する（「返らないと表明した位置が値を返す」）。
分岐合成 join は gradual meet: 完全一致ならその型。同種のジェネリックコンテナ（List / Option / Result / Future / Tuple）は要素ごとに再帰合流し、より精密な分岐へ寄せる — コンテナ内部では Any と Result の既定エラー（Elem2 を省いた Result(T) ≡ Result(T, Error) の未制約な E）を identity とみなし他方の確定型を採る。これにより相補的な variant 分岐が精密に解ける: 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。
例: if (c) { "a" } { "b" } の結果型は String。[1, 2].map({ x | x.to_char() }) は List(String)。分岐の型が割れる if (c) { 1 } { "a" } は Any (通常モード)。strict モードはこの「確実に割れる」分岐をエラーとして報告する (§3 規則 4)。合流型自体は strict でも Any のまま (診断を上乗せするだけで推論精度は変えない)。
if の結果型は then/else サンクの結果型の join で解く（@match と同じ分岐合成）。if は組込関数だが curried 適用（((if cond) {then}) {else}）を汎用の単一化に通すと最初の分岐で多相結果が確定し、2 つ目の分岐が前者へ単一化されて相補的な variant 分岐（Ok / Err）が Any に倒れるため、@match と揃えて専用に join で合流させる。どちらかのサンク結果が未解決なら Unknown 扱い（既存の単一化経路に委ねる）。
@match の結果型も同じ分岐合成で解く。@match subject { arms } の結果型は各 arm pattern => body の body 末尾式型の join で、全 arm が同一の確定型ならその型、型が割れれば Any、1 つでも未解決の arm があれば Unknown とする。arm のパターンが束縛する名前 (レコードパターンのスロット・値コンストラクタの payload) は body スコープへ型つきで束縛し、さらに末尾式より前のローカル束縛 (m := … / m = …) を畳み込んでから末尾式を推論する (関数本体の結果型推論と同じ。上述)。よって @match x { Circle(r) => r … } のように payload を返す body も、Ok(data) => m := @extensible[] … m のように局所束縛を返す body も解ける。例: label := @match weekday { Sat => "weekend" Sun => "weekend" _ => "weekday" } は label を String に推論する。

値コンストラクタ 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) は payload v を T に、Err(e) は payload e を E に単一化する — 例: r: Result(Int, ParseError) を @match r { Ok(v) => v, Err(e) => … } で受けると v は Int・e は ParseError に解ける (既定の Result(Int) ≡ Result(Int, Error) では e は Error)。スクルティニ型が不明・単一化が不発なら宣言 payload 型のまま (解けない型変数は Any に倒す)。

subjectless @match の結果型も同じ分岐合成で解く。@match { pred => body … } の結果型は各 arm body 末尾式型の join で、subjectful と同じく全 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)、フィールドの関数型へ実引数を適用して結果型を解く。

Any は言語の型（任意の値）であり、Unknown は「静的型を確定できなかった」という内部状態で型としては露出しない（hover に型が出ないだけ）。

5. 末尾位置マーキング (TCO)

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

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

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