From 111ee66a4b1c5891818d01b6c2c49b03d29b99dd Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Fri, 25 Sep 2026 20:47:53 +0700 Subject: [PATCH 1/2] A match arm can be a number, char or string literal compared with =, over a number, a string or a dyn, with a _ arm required --- TODO.org | 7 +- lib/ast.ml | 4 + lib/check.ml | 156 +++++++++++++++++++++++++++++-- lib/load.ml | 2 +- lib/parse.ml | 1 + spec-syntax.md | 10 +- test/programs/match-literal.flan | 71 ++++++++++++++ test/test_acceptance.ml | 13 +++ test/test_flan.ml | 66 ++++++++++++- test/test_syntax.ml | 2 + web/index.html | 7 +- 11 files changed, 320 insertions(+), 19 deletions(-) create mode 100644 test/programs/match-literal.flan diff --git a/TODO.org b/TODO.org index 262eec92..68db3b8d 100644 --- a/TODO.org +++ b/TODO.org @@ -296,9 +296,10 @@ keyword resolves against the expected type and against nothing else, so two enum could always share a member spelling. What the prefix buys is the call site read on its own. -** NEXT match over numbers and strings -Decided 2026-09-25: a match arm's pattern can be an integer, a float, a char or a -string literal, compared as =(= t lit)=; a match over such a type needs a =_= arm. +** DONE match over numbers and strings +CLOSED: [2026-09-25] +Rules out a literal the scrutinee's type cannot hold (refused, not widened as =(=)= +would), keyword arms over a dyn, and a bare-name catch-all: a bare name is a nullary case. ** DONE match over enums CLOSED: [2026-09-25] diff --git a/lib/ast.ml b/lib/ast.ml index 824d743d..7ab6b16e 100644 --- a/lib/ast.ml +++ b/lib/ast.ml @@ -222,6 +222,10 @@ and arm = { pat : pattern; body : expr list; aloc : Loc.t } and pattern = | Pctor of string * string list (* (Some e) (Rect w h) None *) | Pkw of string (* :north — an enum member *) + (* 5 -2.5 \a "go" — an Int, UInt, Float, Byte or Str expr, compared as + (= t lit). An expr and not a literal type of its own, so the checker + types it against the scrutinee as any literal is typed against its site. *) + | Plit of expr | Pwild (* _ :else *) (* ── Declarations ──────────────────────────────────────────────────── *) diff --git a/lib/check.ml b/lib/check.ml index 3aa48fab..bd8ab9e8 100644 --- a/lib/check.ml +++ b/lib/check.ml @@ -3801,6 +3801,11 @@ let box_option ctx loc (t : Types.t) (got : Tast.expr) : Tast.expr = (Tast.Let ([ (s, got) ], [ mk loc Types.Dyn (Tast.If (is_some, some_dyn, none_dyn)) ])) +(* [=] over a dyn pair, answering a bool. Shared by the [=] builtin and a + literal [match] over a dyn, which is (= t lit) by definition. *) +let dyn_eq loc u v = + unbox loc Types.Bool (rt loc Types.Dyn "flan_dyn_eq" [ box loc u; box loc v ]) + let unbox_option ctx loc (t : Types.t) (got : Tast.expr) : Tast.expr = let oty = Types.Option t in match t with @@ -8089,10 +8094,44 @@ and check_match ctx ?(tail = false) ?want loc scrutinee arms = "%s is a union, and nothing in one records which member was written, \ so there is nothing to match on. Read the member you mean with \ (.member u), or use a defdata" n + (* A number, a string or a dyn: the arms are literals, and each is the + test (= t lit) over one temporary — the enum's chain, with [=]'s own + two lowerings for the test, so a match over a dyn means what [=] over + it means. [is_equatable]'s set minus the enums, which are above. *) + | (Types.Int _ | Types.Float _ | Types.String | Types.Dyn) as t -> `Lit t | other -> - fail loc "match works on an Option, a data type or an enum, not on %s" + fail loc + "match works on an Option, a data type, an enum, a number, a string \ + or a dyn, not on %s" (Types.to_string other) in + (* A literal arm, spelled as it was written, for the refusals that name one. *) + let spell (e : Ast.expr) = + match e.Ast.e with + | Ast.Int n -> Int64.to_string n + | Ast.UInt (_, t) -> t + | Ast.Float x when Float.is_integer x -> Printf.sprintf "%.1f" x + | Ast.Float x -> Printf.sprintf "%g" x + | Ast.Byte b when b > 32 && b < 127 -> Printf.sprintf "\\%c" (Char.chr b) + | Ast.Byte b -> string_of_int b + | Ast.Str t -> Printf.sprintf "%S" t + | _ -> "this literal" + in + let what_ty t = match t with Types.Dyn -> "a dyn" | t -> Types.to_string t in + (* A literal match that compiles, over the scrutinee's own name where it + has one, for the refusals that need to show the shape. *) + let lit_arms_fix t = + let name = + match scrutinee.Ast.e with Ast.Var n -> n | _ -> "t" + in + Printf.sprintf "(match %s %s)" name + (match t with + | Types.String -> "\"yes\" 1 _ 0" + | Types.Float _ -> "0.5 1 _ 0" + | _ -> "5 1 _ 0") + in + (* The checked literal of each literal arm, by the key [resolve_pat] gave it. *) + let lits : (string, Tast.expr) Hashtbl.t = Hashtbl.create 8 in (* Which case each arm names, and the type of each name it binds. This is the whole of what differs between the two subjects; everything below it is shared. *) @@ -8124,6 +8163,81 @@ and check_match ctx ?(tail = false) ?want loc scrutinee arms = "this match is over the enum %s, and %s is not one of its members. An \ arm names a member as a keyword: %s" n c (String.concat " " (List.map (fun (m, _) -> ":" ^ m) members)) + | `Lit t, Ast.Plit e -> + let v = + match t with + (* [=]'s dyn pair checks its literal at dyn, which boxes it. *) + | Types.Dyn -> check ctx ~want:Types.Dyn e + | t -> + (match trial ctx (fun () -> check ctx ~want:t e) with + | Ok v -> v + | Error _ -> + (* A literal that does not fit is refused, where [=] would widen + the pair and let the arm quietly never match. The literal's + own refusal is not repeated: its fixes are casts, and a cast + is not a pattern. *) + let tn = Types.to_string t in + let an = + match tn.[0] with + | 'a' | 'e' | 'f' | 'i' | 'o' -> "an " ^ tn + | _ -> "a " ^ tn + in + let why = + match e.Ast.e, t with + | Ast.Str _, _ -> "is a string" + | _, Types.String -> "is a number" + | Ast.Float x, Types.Int _ when not (Float.is_integer x) -> + "is not a whole number" + | Ast.Float _, Types.Int _ -> "is a float" + | _ -> "does not fit in one" + in + fail a.Ast.aloc + "this match is over %s, so each arm has to be %s, and %s %s. \ + Change the arm to a value %s holds, or remove it" + tn an (spell e) why an) + in + (* One key per value [=] cannot tell apart, so a second arm that could + never be reached is refused: 97 and \\a are one u8, and over a dyn + 1 and 1.0 are equal, as they are over a float. *) + let key = + let num x = + if Float.is_integer x && Float.abs x < 0x1p62 then + Printf.sprintf "i%Ld" (Int64.of_float x) + else Printf.sprintf "f%h" x + in + match e.Ast.e with + | Ast.Int n -> Printf.sprintf "i%Ld" n + | Ast.Byte b -> Printf.sprintf "i%d" b + | Ast.UInt (n, _) -> Printf.sprintf "u%Lu" n + | Ast.Float x -> num x + | Ast.Str t -> "s" ^ t + | _ -> assert false + in + Hashtbl.replace lits key v; + Some key, [] + | `Lit t, Ast.Pkw k -> + fail a.Ast.aloc + ":%s is an enum member, and this match is over %s, whose arms are \ + literals, as in %s" k (what_ty t) (lit_arms_fix t) + | `Lit t, Ast.Pctor (c, _) -> + fail a.Ast.aloc + "%s names a case, and this match is over %s, whose arms are \ + literals, as in %s" c (what_ty t) (lit_arms_fix t) + | `Option _, Ast.Plit e -> + fail a.Ast.aloc + "%s is a literal, and this match is over an Option, whose arms are \ + (Some x) and None" (spell e) + | `Enum (n, members), Ast.Plit e -> + fail a.Ast.aloc + "%s is a literal, and this match is over the enum %s, whose arms \ + name its members as keywords: %s" (spell e) n + (String.concat " " (List.map (fun (m, _) -> ":" ^ m) members)) + | `Data u, Ast.Plit e -> + fail a.Ast.aloc + "%s is a literal, and this match is over the data type %s, whose \ + arms name its cases: %s" (spell e) u.Tast.dname + (String.concat ", " + (List.map (fun (v : Tast.variant) -> v.Tast.vname) u.Tast.cases)) | `Option _, Ast.Pkw k -> fail a.Ast.aloc ":%s is an enum member, and this match is over an Option, whose arms \ @@ -8184,7 +8298,10 @@ and check_match ctx ?(tail = false) ?want loc scrutinee arms = | Some c -> if Hashtbl.mem seen c then fail a.Ast.aloc "this match has two %s arms" - (match subject with `Enum _ -> ":" ^ c | _ -> c); + (match subject, a.Ast.pat with + | `Enum _, _ -> ":" ^ c + | _, Ast.Plit e -> spell e + | _ -> c); Hashtbl.add seen c ()); (a, ctor, binds)) arms @@ -8286,7 +8403,19 @@ and check_match ctx ?(tail = false) ?want loc scrutinee arms = List.filter_map (fun (m, _) -> if Hashtbl.mem seen m then None else Some (":" ^ m)) members + | `Lit _ -> [] in + (* No list of literals covers a number, a string or a dyn, so a literal + match always needs its [_]. Refused here, before the chain below, which + would otherwise run a lone last arm untested as the enum's does. *) + (match subject with + | `Lit t when not !saw_wild -> + Loc.failk "check/non-exhaustive-match" loc + "this match is not exhaustive — its arms are literals, and no list of \ + them covers every %s. Add a _ arm for the rest, as in %s" + (match t with Types.Dyn -> "dyn value" | t -> Types.to_string t) + (lit_arms_fix t) + | _ -> ()); if not !saw_wild && missing <> [] then (* The data type's declaration, because that is where the case list this match failed to cover actually lives, and because adding a case there is what @@ -8295,7 +8424,7 @@ and check_match ctx ?(tail = false) ?want loc scrutinee arms = ~notes:(match subject with | `Data u -> declared_note ctx.env u.Tast.dname | `Enum (n, _) -> declared_note ctx.env n - | `Option _ -> []) + | `Option _ | `Lit _ -> []) "this match is not exhaustive — %s %s no arm. Add %s, or a _ arm for \ the rest" (String.concat ", " missing) @@ -8304,7 +8433,7 @@ and check_match ctx ?(tail = false) ?want loc scrutinee arms = let ty = match !want with Some t -> t | None -> Types.Never in match subject with | `Option _ | `Data _ -> mk loc ty (Tast.Match (s, arms)) - | `Enum (_, members) -> + | `Enum _ | `Lit _ -> (* The scrutinee once, into a temporary, and then an [if] per arm in the order written. A [_] arm ends the chain, and so does the last arm of a match with none: it is exhaustive by the check above, so the last @@ -8320,10 +8449,18 @@ and check_match ctx ?(tail = false) ?want loc scrutinee arms = | ({ Tast.acase = None; _ } as a) :: _ -> body a | [ a ] -> body a | ({ Tast.acase = Some m; _ } as a) :: rest -> - let v = mk loc s.Tast.ty (Tast.Int (List.assoc m members, Types.I32)) in - mk loc ty - (Tast.If (mk loc Types.Bool (Tast.Prim (Tast.Eq, [ local; v ])), - body a, chain rest)) + let test = + match subject with + | `Enum (_, members) -> + let v = + mk loc s.Tast.ty (Tast.Int (List.assoc m members, Types.I32)) + in + mk loc Types.Bool (Tast.Prim (Tast.Eq, [ local; v ])) + | `Lit Types.Dyn -> dyn_eq loc local (Hashtbl.find lits m) + | _ -> + mk loc Types.Bool (Tast.Prim (Tast.Eq, [ local; Hashtbl.find lits m ])) + in + mk loc ty (Tast.If (test, body a, chain rest)) in mk loc ty (Tast.Let ([ (slot, s) ], [ chain arms ])) @@ -9698,7 +9835,8 @@ and named_call ?(qualified = false) ctx ~want loc name args = and the negation is an [i1] flip the backend folds away. *) let link u v = let cmp = - unbox loc Types.Bool (rt loc Types.Dyn sym ([ u; v ] @ site)) + if String.equal sym "flan_dyn_eq" then dyn_eq loc u v + else unbox loc Types.Bool (rt loc Types.Dyn sym ([ u; v ] @ site)) in if String.equal name "!=" then mk loc Types.Bool (Tast.Prim (Tast.Not, [ cmp ])) diff --git a/lib/load.ml b/lib/load.ml index 9b5688b5..930fdda8 100644 --- a/lib/load.ml +++ b/lib/load.ml @@ -274,7 +274,7 @@ let rec rename_expr owned alias bound (e : Ast.expr) : Ast.expr = let bound = match a.Ast.pat with | Ast.Pctor (_, ns) -> ns @ bound - | Ast.Pkw _ | Ast.Pwild -> bound + | Ast.Pkw _ | Ast.Plit _ | Ast.Pwild -> bound in { a with Ast.body = List.map (rename_expr owned alias bound) a.Ast.body }) arms) diff --git a/lib/parse.ml b/lib/parse.ml index a9aa6e0c..b325e03a 100644 --- a/lib/parse.ml +++ b/lib/parse.ml @@ -1402,6 +1402,7 @@ and pattern (f : Form.t) : Ast.pattern = (* An enum member. Which enum is the scrutinee's type, so [Check] resolves it, as it resolves a keyword anywhere an enum is expected. *) | Kw member -> Ast.Pkw member + | Int _ | UInt _ | Float _ | Byte _ | Str _ -> Ast.Plit (expr f) | List ({ v = Sym ctor; _ } :: binds) -> List.iter no_pattern binds; Ast.Pctor (ctor, List.map dname binds) diff --git a/spec-syntax.md b/spec-syntax.md index c43bebb5..2d075b65 100644 --- a/spec-syntax.md +++ b/spec-syntax.md @@ -202,9 +202,17 @@ Each item: the proposal, then the reason in one line. Rect(w, h) -> w * h :north -> 0 _ -> 0 + + match code + 404 -> "missing" + -1 -> "none" + "ok" -> "fine" + \a -> "a" + _ -> "other" ``` An arm's body can be an indented block, which reads as `(do …)`. **Built** (a - one-line block reads as that line). + one-line block reads as that line). A number, char or string pattern is the + literal as written, compared as `(= t lit)`. - **Conditions**, clauses at the header's column: ``` diff --git a/test/programs/match-literal.flan b/test/programs/match-literal.flan new file mode 100644 index 00000000..9253b7aa --- /dev/null +++ b/test/programs/match-literal.flan @@ -0,0 +1,71 @@ +;;;; match over numbers, chars, strings and dyn values: each arm is (= t lit) +;;;; over one temporary, and a _ arm is the rest. + +(defn small [n i16] string + (match n + 5 "five" + -3 "minus three" + _ "other")) + +(defn half [x f32] i32 + (match x + 0.5 1 + 2 2 + _ 0)) + +(defn letter [c u8] i32 + (match c + \a 1 + 98 2 + _ 0)) + +(defn command [s string] i32 + (match s + "go" 1 + "stop" 2 + "" 3 + _ 0)) + +(defn big [n u64] i32 + (match n + 18446744073709551615 1 + _ 0)) + +;; Over a dyn the test is dyn =, so 1 matches 1.0 and "go" matches only a +;; string. +(defn kind [d dyn] string + (match d + 1 "one" + 2.5 "two and a half" + "go" "go" + _ "other")) + +(defn calls [] i32 + (print "(called) ") + 7) + +;; recur from inside an arm: the arm is the loop's tail. +(defn count-down [from i32] i32 + (loop [n from steps 0] + (match n + 0 steps + _ (recur (- n 1) (+ steps 1))))) + +(defn main [] i32 + (println (small 5)) + (println (small -3)) + (println (small 4)) + (print (half 0.5)) (print (half 2.0)) (print (half 3.0)) (println "") + (print (letter 97)) (print (letter 98)) (print (letter 99)) (println "") + (print (command "go")) (print (command "stop")) (print (command "")) + (print (command "gone")) (println "") + (print (big 18446744073709551615)) (print (big 1)) (println "") + (println (kind 1)) + (println (kind 1.0)) + (println (kind 2.5)) + (println (kind "go")) + (println (kind "1")) + ;; The scrutinee is evaluated once, however many arms test it. + (println (match (calls) 1 "a" 2 "b" 7 "seven" _ "c")) + (print (count-down 4)) (println "") + 0) diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml index 29f9a0b3..1c703e47 100644 --- a/test/test_acceptance.ml +++ b/test/test_acceptance.ml @@ -432,6 +432,19 @@ let () = match_enum_out; outputs ~dev:true "match over an enum, dev" "programs/match-enum.flan" match_enum_out; + (* A literal match is the same chain with (= t lit) as each test, so the + dyn rows (1 and 1.0 both "one") are dyn ='s answer. *) + let match_lit_out = + "five\nminus three\nother\n120\n120\n1230\n10\none\none\n\ + two and a half\ngo\nother\n(called) seven\n4\n" + in + outputs "match over literals" "programs/match-literal.flan" match_lit_out; + outputs ~opt:"-O0" "match over literals, -O0" "programs/match-literal.flan" + match_lit_out; + outputs ~x86:true "match over literals, --x86" "programs/match-literal.flan" + match_lit_out; + outputs ~dev:true "match over literals, dev" "programs/match-literal.flan" + match_lit_out; (* update, ++ and -- evaluate their place's subexpressions once: the counts are the number of calls an index or a key function got. *) let update_out = "3\n11 20 90\n1 1 3\n16\n2\n7 1\n32\n2 50\n" in diff --git a/test/test_flan.ml b/test/test_flan.ml index 1e151779..69dadbed 100644 --- a/test/test_flan.ml +++ b/test/test_flan.ml @@ -2690,7 +2690,7 @@ let () = accepts "a wildcard arm is exhaustive" "(defn g [] (Option i32) None) (defn f [] i32 (match (g) (Some v) v _ 0))"; rejects_check "match on a non-Option" - "(defn f [x i32] i32 (match x _ 0))" ~needle:"match works on an Option"; + "(defn f [x bool] i32 (match x _ 0))" ~needle:"match works on an Option"; (* ── Names, order-independence, entry point ────────────────────── *) accepts "mutually recursive, no forward declaration" @@ -4582,8 +4582,68 @@ let () = (k ^ "(defn f [k K] i32 (match k :lo 1 _ \"x\"))") ~needle:"expected i32, found string"; rejects_check "match over something that is none of them" - "(defn f [n i32] i32 (match n _ 2))" - ~needle:"match works on an Option, a data type or an enum, not on i32"; + "(defn f [n bool] i32 (match n _ 2))" + ~needle:"match works on an Option, a data type, an enum, a number, a \ + string or a dyn, not on bool"; + + (* ── match over literals ───────────────────────────────────────── *) + + (* Each arm is (= t lit) with the literal built at the scrutinee's type, so + a literal that type cannot hold is refused rather than widened into an + arm that never matches. *) + accepts "match over an i16, a literal arm built at i16" + "(defn f [n i16] i32 (match n 5 1 -3 2 _ 0))"; + accepts "match over a string" "(defn f [s string] i32 (match s \"go\" 1 _ 0))"; + accepts "match over a dyn, arms of several kinds" + "(defn f [d dyn] i32 (match d 1 1 2.5 2 \"go\" 3 \\a 4 _ 0))"; + accepts "match over a number, :else for the rest" + "(defn f [n i32] i32 (match n 5 1 :else 0))"; + rejects_check "a literal arm the scrutinee cannot hold" + "(defn f [n i8] i32 (match n 300 1 _ 0))" + ~needle:"this match is over i8, so each arm has to be an i8, and 300 does \ + not fit in one. Change the arm to a value an i8 holds, or remove it"; + rejects_check "a float arm over an integer" + "(defn f [n i32] i32 (match n 1.5 1 _ 0))" + ~needle:"and 1.5 is not a whole number"; + rejects_check "a string arm over a number" + "(defn f [n i32] i32 (match n \"a\" 1 _ 0))" + ~needle:"and \"a\" is a string"; + rejects_check "a number arm over a string" + "(defn f [s string] i32 (match s 5 1 _ 0))" + ~needle:"so each arm has to be a string, and 5 is a number"; + rejects_check "a literal match with no _ arm" + "(defn f [n i32] i32 (match n 5 1 6 2))" + ~needle:"this match is not exhaustive — its arms are literals, and no list \ + of them covers every i32. Add a _ arm for the rest, as in (match \ + n 5 1 _ 0)"; + rejects_check "a literal match over a dyn with no _ arm" + "(defn f [d dyn] i32 (match d 5 1))" + ~needle:"covers every dyn value"; + rejects_check "a literal named twice" + "(defn f [n i32] i32 (match n 5 1 5 2 _ 0))" + ~needle:"this match has two 5 arms"; + rejects_check "a char and a number that are one u8" + "(defn f [c u8] i32 (match c \\a 1 97 2 _ 0))" + ~needle:"this match has two 97 arms"; + rejects_check "1 and 1.0 are one arm over a dyn, as dyn = says" + "(defn f [d dyn] i32 (match d 1 1 1.0 2 _ 0))" + ~needle:"this match has two 1.0 arms"; + rejects_check "a keyword arm among literal arms" + "(defn f [n i32] i32 (match n 5 1 :lo 2 _ 0))" + ~needle:":lo is an enum member, and this match is over i32, whose arms are \ + literals, as in (match n 5 1 _ 0)"; + rejects_check "a case arm among literal arms" + "(defn f [n i32] i32 (match n 5 1 (Some x) 2 _ 0))" + ~needle:"Some names a case, and this match is over i32"; + rejects_check "a literal arm among keyword arms" + (k ^ "(defn f [k K] i32 (match k :lo 1 5 2 _ 0))") + ~needle:"5 is a literal, and this match is over the enum K"; + rejects_check "a literal arm over an Option" + "(defn f [o (Option i32)] i32 (match o 5 1 _ 0))" + ~needle:"5 is a literal, and this match is over an Option"; + rejects_check "a literal match over a byte slice, which = does not compare" + "(defn f [b [u8]] i32 (match b \"a\" 1 _ 0))" + ~needle:"not on [u8]"; (* A destructuring pattern in an arm's binds is a name position like any other. *) rejects_check "a pattern inside a match arm's binds" diff --git a/test/test_syntax.ml b/test/test_syntax.ml index ab4fb6a3..e1a17e11 100644 --- a/test/test_syntax.ml +++ b/test/test_syntax.ml @@ -362,6 +362,8 @@ let () = "(restart-case (f) (continue [] (do)))"; reads "match" "match s\n Circle(r) -> r\n _ ->\n a()\n b()" "(match s (Circle r) r _ (do (a) (b)))"; + reads "match over literals" "match n\n 5 -> a\n -2.5 -> b\n \"go\" -> c\n \\a -> d\n _ -> e" + "(match n 5 a -2.5 b \"go\" c \\a d _ e)"; reads "handler-bind moves the clauses" "handler-bind\n f()\non E(c)\n g(c)" "(handler-bind [(E [c] (g c))] (f))"; reads "quote block" diff --git a/web/index.html b/web/index.html index ea18a0de..a8a8a6e8 100644 --- a/web/index.html +++ b/web/index.html @@ -1096,8 +1096,11 @@ as first-even does above.

Option, match and some

(Option T) is how absence is spelled: a lookup miss, an empty -collection, the end of a stream. match works on an Option and -on a defdata, and on nothing else. some unwraps +collection, the end of a stream. match works on an Option, a +defdata and an enum, whose arms name cases; and on a number, a string or a +dyn, whose arms are literals — (match n 0 "zero" -1 "none" _ "some") +— each compared with =, with a _ arm required for the rest. +some unwraps Some and early-returns None from the enclosing function.

(defconst nums [4 i32] [4 8 15 16])

From 76b2ab31139fe07846d2f43bb2750c2a4b7471d3 Mon Sep 17 00:00:00 2001
From: Joseph Ferano 
Date: Fri, 25 Sep 2026 21:01:15 +0700
Subject: [PATCH 2/2] A duplicate literal arm is one whose value equals an
 earlier arm's at the scrutinee's type, and a literal no dyn holds is refused
 with a pattern fix

---
 lib/check.ml      | 127 ++++++++++++++++++++++++++++++----------------
 test/test_flan.ml |  21 +++++++-
 2 files changed, 103 insertions(+), 45 deletions(-)

diff --git a/lib/check.ml b/lib/check.ml
index bd8ab9e8..6b340ded 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -8110,8 +8110,15 @@ and check_match ctx ?(tail = false) ?want loc scrutinee arms =
     match e.Ast.e with
     | Ast.Int n -> Int64.to_string n
     | Ast.UInt (_, t) -> t
-    | Ast.Float x when Float.is_integer x -> Printf.sprintf "%.1f" x
-    | Ast.Float x -> Printf.sprintf "%g" x
+    | Ast.Float x when Float.is_integer x && Float.abs x < 1e15 ->
+      Printf.sprintf "%.1f" x
+    | Ast.Float x ->
+      (* The shortest spelling that reads back as the same float. *)
+      let rec go p =
+        let t = Printf.sprintf "%.*g" p x in
+        if p >= 17 || float_of_string t = x then t else go (p + 1)
+      in
+      go 1
     | Ast.Byte b when b > 32 && b < 127 -> Printf.sprintf "\\%c" (Char.chr b)
     | Ast.Byte b -> string_of_int b
     | Ast.Str t -> Printf.sprintf "%S" t
@@ -8132,6 +8139,7 @@ and check_match ctx ?(tail = false) ?want loc scrutinee arms =
   in
   (* The checked literal of each literal arm, by the key [resolve_pat] gave it. *)
   let lits : (string, Tast.expr) Hashtbl.t = Hashtbl.create 8 in
+  let lit_values = ref [] in
   (* Which case each arm names, and the type of each name it binds. This is the
      whole of what differs between the two subjects; everything below it is
      shared. *)
@@ -8165,54 +8173,87 @@ and check_match ctx ?(tail = false) ?want loc scrutinee arms =
         (String.concat " " (List.map (fun (m, _) -> ":" ^ m) members))
     | `Lit t, Ast.Plit e ->
       let v =
-        match t with
         (* [=]'s dyn pair checks its literal at dyn, which boxes it. *)
-        | Types.Dyn -> check ctx ~want:Types.Dyn e
-        | t ->
-          (match trial ctx (fun () -> check ctx ~want:t e) with
-           | Ok v -> v
-           | Error _ ->
-             (* A literal that does not fit is refused, where [=] would widen
-                the pair and let the arm quietly never match. The literal's
-                own refusal is not repeated: its fixes are casts, and a cast
-                is not a pattern. *)
-             let tn = Types.to_string t in
-             let an =
-               match tn.[0] with
-               | 'a' | 'e' | 'f' | 'i' | 'o' -> "an " ^ tn
-               | _ -> "a " ^ tn
-             in
-             let why =
-               match e.Ast.e, t with
-               | Ast.Str _, _ -> "is a string"
-               | _, Types.String -> "is a number"
-               | Ast.Float x, Types.Int _ when not (Float.is_integer x) ->
-                 "is not a whole number"
-               | Ast.Float _, Types.Int _ -> "is a float"
-               | _ -> "does not fit in one"
-             in
+        match trial ctx (fun () -> check ctx ~want:t e) with
+        | Ok v -> v
+        | Error _ ->
+          (* A literal that does not fit is refused, where [=] would widen
+             the pair and let the arm quietly never match. The literal's
+             own refusal is not repeated: its fixes are casts, and a cast
+             is not a pattern. *)
+          (match t with
+           | Types.Dyn ->
              fail a.Ast.aloc
-               "this match is over %s, so each arm has to be %s, and %s %s. \
-                Change the arm to a value %s holds, or remove it"
-               tn an (spell e) why an)
+               "this match is over a dyn, which holds a number as an i64 or \
+                an f64, and %s fits in neither. Change the arm to a value an \
+                i64 holds, or remove it" (spell e)
+           | _ -> ());
+          let tn = Types.to_string t in
+          let an =
+            match tn.[0] with
+            | 'a' | 'e' | 'f' | 'i' | 'o' -> "an " ^ tn
+            | _ -> "a " ^ tn
+          in
+          let why =
+            match e.Ast.e, t with
+            | Ast.Str _, _ -> "is a string"
+            | _, Types.String -> "is a number"
+            | Ast.Float x, Types.Int _ when not (Float.is_integer x) ->
+              "is not a whole number"
+            | Ast.Float _, Types.Int _ -> "is a float"
+            | _ -> "does not fit in one"
+          in
+          fail a.Ast.aloc
+            "this match is over %s, so each arm has to be %s, and %s %s. \
+             Change the arm to a value %s holds, or remove it"
+            tn an (spell e) why an
       in
-      (* One key per value [=] cannot tell apart, so a second arm that could
-         never be reached is refused: 97 and \\a are one u8, and over a dyn
-         1 and 1.0 are equal, as they are over a float. *)
-      let key =
+      (* The arm's value at the scrutinee's type, and a second arm [=] could
+         not tell from an earlier one is refused, since it can never be
+         reached: 97 and \a are one u8, 0.1 and 0.10000000001 are one f32,
+         and over a dyn 1 and 1.0 are equal. Compared pairwise rather than
+         hashed, because dyn = between an integer and a float goes through
+         the float and is not transitive past 2^53. *)
+      let value =
+        let f32 x = Int32.float_of_bits (Int32.bits_of_float x) in
         let num x =
-          if Float.is_integer x && Float.abs x < 0x1p62 then
-            Printf.sprintf "i%Ld" (Int64.of_float x)
-          else Printf.sprintf "f%h" x
+          match t with Types.Float Types.F32 -> `F (f32 x) | _ -> `F x
         in
-        match e.Ast.e with
-        | Ast.Int n -> Printf.sprintf "i%Ld" n
-        | Ast.Byte b -> Printf.sprintf "i%d" b
-        | Ast.UInt (n, _) -> Printf.sprintf "u%Lu" n
-        | Ast.Float x -> num x
-        | Ast.Str t -> "s" ^ t
+        match e.Ast.e, t with
+        | Ast.Str s, _ -> `S s
+        | (Ast.Int n | Ast.UInt (n, _)), Types.Float _ -> num (Int64.to_float n)
+        | Ast.Byte b, Types.Float _ -> num (float_of_int b)
+        | (Ast.Int n | Ast.UInt (n, _)), _ -> `I n
+        | Ast.Byte b, _ -> `I (Int64.of_int b)
+        | Ast.Float x, _ -> num x
         | _ -> assert false
       in
+      let same x y =
+        match x, y with
+        | `I a, `I b -> Int64.equal a b
+        | `F a, `F b -> a = b
+        | `I a, `F b | `F b, `I a -> Int64.to_float a = b
+        | `S a, `S b -> String.equal a b
+        | _ -> false
+      in
+      (match List.find_opt (fun (w, _) -> same value w) !lit_values with
+       | Some (_, earlier) when earlier = spell e ->
+         fail a.Ast.aloc "this match has two %s arms" earlier
+       | Some (_, earlier) ->
+         fail a.Ast.aloc
+           "this match has two %s arms — %s equals it as %s, so this arm is \
+            never reached. Remove it"
+           earlier (spell e)
+           (match t with
+            | Types.Dyn -> "a dyn"
+            | t ->
+              let tn = Types.to_string t in
+              (match tn.[0] with
+               | 'a' | 'e' | 'f' | 'i' | 'o' -> "an " ^ tn
+               | _ -> "a " ^ tn))
+       | None -> ());
+      lit_values := (value, spell e) :: !lit_values;
+      let key = string_of_int (Hashtbl.length lits) in
       Hashtbl.replace lits key v;
       Some key, []
     | `Lit t, Ast.Pkw k ->
diff --git a/test/test_flan.ml b/test/test_flan.ml
index 69dadbed..5a85d2b4 100644
--- a/test/test_flan.ml
+++ b/test/test_flan.ml
@@ -4624,10 +4624,27 @@ let () =
     ~needle:"this match has two 5 arms";
   rejects_check "a char and a number that are one u8"
     "(defn f [c u8] i32 (match c \\a 1 97 2 _ 0))"
-    ~needle:"this match has two 97 arms";
+    ~needle:"this match has two \\a arms — 97 equals it as a u8";
   rejects_check "1 and 1.0 are one arm over a dyn, as dyn = says"
     "(defn f [d dyn] i32 (match d 1 1 1.0 2 _ 0))"
-    ~needle:"this match has two 1.0 arms";
+    ~needle:"this match has two 1 arms — 1.0 equals it as a dyn";
+  rejects_check "two literals that round to one f32"
+    "(defn f [x f32] i32 (match x 0.1 1 0.10000000001 2 _ 0))"
+    ~needle:"this match has two 0.1 arms — 0.10000000001 equals it as an f32";
+  rejects_check "two integers that round to one f32"
+    "(defn f [x f32] i32 (match x 16777216 1 16777217 2 _ 0))"
+    ~needle:"two 16777216 arms — 16777217 equals it as an f32";
+  rejects_check "an integer and a float that are one f64"
+    "(defn f [x f64] i32 \
+     (match x 4611686018427387904 1 4611686018427387904.0 2 _ 0))"
+    ~needle:"equals it as an f64";
+  accepts "two f64 literals that differ"
+    "(defn f [x f64] i32 (match x 0.1 1 0.10000000001 2 _ 0))";
+  rejects_check "a literal no dyn holds"
+    "(defn f [x dyn] i32 (match x 18446744073709551615 1 _ 0))"
+    ~needle:"this match is over a dyn, which holds a number as an i64 or an \
+             f64, and 18446744073709551615 fits in neither. Change the arm to \
+             a value an i64 holds, or remove it";
   rejects_check "a keyword arm among literal arms"
     "(defn f [n i32] i32 (match n 5 1 :lo 2 _ 0))"
     ~needle:":lo is an enum member, and this match is over i32, whose arms are \