[jiro-by-nori]

Summary

Fixes #152.

__conv_callable? answered "callable" for every name as soon as the receiver's class had a user method_missing. __check_convert then called the name unguarded, so the NoMethodError from a handler that ends in super escaped where CRuby answers nil.

CRuby's check_funcall_missing calls the user handler under rb_rescue2(... rb_eNoMethodError) and reads that raise as its default miss (Qundef). The new __conv_call reproduces the reading, and — because the reading is per-arm — keeps the neighbouring rules intact:

arm	reading
a name the class defines	body runs; a NoMethodError inside escapes
a user respond_to? or respond_to_missing? claim, with a user method_missing behind it	claim is believed; a NoMethodError escapes (check_funcall_failed re-raises)
a user method_missing with no claim	NoMethodError is the default miss: [false, nil]
nothing can answer	[false, nil]

called is kept apart from value so an answered nil still names its class (#to_i gives NilClass, #to_ary gives NilClass) while a miss reaches no implicit conversion / can't convert X into Y.

Call sites updated:

• __check_convert — String.try_convert, Array.try_convert, Kernel#Array's to_a fallback, and the to_str probe in Kernel#Integer;
• __to_integer / Kernel#Float — use called so a miss falls through to into Integer/into Float instead of naming NilClass;
• __to_array_type — Array#+/#concat now say no implicit conversion for the same miss.

The generated Prelude.lean/PreludeJson.lean are make gen output.

Test plan

• make check — ALL CHECKS PASSED (build, every proof book, soundness, comparator, desugarer, unit tests, conformance, docs).
• make check-not-weakened — CHECKS NOT WEAKENED.
• make conformance — ran 1287, agree 1087 (baseline ≥1087), sut_unsupported 194 (≤194), disagree 0; regressions and tier3 agree.
• New regression case difftest/corpus/regressions/conversion-method-missing.rb (status fixed, filed by hand) pins the issue's table plus the claim/real-method/answered-nil arms; the tier reports agree.

bin/ruby-lean --compare on the issue's table (model and CRuby 4.0.5 now print the same):

String.try_convert => nil
Array.try_convert => nil
Integer => TypeError: can't convert OnlyFoo into Integer
Integer exception: false => nil
Float => TypeError: can't convert OnlyFoo into Float
Float exception: false => nil
Array => [#<OnlyFoo:...>]
String => "#<OnlyFoo:...>"
ary + => TypeError: no implicit conversion of OnlyFoo into Array

Authored by Jiro, an autonomous agent: the code and this description.