Module discharge 

Static discharge of refinement-type predicates (#209 slice 2).

Given a refined parameter type Int{x | x > 0} and a call-site argument 5, this module evaluates the predicate with the binding bound to the argument’s value and returns whether the call site satisfies, violates, or can’t statically decide the constraint.

Scope (deliberately small for v1):

• Argument shape: only CLit literals (Int, Float, Bool, Str). Anything else — variables, calls, arithmetic — defers to slice 3’s runtime residual check.
• Predicate shape: literals, the bound variable, binary arithmetic / comparison, boolean and / or with short-circuit, not. Anything else defers.
• Free variables: the predicate must reference only its binding. Other identifiers (balance, ceiling, etc.) defer — slice 2 doesn’t try to evaluate them. Slice 3 will plumb call-site context bindings.

The deliberate fall-through to “deferred” is what makes this slice ship-able: anything we can’t reason about cleanly stays a type-check pass and waits for slice 3’s runtime check, rather than blocking type-check on cases we can’t yet handle.

Enums

DischargeOutcome

Functions

try_discharge

Try to discharge predicate with binding_name bound to arg. arg is the CallExpr’s argument expression — only literal forms (CLit) participate in static discharge; anything else defers.