JosephFerano/flan
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Which copy a generic call gets stopped depending on argument order

Browse Source 
Implicit widening landed after generics did, and the rule the two of
them left between them read off the order the arguments were written
in. (eq2? i8 i64) was refused, because $t bound to i8 and i64 into i8
can lose. (eq2? i64 i8) was accepted, because $t had already bound to
i64 and the i8 widened into the want that substitution had made
concrete. Same two values, same function, one copy at i8 refused and
one copy at i64 generated.

Neither answer was unsound -- a widen cannot change a number -- so
this is not a bug report, it is a decision that was never taken.
Taking it: implicit widening does not cross a generic binding. A
concrete argument at a variable an earlier argument already bound has
to be that type, and both orders now refuse with the same sentence,
naming the binding, the argument, and the cast to write.

Refusing is the direction that can be walked back. Letting the pair
join at the wider type is a coherent rule too, and it can be added
later without invalidating a program written under this one; the
reverse is not true.

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 it always had when the trial
refuses.
This commit is contained in:
Joseph Ferano 2026-09-20 20:30:36 +07:00
parent 879a439951
commit c91fd51ad6
2 changed files with 114 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

68
lib/check.ml
View File

@ -7486,9 +7486,71 @@ and generic_call ctx ~want loc name vars pats pret args =
let subst = ref [] in
let targs =
map2_lr
(fun p a ->
let p = subst_ty !subst p in
let a = if generic_ty p then check ctx a else check ctx ~want:p a in
(fun pat a ->
let p = subst_ty !subst pat in
(* Which variable, if any, this parameter *is* — written as a bare
[$t] and already bound by an argument to the left. That is the one
shape implicit widening can reach, because [Types.widens_to] admits
only numeric scalars: a variable bound inside [[$t]] or
[(Fn [$t $t] bool)] leaves a parameter no widening applies to, so
the [sort-by] path below is untouched by construction. *)
let bound_scalar =
match pat with
| Types.Var v when (not (generic_ty p)) && Types.is_numeric p ->
Some v
| _ -> None
in
(* An untyped constant has no type of its own to keep, so it still
takes the variable's — [(clamp-to y 0 10)] with [y] an i64 means
three i64s and there is no conversion anywhere in it. Everything
else is checked on its own terms. *)
let untyped_literal =
match a.Ast.e with
| Ast.Int _ | Ast.Float _ | Ast.Byte _ -> true
| _ -> false
in
let a =
if generic_ty p then check ctx a
else if bound_scalar <> None && not untyped_literal then
(* On its own terms first. A form that has no type without a want
— [(zeroed)] is the one that matters — refuses here and is
checked against the parameter as it always was; the trial
leaves no trace of the attempt. *)
(match trial ctx (fun () -> check ctx a) with
| Ok r -> r
| Error _ -> check ctx ~want:p a)
else check ctx ~want:p a
in
(* **Implicit widening does not cross a generic binding.** A concrete
argument at a variable an earlier argument already bound has to be
the same type, not merely a type that widens into it.
This is a decision and not a consequence. Widening landed after
generics did, and left behind a rule that depended on argument
order: [(pair-eq? i64 i8)] was accepted, because [$t] bound to i64
first and the i8 widened into the want; [(pair-eq? i8 i64)] was
refused, because [$t] bound to i8 and i64 into i8 can lose. Same
two values, same function, two answers. Neither is unsound — a
widen cannot change a number — but which instantiation a program
gets should not depend on which argument was written first.
Refusing both is the direction that can be walked back. Allowing
the pair to join at the wider type is a coherent rule too, and it
is the one to reach for if the ergonomics turn out to want it; it
can be added later without invalidating a program that was written
under this rule, and the reverse is not true. FIX.org, "Generics
and implicit widening". *)
(match bound_scalar with
| Some v when not (Types.equal p a.Tast.ty) ->
Loc.failk "check/tyvar-no-widening" a.Tast.loc
"%s's $%s was bound to %s by an earlier argument, and this one \
is %s. Implicit widening does not cross a generic binding: a \
written type is what a type variable takes, so the same \
variable is the same type at every argument. Write the \
conversion — (%s x) — or pass the arguments at one type"
name v (Types.to_string p) (Types.to_string a.Tast.ty)
(Types.to_string p)
| _ -> ());
if not (bind_ty subst p a.Tast.ty) then
fail a.Tast.loc "%s expects %s here, found %s" name
(Types.to_string p) (Types.to_string a.Tast.ty);

49
test/test_flan.ml
View File

@ -4711,6 +4711,55 @@ let () =
accepts "and is accepted when it is"
"(defn outer [s [$t]] () {:where (ordered? $t)} (sort s))";
(* ── Implicit widening does not cross a generic binding ─────────────
Widening landed after generics did, and the rule it left behind depended
on the order the arguments were written in: the i8-then-i64 call was
refused because i64 into i8 can lose, and the i64-then-i8 call was
*accepted*, because $t had already bound to i64 and the i8 widened into
the want. Same two values, same function, two answers.
Neither was unsound — a widen cannot change a number — but which copy a
program gets should not turn on which argument came first, so both are
refused now and both name the binding. Letting the pair join at the wider
type is the other coherent rule and it stays available: it can be added
without invalidating anything written under this one, which is why this
is the direction to be wrong in. FIX.org, "Generics and implicit
widening". *)
rejects_check "a narrower argument does not widen into a bound type variable"
~needle:"was bound to i64 by an earlier argument"
"(defn eq2? [a $t b $t] bool {:where (equal? $t)} (= a b))\n\
(defn main [] () (println (eq2? (i64 3) (i8 3))))";
rejects_check "and the other argument order refuses identically"
~needle:"was bound to i8 by an earlier argument"
"(defn eq2? [a $t b $t] bool {:where (equal? $t)} (= a b))\n\
(defn main [] () (println (eq2? (i8 3) (i64 3))))";
(* The written conversion is what the message asks for, and it is accepted:
the refusal is about the *implicit* step, not about reaching i64. *)
accepts "the written conversion is accepted"
"(defn eq2? [a $t b $t] bool {:where (equal? $t)} (= a b))\n\
(defn main [] () (println (eq2? (i64 3) (i64 (i8 3)))))";
(* An untyped constant has no type of its own to keep, so it still takes the
variable's. Nothing is converted here — three i64s were written. *)
accepts "an untyped literal still takes a bound type variable's type"
"(defn clamp3 [x $t lo $t hi $t] $t {:where (ordered? $t)} \
(min (max x lo) hi))\n\
(defn main [] () (println (clamp3 (i64 12) 0 10)))";
(* And the shapes widening cannot reach are untouched, which is the reason
the rule costs so little: [Types.widens_to] admits only numeric scalars,
so a variable bound inside a slice or a function type leaves a parameter
no widening applied to in the first place. *)
accepts "a variable bound inside a constructor is unaffected"
"(defn sort2 [s [$t] before? (Fn [$t $t] bool)] () \
(sort-by s before?))\n\
(defn main [] () (let [ns [5 3 9 1]] \
(sort2 (slice ns 0 4) (fn [a b] (< a b))) (println (at ns 0))))";
(* A form with no type of its own is still checked against the parameter:
the trial that asks for its natural type refuses, and the want it always
had is what it falls back to. *)
accepts "a form that needs a want still gets one at a bound type variable"
"(defn pick [a $t b $t] $t (do b a))\n\
(defn main [] () (println (pick (i64 3) (zeroed))))";
(* ── A numeric literal where a type variable is wanted ──────────────
The author's motivating family — one pos? over every numeric type from
one definition — needs a written 0 to stand where $t stands. The bound