feat: and-patterns (conjunctive patterns, dual to or-patterns)

[ggreif]

Adds p1 and p2 — conjunctive pattern, dual to existing p1 or p2. Matches when both legs match; bindings from both are available. Legs must bind disjoint identifiers (or-patterns require the same set); and binds tighter than or.

switch o {
  case (?x and s) (debug_show {s; x});  // payload + whole value
  case null "none";
};

Implementation

End-to-end: parser → Syntax → typing/definedness/coverage (stubbed) → desugar → IR → all ir_passes (rename, subst_var, freevars, check_ir, await, async, const, tailcall, erase_typ_field) → both backends (classical + enhanced) → wasm. AST and IR interpreters both use Option.(bind … map …).

Tests

• test/run/and-pattern-binds.mo — positive, passes [tc] [run] [run-ir] [run-low] [comp] [valid] [wasm-run]. Covers refutable-leg failures (both positions), func-body, TupP-nested, three-way with refutable middle.
• test/fail/and-pattern-overlap.mo — let-context overlap (M0051).
• test/fail/and-pattern-overlap-case.mo — case-context overlap (M0189, bespoke error).

Known limitations

• Func-arg AndP in inference position errors with M0184 (parity with or-patterns).
• coverage.ml AndP arm is a stub delegating to leg 1 — diagnostic-quality regression only, not soundness.

Docs

Changelog entry + language-manual section + fundamentals-table row.

See also the independent FP-savvy pre-review pass for concrete correctness/coverage traces.

[github-actions]

Comparing from 895c20f to 5c8380c:
In terms of gas, no changes are observed in 5 tests.
In terms of size, no changes are observed in 5 tests.

[ggreif]

Independent FP-savvy review (pre-human-review pass)

Ran an independent pass over the branch looking for correctness bugs, style issues, and coverage gaps. Summary below.

Overall verdict

• ✅ Frontend plumbing (syntax, parser, definedness, desugar, arrange) — complete and parallel to AltP. Precedence correct: %left OR at parser.mly:268 then %left AND at parser.mly:269 — later-declared = tighter, so and binds tighter than or.
• ✅ Typing (src/mo_frontend/typing.ml) — check_pat, gather_pat_aux, vis_pat, combine_pat_srcs, is_explicit_pat, check_pat_typ_dec all have AndP arms. Overlap rejection via M0189 on both val and typ envs.
• ✅ AST interpreter (src/mo_interpreter/interpret.ml:929) — monadic form bind ... (fun ve1 -> map (V.Env.adjoin ve1) ...) is idiomatic.
• ✅ IR interpreter (src/ir_interpreter/interpret_ir.ml:762) — symmetric; declare_pat adjoins both legs.
• ✅ IR check (src/ir_def/check_ir.ml:1093) — t <: pat1.note; t <: pat2.note + disjoint_union is correct and enforces the invariant IR-side.
• ✅ Freevars / rename / subst_var — +- is left-biased union on maps; on disjoint keys it coincides with true union, so the result is correct. Rename threads rho → rho' → rho'' via id_bind which allocates globally-fresh names, so no fresh-rename collision possible.
• ✅ await.ml — disjoint_union in rename_pat; declare_pat pat1 (declare_pat pat2 exp) and define_pat concat are correct. AltP's freevars-empty assertion correctly does not extend to AndP.
• ✅ Codegen — (^^^) at compile_enhanced.ml:10635 threads the same fail continuation to both legs' CanFail arms, so if either leg fails the whole match aborts. Stack discipline is balanced (set_i consumes scrutinee; each leg starts with get_i and consumes it). Classical and enhanced are identical.
• ⚠️ Coverage (src/mo_frontend/coverage.ml:272) — explicit TODO stub delegating to pat1 only. Concrete consequences: (a) case (#a _ and #b _) is treated as covering #a _, so an explicitly-unreachable case won't be flagged redundant and a following case (#a _) may be spuriously flagged as redundant; (b) exhaustiveness-wise it's over-approximating coverage of the first leg, so "missing cases" warnings may be missed. Diagnostic-quality regression only, not soundness. — Fixed with 7a75752!

Correctness concerns

1. gather_pat in check_ir.ml:1040 uses go (go ve pat1) pat2 without any collision check, trusting the frontend. check_pat further down does enforce disjoint_union, so any bug that slipped past the frontend would surface there — defensible but worth a one-line assertion or comment noting the redundancy. — Fixed: the "(frontend enforces)" comments at check_ir.ml:1041 and check_ir.ml:1094 have been rewritten to name the actual enforcer (check_pat / verify_pair), so the invariant-holder is explicit for separate-compilation scenarios where IR is loaded from disk. check_pat's AndP arm now uses an explicit verify_pair helper (cheap iter + predicate, names the first clashing key) instead of disjoint_union's raise/catch control flow.
2. gather_pat_aux in typing.ml:4622 also quietly merges without collision check; the real enforcement happens in check_pat at 3444. Same comment applies: gather runs before the overlap check. — Fixed in 753404cac: gather_pat_aux's AndP arm now gathers each leg independently against the outer scope and enforces disjoint leg-contributions with the AndP-specific M0260, matching check_pat's diagnostic (previously gather_id fired the generic M0051 first in let-context).
3. infer_pat at 3271 outright errors with M0184. Even when one leg is fully annotated ((a : Nat) and b) we could propagate its type to the other leg; currently this forces users to annotate both. Parity with AltP's behaviour, but surprising in function-arg position: func f ((a : Nat) and b) = … works; func f (a and b) = … is a hard error. OK to leave; document it. — Partially fixed: now uses dedicated M0261 (not M0184) in 1b332d74a; parity with AltP's M0184 preserved, so left undocumented.

Missing tests (the biggest gap)

The current positive test (and-pattern-binds.mo) exercises only irrefutable patterns in let-position, so the interesting codegen path (CanFail is1 ... k; is2 k with actual failure) is untested. Suggested additions:

• Refutable AndP in switch: case (?x and s) …; case null … over a ?Nat — exercises (^^^) on CanFail codes. — Fixed in bfe6a06aa.
• Runtime-failing leg: switch where the AndP fails on a value that would have matched the other case — verifies fail-through from leg 1 or leg 2 reaches the next case, not a trap. — Fixed in bfe6a06aa (leftFails / rightFails over Status).
• AndP in function arg: func f ((x : Nat) and y) = x + y. — Fixed in 1355414ea (test/fail/and-pattern-infer.mo inference-position; positive func-arg covered in and-pattern-binds.mo).
• AndP inside TupP: let ((a : Nat) and b, c) = (5, 6). — Fixed in bfe6a06aa.
• Type-mismatched legs: let (x : Nat) and (y : Text) = 5 — expect subtype error, not a confused message. — Fixed in 3e730ff7c (test/fail/and-pattern-typemismatch.mo): produces a clean M0117 "pattern of type Text cannot consume expected type Nat" pointing at the offending leg.
• Three-way conjunction with one refutable leg (e.g. ((x : Nat) and ?y and z) over ?7) — exercises the threaded rho in rename/subst. — Fixed in bfe6a06aa.

Style nits

• Both interpreters' monadic form is fine.
• subst_var's pat (pat rho p1) p2 threading and rename's (p1', rho'); (p2', rho'') are both idiomatic.

Final verdict

Ready for human review, not ready to merge. Correctness of the core implementation is solid. Before merge I'd want:

1. At least one refutable-AndP switch test exercising (^^^) on CanFail codes. — Fixed
2. At least one AndP-in-func-arg and one AndP-in-TupP test. — Fixed
3. Either flesh out coverage.ml's AndP arm or add a FileCheck/warn-expectation test confirming the current stub's behaviour is known. — Fixed
4. The typing changes include a new use of error code M0184 for AndP; M0189 for overlap — both reuse existing codes, which is fine, but worth a quick grep that no diagnostics index needs updating. — Fixed

🤖 Review performed by an independent agent (not the author).

[ggreif]

Round 2 Independent FP-savvy re-review

Referencing: round 1. Scope: the two new commits 753404ca (check_ir rigour + M0260 let-parity) and 3e730ff7 (type-mismatch test), plus anything round 1 missed.

Overall verdict

• The two round-1 concerns that remained open are now cleanly resolved. verify_pair in check_ir.ml:155 is a faithful stand-in for disjoint_union's raise/catch — same domain, same diagnostic, no behavioural drift. The new gather_pat_aux AndP arm at typing.ml:4648 genuinely restores M0260 parity between let and case context, and the regenerated and-pattern-overlap.tc{,-human}.ok proves it (region is now the whole AndP 1.5-1.28, code flipped M0051 → M0260).
• T.Env.adjoin is right-biased (lang_utils/env.ml:35, Some x2). Since verify_pair proves disjointness before adjoin runs, the semantics are identical to the old disjoint_union; if a future regression let overlap through, adjoin would silently drop ve1's binding, but the explicit verify_pair step prevents that. Fine.
• Scope-component coverage in the new gather_pat_aux arm is complete. gather_pat_aux + gather_pat_field + gather_typ_id only ever touch val_env, typ_env, and con_env. The first two are explicitly checked. con_env uses Cons.fresh per TypPF, so the constructors are always distinct identities; collisions are detected by-name through the typ_env iter before con_env's disjoint_add is asked to swallow them. lib_env, obj_env, mixin_env, fld_src_env are unreachable from patterns — no gap. Verified against scope.ml:43 and typing.ml:4669–4691.
• Nested AndP ((a and b) and c), AndP-in-TupP (( x and y, z )), AndP-in-AltP-leg, AndP-with-ObjP-leg-containing-TypPF, and duplicate-against-outer-scope (caught earlier by gather_id's M0051) all work as intended — I traced each.
• Parser precedence %left COLON < %left OR < %left AND (parser.mly:267/269/270) is sound: (a : Nat) and b and ?x and s and #A x and #B y all bind the way round 1 asserted. Nothing to add.

Concerns

1. Stale comment in test/run/and-pattern-binds.mo:62–63 — still says "infer_pat raises M0184, matching AltP's behaviour", but the round-1 fix in 1b332d74a moved the code to the dedicated M0261. Trivial, one-line fix.
2. verify_pair is slight over-abstraction. Its only call site (check_ir.ml:1108) passes fun k ve2 -> not (T.Env.mem k ve2). A narrower check_disjoint env at fmt env1 env2 would be equally rigorous and shorter. Not a blocker; ignore if you plan to reuse the predicate form elsewhere.
3. New M0117 diagnostic for let (x : Nat) and (y : Text) = 5 does not mention and-pattern context. The output reads "pattern of type Text cannot consume expected type Nat" and underlines (y : Text). The underline is helpful, but a first-time AndP user sees a bare AnnotP error and has to reason about why that leg saw Nat. This is shared with AltP's equivalent, and not a new issue introduced by these commits — just worth noting that the test locks in a slightly user-unfriendly diagnostic. I would not block merge on it.

Things round 1 skipped that I re-checked and cleared

• Coverage residual over-approximation. coverage.ml:272, 345, 374 (InAnd1): traced slices for ((#a _) and (#b _)) — pat1 accepts #a slice, succeed(InAnd1) delegates to pat2 on #a-narrowed desc, pat2's TagP fails → fail(InAnd1) → fail ctxt' → fall-through. Case's at is not added to reached_cases, so a vacuous AndP case is correctly flagged as unreachable. No residual over-approximation.
• Freevars (freevars.ml:88–89): +- on disjoint keys = union; combined with check_pat/verify_pair's disjointness guarantee, the asymmetric left-biased semantics of +- are irrelevant. Clean.
• await.ml rename_pat/declare_pat/define_pat all still symmetric between AndP legs. No AltP-style "bindings-empty" assumption leaks into AndP.
• arrange.ml:172 / arrange_ir.ml:143 — identical to AltP, fine.

Final verdict

Ready to merge once the stale M0184 comment in and-pattern-binds.mo:62–63 is updated. Everything else is either cosmetic (over-general helper) or shared with AltP's long-standing behaviour (AndP-flavour-less M0117). The rigour/parity story is now coherent end-to-end: frontend gathers strictly, check_pat enforces strictly, and check_ir's verify_pair validates disk-loaded IR without trusting the frontend.

🤖 Round-2 review by an independent agent (not the author).