Proposed change:
Replace the string comparison of generic arguments in multi-candidate path resolution with semantic type resolution. Today last_two_items_of_path_match and its helpers (normalized_last_two, impl_self_type_generic_args, strip_redundant_parens, fully_parenthesized in kani-compiler/src/kani_middle/resolve.rs) refine candidates by bracket-, paren-, and whitespace-normalizing the user's turbofish against def_path_str renderings — now over a hundred lines of hand-rolled string handling.
Instead, resolve the turbofish's generic arguments to Ty via type_resolution::resolve_ty and compare against the impl's self-type arguments semantically. The main missing piece is resolve_ty support for the argument kinds it currently rejects — at least TraitObject (type_resolution.rs:91) and BareFn (:86) — after which the rendering-dependent normalizations can be deleted rather than extended.
Motivation:
def_path_str is a diagnostics API with no stability promise: a toolchain bump can change a rendering and silently take contract resolution with it. #4777 is that failure mode and #3773 is the same lineage; the string layer also carries byte-vs-char pitfalls of its own (#4827). One class the string approach cannot close cheaply: a trait object nested inside another argument (S<Box<(dyn Any + 'static)>>) renders with inner parens that top-level paren-stripping does not reach, so the bare user spelling never matches — a semantic Ty compare erases that whole class for free.
The tactical string fixes (#4778, #4828) remain useful until then; this issue tracks the end state that removes the class. Requested in the #4778 review.
Proposed change:
Replace the string comparison of generic arguments in multi-candidate path resolution with semantic type resolution. Today
last_two_items_of_path_matchand its helpers (normalized_last_two,impl_self_type_generic_args,strip_redundant_parens,fully_parenthesizedinkani-compiler/src/kani_middle/resolve.rs) refine candidates by bracket-, paren-, and whitespace-normalizing the user's turbofish againstdef_path_strrenderings — now over a hundred lines of hand-rolled string handling.Instead, resolve the turbofish's generic arguments to
Tyviatype_resolution::resolve_tyand compare against the impl's self-type arguments semantically. The main missing piece isresolve_tysupport for the argument kinds it currently rejects — at leastTraitObject(type_resolution.rs:91) andBareFn(:86) — after which the rendering-dependent normalizations can be deleted rather than extended.Motivation:
def_path_stris a diagnostics API with no stability promise: a toolchain bump can change a rendering and silently take contract resolution with it. #4777 is that failure mode and #3773 is the same lineage; the string layer also carries byte-vs-char pitfalls of its own (#4827). One class the string approach cannot close cheaply: a trait object nested inside another argument (S<Box<(dyn Any + 'static)>>) renders with inner parens that top-level paren-stripping does not reach, so the bare user spelling never matches — a semanticTycompare erases that whole class for free.The tactical string fixes (#4778, #4828) remain useful until then; this issue tracks the end state that removes the class. Requested in the #4778 review.