A generic crosses a package boundary, and a trial leaves one copy

The two compositions the milestone owed, pinned, and the record of the
whole lane.

A package whose exports are generic: pkgs/gen, imported by
pkg-generic.flan at three shapes. One generic at two element types.
One that calls another in its own package at its own variable, so the
transitive copy is generated from a call site two files away. And a
generic written in the program calling one written in the package at
its own $t, which only resolves once Load has flattened both bodies
into one namespace -- the thing that has to change the day a package
becomes a real compilation unit, because a copy is made from a body
and a body that did not cross cannot be copied. Plus the call-site
half of a bound written in another file, quoted here rather than
pointed at in a file the caller cannot change.

And the composition with the widening trial. A binary operator
re-checks its right operand at its left one's type inside a trial, so
a generic call written there is checked twice and once thrown away.
The discarded pass's instantiation 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, so both passes ask for the same types and
the second ask is a cache hit. Pinned by counting the copies in the
checked program.

The widening lane's note said that cache already rewinds itself. It
does not. Corrected in the comment and in FIX.org, in place.

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
+mean deciding what else on ~env~ a trial may have touched.
-~env~ state that genuinely needs rewinding, the generic instantiation cache,
+
-already rewinds itself in ~instantiate~.
+[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.

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
+     what else on [env] a trial may have touched.
-     cache already rolls itself back, in [instantiate].
+
+     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

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

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)

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)

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))

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";

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