diff --git a/lib/check.ml b/lib/check.ml
index b75ec68..1691019 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -1374,6 +1374,19 @@ let rec generic_ty (t : Types.t) =
   | Types.Fn (ps, r) -> List.exists generic_ty ps || generic_ty r
   | _ -> false
 
+(* Does a type a call site bound a variable to reach a [dyn] anywhere? See the
+   refusal in [generic_call]: [dyn] is a concrete type and substitutes like any
+   other, so nothing stopped a copy being made at it, and the copies walked
+   straight into holes the rest of the language has no [dyn] answer for yet. *)
+let rec reaches_dyn (t : Types.t) =
+  match t with
+  | Types.Dyn -> true
+  | Types.Slice e | Types.Array (_, e) | Types.Ptr e | Types.Vec e
+  | Types.Option e -> reaches_dyn e
+  | Types.Map (k, v) -> reaches_dyn k || reaches_dyn v
+  | Types.Fn (ps, r) -> List.exists reaches_dyn ps || reaches_dyn r
+  | _ -> false
+
 (* The refusal plan.org's Types section asks for, in one place so that every
    operator says the same thing: with no constraints a type variable supports
    only what *every* type supports, so [=], [<], [+] and [hash] over one are
@@ -7540,8 +7553,15 @@ and generic_call ctx ~want loc name vars pats pret args =
             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". *)
+         (* Only where the pair is one widening had an opinion about. A string
+            passed where $t was bound to i64 is an ordinary mismatch and gets
+            the ordinary refusal; the sentence below is about the conversion
+            that no longer happens, and it would read as a non-sequitur over a
+            pair that never had one available. *)
          (match bound_scalar with
-          | Some v when not (Types.equal p a.Tast.ty) ->
+          | Some v
+            when (not (Types.equal p a.Tast.ty))
+                 && Types.is_numeric 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 \
@@ -7569,6 +7589,50 @@ and generic_call ctx ~want loc name vars pats pret args =
             generic function is instantiated from its call site, and there is \
             no syntax for naming the type" name v)
     vars;
+  (* **A type variable is not instantiated at dyn.** Nothing stopped it before:
+     [dyn] is an ordinary case of [Types.t], so it substituted like any other
+     type and a copy was generated at it. The copy then reached whatever the
+     body did with the value, and the dyn answers are not all there — [(Option
+     dyn)] has no descriptor the collector can find, [as-slice] over a
+     [(Vec dyn)] refuses. So the refusal existed, it just arrived from inside
+     the generic's own source: [(or-else (Some d) e)] over two dyns is reported
+     against [<prelude>:385], a line the caller did not write and cannot act
+     on. Every one of those is this refusal arriving late and in the wrong
+     place.
+
+     Refusing at the binding is also the honest statement of the split. Two
+     models answer "one body, many types" here and they are not rivals: this
+     one instantiates at compile time and keeps the types, and [defgeneric] /
+     [defmulti] dispatch at run time on a value that carries its own. A dyn
+     argument is asking the second question of the first machinery. The
+     message says so and names the other spelling.
+
+     Bounded variables were already refused — [pred_holds] says no to dyn for
+     all four predicates — so this closes the unbounded half, which is exactly
+     the half that reached the prelude-source diagnostics. A variable that
+     *does* carry a clause is left to that refusal deliberately: it names the
+     predicate the signature actually wrote down, which is the more specific
+     answer of the two, and the generic cast's pin depends on it. *)
+  let clause_on v =
+    match Hashtbl.find_opt ctx.env.generics name with
+    | None -> false
+    | Some gfn ->
+      List.exists
+        (fun (p : Ast.pred) -> String.equal p.Ast.pvar v) gfn.Ast.fwhere
+  in
+  List.iter
+    (fun (v, t) ->
+       if reaches_dyn t && not (clause_on v) then
+         Loc.failk "check/tyvar-at-dyn" loc
+           "this call would instantiate %s at $%s = %s, and a type variable \
+            is not instantiated at dyn: a copy is made per *written* type, \
+            and dyn is the one type whose own type is not known until it \
+            runs. One value, two models — (defgeneric %s [...]) with a \
+            (defmethod ...) per class dispatches on what the value turns out \
+            to be, which is the question a dyn argument is asking. Write the \
+            type the value has, or reach for the dyn side"
+           name v (Types.to_string t) name)
+    !subst;
   let cparams = List.map (subst_ty !subst) pats in
   let cret = subst_ty !subst pret in
   if List.exists generic_ty cparams || generic_ty cret then begin
diff --git a/test/test_flan.ml b/test/test_flan.ml
index d847170..57b64be 100644
--- a/test/test_flan.ml
+++ b/test/test_flan.ml
@@ -4711,6 +4711,43 @@ let () =
   accepts "and is accepted when it is"
     "(defn outer [s [$t]] () {:where (ordered? $t)} (sort s))";
 
+  (* ── A type variable is not instantiated at dyn ─────────────────────
+     Nothing stopped it before: dyn is an ordinary case of Types.t, so it
+     substituted like any other type and the copy was generated. What the copy
+     then ran into was the dyn answers that are not all there — (Option dyn)
+     has no descriptor the collector can find — and the refusal arrived from
+     inside the generic's own source. (or-else (Some d) e) over two dyns used
+     to be reported against <prelude>:385, a line the caller did not write.
+     The refusal is at the call site now, and it names the other model rather
+     than only saying no. *)
+  rejects_check "a type variable is not instantiated at dyn"
+    ~needle:"is not instantiated at dyn"
+    "(defn idf [x $t] $t x)\n\
+     (defvar d dyn 5)\n\
+     (defn main [] () (println (idf d)))";
+  rejects_check "and the refusal names the dyn side rather than only saying no"
+    ~needle:"defmethod"
+    "(defn idf [x $t] $t x)\n\
+     (defvar d dyn 5)\n\
+     (defn main [] () (println (idf d)))";
+  (* Nor at a type that merely *reaches* a dyn, which is the shape that used
+     to walk furthest before failing: (Option dyn) is the case the collector
+     has no descriptor for, and the refusal for it arrived from <prelude>:385.
+     It arrives here now, against the call that asked for the copy. *)
+  rejects_check "nor at a type that merely reaches a dyn"
+    ~needle:"$t = (Option dyn)"
+    "(defn maybe [] (Option dyn) None)\n\
+     (defn idf [x $t] $t x)\n\
+     (defn main [] () (println (some? (idf (maybe)))))";
+  (* A variable that carries a clause keeps the clause's refusal, which names
+     the predicate the signature actually wrote down — the more specific of
+     the two answers, and the one the generic cast's pin above depends on. *)
+  rejects_check "a bounded variable is still refused by its bound"
+    ~needle:"numeric?"
+    "(defn twice [x $t] $t {:where (numeric? $t)} (+ x x))\n\
+     (defvar d dyn 5)\n\
+     (defn main [] () (println (twice d)))";
+
   (* ── 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