[jiro-by-nori]

What this fixes

File.basename, File.dirname, File.extname and File.join began by calling to_s on every path argument, so a non-String path was stringified instead of refused — a wrong answer, not a gate:

program	model (before)	CRuby 4.0.5
File.dirname(123)	"."	TypeError: no implicit conversion of Integer into String
File.basename(123)	"123"	same TypeError
File.join(1, 2)	"1/2"	same TypeError
File.extname(:sym)	""	TypeError: no implicit conversion of Symbol into String

Two related join defects fell out of the same to_s-and-Array#join implementation: File.join(["a", "b"], "c") answered "[\"a\", \"b\"]/c" (CRuby "a/b/c"), and File.join("a/", "/b") answered "a///b" (CRuby "a/b").

The change

ruby-lean/prelude/prelude.rb only; the two generated files are make gen output.

• File.__path_string is CRuby's rb_get_path (file.c): a String is itself; otherwise to_path is asked with rb_check_funcall_default, whose default is the object itself; the answer then goes through StringValue. Nothing is coerced with to_s. Because the conversion dispatches, a method_missing-served to_path converts, a respond_to? that denies it does not, and a to_path returning a non-String is converted again — so dirname(obj_with_to_path_returning_42) names Integer, exactly as CRuby does.
• Kernel#__to_string_value is StringValue (rb_convert_type_with_id) for String, the twin of the existing __to_array_type: no implicit conversion of X into String when no to_str answers, can't convert X to String (X#to_str gives Y) when one answers a non-String.
• File.join follows rb_file_join: each element that is an Array is joined recursively with an identity cycle check (ArgumentError: recursive array; the same array twice is not a cycle, and a to_ary is not consulted), every other element goes through __path_string, and the separator is written only where chompdirsep/isdirsep say one is missing.
• basename's suffix takes the same conversion, which is why File.basename("a/b", :x) is now CRuby's TypeError.

Not modelled, and not pretended to: rb_get_path_check_convert's null-byte and non-ASCII-compatible-encoding refusals (the model has no encodings and refuses neither).

Tests

Two new difftest regression cases, both status: fixed, so this tier ratchets against reintroduction:

• difftest/corpus/regressions/file-path-argument-conversion.rb — the four rows above; nil/true naming; to_path vs to_str precedence; a non-String to_path/to_str answer; method_missing and respond_to? dispatch; Pathname; and basename's suffix.
• difftest/corpus/regressions/file-join-elements.rb — flattening and deep nesting, nested empty arrays, the separator rules, Integer/nil/Hash/Symbol elements, a to_ary element, a shared array, and self/nested cycles.

Validation

Run on the branch from a cold toolchain (Lean v4.32.2, CRuby 4.0.5, GNU Make and the pinned gems installed by hand because this sandbox has no root):

make check              -> make check: ALL CHECKS PASSED
make check-not-weakened -> CHECKS NOT WEAKENED

• make conformance — CRuby 4.0.5 over bootstraptest, the regressions tier and tier3: disagree 0; the regressions tier reports held 224, gated 1 with both new cases agree, so they pin rather than gate.
• Direct differential probes against CRuby 4.0.5 (throwaway, not in the diff): ~40 programs — the four issue rows, to_path/to_str/neither/both, non-String answers, method_missing/respond_to? overrides, Pathname, String subclasses, nested/deep arrays, separator runs, shared and cyclic arrays — byte-identical, messages included.
• make gen-check — regenerated PreludeJson.lean and Prelude.lean are fresh.
• make books, make metatheory, make soundness, make comparator — every proof book builds, including the audited axioms; the boot heap regeneration did not move a pinned id.
• make lint (ruff, RuboCop, shellcheck, actionlint), make difftest-test, make desugar-test, make desugar-coverage, make feature-loading, make book-checks, make docs.

No recorded result fell, no check or theorem was dropped, no sorry/native_decide/axiom/skip was added.

Provenance

Authored by Jiro, an autonomous agent, including this description.

Closes #57