A conversion asks the bound, not a type the variable does not have

(i32 (at xs i)) inside a body bounded integer? was refused with "i32
converts a number, found t". Arithmetic, comparison, min/max, the
bitwise fold and the shifts all ask the where clause; the conversions
were the family nobody had gone back to, and the cast block held three
arms of it.

The machine-type target asked Types.is_numeric of its operand and the
enum target asked Types.Int _, so a variable fell through both to the
refusal however it was bounded. The variable target had the opposite
defect: it asked the bound of the target and then took any generic
operand, so a second variable declared only ordered? passed the abstract
pass on the strength of a sentence about a different one. Nothing wrong
was ever emitted through it — ordered? admits numbers and enums and both
convert at the instantiation — which is exactly why it is worth closing:
the hole opens the day ordered? admits a type that does not.

The rule is the repo's own, applied to a set instead of a type: a
conversion is legal at a bounded variable exactly when it is legal at
every type the bound admits. A machine-type target needs numeric?, an
enum target needs integer? because numeric? admits the floats the
concrete arm refuses, and ordered?/equal?/hashable? admit nothing — the
last by what the predicate says rather than by the set it denotes, since
hashable? already admits strings and ordered? may.

Both float targets and the narrowing i32 stay legal: (f64 i64-x) rounds
above 2^53 and (i32 f64-x) truncates where the types are written, and a
generic that refused what its copies accept would be the fork the rule
forbids. FIX.org, 2026-09-21, has the account, and records what this
costs: no predicate now licenses a generic enum to integer conversion,
and enum? is the eventual answer.

The refusal says what the variable is known to be and what to write, in
the clause spelling unconstrained already uses: a body with no clause
gets the clause, a body that has one is told which predicate to add.

FIX.org

@@ -4739,3 +4739,143 @@ To remove it, three edits together:
    defenum, and the paragraph above it that explains the alias
 3. vendor/raylib/bindings — delete the ~constant TraceLogLevel/warning~ line
    and its comment
+
+* A conversion under a bound, 2026-09-21
+
+** The report
+~(defn total [xs [$t]] i32 {:where [(integer? $t)]} ... (i32 (at xs i)) ...)~
+was refused with "i32 converts a number, found t". The bound says every type
+the body is copied at is an integer, an integer is a number, and the
+conversion is exactly what the bound exists to license.
+
+** The root cause, and it is narrower than "predicates are not consulted"
+Arithmetic, comparison, min/max, the bitwise fold and the shifts all ask the
+bound — each pairs an ~unconstrained ... ~needs:~ call with an ~|| generic_ty~
+escape, and the shifts had already been taught ~integer?~. The conversions
+were the family nobody had gone back to. Three arms in lib/check.ml, all in
+the cast block:
+
+1. ~is_cast~ (a machine type in head position) asked ~Types.is_numeric~ of the
+   operand and nothing else, so a variable — which has no type yet — fell
+   through to the refusal. This is the reported bug.
+2. The enum target asked ~Types.Int _~ of the operand, the same way, so
+   ~(K n)~ inside a generic body was refused however the variable was bounded.
+3. The *variable* target — ~(t x)~ — had the opposite defect. It asked the
+   bound of the target and then accepted any ~generic_ty~ operand, so a
+   second variable declared only ~ordered?~ passed the abstract pass on the
+   strength of a sentence about a different variable. That one was an
+   acceptance, not a refusal, and tightening it is part of this entry.
+
+   It was not reachable, and saying so is the honest version. ~ordered?~ is
+   ~Types.is_comparable~, which admits numbers and enums and nothing else,
+   and every one of those converts at the concrete arm; a string is refused
+   at the instantiation before any of this. So no wrong program was ever
+   compiled through it. What it was is a hole that opens the day ~ordered?~
+   admits a type that does not convert — which is the same future the rule
+   below refuses to bet against, and the best evidence for it: a check keyed
+   to the set a predicate denotes today is correct today and silently wrong
+   later, where one keyed to what the predicate claims stays correct across
+   the widening.
+
+** The rule
+A conversion is legal at a bounded variable exactly when it is legal at every
+type the bound admits, which is the repo rule that generic and concrete code
+compute the same thing, applied to a set instead of a type. Read off the
+concrete arm, that gives one predicate per target:
+
+- A machine-type target needs ~numeric?~. Every type it admits converts to
+  every numeric target today.
+- An enum target needs ~integer?~. ~numeric?~ admits f32 and f64, and the
+  concrete arm refuses a float to an enum — sub-decision 3 of the cast block.
+- ~ordered?~, ~equal?~ and ~hashable?~ admit nothing.
+
+And per predicate:
+
+- Under ~integer?~ every conversion is legal, the float targets included.
+  ~(f64 x)~ at an unknown-width integer is *not* value-preserving — i64 to
+  f64 rounds above 2^53 — and it is allowed anyway, because the written
+  ~(f64 i64-x)~ is allowed and a conversion has never claimed the value
+  survives. Refusing it at the variable would make the generic stricter than
+  the code it is copied into, which is the fork the rule forbids.
+- Under ~numeric?~ every conversion to a number is legal, ~(i32 x)~ included,
+  and it may truncate a float. Same reasoning from the other side: ~(i32
+  f64-x)~ truncates towards zero where the type is written, so the bound
+  cannot refuse what the copy would accept. The enum target is the one thing
+  ~numeric?~ does not buy.
+- Under ~ordered?~ or ~equal?~ alone, refused.
+
+That last one is the only place the "legal at every admitted type" test does
+not decide it, and it is worth naming rather than hiding. ~Types.is_comparable~
+admits numbers and enums and nothing else today, so every type ~ordered?~
+currently admits does in fact convert — the test taken literally would allow
+it. It is still refused, because the predicate is a claim about ordering and
+not about numbers: the day ~ordered?~ admits strings by a chosen collation
+(plan.org, Types leaves that open), a conversion keyed to it would silently
+start meaning something else. Predicates gate operations by what they say,
+not by the set they happen to denote this week. ~hashable?~ makes the point
+without any argument at all: it admits strings and structs now.
+
+** The diagnostics
+The old line named the variable by its bare spelling, said only what was
+wanted, and said nothing about the clause the reader would have to edit —
+"i32 converts a number, found t" against a body whose signature says ~$t~.
+The refusal now says what the variable is known to be and what to write:
+
+  i32 converts a number. The where clause says t is ordered?, and that does
+  not make it a number — add (numeric? $t) to the where clause
+
+  i32 converts a number. Nothing here says t is a number — write
+  {:where (numeric? $t)} at the head of the body
+
+  K converts an integer to an enum. The where clause says t is numeric?, and
+  that does not make it an integer — add (integer? $t) to the where clause
+
+Both spellings compile as written, and the clause is spelled the way
+~unconstrained~ already spells it so the family says it one way: a body with
+no clause is handed the whole clause, a body that already has one is told
+which predicate to add rather than a clause that would drop the predicates it
+has.
+
+** Tests
+test/test_flan.ml pins each conversion generic and concrete side by side —
+the narrowing i32, the widening f64, an unsigned target, and the enum
+direction — and each refusal against its whole message.
+test/programs/int-generic.flan runs the reported program and its concrete
+twin at -O2 and -O0. No x86 row was added: the checker decides more programs
+are legal without changing what any of them emits, and the Cast they emit is
+the one widening.flan already pins on x86.
+
+** Left alone, found while here
+- ~(total v)~ where v is ~[3 i32]~ and the parameter is ~[$t]~ is refused,
+  and a written ~[i32]~ parameter refuses the same array with the same
+  reasoning. Not a fork; an array is not a slice, and the slice/as-slice lane
+  owns whatever changes there.
+- ~i64->bytes~ takes its argument at ~~want:(Types.Int Types.I64)~, so a
+  written i32 or u8 is *accepted* — implicit widening reaches it — while a
+  ~$t~ under ~integer?~ is refused. That is not a fork either, and the reason
+  is the rule rather than symmetry: ~u64~ is refused concretely ("neither
+  widens into the other, so the conversion has to be written"), so ~integer?~
+  admits a type at which the conversion is illegal, and a bound that admits
+  one such type cannot license the operation. ~bytes->i64~ has no argument
+  type to disagree about. Untouched.
+- ~print~/~println~ over a bounded variable already defers to the
+  instantiation and needed nothing.
+
+** Open: there is now no generic enum → integer conversion
+Worth recording as a loss rather than leaving the next reader to find it.
+None of the five predicates admits enums while licensing a cast — ~numeric?~
+excludes them, and ~ordered?~ and ~equal?~ admit them but no longer convert.
+Before this entry the one spelling that worked was ~(t x)~ with the *target*
+bounded ~ordered?~, through the arm item 3 above closes, so the loss is real
+and removing it is still right: it worked by not asking about the operand at
+all.
+
+~enum?~ is the eventual answer and it is not a one-liner, which is why it is
+written here rather than done here. It entails ~ordered?~ and ~equal?~ —
+enums compare and are equal — and it does *not* entail ~numeric?~, because
+arithmetic on an enum is refused where the type is written. So the cast rule
+stops being one predicate per target and becomes a disjunction, ~numeric?~ or
+~enum?~ for a machine-type target, and the refusal has to name whichever one
+the reader meant. A cast *to* a variable bounded ~enum?~ is a second question
+with its own answer. Each of those is a decision, not a fill-in, and the
+author has not been asked.

lib/check.ml

@@ -5674,6 +5674,59 @@ and not_numeric name what (a : Tast.expr) =
   else
     fail where "%s takes %s, found %s" name what (Types.to_string a.Tast.ty)
 
+(* ── A conversion whose operand is a type variable ─────────────────────
+   [(i32 x)] where [x] is a [$t]. The concrete question — is this a number —
+   has no answer during the abstract pass, and asking it anyway is what
+   refused [(i32 (at xs i))] inside a body bounded [integer?]. The question
+   the bound can answer is the one asked here: does what the [where] clause
+   declares about the variable entail the predicate this conversion needs.
+
+   Which predicate that is comes from the *target*, and the rule is the
+   concrete arm's rule read off a set rather than a type: a conversion legal
+   at every type the bound admits is legal at the variable, and one illegal at
+   any of them is refused. A number target needs [numeric?] — every type it
+   admits converts to every numeric target today, truncating or rounding by
+   the same rule a written f64 follows. An enum target needs [integer?],
+   because [numeric?] admits f32 and f64 and a float has no enum reading.
+
+   [ordered?], [equal?] and [hashable?] are refused: they say what can be
+   compared, not what is a number, and nothing about a bound that only orders
+   says a conversion means anything. That they happen to admit only numbers
+   and enums today is a fact about [Types.is_comparable], not about what the
+   predicate claims — keying conversions to it would make widening [ordered?]
+   to strings a silent change to what converts.
+
+   The message says what the variable is known to be and what to write. Both
+   spellings compile as written, and the clause spelling is [unconstrained]'s
+   so that the family says it one way: a body with no clause is given the
+   whole clause, and a body that already has one is told which predicate to
+   add rather than a clause that would drop the ones it has. *)
+and cast_operand ctx loc name ~needs ~what ~is v =
+  if declares ctx.env.tvpreds v needs then ()
+  else
+    let declared =
+      List.filter_map
+        (fun (p : Ast.pred) ->
+           if String.equal p.Ast.pvar v then Some p.Ast.pname else None)
+        ctx.env.tvpreds
+    in
+    let known =
+      match declared with
+      | [] -> Printf.sprintf "Nothing here says %s is %s" v is
+      | ps ->
+        Printf.sprintf
+          "The where clause says %s is %s, and that does not make it %s" v
+          (String.concat " and " ps) is
+    in
+    let fix =
+      if ctx.env.tvpreds = [] then
+        Printf.sprintf "write {:where (%s $%s)} at the head of the body"
+          needs v
+      else Printf.sprintf "add (%s $%s) to the where clause" needs v
+    in
+    Loc.failk "check/unconstrained-type-variable" loc
+      "%s converts %s. %s — %s" name what known fix
+
 and fold_left_prim ctx ~want loc name p ~needs ok what args =
   let x, y, rest =
     match args with x :: y :: rest -> x, y, rest | _ -> assert false
@@ -7993,6 +8046,13 @@ and named_call ?(qualified = false) ctx ~want loc name args =
     let a = check ctx (List.hd args) in
     (match a.Tast.ty with
      | Types.Int _ -> ()
+     (* A type variable, answered by its bound rather than by a type it does
+        not have yet: [integer?] admits exactly the integer kinds, which is
+        what sub-decision 3 above asks for, and [numeric?] is a bound too wide
+        because it admits the floats that decision refuses. *)
+     | Types.Var v ->
+       cast_operand ctx loc name ~needs:"integer?" ~what:"an integer to an enum"
+         ~is:"an integer" v
      | other ->
        fail loc "%s converts an integer to an enum, found %s — an enum or a \
                  float goes through (i32 x) first" name
@@ -8015,7 +8075,18 @@ and named_call ?(qualified = false) ctx ~want loc name args =
     let a = check ctx (List.hd args) in
     (match a.Tast.ty with
      | Types.Enum _ -> ()
-     | t when Types.is_numeric t || generic_ty t -> ()
+     | t when Types.is_numeric t -> ()
+     (* The operand's own bound, asked the same way the target's was one line
+        up. Accepting every [generic_ty] here took the target's [numeric?] as
+        if it said something about the operand, so a second variable declared
+        only [ordered?] passed the abstract pass. Nothing wrong was ever
+        emitted — [ordered?] admits numbers and enums and both convert at the
+        instantiation — which is the point: the hole is only reachable the day
+        [ordered?] admits a type that does not, and that day is why the
+        question is asked of the predicate and not of the set it denotes. *)
+     | Types.Var v ->
+       cast_operand ctx loc name ~needs:"numeric?" ~what:"a number"
+         ~is:"a number" v
      | t -> fail loc "%s converts a number, found %s" name (Types.to_string t));
     prim (Tast.Cast target) target [ a ]
   | _ when is_cast name && List.length args = 1 ->
@@ -8029,6 +8100,12 @@ and named_call ?(qualified = false) ctx ~want loc name args =
         admits. *)
      | Types.Dyn -> ()
      | t when Types.is_numeric t -> ()
+     (* The operand of a conversion inside a generic body. The target is a
+        machine type, so what is in question is only the operand, and the
+        [where] clause is what answers it. *)
+     | Types.Var v ->
+       cast_operand ctx loc name ~needs:"numeric?" ~what:"a number"
+         ~is:"a number" v
      | t -> fail loc "%s converts a number, found %s" name (Types.to_string t));
     (match a.Tast.ty with
      | Types.Dyn -> cast_dyn ctx loc target a

spec-memory.md

@@ -329,6 +329,24 @@ reaches through a container or function type is still bound exactly, because
 a slice's elements cannot be rewritten. An untyped literal is unaffected: it
 has no type of its own to keep.
 
+**A conversion under a bound is legal exactly when it is legal at every type
+the bound admits.** `(i32 x)` asks whether `x` is a number, and inside a
+generic body no type is there to answer; the `where` clause answers for every
+copy at once. `numeric?` is what a conversion to a machine type needs —
+`integer?` entails it, so an `integer?` body converts too — and that covers
+narrowing and widening alike: `(i32 x)` on a written `f64` truncates towards
+zero and `(f64 x)` on a written `i64` rounds above 2^53, neither is refused
+where the type is written, so neither is refused at the variable. A conversion
+was never a claim that the value survives. The conversion *to* an enum needs
+`integer?` exactly, because an enum is an `i32` and a float has no enum
+reading, and `numeric?` would admit an `f32` copy the concrete rule refuses.
+`ordered?`, `equal?` and `hashable?` admit no conversion at all: they say what
+can be compared or keyed, not what is a number — and that is a claim about
+what the predicate says, not about the set it denotes today, which currently
+does admit only numbers and enums. The refusal names the predicate to write
+(FIX.org 2026-09-21). One consequence is recorded there as open: no predicate
+now licenses a generic enum → integer conversion.
+
 **A type variable is not instantiated at `dyn`.** Two models answer "one body,
 many types" and they are not rivals: this one copies per written type at
 compile time, `defgeneric`/`defmethod` dispatch at run time on a value that

test/programs/int-generic.flan

@@ -54,6 +54,45 @@
   {:where (numeric? $t)}
   (+ a (+ b c)))
 
+;; ── Conversions under a bound ──────────────────────────────────────────
+;; A cast asks whether its operand is a number, and inside a generic body no
+;; type is there to answer. The bound answers instead, for every copy at
+;; once: integer? admits only integer kinds and every one of them converts,
+;; so the body is checked once here and the conversion is the ordinary one in
+;; each copy. This is the shape the bug report was written against — a sum
+;; that narrows each element to the i32 it accumulates in.
+(defn total [xs [$t]] i32
+  {:where (integer? $t)}
+  (let [acc 0]
+    (dotimes [i (len xs)] (set acc (+ acc (i32 (at xs i)))))
+    acc))
+
+;; The same rule widening. i64 → f64 rounds above 2^53 and i32 → f64 does
+;; not, and neither is refused when the type is written out, so neither is
+;; refused under the bound: a conversion is not a claim that the value
+;; survives, it is the claim that the operand is a number.
+(defn mean [xs [$t]] f64
+  {:where (integer? $t)}
+  (let [sum 0.0]
+    (dotimes [i (len xs)] (set sum (+ sum (f64 (at xs i)))))
+    (/ sum (f64 (len xs)))))
+
+;; numeric? is the weaker bound and narrowing is legal under it too, because
+;; it is legal at every type it admits: (i32 x) on a written f64 truncates
+;; towards zero, and that is what the f32 copy of this does.
+(defn truncate [x $t] i32
+  {:where (numeric? $t)}
+  (i32 x))
+
+;; The other direction, which is where the two bounds part company. An enum
+;; is an i32 and a float has no enum reading, so this one needs integer?
+;; exactly — numeric? would admit an f64 copy the concrete arm refuses.
+(defenum Step [back -1  stay 0  forward 1])
+
+(defn step-of [n $t] Step
+  {:where (integer? $t)}
+  (Step n))
+
 (defn main [] ()
   ;; abs, one body, six widths.
   (println (abs (i8 -7)))
@@ -109,4 +148,22 @@
   (let [ns [5 3 9 1]]
     (match (index-of (slice ns 0 4) (i16 9))
       (Some i) (println i)
-      _ (println -1))))
+      _ (println -1)))
+
+  ;; The conversions, generic and concrete side by side. Each pair is one
+  ;; conversion written twice — once at a bounded variable and once at the
+  ;; type a copy is made at — and the two answer the same number, which is
+  ;; the whole claim the bound makes.
+  (let [small [5 3 9 1]
+        wide  [(i64 5) (i64 3) (i64 9) (i64 1)]]
+    (println (total (slice small 0 4)))
+    (println (total (slice wide 0 4)))
+    (println (mean (slice small 0 4)))
+    (println (mean (slice wide 0 4))))
+  (println (truncate (i64 9)))
+  (println (truncate 2.75))
+  (println (truncate -2.75))
+  (println (i32 2.75))
+  (println (step-of 1))
+  (println (step-of (u8 0)))
+  (println (i32 (step-of (i64 -1)))))

test/test_acceptance.ml

@@ -2750,14 +2750,27 @@ let () =
        spells. Then the integer?-only operations at several widths, and last
        the join family: [true true], [6 6] and [42] are mixed widths at one
        $t answering identically in both argument orders, from one copy at
-       the wider type (FIX.org 2026-09-20). The closing [2] is an i16 scalar
+       the wider type (FIX.org 2026-09-20). The [2] after them is an i16
-       widening into the i32 a slice fixed index-of's $t at — the one
+       scalar widening into the i32 a slice fixed index-of's $t at — the one
-       direction a container-bound variable admits. *)
+       direction a container-bound variable admits.
+
+       The last eleven lines are the conversions. The two [18]s and the two
+       [4.5]s are one sum and one mean over an i32 slice and an i64 slice —
+       narrowing and widening inside a body bounded [integer?], each pinned
+       at two widths rather than against a written-type twin. [9 2 -2] is
+       (i32 x) at i64, f64 and a negative f64 under [numeric?], and it is the
+       one pair here that really is generic beside concrete: the bare [2]
+       after it is the written (i32 2.75), truncating towards zero to the
+       same number the copy does. The enum direction closes it, an integer
+       variable converting to a Step at two widths and back. The written-type
+       twins of the other three are in test_flan.ml, where the pairing is
+       every case. *)
     let int_generic_out =
       "7\n7\n7\n7\n7\n7\n-2147483648\n-9223372036854775808\n\
        0\n0\n1.5\n2.5\n\
        7\n15\n31\ntrue\nfalse\ntrue\n240\n9\n5\n-2\n301\n301\n\
-       true\ntrue\n6\n6\n42\n2\n"
+       true\ntrue\n6\n6\n42\n2\n\
+       18\n18\n4.5\n4.5\n9\n2\n-2\n2\n:forward\n:stay\n-1\n"
     in
     outputs "integer? and the collapsed abs" "programs/int-generic.flan"
       int_generic_out;

test/test_flan.ml

@@ -5320,6 +5320,81 @@ let () =
     ~needle:"admits no float type"
     "(defn h [x $t] $t {:where (integer? $t)} (+ x 1.5))";
 
+  (* ── Conversions under a bound ───────────────────────────────────────
+     A cast asks whether its operand is a number, and a type variable has no
+     type to answer with — so the bound answers, and the rule is the concrete
+     arm's rule read off the set a predicate admits: a conversion legal at
+     every type the bound admits is legal at the variable, and one illegal at
+     any of them is refused there. Each pair below is the same conversion
+     written twice, once generic and once concrete, and the two agree. *)
+  accepts "integer? admits (i32 x), the narrowing conversion"
+    "(defn to32 [x $t] i32 {:where (integer? $t)} (i32 x))";
+  accepts "and the concrete conversion it stands for"
+    "(defn to32 [x i64] i32 (i32 x))";
+  (* Widening an integer to a float is admitted for the reason every other
+     cast is: (f64 x) on a written i64 rounds above 2^53 and is not refused,
+     so the bound does not refuse it either. A conversion is not a promise
+     that the value survives. *)
+  accepts "integer? admits (f64 x), the widening one"
+    "(defn tof [x $t] f64 {:where (integer? $t)} (f64 x))";
+  accepts "and the concrete widening it stands for"
+    "(defn tof [x i64] f64 (f64 x))";
+  (* numeric? admits floats, so (i32 x) under it can truncate — which is
+     exactly what (i32 x) on a written f64 does, so refusing it at the
+     variable would make the generic stricter than the code it copies. *)
+  accepts "numeric? admits (i32 x), which may truncate a float"
+    "(defn to32 [x $t] i32 {:where (numeric? $t)} (i32 x))";
+  accepts "and the concrete truncation it stands for"
+    "(defn to32 [x f64] i32 (i32 x))";
+  accepts "integer? admits an unsigned target"
+    "(defn tou [x $t] u8 {:where (integer? $t)} (u8 x))";
+  (* ordered?, equal? and hashable? say what can be compared or keyed, not
+     what is a number, so a conversion under one of them alone is refused —
+     and the message says which predicate to write. *)
+  rejects_check "ordered? does not admit a conversion"
+    ~needle:"The where clause says t is ordered?, and that does not make it \
+             a number — add (numeric? $t) to the where clause"
+    "(defn to32 [x $t] i32 {:where (ordered? $t)} (i32 x))";
+  rejects_check "nor does equal?"
+    ~needle:"add (numeric? $t) to the where clause"
+    "(defn to32 [x $t] i32 {:where (equal? $t)} (i32 x))";
+  rejects_check "nor does hashable?"
+    ~needle:"add (numeric? $t) to the where clause"
+    "(defn to32 [x $t] i32 {:where (hashable? $t)} (i32 x))";
+  (* With no clause at all the message hands over the whole clause rather
+     than a predicate to add to one that is not there. *)
+  rejects_check "an unbounded variable does not convert"
+    ~needle:"i32 converts a number. Nothing here says t is a number — write \
+             {:where (numeric? $t)} at the head of the body"
+    "(defn to32 [x $t] i32 (i32 x))";
+  (* The operand of a cast to a *variable* target is asked the same question
+     the target was: the target's bound says nothing about a second variable
+     standing in the argument. *)
+  accepts "a cast to a variable target takes a numeric? operand"
+    "(defn conv [x $u y $t] $t {:where [(numeric? $t) (numeric? $u)]} \
+       (if (< y y) (t x) (t x)))";
+  rejects_check "a cast to a variable target refuses an ordered? operand"
+    ~needle:"add (numeric? $u) to the where clause"
+    "(defn conv [x $u y $t] $t {:where [(numeric? $t) (ordered? $u)]} \
+       (if (< y y) (t x) (t x)))";
+  (* The enum direction, where the two numeric bounds part company: an enum
+     is an i32 and a float has no enum reading, so this conversion needs
+     integer? exactly — numeric? would admit an f64 copy that the concrete
+     arm two lines below refuses. *)
+  accepts "integer? admits the conversion to an enum"
+    "(defenum K [lo -1  hi 1])\n\
+     (defn as-k [n $t] K {:where (integer? $t)} (K n))";
+  rejects_check "numeric? does not, because it admits floats"
+    ~needle:"K converts an integer to an enum. The where clause says t is \
+             numeric?, and that does not make it an integer — add \
+             (integer? $t) to the where clause"
+    "(defenum K [lo -1  hi 1])\n\
+     (defn as-k [n $t] K {:where (numeric? $t)} (K n))";
+  rejects_check "and the concrete float it stands for is refused too"
+    ~needle:"K converts an integer to an enum, found f64"
+    "(defenum K [lo -1  hi 1])\n\
+     (defn as-k [n f64] K (K n))";
+
   accepts "a variable read twice under one predicate"
     "(defn twice [a $t] bool {:where (ordered? $t)} (< a a))";
   rejects_check "a predicate nobody has heard of"