Can't resolve incoherent impls

[carolynzech]

I tried writing a contract for char::as_ascii (in this file), but Kani couldn't find the implementation of as_ascii.

I tried this code:

use crate::char;

    #[kani::proof_for_contract(char::as_ascii)]
    #[kani::proof_for_contract(char::as_ascii)]
    fn check_as_ascii_ascii_char() {
        let ascii: char = kani::any_where(|c : &char| c.is_ascii());
        unsafe { 
            ascii.as_ascii();
        };
    }

    #[kani::proof_for_contract(char::as_ascii)]
    fn check_as_ascii_non_ascii_char() {
        let non_ascii: char = kani::any_where(|c: &char| !c.is_ascii());
        unsafe {
            non_ascii.as_ascii();
        }
    }

with Kani version: 0.53.0

I expected to see this happen: verification successful

Instead, this happened:

error: Failed to resolve checking function char::as_ascii because unable to find `as_ascii` inside module `char`
    --> /Users/cmzech/personal-verify-std/library/core/src/char/methods.rs:1851:5
     |
1851 |     #[kani::proof_for_contract(char::as_ascii)]
     |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
     |
     = note: this error originates in the attribute macro `kani::proof_for_contract` (in Nightly builds, run with -Z macro-backtrace for more info)

I tried adding this logic inside resolve.rs (here)

 match first {
        "char" =>  match tcx.incoherent_impls(SimplifiedType::Char).unwrap() {
            [one] => {
                segments.next();
                Ok(Path {base: *one, segments: segments.collect()})
            },
            _ => panic!("oops")
        }
        ROOT => {

just to see if it was an incoherent impls problem. That produces this new error message:

error: Failed to resolve checking function char::as_ascii because expected module, found implementation `char::methods::<impl char>`
    --> /Users/cmzech/personal-verify-std/library/core/src/char/methods.rs:1859:5
     |
1859 |     #[kani::proof_for_contract(char::as_ascii)]
     |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
     |
     = note: this error originates in the attribute macro `kani::proof_for_contract` (in Nightly builds, run with -Z macro-backtrace for more info)

which makes me think that our handling of incoherent impls is at least part of the problem.