Type Holes - Interactive Type Inference

Provides Idris-style type holes where you can write:

• ?hole - Named hole (e.g., ?returnType)
• _ - Anonymous hole

Features

1. Hover on hole - Shows inferred type
2. Code action - "Fill in hole with: List(Int)"
3. SMT-based inference - Uses type checker + constraint solving

Usage Examples

Return Type Hole

def double_list(numbers: List(Int)): ? =
    map(numbers, fn(x) -> x * 2 end)
    
% Hover shows: ?returnType :: List(Int)
% Code action: Fill in return type

Parameter Type Hole

def process(x: _): Int =
    x + 1
    
% Infers: x :: Int

Expression Type Hole

let result: ? = compute_value()
% Shows inferred type from compute_value

Implementation

Type holes are detected during parsing and marked in the AST. The LSP provides:

1. Diagnostics (info-level) for each hole
2. Hover information with inferred type
3. Code action to fill in the type