Borrowing through dyn T

The 1-mut XOR N-immut rule applies to dyn T borrows exactly as it does to concrete-typed borrows. The borrow checker records the borrow at the $$i dyn T / $$m dyn T variable declaration site, keyed on the source variable's name, regardless of the LHS type. This is what closes Probe D in v0.31.1.10 (a regression slice — no new code was required).

Shapes that compile

Two $$i dyn T borrows of the same source (bug375)

Counter:c = { n: 7i32 };
$$i dyn Readable:b1 = c;
$$i dyn Readable:b2 = c;
int32:r = b1.read() + b2.read();
exit r;                          // 14

Multiple shared borrows of the same source are permitted. Both fat ptrs share a vtable but each has its own data slot pointing at c.

$$m dyn T parameter with mutation (bug374)

func:bump_it = int32($$m dyn Bumpable:b) {
    int32:r = b.bump();
    pass r;
};

func:main = int32() {
    Counter:c = { n: 7i32 };
    int32:r = raw bump_it(c);
    exit c.n;                    // 8
};

The call-site coercion uses &c as the fat ptr's data slot — mutation inside the impl propagates.

$$m dyn T local borrow (bug373)

Counter:c = { n: 5i32 };
$$m dyn Bumpable:b = c;
int32:r = b.bump();
exit c.n;                        // 6

Same alias-based data slot, just as a local.

Shapes that are rejected

Write to source while a $$m dyn borrow is live (bug376)

$$m dyn Bumpable:b = c;
c.n = 99i32;                     // error

Diagnostic:

error: [ARIA-026] Cannot assign to 'c.n' because it is borrowed
   |     c.n = 99i32;
   |     ^
note: Borrowed by 'b' here
   |     $$m dyn Bumpable:b = c;
   |     ^

Two $$m dyn borrows of the same source (bug377)

$$m dyn Bumpable:b1 = c;
$$m dyn Bumpable:b2 = c;         // error

Diagnostic:

error: [ARIA-023] Cannot borrow 'c' as mutable because it conflicts
       with existing borrow
note: Existing mutable borrow by 'b1' of 'c'

$$i dyn live, then pass source as $$m dyn param (bug378)

$$i dyn Bumpable:bi = c;
int32:r = raw bump_it(c);        // error: ARIA-019 + ARIA-023

Two diagnostics fire because (a) passing c by value moves it while it is borrowed (ARIA-019), and (b) the $$m dyn coercion at the call site is itself a fresh $$m borrow that conflicts with the existing $$i (ARIA-023).

Source vs concrete $$m borrow (probe pattern)

$$m dyn Bumpable:b = c;
$$m Counter:c2 = c;              // error: ARIA-023

The borrow checker doesn't care that one borrow is dyn and the other is concrete — they both pin c.

Why the rule extends to dyn T automatically

borrow_checker.cpp extracts the access path of the borrow's initializer at the VAR_DECL site, before any dyn coercion is applied to the value:

AccessPath borrow_path = extractAccessPath(stmt->initializer.get());
if (!borrow_path.base_var.empty()) {
    recordBorrowWithPath(borrow_path, stmt->varName,
                         stmt->isBorrowMut, stmt);
}

The access path is {base_var: "c"} whether the LHS is $$m Counter:b or $$m dyn Bumpable:b. All downstream conflict checks (ARIA-019/023/026) consult that record and fire uniformly.

Reasoning about lifetimes

For both the local-var form and the parameter form, the borrow's lifetime is the lexical scope of the borrower:

• $$m dyn T:b = c; — borrow lasts until b goes out of scope.
• func:f = R($$m dyn T:b) { ... } and a call f(c) — borrow lasts for the duration of the call.

Once the borrow is released, c is fully usable again.

Limitations (carried into v0.31.2.x+)

• Re-borrow from a $$m dyn T parameter: passing b onward as $$m to another call is currently treated conservatively (the callee binds the fat ptr to a struct alloca without setting the __borrow_param_mut marker for b). No fixture exercises this path today; revisit if a real program needs it.
• Field-level borrows of a dyn T struct field are not yet supported — borrow the whole struct.
• Borrows with dyn T flowing across async await points are subject to the same ARIA-030 rules as concrete borrows (see borrow/async).