A char plus or minus an integer is a char checked to be a scalar value, a char minus a char is their distance, and dyn chars do the same.

TODO.org

@@ -31,8 +31,11 @@ dyn-unless-annotated design.
 CLOSED: [2026-09-26]
 Decision 127: a char literal is the number typed code wants there, and a =char= otherwise,
 an untyped array of char literals included; a =char= crosses into dyn as a dyn char, and
-only a dyn char unboxes into one. No arithmetic: =(i32 c)= and =(char n)= convert, the
+only a dyn char unboxes into one. =(i32 c)= and =(char n)= convert, the latter checked.
-latter checked. An untyped defconst of one is that literal where a number is wanted.
+Decision 131, Kotlin's: char ± int and int + char are a char, trapping off a scalar value
+(refused when constant); char - char is an i32; anything else, and comparing with an int,
+is refused; dyn does the same. A let-bound char beside an integer literal stays a char.
+An untyped defconst of one is that literal where a number is wanted.
 Printed as dyn prints one (129a). =runes-next= and =rune-at= give a char; the
 UTF-8 codec (=decode-rune=, =encode-rune=) stays on i32. Rules out the f(\a) fork.
 
@@ -44,9 +47,9 @@ literal, a control character as \\uXXXX. Into any integer width it gives its
 code point where that fits, into a byte only when ASCII; a dyn int into any width is
 range-checked, while a cast on either wraps as a typed cast does. length, at and slice
 on dyn text count code points, a malformed byte counting as one U+FFFD. A non-ASCII
-literal defaults to i32 and is refused where a byte is wanted. Rules out char
+literal defaults to i32 and is refused where a byte is wanted. Rules out a typed code
-arithmetic, a typed code point turning into a char unless =(char n)= says so, and byte
+point turning into a char unless =(char n)= says so, and byte offsets on dyn text. Char
-offsets on dyn text.
+arithmetic is decision 131's, under "A typed char".
 
 ** DONE String is a prelude struct over (Vec u8), kept valid by the checker
 CLOSED: [2026-09-26]

lib/check.ml

@@ -3113,6 +3113,10 @@ let check_fn_ref : (env -> Ast.fn -> Tast.fn) ref =
    by the declaration pass of the program being checked. *)
 let char_consts : (string, int) Hashtbl.t = Hashtbl.create 8
 
+(* A [+] or [-] pair found to be char arithmetic after the ordinary join
+   refused it, with both operands checked on their own terms. *)
+exception Char_pair of Tast.expr * Tast.expr
+
 (* Untyped literals: their machine type comes from context, so when one is an
    operand of a binary operator we look at the *other* operand first. *)
 let is_literal (e : Ast.expr) =
@@ -6682,10 +6686,11 @@ and int_literal loc ~want ?(preds = []) ?(default = Types.I32) n =
       n v v v
   | Some Types.Char ->
     Loc.failk literal_at_want loc
-      "the integer literal %Ld is not a char: a char is a character, not a \
+      "the integer literal %Ld is not a char, and a char compares only with \
-       number. Write the character as a char literal, or make one with %s"
+       a char. Take its code point with %s, or make a char with %s"
-      n (if Source.indented_at loc then Printf.sprintf "char(%Ld)" n
+      n (if Source.indented_at loc then "i32(c)" else "(i32 c)")
-         else Printf.sprintf "(char %Ld)" n)
+      (if Source.indented_at loc then Printf.sprintf "char(%Ld)" n
+       else Printf.sprintf "(char %Ld)" n)
   | Some other when other <> Types.Never ->
     Loc.failk literal_at_want loc "expected %s, found the integer literal %Ld"
       (tyname loc other) n
@@ -10906,16 +10911,62 @@ and not_numeric name what (a : Tast.expr) =
   else
     fail where "%s takes %s, found %s" name what (tyname where a.Tast.ty)
 
-(* A char is a character and not a number, so no operator computes with one;
+(* What a char refuses: every operator but [+] and [-] with an integer and
-   the refusal names the two conversions (decision 127). *)
+   [-] with a char ([char_step], decision 131). The refusal names the two
+   conversions. *)
 and char_arith loc name =
   let fln = fln_source loc in
   Loc.failk "check/char-arithmetic" loc
-    "%s does no arithmetic on a char: a char is a character, not a number. \
+    "%s. Take its code point with %s, and make a char of one with %s"
-     Take its code point with %s, and make a char of one with %s"
+    (match name with
-    name (if fln then "i32(c)" else "(i32 c)")
+     | "+" -> "+ adds an integer to a char, and not a char to a char"
+     | "-" -> "- takes an integer or a char from a char, and not a char from \
+               an integer"
+     | _ -> name ^ " does no arithmetic on a char")
+    (if fln then "i32(c)" else "(i32 c)")
     (if fln then "char(n)" else "(char n)")
 
+(* One step of char arithmetic (decision 131, Kotlin's rules): a char plus or
+   minus an integer is a char, checked to be a scalar value — at compile time
+   when both sides are constants, by [flan_char_of] at run time otherwise —
+   and a char minus a char is the distance between them, an i32. Anything
+   else with a char in it is refused. *)
+and char_step _ctx loc name (a : Tast.expr) (b : Tast.expr) : Tast.expr =
+  let i64 e = widen loc dyn_i64 e in
+  let const (e : Tast.expr) =
+    match e.Tast.e with Tast.Int (n, _) -> Some n | _ -> None
+  in
+  let op = if String.equal name "+" then Tast.Add else Tast.Sub in
+  let fold f = match const a, const b with
+    | Some x, Some y -> Some (f x y) | _ -> None
+  in
+  let apply x y = if String.equal name "+" then Int64.add x y else Int64.sub x y in
+  match a.Tast.ty, b.Tast.ty with
+  | Types.Char, Types.Char when String.equal name "-" ->
+    (match fold Int64.sub with
+     | Some n -> mk loc (Types.Int Types.I32) (Tast.Int (n, Types.I32))
+     | None ->
+       let i32 e = widen loc (Types.Int Types.I32) e in
+       mk loc (Types.Int Types.I32) (Tast.Prim (Tast.Sub, [ i32 a; i32 b ])))
+  | Types.Char, Types.Int _ | Types.Int _, Types.Char
+    when not (String.equal name "-" && b.Tast.ty = Types.Char) ->
+    (match fold apply with
+     | Some n ->
+       if Int64.compare n 0L >= 0 && Int64.compare n 0x10ffffL <= 0
+          && not (Int64.compare n 0xd800L >= 0 && Int64.compare n 0xdfffL <= 0)
+       then mk loc Types.Char (Tast.Int (n, Types.U32))
+       else
+         Loc.failk "check/char-range" loc
+           "this is %Ld, which is not a Unicode scalar value, so it is not a \
+            char. A char is a code point from 0 to 0x10FFFF, outside 0xD800 \
+            to 0xDFFF" n
+     | None ->
+       let sum = mk loc dyn_i64 (Tast.Prim (op, [ i64 a; i64 b ])) in
+       rt loc Types.Char "flan_char_of" [ sum; here loc ])
+  | _ ->
+    char_arith (if a.Tast.ty = Types.Char then a.Tast.loc else b.Tast.loc) name;
+    assert false
+
 (* ── 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
@@ -10989,14 +11040,32 @@ 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
   in
+  let charish = String.equal name "+" || String.equal name "-" in
   let a, b =
-    char_operands ctx name [ x; y ] (fun () ->
+    try
-        binary ctx ~dyn_ok:true name loc ~want:(numeric_want want) [ x; y ])
+      (* An integer literal then a char literal, where no number is wanted:
+         char arithmetic, which the join would read the other way round. *)
+      (match x.Ast.e, y.Ast.e, numeric_want want with
+       | Ast.Int _, Ast.Byte _, None when charish ->
+         raise_notrace (Char_pair (check ctx x, check ctx y))
+       | _ -> ());
+      char_operands ctx ~charish name [ x; y ] (fun () ->
+          binary ctx ~dyn_ok:true ~char_ok:charish name loc
+            ~want:(numeric_want want) [ x; y ])
+    with Char_pair (a, b) -> a, b
   in
   (* One dyn operand makes the whole fold dyn, whichever side it is on. The
      typed side is boxed by [dyn_fold]; a literal was already built at dyn by
      [binary], so [(+ x 1)] over a dyn x folds an i64 one. *)
-  if a.Tast.ty = Types.Dyn || b.Tast.ty = Types.Dyn then
+  if charish && (a.Tast.ty = Types.Char || b.Tast.ty = Types.Char)
+     && a.Tast.ty <> Types.Dyn && b.Tast.ty <> Types.Dyn then
+    let acc =
+      List.fold_left
+        (fun acc arg -> char_step ctx loc name acc (check ctx arg))
+        (char_step ctx loc name a b) rest
+    in
+    expect ctx loc ~want acc
+  else if a.Tast.ty = Types.Dyn || b.Tast.ty = Types.Dyn then
     dyn_fold ctx ~want loc name [ a; b ] rest
   else begin
   (* [~needs] is the operator's own bound: [numeric?] for the arithmetic,
@@ -11024,9 +11093,24 @@ and fold_left_prim ctx ~want loc name p ~needs ok what args =
 (* A pair an arithmetic operator refused, when one operand is a char: that
    is the refusal to give, rather than the mismatch between the two. Asked
    only after the refusal, so a pair that checks costs nothing more. *)
-and char_operands ctx name (args : Ast.expr list) f =
+and char_operands ctx ?(charish = false) name (args : Ast.expr list) f =
   try f ()
   with Loc.Error _ as ex ->
+    (* [+] and [-] take a char beside an integer (decision 131): the pair is
+       read again on its own terms, and [char_step] decides. *)
+    let own () =
+      List.map (fun a -> trial ctx (fun () -> check ctx a)) args
+    in
+    (match charish, args with
+     | true, [ x; y ] ->
+       (match own () with
+        | [ Ok a; Ok b ]
+          when (a.Tast.ty = Types.Char
+                && (Types.is_integer b.Tast.ty || b.Tast.ty = Types.Char))
+               || (b.Tast.ty = Types.Char && Types.is_integer a.Tast.ty) ->
+          raise_notrace (Char_pair (check ctx x, check ctx y))
+        | _ -> ())
+     | _ -> ());
     (* A char literal beside a number is that number, so it says nothing
        unless every operand is a literal. *)
     let all_lit = List.for_all is_literal args in
@@ -12294,7 +12378,10 @@ and named_call ?(qualified = false) ctx ~want loc name args =
      nobody writes on purpose. *)
   | "%" ->
     arity ctx loc name 2 args;
-    let a, b = binary ctx ~dyn_ok:true name loc ~want:(numeric_want want) args in
+    let a, b =
+      char_operands ctx name args (fun () ->
+          binary ctx ~dyn_ok:true name loc ~want:(numeric_want want) args)
+    in
     if a.Tast.ty = Types.Dyn || b.Tast.ty = Types.Dyn then
       dyn_fold ctx ~want loc name [ a; b ] []
     else begin
@@ -12320,7 +12407,28 @@ and named_call ?(qualified = false) ctx ~want loc name args =
        the two, and every operand after them is checked against the answer.
        Past the first pair nothing widens, which is [fold_left_prim]'s rule
        and not a second one. *)
-    let a, b = binary ctx ~dyn_ok:true name loc ~want:None [ x; y ] in
+    let a, b =
+      try binary ctx ~dyn_ok:true name loc ~want:None [ x; y ]
+      with Loc.Error _ as ex ->
+        (* A char beside an integer: said as the char's rule, not as the
+           mismatch (decision 131). *)
+        (* Neither a literal, whose own refusal already says what it is. *)
+        (match
+           if is_literal x || is_literal y then []
+           else List.map (fun a -> trial ctx (fun () -> check ctx a)) [ x; y ]
+         with
+         | [ Ok a; Ok b ]
+           when (a.Tast.ty = Types.Char && Types.is_integer b.Tast.ty)
+                || (b.Tast.ty = Types.Char && Types.is_integer a.Tast.ty) ->
+           let fln = fln_source loc in
+           Loc.failk "check/char-compare" loc
+             "%s compares a char only with a char, and this is %s beside it. \
+              Take its code point with %s, or make a char with %s" name
+             (tyname loc (if a.Tast.ty = Types.Char then b.Tast.ty else a.Tast.ty))
+             (if fln then "i32(c)" else "(i32 c)")
+             (if fln then "char(n)" else "(char n)")
+         | _ -> raise ex)
+    in
     (* Which pairs this operator asks about. Every one but [!=] chains, and
        [!=] asks about all of them — see [all_pairs]. At two operands the two
        readings are one pair and the same answer, which is why the two-operand
@@ -15881,9 +15989,10 @@ and trial_at ctx (y : Ast.expr) (w : Types.t) =
        if !lit_recording = 0 then Hashtbl.add arm_failed y.Ast.loc (y, (ctx.scope, ctx.ret), w, d);
        Error d)
 
-and binary ctx ?(dyn_ok = false) ?(join = true) name loc ~want args =
+and binary ctx ?(dyn_ok = false) ?(join = true) ?(char_ok = false) name loc ~want args =
   match args with
-  | [ x; y ] -> lit_operands ctx x y (fun () -> binary_pair ctx ~dyn_ok ~join loc ~want x y)
+  | [ x; y ] ->
+    lit_operands ctx x y (fun () -> binary_pair ctx ~dyn_ok ~join ~char_ok loc ~want x y)
   | _ -> fail loc "%s takes two arguments" name
 
 (* An operator's two operands, while literal locals' uses are recorded: one
@@ -15897,11 +16006,19 @@ and lit_operands ctx (x : Ast.expr) (y : Ast.expr) f =
   match ctx.lits, key x, key y with
   | Some s, kx, ky when kx <> None || ky <> None ->
     let float_lit (e : Ast.expr) = lit_kind e = Some `Float in
+    (* A char local beside an integer literal stays a char: the pair is char
+       arithmetic, or a comparison the checker refuses (decision 131). Only
+       typed code that wants a particular integer makes it a number. *)
+    let lit_add s k ((_, _, _) as c) (other : Ast.expr) =
+      match lit_kind k, lit_kind other with
+      | Some `Char, Some `Int -> ()
+      | _ -> lit_add s k c
+    in
     (* Before the check, which refuses a float literal beside an integer
        guess. *)
     (match kx, ky with
-     | Some k, _ when float_lit y -> lit_add s k (Hint, Types.Float (float_default ()), y.Ast.loc)
+     | Some k, _ when float_lit y -> lit_add s k (Hint, Types.Float (float_default ()), y.Ast.loc) y
-     | _, Some k when float_lit x -> lit_add s k (Hint, Types.Float (float_default ()), x.Ast.loc)
+     | _, Some k when float_lit x -> lit_add s k (Hint, Types.Float (float_default ()), x.Ast.loc) x
      | _ -> ());
     let saved = !lit_operand_locs in
     lit_operand_locs := x.Ast.loc :: y.Ast.loc :: saved;
@@ -15912,7 +16029,7 @@ and lit_operands ctx (x : Ast.expr) (y : Ast.expr) f =
            i64 x: what the other operand is on its own terms is the use. *)
         let own (k, (other : Ast.expr)) =
           match trial ctx (fun () -> check ctx other) with
-          | Ok e -> lit_add s k (Hint, e.Tast.ty, other.Ast.loc)
+          | Ok e -> lit_add s k (Hint, e.Tast.ty, other.Ast.loc) other
           | Error _ -> ()
         in
         (match kx, ky with
@@ -15923,13 +16040,13 @@ and lit_operands ctx (x : Ast.expr) (y : Ast.expr) f =
     in
     (match kx, ky with
      | Some k1, Some k2 -> lit_union s k1 k2
-     | Some k, None -> lit_add s k (Hint, b.Tast.ty, y.Ast.loc)
+     | Some k, None -> lit_add s k (Hint, b.Tast.ty, y.Ast.loc) y
-     | None, Some k -> lit_add s k (Hint, a.Tast.ty, x.Ast.loc)
+     | None, Some k -> lit_add s k (Hint, a.Tast.ty, x.Ast.loc) x
      | None, None -> ());
     a, b
   | _ -> f ()
 
-and binary_pair ctx ~dyn_ok ~join loc ~want (x : Ast.expr) (y : Ast.expr) =
+and binary_pair ctx ~dyn_ok ~join ~char_ok loc ~want (x : Ast.expr) (y : Ast.expr) =
     (* A char defconst no local shadows reads as the literal it names. *)
     let is_literal (e : Ast.expr) =
       is_literal e
@@ -15955,7 +16072,14 @@ and binary_pair ctx ~dyn_ok ~join loc ~want (x : Ast.expr) (y : Ast.expr) =
     in
     if y_decides then begin
       let b = check ctx ?want y in
-      let a = check ctx ~want:b.Tast.ty x in
+      (* An integer literal before a char, under [+] or [-], is an integer:
+         the pair is char arithmetic ([char_step]). *)
+      let a =
+        match x.Ast.e with
+        | (Ast.Int _ | Ast.UInt _) when char_ok && b.Tast.ty = Types.Char ->
+          check ctx x
+        | _ -> check ctx ~want:b.Tast.ty x
+      in
       a, b
     end
     (* [dyn_ok] is set by the operators that have a dyn lowering, and it exists

runtime/flan_dyn.c

@@ -3078,9 +3078,43 @@ static void want_nums(const uint8_t *loc, int64_t loclen, const char *op,
 
 #define ARITH_NUM "it takes two numbers"
 
+/* Char arithmetic, the typed side's rule (decision 131): a char plus or
+ * minus an int, or an int plus a char, is a char, trapping where the result
+ * is not a scalar value; a char minus a char is the int distance. 0 when the
+ * pair is none of those, for [arith] to refuse as it refuses any non-number. */
+static int char_arith(const uint8_t *loc, int64_t loclen, const char *op,
+                      flan_dyn a, flan_dyn b, flan_dyn *out) {
+  int ca = flan_dyn_tag(a) == FLAN_DYN_TAG_CHAR;
+  int cb = flan_dyn_tag(b) == FLAN_DYN_TAG_CHAR;
+  int64_t n;
+  if (op[0] == '-' && ca && cb) {
+    *out = flan_dyn_from_i64((int64_t)dyn_payload(a) - (int64_t)dyn_payload(b));
+    return 1;
+  }
+  if (ca && flan_dyn_tag(b) == FLAN_DYN_TAG_INT)
+    n = (int64_t)((uint64_t)dyn_payload(a) +
+                  (op[0] == '-' ? -(uint64_t)dyn_int_value(b)
+                                : (uint64_t)dyn_int_value(b)));
+  else if (op[0] == '+' && cb && flan_dyn_tag(a) == FLAN_DYN_TAG_INT)
+    n = (int64_t)((uint64_t)dyn_int_value(a) + (uint64_t)dyn_payload(b));
+  else
+    return 0;
+  if (!is_scalar(n)) {
+    flan_say(loc, loclen,
+             "dyn %s: %lld is not a Unicode scalar value, so it is not a char",
+             op, (long long)n);
+    dyn_trap((const uint8_t *)"InvalidChar", 11);
+  }
+  *out = flan_dyn_from_char((int32_t)n);
+  return 1;
+}
+
 static flan_dyn arith(const uint8_t *loc, int64_t loclen, const char *op,
                       flan_dyn a, flan_dyn b) {
   int64_t x, y;
+  flan_dyn c;
+  if ((op[0] == '+' || op[0] == '-') && char_arith(loc, loclen, op, a, b, &c))
+    return c;
   want_nums(loc, loclen, op, ARITH_NUM, a, b);
   if (flan_dyn_tag(a) == FLAN_DYN_TAG_INT &&
       flan_dyn_tag(b) == FLAN_DYN_TAG_INT) {

test/programs/char-arith.flan

@@ -0,0 +1,43 @@
+;;;; Char arithmetic (decision 131, Kotlin's rules): a char plus or minus an
+;;;; integer is a char, an integer plus a char is too, and a char minus a char
+;;;; is the distance, an i32. Dyn chars do the same. Byte code beside it is
+;;;; unchanged. With "past" a char past U+10FFFF traps, with "surrogate" one
+;;;; landing on a surrogate does, and with "dyn" a dyn char below zero does.
+
+(defn show [x] () (println x))
+(defn add [a b] dyn (+ a b))
+(defn sub [a b] dyn (- a b))
+(defn upper [c char] char (if (and (>= c \a) (<= c \z)) (- c 32) c))
+
+(defn main [args [str]] i32
+  ;; The fork case with arithmetic: a let-bound char stays a char.
+  (let [c \a]
+    (show c)
+    (show (+ c 1)))
+  ;; Each rule, typed.
+  (let [c (char 100)
+        n 3]
+    (println (+ c n) (+ n c) (- c n) (- c \a) (- \a \A) (+ \a 1 1)))
+  (println (upper \q) (upper \Q) (upper \é))
+  ;; += and -= on a char local.
+  (let [c \a]
+    (set c (+ c 2))
+    (set c (- c 1))
+    (println c))
+  ;; Dyn chars follow the same rules.
+  (println (add \a 1) (add 1 \a) (sub \z 1) (sub \a \A) (add (char 120) (the dyn 2)))
+  ;; Byte code: a char difference where a byte is wanted is a byte.
+  (let [b (u8 65)
+        v (vec-new u8)]
+    (push v (+ b (- \a \A)))
+    (println (at v 0) (= (at v 0) \a)))
+  (when (> (length args) 1)
+    (let [k (length args)]
+      (cond
+        (= (at args 1) "past")
+        (println (+ (char 0x10FFFF) (- k 1)))
+        (= (at args 1) "surrogate")
+        (println (+ (char 0xD7FF) (- k 1)))
+        :else
+        (println (sub \a (* k 100))))))
+  0)

test/test_acceptance.ml

@@ -5559,6 +5559,37 @@ level "1"
              ("u64", "programs/char.flan:54:18: 9223372036854775809 is not a \
                       Unicode scalar value, so it is not a char") ])
       [ false; true ];
+    (* Char arithmetic, decision 131: every rule typed and dyn, the fork case
+       with arithmetic, and a byte beside it; then a char past U+10FFFF, one
+       on a surrogate, and a dyn one below zero, each trapping at its form. *)
+    let char_arith_out =
+      "a\nb\ng g a 3 32 c\nQ Q é\nb\nb b y 32 z\n97 true\n"
+    in
+    outputs "char: arithmetic" "programs/char-arith.flan" char_arith_out;
+    outputs ~opt:"-O0" "char: arithmetic, -O0" "programs/char-arith.flan"
+      char_arith_out;
+    outputs ~x86:true "char: arithmetic, --x86" "programs/char-arith.flan"
+      char_arith_out;
+    List.iter
+      (fun x86 ->
+         let exe = compile ~x86 "programs/char-arith.flan" in
+         List.iter
+           (fun (arg, want) ->
+              let code, text = run exe (Some arg) in
+              if code <> 134 || not (contains text want) then begin
+                incr failures;
+                Printf.printf
+                  "FAIL  char arithmetic: %s traps%s\n        got: %S (exit \
+                   %d)\n     wanted: %S (exit 134)\n"
+                  arg (if x86 then ", --x86" else "") text code want
+              end)
+           [ ("past", "programs/char-arith.flan:38:18: 1114112 is not a \
+                       Unicode scalar value, so it is not a char");
+             ("surrogate", "programs/char-arith.flan:40:18: 55296 is not a \
+                            Unicode scalar value, so it is not a char");
+             ("dyn", "programs/char-arith.flan:9:21: dyn -: -103 is not a \
+                      Unicode scalar value, so it is not a char") ])
+      [ false; true ];
     (* A String, and a str made from one, cross into dyn as text measured
        like any other: characters counted, ASCII or not. *)
     let string_char_out =

test/test_flan.ml

@@ -3199,8 +3199,7 @@ let () =
   accepts "an ASCII char is a u8"
     "(defn main [] i32 (let [b (the u8 97)] (if (= b \\a) 0 1)))";
   (* Decision 127: a char literal is a char unless typed code wants a
-     number, and a char is a character: it compares, orders and hashes, and
+     number, and a char is a character: it compares, orders and hashes. *)
-     only a conversion computes with it. *)
   accepts "a let-bound char literal beside a u8 is the u8"
     "(defn main [] i32 (let [b (the u8 97) c \\a] (if (= b c) 0 1)))";
   accepts "a char literal pushed into bytes is a byte"
@@ -3214,21 +3213,45 @@ let () =
     "(defn main [] i32 (let [m (map-new char i32)] (put m \\a 1) 0))";
   accepts "a char converts to an integer and back"
     "(defn f [c char] char (char (+ (i32 c) 1)))";
-  rejects_check "a char does no arithmetic"
+  (* Decision 131, Kotlin's rules: a char plus or minus an integer is a char,
+     a char minus a char is an i32, and nothing else computes with one. *)
+  accepts "a char plus an integer is a char"
+    "(defn f [c char n i32] char (+ c n))";
+  accepts "an integer plus a char is a char"
+    "(defn f [c char] char (+ 1 c))";
+  accepts "a char minus an integer is a char"
+    "(defn f [c char] char (- c 1))";
+  accepts "a char minus a char is an i32"
+    "(defn f [c char] i32 (- c \\a))";
+  accepts "a let-bound char plus a literal stays a char"
+    "(defn f [] char (let [c \\a] (+ c 1)))";
+  accepts "a char difference is a byte where a byte is wanted"
+    "(defn f [b u8] u8 (+ b (- \\a \\A)))";
+  rejects_check "a char does not add to a char"
     "(defn f [c char] char (+ c c))"
-    ~needle:"+ does no arithmetic on a char: a char is a character, not a \
+    ~needle:"+ adds an integer to a char, and not a char to a char. Take its \
-             number. Take its code point with (i32 c)";
+             code point with (i32 c)";
-  rejects_check "nor beside a number"
+  rejects_check "nor multiply"
     "(defn f [c char] i32 (let [n 3] (* n c)))"
     ~needle:"* does no arithmetic on a char";
-  rejects_check "nor with an integer literal"
+  rejects_check "nor come off an integer"
-    "(defn f [c char] char (- c 1))"
+    "(defn f [c char] i32 (- 1 c))"
-    ~needle:"- does no arithmetic on a char";
+    ~needle:"- takes an integer or a char from a char, and not a char from an \
+             integer";
+  rejects_check "nor take a remainder"
+    "(defn f [c char] char (% c 2))" ~needle:"% does no arithmetic on a char";
   rejects_check "an integer literal is not a char"
     "(defn f [c char] bool (= c 97))"
-    ~needle:"the integer literal 97 is not a char";
+    ~needle:"the integer literal 97 is not a char, and a char compares only \
+             with a char. Take its code point with (i32 c)";
+  rejects_check "nor is an integer"
+    "(defn f [c char n i32] bool (< c n))"
+    ~needle:"< compares a char only with a char, and this is i32 beside it";
+  rejects_check "a constant char past the last code point"
+    "(defn f [] char (- \\a 200))"
+    ~needle:"this is -103, which is not a Unicode scalar value";
   rejects_check "nor negated"
-    "(defn f [c char] char (- c))" ~needle:"- does no arithmetic on a char";
+    "(defn f [c char] char (- c))" ~needle:"- takes an integer or a char";
   rejects_check "nor bitwise"
     "(defn f [c char] char (bit-and c c))"
     ~needle:"bit-and does no arithmetic on a char";