Info on whether a type implements a trait

I'm working on a new feature for Kani where we can automatically verify certain functions for you. Currently, to use Kani you need to write a "proof harness" that invokes the function you want to verify on concrete types, e.g.:

fn foo<T: Clone + PartialEq + Eq>(x: T) -> bool {
    x == x.clone()
}

#[kani::proof]
fn harness() {
    let x: u8 = kani::any(); // Generate a nondeterministic u8
    foo(x); // Verify foo with all possible u8 values
}

We would like to make it so that the user doesn't need to write harness at all. Kani would ideally be able to look at the type signature of foo and come up with a handful of types that would satisfy its trait bounds, so that it can autogenerate harnesses for those types. (Note I say "a handful" instead of "all" -- there are obviously many types that implement Clone, PartialEq, and Eq, and it isn't necessarily good UX to generate proofs for all of them. But that's more of a Kani UX problem that we can solve later).

My (purposefully broad) question is: any thoughts about the best way to go about this using the StableMIR APIs? I want to avoid asking an XY question, so I'll outline a few solutions I've thought of, but open to other suggestions as well:

• Go from type --> trait: Have a hardcoded list of options for T in Kani (e.g., the primitive types). Use a method like type_implements_trait to filter those defaults by which satisfy T's trait bounds, then generate harnesses for those.
• Go from trait --> type: Somehow(?) provide the Rust compiler with a list of traits that I need satisfied, and ask it which types it knows of that implement those traits. I suspect this is hard/impossible because of the issues discussed here.

TIA!

Start by reviewing the StableMIR APIs relevant to trait queries, especially the referenced type_implements_trait entry point. Compare the proposed type-to-trait and trait-to-type approaches, then document whether StableMIR supports either direction and what constraints a Kani integration would need.