An expectation outranks the join, because an expectation is information

lib/check.ml

@@ -7580,15 +7580,26 @@ and binary ctx ?(dyn_ok = false) ?(join = true) name loc ~want args =
       if a.Tast.ty = Types.Dyn || b.Tast.ty = Types.Dyn
          || Types.equal a.Tast.ty b.Tast.ty
       then a, b
-      (* Both operands are already in hand here, so the join is read off
+      (* Asking y for [a]'s type stays the first thing tried, and not only for
-         directly rather than through [join_pair]'s retry. Whichever one the
+         continuity: y was checked above with no expectation at all, and an
-         other widens into is the pair's type; with no join, the re-check
+         expectation is information. A sum of two products handed to an f32
-         produces the refusal, which names the cast at y's own line. *)
+         function is the case — test/programs/math.flan does it — because every
+         literal inside those products defaults to f64 on its own terms, so
+         reading the join off the two unexpected halves would answer f64 for a
+         form the site asked to be f32. The re-check builds them at f32 as it
+         always did.
+
+         [b] is only used when that re-check refuses, which is the direction
+         [expect] cannot serve: a is the narrower operand and it is the one
+         that has to move. Nothing is checked a third time — the own-terms [b]
+         already in hand is the answer. *)
       else
-        (match Types.join a.Tast.ty b.Tast.ty with
+        (match check ctx ~want:a.Tast.ty y with
-         | Some t ->
+         | b' -> a, b'
-           widen a.Tast.loc t a, widen b.Tast.loc t b
+         | exception e ->
-         | None -> a, check ctx ~want:a.Tast.ty y)
+           if join && Types.widens_to ~from:a.Tast.ty ~into:b.Tast.ty then
+             widen a.Tast.loc b.Tast.ty a, b
+           else raise e)
     end
     else begin
       let a = check ctx ?want x in