From c04bd2d3a1e2952649a357af8ac25c5b67b06534 Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Thu, 23 Apr 2026 10:53:42 +0200 Subject: [PATCH 01/19] feat(and-patterns): parser + AST + frontend plumbing MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Introduces `AndP (p1, p2)` — conjunctive pattern — as the syntactic counterpart to the existing disjunctive `AltP`. `(p1 and p2)` matches a value iff both `p1` and `p2` match it; bindings from both legs are available in the body. ## Surface syntax Mirrors the or-pattern production in `parser.mly`: pat_bin : | p1=pat_bin OR p2=pat_bin { AltP(p1, p2) } | p1=pat_bin AND p2=pat_bin { AndP(p1, p2) } Precedence: `AND` binds tighter than `OR` (matches the expression-level precedence table), so `#a or #b and #c` parses as `#a or (#b and #c)`. The `AND`/`OR` tokens were already reserved for expression use. ## Frontend plumbing Spot-wise additions (no new abstractions): - `src/mo_def/syntax.ml` — `AndP of pat * pat`; removed the stale `(* | AsP *)` placeholder comment. - `src/mo_def/arrange.ml` — pretty-printing arm. - `src/mo_frontend/typing.ml`: - `is_explicit_pat`, `combine_pat_srcs`, `vis_pat`, `gather_pat_aux` — recurse into both legs (bindings are not shared). - `infer_pat` — error like `AltP` (explicit annotation required). - `check_pat` — check both legs against expected type, union bindings, error M0189 on overlap (duplicate binding across legs). - `check_pat_typ_dec` — analogous for type bindings. - `src/mo_frontend/definedness.ml` — both legs contribute to defined/free sets (same as `AltP`). - `src/mo_frontend/coverage.ml` — stub: approximate as the first leg's coverage. Unsound for refutability but adequate for a frontend-only draft; flagged with a TODO. - `src/mo_interpreter/interpret.ml`: - `declare_pat` — union of both legs' declared identifiers. - `match_pat` — both must match; bindings adjoined. - `src/js/astjs.ml` — AST-to-JSON case. - `src/docs/namespace.ml` — `idents_in_pattern` dedupes defensively (typechecker rejects overlap, but mo-doc may traverse pre-typecheck). ## Lowering `src/lowering/desugar.ml` raises "and-pattern lowering not yet implemented" — IR does not yet have `AndP` and codegen/IR passes haven't been extended. This draft PR intentionally scopes to frontend + typechecking; IR, interpretation of lowered form, and backend come in follow-up commits. ## Tests None yet in this commit; `test/run` tests land in a follow-up so the parser/type-checker fix-ups can be reviewed in isolation first. --- doc/md/examples/grammar.txt | 1 + src/docs/namespace.ml | 5 ++++ src/js/astjs.ml | 1 + src/lowering/desugar.ml | 7 +++++ src/mo_def/arrange.ml | 1 + src/mo_def/syntax.ml | 4 +-- src/mo_frontend/coverage.ml | 6 +++++ src/mo_frontend/definedness.ml | 1 + src/mo_frontend/parser.mly | 2 ++ src/mo_frontend/typing.ml | 47 +++++++++++++++++++++++++++++++++ src/mo_interpreter/interpret.ml | 6 +++++ 11 files changed, 78 insertions(+), 3 deletions(-) diff --git a/doc/md/examples/grammar.txt b/doc/md/examples/grammar.txt index bb3a2397eec..6f9e2a5831a 100644 --- a/doc/md/examples/grammar.txt +++ b/doc/md/examples/grammar.txt @@ -316,6 +316,7 @@ ::= 'or' + 'and' ':' ::= diff --git a/src/docs/namespace.ml b/src/docs/namespace.ml index b59e12969e9..082cacc9e0a 100644 --- a/src/docs/namespace.ml +++ b/src/docs/namespace.ml @@ -20,6 +20,11 @@ let rec idents_in_pattern : Syntax.pat -> string list = | Syntax.AnnotP (p, _) | Syntax.ParP p -> idents_in_pattern p + | Syntax.AndP (p1, p2) -> + (* typechecker rejects overlapping bindings across legs, but + this helper may run on not-yet-checked code (mo-doc), so + dedupe defensively *) + List.sort_uniq compare (idents_in_pattern p1 @ idents_in_pattern p2) | Syntax.WildP | Syntax.SignP (_, _) | Syntax.LitP _ -> [] let from_module = diff --git a/src/js/astjs.ml b/src/js/astjs.ml index 1fc6b9a72f1..dad7bbe3ffb 100644 --- a/src/js/astjs.ml +++ b/src/js/astjs.ml @@ -586,6 +586,7 @@ module Make (Cfg : Config) = struct | OptP p -> to_js_object "OptP" [| pat_js p |] | TagP (i, p) -> to_js_object "TagP" [| js_string ("#" ^ i.it); pat_js p |] | AltP (p1, p2) -> to_js_object "AltP" [| pat_js p1; pat_js p2 |] + | AndP (p1, p2) -> to_js_object "AndP" [| pat_js p1; pat_js p2 |] | ParP p -> to_js_object "ParP" [| pat_js p |] and pat_field_js pf = diff --git a/src/lowering/desugar.ml b/src/lowering/desugar.ml index e95ffcc8725..357ed9ab7bd 100644 --- a/src/lowering/desugar.ml +++ b/src/lowering/desugar.ml @@ -1318,6 +1318,13 @@ and pat' = function | S.OptP p -> I.OptP (pat p) | S.TagP (i, p) -> I.TagP (i.it, pat p) | S.AltP (p1, p2) -> I.AltP (pat p1, pat p2) + | S.AndP (p1, p2) -> + (* TODO: AND-pattern lowering to IR. For the frontend/typecheck + draft PR the IR does not yet have an `AndP` constructor; reach + this arm only if a program containing an and-pattern is + compiled all the way through. *) + ignore (p1, p2); + failwith "and-pattern lowering not yet implemented" | S.AnnotP (p, _) | S.ParP p -> pat' p.it diff --git a/src/mo_def/arrange.ml b/src/mo_def/arrange.ml index 499fad62c5f..e7360de6899 100644 --- a/src/mo_def/arrange.ml +++ b/src/mo_def/arrange.ml @@ -168,6 +168,7 @@ module Make (Cfg : Config) = struct | OptP p -> "OptP" $$ [pat p] | TagP (i, p) -> "TagP" $$ [tag i; pat p] | AltP (p1, p2) -> "AltP" $$ [pat p1; pat p2] + | AndP (p1, p2) -> "AndP" $$ [pat p1; pat p2] | ParP p -> "ParP" $$ [pat p])) and lit = function diff --git a/src/mo_def/syntax.ml b/src/mo_def/syntax.ml index d9f7222792d..481ad16f40a 100644 --- a/src/mo_def/syntax.ml +++ b/src/mo_def/syntax.ml @@ -120,11 +120,9 @@ and pat' = | OptP of pat (* option *) | TagP of id * pat (* tagged variant *) | AltP of pat * pat (* disjunctive *) + | AndP of pat * pat (* conjunctive *) | AnnotP of pat * typ (* type annotation *) | ParP of pat (* parenthesis *) -(* - | AsP of pat * pat (* conjunctive *) -*) and pat_field = pat_field' phrase and pat_field' = diff --git a/src/mo_frontend/coverage.ml b/src/mo_frontend/coverage.ml index 3710f922a4f..d86f9e985d3 100644 --- a/src/mo_frontend/coverage.ml +++ b/src/mo_frontend/coverage.ml @@ -268,6 +268,12 @@ let rec match_pat ctxt desc pat t sets = | AltP (pat1, pat2) -> sets.alts <- AtSet.add pat1.at (AtSet.add pat2.at sets.alts); match_pat (InAlt1 (ctxt, pat1.at, pat2, t)) desc pat1 t sets + | AndP (pat1, _pat2) -> + (* TODO: proper coverage for and-patterns. For now approximate by + treating the pattern as equivalent to its first leg — unsound + for refutability but adequate for a draft that only exercises + the frontend + typecheck. *) + match_pat ctxt desc pat1 t sets | AnnotP (pat1, _) | ParP pat1 -> match_pat ctxt desc pat1 t sets diff --git a/src/mo_frontend/definedness.ml b/src/mo_frontend/definedness.ml index eeec7f36b3e..602af612a92 100644 --- a/src/mo_frontend/definedness.ml +++ b/src/mo_frontend/definedness.ml @@ -156,6 +156,7 @@ and pat msgs p : fd = match p.it with | OptP p | TagP (_, p) -> pat msgs p | AltP (p1, p2) -> pat msgs p1 ++++ pat msgs p2 + | AndP (p1, p2) -> pat msgs p1 ++++ pat msgs p2 and pats msgs ps : fd = union_binders (pat msgs) ps diff --git a/src/mo_frontend/parser.mly b/src/mo_frontend/parser.mly index 852b2da0825..6e5aa5f045f 100644 --- a/src/mo_frontend/parser.mly +++ b/src/mo_frontend/parser.mly @@ -928,6 +928,8 @@ pat_bin : { p } | p1=pat_bin OR p2=pat_bin { AltP(p1, p2) @! at $sloc } + | p1=pat_bin AND p2=pat_bin + { AndP(p1, p2) @! at $sloc } | p=pat_bin COLON t=typ { AnnotP(p, t) @! at $sloc } diff --git a/src/mo_frontend/typing.ml b/src/mo_frontend/typing.ml index f4ef62700f8..0c3b69efae6 100644 --- a/src/mo_frontend/typing.ml +++ b/src/mo_frontend/typing.ml @@ -1157,6 +1157,7 @@ let rec is_explicit_pat p = | TupP ps -> List.for_all is_explicit_pat ps | ObjP pfs -> List.for_all is_explicit_pat_field pfs | AltP (p1, p2) -> is_explicit_pat p1 && is_explicit_pat p2 + | AndP (p1, p2) -> is_explicit_pat p1 && is_explicit_pat p2 | AnnotP _ -> true and is_explicit_pat_field pf = @@ -1414,6 +1415,9 @@ and combine_pat_srcs env t pat : unit = | AltP (pat1, pat2) -> combine_pat_srcs env t pat1; combine_pat_srcs env t pat2; + | AndP (pat1, pat2) -> + combine_pat_srcs env t pat1; + combine_pat_srcs env t pat2; | AnnotP (pat1, _typ) -> combine_pat_srcs env t pat1 | ParP pat1 -> combine_pat_srcs env t pat1 @@ -3264,6 +3268,22 @@ and infer_pat' name_types env pat : T.typ * Scope.val_env = error env pat.at "M0189" "different set of bindings in pattern alternatives"; if not env.pre then T.Env.(iter (fun k t1 -> warn_lossy_bind_type env pat.at k t1 (find k ve2))) ve1; t, T.Env.merge (fun _ -> Lib.Option.map2 (T.lub ~src_fields:env.srcs)) ve1 ve2*) + | AndP (pat1, pat2) -> + error env pat.at "M0184" + "cannot infer the type of this and-pattern, please add a type annotation"; + (*let t1, ve1 = infer_pat env pat1 in + let t2, ve2 = infer_pat env pat2 in + (* Both legs must accept the scrutinee, so the inferred type is the + intersection/glb. No bindings may overlap. *) + if not (T.compatible t1 t2) then + error env pat.at "M0104" + "pattern branches have incompatible types,\nleft consumes%a\nright consumes%a" + display_typ_expand t1 + display_typ_expand t2; + let overlap = T.Env.filter (fun k _ -> T.Env.mem k ve2) ve1 in + if not (T.Env.is_empty overlap) then + error env pat.at "M0???" "and-pattern binds the same variable in both legs"; + T.glb ~src_fields:env.srcs t1 t2, T.Env.union (fun _ v _ -> Some v) ve1 ve2*) | AnnotP ({it = VarP id; _} as pat1, typ) when name_types -> let t = check_typ env typ in T.Named (id.it, t), check_pat env t pat1 @@ -3421,6 +3441,19 @@ and check_pat_aux' env t t_orig pat val_kind : Scope.val_env = ) ve1; let merge_entries (t1, at1, kind1) (t2, at2, kind2) = (T.lub ~src_fields:env.srcs t1 t2, at1, kind1) in T.Env.merge (fun _ -> Lib.Option.map2 merge_entries) ve1 ve2 + | AndP (pat1, pat2) -> + (* Both legs must match the scrutinee; bindings from both are + available in the body. Overlap in binding names is an error. *) + let ve1 = check_pat env t pat1 in + let ve2 = check_pat env t pat2 in + T.Env.iter (fun k _ -> + if T.Env.mem k ve2 then + error env pat.at "M0189" + "variable `%s` bound in both branches of and-pattern" k + ) ve1; + T.Env.merge (fun _ o1 o2 -> match o1, o2 with + | Some v, _ | _, Some v -> Some v + | None, None -> None) ve1 ve2 | AnnotP (pat1, typ) -> let t' = check_typ env typ in if not (sub env pat.at t t') then @@ -3542,6 +3575,18 @@ and check_pat_typ_dec env t pat : Scope.typ_env = error env pat.at "M0189" "mismatched types for type %s in patterns" s else None) te1 te2 in te1 + | AndP (pat1, pat2), _ -> + (* Type-level bindings: union, with error on overlap. *) + let te1 = check_pat_typ_dec env t pat1 in + let te2 = check_pat_typ_dec env t pat2 in + T.Env.iter (fun k _ -> + if T.Env.mem k te2 then + error env pat.at "M0189" + "type identifier `%s` bound in both branches of and-pattern" k + ) te1; + T.Env.merge (fun _ o1 o2 -> match o1, o2 with + | Some v, _ | _, Some v -> Some v + | None, None -> None) te1 te2 | _, _ -> T.Env.empty and check_pats_typ_dec env ts pats te at : Scope.typ_env = @@ -3638,6 +3683,7 @@ and vis_pat src pat xs : visibility_env = | TagP (_, pat1) | AnnotP (pat1, _) | ParP pat1 -> vis_pat src pat1 xs + | AndP (pat1, pat2) -> vis_pat src pat1 (vis_pat src pat2 xs) and vis_pat_field src pf xs = match pf.it with @@ -4573,6 +4619,7 @@ and gather_pat_aux env val_kind scope pat : Scope.t = | ObjP pfs -> List.fold_left (gather_pat_field env) scope pfs | TagP (_, pat1) | AltP (pat1, _) | OptP pat1 | AnnotP (pat1, _) | ParP pat1 -> gather_pat env scope pat1 + | AndP (pat1, pat2) -> gather_pat env (gather_pat env scope pat1) pat2 and gather_pat_field env scope pf : Scope.t = let val_kind = kind_of_field_pattern pf in diff --git a/src/mo_interpreter/interpret.ml b/src/mo_interpreter/interpret.ml index 01a7e00c954..76c84a9c106 100644 --- a/src/mo_interpreter/interpret.ml +++ b/src/mo_interpreter/interpret.ml @@ -838,6 +838,7 @@ and declare_pat pat : val_env = | AltP (pat1, _) (* pat2 has the same identifiers *) | AnnotP (pat1, _) | ParP pat1 -> declare_pat pat1 + | AndP (pat1, pat2) -> V.Env.adjoin (declare_pat pat1) (declare_pat pat2) and declare_pats pats ve : val_env = match pats with @@ -928,6 +929,11 @@ and match_pat pat v : val_env option = | None -> match_pat pat2 v | some -> some ) + | AndP (pat1, pat2) -> + (match match_pat pat1 v, match_pat pat2 v with + | Some ve1, Some ve2 -> Some (V.Env.adjoin ve1 ve2) + | _ -> None + ) | AnnotP (pat1, _) | ParP pat1 -> match_pat pat1 v From 763dd681163b2b0cc5ce07fd1f75b660b669f6f0 Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Thu, 23 Apr 2026 11:03:39 +0200 Subject: [PATCH 02/19] test(and-patterns): run + fail coverage for frontend behaviour MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - `test/run/and-pattern-binds.mo`: exercises the source interpreter on four and-pattern shapes — disjoint VarP+VarP, mixed option+VarP, three-leg and, and an and-inside-or disjunction. Suppresses the M0145 non-exhaustive-let warning on the option leg. Skips `run-ir`, `run-low`, and `comp` since IR/lowering aren't wired up yet. - `test/fail/and-pattern-overlap.mo`: overlapping bindings at top level trigger M0051 ("duplicate definition") from `gather_pat_aux`. - `test/fail/and-pattern-overlap-case.mo`: overlapping bindings inside a switch case trigger M0189 from the `check_pat` AndP arm — the case-pattern context doesn't go through `gather_pat`, so this is the code path where the purpose-built error actually fires. --- test/fail/and-pattern-overlap-case.mo | 7 ++++++ test/fail/and-pattern-overlap.mo | 1 + .../ok/and-pattern-overlap-case.tc-human.ok | 4 ++++ .../and-pattern-overlap-case.tc-human.ret.ok | 1 + test/fail/ok/and-pattern-overlap-case.tc.ok | 1 + .../ok/and-pattern-overlap-case.tc.ret.ok | 1 + test/fail/ok/and-pattern-overlap.tc-human.ok | 4 ++++ .../ok/and-pattern-overlap.tc-human.ret.ok | 1 + test/fail/ok/and-pattern-overlap.tc.ok | 1 + test/fail/ok/and-pattern-overlap.tc.ret.ok | 1 + test/run/and-pattern-binds.mo | 23 +++++++++++++++++++ test/run/ok/and-pattern-binds.run.ok | 4 ++++ 12 files changed, 49 insertions(+) create mode 100644 test/fail/and-pattern-overlap-case.mo create mode 100644 test/fail/and-pattern-overlap.mo create mode 100644 test/fail/ok/and-pattern-overlap-case.tc-human.ok create mode 100644 test/fail/ok/and-pattern-overlap-case.tc-human.ret.ok create mode 100644 test/fail/ok/and-pattern-overlap-case.tc.ok create mode 100644 test/fail/ok/and-pattern-overlap-case.tc.ret.ok create mode 100644 test/fail/ok/and-pattern-overlap.tc-human.ok create mode 100644 test/fail/ok/and-pattern-overlap.tc-human.ret.ok create mode 100644 test/fail/ok/and-pattern-overlap.tc.ok create mode 100644 test/fail/ok/and-pattern-overlap.tc.ret.ok create mode 100644 test/run/and-pattern-binds.mo create mode 100644 test/run/ok/and-pattern-binds.run.ok diff --git a/test/fail/and-pattern-overlap-case.mo b/test/fail/and-pattern-overlap-case.mo new file mode 100644 index 00000000000..715aa61490b --- /dev/null +++ b/test/fail/and-pattern-overlap-case.mo @@ -0,0 +1,7 @@ +// overlap inside a switch case — `gather_pat` is not the first line of +// defence here, so this hits the M0189 check we added in `check_pat` +func f(v : Nat) : Nat = + switch v { + case ((x : Nat) and (x : Nat)) x; + }; +ignore f 3 diff --git a/test/fail/and-pattern-overlap.mo b/test/fail/and-pattern-overlap.mo new file mode 100644 index 00000000000..95b51ff145e --- /dev/null +++ b/test/fail/and-pattern-overlap.mo @@ -0,0 +1 @@ +let (a : Nat) and (a : Nat) = 5; diff --git a/test/fail/ok/and-pattern-overlap-case.tc-human.ok b/test/fail/ok/and-pattern-overlap-case.tc-human.ok new file mode 100644 index 00000000000..7300b559688 --- /dev/null +++ b/test/fail/ok/and-pattern-overlap-case.tc-human.ok @@ -0,0 +1,4 @@ +error[M0189]: variable `x` bound in both branches of and-pattern + ┌─ and-pattern-overlap-case.mo:5:11 + 5 │ case ((x : Nat) and (x : Nat)) x; + │ ^^^^^^^^^^^^^^^^^^^^^^^ diff --git a/test/fail/ok/and-pattern-overlap-case.tc-human.ret.ok b/test/fail/ok/and-pattern-overlap-case.tc-human.ret.ok new file mode 100644 index 00000000000..69becfa16f9 --- /dev/null +++ b/test/fail/ok/and-pattern-overlap-case.tc-human.ret.ok @@ -0,0 +1 @@ +Return code 1 diff --git a/test/fail/ok/and-pattern-overlap-case.tc.ok b/test/fail/ok/and-pattern-overlap-case.tc.ok new file mode 100644 index 00000000000..8fff287b6d5 --- /dev/null +++ b/test/fail/ok/and-pattern-overlap-case.tc.ok @@ -0,0 +1 @@ +and-pattern-overlap-case.mo:5.11-5.34: type error [M0189], variable `x` bound in both branches of and-pattern diff --git a/test/fail/ok/and-pattern-overlap-case.tc.ret.ok b/test/fail/ok/and-pattern-overlap-case.tc.ret.ok new file mode 100644 index 00000000000..69becfa16f9 --- /dev/null +++ b/test/fail/ok/and-pattern-overlap-case.tc.ret.ok @@ -0,0 +1 @@ +Return code 1 diff --git a/test/fail/ok/and-pattern-overlap.tc-human.ok b/test/fail/ok/and-pattern-overlap.tc-human.ok new file mode 100644 index 00000000000..b5335042490 --- /dev/null +++ b/test/fail/ok/and-pattern-overlap.tc-human.ok @@ -0,0 +1,4 @@ +error[M0051]: duplicate definition for a in block + ┌─ and-pattern-overlap.mo:1:20 + 1 │ let (a : Nat) and (a : Nat) = 5; + │ ^ diff --git a/test/fail/ok/and-pattern-overlap.tc-human.ret.ok b/test/fail/ok/and-pattern-overlap.tc-human.ret.ok new file mode 100644 index 00000000000..69becfa16f9 --- /dev/null +++ b/test/fail/ok/and-pattern-overlap.tc-human.ret.ok @@ -0,0 +1 @@ +Return code 1 diff --git a/test/fail/ok/and-pattern-overlap.tc.ok b/test/fail/ok/and-pattern-overlap.tc.ok new file mode 100644 index 00000000000..097a41ab3d6 --- /dev/null +++ b/test/fail/ok/and-pattern-overlap.tc.ok @@ -0,0 +1 @@ +and-pattern-overlap.mo:1.20-1.21: type error [M0051], duplicate definition for a in block diff --git a/test/fail/ok/and-pattern-overlap.tc.ret.ok b/test/fail/ok/and-pattern-overlap.tc.ret.ok new file mode 100644 index 00000000000..69becfa16f9 --- /dev/null +++ b/test/fail/ok/and-pattern-overlap.tc.ret.ok @@ -0,0 +1 @@ +Return code 1 diff --git a/test/run/and-pattern-binds.mo b/test/run/and-pattern-binds.mo new file mode 100644 index 00000000000..498a157f812 --- /dev/null +++ b/test/run/and-pattern-binds.mo @@ -0,0 +1,23 @@ +//MOC-FLAG -A=M0145 +import { debugPrint } = "mo:⛔"; + +// simplest: both legs succeed, two disjoint bindings on the same value +let (a : Nat) and (b : Nat) = 5; +debugPrint (debug_show {a; b}); + +// option pattern + bare name — ?x constrains, s captures the whole value +let (?x) and s = ?7; +debugPrint (debug_show {x; s}); + +// nested and: three legs bind three names to the same value +let (x3 : Nat) and (y3 : Nat) and (z3 : Nat) = 11; +debugPrint (debug_show {x3; y3; z3}); + +// and mixed with or — `and` binds tighter than `or`, so this groups as +// `((#a n) and m) or ((#b n) and m) : ...` +let ((#a n) and m) or ((#b n) and m) : { #a : Nat; #b : Nat } = #a 13; +debugPrint (debug_show {n; m}); + +//SKIP run-ir +//SKIP run-low +//SKIP comp diff --git a/test/run/ok/and-pattern-binds.run.ok b/test/run/ok/and-pattern-binds.run.ok new file mode 100644 index 00000000000..ff7c9726335 --- /dev/null +++ b/test/run/ok/and-pattern-binds.run.ok @@ -0,0 +1,4 @@ +{a = 5; b = 5} +{s = ?7; x = 7} +{x3 = 11; y3 = 11; z3 = 11} +{m = #a(13); n = 13} From 7b4d8aea3eef43fd95d95b1f889a9a0df60c1a80 Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Thu, 23 Apr 2026 11:17:18 +0200 Subject: [PATCH 03/19] refactor(and-patterns): express AST-interpreter match_pat in monadic form MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Model the AndP arm after AltP's short-circuit style and express both failure paths through Option's bind/map rather than an ad-hoc tuple match. Local open `Option.(...)` keeps it one readable line per step: | AndP (pat1, pat2) -> Option.(bind (match_pat pat1 v) (fun ve1 -> map (V.Env.adjoin ve1) (match_pat pat2 v))) Reads as 'match p1; if it succeeds, try p2 and merge the envs'. Observably equivalent to the previous eager-evaluation version (match_pat has no side effects) — this is a style fix, not a behaviour change. All existing and-pattern tests still pass. --- src/mo_interpreter/interpret.ml | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/mo_interpreter/interpret.ml b/src/mo_interpreter/interpret.ml index 76c84a9c106..644c8cacf51 100644 --- a/src/mo_interpreter/interpret.ml +++ b/src/mo_interpreter/interpret.ml @@ -930,10 +930,8 @@ and match_pat pat v : val_env option = | some -> some ) | AndP (pat1, pat2) -> - (match match_pat pat1 v, match_pat pat2 v with - | Some ve1, Some ve2 -> Some (V.Env.adjoin ve1 ve2) - | _ -> None - ) + Option.(bind (match_pat pat1 v) (fun ve1 -> + map (V.Env.adjoin ve1) (match_pat pat2 v))) | AnnotP (pat1, _) | ParP pat1 -> match_pat pat1 v From ac6d7ba572c2c09eaf6a0abb1df38b743982077d Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Thu, 23 Apr 2026 11:31:41 +0200 Subject: [PATCH 04/19] feat(and-patterns): plumb through IR, middle-end passes, and codegen MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Extends AND-pattern support from the frontend-only draft to end-to-end compilation. `test/run/and-pattern-binds.mo` now passes [tc] [run] [run-ir] [run-low] [comp] [valid] [wasm-run]. IR core (`src/ir_def/`): - `ir.ml` — new `AndP of pat * pat` constructor. - `ir_utils.ml` — irrefutable iff BOTH legs are (AND semantics). - `freevars.ml` — same `+-` combine as `AltP` (correct: left-biased union coincides with true union when bindings are disjoint, which the frontend enforces for and-patterns). - `arrange_ir.ml` — "AndP" printer. - `rename.ml`, `subst_var.ml` — bindings from both legs chained left-to-right (no assumption of shared bindings, unlike AltP). - `check_ir.ml` — both legs subtype-check against scrutinee; the resulting val_env is the disjoint_union of the legs'. IR interpreter (`src/ir_interpreter/interpret_ir.ml`) — AndP arm uses the same monadic `Option.(bind … map …)` form as the AST interpreter. Both interpreters short-circuit identically. IR passes — AndP arms added to `tailcall`, `erase_typ_field`, `const`, `async`, `await` (three spots: declare_pat / rename_pat / define_pat). All recurse into both legs; `await`'s renames hit the disjoint-union assumption cleanly. Codegen (both backends) — `fill_pat` stashes the scrutinee in a local named `and_scrut`, feeds it to each leg in sequence via `(^^^)` composition; either leg's failure propagates through the pattern-code's fail-continuation and cancels the whole match. `destruct_const_pat` threads the val_env through both legs sequentially, returning `None` if either rejects. Lowering (`src/lowering/desugar.ml`) — the previous `failwith` is replaced by a direct `S.AndP → I.AndP` translation. Tests (`test/run/and-pattern-binds.mo`) — the SKIP directives for `run-ir`, `run-low`, and `comp` are removed; the new phase outputs match the source-interpreter output exactly. --- src/codegen/compile_classical.ml | 11 +++++++++++ src/codegen/compile_enhanced.ml | 16 ++++++++++++++++ src/ir_def/arrange_ir.ml | 1 + src/ir_def/check_ir.ml | 11 +++++++++++ src/ir_def/freevars.ml | 1 + src/ir_def/ir.ml | 1 + src/ir_def/ir_utils.ml | 1 + src/ir_def/rename.ml | 6 ++++++ src/ir_def/subst_var.ml | 1 + src/ir_interpreter/interpret_ir.ml | 4 ++++ src/ir_passes/async.ml | 2 ++ src/ir_passes/await.ml | 7 +++++++ src/ir_passes/const.ml | 1 + src/ir_passes/erase_typ_field.ml | 2 ++ src/ir_passes/tailcall.ml | 1 + src/lowering/desugar.ml | 8 +------- test/run/and-pattern-binds.mo | 3 --- test/run/ok/and-pattern-binds.run-ir.ok | 4 ++++ test/run/ok/and-pattern-binds.run-low.ok | 4 ++++ test/run/ok/and-pattern-binds.wasm-run.ok | 4 ++++ 20 files changed, 79 insertions(+), 10 deletions(-) create mode 100644 test/run/ok/and-pattern-binds.run-ir.ok create mode 100644 test/run/ok/and-pattern-binds.run-low.ok create mode 100644 test/run/ok/and-pattern-binds.wasm-run.ok diff --git a/src/codegen/compile_classical.ml b/src/codegen/compile_classical.ml index 563bef527e5..5de26f05ad0 100644 --- a/src/codegen/compile_classical.ml +++ b/src/codegen/compile_classical.ml @@ -13166,6 +13166,13 @@ and fill_pat env ae pat : patternCode = CannotFail set_i ^^^ orElse (CannotFail get_i ^^^ code1) (CannotFail get_i ^^^ code2) + | AndP (p1, p2) -> + let code1 = fill_pat env ae p1 in + let code2 = fill_pat env ae p2 in + let (set_i, get_i) = new_local env "and_scrut" in + CannotFail set_i ^^^ + (CannotFail get_i ^^^ code1) ^^^ + (CannotFail get_i ^^^ code2) and alloc_pat_local env ae pat = let d = Freevars.pat pat in @@ -13441,6 +13448,10 @@ and destruct_const_pat ae pat const : VarEnv.t option = match pat.it with let l = destruct_const_pat ae p1 const in if l = None then destruct_const_pat ae p2 const else l + | AndP (p1, p2) -> + (match destruct_const_pat ae p1 const with + | None -> None + | Some ae' -> destruct_const_pat ae' p2 const) | TupP ps -> let cs = match const with (_, Const.Tuple cs) -> cs | (_, Const.Unit) -> [] | _ -> assert false in let go ae p c = match ae with diff --git a/src/codegen/compile_enhanced.ml b/src/codegen/compile_enhanced.ml index 269e355b340..08d139ce08e 100644 --- a/src/codegen/compile_enhanced.ml +++ b/src/codegen/compile_enhanced.ml @@ -13492,6 +13492,17 @@ and fill_pat env ae pat : patternCode = CannotFail set_i ^^^ orElse (CannotFail get_i ^^^ code1) (CannotFail get_i ^^^ code2) + | AndP (p1, p2) -> + (* Both legs must match the same scrutinee; bindings from both + are available. Stash the scrutinee once, feed it to each leg + in sequence. `(^^^)` threads failure through — either leg's + failure cancels the whole match. *) + let code1 = fill_pat env ae p1 in + let code2 = fill_pat env ae p2 in + let (set_i, get_i) = new_local env "and_scrut" in + CannotFail set_i ^^^ + (CannotFail get_i ^^^ code1) ^^^ + (CannotFail get_i ^^^ code2) and alloc_pat_local env ae pat = let d = Freevars.pat pat in @@ -13767,6 +13778,11 @@ and destruct_const_pat ae pat const : VarEnv.t option = match pat.it with let l = destruct_const_pat ae p1 const in if l = None then destruct_const_pat ae p2 const else l + | AndP (p1, p2) -> + (* Both legs must accept; fold bindings left-to-right. *) + (match destruct_const_pat ae p1 const with + | None -> None + | Some ae' -> destruct_const_pat ae' p2 const) | TupP ps -> let cs = match const with Const.Tuple cs -> cs | Const.Unit -> [] | _ -> assert false in let go ae p c = match ae with diff --git a/src/ir_def/arrange_ir.ml b/src/ir_def/arrange_ir.ml index 510128218bf..4e149564740 100644 --- a/src/ir_def/arrange_ir.ml +++ b/src/ir_def/arrange_ir.ml @@ -140,6 +140,7 @@ and pat p = match p.it with | OptP p -> "OptP" $$ [ pat p ] | TagP (i, p) -> "TagP" $$ [ id i; pat p ] | AltP (p1,p2) -> "AltP" $$ [ pat p1; pat p2 ] + | AndP (p1,p2) -> "AndP" $$ [ pat p1; pat p2 ] and lit = function | NullLit -> Atom "NullLit" diff --git a/src/ir_def/check_ir.ml b/src/ir_def/check_ir.ml index 010d3d5896b..76c5cc6246c 100644 --- a/src/ir_def/check_ir.ml +++ b/src/ir_def/check_ir.ml @@ -1037,6 +1037,9 @@ and gather_pat env const ve0 pat : val_env = let ve1, ve2 = go ve pat1, go ve pat2 in let common i1 i2 = { typ = lub env i1.typ i2.typ; loc_known = i1.loc_known && i2.loc_known; const = i1.const && i2.const } in T.Env.merge (fun _ -> Lib.Option.map2 common) ve1 ve2 + | AndP (pat1, pat2) -> + (* legs contribute disjoint bindings (frontend enforces) *) + go (go ve pat1) pat2 | OptP pat1 | TagP (_, pat1) -> go ve pat1 @@ -1087,6 +1090,14 @@ and check_pat env pat : val_env = error env pat.at "set of bindings differ for alternative pattern"; let common i1 i2 = { typ = lub env i1.typ i2.typ; loc_known = i1.loc_known && i2.loc_known; const = i1.const && i2.const } in T.Env.merge (fun _ -> Lib.Option.map2 common) ve1 ve2 + | AndP (pat1, pat2) -> + (* both legs must accept the scrutinee; bindings are disjoint + (frontend enforces) so we can just take the disjoint union *) + let ve1 = check_pat env pat1 in + let ve2 = check_pat env pat2 in + t <: pat1.note; + t <: pat2.note; + disjoint_union env pat.at "duplicate binding for %s in and-pattern" ve1 ve2 and check_pats at env pats ve : val_env = match pats with diff --git a/src/ir_def/freevars.ml b/src/ir_def/freevars.ml index fa52e2c35d3..5ab0d853a13 100644 --- a/src/ir_def/freevars.ml +++ b/src/ir_def/freevars.ml @@ -86,6 +86,7 @@ let rec pat p : td = match p.it with | OptP p | TagP (_, p) -> pat p | AltP (p1, p2) -> pat p1 +- pat p2 + | AndP (p1, p2) -> pat p1 +- pat p2 and pats ps : td = List.(fold_left (+-) M.empty (map pat ps)) diff --git a/src/ir_def/ir.ml b/src/ir_def/ir.ml index 043f2229a17..f423e3042c2 100644 --- a/src/ir_def/ir.ml +++ b/src/ir_def/ir.ml @@ -50,6 +50,7 @@ and pat' = | OptP of pat (* option *) | TagP of Type.lab * pat (* variant *) | AltP of pat * pat (* disjunctive *) + | AndP of pat * pat (* conjunctive *) and pat_field = pat_field' Source.phrase and pat_field' = {name : Type.lab; pat : pat} diff --git a/src/ir_def/ir_utils.ml b/src/ir_def/ir_utils.ml index 880587ce47e..3f150ac552d 100644 --- a/src/ir_def/ir_utils.ml +++ b/src/ir_def/ir_utils.ml @@ -4,6 +4,7 @@ let rec is_irrefutable p = match p.it with | TupP pats -> List.for_all is_irrefutable pats | ObjP pfs -> List.for_all (fun (pf : pat_field) -> is_irrefutable pf.it.pat) pfs | AltP (pat1, _) -> is_irrefutable pat1 + | AndP (pat1, pat2) -> is_irrefutable pat1 && is_irrefutable pat2 | WildP | VarP _ -> true | TagP _ | LitP _ | OptP _ -> false diff --git a/src/ir_def/rename.ml b/src/ir_def/rename.ml index ff11a15eff0..056738271f4 100644 --- a/src/ir_def/rename.ml +++ b/src/ir_def/rename.ml @@ -144,6 +144,10 @@ and pat' rho = function end; let rho' = ids_bind rho is1 in (AltP (pat_subst rho' p1, pat_subst rho' p2), rho') + | AndP (p1, p2) -> + let (p1', rho') = pat rho p1 in + let (p2', rho'') = pat rho' p2 in + (AndP (p1', p2'), rho'') and pats rho ps = match ps with @@ -173,6 +177,8 @@ and pat_subst' rho = function TagP (i, pat_subst rho p) | AltP (p1, p2) -> AltP (pat_subst rho p1, pat_subst rho p2) + | AndP (p1, p2) -> + AndP (pat_subst rho p1, pat_subst rho p2) and pats_subst rho ps = List.map (pat_subst rho) ps diff --git a/src/ir_def/subst_var.ml b/src/ir_def/subst_var.ml index 3819160308d..5b52fdba3bd 100644 --- a/src/ir_def/subst_var.ml +++ b/src/ir_def/subst_var.ml @@ -83,6 +83,7 @@ and pat' rho = function List.compare String.compare is1 is2 = 0 end; ids_bind rho is1 + | AndP (p1, p2) -> pat (pat rho p1) p2 and pats rho ps = List.fold_left pat rho ps diff --git a/src/ir_interpreter/interpret_ir.ml b/src/ir_interpreter/interpret_ir.ml index 53ec87e2945..80d1d9864ac 100644 --- a/src/ir_interpreter/interpret_ir.ml +++ b/src/ir_interpreter/interpret_ir.ml @@ -690,6 +690,7 @@ and declare_pat pat : val_env = | OptP pat1 | TagP (_, pat1) -> declare_pat pat1 | AltP (pat1, _pat2) -> declare_pat pat1 (* pat2 has the same bindings *) + | AndP (pat1, pat2) -> V.Env.adjoin (declare_pat pat1) (declare_pat pat2) and declare_pats pats ve : val_env = match pats with @@ -761,6 +762,9 @@ and match_pat pat v : val_env option = | None -> match_pat pat2 v | some -> some ) + | AndP (pat1, pat2) -> + Option.(bind (match_pat pat1 v) (fun ve1 -> + map (V.Env.adjoin ve1) (match_pat pat2 v))) and match_pats pats vs ve : val_env option = match pats, vs with diff --git a/src/ir_passes/async.ml b/src/ir_passes/async.ml index 51896748dc3..4438da21e8c 100644 --- a/src/ir_passes/async.ml +++ b/src/ir_passes/async.ml @@ -518,6 +518,8 @@ let transform prog = TagP (i, t_pat pat1) | AltP (pat1, pat2) -> AltP (t_pat pat1, t_pat pat2) + | AndP (pat1, pat2) -> + AndP (t_pat pat1, t_pat pat2) and t_typ_bind' tb = { tb with con = t_con tb.con; bound = t_typ tb.bound } diff --git a/src/ir_passes/await.ml b/src/ir_passes/await.ml index 5e7d3bef83d..192e3e6c0b8 100644 --- a/src/ir_passes/await.ml +++ b/src/ir_passes/await.ml @@ -562,6 +562,7 @@ and declare_pat pat exp : exp = | OptP pat1 | TagP (_, pat1) -> declare_pat pat1 exp | AltP (pat1, pat2) -> declare_pat pat1 exp + | AndP (pat1, pat2) -> declare_pat pat1 (declare_pat pat2 exp) and declare_pats pats exp : exp = match pats with @@ -597,6 +598,10 @@ and rename_pat' pat = assert(Freevars.(M.is_empty (pat pat1))); assert(Freevars.(M.is_empty (pat pat2))); (PatEnv.empty,pat.it) + | AndP (pat1, pat2) -> + let (patenv1, pat1') = rename_pat pat1 in + let (patenv2, pat2') = rename_pat pat2 in + (PatEnv.disjoint_union patenv1 patenv2, AndP (pat1', pat2')) and rename_pats pats = match pats with @@ -621,6 +626,8 @@ and define_pat patenv pat : dec list = assert(Freevars.(M.is_empty (pat pat1))); assert(Freevars.(M.is_empty (pat pat2))); [] + | AndP (pat1, pat2) -> + define_pat patenv pat1 @ define_pat patenv pat2 and define_pats patenv (pats : pat list) : dec list = List.concat_map (define_pat patenv) pats diff --git a/src/ir_passes/const.ml b/src/ir_passes/const.ml index 1f5a1ea7edb..0f74fa08173 100644 --- a/src/ir_passes/const.ml +++ b/src/ir_passes/const.ml @@ -78,6 +78,7 @@ let rec pat env p = match p.it with | TupP pats -> List.fold_left pat env pats | ObjP pfs -> List.fold_left pat env (pats_of_obj_pat pfs) | AltP (pat1, _) | OptP pat1 | TagP (_, pat1) -> pat env pat1 + | AndP (pat1, pat2) -> pat (pat env pat1) pat2 let find v env = match M.find_opt v env with | None -> raise (Invalid_argument (Printf.sprintf "Unbound var: %s\n" v)) diff --git a/src/ir_passes/erase_typ_field.ml b/src/ir_passes/erase_typ_field.ml index b78cd79cf58..9c2418e328d 100644 --- a/src/ir_passes/erase_typ_field.ml +++ b/src/ir_passes/erase_typ_field.ml @@ -201,6 +201,8 @@ let transform prog = TagP (i, t_pat pat1) | AltP (pat1, pat2) -> AltP (t_pat pat1, t_pat pat2) + | AndP (pat1, pat2) -> + AndP (t_pat pat1, t_pat pat2) and t_typ_bind' tb = { tb with con = t_con tb.con; bound = t_typ tb.bound } diff --git a/src/ir_passes/tailcall.ml b/src/ir_passes/tailcall.ml index 32b7c41a99d..f0a77331835 100644 --- a/src/ir_passes/tailcall.ml +++ b/src/ir_passes/tailcall.ml @@ -156,6 +156,7 @@ and pat' env = function | OptP p | TagP (_, p) -> pat env p | AltP (p1, _p2) -> pat env p1 (* both bind the same vars, ensured in check_pat *) + | AndP (p1, p2) -> pat (pat env p1) p2 and pats env ps = match ps with diff --git a/src/lowering/desugar.ml b/src/lowering/desugar.ml index 357ed9ab7bd..ed6fca2d20c 100644 --- a/src/lowering/desugar.ml +++ b/src/lowering/desugar.ml @@ -1318,13 +1318,7 @@ and pat' = function | S.OptP p -> I.OptP (pat p) | S.TagP (i, p) -> I.TagP (i.it, pat p) | S.AltP (p1, p2) -> I.AltP (pat p1, pat p2) - | S.AndP (p1, p2) -> - (* TODO: AND-pattern lowering to IR. For the frontend/typecheck - draft PR the IR does not yet have an `AndP` constructor; reach - this arm only if a program containing an and-pattern is - compiled all the way through. *) - ignore (p1, p2); - failwith "and-pattern lowering not yet implemented" + | S.AndP (p1, p2) -> I.AndP (pat p1, pat p2) | S.AnnotP (p, _) | S.ParP p -> pat' p.it diff --git a/test/run/and-pattern-binds.mo b/test/run/and-pattern-binds.mo index 498a157f812..9e7d8d8010c 100644 --- a/test/run/and-pattern-binds.mo +++ b/test/run/and-pattern-binds.mo @@ -18,6 +18,3 @@ debugPrint (debug_show {x3; y3; z3}); let ((#a n) and m) or ((#b n) and m) : { #a : Nat; #b : Nat } = #a 13; debugPrint (debug_show {n; m}); -//SKIP run-ir -//SKIP run-low -//SKIP comp diff --git a/test/run/ok/and-pattern-binds.run-ir.ok b/test/run/ok/and-pattern-binds.run-ir.ok new file mode 100644 index 00000000000..ff7c9726335 --- /dev/null +++ b/test/run/ok/and-pattern-binds.run-ir.ok @@ -0,0 +1,4 @@ +{a = 5; b = 5} +{s = ?7; x = 7} +{x3 = 11; y3 = 11; z3 = 11} +{m = #a(13); n = 13} diff --git a/test/run/ok/and-pattern-binds.run-low.ok b/test/run/ok/and-pattern-binds.run-low.ok new file mode 100644 index 00000000000..ff7c9726335 --- /dev/null +++ b/test/run/ok/and-pattern-binds.run-low.ok @@ -0,0 +1,4 @@ +{a = 5; b = 5} +{s = ?7; x = 7} +{x3 = 11; y3 = 11; z3 = 11} +{m = #a(13); n = 13} diff --git a/test/run/ok/and-pattern-binds.wasm-run.ok b/test/run/ok/and-pattern-binds.wasm-run.ok new file mode 100644 index 00000000000..ff7c9726335 --- /dev/null +++ b/test/run/ok/and-pattern-binds.wasm-run.ok @@ -0,0 +1,4 @@ +{a = 5; b = 5} +{s = ?7; x = 7} +{x3 = 11; y3 = 11; z3 = 11} +{m = #a(13); n = 13} From b351b229826ab4ad927bcca2403fab72a3ab5ca2 Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Thu, 23 Apr 2026 11:32:48 +0200 Subject: [PATCH 05/19] docs(changelog): add Next entry for and-patterns (#6049) --- Changelog.md | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/Changelog.md b/Changelog.md index 15f1e6e20fe..c0899ac8dc4 100644 --- a/Changelog.md +++ b/Changelog.md @@ -1,5 +1,11 @@ # Motoko compiler changelog +## Next + +* motoko (`moc`) + + * feat: and-patterns — `(p1 and p2)` matches when both legs match, binding from both (#6049). + ## 1.6.0 (2026-04-21) * motoko (`moc`) From e7f728d4ec1a712921609448a547390d443f2444 Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Thu, 23 Apr 2026 11:40:12 +0200 Subject: [PATCH 06/19] docs(and-patterns): language-manual section + fundamentals-table row - `doc/md/16-language-manual.md`: add 'And pattern' section after 'Or pattern', modelled on the existing 'Or pattern' wording and noting that sides must bind disjoint identifiers (the key semantic difference from or-patterns). Include the `and`-binds- tighter-than-`or` precedence note so `p1 or p2 and p3` parses unambiguously. Also a tiny wording tweak to the or-pattern section ('the types assigned to it' rather than 'its type in'). - `doc/md/fundamentals/8-pattern-matching.md`: add a table row for the and-pattern mirroring the or-pattern row. Also fix a small typo on the 'refutable/irrefutable' line where the opening `**` for bold was missing. --- doc/md/16-language-manual.md | 12 +++++++++++- doc/md/fundamentals/8-pattern-matching.md | 3 ++- 2 files changed, 13 insertions(+), 2 deletions(-) diff --git a/doc/md/16-language-manual.md b/doc/md/16-language-manual.md index 0766a563972..4c95b5f03dd 100644 --- a/doc/md/16-language-manual.md +++ b/doc/md/16-language-manual.md @@ -1618,7 +1618,17 @@ The or pattern ` or ` is a disjunctive pattern. The result of matching ` or ` against a value is the result of matching ``, if it succeeds, or the result of matching ``, if the first match fails. -An `or`-pattern may contain identifier (``) patterns with the restriction that both alternatives must bind the same set of identifiers. Each identifier's type is the least upper bound of its type in `` and ``. +An `or`-pattern may contain identifier (``) patterns with the restriction that both alternatives must bind the same set of identifiers. Each identifier's type is the least upper bound of the types assigned to it by `` and ``. + +### And pattern + +The and pattern ` and ` is a conjunctive pattern. + +The result of matching ` and ` against a value is the union of the bindings produced by matching `` and then ``, both against the same value. The match fails if either sub-match fails. + +Unlike an `or`-pattern, the two sides of an `and`-pattern must bind *disjoint* sets of identifiers; a name bound in both sides is a type error. + +`and` binds tighter than `or`, so ` or and ` parses as ` or ( and )`. ### Expression declaration diff --git a/doc/md/fundamentals/8-pattern-matching.md b/doc/md/fundamentals/8-pattern-matching.md index bdf77e8b1eb..3c9efdc4e8e 100644 --- a/doc/md/fundamentals/8-pattern-matching.md +++ b/doc/md/fundamentals/8-pattern-matching.md @@ -20,6 +20,7 @@ Motoko supports several types of patterns: | Named | Introduces identifiers into a new scope. | `age`, `x` | | Tuple | Must have at least two components. | `( component0, component1, …​ )` | | Alternative (`or`-pattern) | Match multiple patterns. | `0 or 1` | +| Conjunctive (`and`-pattern) | Match both patterns; bindings combine. | `?x and s` | ## Concepts @@ -29,7 +30,7 @@ Unlike traditional `enum` types in other languages, which define fixed sets of v ### Irrefutable and refutable patterns -Patterns are either refutable** or irrefutable. A refutable pattern can fail to match (like literal patterns or specific variant tags). An irrefutable pattern always matches any value of its type. Examples include the wildcard `_`, simple variable names, or structured patterns (like records or tuples) made only from irrefutable parts. +Patterns are either **refutable** or **irrefutable**. A refutable pattern can fail to match (like literal patterns or specific variant tags). An irrefutable pattern always matches any value of its type. Examples include the wildcard `_`, simple variable names, or structured patterns (like records or tuples) made only from irrefutable parts. ### Singleton types From bfe6a06aadee391eb4e6e4cabf36c09b0f68d614 Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Thu, 23 Apr 2026 12:05:41 +0200 Subject: [PATCH 07/19] test(and-patterns): cover codegen CanFail paths and disjoint-bindings threading MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Extends `and-pattern-binds.mo` from the earlier irrefutable-only coverage with the test cases flagged in the pre-review pass: - **refutable AndP in switch** (`describeOpt`): `?x4` is refutable, so the switch exercises `(^^^)` composition on `CanFail` codes. - **leg-1 failure falls through** (`leftFails`): `(#Ok 42) and s5` — when the refutable first leg fails the next case must catch it. - **leg-2 failure falls through** (`rightFails`): `(#Ok _) and (#Ok 99)` — leg 1 succeeds on any `#Ok`, leg 2 narrows further; when leg 2 fails the fail-continuation must abandon leg 1's partial match and advance. - **AndP inside a function body** (`addBoth`): wraps the switch-AndP in a function. (Direct func-arg AndP would hit the documented M0184 limitation — infer_pat has no scrutinee type to propagate — so we use a switch to enter check_pat instead.) - **AndP inside TupP**: `let ((a7 : Nat) and b7, c7) = (7, "world")`. - **three-way with refutable middle leg** (`peelOpt`): `?y8 and x8 and z8` — exercises the rho threading in `rename.ml` / `subst_var.ml`, where each leg contributes its own bindings to the accumulating environment. The reviewer-suggested 'type-mismatched legs' case was rejected as not a new failure mode: both legs are `check_pat`'d against the same scrutinee type, so an incompatible annotation on either leg is just the standard M0117 `AnnotP` subtype error — not AndP-specific. The analogous 'same-name bindings with different types' IS distinct for `or`-patterns (drives `lub` + `warn_lossy_bind_type`) and is already covered by `test/run/or-pattern-mismatch.mo`. --- test/run/and-pattern-binds.mo | 62 +++++++++++++++++++++++ test/run/ok/and-pattern-binds.run-ir.ok | 11 ++++ test/run/ok/and-pattern-binds.run-low.ok | 11 ++++ test/run/ok/and-pattern-binds.run.ok | 11 ++++ test/run/ok/and-pattern-binds.tc.ok | 1 + test/run/ok/and-pattern-binds.wasm-run.ok | 11 ++++ 6 files changed, 107 insertions(+) create mode 100644 test/run/ok/and-pattern-binds.tc.ok diff --git a/test/run/and-pattern-binds.mo b/test/run/and-pattern-binds.mo index 9e7d8d8010c..999185c94c0 100644 --- a/test/run/and-pattern-binds.mo +++ b/test/run/and-pattern-binds.mo @@ -18,3 +18,65 @@ debugPrint (debug_show {x3; y3; z3}); let ((#a n) and m) or ((#b n) and m) : { #a : Nat; #b : Nat } = #a 13; debugPrint (debug_show {n; m}); +// refutable AndP in a switch — the `?x4` leg is refutable and drives +// the fail-continuation through `(^^^)` on `CanFail` codes. +func describeOpt(o : ?Nat) : Text = + switch o { + case ((?x4) and s4) (debug_show {s4; x4}); + case null "none"; + }; +debugPrint (describeOpt (?42)); +debugPrint (describeOpt null); + +// failing AndP leg falls through to the next case — verifies that the +// fail-continuation threads all the way out to `orsPatternFailure`. +// Tests BOTH leg-positions failing in turn. +type Status = { #Ok : Nat; #Err : Text }; + +// leg-1 fails: `(#Ok 42)` is the refutable side; when it fails the +// whole AndP fails and flow advances to the next case. +func leftFails(s : Status) : Text = + switch s { + case ((#Ok 42) and s5) ("42-left: " # debug_show s5); + case (#Ok n) ("ok " # debug_show n); + case (#Err e) ("err " # e); + }; +debugPrint (leftFails (#Ok 42)); +debugPrint (leftFails (#Ok 7)); +debugPrint (leftFails (#Err "boom")); + +// leg-2 fails: leg 1 `(#Ok _)` accepts any #Ok; leg 2 narrows further. +// When scrutinee is `#Ok 7`, leg 1 succeeds (any #Ok), but leg 2 +// rejects (needs payload 99) — so fail-continuation must cancel leg 1's +// partial match and advance to the next case. +func rightFails(s : Status) : Text = + switch s { + case ((#Ok _) and (#Ok 99)) "99-right"; + case (#Ok n) ("ok " # debug_show n); + case (#Err _) "err"; + }; +debugPrint (rightFails (#Ok 99)); +debugPrint (rightFails (#Ok 7)); + +// AndP inside a function body — direct func-arg AndP would need type +// inference we deliberately reject (infer_pat raises M0184, matching +// AltP's behaviour); a switch lifts the scrutinee into check_pat. +func addBoth(p : Nat) : Nat = + switch p { + case ((x6 : Nat) and y6) (x6 + y6); + }; +debugPrint (debug_show (addBoth 21)); + +// AndP nested inside a TupP +let ((a7 : Nat) and b7, c7) = (7, "world"); +debugPrint (debug_show {a7; b7; c7}); + +// three-way and with a refutable middle leg — exercises rho threading +// in rename/subst (each leg contributes its own bindings). +func peelOpt(o : ?Nat) : Text = + switch o { + case (?y8 and x8 and z8) (debug_show {x8; y8; z8}); + case null "null"; + }; +debugPrint (peelOpt (?11)); +debugPrint (peelOpt null); diff --git a/test/run/ok/and-pattern-binds.run-ir.ok b/test/run/ok/and-pattern-binds.run-ir.ok index ff7c9726335..8025549e3e0 100644 --- a/test/run/ok/and-pattern-binds.run-ir.ok +++ b/test/run/ok/and-pattern-binds.run-ir.ok @@ -2,3 +2,14 @@ {s = ?7; x = 7} {x3 = 11; y3 = 11; z3 = 11} {m = #a(13); n = 13} +{s4 = ?42; x4 = 42} +none +42-left: #Ok(42) +ok 7 +err boom +99-right +ok 7 +42 +{a7 = 7; b7 = 7; c7 = "world"} +{x8 = ?11; y8 = 11; z8 = ?11} +null diff --git a/test/run/ok/and-pattern-binds.run-low.ok b/test/run/ok/and-pattern-binds.run-low.ok index ff7c9726335..8025549e3e0 100644 --- a/test/run/ok/and-pattern-binds.run-low.ok +++ b/test/run/ok/and-pattern-binds.run-low.ok @@ -2,3 +2,14 @@ {s = ?7; x = 7} {x3 = 11; y3 = 11; z3 = 11} {m = #a(13); n = 13} +{s4 = ?42; x4 = 42} +none +42-left: #Ok(42) +ok 7 +err boom +99-right +ok 7 +42 +{a7 = 7; b7 = 7; c7 = "world"} +{x8 = ?11; y8 = 11; z8 = ?11} +null diff --git a/test/run/ok/and-pattern-binds.run.ok b/test/run/ok/and-pattern-binds.run.ok index ff7c9726335..8025549e3e0 100644 --- a/test/run/ok/and-pattern-binds.run.ok +++ b/test/run/ok/and-pattern-binds.run.ok @@ -2,3 +2,14 @@ {s = ?7; x = 7} {x3 = 11; y3 = 11; z3 = 11} {m = #a(13); n = 13} +{s4 = ?42; x4 = 42} +none +42-left: #Ok(42) +ok 7 +err boom +99-right +ok 7 +42 +{a7 = 7; b7 = 7; c7 = "world"} +{x8 = ?11; y8 = 11; z8 = ?11} +null diff --git a/test/run/ok/and-pattern-binds.tc.ok b/test/run/ok/and-pattern-binds.tc.ok new file mode 100644 index 00000000000..5a5c5625478 --- /dev/null +++ b/test/run/ok/and-pattern-binds.tc.ok @@ -0,0 +1 @@ +and-pattern-binds.mo:55.10-55.17: warning [M0146], this pattern is never matched diff --git a/test/run/ok/and-pattern-binds.wasm-run.ok b/test/run/ok/and-pattern-binds.wasm-run.ok index ff7c9726335..8025549e3e0 100644 --- a/test/run/ok/and-pattern-binds.wasm-run.ok +++ b/test/run/ok/and-pattern-binds.wasm-run.ok @@ -2,3 +2,14 @@ {s = ?7; x = 7} {x3 = 11; y3 = 11; z3 = 11} {m = #a(13); n = 13} +{s4 = ?42; x4 = 42} +none +42-left: #Ok(42) +ok 7 +err boom +99-right +ok 7 +42 +{a7 = 7; b7 = 7; c7 = "world"} +{x8 = ?11; y8 = 11; z8 = ?11} +null From 39cc51ac5840390fe8f8d6fb1a189110dcf38183 Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Thu, 23 Apr 2026 15:16:43 +0200 Subject: [PATCH 08/19] test: accept parser-error listing now including `and ` The `test_recovery` expect-test enumerates the syntax-error followup tokens parser.mly emits when recovery kicks in. Adding the `AND` production at `pat_bin` naturally extends that list by one entry (`and (e.g. 'and x')`); promote the new baseline. --- src/mo_frontend/test_recovery.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/mo_frontend/test_recovery.ml b/src/mo_frontend/test_recovery.ml index fc65734ce36..d030c801660 100644 --- a/src/mo_frontend/test_recovery.ml +++ b/src/mo_frontend/test_recovery.ml @@ -293,6 +293,7 @@ let%expect_test "test3" = or (e.g. 'or x') , seplist(,,) (e.g. ', x') : (e.g. ': Int') + and (e.g. 'and x') (unknown location): syntax error [M0001], unexpected token 'private', expected one of token or sequence: } @@ -300,7 +301,8 @@ let%expect_test "test3" = (unknown location): syntax error [M0001], unexpected token 'let', expected one of token or sequence: } - ; seplist(,) (e.g. '; public let x : Int = 0') |}] + ; seplist(,) (e.g. '; public let x : Int = 0') + |}] let%expect_test "test4" = From 91722b38620ca000b36285a4e4169bfaea48508c Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Thu, 23 Apr 2026 15:23:20 +0200 Subject: [PATCH 09/19] tweak test that `and` has lower precedence than tags --- test/run/and-pattern-binds.mo | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/run/and-pattern-binds.mo b/test/run/and-pattern-binds.mo index 999185c94c0..a9e33ff425c 100644 --- a/test/run/and-pattern-binds.mo +++ b/test/run/and-pattern-binds.mo @@ -37,7 +37,7 @@ type Status = { #Ok : Nat; #Err : Text }; // whole AndP fails and flow advances to the next case. func leftFails(s : Status) : Text = switch s { - case ((#Ok 42) and s5) ("42-left: " # debug_show s5); + case (#Ok 42 and s5) ("42-left: " # debug_show s5); case (#Ok n) ("ok " # debug_show n); case (#Err e) ("err " # e); }; From c4b106620c350d472fce0aea6b61ab9f1a21dc1d Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Thu, 23 Apr 2026 16:28:15 +0200 Subject: [PATCH 10/19] and-patterns: dedicated M0260 error code + style polish MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - New error code M0260 (\`lang_utils/error_codes.ml\`): "\`and\`-pattern binds the same variable in both legs". Previously the overlap check emitted M0189 (which covers or-pattern-alternatives binding mismatches) — reusing it conflated two distinct conditions. typing.ml now raises M0260 at the three overlap sites (live \`check_pat\` val-env, live \`check_pat_typ_dec\` typ-env, and the commented-out speculative \`infer_pat\` arm). The fail-baseline for \`test/fail/and-pattern-overlap-case.mo\` is updated. - Codegen style (both backends): collapse two sequential \`let\` bindings in \`fill_pat\` AndP to a single tuple-bind \`let code1, code2 = fill_pat env ae p1, fill_pat env ae p2 in\` and drop the parens on \`let set_i, get_i = new_local env \"and_scrut\"\`. Also refactor \`destruct_const_pat\` AndP to monadic form \`Option.bind (... p1 ...) (fun ae' -> ... ae' p2 ...)\`. All behaviourally equivalent; just reads cleaner. --- src/codegen/compile_classical.ml | 10 ++++------ src/codegen/compile_enhanced.ml | 10 ++++------ src/lang_utils/error_codes.ml | 1 + src/mo_frontend/typing.ml | 6 +++--- test/fail/ok/and-pattern-overlap-case.tc-human.ok | 2 +- test/fail/ok/and-pattern-overlap-case.tc.ok | 2 +- 6 files changed, 14 insertions(+), 17 deletions(-) diff --git a/src/codegen/compile_classical.ml b/src/codegen/compile_classical.ml index 5de26f05ad0..0544f88c621 100644 --- a/src/codegen/compile_classical.ml +++ b/src/codegen/compile_classical.ml @@ -13167,9 +13167,8 @@ and fill_pat env ae pat : patternCode = orElse (CannotFail get_i ^^^ code1) (CannotFail get_i ^^^ code2) | AndP (p1, p2) -> - let code1 = fill_pat env ae p1 in - let code2 = fill_pat env ae p2 in - let (set_i, get_i) = new_local env "and_scrut" in + let code1, code2 = fill_pat env ae p1, fill_pat env ae p2 in + let set_i, get_i = new_local env "and_scrut" in CannotFail set_i ^^^ (CannotFail get_i ^^^ code1) ^^^ (CannotFail get_i ^^^ code2) @@ -13449,9 +13448,8 @@ and destruct_const_pat ae pat const : VarEnv.t option = match pat.it with if l = None then destruct_const_pat ae p2 const else l | AndP (p1, p2) -> - (match destruct_const_pat ae p1 const with - | None -> None - | Some ae' -> destruct_const_pat ae' p2 const) + Option.bind (destruct_const_pat ae p1 const) (fun ae' -> + destruct_const_pat ae' p2 const) | TupP ps -> let cs = match const with (_, Const.Tuple cs) -> cs | (_, Const.Unit) -> [] | _ -> assert false in let go ae p c = match ae with diff --git a/src/codegen/compile_enhanced.ml b/src/codegen/compile_enhanced.ml index 08d139ce08e..ba2cbdf066b 100644 --- a/src/codegen/compile_enhanced.ml +++ b/src/codegen/compile_enhanced.ml @@ -13497,9 +13497,8 @@ and fill_pat env ae pat : patternCode = are available. Stash the scrutinee once, feed it to each leg in sequence. `(^^^)` threads failure through — either leg's failure cancels the whole match. *) - let code1 = fill_pat env ae p1 in - let code2 = fill_pat env ae p2 in - let (set_i, get_i) = new_local env "and_scrut" in + let code1, code2 = fill_pat env ae p1, fill_pat env ae p2 in + let set_i, get_i = new_local env "and_scrut" in CannotFail set_i ^^^ (CannotFail get_i ^^^ code1) ^^^ (CannotFail get_i ^^^ code2) @@ -13780,9 +13779,8 @@ and destruct_const_pat ae pat const : VarEnv.t option = match pat.it with else l | AndP (p1, p2) -> (* Both legs must accept; fold bindings left-to-right. *) - (match destruct_const_pat ae p1 const with - | None -> None - | Some ae' -> destruct_const_pat ae' p2 const) + Option.bind (destruct_const_pat ae p1 const) (fun ae' -> + destruct_const_pat ae' p2 const) | TupP ps -> let cs = match const with Const.Tuple cs -> cs | Const.Unit -> [] | _ -> assert false in let go ae p c = match ae with diff --git a/src/lang_utils/error_codes.ml b/src/lang_utils/error_codes.ml index b6c3bacafda..0ea3db4e274 100644 --- a/src/lang_utils/error_codes.ml +++ b/src/lang_utils/error_codes.ml @@ -217,6 +217,7 @@ let error_codes : (string * string option) list = "M0257", None; (* Misplaced uninitialized dec *) "M0258", None; (* Uninitialized `let` with non : pattern *) "M0259", None; (* Uninitialized dec requires type annotation *) + "M0260", None; (* `and`-pattern binds the same variable in both legs *) ] (** Message codes that can be both used as warnings and errors *) diff --git a/src/mo_frontend/typing.ml b/src/mo_frontend/typing.ml index 612a8e79c6d..d3a07b58515 100644 --- a/src/mo_frontend/typing.ml +++ b/src/mo_frontend/typing.ml @@ -3308,7 +3308,7 @@ and infer_pat' name_types env pat : T.typ * Scope.val_env = display_typ_expand t2; let overlap = T.Env.filter (fun k _ -> T.Env.mem k ve2) ve1 in if not (T.Env.is_empty overlap) then - error env pat.at "M0???" "and-pattern binds the same variable in both legs"; + error env pat.at "M0260" "and-pattern binds the same variable in both legs"; T.glb ~src_fields:env.srcs t1 t2, T.Env.union (fun _ v _ -> Some v) ve1 ve2*) | AnnotP ({it = VarP id; _} as pat1, typ) when name_types -> let t = check_typ env typ in @@ -3474,7 +3474,7 @@ and check_pat_aux' env t t_orig pat val_kind : Scope.val_env = let ve2 = check_pat env t pat2 in T.Env.iter (fun k _ -> if T.Env.mem k ve2 then - error env pat.at "M0189" + error env pat.at "M0260" "variable `%s` bound in both branches of and-pattern" k ) ve1; T.Env.merge (fun _ o1 o2 -> match o1, o2 with @@ -3607,7 +3607,7 @@ and check_pat_typ_dec env t pat : Scope.typ_env = let te2 = check_pat_typ_dec env t pat2 in T.Env.iter (fun k _ -> if T.Env.mem k te2 then - error env pat.at "M0189" + error env pat.at "M0260" "type identifier `%s` bound in both branches of and-pattern" k ) te1; T.Env.merge (fun _ o1 o2 -> match o1, o2 with diff --git a/test/fail/ok/and-pattern-overlap-case.tc-human.ok b/test/fail/ok/and-pattern-overlap-case.tc-human.ok index 7300b559688..de7866d8f53 100644 --- a/test/fail/ok/and-pattern-overlap-case.tc-human.ok +++ b/test/fail/ok/and-pattern-overlap-case.tc-human.ok @@ -1,4 +1,4 @@ -error[M0189]: variable `x` bound in both branches of and-pattern +error[M0260]: variable `x` bound in both branches of and-pattern ┌─ and-pattern-overlap-case.mo:5:11 5 │ case ((x : Nat) and (x : Nat)) x; │ ^^^^^^^^^^^^^^^^^^^^^^^ diff --git a/test/fail/ok/and-pattern-overlap-case.tc.ok b/test/fail/ok/and-pattern-overlap-case.tc.ok index 8fff287b6d5..0d0382b9001 100644 --- a/test/fail/ok/and-pattern-overlap-case.tc.ok +++ b/test/fail/ok/and-pattern-overlap-case.tc.ok @@ -1 +1 @@ -and-pattern-overlap-case.mo:5.11-5.34: type error [M0189], variable `x` bound in both branches of and-pattern +and-pattern-overlap-case.mo:5.11-5.34: type error [M0260], variable `x` bound in both branches of and-pattern From 6d25f82120164bd1697083b6565dba5fdb9f3718 Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Thu, 23 Apr 2026 16:30:17 +0200 Subject: [PATCH 11/19] test: fix stale M0189 reference in and-pattern-overlap-case comment The inline comment still pointed at M0189; the check in typing.ml's AndP arm now emits M0260 (the dedicated and-pattern overlap code added in the previous commit). --- test/fail/and-pattern-overlap-case.mo | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/fail/and-pattern-overlap-case.mo b/test/fail/and-pattern-overlap-case.mo index 715aa61490b..0e6473bab4a 100644 --- a/test/fail/and-pattern-overlap-case.mo +++ b/test/fail/and-pattern-overlap-case.mo @@ -1,5 +1,5 @@ // overlap inside a switch case — `gather_pat` is not the first line of -// defence here, so this hits the M0189 check we added in `check_pat` +// defence here, so this hits the M0260 check we added in `check_pat` func f(v : Nat) : Nat = switch v { case ((x : Nat) and (x : Nat)) x; From 7a757525d8e0dde8ee387a12e1c570adad1bfbe8 Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Thu, 23 Apr 2026 16:56:11 +0200 Subject: [PATCH 12/19] coverage(and-patterns): proper InAnd1 context + dedicated test MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Replaces the previous stub (delegate to leg-1, documented as unsound for refutability) with a proper intersection-semantics check. New `InAnd1 of ctxt * pat * T.typ` ctxt wraps the first-leg match; on succeed, the second leg runs against the narrowed desc under the outer ctxt; on fail, the whole AndP fails for that desc slice. Non- covering content in pat2 (e.g. a narrower tag than pat1 admitted) surfaces as uncovered via the normal flow — no special casing. Also drops one spurious M0146 'this pattern is never matched' that the stub was emitting against a reachable `(#Ok _) and (#Ok 99)` case in and-pattern-binds.mo. Adds test/run/and-pattern-coverage.mo: three switches that each combine a refutable AndP case with later cases so that the ctxt flow must propagate pat1's narrowing correctly to subsequent cases. None emits warnings under the new logic, confirming the fix. --- src/mo_frontend/coverage.ml | 22 ++++++++++---- test/run/and-pattern-coverage.mo | 47 +++++++++++++++++++++++++++++ test/run/ok/and-pattern-binds.tc.ok | 1 - 3 files changed, 63 insertions(+), 7 deletions(-) create mode 100644 test/run/and-pattern-coverage.mo delete mode 100644 test/run/ok/and-pattern-binds.tc.ok diff --git a/src/mo_frontend/coverage.ml b/src/mo_frontend/coverage.ml index d86f9e985d3..f3e5bfde25c 100644 --- a/src/mo_frontend/coverage.ml +++ b/src/mo_frontend/coverage.ml @@ -30,6 +30,7 @@ type ctxt = | InObj of ctxt * desc LabMap.t * string * pat_field list * T.field list | InAlt1 of ctxt * region * pat * T.typ | InAlt2 of ctxt * region + | InAnd1 of ctxt * pat * T.typ | InCase of region * case list * T.typ type sets = @@ -268,12 +269,15 @@ let rec match_pat ctxt desc pat t sets = | AltP (pat1, pat2) -> sets.alts <- AtSet.add pat1.at (AtSet.add pat2.at sets.alts); match_pat (InAlt1 (ctxt, pat1.at, pat2, t)) desc pat1 t sets - | AndP (pat1, _pat2) -> - (* TODO: proper coverage for and-patterns. For now approximate by - treating the pattern as equivalent to its first leg — unsound - for refutability but adequate for a draft that only exercises - the frontend + typecheck. *) - match_pat ctxt desc pat1 t sets + | AndP (pat1, pat2) -> + (* AndP accepts v iff both pat1 and pat2 accept v. + Match pat1 first under an InAnd1 context; on success, continue + with pat2 on the narrowed `desc` under the outer context; on + failure, the whole AndP fails for that desc-slice. Non-covering + content in pat2 (e.g. a variant tag incompatible with what pat1 + already admitted) surfaces as uncovered via the normal ctxt + flow — no special casing needed. *) + match_pat (InAnd1 (ctxt, pat2, t)) desc pat1 t sets | AnnotP (pat1, _) | ParP pat1 -> match_pat ctxt desc pat1 t sets @@ -338,6 +342,9 @@ and succeed ctxt desc sets : bool = | InAlt2 (ctxt', at2) -> sets.reached_alts <- AtSet.add at2 sets.reached_alts; succeed ctxt' desc sets + | InAnd1 (ctxt', pat2, t) -> + (* pat1 accepted `desc`; now pat2 must also accept it *) + match_pat ctxt' desc pat2 t sets | InCase (at, cases, _t) -> sets.reached_cases <- AtSet.add at sets.reached_cases; skip cases sets @@ -364,6 +371,9 @@ and fail ctxt desc sets : bool = match_pat (InAlt2 (ctxt', pat2.at)) desc pat2 t sets | InAlt2 (ctxt', at2) -> fail ctxt' desc sets + | InAnd1 (ctxt', _pat2, _t) -> + (* pat1 rejected `desc`; AndP rejects too *) + fail ctxt' desc sets | InCase (at, [], t) -> T.span t = Some 0 || not (T.inhabited t) || (sets.missing <- desc::sets.missing; false) diff --git a/test/run/and-pattern-coverage.mo b/test/run/and-pattern-coverage.mo new file mode 100644 index 00000000000..322ec4b7c3e --- /dev/null +++ b/test/run/and-pattern-coverage.mo @@ -0,0 +1,47 @@ +// Coverage-check regression test for and-patterns. Each switch here +// is exhaustive and every case is reachable — `coverage.ml`'s +// `InAnd1` context must: +// 1) not spuriously flag any case as redundant, +// 2) not leave any refined-desc path uncovered, +// 3) propagate a refutable leg's narrowing correctly to the next +// case so the fall-through branch is seen as useful. + +type Status = { #Ok : Nat; #Err : Text }; + +// leg 1 refutable (narrows to #Ok 42), leg 2 irrefutable (any Status); +// fall-through to `#Ok n` and `#Err _` must stay reachable +func a(s : Status) : Nat = + switch s { + case ((#Ok 42) and _) 42; + case (#Ok n) n; + case (#Err _) 0; + }; +ignore a (#Ok 42); ignore a (#Ok 7); ignore a (#Err "x"); + +// leg 1 irrefutable, leg 2 refutable narrower than leg 1 — the AndP +// matches exactly where leg 2 would, but the InAnd1 flow must still +// reach both legs and leave the remaining `#Ok n` / `#Err _` slices +// uncovered-for-this-case (consumed by later cases) +func b(s : Status) : Nat = + switch s { + case (_ and (#Ok 99)) 99; + case (#Ok n) n; + case (#Err _) 0; + }; +ignore b (#Ok 99); ignore b (#Ok 1); ignore b (#Err "y"); + +// both legs refutable on the same shape — vacuous (accepts `#Ok 99`), +// pat1's complement still flows through to case 2 (`#Err _`) +// covering the rest of the type +func c(s : Status) : Nat = + switch s { + case ((#Ok _) and (#Ok 99)) 99; + case (#Ok n) n; + case (#Err _) 0; + }; +ignore c (#Ok 99); ignore c (#Ok 1); ignore c (#Err "z"); + +//SKIP run +//SKIP run-ir +//SKIP run-low +//SKIP comp diff --git a/test/run/ok/and-pattern-binds.tc.ok b/test/run/ok/and-pattern-binds.tc.ok deleted file mode 100644 index 5a5c5625478..00000000000 --- a/test/run/ok/and-pattern-binds.tc.ok +++ /dev/null @@ -1 +0,0 @@ -and-pattern-binds.mo:55.10-55.17: warning [M0146], this pattern is never matched From 1b332d74a3e443d72d505ae67af2b6614ce330e3 Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Thu, 23 Apr 2026 17:11:16 +0200 Subject: [PATCH 13/19] and-patterns: dedicated M0261 for 'cannot infer', stop reusing M0184 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit M0184 is registered as 'Cannot infer or-pattern' — reusing it for and-patterns in `infer_pat`'s AndP arm conflated two distinct semantics (users looking up M0184 would see or-pattern docs while hitting the error on an and-pattern). Introduce M0261 dedicated to and-patterns and retarget the infer_pat arm at it. --- src/lang_utils/error_codes.ml | 1 + src/mo_frontend/typing.ml | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/src/lang_utils/error_codes.ml b/src/lang_utils/error_codes.ml index 0ea3db4e274..01af5554863 100644 --- a/src/lang_utils/error_codes.ml +++ b/src/lang_utils/error_codes.ml @@ -218,6 +218,7 @@ let error_codes : (string * string option) list = "M0258", None; (* Uninitialized `let` with non : pattern *) "M0259", None; (* Uninitialized dec requires type annotation *) "M0260", None; (* `and`-pattern binds the same variable in both legs *) + "M0261", None; (* Cannot infer and-pattern, please use an annotation *) ] (** Message codes that can be both used as warnings and errors *) diff --git a/src/mo_frontend/typing.ml b/src/mo_frontend/typing.ml index d3a07b58515..793d97b031e 100644 --- a/src/mo_frontend/typing.ml +++ b/src/mo_frontend/typing.ml @@ -3295,7 +3295,7 @@ and infer_pat' name_types env pat : T.typ * Scope.val_env = if not env.pre then T.Env.(iter (fun k t1 -> warn_lossy_bind_type env pat.at k t1 (find k ve2))) ve1; t, T.Env.merge (fun _ -> Lib.Option.map2 (T.lub ~src_fields:env.srcs)) ve1 ve2*) | AndP (pat1, pat2) -> - error env pat.at "M0184" + error env pat.at "M0261" "cannot infer the type of this and-pattern, please add a type annotation"; (*let t1, ve1 = infer_pat env pat1 in let t2, ve2 = infer_pat env pat2 in From 1355414ea239500733e54022550140d4f4708967 Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Thu, 23 Apr 2026 18:26:54 +0200 Subject: [PATCH 14/19] test: exercise M0261 'cannot infer and-pattern' via func-arg AndP Direct and-pattern in function-arg position has no scrutinee-type context to check against, so it hits `infer_pat`'s AndP arm and raises M0261. Mirrors the pattern of `test/fail/or-pattern-diff.mo` (which covers M0184 for the or-pattern counterpart). --- test/fail/and-pattern-infer.mo | 5 +++++ test/fail/ok/and-pattern-infer.tc-human.ok | 4 ++++ test/fail/ok/and-pattern-infer.tc-human.ret.ok | 1 + test/fail/ok/and-pattern-infer.tc.ok | 1 + test/fail/ok/and-pattern-infer.tc.ret.ok | 1 + 5 files changed, 12 insertions(+) create mode 100644 test/fail/and-pattern-infer.mo create mode 100644 test/fail/ok/and-pattern-infer.tc-human.ok create mode 100644 test/fail/ok/and-pattern-infer.tc-human.ret.ok create mode 100644 test/fail/ok/and-pattern-infer.tc.ok create mode 100644 test/fail/ok/and-pattern-infer.tc.ret.ok diff --git a/test/fail/and-pattern-infer.mo b/test/fail/and-pattern-infer.mo new file mode 100644 index 00000000000..fe28df4e356 --- /dev/null +++ b/test/fail/and-pattern-infer.mo @@ -0,0 +1,5 @@ +// and-pattern in a context that needs type inference (no scrutinee +// type to propagate to `check_pat`) — hits the dedicated M0261 +// "cannot infer and-pattern" code. +func f(x and y) : Nat = x; +ignore f 3 diff --git a/test/fail/ok/and-pattern-infer.tc-human.ok b/test/fail/ok/and-pattern-infer.tc-human.ok new file mode 100644 index 00000000000..54046d74524 --- /dev/null +++ b/test/fail/ok/and-pattern-infer.tc-human.ok @@ -0,0 +1,4 @@ +error[M0261]: cannot infer the type of this and-pattern, please add a type annotation + ┌─ and-pattern-infer.mo:4:8 + 4 │ func f(x and y) : Nat = x; + │ ^^^^^^^ diff --git a/test/fail/ok/and-pattern-infer.tc-human.ret.ok b/test/fail/ok/and-pattern-infer.tc-human.ret.ok new file mode 100644 index 00000000000..69becfa16f9 --- /dev/null +++ b/test/fail/ok/and-pattern-infer.tc-human.ret.ok @@ -0,0 +1 @@ +Return code 1 diff --git a/test/fail/ok/and-pattern-infer.tc.ok b/test/fail/ok/and-pattern-infer.tc.ok new file mode 100644 index 00000000000..20010dcd2ab --- /dev/null +++ b/test/fail/ok/and-pattern-infer.tc.ok @@ -0,0 +1 @@ +and-pattern-infer.mo:4.8-4.15: type error [M0261], cannot infer the type of this and-pattern, please add a type annotation diff --git a/test/fail/ok/and-pattern-infer.tc.ret.ok b/test/fail/ok/and-pattern-infer.tc.ret.ok new file mode 100644 index 00000000000..69becfa16f9 --- /dev/null +++ b/test/fail/ok/and-pattern-infer.tc.ret.ok @@ -0,0 +1 @@ +Return code 1 From 753404cacef4dc14fdbfa69874434e916930a779 Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Fri, 24 Apr 2026 11:56:46 +0200 Subject: [PATCH 15/19] refactor(and-patterns): rigour in check_ir and M0260 parity in let-context MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - `check_ir.ml`: add `verify_pair` helper (cheap iter + predicate, no raise/catch) and use it to enforce disjoint AndP leg bindings in `check_pat`; rewrite the misleading "(frontend enforces)" comments at both `gather_pat` and `check_pat` sites so the actual enforcer is named — matters for separate compilation where IR is read from disk. - `typing.ml`: `gather_pat_aux`'s AndP arm now gathers each leg against the outer scope independently and enforces disjoint leg-contributions with the AndP-specific M0260 (matching `check_pat`). Previously, `gather_id` would fire the generic M0051 first in let-context, so M0260 was only reachable from `case`. - `test/fail/ok/and-pattern-overlap.{tc,tc-human}.ok`: regenerated — now shows M0260 with the AndP's full region. Co-Authored-By: Claude Opus 4.7 (1M context) --- src/ir_def/check_ir.ml | 18 +++++++++++++---- src/mo_frontend/typing.ml | 21 +++++++++++++++++++- test/fail/ok/and-pattern-overlap.tc-human.ok | 6 +++--- test/fail/ok/and-pattern-overlap.tc.ok | 2 +- 4 files changed, 38 insertions(+), 9 deletions(-) diff --git a/src/ir_def/check_ir.ml b/src/ir_def/check_ir.ml index 76c5cc6246c..ee36865da30 100644 --- a/src/ir_def/check_ir.ml +++ b/src/ir_def/check_ir.ml @@ -149,6 +149,12 @@ let disjoint_union env at fmt env1 env2 = try T.Env.disjoint_union env1 env2 with T.Env.Clash k -> error env at fmt k +(* Error on the first key of env1 that falsifies `ok k env2`, naming + that key via `fmt`. A cheap iter + predicate test, without the + raise/catch machinery of `disjoint_union`. *) +let verify_pair env at fmt ok env1 env2 = + T.Env.iter (fun k _ -> if not (ok k env2) then error env at fmt k) env1 + (* Types *) (* FIX ME: these error reporting functions are eager and will construct unnecessary type strings !*) @@ -1038,7 +1044,9 @@ and gather_pat env const ve0 pat : val_env = let common i1 i2 = { typ = lub env i1.typ i2.typ; loc_known = i1.loc_known && i2.loc_known; const = i1.const && i2.const } in T.Env.merge (fun _ -> Lib.Option.map2 common) ve1 ve2 | AndP (pat1, pat2) -> - (* legs contribute disjoint bindings (frontend enforces) *) + (* pre-population only; check_pat below rejects overlapping + bindings via verify_pair, so IR loaded from disk is + validated without trusting the frontend *) go (go ve pat1) pat2 | OptP pat1 | TagP (_, pat1) -> @@ -1091,13 +1099,15 @@ and check_pat env pat : val_env = let common i1 i2 = { typ = lub env i1.typ i2.typ; loc_known = i1.loc_known && i2.loc_known; const = i1.const && i2.const } in T.Env.merge (fun _ -> Lib.Option.map2 common) ve1 ve2 | AndP (pat1, pat2) -> - (* both legs must accept the scrutinee; bindings are disjoint - (frontend enforces) so we can just take the disjoint union *) + (* both legs must accept the scrutinee; verify_pair enforces + disjoint bindings without trusting the frontend *) let ve1 = check_pat env pat1 in let ve2 = check_pat env pat2 in t <: pat1.note; t <: pat2.note; - disjoint_union env pat.at "duplicate binding for %s in and-pattern" ve1 ve2 + verify_pair env pat.at "duplicate binding for %s in and-pattern" + (fun k ve2 -> not (T.Env.mem k ve2)) ve1 ve2; + T.Env.adjoin ve1 ve2 and check_pats at env pats ve : val_env = match pats with diff --git a/src/mo_frontend/typing.ml b/src/mo_frontend/typing.ml index 793d97b031e..2b7d6894c57 100644 --- a/src/mo_frontend/typing.ml +++ b/src/mo_frontend/typing.ml @@ -4645,7 +4645,26 @@ and gather_pat_aux env val_kind scope pat : Scope.t = | ObjP pfs -> List.fold_left (gather_pat_field env) scope pfs | TagP (_, pat1) | AltP (pat1, _) | OptP pat1 | AnnotP (pat1, _) | ParP pat1 -> gather_pat env scope pat1 - | AndP (pat1, pat2) -> gather_pat env (gather_pat env scope pat1) pat2 + | AndP (pat1, pat2) -> + (* Gather each leg against the outer scope independently, then + enforce disjoint leg-contributions with the AndP-specific M0260 + diagnostic (mirrors check_pat). Otherwise `gather_id` would fire + the generic M0051 in let-context on a duplicate. *) + let scope1 = gather_pat env scope pat1 in + let scope2 = gather_pat env scope pat2 in + T.Env.iter (fun k _ -> + if not (T.Env.mem k scope.Scope.val_env) + && T.Env.mem k scope2.Scope.val_env then + error env pat.at "M0260" + "variable `%s` bound in both branches of and-pattern" k) + scope1.Scope.val_env; + T.Env.iter (fun k _ -> + if not (T.Env.mem k scope.Scope.typ_env) + && T.Env.mem k scope2.Scope.typ_env then + error env pat.at "M0260" + "type identifier `%s` bound in both branches of and-pattern" k) + scope1.Scope.typ_env; + Scope.adjoin scope1 scope2 and gather_pat_field env scope pf : Scope.t = let val_kind = kind_of_field_pattern pf in diff --git a/test/fail/ok/and-pattern-overlap.tc-human.ok b/test/fail/ok/and-pattern-overlap.tc-human.ok index b5335042490..7f678dccba3 100644 --- a/test/fail/ok/and-pattern-overlap.tc-human.ok +++ b/test/fail/ok/and-pattern-overlap.tc-human.ok @@ -1,4 +1,4 @@ -error[M0051]: duplicate definition for a in block - ┌─ and-pattern-overlap.mo:1:20 +error[M0260]: variable `a` bound in both branches of and-pattern + ┌─ and-pattern-overlap.mo:1:5 1 │ let (a : Nat) and (a : Nat) = 5; - │ ^ + │ ^^^^^^^^^^^^^^^^^^^^^^^ diff --git a/test/fail/ok/and-pattern-overlap.tc.ok b/test/fail/ok/and-pattern-overlap.tc.ok index 097a41ab3d6..fc331b6ef41 100644 --- a/test/fail/ok/and-pattern-overlap.tc.ok +++ b/test/fail/ok/and-pattern-overlap.tc.ok @@ -1 +1 @@ -and-pattern-overlap.mo:1.20-1.21: type error [M0051], duplicate definition for a in block +and-pattern-overlap.mo:1.5-1.28: type error [M0260], variable `a` bound in both branches of and-pattern From 3e730ff7cd67232234eedd3e631a1b33cb091f22 Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Fri, 24 Apr 2026 11:59:38 +0200 Subject: [PATCH 16/19] test(and-patterns): cover type-mismatched legs MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `let (x : Nat) and (y : Text) = 5` — expects a clean M0117 subtype error pointing at the offending leg, per the review's missing-test list. Co-Authored-By: Claude Opus 4.7 (1M context) --- test/fail/and-pattern-typemismatch.mo | 6 ++++++ test/fail/ok/and-pattern-typemismatch.tc-human.ok | 7 +++++++ test/fail/ok/and-pattern-typemismatch.tc-human.ret.ok | 1 + test/fail/ok/and-pattern-typemismatch.tc.ok | 4 ++++ test/fail/ok/and-pattern-typemismatch.tc.ret.ok | 1 + 5 files changed, 19 insertions(+) create mode 100644 test/fail/and-pattern-typemismatch.mo create mode 100644 test/fail/ok/and-pattern-typemismatch.tc-human.ok create mode 100644 test/fail/ok/and-pattern-typemismatch.tc-human.ret.ok create mode 100644 test/fail/ok/and-pattern-typemismatch.tc.ok create mode 100644 test/fail/ok/and-pattern-typemismatch.tc.ret.ok diff --git a/test/fail/and-pattern-typemismatch.mo b/test/fail/and-pattern-typemismatch.mo new file mode 100644 index 00000000000..b575e880d1c --- /dev/null +++ b/test/fail/and-pattern-typemismatch.mo @@ -0,0 +1,6 @@ +// Legs with incompatible types: `(x : Nat)` and `(y : Text)` cannot +// both accept a `Nat 5` — expect a clean subtype error naming the +// offending leg, not a confused message. +let (x : Nat) and (y : Text) = 5; +ignore x; +ignore y diff --git a/test/fail/ok/and-pattern-typemismatch.tc-human.ok b/test/fail/ok/and-pattern-typemismatch.tc-human.ok new file mode 100644 index 00000000000..fe06e527fde --- /dev/null +++ b/test/fail/ok/and-pattern-typemismatch.tc-human.ok @@ -0,0 +1,7 @@ +error[M0117]: pattern of type + Text +cannot consume expected type + Nat + ┌─ and-pattern-typemismatch.mo:4:20 + 4 │ let (x : Nat) and (y : Text) = 5; + │ ^^^^^^^^ diff --git a/test/fail/ok/and-pattern-typemismatch.tc-human.ret.ok b/test/fail/ok/and-pattern-typemismatch.tc-human.ret.ok new file mode 100644 index 00000000000..69becfa16f9 --- /dev/null +++ b/test/fail/ok/and-pattern-typemismatch.tc-human.ret.ok @@ -0,0 +1 @@ +Return code 1 diff --git a/test/fail/ok/and-pattern-typemismatch.tc.ok b/test/fail/ok/and-pattern-typemismatch.tc.ok new file mode 100644 index 00000000000..f6b6359144f --- /dev/null +++ b/test/fail/ok/and-pattern-typemismatch.tc.ok @@ -0,0 +1,4 @@ +and-pattern-typemismatch.mo:4.20-4.28: type error [M0117], pattern of type + Text +cannot consume expected type + Nat diff --git a/test/fail/ok/and-pattern-typemismatch.tc.ret.ok b/test/fail/ok/and-pattern-typemismatch.tc.ret.ok new file mode 100644 index 00000000000..69becfa16f9 --- /dev/null +++ b/test/fail/ok/and-pattern-typemismatch.tc.ret.ok @@ -0,0 +1 @@ +Return code 1 From 844603ebad08a3c810993ce476986111bcca8eb7 Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Fri, 24 Apr 2026 12:16:10 +0200 Subject: [PATCH 17/19] docs(and-patterns): fix stale M0184 comment and clarify check-mode MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The comment on the switch-lifted AndP test named the wrong error code (M0184 is AltP's; AndP uses its own M0261 since 1b332d74a) and framed inference-position rejection as blanket policy. In reality it only bites when FuncE has to synthesise its own domain (top-level `func f` desugars to LetD with no outer type); any checking-mode context — HOF arguments, class members, `let f : T -> U = func(...) = ...` — accepts AndP in func-arg position via check_pat's M0260-enforcing path. Co-Authored-By: Claude Opus 4.7 (1M context) --- test/run/and-pattern-binds.mo | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/test/run/and-pattern-binds.mo b/test/run/and-pattern-binds.mo index a9e33ff425c..9d0094e575c 100644 --- a/test/run/and-pattern-binds.mo +++ b/test/run/and-pattern-binds.mo @@ -58,9 +58,12 @@ func rightFails(s : Status) : Text = debugPrint (rightFails (#Ok 99)); debugPrint (rightFails (#Ok 7)); -// AndP inside a function body — direct func-arg AndP would need type -// inference we deliberately reject (infer_pat raises M0184, matching -// AltP's behaviour); a switch lifts the scrutinee into check_pat. +// AndP inside a function body. A top-level `func addBoth(AndP) : Nat = +// …` desugars to `let addBoth = func …`, putting the FuncE into +// inference mode — which rejects AndP with M0261. We lift the scrutinee +// into check_pat via a switch here; equivalently, `let f : Nat -> Nat = +// func(a and b) = …` or any HOF/class position that supplies the +// expected Func type also works. func addBoth(p : Nat) : Nat = switch p { case ((x6 : Nat) and y6) (x6 + y6); From 28229fdedbeb804d0c653400586e021d7f8d4656 Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Fri, 24 Apr 2026 12:18:40 +0200 Subject: [PATCH 18/19] refactor(check_ir): use verify_pair in check_pats sibling-disjointness MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Drops the last `disjoint_union env at fmt …` call in `check_ir.ml` (the TupP/ObjP sibling-check) in favour of an explicit verify_pair + T.Env.adjoin, matching the AndP site. Rigorous without raise/catch. Co-Authored-By: Claude Opus 4.7 (1M context) --- src/ir_def/check_ir.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/ir_def/check_ir.ml b/src/ir_def/check_ir.ml index ee36865da30..39ef4aab9d9 100644 --- a/src/ir_def/check_ir.ml +++ b/src/ir_def/check_ir.ml @@ -1114,8 +1114,9 @@ and check_pats at env pats ve : val_env = | [] -> ve | pat::pats' -> let ve1 = check_pat env pat in - let ve' = disjoint_union env at "duplicate binding for %s in pattern" ve ve1 in - check_pats at env pats' ve' + verify_pair env at "duplicate binding for %s in pattern" + (fun k ve -> not (T.Env.mem k ve)) ve1 ve; + check_pats at env pats' (T.Env.adjoin ve ve1) and check_pat_fields env t = List.iter (check_pat_field env t) From 5c8380c2b685253d8c20d1b5d9ca5eb911c7b42e Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Fri, 24 Apr 2026 14:51:29 +0200 Subject: [PATCH 19/19] feat(and-patterns): propagate one-leg inference into the other leg MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Before: `infer_pat'` rejected every AndP with M0261, forcing both legs to be annotated in inference-position contexts (top-level `func f(pat)`, bare lambda as LetD RHS, etc.). Now: if at least one leg is `is_explicit_pat`, use `infer_pat` on that leg and `check_pat` the other against the inferred type; if both are explicit, take the `glb`. M0261 only fires when *neither* leg carries enough annotation. Disjointness enforcement is unchanged — walks `ve1` and emits M0260 on any key present in `ve2`. - `test/run/and-pattern-infer.mo` — new positive test covering left-only / right-only / both-annotated / let-context / TupP-nested. - `test/fail/and-pattern-infer.mo` — comment clarified; cross-refs the new positive test. `.ok` regenerated via `make accept`. Co-Authored-By: Claude Opus 4.7 (1M context) --- src/mo_frontend/typing.ml | 51 +++++++++++++++------- test/fail/and-pattern-infer.mo | 7 +-- test/fail/ok/and-pattern-infer.tc-human.ok | 4 +- test/fail/ok/and-pattern-infer.tc.ok | 2 +- test/run/and-pattern-infer.mo | 25 +++++++++++ 5 files changed, 68 insertions(+), 21 deletions(-) create mode 100644 test/run/and-pattern-infer.mo diff --git a/src/mo_frontend/typing.ml b/src/mo_frontend/typing.ml index 2b7d6894c57..c4c651ea9f6 100644 --- a/src/mo_frontend/typing.ml +++ b/src/mo_frontend/typing.ml @@ -3295,21 +3295,42 @@ and infer_pat' name_types env pat : T.typ * Scope.val_env = if not env.pre then T.Env.(iter (fun k t1 -> warn_lossy_bind_type env pat.at k t1 (find k ve2))) ve1; t, T.Env.merge (fun _ -> Lib.Option.map2 (T.lub ~src_fields:env.srcs)) ve1 ve2*) | AndP (pat1, pat2) -> - error env pat.at "M0261" - "cannot infer the type of this and-pattern, please add a type annotation"; - (*let t1, ve1 = infer_pat env pat1 in - let t2, ve2 = infer_pat env pat2 in - (* Both legs must accept the scrutinee, so the inferred type is the - intersection/glb. No bindings may overlap. *) - if not (T.compatible t1 t2) then - error env pat.at "M0104" - "pattern branches have incompatible types,\nleft consumes%a\nright consumes%a" - display_typ_expand t1 - display_typ_expand t2; - let overlap = T.Env.filter (fun k _ -> T.Env.mem k ve2) ve1 in - if not (T.Env.is_empty overlap) then - error env pat.at "M0260" "and-pattern binds the same variable in both legs"; - T.glb ~src_fields:env.srcs t1 t2, T.Env.union (fun _ v _ -> Some v) ve1 ve2*) + (* If at least one leg is explicit enough to infer, lift the other + leg into check-mode against that type. If both are explicit, + take the glb of their inferred types (both must accept the + scrutinee). Only reject with M0261 when neither leg carries + enough annotation to drive inference. *) + let t, ve1, ve2 = + match is_explicit_pat pat1, is_explicit_pat pat2 with + | true, true -> + let t1, ve1 = infer_pat false env pat1 in + let t2, ve2 = infer_pat false env pat2 in + if not (T.compatible t1 t2) then + error env pat.at "M0104" + "and-pattern legs have incompatible types,\nleft accepts%a\nright accepts%a" + display_typ_expand t1 + display_typ_expand t2; + T.glb ~src_fields:env.srcs t1 t2, ve1, ve2 + | true, false -> + let t1, ve1 = infer_pat false env pat1 in + let ve2 = check_pat env t1 pat2 in + t1, ve1, ve2 + | false, true -> + let t2, ve2 = infer_pat false env pat2 in + let ve1 = check_pat env t2 pat1 in + t2, ve1, ve2 + | false, false -> + error env pat.at "M0261" + "cannot infer the type of this and-pattern, please add a type annotation" + in + T.Env.iter (fun k _ -> + if T.Env.mem k ve2 then + error env pat.at "M0260" + "variable `%s` bound in both branches of and-pattern" k + ) ve1; + t, T.Env.merge (fun _ o1 o2 -> match o1, o2 with + | Some v, _ | _, Some v -> Some v + | None, None -> None) ve1 ve2 | AnnotP ({it = VarP id; _} as pat1, typ) when name_types -> let t = check_typ env typ in T.Named (id.it, t), check_pat env t pat1 diff --git a/test/fail/and-pattern-infer.mo b/test/fail/and-pattern-infer.mo index fe28df4e356..645f61376ca 100644 --- a/test/fail/and-pattern-infer.mo +++ b/test/fail/and-pattern-infer.mo @@ -1,5 +1,6 @@ -// and-pattern in a context that needs type inference (no scrutinee -// type to propagate to `check_pat`) — hits the dedicated M0261 -// "cannot infer and-pattern" code. +// and-pattern in inference position with *neither* leg annotated — +// hits the dedicated M0261 "cannot infer and-pattern" code. Compare +// `test/run/and-pattern-infer.mo`, which exercises the inference +// path that now succeeds when at least one leg is explicit. func f(x and y) : Nat = x; ignore f 3 diff --git a/test/fail/ok/and-pattern-infer.tc-human.ok b/test/fail/ok/and-pattern-infer.tc-human.ok index 54046d74524..7103f13db3d 100644 --- a/test/fail/ok/and-pattern-infer.tc-human.ok +++ b/test/fail/ok/and-pattern-infer.tc-human.ok @@ -1,4 +1,4 @@ error[M0261]: cannot infer the type of this and-pattern, please add a type annotation - ┌─ and-pattern-infer.mo:4:8 - 4 │ func f(x and y) : Nat = x; + ┌─ and-pattern-infer.mo:5:8 + 5 │ func f(x and y) : Nat = x; │ ^^^^^^^ diff --git a/test/fail/ok/and-pattern-infer.tc.ok b/test/fail/ok/and-pattern-infer.tc.ok index 20010dcd2ab..5d39d1a1eae 100644 --- a/test/fail/ok/and-pattern-infer.tc.ok +++ b/test/fail/ok/and-pattern-infer.tc.ok @@ -1 +1 @@ -and-pattern-infer.mo:4.8-4.15: type error [M0261], cannot infer the type of this and-pattern, please add a type annotation +and-pattern-infer.mo:5.8-5.15: type error [M0261], cannot infer the type of this and-pattern, please add a type annotation diff --git a/test/run/and-pattern-infer.mo b/test/run/and-pattern-infer.mo new file mode 100644 index 00000000000..a1355ddd9c1 --- /dev/null +++ b/test/run/and-pattern-infer.mo @@ -0,0 +1,25 @@ +// AndP in inference position: previously rejected wholesale with +// M0261; now accepted when at least one leg carries enough type +// information to drive inference (`is_explicit_pat` true on a leg). + +// Left leg annotated — pat1 drives inference, pat2 checked against +// the inferred Nat. +func fL((x : Nat) and y) : Nat = x + y; +assert (fL 3 == 6); + +// Right leg annotated — symmetric. +func fR(x and (y : Nat)) : Nat = x + y; +assert (fR 4 == 8); + +// Both legs annotated: AndP's type is the glb of the two. Here both +// are Nat, so Nat. +func fB((x : Nat) and (y : Nat)) : Nat = x + y; +assert (fB 5 == 10); + +// let-context, left-annotated: `a` typed as Nat, `b` checked against Nat. +let ((a : Nat) and b) = 7; +assert (a + b == 14); + +// TupP surrounding AndP: each leg gets to drive its own inference. +let ((p : Nat) and q, (r : Nat) and s) = (11, 13); +assert (p + q + r + s == 48);