diff --git a/FIX.org b/FIX.org
index 27e1313..aafb23f 100644
--- a/FIX.org
+++ b/FIX.org
@@ -3218,9 +3218,13 @@ an abandoned trial that lifted a function out of an ~fn~ literal leaves it in
 out by count, so the live pass gets fresh ones and nothing refers to the
 orphan — and it rides into the module as a function nobody calls. Left because
 ~env~ is the program's table rather than this form's, and rewinding it would
-mean deciding what else on ~env~ a trial may have touched; the one piece of
-~env~ state that genuinely needs rewinding, the generic instantiation cache,
-already rewinds itself in ~instantiate~.
+mean deciding what else on ~env~ a trial may have touched.
+
+[Corrected by the milestone-5 lane, below: the generic instantiation cache
+does not rewind itself either, and does not need to. ~instantiate~ rewinds a
+copy whose *body* refused, which is a different event from a copy the caller
+abandoned. The abandoned one is harmless because the trial and the live pass
+cannot disagree about which copy to make.]
 
 All five symptoms pinned — the two accepts, the shadow, the unknown name, and
 the loop diagnostic.
@@ -3272,3 +3276,217 @@ a reason that is now stated correctly.
 deliberately*: the website has its own rewrite lane, and a marketing page is
 not the place for this lane to be making edits it cannot test. Flagged here so
 that lane picks it up.
+
+* Milestone 5, and the sweep behind it, 2026-09-20
+
+** What was already there
+Almost all of it, and the first finding of this lane is that finding.
+docs/SPIKE-GENERICS.md carries a banner saying so — "it stopped being current
+when generics landed for real, on 2026-09-13" — and the code agrees:
+~$t~ binds and bare ~t~ reads; ~collect~ puts a generic signature in ~gsigs~
+and keeps it out of ~env.fns~; ~generic_call~ binds left to right,
+substituting each binding into the parameters still to come; ~instantiate~
+caches by ~Types.equal~ on the concrete parameter list; the body is checked
+once abstractly so a refusal lands at the definition; ~{:where~ carries four
+predicates with an entailment table; ~runaway~ caps the depth; a copy is an
+ordinary ~Tast.fn~ with a cell, so both backends were untouched then and are
+untouched now; and ~Check.instantiations~ expands a redefined generic's name
+for ~Session.eval~, which test_session pins at four shapes including a copy
+the running process was never built with.
+
+So this lane is not "start M5". It is the four things M5 did not reach, and
+the sweep the author asked for.
+
+** 1. A written zero may stand where a numeric type variable stands
+The one thing the landed generics could not express was the family the whole
+feature was asked for:
+
+#+begin_src lisp
+(defn pos? [x $t] bool {:where (numeric? $t)} (> x 0))
+#+end_src
+
+~(> x 0)~ was refused with "expected t, found the integer literal 0", because
+~int_literal~ had no arm for a want that is a type variable. It has one now,
+and *the bound is what makes it sound rather than optimistic*: every type
+~numeric?~ admits is an integer or a float, and an untyped integer constant is
+usable at all of them, so there is no instantiation of a ~numeric?~ variable
+at which the literal has no meaning. Under anything weaker there is —
+~ordered?~ admits an enum, which holds no number — so ~numeric?~ is what is
+asked for and the refusal names it.
+
+*The float literal is refused at a type variable even under ~numeric?~*, and
+that asymmetry is the concrete arms' own rather than a new rule: an integer
+constant is usable where a float is wanted, and a float literal is never
+usable where an integer is wanted. ~numeric?~ covers both halves of the
+numbers, so a body written with ~0.5~ has no meaning at the integer half of
+its own bound, and refusing at the definition is what the abstract pass is
+for.
+
+Nothing built here is emitted. The abstract pass builds a placeholder at i64
+and throws it away with the rest of the body; each copy re-checks the same
+form with the variable substituted, and that is where the literal is built at
+the concrete width and range-checked — so ~(+ x 300)~ is fine at i32 and a
+refusal at u8, and u8 is where it is refused.
+
+** 2. Generics and implicit widening
+*Decided: implicit widening does not cross a generic binding.*
+
+Widening landed days after generics did, and the rule the two of them left
+between them read off the order the arguments were written in:
+
+#+begin_src lisp
+(defn eq2? [a $t  b $t] bool {:where (equal? $t)} (= a b))
+(eq2? (i8 3) (i64 3))   ; refused — i64 into i8 can lose
+(eq2? (i64 3) (i8 3))   ; accepted — $t was i64 already, the i8 widened in
+#+end_src
+
+Same two values, same function, one copy at i8 refused and one copy at i64
+generated. Neither answer is unsound — a widen cannot change a number — so
+this is not a bug report; it is a decision nobody had taken, because the two
+features had never been in the tree at the same time.
+
+Taken: a concrete argument at a variable an earlier argument already bound has
+to be that type. Both orders refuse now, with one sentence naming the binding,
+the argument and the cast to write.
+
+*Why refuse rather than join.* Letting the pair meet at the wider type is the
+other coherent rule, and it is the better one if the ergonomics ask for it.
+It can be added later without invalidating a single program written under this
+rule. The reverse is not true. Refusing is the direction that can be walked
+back, and with two features that had never met, that is the direction to be
+wrong in.
+
+The rule costs almost nothing, because ~Types.widens_to~ admits only numeric
+scalars: a variable bound inside ~[$t]~ or ~(Fn [$t $t] bool)~ leaves a
+parameter no widening ever applied to, so ~sort-by~ and the whole fn-literal
+path are untouched by construction. Two exceptions keep the ergonomics —
+an untyped literal has no type of its own to keep, so it still takes the
+variable's; and a form with no type without a want (~(zeroed)~) is asked for
+its natural type through a ~trial~ and falls back to the want when that
+refuses.
+
+*** And the composition with the trial machinery, which is the reason to care
+A binary operator whose operands disagree re-checks the right one at the left
+one's type inside a ~trial~, so a generic call written there is checked twice,
+once in a pass that is thrown away. An instantiation made during the discarded
+pass does *not* go back out: ~instantiate~ rewinds a copy whose body refused,
+which is a different event.
+
+It does not have to, and the reason is this lane's own rule rather than luck.
+*A generic call's instantiation is read off its arguments and never off the
+ambient want* — an unbound variable is checked with no expectation at all, and
+a bound one no longer widens — so the trial and the live pass ask
+~instantiate~ for the same types, the second ask is a cache hit on the first,
+and exactly one copy exists either way. Pinned by counting copies in the
+checked program, not by reading the comment.
+
+The widening lane's own note said the instantiation cache "already rewinds
+itself"; it does not, and the entry above has been corrected in place.
+
+** 3. A type variable is not instantiated at dyn
+*Decided: refused, at the binding.*
+
+Nothing stopped it before, 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~, about a descriptor the collector cannot build for
+~(Option dyn)~ — a line the caller did not write and cannot act on. Every
+such case is this refusal arriving late and in the wrong place.
+
+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. A dyn argument is asking the second question of the first machinery,
+so the sentence names the other spelling.
+
+Only the unbounded half is new — a variable carrying a ~{:where}~ clause was
+already refused by ~pred_holds~, and that refusal is left in front of this one
+deliberately, because it names the predicate the signature wrote down.
+
+*Open, and the author's:* whether dyn should eventually flow through a
+generic at all. Refusing now is the walk-backable direction for the same
+reason as the widening decision.
+
+** 4. Three messages about milestone 5, from a milestone that arrived
+Swept, and they were not all the same kind of stale.
+
+- ~check.ml~'s unknown-lowercase-type arm reported "generic code over the
+  type variable X is not implemented yet — milestone 5 work". Generics are
+  implemented, and ~resolve_name~ consults ~env.tyvars~ and ~env.subst~ long
+  before anything reaches that arm, so a lowercase name arriving there is a
+  typo too far from any type to guess at, or a type variable nobody
+  introduced. It names the sigil that would introduce it.
+- The type resolver's "X takes no type arguments — generics are milestone 5"
+  and the value-position fork's "a type given type arguments is generic code,
+  which is milestone 5" are about the *other* half, which is genuinely
+  unbuilt: ~Types.Named~ is a bare string with no room for parameters, and
+  giving it some is a change to ~Types.t~ and therefore to the layout
+  calculator, both backends, ~Render~ and DWARF. Both now say a generic
+  *type* is not there yet and point at the generic function that is. Nothing
+  was built for them.
+
+Three test needles moved with them.
+
+** 5. The prelude sweep — what collapsed, what did not
+*Added:* ~pos?~, ~neg?~, ~zero?~. Three questions about a number's sign, one
+body each, answering at i8 through u64 and at both float widths. They were
+never written before because without a type variable they are three functions
+per width; they are writable now because of item 1 above and not because of
+the type variable alone.
+
+*Declined, with the real reason written where the old one was:*
+
+- ~abs-i32~/~abs-i64~ stay two functions. The comment's old reason — "there
+  are no generics over the numeric types" — is false now, and the generic
+  body checks and runs at every integer width. What stops it is the float
+  half of its own bound: ~numeric?~ is the only predicate that admits a
+  written ~0~ and it admits f32/f64 too, and ~(if (< x 0) (- 0 x) x)~ is the
+  wrong abs for a float — it hands back a negative zero. The float pair is
+  libm's ~fabs~ for exactly that reason. *The collapse waits on a bound that
+  spells "an integer type".*
+- ~min~/~max~ stay builtins. Not a type-system limit: they are variadic, and
+  each step slots both of its sides so every operand is evaluated exactly
+  once. A binary prelude generic would have to be nested at the call site,
+  which puts the double evaluation back. Their generic half was never missing
+  — ~ordered?~ already admits them in any body that declares it.
+
+*** An ~integer?~ predicate — recorded, not built
+It would collapse ~abs~, and it would let ~%~, the bitwise operators and the
+shifts be written over a variable. It is four lines in ~pred_holds~,
+~predicate_names~ and ~pred_entails~ (declared ~integer?~ gives ~numeric?~,
+~ordered?~ and ~equal?~). It is not built here because adding a predicate is
+language surface — the vocabulary a programmer writes — and that is the
+author's call, not a lane's.
+
+** What this lane did not build, deliberately
+- *Generic types.* ~(defstruct Pair [a $t b $t])~ cannot be spelled, and
+  the price is in the spike: ~Types.t~ and every backend. Out of scope, and
+  the two messages above now say so accurately.
+- *"In instantiation of" notes.* A refusal inside a copy points at the
+  generic's source with no note saying which call site asked for that type.
+  ~Check.instantiation_origin~ exists and ~session.ml~ already uses it for
+  compatibility reports, so the data is there; wiring it into every ~fail~
+  under an instantiation is the spike's "bulky, not hard" bucket and is a
+  lane of its own. Two of the three places it mattered most are closed by
+  items 2 and 3 above, which move those refusals to the call site outright.
+- *~$n~ in length position.* Same price as generic types, smaller prize.
+
+** Pins added
+Cross-package generics (~programs/pkg-generic.flan~ and a new
+~pkgs/gen~ package — one generic at two element types, one calling another in
+its own package at its own variable so the transitive copy is generated from a
+call site two files away, and a local generic calling across the boundary at
+its own ~$t~), both backends and -O0; the package bound refused at the call
+with the clause quoted; the literal family at six numeric types in the
+generics corpus row; the prelude's three under their real names including
+~zero?~ at ~-0.0~; both widening orders refusing; the written conversion and
+the untyped literal still accepted; the fn-literal path unaffected; ~(zeroed)~
+still getting its want; ~$t~ at dyn and at ~(Option dyn)~; a bounded variable
+still refused by its bound; the abandoned-trial copy count; and the three
+reworded messages.
+
+Dev-loop reload needed nothing: test_session already pins ~C-c C-c~ on a
+generic installing its copies, the callee side, the absence of a stale cache
+across two evaluations, and a redefinition that needs a copy the process was
+never built with.
diff --git a/lib/check.ml b/lib/check.ml
index 0e4b2f9..a3dffc2 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -7882,8 +7882,18 @@ and trial ctx f =
      fresh ones and nothing refers to the orphan — and it rides along into the
      module as a function nobody calls. Left alone because [env] is the
      program's table and not this form's, and rewinding it would mean deciding
-     what else on [env] a trial may have touched; the generic instantiation
-     cache already rolls itself back, in [instantiate].
+     what else on [env] a trial may have touched.
+
+     The generic instantiation cache is the other table a trial reaches, and
+     it does not rewind either. [instantiate] rewinds a copy whose *body*
+     refused, which is a different event from a copy the caller abandoned —
+     and the abandoned one does not need rewinding. A generic call's
+     instantiation is read off its arguments and never off the ambient want:
+     an unbound variable is checked with no expectation at all, and a bound
+     one does not widen. So the trial and the live pass ask [instantiate] for
+     the same types, the second ask is a cache hit on the first, and exactly
+     one copy exists either way. Pinned in test_flan, "a generic inside an
+     abandoned trial".
 
      Only [Loc.Error] is caught. A timeout or a stack overflow is not a
      refusal to reconsider, and silently continuing past one would turn a
diff --git a/test/dune b/test/dune
index fe33b84..62338d6 100644
--- a/test/dune
+++ b/test/dune
@@ -60,6 +60,10 @@
   ; it defines a get of its own — shadow-builtin.flan, which is the pin that
   ; a shadow stops at the file that declared it.
   (glob_files programs/pkgs/shadowed/*)
+  ; The package whose exports are generic, which pkg-generic.flan and
+  ; pkg-generic-reject.flan import: the body has to be present where the copy
+  ; is made, so the directory comes whole like every other package.
+  (glob_files programs/pkgs/gen/*)
   ; The synthetic C header the importer's table reads. Committed rather than
   ; reached for on the machine: the raylib case needs raylib installed, at the
   ; right version, with a variable set, so it skips everywhere and covers
@@ -221,7 +225,8 @@
   (glob_files programs/pkgs/macring/*)
   (glob_files programs/pkgs/macspin/*)
   ; And the package shadow-builtin.flan imports.
-  (glob_files programs/pkgs/shadowed/*))
+  (glob_files programs/pkgs/shadowed/*)
+  (glob_files programs/pkgs/gen/*))
  (action (run ./test_valgrind.exe)))
 
 ; The corpus a fourth time, through the hand-written x86-64 backend, compared
@@ -280,7 +285,8 @@
   (glob_files programs/pkgs/macring/*)
   (glob_files programs/pkgs/macspin/*)
   ; And the package shadow-builtin.flan imports.
-  (glob_files programs/pkgs/shadowed/*))
+  (glob_files programs/pkgs/shadowed/*)
+  (glob_files programs/pkgs/gen/*))
  (action
   (setenv SURVEY_STRICT 1
    (setenv SURVEY_QUIET 1
@@ -445,7 +451,8 @@
   (glob_files programs/pkgs/macring/*)
   (glob_files programs/pkgs/macspin/*)
   ; And the package shadow-builtin.flan imports.
-  (glob_files programs/pkgs/shadowed/*))
+  (glob_files programs/pkgs/shadowed/*)
+  (glob_files programs/pkgs/gen/*))
  (action
   (setenv SURVEY_STRICT 1
    (setenv SURVEY_QUIET 1
diff --git a/test/programs/pkg-generic-reject.flan b/test/programs/pkg-generic-reject.flan
new file mode 100644
index 0000000..29d36b7
--- /dev/null
+++ b/test/programs/pkg-generic-reject.flan
@@ -0,0 +1,12 @@
+;;;; The call-site half of a bound written in another file.
+;;;;
+;;;; gen/largest is {:where (ordered? $t)}, and a [string] is not ordered. The
+;;;; refusal has to arrive here, against the call that asked for the copy, and
+;;;; it has to quote the clause — a message pointing into pkgs/gen/gen.flan
+;;;; would be naming a line the caller did not write and cannot change.
+(import gen "pkgs/gen")
+
+(defn main [] i32
+  (let [ss ["a" "b"]]
+    (println (gen/largest (slice ss 0 2))))
+  0)
diff --git a/test/programs/pkg-generic.flan b/test/programs/pkg-generic.flan
new file mode 100644
index 0000000..58a7289
--- /dev/null
+++ b/test/programs/pkg-generic.flan
@@ -0,0 +1,35 @@
+;;;; A generic defined in a package, instantiated by the program.
+;;;;
+;;;; The copies are made here, from a body written there. Three things are
+;;;; being asserted and only the first is obvious: that the call works at all;
+;;;; that instantiation is still transitive across the boundary, so gen/ends
+;;;; asking for gen/last-of at its own variable generates that copy from this
+;;;; file's call site; and that a {:where} clause written in the package is
+;;;; what a caller here is judged against.
+;;;;
+;;;; And one thing in the other direction: a generic written *here* calling a
+;;;; generic written *there* at its own variable, which is the shape that only
+;;;; resolves once both bodies are in one namespace.
+
+(import gen "pkgs/gen")
+
+;;; Local generic over the imported one, at this file's variable.
+(defn tail-twice [s [$t]] $t
+  {:where (numeric? $t)}
+  (+ (gen/ends s) (gen/ends s)))
+
+(defn main [] i32
+  (let [ns [5 3 9 1]
+        fs [2.5 0.5 1.5]]
+    ;; One package generic at two element types: two copies, one body.
+    (println (gen/last-of (slice ns 0 4)))
+    (println (gen/last-of (slice fs 0 3)))
+    ;; The transitive one, also at two.
+    (println (gen/ends (slice ns 0 4)))
+    (println (gen/ends (slice fs 0 3)))
+    ;; The bounded one.
+    (println (gen/largest (slice ns 0 4)))
+    ;; And the local generic that calls across the boundary at its own $t.
+    (println (tail-twice (slice ns 0 4)))
+    (println (tail-twice (slice fs 0 3))))
+  0)
diff --git a/test/programs/pkgs/gen/gen.flan b/test/programs/pkgs/gen/gen.flan
new file mode 100644
index 0000000..24146a0
--- /dev/null
+++ b/test/programs/pkgs/gen/gen.flan
@@ -0,0 +1,33 @@
+;;;; A package whose exports are generic.
+;;;;
+;;;; The spike's "no plan" bucket named this one, and named what makes it
+;;;; work: Load flattens every import into one namespace *before* the checker
+;;;; runs, so the generic's body is present at the call site the way a C++
+;;;; template's is because it sits in a header. Nothing here crosses a real
+;;;; compilation-unit boundary, and the day a package becomes one, this is the
+;;;; thing that has to change — a copy is made from a body, and a body that
+;;;; did not cross cannot be copied.
+;;;;
+;;;; What this package is for: a generic called from the program at two types,
+;;;; a bounded generic whose {:where} has to be readable from outside the
+;;;; file that wrote it, and a generic that calls another generic in its own
+;;;; package at its own variable, so the transitive copy is generated from a
+;;;; call site two files away.
+
+(defn last-of [s [$t]] $t
+  (at s (- (len s) 1)))
+
+;;; Calls last-of at its own variable: the copy of last-of is generated when
+;;; this is instantiated, and this is instantiated from the program.
+(defn ends [s [$t]] $t
+  (last-of s))
+
+;;; The bound travels with the signature. A caller that passes a type the
+;;; clause refuses is refused at the call, against a requirement written in
+;;; another file.
+(defn largest [s [$t]] $t
+  {:where (ordered? $t)}
+  (let [m (at s 0)]
+    (dotimes [i (len s)]
+      (set m (max m (at s i))))
+    m))
diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml
index 1a2dbc0..7bbbe26 100644
--- a/test/test_acceptance.ml
+++ b/test/test_acceptance.ml
@@ -2513,6 +2513,30 @@ let () =
        raylib itself. Loading it twice would declare every binding twice. *)
     outputs "a package reached along two routes" "programs/pkg-shared.flan"
       "ok\n";
+    (* A generic defined in a package and instantiated by the program. The
+       spike's "no plan" bucket named this and named what makes it work: Load
+       flattens every import into one namespace before the checker runs, so
+       the generic's *body* is present where the copy is made, the way a C++
+       template's is because it sits in a header. It is also the thing that
+       has to change the day a package becomes a real compilation unit — a
+       copy is made from a body, and a body that did not cross cannot be
+       copied.
+
+       Three shapes, because only the first is obvious. gen/last-of at two
+       element types is one body and two copies. gen/ends calls gen/last-of at
+       its *own* variable, so that copy is generated from this file's call
+       site and instantiation is still transitive across the boundary. And
+       tail-twice is a generic written here calling one written there at its
+       own $t, which only resolves once both bodies are in the one namespace.
+
+       The numbers are: last-of at i32 and f64, ends at the same two, largest
+       at i32, and tail-twice at both. *)
+    outputs "a generic defined in a package" "programs/pkg-generic.flan"
+      "1\n1.5\n1\n1.5\n9\n2\n3\n";
+    outputs ~opt:"-O0" "a generic defined in a package, -O0"
+      "programs/pkg-generic.flan" "1\n1.5\n1\n1.5\n9\n2\n3\n";
+    (* The call-site half of a bound written in another file is pinned with
+       the other refusals, further down — see "a package generic's bound". *)
     (* And the diamond with a type crossing it, which is the case the dedupe
        exists for rather than a restatement of the one above. pkg-diamond
        imports area and draw; both import shape; a shape/Box is built inside
@@ -2660,6 +2684,18 @@ let () =
        beneath it, naming rl/with-mode-2d at the call site rather than
        pointing into the package — that half is rendering and is not asserted
        here. *)
+    (* A {:where} clause travels with the signature across a package
+       boundary, and the refusal it produces lands at the call. Both halves
+       are asserted because only together are they the Elm-grade answer: the
+       type that failed and the clause it failed against, quoted here rather
+       than pointed at in pkgs/gen/gen.flan — a line the caller did not write
+       and cannot change. *)
+    refuses "a package generic's bound, refused at the call"
+      "programs/pkg-generic-reject.flan"
+      "string does not answer ordered?";
+    refuses "and the refusal quotes the clause the package wrote"
+      "programs/pkg-generic-reject.flan" "{:where (ordered? $t)}";
+
     refuses "with-mode-2d written without a camera"
       "programs/rl-with-reject.flan"
       "with-mode-2d-takes-a-camera-and-a-body";
diff --git a/test/test_flan.ml b/test/test_flan.ml
index 9965aca..cd985b9 100644
--- a/test/test_flan.ml
+++ b/test/test_flan.ml
@@ -4721,6 +4721,47 @@ let () =
   accepts "and is accepted when it is"
     "(defn outer [s [$t]] () {:where (ordered? $t)} (sort s))";
 
+  (* ── A generic call inside an abandoned widening trial ──────────────
+     The two features land days apart and meet here. A binary operator whose
+     operands disagree re-checks the right one at the left one's type inside a
+     [trial], and on a refusal reconsiders with the join — so a generic call
+     written on the right is checked twice, once in a pass that is thrown
+     away. What the discarded pass leaves behind in [env] is the question, and
+     [env] is the program's table, not the form's: an instantiation made
+     during it does not go back out, because [instantiate] rewinds only a copy
+     whose *body* refused.
+
+     It does not have to. The answer is that the two passes cannot disagree
+     about which copy to make, and that is a consequence of the rule above
+     rather than luck: a generic call's instantiation is read off its
+     arguments and never off the ambient want — an unbound variable is checked
+     with no expectation at all, and a bound one no longer widens — so the
+     trial and the live pass ask [instantiate] for the same types, and the
+     second ask is a cache hit on the first. One copy is emitted, at the type
+     the arguments chose, and the widening happens around the call.
+
+     (twoq 2 3) is i32 both times; the i8 on the left is what moves. *)
+  (let p =
+     checked
+       "(defn twoq [a $t  b $t] $t {:where (numeric? $t)} (+ a b))\n\
+        (defn main [] () (let [small (i8 1)] \
+          (println (+ small (twoq 2 3)))))"
+   in
+   let copies =
+     List.filter
+       (fun (f : Tast.fn) ->
+          String.length f.Tast.name >= 5 && String.sub f.Tast.name 0 5 = "twoq-")
+       p.Tast.fns
+   in
+   match copies with
+   | [ { Tast.name = "twoq-i32"; _ } ] -> ()
+   | l ->
+     check
+       (Printf.sprintf
+          "a generic inside an abandoned trial is instantiated once: %s"
+          (String.concat " " (List.map (fun (f : Tast.fn) -> f.Tast.name) l)))
+       false);
+
   (* ── 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