diff --git a/lib/check.ml b/lib/check.ml
index fcae594f..8b0aa8a3 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -4108,6 +4108,17 @@ let box loc (e : Tast.expr) : Tast.expr =
   | Types.LArray _ ->
     no_dyn_yet loc ~into:true e.Tast.ty ""
 
+(* Every dyn an expectation opened ([expect]'s dyn arm), by the node that
+   opened it, and the box: what lets a caller that asked for a typed value
+   see that the value was a dyn, whichever opening the want picked. Keyed by
+   identity and held weakly, so it is gone with the tree. *)
+module Opened = Ephemeron.K1.Make (struct
+    type t = Tast.expr
+    let equal = ( == )
+    let hash = Hashtbl.hash
+  end)
+let opened_by_want : Tast.expr Opened.t = Opened.create 16
+
 let unbox loc (want : Types.t) (e : Tast.expr) : Tast.expr =
   let need sym ty = rt loc ty sym [ e ] in
   match want with
@@ -4485,6 +4496,10 @@ let expect ctx loc ~want (got : Tast.expr) =
       | Types.Dyn, Types.Dyn -> got
       | Types.Dyn, Types.Option t -> box_option ctx loc t got
       | Types.Dyn, _ -> box loc got
+      | Types.Option t, Types.Dyn when not (is_nil_lit got) ->
+        let opened = unbox_option ctx loc t got in
+        Opened.replace opened_by_want opened got;
+        opened
       | Types.Option t, Types.Dyn -> unbox_option ctx loc t got
       (* A bare T has no None to become, and this nil is one the checker can
          actually see — the literal, written right where the mismatch is.
@@ -4496,7 +4511,10 @@ let expect ctx loc ~want (got : Tast.expr) =
            or to dyn itself; wrap the type in Option, or keep the value dyn"
           (Types.to_string w)
       | _, Types.Dyn when Types.fits ~expected:w ~actual:Types.Dyn -> got
-      | _, Types.Dyn -> unbox loc w got
+      | _, Types.Dyn ->
+        let opened = unbox loc w got in
+        Opened.replace opened_by_want opened got;
+        opened
       (* Implicit widening, and this single arm is the whole of its surface.
          [expect] is called by every site that annotates and by nothing else,
          so an argument, a return, a let or defonce with a type, a struct field
@@ -5357,11 +5375,21 @@ let arm_failed :
    the dyn one opened — whichever is written first. *)
 let not_kept = "check/arm-not-kept"
 
-let opened_dyn (v : Tast.expr) =
+let rec opened_dyn (v : Tast.expr) =
   match v.Tast.e with
-  | Tast.Prim (Tast.Rt ("flan_dyn_need_i64" | "flan_dyn_need_f64"), [ inner ])
-    when Types.equal inner.Tast.ty Types.Dyn -> Some inner
-  | _ -> None
+  (* A block — a match arm's body — opened its last form. *)
+  | Tast.Do (_ :: _ as xs) ->
+    let rec split = function
+      | [ l ] -> ([], l)
+      | x :: r -> let i, l = split r in (x :: i, l)
+      | [] -> assert false
+    in
+    let init, last = split xs in
+    Option.map
+      (fun (box : Tast.expr) ->
+         { v with Tast.e = Tast.Do (init @ [ box ]); ty = Types.Dyn })
+      (opened_dyn last)
+  | _ -> Opened.find_opt opened_by_want v
 
 
 (* A Vec or a Map parameter is a copy of the caller's header — Odin's rule —
@@ -13988,6 +14016,25 @@ and join_pair ctx (a : Tast.expr) (y : Ast.expr) (d : Loc.diag) =
      | Some pair -> pair
      | None -> raise (Loc.Error d))
 
+(* [y] checked at [w] in a trial, and a refusal kept ([arm_failed]) so the
+   same operand asked again at the same type, in the same scope, is refused
+   without being walked: a chain of these nested in their second operands is
+   asked once per level above it. *)
+and trial_at ctx (y : Ast.expr) (w : Types.t) =
+  match
+    List.find_opt
+      (fun (n, (sc, r), w', _) ->
+         n == y && r == ctx.ret && Types.equal w' w && same_scope sc ctx.scope)
+      (Hashtbl.find_all arm_failed y.Ast.loc)
+  with
+  | Some (_, _, _, d) -> Error d
+  | None ->
+    (match trial ctx (fun () -> check ctx ~want:w y) with
+     | Ok b -> Ok b
+     | Error d ->
+       Hashtbl.add arm_failed y.Ast.loc (y, (ctx.scope, ctx.ret), w, d);
+       Error d)
+
 and binary ctx ?(dyn_ok = false) ?(join = true) name loc ~want args =
   match args with
   | [ x; y ] ->
@@ -14034,9 +14081,7 @@ and binary ctx ?(dyn_ok = false) ?(join = true) name loc ~want args =
       let at_a =
         if a.Tast.ty = Types.Dyn then None
         else
-          match trial ctx (fun () -> check ctx ~want:a.Tast.ty y) with
-          | Ok b' -> Some (Ok b')
-          | Error d -> Some (Error d)
+          Some (trial_at ctx y a.Tast.ty)
       in
       match at_a with
       | Some (Ok b') ->
@@ -14066,7 +14111,7 @@ and binary ctx ?(dyn_ok = false) ?(join = true) name loc ~want args =
         (match
            match at_a with
            | Some (Error d) -> Error d
-           | _ -> trial ctx (fun () -> check ctx ~want:a.Tast.ty y)
+           | _ -> trial_at ctx y a.Tast.ty
          with
          | Ok b' -> a, b'
          | Error d ->
@@ -14078,10 +14123,16 @@ and binary ctx ?(dyn_ok = false) ?(join = true) name loc ~want args =
     end
     else begin
       let a = check ctx ?want x in
-      match trial ctx (fun () -> check ctx ~want:a.Tast.ty y) with
+      match trial_at ctx y a.Tast.ty with
       | Ok b -> a, b
       | Error d ->
-        if join && reconsiderable d then join_pair ctx a y d
+        (* The join moves [a] to something wider, and [a] already has the
+           type asked of the whole: that can only be refused, so y is not
+           walked on its own terms to find it out. *)
+        let doomed =
+          match want with Some w -> Types.equal a.Tast.ty w | None -> false
+        in
+        if join && reconsiderable d && not doomed then join_pair ctx a y d
         else raise (Loc.Error d)
     end
   | _ -> fail loc "%s takes two arguments" name
diff --git a/test/programs/dyn-opened.flan b/test/programs/dyn-opened.flan
new file mode 100644
index 00000000..529b3db5
--- /dev/null
+++ b/test/programs/dyn-opened.flan
@@ -0,0 +1,25 @@
+;;;; A dyn beside a typed value is compared, added and joined as a dyn, in
+;;;; either order, whichever conversion asking for the typed value would have
+;;;; opened it with — a bool compared with a dyn int is false, not a trap.
+
+(defn as-dyn [d dyn] dyn d)
+(defn eqb [b bool d dyn] bool (= b d))
+(defn eqi [b i64 d dyn] bool (= b d))
+(defn addf [b f64 d dyn] dyn (+ b d))
+(defn addi [b i64 d dyn] dyn (+ b d))
+(defn mb [o (Option i32) b bool d dyn] dyn (let [v (match o (Some q) b None d)] v))
+(defn mb2 [o (Option i32) b bool d dyn] dyn (let [v (match o None d (Some q) b)] v))
+(defn ib [c bool b bool d dyn] dyn (let [v (if c b d)] v))
+(defn ib2 [c bool b bool d dyn] dyn (let [v (if c d b)] v))
+
+(defn main [] i32
+  (println (eqb true (as-dyn 1)))
+  (println (eqb true (as-dyn true)))
+  (println (eqi 1 (as-dyn 1.0)))
+  (println (addi 1 (as-dyn 1.5)))
+  (println (addf 1.0 (as-dyn 2)))
+  (println (mb None true (as-dyn 5)))
+  (println (mb2 None true (as-dyn 5)))
+  (println (ib false true (as-dyn 5)))
+  (println (ib2 true true (as-dyn 5)))
+  0)
diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml
index a470865d..af5a600d 100644
--- a/test/test_acceptance.ml
+++ b/test/test_acceptance.ml
@@ -590,6 +590,11 @@ let () =
       "programs/return-defer.flan" rd_out;
     outputs ~x86:true "a return computes its value before its defers, x86"
       "programs/return-defer.flan" rd_out;
+    (* A dyn opened by the other operand's or arm's type is seen as a dyn. *)
+    let do_out = "false\ntrue\ntrue\n2.5\n3\n5\n5\n5\n5\n" in
+    outputs "a dyn beside a typed value stays a dyn" "programs/dyn-opened.flan" do_out;
+    outputs ~x86:true "a dyn beside a typed value stays a dyn, x86"
+      "programs/dyn-opened.flan" do_out;
     (* An arm is checked at the other arm's type first. *)
     let aw_out =
       "2147483648\n2147483648\n10000000000\n2147483648\n1.5\n2147483648\n\
diff --git a/test/test_flan.ml b/test/test_flan.ml
index da911778..c186c9dd 100644
--- a/test/test_flan.ml
+++ b/test/test_flan.ml
@@ -8061,6 +8061,34 @@ let () =
        "(if c p (do (println 1) 7))", "f [bool u8] u8");
       ("a match's nil arm first", "[o (Option i32) p (Option i64)]",
        "(match o None nil (Some z) p)", "f [(Option i32) (Option i64)] (Option i64)") ]);
+  (* Thirty deep, each level's first try refused: a chain of matches whose
+     last arm is wider, and sums nested in their second operands. *)
+  List.iter
+    (fun (what, src) ->
+       let t0 = Unix.gettimeofday () in
+       (match checked src with
+        | _ -> ()
+        | exception Loc.Error { Loc.dmsg; _ } -> check (what ^ ": " ^ dmsg) false);
+       check (what ^ " checks fast") (Unix.gettimeofday () -. t0 < 3.0))
+    (let nest f = let rec go k e = if k = 0 then e else go (k - 1) (f e) in go 30 in
+     [ ("thirty matches whose last arm is wider",
+        "(defn f [o (Option i32) a i64 b i32] i64 (let [v "
+        ^ nest (Printf.sprintf "(match o (Some q) (+ q 1) None (+ b %s))") "a"
+        ^ "] v))");
+       ("thirty matches with the narrow arm last",
+        "(defn f [o (Option i32) a i64 b i32] i64 (let [v "
+        ^ nest (Printf.sprintf "(match o None b (Some q) (+ b %s))") "a"
+        ^ "] v))");
+       ("thirty matches over a dyn at the bottom",
+        "(defn f [o (Option i32) d dyn b i32] dyn (let [v "
+        ^ nest (Printf.sprintf "(match o (Some q) q None (+ b %s))") "d"
+        ^ "] v))");
+       ("thirty sums nested in their second operands",
+        "(defn f [a i64 b i32] i64 (let [v "
+        ^ nest (Printf.sprintf "(+ b %s)") "a" ^ "] v))") ]);
+  rejects_check "an Option compared with a dyn, as before"
+    ~needle:"(Option i64) does not cross into dyn yet"
+    "(defn eqo [b (Option i64) d dyn] bool (= b d))\n(defn main [] ())";
   rejects_check "nil beside a string, as before"
     ~needle:"string"
     "(defn f [c bool s string] string (let [v (if c s nil)] v))\n(defn main [] ())";