AILang/design/contracts/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](../models/effects.md).
  `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](data-model.md)). 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](language-constraints.md). 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](../models/pipeline.md)).
- 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](prelude-classes.md)) 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](str-abi.md) 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](float-semantics.md)); 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](../../crates/ailang-core/src/desugar.rs) and
  [Pipeline](../models/pipeline.md).
- 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](float-semantics.md)). `(pat-lit "hi")` over
  a `Str` scrutinee is exercised by `examples/eq_demo.ail.json`.
- **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.json`)
  exercise this end-to-end.
- **AI-authoring text surface, form (A)** (see
  [authoring surface](authoring-surface.md)). 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](../models/rc-uniqueness.md)), 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](../models/rc-uniqueness.md). The per-fn-arena
  path is exercised end-to-end by
  `examples/escape_local_demo.ail.json`.
- **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.json` → prints 55 (recursion, arithmetic).
- `examples/list.ail.json` → prints 42 (ADTs + match).
- `examples/hof.ail.json` → prints 42 (first-class fn-refs, indirect call).
- `examples/closure.ail.json` → prints 42 (lambda capturing a let-bound var).
- `examples/list_map.ail.json` → prints 2/4/6 (ADTs + closure + recursive
  HOF + IO; the dogfood smoke test).
- `examples/sort.ail.json` → 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.json` → prints 42 then "true" (polymorphic
  identity at `Int` and `Bool`; two specialised fns emitted).
- `examples/poly_apply.ail.json` → prints 42 (polymorphic `apply`
  with a fn-typed parameter; `apply(succ, 41)`).
- `examples/box.ail.json` → 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.json` → prints 7 then 99 (pattern match
  over `Maybe<Int>`: `or_else(Some(7), 99)` then
  `or_else(None, 99)`).
- `examples/std_list_demo.ail.json` → 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.json` → exercises `std_maybe`
  combinators over `Maybe<Int>`, including `from_maybe` and `map`.
- `examples/std_either_demo.ail.json` → 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.json` → drives every
  `std_pair` combinator (fst, snd, swap, map_first, map_second);
  expected output 7, 9, 9, 7, 8, 18.
- `examples/nested_pat.ail.json` → 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`.