diff --git a/lib/check.ml b/lib/check.ml
index 8138d16..b75ec68 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -7486,9 +7486,71 @@ and generic_call ctx ~want loc name vars pats pret args =
   let subst = ref [] in
   let targs =
     map2_lr
-      (fun p a ->
-         let p = subst_ty !subst p in
-         let a = if generic_ty p then check ctx a else check ctx ~want:p a in
+      (fun pat a ->
+         let p = subst_ty !subst pat in
+         (* Which variable, if any, this parameter *is* — written as a bare
+            [$t] and already bound by an argument to the left. That is the one
+            shape implicit widening can reach, because [Types.widens_to] admits
+            only numeric scalars: a variable bound inside [[$t]] or
+            [(Fn [$t $t] bool)] leaves a parameter no widening applies to, so
+            the [sort-by] path below is untouched by construction. *)
+         let bound_scalar =
+           match pat with
+           | Types.Var v when (not (generic_ty p)) && Types.is_numeric p ->
+             Some v
+           | _ -> None
+         in
+         (* An untyped constant has no type of its own to keep, so it still
+            takes the variable's — [(clamp-to y 0 10)] with [y] an i64 means
+            three i64s and there is no conversion anywhere in it. Everything
+            else is checked on its own terms. *)
+         let untyped_literal =
+           match a.Ast.e with
+           | Ast.Int _ | Ast.Float _ | Ast.Byte _ -> true
+           | _ -> false
+         in
+         let a =
+           if generic_ty p then check ctx a
+           else if bound_scalar <> None && not untyped_literal then
+             (* On its own terms first. A form that has no type without a want
+                — [(zeroed)] is the one that matters — refuses here and is
+                checked against the parameter as it always was; the trial
+                leaves no trace of the attempt. *)
+             (match trial ctx (fun () -> check ctx a) with
+              | Ok r -> r
+              | Error _ -> check ctx ~want:p a)
+           else check ctx ~want:p a
+         in
+         (* **Implicit widening does not cross a generic binding.** A concrete
+            argument at a variable an earlier argument already bound has to be
+            the same type, not merely a type that widens into it.
+
+            This is a decision and not a consequence. Widening landed after
+            generics did, and left behind a rule that depended on argument
+            order: [(pair-eq? i64 i8)] was accepted, because [$t] bound to i64
+            first and the i8 widened into the want; [(pair-eq? i8 i64)] was
+            refused, because [$t] bound to i8 and i64 into i8 can lose. Same
+            two values, same function, two answers. Neither is unsound — a
+            widen cannot change a number — but which instantiation a program
+            gets should not depend on which argument was written first.
+
+            Refusing both is the direction that can be walked back. Allowing
+            the pair to join at the wider type is a coherent rule too, and it
+            is the one to reach for if the ergonomics turn out to want it; it
+            can be added later without invalidating a program that was written
+            under this rule, and the reverse is not true. FIX.org, "Generics
+            and implicit widening". *)
+         (match bound_scalar with
+          | Some v when not (Types.equal p a.Tast.ty) ->
+            Loc.failk "check/tyvar-no-widening" a.Tast.loc
+              "%s's $%s was bound to %s by an earlier argument, and this one \
+               is %s. Implicit widening does not cross a generic binding: a \
+               written type is what a type variable takes, so the same \
+               variable is the same type at every argument. Write the \
+               conversion — (%s x) — or pass the arguments at one type"
+              name v (Types.to_string p) (Types.to_string a.Tast.ty)
+              (Types.to_string p)
+          | _ -> ());
          if not (bind_ty subst p a.Tast.ty) then
            fail a.Tast.loc "%s expects %s here, found %s" name
              (Types.to_string p) (Types.to_string a.Tast.ty);
diff --git a/test/test_flan.ml b/test/test_flan.ml
index aef9577..d847170 100644
--- a/test/test_flan.ml
+++ b/test/test_flan.ml
@@ -4711,6 +4711,55 @@ let () =
   accepts "and is accepted when it is"
     "(defn outer [s [$t]] () {:where (ordered? $t)} (sort s))";
 
+  (* ── Implicit widening does not cross a generic binding ─────────────
+     Widening landed after generics did, and the rule it left behind depended
+     on the order the arguments were written in: the i8-then-i64 call was
+     refused because i64 into i8 can lose, and the i64-then-i8 call was
+     *accepted*, because $t had already bound to i64 and the i8 widened into
+     the want. Same two values, same function, two answers.
+
+     Neither was unsound — a widen cannot change a number — but which copy a
+     program gets should not turn on which argument came first, so both are
+     refused now and both name the binding. Letting the pair join at the wider
+     type is the other coherent rule and it stays available: it can be added
+     without invalidating anything written under this one, which is why this
+     is the direction to be wrong in. FIX.org, "Generics and implicit
+     widening". *)
+  rejects_check "a narrower argument does not widen into a bound type variable"
+    ~needle:"was bound to i64 by an earlier argument"
+    "(defn eq2? [a $t  b $t] bool {:where (equal? $t)} (= a b))\n\
+     (defn main [] () (println (eq2? (i64 3) (i8 3))))";
+  rejects_check "and the other argument order refuses identically"
+    ~needle:"was bound to i8 by an earlier argument"
+    "(defn eq2? [a $t  b $t] bool {:where (equal? $t)} (= a b))\n\
+     (defn main [] () (println (eq2? (i8 3) (i64 3))))";
+  (* The written conversion is what the message asks for, and it is accepted:
+     the refusal is about the *implicit* step, not about reaching i64. *)
+  accepts "the written conversion is accepted"
+    "(defn eq2? [a $t  b $t] bool {:where (equal? $t)} (= a b))\n\
+     (defn main [] () (println (eq2? (i64 3) (i64 (i8 3)))))";
+  (* An untyped constant has no type of its own to keep, so it still takes the
+     variable's. Nothing is converted here — three i64s were written. *)
+  accepts "an untyped literal still takes a bound type variable's type"
+    "(defn clamp3 [x $t  lo $t  hi $t] $t {:where (ordered? $t)} \
+       (min (max x lo) hi))\n\
+     (defn main [] () (println (clamp3 (i64 12) 0 10)))";
+  (* And the shapes widening cannot reach are untouched, which is the reason
+     the rule costs so little: [Types.widens_to] admits only numeric scalars,
+     so a variable bound inside a slice or a function type leaves a parameter
+     no widening applied to in the first place. *)
+  accepts "a variable bound inside a constructor is unaffected"
+    "(defn sort2 [s [$t]  before? (Fn [$t $t] bool)] () \
+       (sort-by s before?))\n\
+     (defn main [] () (let [ns [5 3 9 1]] \
+       (sort2 (slice ns 0 4) (fn [a b] (< a b))) (println (at ns 0))))";
+  (* A form with no type of its own is still checked against the parameter:
+     the trial that asks for its natural type refuses, and the want it always
+     had is what it falls back to. *)
+  accepts "a form that needs a want still gets one at a bound type variable"
+    "(defn pick [a $t  b $t] $t (do b a))\n\
+     (defn main [] () (println (pick (i64 3) (zeroed))))";
+
   (* ── A numeric literal where a type variable is wanted ──────────────
      The author's motivating family — one pos? over every numeric type from
      one definition — needs a written 0 to stand where $t stands. The bound