Reject mutable guarded with when source lacks ScopedMut

[ehartford]

Summary

with e as mut x currently falls back to the plain binding path when e implements immutable Scoped[T] but not mutable ScopedMut[T]. Per the BDFL ruling for problematic requirement #21, this should be a compile error: mut requests mutable guarded access; it must not select a different protocol or silently turn a guarded form into a plain binding.

Repro

type Guard {
    value: i32,
}

impl Scoped[i32] for Guard =
    fn with_enter(self: &Self) -> i32:
        self.value

    fn with_exit(self: &Self) -> void:
        ()

fn main:
    let guard = Guard { value: 1 }
    with guard as mut data:
        data = data + 1

Actual

The checker falls back to plain binding, so data is bound as Guard. The diagnostic is downstream and misleading:

error: arithmetic operator requires numeric operands

Expected

The checker should reject the with dispatch itself with a directional diagnostic, for example:

error: mutable guarded with requires ScopedMut; this type only supports Scoped

If the type implements no guarded protocol at all, with e as mut x remains the plain builder/scoped-mutation form.

Root cause / 5 Whys

1. Why does the wrong error happen? classify_guarded_with checks ScopedMut when as mut is present.
2. Why does it become a plain binding? If ScopedMut is absent, the function returns WithFormKind.Binding unconditionally.
3. Why is that wrong? The expression type may still implement immutable Scoped, meaning the syntax is operating on a guarded-access type and mut requested an unsupported mutable guard capability.
4. Why is this dangerous? Falling back skips guarded acquire/release and no-await-guard semantics for code the user intended as guarded access.
5. Root cause: the classifier treats absence of the requested guard capability as “not guarded” instead of distinguishing “not guarded at all” from “guarded type, wrong mutability capability.”

Code pointers

• src/SemaCheck.w:2022 classify_guarded_with
• src/SemaCheck.w:7221 check_with_expr
• src/MirLower.w:8218 guarded lowering based on with_form_kinds
• Positive coverage exists in test/spec/spec_ss07_5_with_type_based_dispatch.w; add negative coverage for immutable-only guard plus as mut.

Acceptance criteria

• with e as mut x on a type that implements Scoped[T] but not ScopedMut[T] is a compile error at the with expression.
• The diagnostic names the missing mutable guard capability and does not fall through to unrelated body type errors.
• with e as mut x for non-guarded values still uses the plain builder/scoped-mutation path.
• Existing guarded Scoped and ScopedMut tests keep passing.
• Add a compile-error fixture for this case.
• with build, with build :fixpoint, with build :test, and with build :test-green pass.