A dyn opened in any value position of an operand or an arm makes it meet as a dyn, found by the one walk of value positions the frame-escape check also uses

lib/check.ml

@@ -3944,26 +3944,11 @@ let refuse_frame_escapes (f : Tast.fn) =
        else String.capitalize_ascii who)
       verb (what hit) target whose who fix
   in
-  let rec tails (e : Tast.expr) =
-    match e.Tast.e with
-    | Tast.Do es | Tast.Let (_, es) | Tast.WithAlloc (_, es)
-    | Tast.Handled (_, es) ->
-      (match List.rev es with x :: _ -> tails x | [] -> ())
-    (* A restart clause is a branch of this function whose value is the
-       form's value when that restart is taken. *)
-    | Tast.RestartCase (cs, body) ->
-      List.iter
-        (fun (c : Tast.rclause) ->
-           match List.rev c.Tast.rbody with x :: _ -> tails x | [] -> ())
-        cs;
-      tails body
-    | Tast.If (_, a, b) -> tails a; tails b
-    | Tast.Match (_, arms) ->
-      List.iter
-        (fun (a : Tast.arm) ->
-           match List.rev a.Tast.abody with x :: _ -> tails x | [] -> ())
-        arms
-    | _ ->
+  (* Every value position of the body, walked by [Tast.iter_tails]: a
+     restart clause is a branch of this function whose value is the form's
+     value when that restart is taken, and it is on that list. *)
+  let tails =
+    Tast.iter_tails (fun (e : Tast.expr) ->
       Option.iter
         (fail ~verb:"returns" ~target:""
            ~fix_slice:(fun c ->
@@ -3976,7 +3961,7 @@ let refuse_frame_escapes (f : Tast.fn) =
                else
                  "Return the value, of type " ^ t
                  ^ ", instead of its address: drop the addr"))
-        (escapes 0 e)
+        (escapes 0 e))
   in
   (* Only a store into the global itself can be fixed by changing the
      global's type; for a field, an element or a push, the value's type
@@ -4119,6 +4104,15 @@ module Opened = Ephemeron.K1.Make (struct
   end)
 let opened_by_want : Tast.expr Opened.t = Opened.create 16
 
+(* What an [expect] mismatch found, by the refusal: the type a caller that
+   skipped a join can still name the way the join would have. *)
+module Found = Ephemeron.K1.Make (struct
+    type t = Loc.diag
+    let equal = ( == )
+    let hash = Hashtbl.hash
+  end)
+let mismatch_found : Types.t Found.t = Found.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
@@ -4560,10 +4554,14 @@ let expect ctx loc ~want (got : Tast.expr) =
          numbers, and it is on this message rather than beside it because a
          reader who has just been told i64 and i32 are different types needs
          to be told, in the same breath, which direction needed nothing. *)
+      (try
          Loc.failk "check/type-mismatch" loc "expected %s, found %s%s%s"
            (Types.to_string w) (Types.to_string got.Tast.ty)
            (numeric_note ~want:w ~got:got.Tast.ty)
            (const_note ctx.env ~want:w ~got:got.Tast.ty)
+       with Loc.Error d ->
+         Found.replace mismatch_found d got.Tast.ty;
+         raise (Loc.Error d))
 
 (* Something a [break] may not jump out of, named so the refusal can say which.
    See [lentry]: it is a barrier and not a blanket refusal, so a loop written
@@ -5375,21 +5373,25 @@ let arm_failed :
    the dyn one opened — whichever is written first. *)
 let not_kept = "check/arm-not-kept"
 
-let rec opened_dyn (v : Tast.expr) =
-  match v.Tast.e with
-  (* 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
+let to_dyn ctx (x : Tast.expr) = expect ctx x.Tast.loc ~want:(Some Types.Dyn) x
+
+let opened_dyn ~(box : Tast.expr -> Tast.expr) (v : Tast.expr) =
+  (* An opening is a value position of its own, whatever shape the
+     conversion built. *)
+  let stop x = Opened.mem opened_by_want x in
+  let any = ref false in
+  Tast.iter_tails ~stop (fun x -> if stop x then any := true) v;
+  if not !any then None
+  else
+    (* Every value position meets at dyn: an opened one is put back to the
+       box it opened, and any other is boxed. *)
+    Some
+      (Tast.map_tails ~stop ~ty:Types.Dyn
+         (fun x ->
+            match Opened.find_opt opened_by_want x with
+            | Some b -> b
+            | None -> box x)
+         v)
 
 
 (* A Vec or a Map parameter is a copy of the caller's header — Odin's rule —
@@ -7571,7 +7573,7 @@ and check_if_once ctx ~tail ?want loc c t e =
         in
         match at_then () with
         | Ok v ->
-          (match opened_dyn v with
+          (match opened_dyn ~box:(to_dyn ctx) v with
            | Some box -> Some (Types.Dyn, box)
            | None -> Some (t.Tast.ty, v))
         | Error _ when adapts e -> None
@@ -9125,7 +9127,7 @@ and check_match ctx ?(tail = false) ?want loc scrutinee arms =
                in
                match at_join () with
                | Ok b ->
-                 (match opened_dyn b with
+                 (match opened_dyn ~box:(to_dyn ctx) b with
                   | Some box -> want := Some Types.Dyn; box
                   | None -> b)
                | Error d ->
@@ -14085,7 +14087,7 @@ and binary ctx ?(dyn_ok = false) ?(join = true) name loc ~want args =
       in
       match at_a with
       | Some (Ok b') ->
-        (match opened_dyn b' with Some box -> a, box | None -> a, b')
+        (match opened_dyn ~box:(to_dyn ctx) b' with Some box -> a, box | None -> a, b')
       | _ ->
       let b = check ctx y in
       (* Nothing dyn about this pair after all, so it is put back the way the
@@ -14133,7 +14135,20 @@ and binary ctx ?(dyn_ok = false) ?(join = true) name loc ~want args =
           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)
+        else
+          (* Doomed: said the way the join would have been refused — the
+             pair at the wider type, at this form — when y's own refusal
+             names the wider type it found. *)
+          match want, (if doomed then Found.find_opt mismatch_found d else None) with
+          | Some w, Some found
+            when String.equal d.Loc.dloc.Loc.file y.Ast.loc.Loc.file
+                 && d.Loc.dloc = y.Ast.loc ->
+            (match Types.join w found with
+             | Some j when not (Types.equal j w) ->
+               ignore (expect ctx loc ~want:(Some w) (mk loc j Tast.Unit));
+               raise (Loc.Error d)
+             | _ -> raise (Loc.Error d))
+          | _ -> raise (Loc.Error d)
     end
   | _ -> fail loc "%s takes two arguments" name
 

lib/tast.ml

@@ -471,6 +471,44 @@ let is_watch_guard (c : expr) =
   | Prim (Ne, [ { e = Prim (Rt s, _); _ }; _ ]) -> String.equal s watch_begin
   | _ -> false
 
+(* The value positions of an expression: the forms whose value is the
+   expression's value — a block's last form, both arms of an [if], every
+   arm of a [match] and of a [restart-case]. Everything that asks "what does
+   this expression answer with" walks these, so a form that carries a value
+   through from one of its parts is added here once. [map_tails ~ty] rebuilds
+   the expression with each value position replaced by [f] of it and every
+   form on the way given [ty]; a position that never arrives (its type
+   Never) is left alone unless [all]. A form [stop] answers yes for is taken
+   as a value position whole, not looked into. *)
+let rec map_tails ?(all = false) ?(stop = fun _ -> false) ?ty (f : expr -> expr)
+    (e : expr) : expr =
+  let go = map_tails ~all ~stop ?ty f in
+  let last es =
+    match List.rev es with
+    | x :: rest -> List.rev (go x :: rest)
+    | [] -> es
+  in
+  let retype k =
+    let t = match ty with Some t -> t | None -> e.ty in
+    { e with e = k; ty = (if e.ty = Types.Never then e.ty else t) }
+  in
+  if stop e then f e else
+  match e.e with
+  | Do es -> retype (Do (last es))
+  | Let (bs, es) -> retype (Let (bs, last es))
+  | WithAlloc (a, es) -> retype (WithAlloc (a, last es))
+  | Handled (hs, es) -> retype (Handled (hs, last es))
+  | If (c, a, b) -> retype (If (c, go a, go b))
+  | Match (sc, arms) ->
+    retype (Match (sc, List.map (fun a -> { a with abody = last a.abody }) arms))
+  | RestartCase (cs, body) ->
+    retype
+      (RestartCase (List.map (fun c -> { c with rbody = last c.rbody }) cs, go body))
+  | _ -> if e.ty = Types.Never && not all then e else f e
+
+let iter_tails ?stop (f : expr -> unit) (e : expr) =
+  ignore (map_tails ~all:true ?stop (fun x -> f x; x) e)
+
 let rec walk (f : expr -> unit) (e : expr) =
   f e;
   let go = walk f in

test/programs/dyn-tails.flan

@@ -0,0 +1,88 @@
+;;;; A dyn in any value position of an operand or an arm — the last form
+;;;; of a let, either arm of an if, an arm of a match, the operand an and
+;;;; or an or answers with — meets its typed partner as a dyn, so what the
+;;;; runtime compares or adds is the dyn value and nothing traps.
+
+(defn as-dyn [d dyn] dyn d)
+
+(defn a1-t [c bool i i64 d dyn] dyn (+ i (let [z 1] d)))
+(defn a2-t [c bool i i64 d dyn] dyn (+ i (if c d d)))
+(defn a3-t [c bool i i64 d dyn] dyn (+ i (if c d 2)))
+(defn a4-t [c bool i i64 d dyn] dyn (= i (if c d 2)))
+(defn a5-t [c bool i i64 d dyn] dyn (* i (match (Some 1) (Some q) d None d)))
+(defn a6-t [c bool i i64 d dyn] dyn (let [v (if c i (let [z 1] d))] v))
+(defn a7-t [c bool i i64 d dyn] dyn (let [v (match (Some 1) (Some q) i None (let [z 1] d))] v))
+(defn a8-t [c bool i i64 d dyn] dyn (let [v (match (Some 1) None i (Some q) (if c d d))] v))
+(defn a9-t [c bool i i64 d dyn] dyn (- i (do (println 0) d)))
+(defn o1-t [c bool b bool i i64 d dyn] dyn (= b (and d)))
+(defn o2-t [c bool b bool i i64 d dyn] dyn (= b (or d)))
+(defn o3-t [c bool b bool i i64 d dyn] dyn (= b (and c d)))
+(defn o4-t [c bool b bool i i64 d dyn] dyn (= b (not d)))
+(defn o6-t [c bool b bool i i64 d dyn] dyn (let [v (if c b (and d))] v))
+(defn w1-t [c bool b bool d dyn] bool (= b (do (println 0) d)))
+(defn w2-t [c bool b bool d dyn] bool (= b (let [z 1] d)))
+(defn w3-t [c bool b bool d dyn] bool (= b (if c d d)))
+(defn w4-t [c bool b bool d dyn] bool (= b (if c d false)))
+(defn w5-t [c bool b bool d dyn] bool (= b (if c false d)))
+(defn w6-t [c bool b bool d dyn] bool (= b (match (Some 1) (Some q) d None d)))
+(defn w7-t [c bool b bool d dyn] bool (= (do d) b))
+(defn w9-t [c bool b bool d dyn] bool (= b (cond c d :else d)))
+(defn w10-t [c bool b bool d dyn] bool (= b (as-dyn d)))
+(defn w11-t [c bool b bool d dyn] bool (let [v (if c b (let [z 1] d))] (= v v)))
+(defn w12-t [c bool b bool d dyn] bool (= b (if c (do d) (do d))))
+(defn w13-t [c bool b bool d dyn] bool (!= b (let [z 1] (println z) d)))
+
+(defn main [] i32
+  (println (a1-t true 1 (as-dyn 1.5)))
+  (println (a1-t false 1 (as-dyn 1.5)))
+  (println (a2-t true 1 (as-dyn 1.5)))
+  (println (a2-t false 1 (as-dyn 1.5)))
+  (println (a3-t true 1 (as-dyn 1.5)))
+  (println (a3-t false 1 (as-dyn 1.5)))
+  (println (a4-t true 1 (as-dyn 1.5)))
+  (println (a4-t false 1 (as-dyn 1.5)))
+  (println (a5-t true 1 (as-dyn 1.5)))
+  (println (a5-t false 1 (as-dyn 1.5)))
+  (println (a6-t true 1 (as-dyn 1.5)))
+  (println (a6-t false 1 (as-dyn 1.5)))
+  (println (a7-t true 1 (as-dyn 1.5)))
+  (println (a7-t false 1 (as-dyn 1.5)))
+  (println (a8-t true 1 (as-dyn 1.5)))
+  (println (a8-t false 1 (as-dyn 1.5)))
+  (println (a9-t true 1 (as-dyn 1.5)))
+  (println (a9-t false 1 (as-dyn 1.5)))
+  (println (o1-t true true 1 (as-dyn 1)))
+  (println (o1-t true true 1 (as-dyn true)))
+  (println (o2-t true true 1 (as-dyn 1)))
+  (println (o2-t true true 1 (as-dyn true)))
+  (println (o3-t true true 1 (as-dyn 1)))
+  (println (o3-t true true 1 (as-dyn true)))
+  (println (o4-t true true 1 (as-dyn 1)))
+  (println (o4-t true true 1 (as-dyn true)))
+  (println (o6-t true true 1 (as-dyn 1)))
+  (println (o6-t true true 1 (as-dyn true)))
+  (println (w1-t true true (as-dyn 5)))
+  (println (w1-t false true (as-dyn 5)))
+  (println (w2-t true true (as-dyn 5)))
+  (println (w2-t false true (as-dyn 5)))
+  (println (w3-t true true (as-dyn 5)))
+  (println (w3-t false true (as-dyn 5)))
+  (println (w4-t true true (as-dyn 5)))
+  (println (w4-t false true (as-dyn 5)))
+  (println (w5-t true true (as-dyn 5)))
+  (println (w5-t false true (as-dyn 5)))
+  (println (w6-t true true (as-dyn 5)))
+  (println (w6-t false true (as-dyn 5)))
+  (println (w7-t true true (as-dyn 5)))
+  (println (w7-t false true (as-dyn 5)))
+  (println (w9-t true true (as-dyn 5)))
+  (println (w9-t false true (as-dyn 5)))
+  (println (w10-t true true (as-dyn 5)))
+  (println (w10-t false true (as-dyn 5)))
+  (println (w11-t true true (as-dyn 5)))
+  (println (w11-t false true (as-dyn 5)))
+  (println (w12-t true true (as-dyn 5)))
+  (println (w12-t false true (as-dyn 5)))
+  (println (w13-t true true (as-dyn 5)))
+  (println (w13-t false true (as-dyn 5)))
+  0)

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 in any value position of an operand or an arm is a dyn. *)
+    let dt_out = "2.5\n2.5\n2.5\n2.5\n2.5\n3\nfalse\nfalse\n1.5\n1.5\n1\n1.5\n1\n1\n1.5\n1.5\n0\n-0.5\n0\n-0.5\nfalse\ntrue\nfalse\ntrue\nfalse\ntrue\nfalse\nfalse\ntrue\ntrue\n0\nfalse\n0\nfalse\nfalse\nfalse\nfalse\nfalse\nfalse\nfalse\nfalse\nfalse\nfalse\nfalse\nfalse\nfalse\nfalse\nfalse\nfalse\nfalse\ntrue\ntrue\nfalse\nfalse\n1\ntrue\n1\ntrue\n" in
+    outputs "a dyn in a value position stays a dyn" "programs/dyn-tails.flan" dt_out;
+    outputs ~x86:true "a dyn in a value position stays a dyn, x86"
+      "programs/dyn-tails.flan" dt_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;