A kept if-let chain takes its type from what its arm answered, so an arm that returns stays Never and one with no value makes the chain a statement.

lib/check.ml

@@ -9764,12 +9764,13 @@ and check_array_gen ctx ~want loc dims f =
        ~element:(fun idxs -> mk loc elem (Tast.CallPtr (fv, idxs))))
 
 and check_match ctx ?(tail = false) ?(used = false) ?(stmt = false) ?(opt = false)
-    ?want loc scrutinee arms =
+    ?opt_rest ?want loc scrutinee arms =
   (* [stmt] is an [if let] with no else: a statement, Unit whatever its arm
      answers, as a one-armed [if] is when nothing keeps it. [opt] is one that
      is kept: its arm answers [Some], and the arm with no body [None]. *)
   let used = used && not stmt in
   let arms_ast_for_opt = arms in
+  let want0 = want in
   let want =
     if stmt then None
     else if opt then (match want with Some (Types.Option i) -> Some i | _ -> None)
@@ -10281,19 +10282,74 @@ and check_match ctx ?(tail = false) ?(used = false) ?(stmt = false) ?(opt = fals
   let arms =
     List.map snd (List.sort (fun (i, _) (j, _) -> compare i j) checked)
   in
-  let opt_ty = Option.map (fun t -> Types.Option t) !want in
+  (* [opt]: what the pattern's arm answered decides the whole, as a
+     one-armed [if]'s branch does — no value is a statement, Never stays
+     Never, a dyn is the value or nil, and anything else is [Some] of it. The
+     arm with no body is the rest of the chain, [opt_rest], checked now that
+     its want is known, or [None] when the chain ends here. *)
+  let opt_result = ref None in
   let arms =
-    match opt, opt_ty with
+    if not opt then arms
-    | true, Some oty ->
+    else
-      List.map2
+      let raw =
-        (fun (a : Ast.arm) (arm : Tast.arm) ->
+        List.fold_left2
-           match a.Ast.body, arm.Tast.abody with
+          (fun acc (a : Ast.arm) (arm : Tast.arm) ->
-           | [], _ -> { arm with Tast.abody = [ mk a.Ast.aloc oty Tast.None_ ] }
+             match a.Ast.body, arm.Tast.abody with
-           | _, [ b ] when b.Tast.ty <> Types.Never ->
+             | _ :: _, [ b ] -> Some b.Tast.ty
-             { arm with Tast.abody = [ mk b.Tast.loc oty (Tast.Some_ b) ] }
+             | _ -> acc)
-           | _ -> arm)
+          None arms_ast_for_opt arms
-        arms_ast_for_opt arms
+      in
-    | _ -> arms
+      let rest ~used ?want () =
+        match opt_rest with
+        | Some f -> Some (f ~used ?want ())
+        | None -> None
+      in
+      let fill body_of wild_of =
+        List.map2
+          (fun (a : Ast.arm) (arm : Tast.arm) ->
+             match a.Ast.body, arm.Tast.abody with
+             | [], _ -> { arm with Tast.abody = [ wild_of a ] }
+             | _, [ b ] -> { arm with Tast.abody = [ body_of b ] }
+             | _ -> arm)
+          arms_ast_for_opt arms
+      in
+      match raw with
+      | None | Some Types.Unit ->
+        opt_result := Some Types.Unit;
+        let r = rest ~used:false () in
+        fill Fun.id (fun a ->
+            match r with
+            | Some e when e.Tast.ty = Types.Unit || e.Tast.ty = Types.Never -> e
+            | Some e -> mk e.Tast.loc Types.Unit (Tast.Do [ e; unit_at e.Tast.loc ])
+            | None -> unit_at a.Ast.aloc)
+      | Some Types.Never ->
+        (match rest ~used:true ?want:want0 () with
+         | Some e ->
+           opt_result := Some e.Tast.ty;
+           fill Fun.id (fun _ -> e)
+         | None ->
+           (match want0 with
+            | Some (Types.Option _ as o) ->
+              opt_result := Some o;
+              fill Fun.id (fun a -> mk a.Ast.aloc o Tast.None_)
+            | _ ->
+              opt_result := Some Types.Unit;
+              fill Fun.id (fun a -> unit_at a.Ast.aloc)))
+      | Some Types.Dyn ->
+        opt_result := Some Types.Dyn;
+        let r = rest ~used:true ~want:Types.Dyn () in
+        fill Fun.id (fun a ->
+            match r with
+            | Some e -> e
+            | None -> rt a.Ast.aloc Types.Dyn "flan_dyn_nil" [])
+      | Some t ->
+        let oty = Types.Option t in
+        opt_result := Some oty;
+        let r = rest ~used:true ~want:oty () in
+        fill (fun b -> mk b.Tast.loc oty (Tast.Some_ b)) (fun a ->
+            match r with
+            | Some e -> e
+            | None -> mk a.Ast.aloc oty Tast.None_)
   in
   (* Exhaustiveness is refused, not defaulted. A match that silently fell
      through would have to produce a value of the match's type out of nothing,
@@ -10344,7 +10400,7 @@ and check_match ctx ?(tail = false) ?(used = false) ?(stmt = false) ?(opt = fals
       (if List.length missing = 1 then "it" else "them");
   let ty =
     if stmt then Types.Unit
-    else if opt then (match opt_ty with Some t -> t | None -> Types.Never)
+    else if opt then (match !opt_result with Some t -> t | None -> Types.Never)
     else match !want with Some t -> t | None -> Types.Never
   in
   match subject with
@@ -10438,19 +10494,18 @@ and check_if_let ctx ~tail ~used ?want loc scrutinee (arm : Ast.arm) els =
      | Some Types.Dyn ->
        check_match ctx ~tail ~used:true ?want loc scrutinee [ arm; wild [ rest ] ]
      | _ ->
-       match els with
+       (* The rest of the chain is checked once the arm's own type is
-       | None ->
+          known, as a one-armed [if]'s else is: see [opt] in [check_match]. *)
-         expect ctx loc ~want
+       let opt_rest =
-           (check_match ctx ~tail ~used:true ~opt:true ?want loc scrutinee
+         Option.map
-              [ arm; wild [] ])
+           (fun e ~used ?want () ->
-       | Some rest ->
+              branch ctx (fun () ->
-         let some =
+                  ctx.tail <- tail; ctx.used <- used; check ctx ?want e))
-           List.map
+           els
-             (fun (b : Ast.expr) -> at b (Ast.Call (at b (Ast.Var "Some"), [ b ])))
+       in
-             arm.Ast.body
+       expect ctx loc ~want
-         in
+         (check_match ctx ~tail ~used:true ~opt:true ?opt_rest ?want loc scrutinee
-         check_match ctx ~tail ~used:true ?want loc scrutinee
+            [ arm; wild [] ]))
-           [ { arm with Ast.body = some }; wild [ rest ] ])
   | Some e ->
     check_match ctx ~tail ~used ?want loc scrutinee [ arm; wild [ e ] ]
   | None ->

test/programs/if-let-kept.fln

@@ -14,6 +14,13 @@ fn lead(k: i32, b: Option(i32)) -> Option(i32)
   elif let Some(y) = b
     y
 
+;; An arm that returns stays Never, and the rest of the chain decides.
+fn early(a: Option(i32)) -> Option(i32)
+  if let Some(x) = a
+    return None
+  elif true
+    3
+
 fn dyn_only(a: Option(i32)) -> dyn
   if let Some(x) = a then x
 
@@ -31,6 +38,8 @@ fn main()
   show(lead(9, None))
   show(lead(1, Some(2)))
   show(lead(1, None))
+  show(early(None))
+  show(early(Some(1)))
   println(dyn_only(Some(5)))
   println(dyn_only(None))
   ;; As a statement it is unchanged.

test/programs/when-value.flan

@@ -21,6 +21,10 @@
 ;; Dyn: the body or nil.
 (defn dyn-when [x] dyn (when x 5))
 
+;; An if-let arm that returns stays Never; the when after it decides.
+(defn early [a (Option i32)] (Option i32)
+  (if-let [(Some x) a] (return None) (when true 3)))
+
 ;; A lambda's last form is kept at the return type its position wants.
 (defn call-it [f (Fn [] (Option i32))] () (show (f)))
 
@@ -43,6 +47,8 @@
   (level (wrap false (Some 1)))
   (println (dyn-when true))
   (println (dyn-when nil))
+  (show (early None))
+  (show (early (Some 1)))
   (call-it (fn [] (when true 6)))
   (call-it (fn [] (when false 6)))
   (show (pick 2))

test/test_acceptance.ml

@@ -2226,7 +2226,7 @@ let () =
       dyn_if_truthy_out;
     (* A kept when is an Option; get is a checked lookup; if let. *)
     let when_value_out =
-      "5\nnone\n42\nnone\n9\n1\nsome none\nnone\n5\nnil\n6\nnone\n20\nnone\n2\n\
+      "5\nnone\n42\nnone\n9\n1\nsome none\nnone\n5\nnil\n3\nnone\n6\nnone\n20\nnone\n2\n\
        a\nnil\ncond stmt\nran\nend\n"
     in
     outputs "when as a value" "programs/when-value.flan" when_value_out;
@@ -2245,7 +2245,9 @@ let () =
     let if_let_out =
       "5\n100\n0\n9\n1\n20\n100\n0\n1\n7\nabsent\nnorth\n6\n-1\n-2\n14\nwhen block\n"
     in
-    let if_let_kept_out = "1\n4\nnone\n6\nnone\n9\n2\nnone\n5\nnil\n7\n" in
+    let if_let_kept_out =
+      "1\n4\nnone\n6\nnone\n9\n2\nnone\n3\nnone\n5\nnil\n7\n"
+    in
     outputs "a kept if let chain" "programs/if-let-kept.fln" if_let_kept_out;
     outputs ~opt:"-O0" "a kept if let chain, -O0" "programs/if-let-kept.fln" if_let_kept_out;
     outputs ~x86:true "a kept if let chain, --x86" "programs/if-let-kept.fln" if_let_kept_out;

test/test_syntax.ml

@@ -1383,6 +1383,24 @@ let checks name text =
   | _ -> ()
   | exception e -> fail "%s does not check: %s" name (diag_text e)
 
+(* A kept if-let chain whose arm gives no value is a statement, refused as a
+   plain if's is; one whose arm returns stays Never, in both syntaxes. *)
+let () =
+  refused "if-let-unit.flan"
+    "(defn main [] () (let [a (Some 1) r (if-let [(Some x) a] (println x) \
+     (when true (println 2)))] (println r)))\n"
+    [ "r would be bound to (), which is not a value" ];
+  refused "if-let-unit.fln"
+    "fn main()\n  let a = Some(1)\n  let r = if let Some(x) = a then println(x) \
+     else when true then println(2)\n  println(r)\n"
+    [ "r would be bound to (), which is not a value" ];
+  checks "if-let-never.flan"
+    "(defn f [a (Option i32)] (Option i32) (if-let [(Some x) a] (return None) \
+     (when true 3)))\n(defn main [] () (println (f None)))\n";
+  checks "if-let-never.fln"
+    "fn f(a: Option(i32)) -> Option(i32)\n  if let Some(x) = a\n    return None\n  \
+     elif true\n    3\n\nfn main()\n  println(f(None))\n"
+
 let () =
   let poke_fln = "fn poke(coll) -> dyn\n  coll[0] = 99\n  coll\n\n" in
   let poke_flan = "(defn poke [coll] dyn (set (at coll 0) 99) coll)\n" in