Add basic support for RPIT #1351
Conversation
| @@ -436,7 +438,7 @@ fn resolve_function<'tcx>( | |||
|
|
|||
| // Try to extract a function defid from an operand | |||
| fn func_defid<'tcx>(op: &Operand<'tcx>) -> Option<(DefId, GenericArgsRef<'tcx>)> { | |||
| let fun_ty = op.constant().unwrap().const_.ty(); | |||
| let fun_ty = op.constant()?.const_.ty(); | |||
There was a problem hiding this comment.
this just allows us to report a nicer error rather than panic.
| @@ -444,7 +444,12 @@ impl<'tcx> TranslationCtx<'tcx> { | |||
| pub(crate) fn typing_env(&self, def_id: DefId) -> TypingEnv<'tcx> { | |||
| // FIXME: is it correct to pretend we are doing a non-body analysis? | |||
| let param_env = self.param_env(def_id); | |||
| TypingEnv { typing_mode: TypingMode::non_body_analysis(), param_env } | |||
| let mode = if self.is_mir_available(def_id) && def_id.is_local() { | |||
| TypingMode::post_borrowck_analysis(self.tcx, def_id.as_local().unwrap()) | |||
There was a problem hiding this comment.
I tried to use [analysis_in_body](https://doc.rust-lang.org/beta/nightly-rustc/rustc_type_ir/infer_ctxt/enum.TypingMode.html#tymethod.analysis_in_body) but that panicked whereas this seems to give the correct results.
| tcx.def_path(aty.def_id).data.last().unwrap().disambiguator | ||
| ))), | ||
| TyKind::Alias(_, aty) => Some(Symbol::intern(&type_name( | ||
| tcx.opt_item_name(aty.def_id).unwrap_or(Symbol::intern("synthetic")).as_str(), |
There was a problem hiding this comment.
I'm not sure how but I'm getting these new "synthetic" types in the code I'm looking at which I don't yet know how to handle cleanly here.
|
Thanks, Xavier, I'll have a look into that. In particular I'd like to better understand the choices about the type checker mode. Ot does not seem like that post analysis mode is the right mode... Also, I don't see why these types in parameter position are more difficult to handle : cannot we handle them as abstract types in the body, and ask the type checker what they at the call site ? |
It's not fundamentally more difficult but Rust compiles them to additional generic parameters literally called |
I agree but normalization panics when in |
| pub fn main() { | ||
| let x = returns_iterator().a(); | ||
|
|
||
| proof_assert!(x); |
There was a problem hiding this comment.
I guess I should move this to should_fail as I specifically want to test that we can't observe anything about x (other than what is specified by the trait). Would need to add a spec to the impl though for that to work.
|
I forgot I actually did have some argument position impl traits: which generate invalid coma: |
|
hmm I may just have added support for APIT by replacing spaces with |
|
Please try to avoid name clashes... |
|
The whole thing goes through the clone map after so it should get a unique count. |
|
Specifying functions with RPIT is tricky because our encoding of ensures won't work, specifically we create a closure with |
A proof I was working on was using
impl Iteratorand I got annoyed at us not supporting it. Return position impl trait is a lot simpler than the argument position since we can just compile it to an opaque type outside the defining scope (now that we "monomorphize" everything).