A refusal about a dyn stopped being reported against a prelude line

Nothing stopped a type variable being instantiated at dyn, because dyn
is an ordinary case of Types.t and substituted like any other type. The
copy was then made and walked into the dyn answers that are not all
there, and the refusal arrived from inside the generic's own source:
(or-else (Some d) e) over two dyns was reported against <prelude>:385,
a line the caller did not write and cannot act on.

Refused at the binding instead, where the call site is. The message
does not only say no: two models answer "one body, many types" here
and they are not rivals -- this one copies per written type at compile
time, defgeneric/defmethod dispatch at run time on a value that
carries its own -- so a dyn argument is asking the second question of
the first machinery, and the sentence names the other spelling.

Only the unbounded half is new. A variable carrying a {:where} clause
was already refused, because pred_holds says no to dyn for all four
predicates, and that refusal is left in front of this one on purpose:
it names the predicate the signature wrote down, which is the more
specific of the two answers.

Whether dyn should eventually flow through a generic is the author's
call and is recorded as open. Refusing now is the direction that can
be walked back: allowing it later adds programs, and nothing written
under this rule stops compiling.

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

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