v0.14.0 high-risk boundary probes

These probes record failures on core b85a6cd6 (2026-10-08). The baseline results below are historical; fixes and regression fixtures are now present in the local integration worktree, pending merge. Run each standalone source with target/debug/metel, adding --move-check for the ownership cases. Code blocks deliberately use text: accepting a known defect as a successful documentation example would misrepresent the intended behavior.

Finding	Tracker	Local regression coverage
F06	#1423	evaluator/records/equation_remainder_method.mtl
F07	#1424	evaluator/aspects/bounded_method_aspect_arguments.mtl
F08	#1425	evaluator/type_aliases/row_parameter_aliases.mtl
F09	#1426	module_semantics/renamed_row_nominal/main.mtl
F10	#1427	typechecking/aspects/dyn_generic_method_excluded_{local,parameter,tuple}.mtl
F11	#273	typechecking/move_check/associated_row_result_double_move.mtl; evaluator/records/associated_row_result_move_analysis.mtl

F11 fixes concrete reconstruction failures, including E29's structural conditional-method body. It does not resolve #273's broader fail-open policy or change that tracker's v0.16.0 milestone.

F06 — Conditional dispatch on an equation-derived remainder

Expected: assertion succeeds. Actual: T0012 at cleared.cleared(), saying the negative candidate requires a missing token label. Adding an explicit row Rest: !{token} bound also fails. Calling the method on the returned concrete remainder outside the generic definition succeeds (E29).

record Session<row R> { data: { ..R } }
extend<row R: !{token}> Session<..R> { fun cleared(self) -> i64 { 2 } }
fun strip<row R, row Rest>(session: Session<..R>) -> i64
where R = { token: String, ..Rest } {
    let { token: _, ..rest } := session.data;
    let cleared: Session<..Rest> := Session { data = rest };
    cleared.cleared()
}
fun main() { assert(strip(Session { data = { token = "gone" } }) == 2); }

Rules: spec.types.generics.open-rows.legality-2, spec.types.generics.row-conditional-impls.legality-3.

F07 — Concrete aspect arguments are not substituted in a bounded body

Expected: assertion succeeds. Actual: T0001, cannot unify i64 with A, at value.again(input). Concrete and dyn calls to the same default method work (E32). This probe avoids integer-literal ambiguity by annotating input.

aspect Transform<A, B> {
    fun transform(&self, value: A) -> B;
    fun again(&self, value: A) -> B { self.transform(value) }
}
struct Doubler {}
extend Doubler: Transform<i64, i64> {
    fun transform(&self, value: i64) -> i64 { value * 2 }
}
fun generic<T: Transform<i64, i64>>(value: &T, input: i64) -> i64 {
    value.again(input)
}
fun main() { assert(generic(&Doubler {}, 6) == 12); }

Rules: spec.types.generics.rigid-type-parameters.legality-2, spec.declarations.aspects.default-methods.dynamics-1.

F08 — Row-parameter alias expansion leaves a free row name

Expected: empty row alias expands to {}. Actual: T0003, undefined row variable R at the annotated binding. Ordinary type-parameter aliases with row-valued arguments and closed row aliases work (E31).

type Row<row R> := { ..R };
fun main() { let empty: Row<{}> := {}; }

Rules: spec.declarations.type-aliases.legality-1, spec.types.generics.open-rows.legality-1.

F09 — Renaming an imported row nominal loses argument compatibility

Expected: assertion succeeds with the same definition-site Packet identity. Actual: T0001 argument type mismatch. Importing Packet without as Renamed and constructing Packet is a passing control. No second module or collision is required to reproduce this.

model.mtl:

public record Packet<row R> { data: { ..R } }
public fun inspect<row R>(packet: &Packet<..R>) -> i64 { 1 }

main.mtl:

import model::Packet as Renamed;
import model::inspect;
fun main() { assert(inspect(&Renamed { data = {} }) == 1); }

Rules: definition-site nominal identity, spec.declarations.records.legality-1.

F10 — An excluded generic method is callable on a local dyn binding

Expected: reject calling identity through dyn. Actual: the standalone program is accepted and executes when its generic result is discarded. Constraining the result or moving the call into a function taking dyn Mapper instead produces a T0001/T0005 involving the unresolved method parameter T, rather than enforcing the method's exclusion from dyn dispatch.

aspect Mapper {
    fun identity<T>(&self, value: T) -> T;
    fun ordinary(&self) -> i64;
}
struct Item {}
extend Item: Mapper {
    fun identity<T>(&self, value: T) -> T { value }
    fun ordinary(&self) -> i64 { 1 }
}
fun main() {
    let value: dyn Mapper := Item {};
    value.identity(1);
}

Rule: spec.declarations.aspects.dyn-aspect.legality-3.

F11 — Associated row result skips generic ownership checking

Existing tracker: #273, currently v0.16.0. This is not a new fail-open policy gap, but a concrete additional reconstruction failure relevant to v0.14.0 integration.

Expected with --move-check: T0019 at the second consuming call in an uncalled generic definition. Actual: exit success, with a warning that the generic body could not be analyzed: I0001, missing nominal record identity. The valid single-call variant also warns; its concrete Holder implementation executes.

aspect Source { type Item; fun take(self) -> Item; }
fun invalid<S: Source<Item = { token: String }>>(source: S) -> {} {
    let { token: _, ..rest } := source.take();
    let again := source.take();
    rest
}
fun main() {}

Rules: spec.ownership.values-move-by-default.legality-1, spec.declarations.aspects.associated-types.legality-1.

E29's marked body is another reconstruction warning under #273: no method mark on the symbolic nominal. Its concrete assertions pass, but that does not establish generic-body ownership checking. It adds one skipped user body to the corpus relative to the preceding tree; the F11 negative probe is kept here rather than counted as a passing negative fixture.