AILang/design/contracts/0010-scope-boundaries.md

What is not (yet) supported

What is not (yet) supported

Snapshot of the current boundary.

• No effect handlers — only the built-in IO op (io/print_str); the effect system is described in effects. Diverge is a reserved effect name with no op and no codegen.
• No refinements / SMT escalation.
• No HM inference inside bodies. Top-level def types are explicit; polymorphism is opt-in via Type::Forall { vars, body } (see Data model). Inside a body, lambdas check monomorphically against their declared type.
• Polymorphic fns must be directly called at the use site. Passing a polymorphic fn as a value (let f = id in f(42)) is not yet supported.
• No higher-rank polymorphism. Passing a polymorphic fn to another polymorphic fn (apply(id, 42)) is not supported.
• No recursive let for non-fn values. Plain let x = … in … only sees x inside the body, not inside its own RHS — recursive value bindings would break the acyclicity invariant. Recursive fn bindings are supported via Term::LetRec ({ "t": "letrec", ... }); the desugar pass lifts most occurrences to a synthetic top-level fn, with lift_letrecs finishing the residue after typecheck (see pipeline).
• No visibility rules in imports. Every top-level def of an imported module is reachable; there is no pub / priv.

What is supported (and used as the smoke test for the pipeline):

• Int, Bool, Unit, Str, Float as primitive types.

• if, let, function calls, recursion.

• Effects on function signatures, with do op(args) for direct effect ops (io/print_str). The polymorphic print (see prelude classes) is the canonical output path for non-Str values.

• Builtins. Arithmetic operators (+, -, *, /) of type forall a. (a, a) -> a (codegen-restricted to {Int, Float}); % of type (Int, Int) -> Int (Int-only — fmod semantics for Float deferred); polymorphic neg : forall a. (a) -> a (codegen-restricted to {Int, Float}; Float arm uses LLVM fneg double for correct -0.0 handling); logical not : (Bool) -> Bool; conversions int_to_float : (Int) -> Float, float_to_int_truncate : (Float) -> Int (saturating, NaN → 0), float_to_str : (Float) -> Str, int_to_str : (Int) -> Str (both allocate a heap-Str slab at call time and return it with ret_mode: Own; see Str ABI for the dual heap-/static-Str realisation); inspection is_nan : (Float) -> Bool (LLVM fcmp uno); Float bit-pattern constants nan : Float, inf : Float, neg_inf : Float (resolved as bare values, lower to direct hex-float double SSA constants at use site); the IO effect op io/print_str; and __unreachable__ : forall a. a.

  • Equality + ordering are not builtins. The class method eq (prelude.Eq) dispatches via the per-type Eq instance; the class method compare (prelude.Ord) dispatches via the per-type Ord instance, returning a three-ctor Ordering ADT (LT / EQ / GT). The five free helpers ne / lt / le / gt / ge are defined in the prelude in terms of eq / compare. The primitive Eq/Ord instance bodies are emitted by the codegen intercept try_emit_primitive_instance_body: Eq Int → icmp eq i64, Eq Bool → icmp eq i1, Eq Str → call @ail_str_eq(...), Eq Unit → ret i1 1, Ord Int / Bool / Str → three-way icmp slt / icmp eq ladder constructing the Ordering ctor; every primitive instance body carries the alwaysinline attribute so the call folds at every use site. Float has no Eq / Ord instance (see Float semantics); explicit comparison is via the named fns float_eq / float_ne / float_lt / float_le / float_gt / float_ge, each lowering to a single fcmp with the matching predicate. float_ne uses fcmp une double (NOT one) so nan != nan returns true per IEEE.
  • __unreachable__ is a polymorphic bottom value: a use of __unreachable__ typechecks against any expected type at the use site and codegens to the LLVM unreachable instruction (UB if ever executed). It is the chain machinery's deepest fall-through for matches that the typechecker proved exhaustive, and it is available to user code as an explicit panic primitive ((if cond __unreachable__ ...) for assertions or impossible branches). Reference site is Term::Var { name = "__unreachable__" } / form-A bare __unreachable__.

• ADTs + pattern matching. Sub-patterns of a Ctor pattern may be Var, Wild, another Ctor, or a literal. The desugar pass flattens nested Ctor patterns into a chain of let + match and rewrites every Pattern::Lit (top-level or sub-) to a Term::If on eq (the class method prelude.Eq.eq) before typecheck/codegen — see desugar and Pipeline.

• Literal patterns at top level and inside Ctor sub-patterns (via desugar). (pat-lit 0) and (pat-ctor Cons (pat-lit 0) _) both parse and lower; the rewrite is to Term::If { cond = (eq sv lit) }, so any literal kind whose eq dispatch resolves to a known primitive Eq instance is authorable. The primitive instances cover Int / Bool / Str / Unit; Float lit-patterns are hard-rejected at typecheck (CheckError::FloatPatternNotAllowed, see float-semantics). (pat-lit "hi") over a Str scrutinee is exercised by examples/eq_demo.ail.

• Imports + qualified cross-module references via dotted names. Extends to types and constructors: a foreign module's ADT is referenced as (con std_pair.Pair a b), its ctors as (term-ctor std_pair.Pair MkPair x y) and (pat-ctor MkPair x y) inside that scrutinee. Std-library demos (examples/std_*_demo.ail) exercise this end-to-end.

• AI-authoring text surface, form (A) (see authoring surface). The ailang-surface crate parses .ail form-A text into a canonical ailang-core::ast::Module and prints any module back as form-A text. ail render and ail describe use it as the sole text projection; ail parse is the inverse direction. Round-trip identity (text → AST → JSON → AST → text) is gated by ailang-surface/tests/round_trip.rs over every shipped fixture.

• Memory management via reference counting + uniqueness inference (see RC + uniqueness), with per-fn arena via stack alloca for non-escaping allocations layered on top. Every ADT box, lambda env, and closure pair allocates either via @ailang_rc_alloc (escaping; RC-managed with inc/dec instrumentation per the memory model) or via LLVM alloca (non-escaping; freed at fn return). The decision is made by an escape-analysis pre-pass over the fn body — see the "Per-fn arena via stack alloca" subsection of RC + uniqueness. The per-fn-arena path is exercised end-to-end by examples/escape_local_demo.ail.

• First-class function references. A top-level fn name (or qualified prefix.def) used as a Term::Var is a fn-value.

• Anonymous lambdas with capture. Term::Lam constructs a closure that captures any free variables of its body from the enclosing scope. All fn-values share a single ABI: a ptr to a closure pair { thunk_ptr, env_ptr }. Top-level fns get an auto- generated adapter and a static closure pair (env = null) so they remain passable as values without heap overhead.

• Polymorphism via Type::Forall at top-level def types. Use sites instantiate fresh metavars; unification pins them against the concrete types of the call args. Codegen monomorphises on demand: each unique instantiation emits a specialised LLVM fn mangled @ail_<m>_<def>__<descriptor> (e.g. id__I for id at Int, apply__I_I for apply at (Int, Int)).

• Parameterised ADTs. TypeDef.vars: Vec<String> declares type parameters; Type::Con.args: Vec<Type> carries the type arguments at use sites. Both fields default to empty and are skipped during serialization, so canonical-JSON hashes of every existing definition stay bit-identical (regression test in crates/ailang-core/src/hash.rs). Ctor and match codegen stay inline at every use site — there is no specialised ADT symbol — but LLVM field types are derived per use site by substituting through cdef.ail_fields. The substitution is read off the call's arg types (ctor) or the scrutinee's Type::Con.args (match). An unresolved Type::Var reaching llvm_type is a hard error rather than a silent fallback to ptr. Pipeline regression smoke tests:

• examples/sum.ail → prints 55 (recursion, arithmetic).

• examples/list.ail → prints 42 (ADTs + match).

• examples/hof.ail → prints 42 (first-class fn-refs, indirect call).

• examples/closure.ail → prints 42 (lambda capturing a let-bound var).

• examples/list_map.ail → prints 2/4/6 (ADTs + closure + recursive HOF + IO; the dogfood smoke test).

• examples/sort.ail → prints sorted [3,1,4,1,5,9,2,6,5,3,5] one-per-line (insertion sort over an 11-element list).

• examples/poly_id.ail → prints 42 then "true" (polymorphic identity at Int and Bool; two specialised fns emitted).

• examples/poly_apply.ail → prints 42 (polymorphic apply with a fn-typed parameter; apply(succ, 41)).

• examples/box.ail → prints 42 (parameterised ADT round- trip: MkBox(42) constructed, then projected by a polymorphic unbox : forall a. (Box<a>) -> a and printed).

• examples/maybe_int.ail → prints 7 then 99 (pattern match over Maybe<Int>: or_else(Some(7), 99) then or_else(None, 99)).

• examples/std_list_demo.ail → exercises std_list's combinators (length, sum, reverse, take/drop-style uses) end-to-end against std_list's List<a>.

• examples/std_maybe_demo.ail → exercises std_maybe combinators over Maybe<Int>, including from_maybe and map.

• examples/std_either_demo.ail → first program with three distinct type variables in a single fn (the either eliminator), monomorphised six different ways in the IR.

• examples/std_pair_demo.ail → drives every std_pair combinator (fst, snd, swap, map_first, map_second); expected output 7, 9, 9, 7, 8, 18.

• examples/nested_pat.ail → first program to use a nested (pat-ctor Cons a (pat-ctor Cons b _)); the desugar pass flattens it into a chain that the existing flat-match codegen consumes. Prints 30 for a 3-element input list.

Ratified by: crates/ailang-core/tests/effect_doc_honesty_pin.rs.