A literal local read at T? takes T, None may come first in an if, an Option around an array of Options takes a literal, and a literal refused at T? names the Option.

lib/check.ml

@@ -3234,6 +3234,10 @@ let rec literal_arith (e : Ast.expr) : int64 option =
    over literals alone. *)
 let lone_literal (e : Ast.expr) = is_literal e || literal_arith e <> None
 
+(* Set for one [check_value] entry: the literal is checked at the Option
+   itself, not wrapped, so a refusal names the Option (decision 138). *)
+let skip_wrap = ref false
+
 (* [None] as written, which has no type until an Option is asked of it. *)
 let is_none_lit (e : Ast.expr) =
   match e.Ast.e with Ast.Var "None" -> true | _ -> false
@@ -3822,6 +3826,12 @@ let lit_admits kind (t : Types.t) =
   | `Box, t -> not (Types.equal t Types.Dyn)
   | _ -> false
 
+(* What a use at [t] says about a literal local: an (Option T) wanted of it
+   says T, since the local is built at T and then wrapped (decision 138), so
+   [let w: i64? = x] makes [x] the i64 [let w: i64 = x] does. *)
+let rec lit_payload (t : Types.t) =
+  match t with Types.Option p -> lit_payload p | t -> t
+
 (* The rounds a session may take before its last guesses are checked as
    they stand. Merging makes two the usual count; the bound only stops a
    pathological program from looping. *)
@@ -6128,19 +6138,26 @@ and check_value ctx ?want (e : Ast.expr) : Tast.expr =
   ctx.tail <- false;
   let used = ctx.used || List.memq e ctx.kept in
   ctx.used <- false;
+  let skipping = !skip_wrap in
+  skip_wrap := false;
   match e.Ast.e with
   (* A literal where an (Option T) is wanted is built at T and then wrapped
      (decision 138): [s = -1] over an [i64?] is [Some] of an i64 -1. It has
      no type until one is asked of it, so it is asked the payload's, rather
      than being built at a default and wrapped at the wrong width. *)
   | Ast.Int _ | Ast.UInt _ | Ast.Float _ | Ast.Byte _ | Ast.Call _ | Ast.Arr (_ :: _)
-    when (match want with Some (Types.Option _) -> true | _ -> false)
+    when (match want with Some (Types.Option _) -> not skipping | _ -> false)
          && (lone_literal e || (match e.Ast.e with Ast.Arr _ -> true | _ -> false)) ->
     let w = Option.get want in
     let t = match w with Types.Option t -> t | _ -> assert false in
-    let v = check ctx ~want:t e in
-    if Types.fits ~expected:t ~actual:v.Tast.ty then mk loc w (Tast.Some_ v)
-    else expect ctx loc ~want v
+    (match trial ctx (fun () -> check ctx ~want:t e) with
+     | Ok v when Types.fits ~expected:t ~actual:v.Tast.ty -> mk loc w (Tast.Some_ v)
+     | Ok v -> expect ctx loc ~want v
+     (* Refused at T: checked again at the Option as it was before 138, so
+        the refusal names what was wanted, [str?], and not only its payload. *)
+     | Error _ ->
+       skip_wrap := true;
+       check ctx ?want e)
   (* A negative literal in a generic body, at an instantiation that made it
      unsigned. The cast the ordinary refusal names would be wrong at every
      other type the function is called at, so the fix is one that needs no
@@ -6991,18 +7008,19 @@ and var ctx ?(qualified = false) loc ~want name =
     | Some ({ blit = Some key; _ } as b)
       when (match ctx.lits, want with
             | Some s, Some t ->
+              let t = lit_payload t in
               s.recording && not !lit_quiet
               && (Types.equal t Types.Dyn
                   || lit_admits (Option.value (lit_kind key) ~default:`Int) t)
             | _ -> false) ->
-      let s = Option.get ctx.lits and t = Option.get want in
+      let s = Option.get ctx.lits and t = lit_payload (Option.get want) in
       let operand = List.memq loc !lit_operand_locs in
       let c = if operand || Types.equal t Types.Dyn then Hint else Up in
       lit_add s key (c, t, loc);
       (try expect ctx loc ~want (mk loc b.bty (Tast.Local b.slot))
        with Loc.Error _ when lit_kind key <> Some `Box && not operand ->
          s.dirty <- true;
-         mk loc t (Tast.Local b.slot))
+         expect ctx loc ~want (mk loc t (Tast.Local b.slot)))
     | Some b ->
       expect ctx loc ~want (local_of loc b)
     (* A local of the enclosing function, in a body that was lifted out of it:
@@ -8655,8 +8673,11 @@ and check_if_once ctx ~tail ~used ?want loc c t e =
     let t = branch ctx (fun () -> in_tail (fun () -> check ctx ?want t)) in
     let e = branch ctx (fun () -> in_tail (fun () -> check ctx ?want e)) in
     mk loc t.Tast.ty (Tast.If (c, t, e))
-  | Some e when want = None && (adapts t || is_none_lit t)
-                && not (adapts e || is_none_lit e)
+  | Some e when want = None
+                && ((adapts t && not (adapts e || is_none_lit e))
+                    (* [if c then None else 5]: the else arm decides T, and
+                       None meets it at T? below, as the other order does. *)
+                    || (is_none_lit t && not (is_none_lit e)))
                 && not (and_sentinel e) ->
     (* A literal has no type of its own until something asks, so with no
        expectation the other arm decides: [(if c 4000000 n)] over an i64 [n]
@@ -9841,10 +9862,20 @@ and check_the ctx ~want loc (t : Ast.texpr) (v : Ast.expr) =
         not agree among themselves — [[1, None]] — is built at the annotation
         when every element fits it, as [x: [2 i32?] = [1, None]] (decision
         138). Nothing is converted: the literal is built at T. *)
-     && not (match v.Ast.e, ty with
-             | Ast.Arr _, (Types.Array (_, Types.Option _) | Types.Slice (_, Types.Option _)) ->
-               probe ctx loc (fun () -> ignore (check ctx ~want:ty v)) <> None
-             | _ -> false)
+     && not (let rec holds_option = function
+                | Types.Option _ -> true
+                | Types.Array (_, t) | Types.Slice (_, t) -> holds_option t
+                | _ -> false
+              in
+              let rec elems_option = function
+                | Types.Array (_, t) | Types.Slice (_, t) -> holds_option t
+                | Types.Option t -> elems_option t
+                | _ -> false
+              in
+              match v.Ast.e with
+              | Ast.Arr _ when elems_option ty ->
+                probe ctx loc (fun () -> ignore (check ctx ~want:ty v)) <> None
+              | _ -> false)
   then begin
     let tn = tyname loc ty in
     let numeric = match ty with Types.Int _ | Types.Float _ -> true | _ -> false in

test/programs/autowrap.fln

@@ -38,6 +38,8 @@ fn arms(k: i32, x: i32) -> i32?
     4 -> x
     _ -> 0
 
+fn big(x: i64?) -> i64 = x ?? 0
+
 fn chain(a: bool, b: bool, opt: i32?) -> Option(i32?)
   if a
     1
@@ -93,6 +95,33 @@ fn main()
   println(two(kk))
   ;; generics
   println(first(9), first(Some(8)), wrap(3) ?? 0, through(5))
+  ;; a literal local takes the payload's type from an Option use, as it
+  ;; takes T from a T use: each pair prints the same
+  let la = 4
+  let wa: i64? = la
+  let lb = 4
+  let wb: i64 = lb
+  println(la * 1000000000, lb * 1000000000, wa ?? 0, wb)
+  let lc = 4
+  println(big(lc), lc * 1000000000)
+  let lf = 7
+  let wf: f64? = lf
+  let lg = 7
+  let wg: f64 = lg
+  println(lf / 2, lg / 2, wf ?? 0.0, wg)
+  let lu = 200
+  let wu: u8? = lu
+  let lv = 200
+  let wv: u8 = lv
+  println(wu ?? 0, wv)
+  ;; None first in an if, as in a match
+  let e1 = if x > 1 then None else 5
+  let e2 = if x > 1 then 5 else None
+  println(e1 ?? -1, e2 ?? -1)
+  ;; an Option around an array of Options
+  let ao: [2 i32?]? = [1, None]
+  let ai = ao!
+  println(ai[0] ?? 0, ai[1] ?? 0)
   ;; a narrowed name still takes a payload value
   let o: i32? = Some(1)
   if o?

test/test_acceptance.ml

@@ -2277,7 +2277,8 @@ let () =
         (* A T where a T? is wanted is Some of it (decision 138). *)
         ("autowrap.fln",
          "-1\n5 4 2\n7 8 -1\n3 4\n7\n1 0 4\n5\n2 6 0\n2 -1 -1 2\n4\n-1 3 0\n\
-          some some some none\nsome some some none none\nsome some\n9 8 3 5\n10\n");
+          some some some none\nsome some some none none\nsome some\n9 8 3 5\n\
+          4000000000 4000000000 4 4\n4 4000000000\n3.5 3.5 7 7\n200 200\n-1 5\n1 0\n10\n");
         (* x? tests and narrows, e? as g names what it found (decision 133). *)
         ("presence.fln", "true false true\n6\n-1\n3\n101 209 0\n11\n42\n2\nabsent\n6\nfalse true\n3\n6\n15\n"); ("presence-dyn.fln", "true false\n103 209 0\nno pet\nann\n3 2\n") ];
     (* The pipe (decision 137): chains, multi-line, qualified, dyn, and the

test/test_flan.ml

@@ -8412,6 +8412,9 @@ let () =
   rejects_check "a payload that does not fit is refused at the Option"
     ~needle:"expected (Option i32), found str"
     "(defn f [] (Option i32) \"no\")\n(defn main [] ())";
+  rejects_check "a literal that does not fit is refused at the Option"
+    ~needle:"expected (Option string), found the integer literal 5"
+    "(defn f [] (Option string) 5)\n(defn main [] ())";
   rejects_check "a narrowing is not wrapped" ~needle:"expected (Option i32), found i64"
     "(defn f [x i64] (Option i32) x)\n(defn main [] ())";
   rejects_check "no wrap inside a container" ~needle:"expected (Vec (Option i32)), found (Vec i32)"