LSP Code Actions & Quick Fixes

This module provides automated fixes and suggestions for constraint violations:

Quick Fix Categories

1. Add Runtime Checks

• Insert guard clauses: when x > 0
• Add assertions: assert x > 0
• Add conditional checks with error handling

2. Relax Constraints

• Suggest weaker constraints that would pass
• Example: x > 0 → x >= 0
• Offer alternative type signatures

3. Add Type Annotations

• Suggest refinement types based on usage
• Auto-infer constraints from guards
• Propagate constraints from callers

4. Pattern Completion

• Add missing pattern match cases
• Generate exhaustive match arms

Example Quick Fixes

Add Guard:

% Before
def divide(a: Int, b: Int): Int = a / b

% After
def divide(a: Int, b: Int) when b /= 0: Int = a / b

Relax Constraint:

% Error: Cannot prove Percentage <: Positive
type Percentage = Int when x >= 0 and x <= 100

% Suggested: Use NonNegative instead
type NonNegative = Int when x >= 0
def use_percentage(p: NonNegative): Int = ...

Add Runtime Check:

def process(n: Int): Result =
    if n > 0 then
        divide(100, n)
    else
        error(\"n must be positive\")
    end