diff --git a/Changelog.md b/Changelog.md
index 71247083a83..e4846ba522a 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -4,6 +4,7 @@
 
 * motoko (`moc`)
 
+  * feat: and-patterns — `(p1 and p2)` matches when both legs match, binding from both (#6049).
   * feat: Add null-coalescing operator `??` (#5722).
     `e1 ?? e2` evaluates to the unwrapped contents of `e1` when `e1` is `?v`,
     otherwise to `e2`. The right-hand side is evaluated lazily (short-circuit).
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 `<pat1> or <pat2>` is a disjunctive pattern.
 
 The result of matching `<pat1> or <pat2>` against a value is the result of matching `<pat1>`, if it succeeds, or the result of matching `<pat2>`, if the first match fails.
 
-An `or`-pattern may contain identifier (`<id>`) 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 `<pat1>` and `<pat2>`.
+An `or`-pattern may contain identifier (`<id>`) 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 `<pat1>` and `<pat2>`.
+
+### And pattern
+
+The and pattern `<pat1> and <pat2>` is a conjunctive pattern.
+
+The result of matching `<pat1> and <pat2>` against a value is the union of the bindings produced by matching `<pat1>` and then `<pat2>`, 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 `<pat1> or <pat2> and <pat3>` parses as `<pat1> or (<pat2> and <pat3>)`.
 
 ### Expression declaration
 
diff --git a/doc/md/examples/grammar.txt b/doc/md/examples/grammar.txt
index 530d2093d84..c150f14c7c3 100644
--- a/doc/md/examples/grammar.txt
+++ b/doc/md/examples/grammar.txt
@@ -320,6 +320,7 @@
 <pat_bin> ::= 
     <pat_un>
     <pat_bin> 'or' <pat_bin>
+    <pat_bin> 'and' <pat_bin>
     <pat_bin> ':' <typ>
 
 <pat> ::= 
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
 
diff --git a/src/codegen/compile_classical.ml b/src/codegen/compile_classical.ml
index 563bef527e5..0544f88c621 100644
--- a/src/codegen/compile_classical.ml
+++ b/src/codegen/compile_classical.ml
@@ -13166,6 +13166,12 @@ and fill_pat env ae pat : patternCode =
       CannotFail set_i ^^^
       orElse (CannotFail get_i ^^^ code1)
              (CannotFail get_i ^^^ code2)
+  | AndP (p1, p2) ->
+      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)
 
 and alloc_pat_local env ae pat =
   let d = Freevars.pat pat in
@@ -13441,6 +13447,9 @@ 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) ->
+    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 269e355b340..ba2cbdf066b 100644
--- a/src/codegen/compile_enhanced.ml
+++ b/src/codegen/compile_enhanced.ml
@@ -13492,6 +13492,16 @@ 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, 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)
 
 and alloc_pat_local env ae pat =
   let d = Freevars.pat pat in
@@ -13767,6 +13777,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) ->
+    (* Both legs must accept; fold bindings left-to-right. *)
+    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/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/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..39ef4aab9d9 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 !*)
@@ -1037,6 +1043,11 @@ 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) ->
+      (* 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) ->
       go ve pat1
@@ -1087,14 +1098,25 @@ 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; 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;
+    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
   | [] -> 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)
 
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/js/astjs.ml b/src/js/astjs.ml
index 884046bc4a5..9f28005ec39 100644
--- a/src/js/astjs.ml
+++ b/src/js/astjs.ml
@@ -587,6 +587,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/lang_utils/error_codes.ml b/src/lang_utils/error_codes.ml
index b6c3bacafda..01af5554863 100644
--- a/src/lang_utils/error_codes.ml
+++ b/src/lang_utils/error_codes.ml
@@ -217,6 +217,8 @@ let error_codes : (string * string option) list =
     "M0257", None; (* Misplaced uninitialized dec *)
     "M0258", None; (* Uninitialized `let` with non <id> : <typ> 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/lowering/desugar.ml b/src/lowering/desugar.ml
index b2da68cdde8..e9d088a6f3d 100644
--- a/src/lowering/desugar.ml
+++ b/src/lowering/desugar.ml
@@ -1324,6 +1324,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) -> I.AndP (pat p1, pat p2)
   | S.AnnotP (p, _)
   | S.ParP p -> pat' p.it
 
diff --git a/src/mo_def/arrange.ml b/src/mo_def/arrange.ml
index abd5608d97d..66378258462 100644
--- a/src/mo_def/arrange.ml
+++ b/src/mo_def/arrange.ml
@@ -169,6 +169,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 40d457383fd..2c335bbe7dc 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..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,6 +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) ->
+    (* 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
@@ -332,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
@@ -358,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/src/mo_frontend/definedness.ml b/src/mo_frontend/definedness.ml
index 846bed12265..54b3e424df5 100644
--- a/src/mo_frontend/definedness.ml
+++ b/src/mo_frontend/definedness.ml
@@ -157,6 +157,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 51e47f640df..6e21b055f92 100644
--- a/src/mo_frontend/parser.mly
+++ b/src/mo_frontend/parser.mly
@@ -940,6 +940,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/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 <pat_bin> (e.g. 'or x')
       , seplist(<pat_bin>,,) (e.g. ', x')
       : <typ> (e.g. ': Int')
+      and <pat_bin> (e.g. 'and x')
 
     (unknown location): syntax error [M0001], unexpected token 'private', expected one of token or <phrase> sequence:
       }
@@ -300,7 +301,8 @@ let%expect_test "test3" =
 
     (unknown location): syntax error [M0001], unexpected token 'let', expected one of token or <phrase> sequence:
       }
-      ; seplist(<dec_field>,<semicolon>) (e.g. '; public let x : Int = 0') |}] 
+      ; seplist(<dec_field>,<semicolon>) (e.g. '; public let x : Int = 0')
+    |}] 
 
 
 let%expect_test "test4" =
diff --git a/src/mo_frontend/typing.ml b/src/mo_frontend/typing.ml
index ea57daac11c..c4c651ea9f6 100644
--- a/src/mo_frontend/typing.ml
+++ b/src/mo_frontend/typing.ml
@@ -1176,6 +1176,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 =
@@ -1433,6 +1434,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
 
@@ -3290,6 +3294,43 @@ 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) ->
+    (* 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
@@ -3447,6 +3488,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 "M0260"
+          "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
@@ -3568,6 +3622,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 "M0260"
+          "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 =
@@ -3664,6 +3730,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
@@ -4599,6 +4666,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 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/src/mo_interpreter/interpret.ml b/src/mo_interpreter/interpret.ml
index 9ee7f4d5f19..cbe5428322c 100644
--- a/src/mo_interpreter/interpret.ml
+++ b/src/mo_interpreter/interpret.ml
@@ -845,6 +845,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
@@ -935,6 +936,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)))
   | AnnotP (pat1, _)
   | ParP pat1 ->
     match_pat pat1 v
diff --git a/test/fail/and-pattern-infer.mo b/test/fail/and-pattern-infer.mo
new file mode 100644
index 00000000000..645f61376ca
--- /dev/null
+++ b/test/fail/and-pattern-infer.mo
@@ -0,0 +1,6 @@
+// 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/and-pattern-overlap-case.mo b/test/fail/and-pattern-overlap-case.mo
new file mode 100644
index 00000000000..0e6473bab4a
--- /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 M0260 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/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-infer.tc-human.ok b/test/fail/ok/and-pattern-infer.tc-human.ok
new file mode 100644
index 00000000000..7103f13db3d
--- /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:5:8
+  5 │  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..5d39d1a1eae
--- /dev/null
+++ b/test/fail/ok/and-pattern-infer.tc.ok
@@ -0,0 +1 @@
+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/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
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..de7866d8f53
--- /dev/null
+++ b/test/fail/ok/and-pattern-overlap-case.tc-human.ok
@@ -0,0 +1,4 @@
+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-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..0d0382b9001
--- /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 [M0260], 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..7f678dccba3
--- /dev/null
+++ b/test/fail/ok/and-pattern-overlap.tc-human.ok
@@ -0,0 +1,4 @@
+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-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..fc331b6ef41
--- /dev/null
+++ b/test/fail/ok/and-pattern-overlap.tc.ok
@@ -0,0 +1 @@
+and-pattern-overlap.mo:1.5-1.28: type error [M0260], variable `a` bound in both branches of and-pattern
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/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
diff --git a/test/run/and-pattern-binds.mo b/test/run/and-pattern-binds.mo
new file mode 100644
index 00000000000..9d0094e575c
--- /dev/null
+++ b/test/run/and-pattern-binds.mo
@@ -0,0 +1,85 @@
+//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});
+
+// 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. 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);
+  };
+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/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/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);
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..8025549e3e0
--- /dev/null
+++ b/test/run/ok/and-pattern-binds.run-ir.ok
@@ -0,0 +1,15 @@
+{a = 5; b = 5}
+{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
new file mode 100644
index 00000000000..8025549e3e0
--- /dev/null
+++ b/test/run/ok/and-pattern-binds.run-low.ok
@@ -0,0 +1,15 @@
+{a = 5; b = 5}
+{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
new file mode 100644
index 00000000000..8025549e3e0
--- /dev/null
+++ b/test/run/ok/and-pattern-binds.run.ok
@@ -0,0 +1,15 @@
+{a = 5; b = 5}
+{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.wasm-run.ok b/test/run/ok/and-pattern-binds.wasm-run.ok
new file mode 100644
index 00000000000..8025549e3e0
--- /dev/null
+++ b/test/run/ok/and-pattern-binds.wasm-run.ok
@@ -0,0 +1,15 @@
+{a = 5; b = 5}
+{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