identifying which method will run for a trait

[nikomatsakis]

As part of rust-analyzer/rust-analyzer#4558, we would like to extend chalk so that it can identify the fn that will run. The basic idea is to model this in a similar fashion to how associated type normalization works.

Summary of the idea

Given:

impl<A> Foo for Bar<A> {
    fn method(&self) { }
}

where method has the type FnDef(X, [_]) we will generate a program clause like

forall<A> {
    NormalizeFn(<Foo as Bar<A>>::method => FnDef(X, [A]))
}

Rust-analyzer can then do a query like NormalizeFn(<Foo as Bar<u32>>::method => ?X) to find the FnDef type for the method that will run (which includes its unique id and the values of all its relevant type parameters).

[nikomatsakis]

Implementation steps:

• [ ] Extend chalk-ir
• [ ] Extend RustIrDatabase types
• [ ] Extend program clause generation
• [ ] Extend parser and unit testing

Extend the chalk-ir

• Refactor chalk_ir with a FnDefTy { fn_def_id, substitution } (analogous to ProjectionTy) and reference it from TyKind::FnDef
• Extend DomainGoal with a NormalizeFn(FnDefTy, Ty) predicate; the output type will (in practice) always be a FnDef type, but it's a pain to encode that I think so not worth it
  • here the FnDefTy represents the FnDef for the unnormalized trait method

Extend the database types

• The TraitDatum probably needs a list of functions (FnDefTy) for each thing in the trait
• The ImplDatum needs to have "fn-def values" for each method in the impl
• The RustIrDatabase needs a way to query for information about a fn-def value
  • This should link to the stuff in the trait

Actually, I think we have function signature and other information already accessible for FnDef, so we should leverage that.

Extend the program clause generation

The program_clauses_that_could_match function needs to be extended so that when we try to prove a NormalizeFn goal, we go to the relevant impls, and we generate NormalizeFn rules.

Extend the parser and unit testing

We ought to be able to write unit tests that include fn foo<A>() { } in them. We may want to include ABI and argument types -- I think we already have some of that logic in order to generate the impls of the Fn traits, so we just want to extend it to be included within traits and impls.

[nikomatsakis]

@rustbot assign @lf-

[lf-]

I am working on this on https://github.com/lf-/chalk/tree/source-impl (obviously it will be rebased and commits cleaned up when it's ready for proper review; I'm posting this for reference)

So far done:

• IR/database types, lowering, parsing. The way that the associated functions work is in the ChalkIr is that the IDs for those are just wrappers around FnDefIds, which can be used to look up AssociatedFnDatums.

To do as I keep going:

• Implement DB functions as required.

Confused about:

What to generate for program clauses for NormalizeFn(FnDefTy, Ty). I would really like an example of something reasonable for this from the stdlib for instance. I'm currently unsure what exact info this goal needs to encode and what program clauses to make.

[lf-]

So that was a lie. It turns out the lowering and parsing contains way more lowering and parsing than I thought 😭. Moving slowly but getting places. Total diff has already crossed 1000 lines :V

[jackh726]

@rustbot release-assignment

[compiler-errors]

@jackh726, is this up for grabs? i would be interested in continuing the work in the linked PR. been looking for some chalk work.

[jackh726]

I think in theory yes. But this is more of a question for Niko. He said he has thoughts for a different approach :)

[nikomatsakis]

@compiler-errors I'd be very psyched to see you continue with this work!

I did have thoughts for another approach, but essentially what I wanted to do was to make "methods" kind of a special sort of associated type, I believe. We could schedule some time to talk about it at https://calendly.com/nikomatsakis/, @compiler-errors.

[jackh726]

I think it would be cool to treat associated types, consts, and methods similarly in how we resolve them (thinking with #745 in mind)