a-mir-formality icon indicating copy to clipboard operation
a-mir-formality copied to clipboard

Split Rust surface types from type layer types

Open nikomatsakis opened this issue 3 years ago • 2 comments

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 avatar Jun 02 '22 09:06 nikomatsakis

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 avatar Jun 02 '22 10:06 nikomatsakis

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.

nikomatsakis avatar Jun 03 '22 01:06 nikomatsakis