Exact and bounded binder annotations: x: T fixes the type, x <: T bounds it

[dpmills]

CHL gets two binder-annotation forms, meaning the same thing at every binder position — =, :=, and def parameters. x: T is exact: the binder's type is T, and nothing downstream sees more. x <: T is bounded: the type is inferred with T as an upper bound, so the value's own type flows through. Bounded is the behaviour both positions already had, so existing programs keep working under <: and the corpus needed no migration; what is new is : meaning what it says. That closes the asymmetry that motivated the work — def f(v: {a: Int}): v.b and x: {a: Int} = (a=1, b=2); x.b now agree — and it gives a program its one lever over specialization count. Spec: Two annotation forms: exact and bounded; design: type-inference.md.

The forms coincide only where the value's type already is the annotation. They differ on width (x: {a: Int} = (a=1, b=2) makes x.b an error; <: binds at {a: 1, b: 2}) and on literal singletons (x: Int = 5 discards the singleton, x <: Int = 5 keeps 5 and still discharges arr[x]'s index obligation) — so a "simple" annotation is no guarantee that the two agree.

Type::BoundedHole(T) is a marker in a type slot, not a type

In annotation position only; normalize_annotation erases it into a fresh variable bounded above by T. It is Type::Hole one rung up, and the two compose where a compound annotation is partly specified. It denotes nothing — a bound picks out no set of values — so no typing rule may take one: five solver sites assert that rather than inventing a rule, and only the structural walks that rewrite every slot uniformly pass through. Putting the bound in the type is forced by the multi-parameter encoding: def f(x: A, y <: B, z) uncurries to one tuple annotation, and Tuple([A, BoundedHole(B), Hole]) expresses three modes inside one type.

Neither binder rule needs a mode test

A parameter binds at normalize(annotation) — exact to T itself, bounded to a variable bounded by T — which retires emit_lambda's bind-fresh-then-reconcile step, the reason an exact annotation used to behave as neither reading. A let binds at the same normalization of its completed annotation (emit::complete_annotation fills each Hole from the initializer's type, structurally rather than by constraint, because variables minted after the RHS's level is popped escape inference unresolved). Two special cases fall out as consequences: a deref-copy binds at the annotation because that is what exact means, and a bare _ completes to the initializer's type.

A bound on a mutable variable bounds its value type, so x <: Mut(V) := e and x <: V := e are one declaration: lowering applies the binder's mode to the value it extracts from a Mut(…) annotation (apply_annotation_mode). The value position is also the only one available — the binder's slot must stay structurally a History for mut_value_type, mut_elim and transact_phase to dispatch on — so normalize_annotation asserts a bound never wraps a history rather than collapsing one.

Two things a reader might expect and should not

• A bounded parameter's type is still the meet of its bound and its body's demands, so def f(v <: {a: Int}): v.b requires callers to supply both fields.
• <: is not writable in nested positions, because it describes a binder, not a type. That, and the bounded reading arguably being the more common intent while carrying the heavier spelling, is why the spec marks the spelling [Open]; the mode is a two-valued property lowering reads off the surface, so a respelling is a parser change.

Tests cover both differing columns, the two binder positions agreeing, _ completion, a bounded variable's bound constraining seed and writes, and specialization count: def f(v <: Int) called at f(1) and f(2) produces two clones, def f(v: Int) one. Only four existing assertions changed, each asserting the old reading of : directly.

[dpmills]

This change is part of the following stack:

• Freshening asks a different question than type_level, so it needs its own #71
  • SharedHole: let lowering state that two type positions are the same #72
    • Traits: state what an operator requires of its operands, not that they are the same #73
      • Mutable-variable typing: an honest seed, a fixed history read-through, and a polarity-directed base #52
        • Annotations stop standing in for binder structure, and stop outliving inference #60
          • Four defects in how Mut is typed: message polarity, an unclosable refinement, and op= as a rebind #63
            • A mutable variable read is an explicit operation, not a subtyping rule #64
              • Exact and bounded binder annotations: x: T fixes the type, x <: T bounds it #62 ◀
                • constrain_go asserts the uniquely-keyed invariant it rests on #74
                  • Update the value-Case fan-out's prose to the DisjointJoin it builds #75
                  • Canonicalize each arrow's Pi binder as the solver flattens types #76
                  • Hold a refined type's refinements in one unordered set instead of nested layers #77
                  • Derive a Cast's refinements from its term instead of overwriting the target #78
                  • Add a Lean model of the CCL type system and fuzz the solver against it #79

_{Change managed by git-spice.}