rustc-chalk integration

2019.04.23

Goals

  • validate the “chalk approach”: this seems like something that can mainly be done through integration
  • rust-analyzer integration
  • rustc integration
  • top concerns:
  • ensuring our story on region constraints holds together
  • validating the performance story
  • complete the chalk lowering: chalk doesn’t present handle all of rustc’s semantics
  • dyn Foo types
  • impl Foo types and inference
  • specialization
  • const generics integration
  • looking a bit further ahead: 
  • subtyping, coercions, other parts of type-checking?
  • document chalk thoroughly, reduce bus factor: we need more experts in traits + types
  • videos
  • rustc-guide chapters
  • coherence
  • what else?

Potential sprint goals

  • Smart predicate order selection — fairly trivial
  • Non-enumerable predicates — “intermediate” level of difficulty, good way to learn the solver

Work item table

description
category
next steps
smart predicate order selection
eng, easy
land chalk#193, then define better order rules
non-enumerable predicates
eng, hard
the design seems “clear” but it’ll be some work to do
region constraints
explore
the pieces are vaguely there but it’s going to take more exploration work and writing up blog posts etc
trait object types
eng, med
I think I’m persuaded to the general plan of ‘unfolding’ rules like dyn Foo: Foo during the clause lowering phase; it seems like this is (conceptually) straight-forward
trait object types and implied bounds
eng, doc, medium
we have to write-up the plan and generally agree on it, but the actual impl work should not be so hard
opaque types

I think that from chalk’s perspective, these are the same as trait object types
truncation
eng, easy
we could implement truncation on the rustc side, might be a good “intro task”
queryification
eng, med
generally getting close, have to do a bit more refactoring probably
specialization
explore
the next step is probably trying to write rules on paper and clarifying where the gaps are
universe-maps
eng, med
this is an important efficiency win in rustc, but it can be deferred for now
lazy normalization
unclear
this refers to removing the “eager norm” steps in rustc; it’s important but sort of unclear
test running
eng, easy
we can try to run the run-pass tests with chalk enabled and see what happens, so as to guide next steps
rust-analyzer integration
unclear
what will it really take to integrate with rust-analyzer? we’re getting close to the point where we need to plot out next steps, but they remain vague in my mind

Work items

  • Smart predicate order selection
  • Affects: chalk-engine, chalk-solve, rustc
  • e.g., defer Sized goals as long as possible
  • Support for “non-enumerable” predicates like ?T: Sized 
  • Affects: chalk-engine, chalk-solve, rustc
  • At minimum, we can defer work on them via smarter predicate order selection
  • We can then “bubble them up” by delaying answers. Probably the program_clauses callback would be able to return some kind of “option” like unenumerable, but we could handle it in many ways (e.g., perhaps a “special goal” much like CannotProve)
  • This feels like a bit of a distinct kind of delaying, though. Some of the specifics of how delaying works around negative goals don’t feel like a good fit.