How other type checkers bound inference — prior art for Rigor's budgets

2026-06-03。調査ノート ── 参考情報であり規範的ではない。20260603-inference-budget-reality-survey.mdの姉妹編。Rigorの理想的なバジェット設計に関する計画中のADRの基盤。

なぜこの調査か

Rigorのinference-budgets.mdは設定可能なbudgets:テーブルを掲げているが、姉妹調査が示したのは、それが大半は配線されておらず、しかも大規模アプリで実際にコストを牽引するカテゴリー（union_size、structural_growth）こそが配線されていないものだということだった。何をどのデフォルト値で配線するかを設計する前に、本ノートは確立した6つのチェッカーが同じ問題をどう解決しているかを地図化する: 何が型推論を無制限に走らせたり使えない型を生成したりするのを防いでいるのか、そして上限に達したとき何が起きるのか。

2つの陣営

すべてのツールは2つのアーキテクチャ戦略のいずれかに属し、その選択が推論バジェットをそもそも必要とするかを決める。

陣営（a） ── 境界でシグネチャを要求し、ローカルにのみ推論する。推論は単一のメソッドボディ（およびフローセンシティブ（flow-sensitive）なナローイング（narrowing））に限定される。メソッド境界をまたぐと、型は宣言されたシグネチャを通じてのみ流れる。終了させるべき全プログラムの不動点が存在しないため、拡大／反復の機構は不要である ── 「バジェット」はシグネチャを書く人間が支払う。SorbetとSteepは純粋な陣営（a）。mypyは関数間の戻り値型について陣営（a）である（それらを決して推論しない）。

陣営（b） ── シグネチャ要求なしの全プログラム／深い推論。解析器はコールグラフをまたいで型を追跡するため、明示的な終了機構を課さなければならない。TypeProf、Pyright、TypeScript（型レベルで）、PHPStan／Psalm（値追跡）が陣営（b）である。

Rigorは戻り値推論について陣営（b）であり（シグネチャ要求なしでユーザーメソッドの戻り値を推論する ── 再帰ガードが存在するのはまさにこのためである）、陣営（a）の脱出ハッチ付きである。すなわち境界でのRBS／インラインRBS／生成シグネチャが深い推論を止める。そのハイブリッドが設計空間であり、本ノートの残りは陣営（b）のツールがどうバジェットを調整するかについてである。なぜならそこにRigorの未解決の問いが宿るからである。

2つのバジェットスタイル: カウンティングvs. 拡大

陣営（b）の内部にはバジェットを強制する2つの方法があり、ほとんどのツールはそれらを混在させる:

• カウンティングバジェット ── 作業量に対する数値的な上限（再帰深さ、インスタンス化回数、比較回数、配列キー数）。到達時にはエラーにするか、センチネルに退化させる。鋭く予測可能だが、その数値は恣意的でバージョンによってドリフトする。
• 拡大バジェット ── 型が閾値を超えて成長したとき、それをスーパータイプに一般化する（ユニオン → 共通の祖先、深い型 → untyped／any、形状付き配列 → 一般的な配列）。到達時には静かに精度を失うが、決してエラーにしない。単調なので、不動点の収束保証も兼ねる。

ツール別

Sorbet ── 陣営（a）、バジェット不要

メソッドシグネチャを決して推論しない（「Sorbetがコードベースを素早く型チェックできることの鍵となる部分」）。推論はメソッドボディにローカルである。sigの付いていない境界はパラメータと戻り値に対してT.untypedを返す。「あるメソッドの型チェックが別のメソッドに影響を与えることはできない」ため、すべてのメソッドが独立かつ並列にチェックされる ── 不動点が存在せず、したがってユニオンサイズや反復の上限もない。バジェットは必須のsigである。

Steep ── 陣営（a）、構造的終了

境界でRBSを消費し、ローカルに推論しつつボディ内でナローイングする。未宣言／untypedなRBSが吸収フォールバックである。# @type var x: Tは手動のローカルカットオフである。RBS自体が非正則な再帰型を禁止しており、シグネチャ層で一群の非終了な展開を取り除いている。チェッカーのコアにグローバルなタイムアウト／反復バジェットはない ── 終了は構造的である（有限の宣言型、メソッドごとのローカル解析）。

mypy ── 戻り値については陣営（a）、joinによる拡大

「戻り値型を決して推論せず、戻り値型注釈のない関数は戻り値型Anyを持つと仮定する。」これが関数間の作業を制限するハード境界である。その範囲内では、mypyは分岐の型を共通のスーパータイプへのjoinでマージする ── そのため2つの分岐のstrとintはobjectに推論され、ユニオンを破棄する。これは精度を犠牲にした拡大バジェット（単調 → 高速な不動点）である。メンテナーはjoinに起因する偽陽性の長いリストを追跡している（#12056）。数値的なユニオン／オーバーロード上限は表面化していない。再帰型エイリアスはmypy 0.990でデフォルトになり、深さの定数ではなく発散時の穏当な拒否で処理する。

Pyright ── 陣営（b）、カウンティングバジェット（密な側）

return／yieldから戻り値型を推論し（アグレッシブ）、その代償をtypeEvaluator.tsの十数個のハードコードされた数値上限で支払う: maxInferFunctionReturnRecursionCount = 12、maxReturnTypeInferenceStackSize = 2、maxRecursiveTypeAliasRecursionCount = 10、オーバーロード展開64 / 256、推論サンプリング16 / 64、フロー収束maxConvergenceAttemptLimit = 256（静かに最後の型を「ピン留め」する）、そして全関数のmaxCodeComplexity（約768、バージョンドリフトする。かつては1024）── これは唯一ユーザー向けのエラー「Code is too complex to analyze…」を発し、そのスコープのフロー解析を放棄する。それ以外はすべて静かにキャッシュされた／Unknownな型に退化する。ユニオン（精密）を使い、joinは決して使わない ── mypyの逆である。

TypeScript ── 陣営（b）、カウンティングバジェット（型レベル）

終了は注釈に関わらずハード定数によって保証される（checker.ts v5.4.5に対して検証済み）: インスタンス化depth = 100／count = 5,000,000（→ TS2589 errorType）、条件型tailCount = 1000（→ TS2589）、関係の再帰depth = 100（→ TS2321）、呼び出しごとの比較バジェット(16,000,000 − relation.size) >> 3、部分型簡約の作業チェックポイントが100,000（投影値が1,000,000を超えたら中断 → TS2590）、直積ユニオンsize ≥ 100,000（→ TS2590）。別個の余帰納的ガード（isDeeplyNestedType、maxDepth = 3）が関連すると仮定して、真の再帰型（リスト、ツリー）をエラーなく終了させる。明示的な戻り値注釈が推奨される脱出ハッチである（推論＋伝播の代わりにボディを注釈に対してチェックする）。バジェット超過のほとんどのケースは退化ではなくエラーにする ── 6つのうち到達時の姿勢が最も厳格である。

PHPStan／Psalm ── 陣営（b）、値追跡型の拡大

PHPStanはリテラル値を追跡するため、そのバジェットは値の精度を制限し、すべて静かに拡大する（決してエラーにしない）: 定数配列ARRAY_COUNT_LIMIT = 256（→ 一般的なarray<K,V>）、配列リテラル要素 > 256（→ 退化）、オフセット制約 > 32（→ OversizedArrayType、キーごとの追跡を停止）、ユニオン重複排除スイッチ > 16。教訓: PHPStanはかつてCONSTANT_SCALAR_UNION_THRESHOLD（コミュニティ報告で約8）を持ち、大きな定数スカラーユニオンをベース型に拡大していた。これを取り除いたことがメモリ不足のリグレッションを引き起こした（issue #5527 ── base64ルックアップテーブルが無制限のユニオンに爆発）。循環参照検出を逃れる再帰エイリアス／テンプレートは深さバジェットで制限されるのではなくバグとして扱われる。未宣言の再帰戻り値はmixedに底打ちする。Psalmは同じ配列／文字列バジェットをユーザー調整可能な設定として公開している（maxShapedArraySize = 100、maxStringLength = 1000バイト）── 調査の中でこれらを第一級の設定にしている唯一のツールであり、「これらを変更するとバグではなく望ましくない副作用が生じる可能性がある」という明示的な警告を伴う。

TypeProf ── 陣営（b）、拡大。Rigorに最も近い類似物

シグネチャ要求なしで推論する唯一のRubyツール ── 全プログラムの抽象解釈で、「Rubyを型レベルで抽象的に実行する」。untypedは「解析の限界により値を追跡できないときにTypeProfが生成する抽象値」である。その終了プリミティブ（type.rb／config.rb、v0.21.xより）:

• union_width_limit = 10 ── ユニオンがクラスインスタンスを10個以上累積すると、Union.createはそれらを単一の退化したインスタンスに潰す。
• type_depth_limit = 5 ── limit_size／globalize／substituteは深さが0に達するとType.anyを返すため、深くネストした／再帰的な型は深さ5でType.any（≈ untyped）に拡大する。
• max_iter／max_sec ── グローバルな不動点反復と実時間の上限（つまみは確認済み、デフォルト値は未確認）。

バジェット超過はuntypedに拡大し、決してエラーにしない。TypeProf v1は約3秒で非インクリメンタルだった。TypeProf 2はAST＋データフローグラフの書き直し（Tern／SpiderMonkeyの型推論をモデルにしている）で、不動点をインクリメンタルにする ── 編集すると変更されたメソッドのサブグラフのみを再計算する（自身の約7k LOCで全体約1.0秒／インクリメンタル約0.029秒）。拡大プリミティブはそのまま残る。勝ち取ったのは、実行ごとではなく編集ごとにバジェットを再消費することである。

Rigorのスペックデフォルトとの比較

関心事	Rigor（スペック／配線済み）	最も近い類似物
再帰／型深さ	recursion_depth 5／配線済み1	TypeProf type_depth_limit 5、Pyright戻り値再帰12、TSインスタンス化100
ユニオン幅	union_size 24（未配線）	TypeProf union_width_limit 10、PHPStanユニオン重複排除16、撤去されたスカラー上限 約8、TS直積100,000
構造的成長	structural_growth 16（未配線）	PHPStan配列キー256／ オフセット32、Psalm maxShapedArraySize 100
到達時の挙動	拡大 → Dynamic[top]、サイレント	拡大サイレント（mypy、TypeProf、PHPStan、Pyright大半）、エラー（TS、Pyright maxCodeComplexity）
境界の脱出ハッチ	RBS／ インラインRBS／sig-gen	TS明示的戻り値型、Sorbet／Steepの必須sig／RBS

ADRへの示唆

1. Rigorのアーキテクチャ（深い戻り値推論＋境界の脱出ハッチ）はTypeProfに最も近いため、TypeProfのunion_width_limit（10）とtype_depth_limit（5）が最も直接的に比較可能な先行事例であり ── 注目すべきことにRigorのスペックunion_size = 24より厳しい。これは24を信頼する前に測定すべきだという論拠になる。
2. エラーではなく拡大が、到達時の主流の挙動である。 6つのうち5つのツールがバジェットで静かに拡大する。日常的にエラーにするのはTSだけである。これはRigorのDynamic[top]退化を裏付ける ── ただし静かに拡大するすべてのツールは、その結果生じる不透明性で批判されている（mypyのjoin、Pyrightの「ピン」）。Rigorのスペックの答え ── カットオフでstatic.*の不完全推論診断を発する ── が差別化要因である: TypeProfのように拡大するが、他の誰もやらない形で、どこでそうしたかをユーザーに伝える。
3. 上限は荷重を支えている。取り除いてはいけないが、測定で設定する。 PHPStanの撤去されたスカラーユニオン上限 → OOMは、RigorのLayer 2への直接の警告である。ユニオン／構造の上限こそがRedmineの1.5 GBプロファイルを防ぐものであり、適切な値は推測ではなく観測された分布から来る。
4. Psalmは設定可能性のモデルである ── 2つの値精度バジェットを、「バグではなく副作用」という注意書き付きの文書化された設定として公開している。Rigorがbudgets:をユーザー調整可能にするなら（スペックが言うように）、Psalmの枠組み（およびPHPStanのハードコード定数という対照モデル）が設計選択を画定する。
5. 再帰ガードは深さ1での終了の下限として問題ない。 TypeProfはtype_depth_limitを5で走らせるがanyに拡大する（精度の主張はない）── これはまさにRigorの深さ1がDynamic[top]に拡大するのと同じである。Rigorの実効深さを上げることが意味を持つのは、精度を得るアンロールと組み合わせたときだけであり、それは陣営（b）のどのツールも一般再帰に対して試みていない。

ソースの信頼度

TypeScript（checker.ts v5.4.5）、PHPStan（TypeCombinator／ConstantArrayTypeBuilder）、Pyright（typeEvaluator.ts／codeFlowEngine.ts）、TypeProf（type.rb／config.rb v0.21.x）の数値定数はソースに裏付けられている。ソースエージェントが推測としてフラグした項目: mypyの数値上限の不在（明示的な記述ではなく、join拡大＋Any境界設計から論じた）、PHPStanの撤去された閾値の正確な値8（コミュニティ報告）、TypeProf max_iter／max_secのデフォルト値（つまみは確認済み、デフォルトは未確認）、TypeProf 2がv1の拡大定数を保持していること（アーキテクチャ的に整合的だが、v2のソースに対して再確認はしていない）。内部コンパイラ定数（TS／Pyright）はバージョン間でドリフトする ── 規範的に引用する前にコミットに固定すること。