Split Rust surface types from type layer types

rust-lang / a-mir-formality

a model of MIR and the Rust type/trait system

Apache License 2.0

285 stars 33 forks source link

Split Rust surface types from type layer types #54

Open nikomatsakis opened 2 years ago

nikomatsakis commented 2 years ago

Much as we have split out WhereClause (Rust surface level) from the logic layer's notion of goals/clauses, we should split out Rust types that user's write from the surface layer. This shows up in #22 because e.g. fn types like fn(_, &'a T) -> &'static T should have some notion of implied bounds.

nikomatsakis commented 2 years ago

Started on this in the user-ty branch. I'm currently just adding a (user-ty ...) function that converts types "in place", might be nicer eventually to move into the grammar.

nikomatsakis commented 2 years ago

Now that #56 added user-ty, I think the next step would be to modify the decl layer and the WhereClause to actually just use UserTy instead of Ty, and then do the (user-ty ...) invocations in the various decl metafunctions as well as where-clause->goal and friends. I'm going to hold off on doing that but it would make the code examples much nicer.