# 機能設計書 5-制約ソルバー

## 概要

本ドキュメントは、F#コンパイラの制約ソルバー機能の設計を記述する。制約ソルバーは、型推論における型制約を解決し、型変数に具体的な型を割り当てる機能である。

### 本機能の処理概要

制約ソルバーは、型チェック中に収集された型制約（型等式、サブタイプ関係、トレイト制約等）を解決し、すべての型変数に具体的な型を割り当てる。

**業務上の目的・背景**：F#の型推論では、式の型チェック時に型制約が収集され、これらの制約を統一アルゴリズムで解決する必要がある。制約ソルバーは、型等式（ty1 = ty2）、サブタイプ不等式（ty1 :> ty2）、トレイト制約（tyname: (static member op_Addition: 'a * 'b -> 'c)）などを処理し、解が存在すれば型変数を具体化する。解が存在しない場合は型エラーを報告する。

**機能の利用シーン**：型チェック中の型推論、メソッドオーバーロード解決、SRTP（静的解決型パラメータ）の解決で使用される。

**主要な処理内容**：
1. 型等式制約の解決（統一アルゴリズム）
2. サブタイプ制約の解決
3. トレイト制約（SRTP）の解決
4. 型変数の具体化
5. エラー発生時の診断情報生成

**関連システム・外部連携**：型チェック（CheckExpressions）、メソッド呼び出し解決（MethodCalls）と連携する。

**権限による制御**：特になし。

## 関連画面

| 画面No | 画面名 | 関連種別 | 関連する操作・処理 |
|--------|--------|----------|------------------|
| - | - | - | 制約ソルバーは直接的なUI画面を持たない |

## 機能種別

型制約解決処理

## 入力仕様

### 入力パラメータ

| パラメータ名 | 型 | 必須 | 説明 | バリデーション |
|-------------|-----|-----|------|---------------|
| csenv | ConstraintSolverEnv | Yes | 制約ソルバー環境 | 初期化済み |
| ty1 | TType | Yes | 型1 | 有効な型 |
| ty2 | TType | Yes | 型2 | 有効な型 |
| contextInfo | ContextInfo | No | コンテキスト情報 | - |

### 入力データソース

- 型チェックフェーズからの型制約

## 出力仕様

### 出力データ

| 項目名 | 型 | 説明 |
|--------|-----|------|
| 解決結果 | OperationResult | 成功または失敗（制約違反情報含む） |
| 型変数の具体化 | - | 型変数への型割り当て（副作用） |

### 出力先

- 型変数の更新（ミュータブル状態）
- エラー時は診断情報

## 処理フロー

### 処理シーケンス

```
1. 制約分類
   ├─ 型等式制約
   ├─ サブタイプ制約
   └─ トレイト制約

2. 型等式解決
   ├─ 型変数の展開
   ├─ 構造的統一
   └─ 出現チェック（循環検出）

3. サブタイプ解決
   ├─ 継承関係チェック
   └─ インターフェース実装チェック

4. トレイト解決
   ├─ メンバー検索
   ├─ オーバーロード解決
   └─ 静的メンバー解決

5. 結果統合
   └─ 型変数の具体化またはエラー報告
```

### フローチャート

```mermaid
flowchart TD
    A[型制約入力] --> B{制約種別}
    B -->|型等式| C[統一アルゴリズム]
    B -->|サブタイプ| D[継承チェック]
    B -->|トレイト| E[メンバー検索]
    C --> F{解決成功?}
    D --> F
    E --> F
    F -->|Yes| G[型変数具体化]
    F -->|No| H[エラー報告]
    G --> I[完了]
    H --> I
```

## ビジネスルール

### 業務ルール

| ルールNo | ルール名 | 内容 | 適用条件 |
|---------|---------|------|---------|
| BR-001 | 出現チェック | 型変数は自身を含む型に統一できない | 常時 |
| BR-002 | 剛性型変数 | 一部の型変数は統一不可 | ジェネリック定義時 |
| BR-003 | SRTP解決順序 | SRTPは定義済み順序で解決 | inline関数時 |
| BR-004 | アンドゥ | オーバーロード解決では一時的な統一を取り消し可能 | オーバーロード時 |

### 計算ロジック

統一アルゴリズムは、2つの型を等しくする最も一般的な代入（MGU: Most General Unifier）を計算する。型変数は型式にマッチし、具体型は構造が一致する場合のみ統一可能。

## データベース操作仕様

該当なし

## エラー処理

### エラーケース一覧

| エラーコード | エラー種別 | 発生条件 | 対処方法 |
|------------|----------|---------|---------|
| FS0001 | 型不一致 | 統一不可能な型 | 型注釈追加または式修正 |
| FS0043 | 型制約違反 | ジェネリック制約不満足 | 制約修正 |
| FS0071 | SRTP解決失敗 | 該当メンバー不在 | 型定義またはinline関数修正 |

### リトライ仕様

制約ソルバーはアンドゥ機能を持ち、オーバーロード解決時に一時的な統一を取り消して別の候補を試行できる。

## トランザクション仕様

該当なし（ただしアンドゥ機能あり）

## パフォーマンス要件

- 単一制約の解決は即座に完了
- 大量の制約でもO(n log n)程度の計算量

## セキュリティ考慮事項

特になし

## 備考

F#の制約ソルバーは.NETジェネリクスとSRTPの両方をサポートする高度な実装であり、メソッドオーバーロード解決とも密接に連携する。

---

## コードリーディングガイド

本機能を理解するために参照すべきファイルと、推奨する読み解き順序を以下に示す。

### 推奨読解順序

#### Step 1: データ構造を理解する

| 順序 | ファイル | パス | 読解ポイント |
|-----|---------|------|-------------|
| 1-1 | ConstraintSolver.fs | `src/Compiler/Checking/ConstraintSolver.fs` | ContextInfo、OverloadInformation等の定義 |

**読解のコツ**:
- ContextInfoは型エラーのコンテキスト情報（IF式、else分岐等）
- OverloadInformationはオーバーロード解決失敗時の情報

#### Step 2: 型変数操作を理解する

| 順序 | ファイル | パス | 読解ポイント |
|-----|---------|------|-------------|
| 2-1 | ConstraintSolver.fs | `src/Compiler/Checking/ConstraintSolver.fs` | NewCompGenTypar、FreshenTypar等の型変数生成 |

**主要処理フロー**:
- **83-129行目**: 型変数生成関数群
- NewCompGenTypar: コンパイラ生成型変数
- FreshenTypar: 型変数の新規化

#### Step 3: 統一アルゴリズムを理解する

| 順序 | ファイル | パス | 読解ポイント |
|-----|---------|------|-------------|
| 3-1 | ConstraintSolver.fs | `src/Compiler/Checking/ConstraintSolver.fs` | SolveTypeEqualsType等の統一関数 |

#### Step 4: トレイト解決を理解する

| 順序 | ファイル | パス | 読解ポイント |
|-----|---------|------|-------------|
| 4-1 | ConstraintSolver.fs | `src/Compiler/Checking/ConstraintSolver.fs` | SRTP解決ロジック |

### プログラム呼び出し階層図

```
ConstraintSolver
    │
    ├─ SolveTypeEqualsType（型等式解決）
    │      ├─ UnifyTypes
    │      └─ 出現チェック
    │
    ├─ SolveTypeSubsumesType（サブタイプ解決）
    │      ├─ CheckSubtype
    │      └─ 継承関係チェック
    │
    └─ SolveMemberConstraint（トレイト解決）
           ├─ FindMember
           └─ ResolveOverload
```

### データフロー図

```
[入力]                     [処理]                           [出力]

型制約             ──▶  制約分類                 ──▶  分類済み制約
(ty1 = ty2)                │
                           ▼
分類済み制約       ──▶  統一アルゴリズム         ──▶  型代入
                           │
                           ▼
型代入             ──▶  型変数具体化             ──▶  解決済み型
                                                    またはエラー
```

### 関連ファイル一覧

| ファイル | パス | 種別 | 役割 |
|---------|------|------|------|
| ConstraintSolver.fs | `src/Compiler/Checking/ConstraintSolver.fs` | ソース | 制約ソルバーメイン |
| TypeRelations.fs | `src/Compiler/Checking/TypeRelations.fs` | ソース | 型関係チェック |
| MethodCalls.fs | `src/Compiler/Checking/MethodCalls.fs` | ソース | メソッド呼び出し解決 |
| MethodOverrides.fs | `src/Compiler/Checking/MethodOverrides.fs` | ソース | メソッドオーバーライド |
| TypeHierarchy.fs | `src/Compiler/Checking/TypeHierarchy.fs` | ソース | 型階層 |
