# bhc-typeck

Hindley-Milner type inference for the Basel Haskell Compiler.

## Overview

`bhc-typeck` implements type inference for HIR (High-level IR), producing typed HIR suitable for lowering to Core IR. Features:

- **Algorithm W**: Classic Hindley-Milner inference
- **Let-polymorphism**: Types generalized at let-bindings
- **Mutual recursion**: SCC-based binding group analysis
- **Type signatures**: Checked against inferred types
- **Error recovery**: Continues after errors using error types
- **M9 Shape inference**: Tensor dimension checking

## Core Types

| Type | Description |
|------|-------------|
| `TyCtxt` | Type checking context |
| `TypeEnv` | Type environment |
| `TypedModule` | Output with type annotations |
| `KindEnv` | Kind checking environment |

## Quick Start

```rust
use bhc_typeck::type_check_module;
use bhc_hir::Module;
use bhc_span::FileId;

let result = type_check_module(&hir_module, FileId::new(0));

match result {
    Ok(typed) => {
        // Access inferred types
        for (hir_id, ty) in &typed.expr_types {
            println!("{:?}: {}", hir_id, ty);
        }
    }
    Err(diagnostics) => {
        // Report type errors
        for diag in diagnostics {
            eprintln!("{}", diag.message);
        }
    }
}
```

## Type Checking Pipeline

```
HIR Module
    ↓
Register data types
    ↓
Compute binding groups (SCC)
    ↓
For each group:
    ↓
    ┌─────────────────────────┐
    │ Constraint generation   │
    │        ↓                │
    │ Unification            │
    │        ↓                │
    │ Generalization         │
    └─────────────────────────┘
    ↓
TypedModule
```

## TypedModule

The result of type checking:

```rust
pub struct TypedModule {
    /// Original HIR module
    pub hir: Module,

    /// Types for each expression (by HirId)
    pub expr_types: FxHashMap<HirId, Ty>,

    /// Type schemes for each definition (by DefId)
    pub def_schemes: FxHashMap<DefId, Scheme>,
}
```

## Binding Group Analysis

Mutually recursive bindings are grouped using SCCs:

```rust
// These form a binding group (mutually recursive)
// f x = g (x - 1)
// g y = if y == 0 then 1 else f y

let groups = binding_groups::compute_binding_groups(&items);

for group in groups {
    ctx.check_binding_group(&group);
}
```

### Monomorphism Restriction

Bindings without explicit signatures may be restricted:

```rust
// Generalized: has explicit type signature
id :: a -> a
id x = x

// May be restricted: no signature, uses overloaded operations
foo = (+) 1 2
```

## Constraint Generation

Type constraints are generated by walking the HIR:

```rust
// Expression: f x
// Generates: fresh t, constraint: type(f) ~ type(x) -> t

// Expression: \x -> e
// Generates: fresh a, check e with x:a, result: a -> type(e)

// Expression: let x = e1 in e2
// Generates: infer e1, generalize, check e2
```

### Constraint Types

```rust
enum Constraint {
    /// Two types must be equal
    Equal(Ty, Ty, Span),

    /// Type must be an instance of scheme
    Instance(Ty, Scheme, Span),

    /// Class constraint must be satisfied
    Class(Symbol, Vec<Ty>, Span),
}
```

## Unification

The unification algorithm solves constraints:

```rust
// unify(t1, t2) produces substitution S such that S(t1) = S(t2)

unify(Int, Int)                  // Ok(empty)
unify(a, Int)                    // Ok([a -> Int])
unify(a -> b, Int -> Bool)       // Ok([a -> Int, b -> Bool])
unify(Int, Bool)                 // Error: type mismatch
unify(a, [a])                    // Error: occurs check
```

### Occurs Check

Prevents infinite types:

```rust
// Cannot unify: a ~ [a]
// Would create infinite type: [[[[...]]]]
```

## Generalization

Types are generalized at let-bindings:

```rust
// let id = \x -> x
// Inferred: t0 -> t0
// Generalized: forall a. a -> a

fn generalize(ty: &Ty, env: &TypeEnv) -> Scheme {
    let free_in_ty = ty.free_vars();
    let free_in_env = env.free_vars();
    let quantified: Vec<_> = free_in_ty
        .into_iter()
        .filter(|v| !free_in_env.contains(v))
        .collect();
    Scheme::poly(quantified, ty.clone())
}
```

## Instantiation

Schemes are instantiated with fresh variables:

```rust
// instantiate(forall a. a -> a)
// Creates fresh t42
// Returns: t42 -> t42

fn instantiate(scheme: &Scheme) -> Ty {
    let fresh_vars: Vec<_> = scheme.vars
        .iter()
        .map(|_| fresh_ty_var())
        .collect();
    // Substitute bound vars with fresh vars
    apply_subst(&scheme.ty, &fresh_vars)
}
```

## Type Signatures

User signatures are checked:

```rust
// Source:
// foo :: Int -> Int
// foo x = x + 1

// Checking:
// 1. Infer type of RHS: Int -> Int
// 2. Check inferred is at least as general as declared
// 3. Use declared scheme
```

## Type Environment

```rust
pub struct TypeEnv {
    /// Variable types: x -> scheme
    vars: FxHashMap<Symbol, Scheme>,

    /// Data constructor types: Just -> forall a. a -> Maybe a
    constructors: FxHashMap<Symbol, DataConInfo>,

    /// Type constructor kinds: Maybe -> * -> *
    type_cons: FxHashMap<Symbol, Kind>,
}

impl TypeEnv {
    pub fn lookup(&self, name: Symbol) -> Option<&Scheme>;
    pub fn insert(&mut self, name: Symbol, scheme: Scheme);
    pub fn extend(&self, bindings: &[(Symbol, Scheme)]) -> TypeEnv;
}
```

## Kind Checking

Types are kind-checked:

```rust
// Maybe Int -- valid: Maybe :: * -> *, Int :: *
// Int Maybe -- invalid: Int :: *, can't apply to type

pub fn kind_check(ty: &Ty, env: &KindEnv) -> Result<Kind, KindError>;
```

## M9: Shape Inference

Tensor shapes are inferred and checked:

```rust
// matmul :: Tensor '[m, k] a -> Tensor '[k, n] a -> Tensor '[m, n] a
//
// x :: Tensor '[1024, 768] Float
// y :: Tensor '[768, 512] Float
// matmul x y :: Tensor '[1024, 512] Float

pub mod nat_solver {
    // Solve constraints like: m + n ~ 10, n ~ 3 => m = 7
    pub fn solve(constraints: &[NatConstraint]) -> Result<NatSubst, NatError>;
}
```

### Shape Mismatch Errors

```rust
// x :: Tensor '[3, 4] Float
// y :: Tensor '[5, 6] Float
// matmul x y
// Error: dimension mismatch, expected 4, found 5
```

## Type Families

Support for type-level computation:

```rust
pub mod type_families {
    // type family Add (m :: Nat) (n :: Nat) :: Nat
    // type instance Add 0 n = n
    // type instance Add (S m) n = S (Add m n)

    pub fn reduce_family(family: Symbol, args: &[Ty]) -> Option<Ty>;
}
```

## Error Reporting

Diagnostics with suggestions:

```rust
pub mod suggest {
    /// Suggest similar names for undefined variables
    pub fn similar_names(name: &str, env: &TypeEnv) -> Vec<String>;

    /// Suggest type annotations for ambiguous types
    pub fn type_annotation(ty: &Ty) -> Option<String>;
}

pub mod diagnostics {
    /// Create diagnostic for type mismatch
    pub fn type_mismatch(expected: &Ty, found: &Ty, span: Span) -> Diagnostic;

    /// Create diagnostic for undefined variable
    pub fn undefined_var(name: &str, span: Span, suggestions: &[String]) -> Diagnostic;
}
```

### Example Error

```
error[E0201]: type mismatch
 --> Main.hs:5:10
   |
 5 |   foo = "hello" + 1
   |         ^^^^^^^
   |         expected `Int`, found `String`
   |
 = note: `(+)` requires both arguments to be `Num`
```

## Built-in Types

Registered at startup:

```rust
impl TyCtxt {
    pub fn register_builtins(&mut self) {
        // Primitive types
        self.register_type("Int", Kind::Star);
        self.register_type("Float", Kind::Star);
        self.register_type("Double", Kind::Star);
        self.register_type("Char", Kind::Star);
        self.register_type("Bool", Kind::Star);

        // Type constructors
        self.register_type("Maybe", Kind::star_to_star());
        self.register_type("[]", Kind::star_to_star());
        self.register_type("IO", Kind::star_to_star());

        // Tensor (M9)
        self.register_type("Tensor", Kind::tensor_kind());
    }
}
```

## Pattern Type Checking

Patterns contribute bindings:

```rust
// case x of
//   Just y -> ...    -- y :: a when x :: Maybe a
//   Nothing -> ...

fn check_pattern(pat: &Pat, expected: &Ty) -> Vec<(Symbol, Ty)> {
    match pat {
        Pat::Var(name) => vec![(*name, expected.clone())],
        Pat::Con(con, pats) => {
            let (arg_tys, result_ty) = instantiate_con(con);
            unify(result_ty, expected);
            // Check sub-patterns
        }
        // ...
    }
}
```

## Performance Considerations

- Substitutions applied lazily where possible
- SCCs computed once per module
- Fresh variable IDs use atomic counter
- Error types prevent cascading errors

## Testing

```rust
#[test]
fn test_identity_type() {
    let module = parse_module("id x = x");
    let typed = type_check_module(&lower(&module), file_id).unwrap();

    // Should infer: forall a. a -> a
    let scheme = typed.def_schemes.get(&id_def).unwrap();
    assert_eq!(scheme.vars.len(), 1);
    assert!(matches!(&scheme.ty, Ty::Fun(_, _)));
}
```

## See Also

- `bhc-types`: Type representation
- `bhc-hir`: Input HIR
- `bhc-core`: Output (after lowering)
- `bhc-diagnostics`: Error reporting
