静的検査 (hikari check) 仕様

本書は hikari check の仕様を定める。起動ディスパッチ全体と終了コードの共通表は hikari-command.md、検査そのものの規則は static-analysis.md を参照。

指定した各 .hika を起点 (entry) に、評価せず 静的検査 (static-analysis.md §1) のみを実行する。entry とそこから到達可能なモジュールグラフ全体を構文検査し、結果に応じた終了コードを返す。CI や保存時フックでの利用を想定する。check / format / lint の住み分けは hikari-command.md §1.2。

構文

hikari check [--smt=z3] <path>...

引数は .hika ファイルまたはディレクトリを 1 個以上。ディレクトリは配下の .hika を再帰収集する (format (format.md) / lint (lint.md) と同じパス展開)。収集した各ファイルをそれぞれ entry として検査する。1 件の検査単位は到達可能なモジュールグラフ全体であり、lint の「ファイル単位・import 解決なし」とは異なる (hikari-command.md §1.2)。

オプション

検査内容

ファイル実行 (hikari-command.md §5) の開始前に走るものと同一の検査 (同じ analyze)。検出対象は static-analysis.md §1 を参照。

hikari check は構文・import 解決層 (前段) に加えて、静的型検査 (static-analysis.md §2) を行う。検査は 1 つで、水準を下げるフラグは持たない — hikari check が緑なら実行もできる、という対応を崩さないためである。規則はファイル実行 hikari <path> (hikari-command.md §5.5) と同じで、全実行系・LSP (lsp.md「起動」)・ビルド (build.md「静的型検査」) が同じ水準で検査する。診断・終了コードの形式は「出力と終了コード」のとおり (型エラーは exit 1)。

報告する診断は 2 つの根拠に分かれる (static-analysis.md §2.1)。どちらも誤検出を出さず、静的に確定しない箇所は素通しする (漸進的型付け)。

「到達すれば確実に panic」を根拠とするもの: 実行すれば確実に型不一致 panic になることが静的に確定する箇所を報告する。型注釈と値の照合・型注釈位置の未定義型名 (static-analysis.md §2.4)、存在しないメソッド／スロット・ブロックリテラルへの位置列メソッド・原始型メソッドの引数型 (同 §2.7)、演算子レベルの型不一致・関数でない値への適用・arity 超過 (同 §2.8)、値位置の未定義参照 (同 §2.13)、Future ブロック内の脱出 (同 §2.12) がこれにあたる。関数結果の越境照合 (再帰関数を含む。同 §2.2 / §2.6) と、条件に書いた matches による枝内の型の絞り込み (同 §2.3) は、これらの検出を呼び出し越しと分岐の枝の中まで広げる。

契約系のもの: 到達してもその地点では panic しないが、宣言された型・述語・網羅性という契約に反する箇所を実行前に塞ぐ。主なものは次のとおり。

• 名前付き関数の結果型の暗黙 Any を禁止: 名前に束縛された関数 (body 非空) で、結果型注釈を省略して本体推論がネスト位置に Any を含む (List(Any)・Result(Any)・record の Any フィールド等。bare な top-level Any は値束縛と同じく対象外) と型エラー。Any を意図する場合は束縛注釈 add: {Int, Int | Any} := …／内部名注釈 { inner self: {Int, Int | Any} | … } で明示すればオプトインとして許容し、body 末尾アスクリプション {x, y | expr: Any} の Any は禁止する (language-spec.md §17.3・許否は static-analysis.md §2.5 のマトリクス)。
• 名前付き関数のパラメーター型必須化: 名前に束縛された関数 (body 非空) の各パラメーター型が、インライン注釈・宣言関数型の対応位置 (非 Any)・推論可能なデフォルトのいずれでも確定しなければ型エラー。インライン x: Any は動的型へのオプトインとして充足する。bare パラメーターと関数型注釈位置の Any は充足とみなさない (static-analysis.md §2.5)。
• 宣言結果型を契約とした越境照合 (同 §2.6): 完全適用 f(args) の結果型を宣言から確定し、x: T := f(args) 等の照合に用いる。宣言結果型は末尾式だけでなく return / ? の全脱出経路とも照合する。
• 分岐の収束と網羅性 (同 §2.9): if/match の分岐結果型が確実に割れる場合、closed variant の match の被覆漏れ (非網羅)、および到達しえないアーム・冗長な catch-all (不要 default)。
• 可変状態の型安定性 (同 §2.10)・refinement 境界の証明義務 (同 §2.11)・Future payload の照合 (同 §2.12)。
• 多重度型の消費追跡 (同 §2.14): 多重度型 (language-spec.md §17.8) が課す契約の破れ。消費済みの値への出現・分岐での消費状態の割れ・ExactlyOnce の未消費がこれにあたる。多重度は実行時に何も照合しないため、この系統はすべて契約系である。

残る将来段階・対象外は static-analysis.md §2.16 を参照。

import 解決規則はファイル実行 (hikari-command.md §5.3) と同じ (caller ディレクトリ基準、OS filepath ベース)。各 entry は独立に検査するため、複数 entry が同じモジュールを import する場合そのモジュールは複数回検査される (診断は冪等)。

出力と終了コード

• 全 entry の検査がクリーンな場合は 何も出力せず exit code 0。
• 静的エラーがある場合は各診断を <file>:<line>:<col>: <msg> (<code>) 形式で stderr に出す。末尾の (<code>) は診断コードで、hikari lint と同じ体裁で添える。コードの一覧は static-analysis.md が定める。
• 複数 entry のときは全 entry を検査し、終了コードはそれらの最大値を返す (いずれかに静的エラーがあれば 1、いずれかの読み取りに失敗すれば 2)。