check predicates, well-formedness in the MIR type-checker #45827

Activity

1. nikomatsakis

   added

   T-compilerRelevant to the compiler team, which will review and decide on the PR/issue.Relevant to the compiler team, which will review and decide on the PR/issue.

   WG-compiler-nll

   on Nov 7, 2017
2. arielb1

   added this to the NLL prototype milestone on Nov 15, 2017
3. SimonSapin commented on Nov 17, 2017

   

   SimonSapin

   on Nov 17, 2017

   Last edited by SimonSapin

   Contributor

   More actions

   Has this been implemented? In b3f3390 the test case wrote (and expected to fail) passes. Or is my test not testing the right thing?

   // Copyright 2017 The Rust Project Developers. See the COPYRIGHT
   // file at the top-level directory of this distribution and at
   // http://rust-lang.org/COPYRIGHT.
   //
   // Licensed under the Apache License, Version 2.0 <LICENSE-APACHE or
   // http://www.apache.org/licenses/LICENSE-2.0> or the MIT license
   // <LICENSE-MIT or http://opensource.org/licenses/MIT>, at your
   // option. This file may not be copied, modified, or distributed
   // except according to those terms.
   
   //revisions: ast mir
   //[mir] compile-flags: -Z emit-end-regions -Z borrowck-mir -Z nll
   
   use std::cell::Cell;
   
   fn assert_sync<T>(x: T) -> T where T: Sync { x }
   struct AssertSync<T>(T) where T: Sync;
   
   fn foo() {
       let _x = assert_sync(Cell::new(()));
       //[ast]~^ ERROR the trait bound `std::cell::Cell<()>: std::marker::Sync` is not satisfied [E0277]
       //[mir]~^^ ERROR the trait bound `std::cell::Cell<()>: std::marker::Sync` is not satisfied [E0277]
       let _x = AssertSync(Cell::new(()));
       //[ast]~^ ERROR the trait bound `std::cell::Cell<()>: std::marker::Sync` is not satisfied [E0277]
       //[ast]~^^ ERROR the trait bound `std::cell::Cell<()>: std::marker::Sync` is not satisfied [E0277]
       //[mir]~^^^ ERROR the trait bound `std::cell::Cell<()>: std::marker::Sync` is not satisfied [E0277]
       //[mir]~^^^^ ERROR the trait bound `std::cell::Cell<()>: std::marker::Sync` is not satisfied [E0277]
   }
   
   fn main() {}

   (I don’t know why the same error is reported twice in the struct case, but that’s even further from the expected zero.)
4. nikomatsakis commented on Nov 20, 2017

   

   nikomatsakis

   on Nov 20, 2017

   Last edited by nikomatsakis

   ContributorAuthor

   More actions

   Some example tests that ought not to pass. Try running them with -Znll -Zborrowck-mir. I'll update with more as I go.

   ---

   #![allow(dead_code)]
   
   fn foo<'a, 'b>(x: &'a u32, y: &'b u32) -> (&'a u32, &'b u32)
       where 'a: 'b
   {
       (x, y)
   }
   
   fn bar<'a, 'b>(x: &'a u32, y: &'b u32) -> (&'a u32, &'b u32)
   {
       foo(x, y)
   }
   
   fn main() { }
   

   The problem here is that the where-clauses on foo are not being enforced by the MIR type-checker.

   ---

   Another example, with structs.

   #![allow(dead_code)]
   
   use std::cell::Cell;
   
   struct Foo<'a, 'b> where 'a: 'b {
       x: Cell<&'a u32>,
       y: Cell<&'b u32>,
   }
   
   fn bar<'a, 'b>(x: Cell<&'a u32>, y: Cell<&'b u32>) {
       Foo { x, y };
   }
   
   fn main() { }

   ---

   In check_rvalue, when checking aggregate values, we need to also enforce the predicates from the aggregate.

   To get those, we will want to write a helper like aggregate_field_ty. This will use predicates_of to get the predicates for the various kinds of things and then apply the appropriate substitutes. Example for ADTs:

   match **ak {
       AggregateKind::Adt(def, _, substs, _) =>
           tcx.predicates_of(def).instantiate(tcx, substs),
       ...
   }
   
5. bors

   added a commit that references this issue on Nov 23, 2017

   Auto merge of #46054 - nikomatsakis:nll-master-to-rust-master-1, r=ar…

   ...

   b9b82fd
6. nikomatsakis commented on Dec 5, 2017

   

   nikomatsakis

   on Dec 5, 2017

   ContributorAuthor

   More actions

   Done (in nll-master)
7. nikomatsakis

   closed this as completedon Dec 5, 2017