diff --git a/crates/formality-rust/src/check/fns.rs b/crates/formality-rust/src/check/fns.rs index a790c7e91..a7207e8ea 100644 --- a/crates/formality-rust/src/check/fns.rs +++ b/crates/formality-rust/src/check/fns.rs @@ -1,6 +1,7 @@ use crate::check::borrow_check::env::TypeckEnv; use crate::check::borrow_check::flow_state::FlowState; use crate::check::borrow_check::nll::borrow_check; +use crate::check::implied_bounds::implied_bounds_from_fn; use crate::check::prove_goal; use crate::check::where_clauses::prove_where_clauses_well_formed; use crate::grammar::{CrateId, FnBody, MaybeFnBody, Relation, Wcs}; @@ -47,7 +48,8 @@ judgment_fn! { ( (let (env, bound_data) = env.instantiate_universally(&f.binder)) (let FnBoundData { input_args, output_ty, where_clauses, body } = bound_data) - (let assumptions: Wcs = (assumptions, where_clauses).to_wcs()) + (implied_bounds_from_fn(input_args, output_ty) => implied_bounds) + (let assumptions: Wcs = (assumptions, where_clauses, implied_bounds).to_wcs()) (prove_where_clauses_well_formed(program, env, assumptions, where_clauses) => ()) (for_all(input_arg in input_args) (prove_goal(program, env, assumptions, Relation::well_formed(&input_arg.ty)) => ())) diff --git a/crates/formality-rust/src/check/implied_bounds.rs b/crates/formality-rust/src/check/implied_bounds.rs new file mode 100644 index 000000000..17e0e224d --- /dev/null +++ b/crates/formality-rust/src/check/implied_bounds.rs @@ -0,0 +1,94 @@ +use crate::grammar::{InputArg, Parameter, RigidName, RigidTy, Ty, Wcs, WhereClause}; +use formality_core::{judgment_fn, Cons}; + +judgment_fn! { + pub fn implied_bounds_from_fn( + args: Vec, + output: Ty, + ) => Wcs { + debug(args, output) + + ( + (implied_bounds_from_args(args) => args_wcs) + (implied_bounds_from_ty(output) => output_wcs) + ------------------------------------------------------------ ("bounds") + (implied_bounds_from_fn(args, output) => (args_wcs, output_wcs)) + ) + } + +} + +judgment_fn! { + fn implied_bounds_from_args( + tys: Vec + ) => Wcs { + debug(tys) + + ( + ((implied_bounds_from_ty(&arg.ty)) => head_wcs) + (implied_bounds_from_args(tail) => tail_wcs) + ------------------------------------------------------------ ("recurse args") + (implied_bounds_from_args(Cons(arg, tail)) => (head_wcs, tail_wcs)) + ) + + ( + ------------------------------------------------------------ ("nil") + (implied_bounds_from_args(()) => ()) + ) + } + +} + +judgment_fn! { + fn implied_bounds_from_ty( + ty: Ty, + ) => Wcs { + debug(ty) + + ( + (if let [Parameter::Lt(lt), inner] = ¶meters[..]) + (let wc = vec![WhereClause::outlives(inner, lt)]) + (implied_bounds_from_params(vec![inner]) => inner_wcs) + ------------------------------------------------------------ ("inner ref") + (implied_bounds_from_ty(RigidTy { name: RigidName::Ref(_), parameters }, ) => (inner_wcs, wc)) + ) + + ( + (implied_bounds_from_params(parameters) => wcs) + ------------------------------------------------------------ ("inner T") + (implied_bounds_from_ty(RigidTy { name: _, parameters }) => wcs) + ) + + ( + ------------------------------------------------------------ ("no bounds") + (implied_bounds_from_ty(ty) => ()) + ) + } + +} + +judgment_fn! { + fn implied_bounds_from_params( + param: Vec + ) => Wcs { + debug(param) + + ( + (implied_bounds_from_ty(ty) => head_wcs) + (implied_bounds_from_params(tail) => tail_wcs) + ------------------------------------------------------------ ("recurse ty param") + (implied_bounds_from_params(Cons(Parameter::Ty(ty), tail)) => (head_wcs, tail_wcs)) + ) + + ( + (implied_bounds_from_params(tail) => tail_wcs) + ------------------------------------------------------------ ("param not ty") + (implied_bounds_from_params(Cons(_, tail)) => tail_wcs) + ) + + ( + ------------------------------------------------------------ ("nil") + (implied_bounds_from_params(_x) => ()) + ) + } +} diff --git a/crates/formality-rust/src/check/mod.rs b/crates/formality-rust/src/check/mod.rs index a45d7a3b8..dd8bbe8dc 100644 --- a/crates/formality-rust/src/check/mod.rs +++ b/crates/formality-rust/src/check/mod.rs @@ -25,6 +25,7 @@ mod adts; mod coherence; mod core_crate; mod fns; +mod implied_bounds; mod impls; mod traits; mod where_clauses; diff --git a/tests/borrowck.rs b/tests/borrowck.rs index 3eb80e36f..99db0a67d 100644 --- a/tests/borrowck.rs +++ b/tests/borrowck.rs @@ -2183,6 +2183,36 @@ fn min_problem_case_3() { the rule "write-indirect" at (nll.rs) failed because pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `m` + the rule "write-indirect" at (nll.rs) failed because + condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)` + place_accessed = *(m : &!lt_1 mut Map) : <&!lt_1 mut Map as Derefable>::Target + place_loaned_ref = m : &!lt_1 mut Map + + the rule "borrow of disjoint places" at (nll.rs) failed because + condition evaluated to false: `place_disjoint_from_place(&loan.place, &access.place)` + &loan.place = *(m : &!lt_1 mut Map) : <&!lt_1 mut Map as Derefable>::Target + &access.place = *(m : &!lt_1 mut Map) : <&!lt_1 mut Map as Derefable>::Target + + the rule "loan_cannot_outlive" at (nll.rs) failed because + condition evaluated to false: `!outlived_by_loan.contains(&lifetime.upcast())` + outlived_by_loan = {!lt_1, ?lt_2, ?lt_3} + &lifetime.upcast() = !lt_1 + + the rule "loan_not_required_by_universal_regions" at (nll.rs) failed because + condition evaluated to false: `outlived_by_loan.iter().all(|p| match p + { + Parameter::Ty(_) => false, Parameter::Lt(lt) => match lt.as_ref() + { + Lt::Static => false, Lt::Variable(Variable::UniversalVar(_)) => false, + Lt::Variable(Variable::ExistentialVar(_)) => true, + Lt::Variable(Variable::BoundVar(_)) => + panic!("cannot outlive a bound var"), Lt::Erased => true, + }, Parameter::Const(_) => panic!("cannot outlive a constant"), + })` + + the rule "write-indirect" at (nll.rs) failed because + pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `m` + the rule "write-indirect" at (nll.rs) failed because condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)` place_accessed = *(m : &!lt_1 mut Map) : <&!lt_1 mut Map as Derefable>::Target @@ -2390,13 +2420,53 @@ fn undeclared_universal_region_relationship() { } } }]).borrowck_err(BorrowCheckFailure::All, expect_test::expect![[r#" - crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_1 : !lt_2, via: @ wf(?lt_0), assumptions: {@ wf(?lt_0)}, env: Env { variables: [!lt_1, !lt_2, ?lt_0], bias: Soundness, pending: [], allow_pending_outlives: false } } + crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_0 : !lt_1, via: @ wf(?lt_2), assumptions: {u32 : !lt_0, u32 : !lt_1, @ wf(?lt_2)}, env: Env { variables: [!lt_0, !lt_1, ?lt_2], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_0 : !lt_1, via: u32 : !lt_0, assumptions: {u32 : !lt_0, u32 : !lt_1, @ wf(?lt_2)}, env: Env { variables: [!lt_0, !lt_1, ?lt_2], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_0 : !lt_1, via: u32 : !lt_1, assumptions: {u32 : !lt_0, u32 : !lt_1, @ wf(?lt_2)}, env: Env { variables: [!lt_0, !lt_1, ?lt_2], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_0, b: !lt_1, assumptions: {u32 : !lt_0, u32 : !lt_1, @ wf(?lt_2)}, env: Env { variables: [!lt_0, !lt_1, ?lt_2], bias: Soundness, pending: [], allow_pending_outlives: false } } - crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_1, b: !lt_2, assumptions: {@ wf(?lt_0)}, env: Env { variables: [!lt_1, !lt_2, ?lt_0], bias: Soundness, pending: [], allow_pending_outlives: false } } + crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_0 : !lt_1, via: @ wf(?lt_2), assumptions: {u32 : !lt_0, u32 : !lt_1, @ wf(?lt_2)}, env: Env { variables: [!lt_0, !lt_1, ?lt_2], bias: Soundness, pending: [], allow_pending_outlives: false } } - crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_1 : !lt_2, via: @ wf(?lt_0), assumptions: {@ wf(?lt_0)}, env: Env { variables: [!lt_1, !lt_2, ?lt_0], bias: Soundness, pending: [], allow_pending_outlives: false } } + crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_0 : !lt_1, via: u32 : !lt_0, assumptions: {u32 : !lt_0, u32 : !lt_1, @ wf(?lt_2)}, env: Env { variables: [!lt_0, !lt_1, ?lt_2], bias: Soundness, pending: [], allow_pending_outlives: false } } - crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_1, b: !lt_2, assumptions: {@ wf(?lt_0)}, env: Env { variables: [!lt_1, !lt_2, ?lt_0], bias: Soundness, pending: [], allow_pending_outlives: false } }"#]]) + crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_0 : !lt_1, via: u32 : !lt_1, assumptions: {u32 : !lt_0, u32 : !lt_1, @ wf(?lt_2)}, env: Env { variables: [!lt_0, !lt_1, ?lt_2], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_0, b: !lt_1, assumptions: {u32 : !lt_0, u32 : !lt_1, @ wf(?lt_2)}, env: Env { variables: [!lt_0, !lt_1, ?lt_2], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_0 : !lt_2, via: @ wf(?lt_1), assumptions: {u32 : !lt_0, @ wf(?lt_1)}, env: Env { variables: [!lt_0, !lt_2, ?lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_0 : !lt_2, via: u32 : !lt_0, assumptions: {u32 : !lt_0, @ wf(?lt_1)}, env: Env { variables: [!lt_0, !lt_2, ?lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_0, b: !lt_2, assumptions: {u32 : !lt_0, @ wf(?lt_1)}, env: Env { variables: [!lt_0, !lt_2, ?lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_0 : !lt_2, via: @ wf(?lt_1), assumptions: {u32 : !lt_0, @ wf(?lt_1)}, env: Env { variables: [!lt_0, !lt_2, ?lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_0 : !lt_2, via: u32 : !lt_0, assumptions: {u32 : !lt_0, @ wf(?lt_1)}, env: Env { variables: [!lt_0, !lt_2, ?lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_0, b: !lt_2, assumptions: {u32 : !lt_0, @ wf(?lt_1)}, env: Env { variables: [!lt_0, !lt_2, ?lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_2 : !lt_0, via: @ wf(?lt_1), assumptions: {u32 : !lt_0, @ wf(?lt_1)}, env: Env { variables: [!lt_2, !lt_0, ?lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_2 : !lt_0, via: u32 : !lt_0, assumptions: {u32 : !lt_0, @ wf(?lt_1)}, env: Env { variables: [!lt_2, !lt_0, ?lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_2, b: !lt_0, assumptions: {u32 : !lt_0, @ wf(?lt_1)}, env: Env { variables: [!lt_2, !lt_0, ?lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_2 : !lt_0, via: @ wf(?lt_1), assumptions: {u32 : !lt_0, @ wf(?lt_1)}, env: Env { variables: [!lt_2, !lt_0, ?lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_2 : !lt_0, via: u32 : !lt_0, assumptions: {u32 : !lt_0, @ wf(?lt_1)}, env: Env { variables: [!lt_2, !lt_0, ?lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_2, b: !lt_0, assumptions: {u32 : !lt_0, @ wf(?lt_1)}, env: Env { variables: [!lt_2, !lt_0, ?lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_1 : !lt_2, via: @ wf(?lt_0), assumptions: {@ wf(?lt_0)}, env: Env { variables: [!lt_1, !lt_2, ?lt_0], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_1, b: !lt_2, assumptions: {@ wf(?lt_0)}, env: Env { variables: [!lt_1, !lt_2, ?lt_0], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_1 : !lt_2, via: @ wf(?lt_0), assumptions: {@ wf(?lt_0)}, env: Env { variables: [!lt_1, !lt_2, ?lt_0], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_1, b: !lt_2, assumptions: {@ wf(?lt_0)}, env: Env { variables: [!lt_1, !lt_2, ?lt_0], bias: Soundness, pending: [], allow_pending_outlives: false } }"#]]) } /// Same as `undeclared_universal_region_relationship`, but the function @@ -2412,13 +2482,69 @@ fn undeclared_universal_region_relationship_no_return() { } } }]).borrowck_err(BorrowCheckFailure::All, expect_test::expect![[r#" - crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_0, b: !lt_1, assumptions: {}, env: Env { variables: [!lt_0, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } } + crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_0 : !lt_1, via: u32 : !lt_0, assumptions: {u32 : !lt_0, u32 : !lt_1}, env: Env { variables: [!lt_0, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_0 : !lt_1, via: u32 : !lt_1, assumptions: {u32 : !lt_0, u32 : !lt_1}, env: Env { variables: [!lt_0, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_0, b: !lt_1, assumptions: {u32 : !lt_0, u32 : !lt_1}, env: Env { variables: [!lt_0, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_0 : !lt_1, via: u32 : !lt_0, assumptions: {u32 : !lt_0, u32 : !lt_1}, env: Env { variables: [!lt_0, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_0 : !lt_1, via: u32 : !lt_1, assumptions: {u32 : !lt_0, u32 : !lt_1}, env: Env { variables: [!lt_0, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_0, b: !lt_1, assumptions: {u32 : !lt_0, u32 : !lt_1}, env: Env { variables: [!lt_0, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_0 : !lt_1, via: u32 : !lt_0, assumptions: {u32 : !lt_0, u32 : !lt_1}, env: Env { variables: [!lt_0, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_0 : !lt_1, via: u32 : !lt_1, assumptions: {u32 : !lt_0, u32 : !lt_1}, env: Env { variables: [!lt_0, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_0, b: !lt_1, assumptions: {u32 : !lt_0, u32 : !lt_1}, env: Env { variables: [!lt_0, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_0 : !lt_1, via: u32 : !lt_0, assumptions: {u32 : !lt_0, u32 : !lt_1}, env: Env { variables: [!lt_0, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_0 : !lt_1, via: u32 : !lt_1, assumptions: {u32 : !lt_0, u32 : !lt_1}, env: Env { variables: [!lt_0, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_0, b: !lt_1, assumptions: {u32 : !lt_0, u32 : !lt_1}, env: Env { variables: [!lt_0, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_0 : !lt_1, via: u32 : !lt_0, assumptions: {u32 : !lt_0}, env: Env { variables: [!lt_0, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_0, b: !lt_1, assumptions: {u32 : !lt_0}, env: Env { variables: [!lt_0, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_0 : !lt_1, via: u32 : !lt_0, assumptions: {u32 : !lt_0}, env: Env { variables: [!lt_0, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_0, b: !lt_1, assumptions: {u32 : !lt_0}, env: Env { variables: [!lt_0, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } } - crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_0, b: !lt_1, assumptions: {}, env: Env { variables: [!lt_0, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } } + crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_0 : !lt_1, via: u32 : !lt_0, assumptions: {u32 : !lt_0}, env: Env { variables: [!lt_0, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } } - crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_0, b: !lt_1, assumptions: {}, env: Env { variables: [!lt_0, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } } + crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_0, b: !lt_1, assumptions: {u32 : !lt_0}, env: Env { variables: [!lt_0, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } } - crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_0, b: !lt_1, assumptions: {}, env: Env { variables: [!lt_0, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } }"#]]) + crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_0 : !lt_1, via: u32 : !lt_0, assumptions: {u32 : !lt_0}, env: Env { variables: [!lt_0, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_0, b: !lt_1, assumptions: {u32 : !lt_0}, env: Env { variables: [!lt_0, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_1 : !lt_0, via: u32 : !lt_0, assumptions: {u32 : !lt_0}, env: Env { variables: [!lt_1, !lt_0], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_1, b: !lt_0, assumptions: {u32 : !lt_0}, env: Env { variables: [!lt_1, !lt_0], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_1 : !lt_0, via: u32 : !lt_0, assumptions: {u32 : !lt_0}, env: Env { variables: [!lt_1, !lt_0], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_1, b: !lt_0, assumptions: {u32 : !lt_0}, env: Env { variables: [!lt_1, !lt_0], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_1 : !lt_0, via: u32 : !lt_0, assumptions: {u32 : !lt_0}, env: Env { variables: [!lt_1, !lt_0], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_1, b: !lt_0, assumptions: {u32 : !lt_0}, env: Env { variables: [!lt_1, !lt_0], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_1 : !lt_0, via: u32 : !lt_0, assumptions: {u32 : !lt_0}, env: Env { variables: [!lt_1, !lt_0], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_1, b: !lt_0, assumptions: {u32 : !lt_0}, env: Env { variables: [!lt_1, !lt_0], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_0, b: !lt_1, assumptions: {}, env: Env { variables: [!lt_0, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_0, b: !lt_1, assumptions: {}, env: Env { variables: [!lt_0, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_0, b: !lt_1, assumptions: {}, env: Env { variables: [!lt_0, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_0, b: !lt_1, assumptions: {}, env: Env { variables: [!lt_0, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } }"#]]) } /// Upcasting from `'a` to `'b` is allowed because @@ -2475,7 +2601,47 @@ fn undeclared_transitive_universal_region_relationship() { crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_0 : !lt_2, via: !lt_0 : !lt_1, assumptions: {!lt_0 : !lt_1}, env: Env { variables: [!lt_0, !lt_1, !lt_2], bias: Soundness, pending: [], allow_pending_outlives: false } } - crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_0, b: !lt_2, assumptions: {!lt_0 : !lt_1}, env: Env { variables: [!lt_0, !lt_1, !lt_2], bias: Soundness, pending: [], allow_pending_outlives: false } }"#]]) + crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_0, b: !lt_2, assumptions: {!lt_0 : !lt_1}, env: Env { variables: [!lt_0, !lt_1, !lt_2], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_0 : !lt_2, via: !lt_0 : !lt_1, assumptions: {u32 : !lt_0, !lt_0 : !lt_1}, env: Env { variables: [!lt_0, !lt_1, !lt_2], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_0 : !lt_2, via: u32 : !lt_0, assumptions: {u32 : !lt_0, !lt_0 : !lt_1}, env: Env { variables: [!lt_0, !lt_1, !lt_2], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_0, b: !lt_2, assumptions: {u32 : !lt_0, !lt_0 : !lt_1}, env: Env { variables: [!lt_0, !lt_1, !lt_2], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_0 : !lt_2, via: !lt_0 : !lt_1, assumptions: {u32 : !lt_0, !lt_0 : !lt_1}, env: Env { variables: [!lt_0, !lt_1, !lt_2], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_0 : !lt_2, via: u32 : !lt_0, assumptions: {u32 : !lt_0, !lt_0 : !lt_1}, env: Env { variables: [!lt_0, !lt_1, !lt_2], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_0, b: !lt_2, assumptions: {u32 : !lt_0, !lt_0 : !lt_1}, env: Env { variables: [!lt_0, !lt_1, !lt_2], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_0 : !lt_1, via: !lt_0 : !lt_2, assumptions: {u32 : !lt_0, u32 : !lt_1, !lt_0 : !lt_2}, env: Env { variables: [!lt_0, !lt_2, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_0 : !lt_1, via: u32 : !lt_0, assumptions: {u32 : !lt_0, u32 : !lt_1, !lt_0 : !lt_2}, env: Env { variables: [!lt_0, !lt_2, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_0 : !lt_1, via: u32 : !lt_1, assumptions: {u32 : !lt_0, u32 : !lt_1, !lt_0 : !lt_2}, env: Env { variables: [!lt_0, !lt_2, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_0, b: !lt_1, assumptions: {u32 : !lt_0, u32 : !lt_1, !lt_0 : !lt_2}, env: Env { variables: [!lt_0, !lt_2, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_0 : !lt_1, via: !lt_0 : !lt_2, assumptions: {u32 : !lt_0, u32 : !lt_1, !lt_0 : !lt_2}, env: Env { variables: [!lt_0, !lt_2, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_0 : !lt_1, via: u32 : !lt_0, assumptions: {u32 : !lt_0, u32 : !lt_1, !lt_0 : !lt_2}, env: Env { variables: [!lt_0, !lt_2, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_0 : !lt_1, via: u32 : !lt_1, assumptions: {u32 : !lt_0, u32 : !lt_1, !lt_0 : !lt_2}, env: Env { variables: [!lt_0, !lt_2, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_0, b: !lt_1, assumptions: {u32 : !lt_0, u32 : !lt_1, !lt_0 : !lt_2}, env: Env { variables: [!lt_0, !lt_2, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_1 : !lt_0, via: !lt_1 : !lt_2, assumptions: {u32 : !lt_0, !lt_1 : !lt_2}, env: Env { variables: [!lt_1, !lt_2, !lt_0], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_1 : !lt_0, via: u32 : !lt_0, assumptions: {u32 : !lt_0, !lt_1 : !lt_2}, env: Env { variables: [!lt_1, !lt_2, !lt_0], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_1, b: !lt_0, assumptions: {u32 : !lt_0, !lt_1 : !lt_2}, env: Env { variables: [!lt_1, !lt_2, !lt_0], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_1 : !lt_0, via: !lt_1 : !lt_2, assumptions: {u32 : !lt_0, !lt_1 : !lt_2}, env: Env { variables: [!lt_1, !lt_2, !lt_0], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_1 : !lt_0, via: u32 : !lt_0, assumptions: {u32 : !lt_0, !lt_1 : !lt_2}, env: Env { variables: [!lt_1, !lt_2, !lt_0], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_1, b: !lt_0, assumptions: {u32 : !lt_0, !lt_1 : !lt_2}, env: Env { variables: [!lt_1, !lt_2, !lt_0], bias: Soundness, pending: [], allow_pending_outlives: false } }"#]]) } // For `list: &mut Map`, borrow `&mut (*list).value` then assign to `list`. @@ -2985,6 +3151,36 @@ fn if_false_borrowck() { the rule "write-indirect" at (nll.rs) failed because pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `m` + the rule "write-indirect" at (nll.rs) failed because + condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)` + place_accessed = *(m : &!lt_1 mut Map) : <&!lt_1 mut Map as Derefable>::Target + place_loaned_ref = m : &!lt_1 mut Map + + the rule "borrow of disjoint places" at (nll.rs) failed because + condition evaluated to false: `place_disjoint_from_place(&loan.place, &access.place)` + &loan.place = *(m : &!lt_1 mut Map) : <&!lt_1 mut Map as Derefable>::Target + &access.place = *(m : &!lt_1 mut Map) : <&!lt_1 mut Map as Derefable>::Target + + the rule "loan_cannot_outlive" at (nll.rs) failed because + condition evaluated to false: `!outlived_by_loan.contains(&lifetime.upcast())` + outlived_by_loan = {!lt_1, ?lt_2, ?lt_3} + &lifetime.upcast() = !lt_1 + + the rule "loan_not_required_by_universal_regions" at (nll.rs) failed because + condition evaluated to false: `outlived_by_loan.iter().all(|p| match p + { + Parameter::Ty(_) => false, Parameter::Lt(lt) => match lt.as_ref() + { + Lt::Static => false, Lt::Variable(Variable::UniversalVar(_)) => false, + Lt::Variable(Variable::ExistentialVar(_)) => true, + Lt::Variable(Variable::BoundVar(_)) => + panic!("cannot outlive a bound var"), Lt::Erased => true, + }, Parameter::Const(_) => panic!("cannot outlive a constant"), + })` + + the rule "write-indirect" at (nll.rs) failed because + pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `m` + the rule "write-indirect" at (nll.rs) failed because condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)` place_accessed = *(m : &!lt_1 mut Map) : <&!lt_1 mut Map as Derefable>::Target @@ -3140,9 +3336,37 @@ fn call_generic_fn_with_turbofish_missing_relation_upcast() { return r; } }]).borrowck_err(BorrowCheckFailure::All, expect_test::expect![[r#" - crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_0, b: !lt_1, assumptions: {}, env: Env { variables: [!lt_0, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } } + crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_0 : !lt_1, via: u32 : !lt_0, assumptions: {u32 : !lt_0, u32 : !lt_1}, env: Env { variables: [!lt_0, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_0 : !lt_1, via: u32 : !lt_1, assumptions: {u32 : !lt_0, u32 : !lt_1}, env: Env { variables: [!lt_0, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } } - crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_0, b: !lt_1, assumptions: {}, env: Env { variables: [!lt_0, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } }"#]]) + crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_0, b: !lt_1, assumptions: {u32 : !lt_0, u32 : !lt_1}, env: Env { variables: [!lt_0, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_0 : !lt_1, via: u32 : !lt_0, assumptions: {u32 : !lt_0, u32 : !lt_1}, env: Env { variables: [!lt_0, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_0 : !lt_1, via: u32 : !lt_1, assumptions: {u32 : !lt_0, u32 : !lt_1}, env: Env { variables: [!lt_0, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_0, b: !lt_1, assumptions: {u32 : !lt_0, u32 : !lt_1}, env: Env { variables: [!lt_0, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_0 : !lt_1, via: u32 : !lt_0, assumptions: {u32 : !lt_0}, env: Env { variables: [!lt_0, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_0, b: !lt_1, assumptions: {u32 : !lt_0}, env: Env { variables: [!lt_0, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_0 : !lt_1, via: u32 : !lt_0, assumptions: {u32 : !lt_0}, env: Env { variables: [!lt_0, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_0, b: !lt_1, assumptions: {u32 : !lt_0}, env: Env { variables: [!lt_0, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_1 : !lt_0, via: u32 : !lt_0, assumptions: {u32 : !lt_0}, env: Env { variables: [!lt_1, !lt_0], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_1, b: !lt_0, assumptions: {u32 : !lt_0}, env: Env { variables: [!lt_1, !lt_0], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_1 : !lt_0, via: u32 : !lt_0, assumptions: {u32 : !lt_0}, env: Env { variables: [!lt_1, !lt_0], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_1, b: !lt_0, assumptions: {u32 : !lt_0}, env: Env { variables: [!lt_1, !lt_0], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_0, b: !lt_1, assumptions: {}, env: Env { variables: [!lt_0, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_0, b: !lt_1, assumptions: {}, env: Env { variables: [!lt_0, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } }"#]]) } /// Test call to a generic function using turbofish syntax with lifetime and type. @@ -3412,6 +3636,36 @@ fn outlive_before_return_does_not_affect_merged_paths() { the rule "write-indirect" at (nll.rs) failed because pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `a` + the rule "write-indirect" at (nll.rs) failed because + condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)` + place_accessed = *(a : &!lt_1 mut u8) : <&!lt_1 mut u8 as Derefable>::Target + place_loaned_ref = a : &!lt_1 mut u8 + + the rule "borrow of disjoint places" at (nll.rs) failed because + condition evaluated to false: `place_disjoint_from_place(&loan.place, &access.place)` + &loan.place = *(a : &!lt_1 mut u8) : <&!lt_1 mut u8 as Derefable>::Target + &access.place = *(a : &!lt_1 mut u8) : <&!lt_1 mut u8 as Derefable>::Target + + the rule "loan_cannot_outlive" at (nll.rs) failed because + condition evaluated to false: `!outlived_by_loan.contains(&lifetime.upcast())` + outlived_by_loan = {!lt_1, ?lt_2, ?lt_3, ?lt_4, ?lt_5} + &lifetime.upcast() = !lt_1 + + the rule "loan_not_required_by_universal_regions" at (nll.rs) failed because + condition evaluated to false: `outlived_by_loan.iter().all(|p| match p + { + Parameter::Ty(_) => false, Parameter::Lt(lt) => match lt.as_ref() + { + Lt::Static => false, Lt::Variable(Variable::UniversalVar(_)) => false, + Lt::Variable(Variable::ExistentialVar(_)) => true, + Lt::Variable(Variable::BoundVar(_)) => + panic!("cannot outlive a bound var"), Lt::Erased => true, + }, Parameter::Const(_) => panic!("cannot outlive a constant"), + })` + + the rule "write-indirect" at (nll.rs) failed because + pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `a` + the rule "write-indirect" at (nll.rs) failed because condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)` place_accessed = *(a : &!lt_1 mut u8) : <&!lt_1 mut u8 as Derefable>::Target @@ -3673,7 +3927,12 @@ fn reborrow_requires_ref_outlives_loan() { } }]) .skip_execute() - .borrowck_err(BorrowCheckFailure::All, expect_test::expect!["crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_0, b: !lt_1, assumptions: {}, env: Env { variables: [!lt_0, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } }"]); + .borrowck_err(BorrowCheckFailure::All, expect_test::expect![[r#" + crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_0 : !lt_1, via: u32 : !lt_0, assumptions: {u32 : !lt_0}, env: Env { variables: [!lt_0, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_0, b: !lt_1, assumptions: {u32 : !lt_0}, env: Env { variables: [!lt_0, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_0, b: !lt_1, assumptions: {}, env: Env { variables: [!lt_0, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } }"#]]); } #[test] @@ -3866,6 +4125,24 @@ fn issue_63908_remove_last_node_iterative() { the rule "write-indirect" at (nll.rs) failed because pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `cursor` + the rule "write-indirect" at (nll.rs) failed because + condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)` + place_accessed = *(cursor : &?lt_2 mut List) : <&?lt_2 mut List as Derefable>::Target + place_loaned_ref = cursor : &?lt_2 mut List + + the rule "borrow of disjoint places" at (nll.rs) failed because + condition evaluated to false: `place_disjoint_from_place(&loan.place, &access.place)` + &loan.place = *(cursor : &?lt_2 mut List) : <&?lt_2 mut List as Derefable>::Target + &access.place = *(cursor : &?lt_2 mut List) : <&?lt_2 mut List as Derefable>::Target + + the rule "loan_cannot_outlive" at (nll.rs) failed because + condition evaluated to false: `!outlived_by_loan.contains(&lifetime.upcast())` + outlived_by_loan = {?lt_2, ?lt_3} + &lifetime.upcast() = ?lt_2 + + the rule "write-indirect" at (nll.rs) failed because + pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `cursor` + the rule "write-indirect" at (nll.rs) failed because condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)` place_accessed = *(cursor : &?lt_2 mut List) : <&?lt_2 mut List as Derefable>::Target @@ -4300,53 +4577,266 @@ fn issue_46859_decoder_next() { the rule "write-indirect" at (nll.rs) failed because condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)` place_accessed = *(d : &!lt_1 mut Decoder) : <&!lt_1 mut Decoder as Derefable>::Target . buf_read[Decoder , struct] : u32 - place_loaned_ref = d : &!lt_1 mut Decoder"#]]); -} + place_loaned_ref = d : &!lt_1 mut Decoder -/// Port of `tests/ui/nll/polonius/filtering-lending-iterator-issue-92985.rs` -/// (`::next`), which is similar to NLL problem -/// case #3 inside a loop. -/// -/// ```rust,ignore -/// fn next(&mut self) -> Option> { -/// while let Some(item) = self.iter.next() { -/// if (self.predicate)(&item) { -/// return Some(item); -/// } -/// } -/// return None; -/// } -/// ``` -/// -/// `iter_next` models the lending iterator's `next` (the item borrows from -/// the iterator field), `call_predicate` models calling the boxed predicate -/// (a disjoint field), and `no_item` models `return None`. -/// -/// rustc: [nll] error, [polonius] pass, [legacy] pass. -#[test] -fn issue_92985_filtering_lending_iterator() { - FormalityTest::new(crates![crate Foo { - struct Filter { iter: u32, predicate: u32 } + the rule "fixed-point" at (nll.rs) failed because + condition evaluated to false: `state0 == state1` + state0 = flow_state([scope(some(U(1)), None, {}, None, [(d, &!lt_1 mut Decoder)], [d : &!lt_1 mut Decoder]), scope(some(U(1)), None, {}, None, [], []), scope(some(U(3)), None, {}, None, [], []), scope(some(U(3)), Some('l), {}, Some({(* d) . buf_read}), [], [])], point_flow_state({pending_outlives(!lt_1, ?lt_2), pending_outlives(?lt_2, ?lt_3), pending_outlives(?lt_3, !lt_1)}, {}, {}), {}, {}, {pending_outlives(!lt_1, ?lt_2), pending_outlives(?lt_2, ?lt_3), pending_outlives(?lt_3, !lt_1)}) + state1 = flow_state([scope(some(U(1)), None, {}, None, [(d, &!lt_1 mut Decoder)], [d : &!lt_1 mut Decoder]), scope(some(U(1)), None, {}, None, [], []), scope(some(U(3)), None, {}, None, [], []), scope(some(U(3)), Some('l), {}, Some({(* d) . buf_read}), [], [])], point_flow_state({pending_outlives(!lt_1, ?lt_2), pending_outlives(?lt_2, ?lt_3), pending_outlives(?lt_3, !lt_1)}, {loan(?lt_2, *(d : &!lt_1 mut Decoder) : <&!lt_1 mut Decoder as Derefable>::Target . buf_read[Decoder , struct] : u32, mut)}, {}), {}, {}, {pending_outlives(!lt_1, ?lt_2), pending_outlives(?lt_2, ?lt_3), pending_outlives(?lt_3, !lt_1)}) - fn iter_next<'x>(i: &'x mut u32) -> &'x mut u32 { trusted } + the rule "borrow of disjoint places" at (nll.rs) failed because + condition evaluated to false: `place_disjoint_from_place(&loan.place, &access.place)` + &loan.place = *(d : &!lt_1 mut Decoder) : <&!lt_1 mut Decoder as Derefable>::Target . buf_read[Decoder , struct] : u32 + &access.place = *(d : &!lt_1 mut Decoder) : <&!lt_1 mut Decoder as Derefable>::Target . buf_read[Decoder , struct] : u32 - fn call_predicate<'p, 'i>(p: &'p mut u32, item: &'i u32) -> bool { trusted } + the rule "loan_cannot_outlive" at (nll.rs) failed because + condition evaluated to false: `!outlived_by_loan.contains(&lifetime.upcast())` + outlived_by_loan = {!lt_1, ?lt_2, ?lt_3} + &lifetime.upcast() = !lt_1 - fn no_item<'x>() -> &'x mut u32 { trusted } + the rule "loan_not_required_by_universal_regions" at (nll.rs) failed because + condition evaluated to false: `outlived_by_loan.iter().all(|p| match p + { + Parameter::Ty(_) => false, Parameter::Lt(lt) => match lt.as_ref() + { + Lt::Static => false, Lt::Variable(Variable::UniversalVar(_)) => false, + Lt::Variable(Variable::ExistentialVar(_)) => true, + Lt::Variable(Variable::BoundVar(_)) => + panic!("cannot outlive a bound var"), Lt::Erased => true, + }, Parameter::Const(_) => panic!("cannot outlive a constant"), + })` - fn next<'s>(f: &'s mut Filter) -> &'s mut u32 { - exists<'r0, 'r1, 'r2> { - 'l: loop { - let item: &'r0 mut u32 = iter_next::<'r0>(&'r0 mut (*f).iter); - if true { - let keep: bool = call_predicate::<'r1, 'r2>(&'r1 mut (*f).predicate, &'r2 *item); - if keep { - return item; - } else { - } - } else { - break 'l; - } + the rule "write-indirect" at (nll.rs) failed because + pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `*(d : &!lt_1 mut Decoder) : <&!lt_1 mut Decoder as Derefable>::Target . buf_read[Decoder , struct]` + + the rule "write-indirect" at (nll.rs) failed because + pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `d` + + the rule "write-indirect" at (nll.rs) failed because + condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)` + place_accessed = *(d : &!lt_1 mut Decoder) : <&!lt_1 mut Decoder as Derefable>::Target . buf_read[Decoder , struct] : u32 + place_loaned_ref = d : &!lt_1 mut Decoder + + the rule "borrow of disjoint places" at (nll.rs) failed because + condition evaluated to false: `place_disjoint_from_place(&loan.place, &access.place)` + &loan.place = *(d : &!lt_1 mut Decoder) : <&!lt_1 mut Decoder as Derefable>::Target . buf_read[Decoder , struct] : u32 + &access.place = *(d : &!lt_1 mut Decoder) : <&!lt_1 mut Decoder as Derefable>::Target . buf_read[Decoder , struct] : u32 + + the rule "loan_cannot_outlive" at (nll.rs) failed because + condition evaluated to false: `!outlived_by_loan.contains(&lifetime.upcast())` + outlived_by_loan = {!lt_1, ?lt_2, ?lt_3} + &lifetime.upcast() = !lt_1 + + the rule "loan_not_required_by_universal_regions" at (nll.rs) failed because + condition evaluated to false: `outlived_by_loan.iter().all(|p| match p + { + Parameter::Ty(_) => false, Parameter::Lt(lt) => match lt.as_ref() + { + Lt::Static => false, Lt::Variable(Variable::UniversalVar(_)) => false, + Lt::Variable(Variable::ExistentialVar(_)) => true, + Lt::Variable(Variable::BoundVar(_)) => + panic!("cannot outlive a bound var"), Lt::Erased => true, + }, Parameter::Const(_) => panic!("cannot outlive a constant"), + })` + + the rule "write-indirect" at (nll.rs) failed because + pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `*(d : &!lt_1 mut Decoder) : <&!lt_1 mut Decoder as Derefable>::Target . buf_read[Decoder , struct]` + + the rule "write-indirect" at (nll.rs) failed because + pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `d` + + the rule "write-indirect" at (nll.rs) failed because + condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)` + place_accessed = *(d : &!lt_1 mut Decoder) : <&!lt_1 mut Decoder as Derefable>::Target . buf_read[Decoder , struct] : u32 + place_loaned_ref = d : &!lt_1 mut Decoder + + the rule "fixed-point" at (nll.rs) failed because + condition evaluated to false: `state0 == state1` + state0 = flow_state([scope(some(U(1)), None, {}, None, [(d, &!lt_1 mut Decoder)], [d : &!lt_1 mut Decoder]), scope(some(U(1)), None, {}, None, [], []), scope(some(U(3)), None, {}, None, [], []), scope(some(U(3)), Some('l), {}, Some({(* d) . buf_read}), [], [])], point_flow_state({pending_outlives(!lt_1, ?lt_2), pending_outlives(?lt_2, ?lt_3), pending_outlives(?lt_3, !lt_1)}, {}, {}), {}, {}, {pending_outlives(!lt_1, ?lt_2), pending_outlives(?lt_2, ?lt_3), pending_outlives(?lt_3, !lt_1)}) + state1 = flow_state([scope(some(U(1)), None, {}, None, [(d, &!lt_1 mut Decoder)], [d : &!lt_1 mut Decoder]), scope(some(U(1)), None, {}, None, [], []), scope(some(U(3)), None, {}, None, [], []), scope(some(U(3)), Some('l), {}, Some({(* d) . buf_read}), [], [])], point_flow_state({pending_outlives(!lt_1, ?lt_2), pending_outlives(?lt_2, ?lt_3), pending_outlives(?lt_3, !lt_1)}, {loan(?lt_2, *(d : &!lt_1 mut Decoder) : <&!lt_1 mut Decoder as Derefable>::Target . buf_read[Decoder , struct] : u32, mut)}, {}), {}, {}, {pending_outlives(!lt_1, ?lt_2), pending_outlives(?lt_2, ?lt_3), pending_outlives(?lt_3, !lt_1)}) + + the rule "borrow of disjoint places" at (nll.rs) failed because + condition evaluated to false: `place_disjoint_from_place(&loan.place, &access.place)` + &loan.place = *(d : &!lt_1 mut Decoder) : <&!lt_1 mut Decoder as Derefable>::Target . buf_read[Decoder , struct] : u32 + &access.place = *(d : &!lt_1 mut Decoder) : <&!lt_1 mut Decoder as Derefable>::Target . buf_read[Decoder , struct] : u32 + + the rule "loan_cannot_outlive" at (nll.rs) failed because + condition evaluated to false: `!outlived_by_loan.contains(&lifetime.upcast())` + outlived_by_loan = {!lt_1, ?lt_2, ?lt_3} + &lifetime.upcast() = !lt_1 + + the rule "loan_not_required_by_universal_regions" at (nll.rs) failed because + condition evaluated to false: `outlived_by_loan.iter().all(|p| match p + { + Parameter::Ty(_) => false, Parameter::Lt(lt) => match lt.as_ref() + { + Lt::Static => false, Lt::Variable(Variable::UniversalVar(_)) => false, + Lt::Variable(Variable::ExistentialVar(_)) => true, + Lt::Variable(Variable::BoundVar(_)) => + panic!("cannot outlive a bound var"), Lt::Erased => true, + }, Parameter::Const(_) => panic!("cannot outlive a constant"), + })` + + the rule "write-indirect" at (nll.rs) failed because + pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `*(d : &!lt_1 mut Decoder) : <&!lt_1 mut Decoder as Derefable>::Target . buf_read[Decoder , struct]` + + the rule "write-indirect" at (nll.rs) failed because + pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `d` + + the rule "write-indirect" at (nll.rs) failed because + condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)` + place_accessed = *(d : &!lt_1 mut Decoder) : <&!lt_1 mut Decoder as Derefable>::Target . buf_read[Decoder , struct] : u32 + place_loaned_ref = d : &!lt_1 mut Decoder + + the rule "borrow of disjoint places" at (nll.rs) failed because + condition evaluated to false: `place_disjoint_from_place(&loan.place, &access.place)` + &loan.place = *(d : &!lt_1 mut Decoder) : <&!lt_1 mut Decoder as Derefable>::Target . buf_read[Decoder , struct] : u32 + &access.place = *(d : &!lt_1 mut Decoder) : <&!lt_1 mut Decoder as Derefable>::Target . buf_read[Decoder , struct] : u32 + + the rule "loan_cannot_outlive" at (nll.rs) failed because + condition evaluated to false: `!outlived_by_loan.contains(&lifetime.upcast())` + outlived_by_loan = {!lt_1, ?lt_2, ?lt_3} + &lifetime.upcast() = !lt_1 + + the rule "loan_not_required_by_universal_regions" at (nll.rs) failed because + condition evaluated to false: `outlived_by_loan.iter().all(|p| match p + { + Parameter::Ty(_) => false, Parameter::Lt(lt) => match lt.as_ref() + { + Lt::Static => false, Lt::Variable(Variable::UniversalVar(_)) => false, + Lt::Variable(Variable::ExistentialVar(_)) => true, + Lt::Variable(Variable::BoundVar(_)) => + panic!("cannot outlive a bound var"), Lt::Erased => true, + }, Parameter::Const(_) => panic!("cannot outlive a constant"), + })` + + the rule "write-indirect" at (nll.rs) failed because + pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `*(d : &!lt_1 mut Decoder) : <&!lt_1 mut Decoder as Derefable>::Target . buf_read[Decoder , struct]` + + the rule "write-indirect" at (nll.rs) failed because + pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `d` + + the rule "write-indirect" at (nll.rs) failed because + condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)` + place_accessed = *(d : &!lt_1 mut Decoder) : <&!lt_1 mut Decoder as Derefable>::Target . buf_read[Decoder , struct] : u32 + place_loaned_ref = d : &!lt_1 mut Decoder + + the rule "fixed-point" at (nll.rs) failed because + condition evaluated to false: `state0 == state1` + state0 = flow_state([scope(some(U(1)), None, {}, None, [(d, &!lt_1 mut Decoder)], [d : &!lt_1 mut Decoder]), scope(some(U(1)), None, {}, None, [], []), scope(some(U(3)), None, {}, None, [], []), scope(some(U(3)), Some('l), {}, Some({(* d) . buf_read}), [], [])], point_flow_state({pending_outlives(!lt_1, ?lt_2), pending_outlives(?lt_2, ?lt_3), pending_outlives(?lt_3, !lt_1)}, {}, {}), {}, {}, {pending_outlives(!lt_1, ?lt_2), pending_outlives(?lt_2, ?lt_3), pending_outlives(?lt_3, !lt_1)}) + state1 = flow_state([scope(some(U(1)), None, {}, None, [(d, &!lt_1 mut Decoder)], [d : &!lt_1 mut Decoder]), scope(some(U(1)), None, {}, None, [], []), scope(some(U(3)), None, {}, None, [], []), scope(some(U(3)), Some('l), {}, Some({(* d) . buf_read}), [], [])], point_flow_state({pending_outlives(!lt_1, ?lt_2), pending_outlives(?lt_2, ?lt_3), pending_outlives(?lt_3, !lt_1)}, {loan(?lt_2, *(d : &!lt_1 mut Decoder) : <&!lt_1 mut Decoder as Derefable>::Target . buf_read[Decoder , struct] : u32, mut)}, {}), {}, {}, {pending_outlives(!lt_1, ?lt_2), pending_outlives(?lt_2, ?lt_3), pending_outlives(?lt_3, !lt_1)}) + + the rule "borrow of disjoint places" at (nll.rs) failed because + condition evaluated to false: `place_disjoint_from_place(&loan.place, &access.place)` + &loan.place = *(d : &!lt_1 mut Decoder) : <&!lt_1 mut Decoder as Derefable>::Target . buf_read[Decoder , struct] : u32 + &access.place = *(d : &!lt_1 mut Decoder) : <&!lt_1 mut Decoder as Derefable>::Target . buf_read[Decoder , struct] : u32 + + the rule "loan_cannot_outlive" at (nll.rs) failed because + condition evaluated to false: `!outlived_by_loan.contains(&lifetime.upcast())` + outlived_by_loan = {!lt_1, ?lt_2, ?lt_3} + &lifetime.upcast() = !lt_1 + + the rule "loan_not_required_by_universal_regions" at (nll.rs) failed because + condition evaluated to false: `outlived_by_loan.iter().all(|p| match p + { + Parameter::Ty(_) => false, Parameter::Lt(lt) => match lt.as_ref() + { + Lt::Static => false, Lt::Variable(Variable::UniversalVar(_)) => false, + Lt::Variable(Variable::ExistentialVar(_)) => true, + Lt::Variable(Variable::BoundVar(_)) => + panic!("cannot outlive a bound var"), Lt::Erased => true, + }, Parameter::Const(_) => panic!("cannot outlive a constant"), + })` + + the rule "write-indirect" at (nll.rs) failed because + pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `*(d : &!lt_1 mut Decoder) : <&!lt_1 mut Decoder as Derefable>::Target . buf_read[Decoder , struct]` + + the rule "write-indirect" at (nll.rs) failed because + pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `d` + + the rule "write-indirect" at (nll.rs) failed because + condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)` + place_accessed = *(d : &!lt_1 mut Decoder) : <&!lt_1 mut Decoder as Derefable>::Target . buf_read[Decoder , struct] : u32 + place_loaned_ref = d : &!lt_1 mut Decoder + + the rule "borrow of disjoint places" at (nll.rs) failed because + condition evaluated to false: `place_disjoint_from_place(&loan.place, &access.place)` + &loan.place = *(d : &!lt_1 mut Decoder) : <&!lt_1 mut Decoder as Derefable>::Target . buf_read[Decoder , struct] : u32 + &access.place = *(d : &!lt_1 mut Decoder) : <&!lt_1 mut Decoder as Derefable>::Target . buf_read[Decoder , struct] : u32 + + the rule "loan_cannot_outlive" at (nll.rs) failed because + condition evaluated to false: `!outlived_by_loan.contains(&lifetime.upcast())` + outlived_by_loan = {!lt_1, ?lt_2, ?lt_3} + &lifetime.upcast() = !lt_1 + + the rule "loan_not_required_by_universal_regions" at (nll.rs) failed because + condition evaluated to false: `outlived_by_loan.iter().all(|p| match p + { + Parameter::Ty(_) => false, Parameter::Lt(lt) => match lt.as_ref() + { + Lt::Static => false, Lt::Variable(Variable::UniversalVar(_)) => false, + Lt::Variable(Variable::ExistentialVar(_)) => true, + Lt::Variable(Variable::BoundVar(_)) => + panic!("cannot outlive a bound var"), Lt::Erased => true, + }, Parameter::Const(_) => panic!("cannot outlive a constant"), + })` + + the rule "write-indirect" at (nll.rs) failed because + pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `*(d : &!lt_1 mut Decoder) : <&!lt_1 mut Decoder as Derefable>::Target . buf_read[Decoder , struct]` + + the rule "write-indirect" at (nll.rs) failed because + pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `d` + + the rule "write-indirect" at (nll.rs) failed because + condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)` + place_accessed = *(d : &!lt_1 mut Decoder) : <&!lt_1 mut Decoder as Derefable>::Target . buf_read[Decoder , struct] : u32 + place_loaned_ref = d : &!lt_1 mut Decoder"#]]); +} + +/// Port of `tests/ui/nll/polonius/filtering-lending-iterator-issue-92985.rs` +/// (`::next`), which is similar to NLL problem +/// case #3 inside a loop. +/// +/// ```rust,ignore +/// fn next(&mut self) -> Option> { +/// while let Some(item) = self.iter.next() { +/// if (self.predicate)(&item) { +/// return Some(item); +/// } +/// } +/// return None; +/// } +/// ``` +/// +/// `iter_next` models the lending iterator's `next` (the item borrows from +/// the iterator field), `call_predicate` models calling the boxed predicate +/// (a disjoint field), and `no_item` models `return None`. +/// +/// rustc: [nll] error, [polonius] pass, [legacy] pass. +#[test] +fn issue_92985_filtering_lending_iterator() { + FormalityTest::new(crates![crate Foo { + struct Filter { iter: u32, predicate: u32 } + + fn iter_next<'x>(i: &'x mut u32) -> &'x mut u32 { trusted } + + fn call_predicate<'p, 'i>(p: &'p mut u32, item: &'i u32) -> bool { trusted } + + fn no_item<'x>() -> &'x mut u32 { trusted } + + fn next<'s>(f: &'s mut Filter) -> &'s mut u32 { + exists<'r0, 'r1, 'r2> { + 'l: loop { + let item: &'r0 mut u32 = iter_next::<'r0>(&'r0 mut (*f).iter); + if true { + let keep: bool = call_predicate::<'r1, 'r2>(&'r1 mut (*f).predicate, &'r2 *item); + if keep { + return item; + } else { + } + } else { + break 'l; + } } return no_item::<'s>(); } @@ -4420,6 +4910,219 @@ fn issue_92985_filtering_lending_iterator() { the rule "write-indirect" at (nll.rs) failed because pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `f` + the rule "write-indirect" at (nll.rs) failed because + condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)` + place_accessed = *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct] : u32 + place_loaned_ref = f : &!lt_1 mut Filter + + the rule "fixed-point" at (nll.rs) failed because + condition evaluated to false: `state0 == state1` + state0 = flow_state([scope(some(U(1)), None, {}, None, [(f, &!lt_1 mut Filter)], [f : &!lt_1 mut Filter]), scope(some(U(1)), None, {}, None, [], []), scope(some(U(4)), None, {}, None, [], []), scope(some(U(4)), Some('l), {}, Some({(* f) . iter, (* f) . predicate}), [], [])], point_flow_state({pending_outlives(!lt_1, ?lt_2), pending_outlives(!lt_1, ?lt_3), pending_outlives(?lt_2, !lt_1), pending_outlives(?lt_2, ?lt_4)}, {}, {}), {}, {}, {pending_outlives(!lt_1, ?lt_2), pending_outlives(!lt_1, ?lt_3), pending_outlives(?lt_2, !lt_1), pending_outlives(?lt_2, ?lt_4)}) + state1 = flow_state([scope(some(U(1)), None, {}, None, [(f, &!lt_1 mut Filter)], [f : &!lt_1 mut Filter]), scope(some(U(1)), None, {}, None, [], []), scope(some(U(4)), None, {}, None, [], []), scope(some(U(4)), Some('l), {}, Some({(* f) . iter, (* f) . predicate}), [], [])], point_flow_state({pending_outlives(!lt_1, ?lt_2), pending_outlives(!lt_1, ?lt_3), pending_outlives(?lt_2, !lt_1), pending_outlives(?lt_2, ?lt_4)}, {loan(?lt_2, *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct] : u32, mut), loan(?lt_3, *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . predicate[Filter , struct] : u32, mut)}, {}), {labeled_flow_state('l, point_flow_state({pending_outlives(!lt_1, ?lt_2), pending_outlives(!lt_1, ?lt_3), pending_outlives(?lt_2, !lt_1), pending_outlives(?lt_2, ?lt_4)}, {loan(?lt_2, *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct] : u32, mut)}, {}))}, {}, {pending_outlives(!lt_1, ?lt_2), pending_outlives(!lt_1, ?lt_3), pending_outlives(?lt_2, !lt_1), pending_outlives(?lt_2, ?lt_4)}) + + the rule "borrow of disjoint places" at (nll.rs) failed because + condition evaluated to false: `place_disjoint_from_place(&loan.place, &access.place)` + &loan.place = *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct] : u32 + &access.place = *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct] : u32 + + the rule "loan_cannot_outlive" at (nll.rs) failed because + condition evaluated to false: `!outlived_by_loan.contains(&lifetime.upcast())` + outlived_by_loan = {!lt_1, ?lt_2, ?lt_3, ?lt_4} + &lifetime.upcast() = !lt_1 + + the rule "loan_not_required_by_universal_regions" at (nll.rs) failed because + condition evaluated to false: `outlived_by_loan.iter().all(|p| match p + { + Parameter::Ty(_) => false, Parameter::Lt(lt) => match lt.as_ref() + { + Lt::Static => false, Lt::Variable(Variable::UniversalVar(_)) => false, + Lt::Variable(Variable::ExistentialVar(_)) => true, + Lt::Variable(Variable::BoundVar(_)) => + panic!("cannot outlive a bound var"), Lt::Erased => true, + }, Parameter::Const(_) => panic!("cannot outlive a constant"), + })` + + the rule "write-indirect" at (nll.rs) failed because + pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `*(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct]` + + the rule "write-indirect" at (nll.rs) failed because + pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `f` + + the rule "write-indirect" at (nll.rs) failed because + condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)` + place_accessed = *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct] : u32 + place_loaned_ref = f : &!lt_1 mut Filter + + the rule "borrow of disjoint places" at (nll.rs) failed because + condition evaluated to false: `place_disjoint_from_place(&loan.place, &access.place)` + &loan.place = *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct] : u32 + &access.place = *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct] : u32 + + the rule "loan_cannot_outlive" at (nll.rs) failed because + condition evaluated to false: `!outlived_by_loan.contains(&lifetime.upcast())` + outlived_by_loan = {!lt_1, ?lt_2, ?lt_3, ?lt_4} + &lifetime.upcast() = !lt_1 + + the rule "loan_not_required_by_universal_regions" at (nll.rs) failed because + condition evaluated to false: `outlived_by_loan.iter().all(|p| match p + { + Parameter::Ty(_) => false, Parameter::Lt(lt) => match lt.as_ref() + { + Lt::Static => false, Lt::Variable(Variable::UniversalVar(_)) => false, + Lt::Variable(Variable::ExistentialVar(_)) => true, + Lt::Variable(Variable::BoundVar(_)) => + panic!("cannot outlive a bound var"), Lt::Erased => true, + }, Parameter::Const(_) => panic!("cannot outlive a constant"), + })` + + the rule "write-indirect" at (nll.rs) failed because + pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `*(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct]` + + the rule "write-indirect" at (nll.rs) failed because + pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `f` + + the rule "write-indirect" at (nll.rs) failed because + condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)` + place_accessed = *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct] : u32 + place_loaned_ref = f : &!lt_1 mut Filter + + the rule "fixed-point" at (nll.rs) failed because + condition evaluated to false: `state0 == state1` + state0 = flow_state([scope(some(U(1)), None, {}, None, [(f, &!lt_1 mut Filter)], [f : &!lt_1 mut Filter]), scope(some(U(1)), None, {}, None, [], []), scope(some(U(4)), None, {}, None, [], []), scope(some(U(4)), Some('l), {}, Some({(* f) . iter, (* f) . predicate}), [], [])], point_flow_state({pending_outlives(!lt_1, ?lt_2), pending_outlives(!lt_1, ?lt_3), pending_outlives(?lt_2, !lt_1), pending_outlives(?lt_2, ?lt_4)}, {}, {}), {}, {}, {pending_outlives(!lt_1, ?lt_2), pending_outlives(!lt_1, ?lt_3), pending_outlives(?lt_2, !lt_1), pending_outlives(?lt_2, ?lt_4)}) + state1 = flow_state([scope(some(U(1)), None, {}, None, [(f, &!lt_1 mut Filter)], [f : &!lt_1 mut Filter]), scope(some(U(1)), None, {}, None, [], []), scope(some(U(4)), None, {}, None, [], []), scope(some(U(4)), Some('l), {}, Some({(* f) . iter, (* f) . predicate}), [], [])], point_flow_state({pending_outlives(!lt_1, ?lt_2), pending_outlives(!lt_1, ?lt_3), pending_outlives(?lt_2, !lt_1), pending_outlives(?lt_2, ?lt_4)}, {loan(?lt_2, *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct] : u32, mut), loan(?lt_3, *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . predicate[Filter , struct] : u32, mut)}, {}), {labeled_flow_state('l, point_flow_state({pending_outlives(!lt_1, ?lt_2), pending_outlives(!lt_1, ?lt_3), pending_outlives(?lt_2, !lt_1), pending_outlives(?lt_2, ?lt_4)}, {loan(?lt_2, *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct] : u32, mut)}, {}))}, {}, {pending_outlives(!lt_1, ?lt_2), pending_outlives(!lt_1, ?lt_3), pending_outlives(?lt_2, !lt_1), pending_outlives(?lt_2, ?lt_4)}) + + the rule "borrow of disjoint places" at (nll.rs) failed because + condition evaluated to false: `place_disjoint_from_place(&loan.place, &access.place)` + &loan.place = *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct] : u32 + &access.place = *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct] : u32 + + the rule "loan_cannot_outlive" at (nll.rs) failed because + condition evaluated to false: `!outlived_by_loan.contains(&lifetime.upcast())` + outlived_by_loan = {!lt_1, ?lt_2, ?lt_3, ?lt_4} + &lifetime.upcast() = !lt_1 + + the rule "loan_not_required_by_universal_regions" at (nll.rs) failed because + condition evaluated to false: `outlived_by_loan.iter().all(|p| match p + { + Parameter::Ty(_) => false, Parameter::Lt(lt) => match lt.as_ref() + { + Lt::Static => false, Lt::Variable(Variable::UniversalVar(_)) => false, + Lt::Variable(Variable::ExistentialVar(_)) => true, + Lt::Variable(Variable::BoundVar(_)) => + panic!("cannot outlive a bound var"), Lt::Erased => true, + }, Parameter::Const(_) => panic!("cannot outlive a constant"), + })` + + the rule "write-indirect" at (nll.rs) failed because + pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `*(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct]` + + the rule "write-indirect" at (nll.rs) failed because + pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `f` + + the rule "write-indirect" at (nll.rs) failed because + condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)` + place_accessed = *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct] : u32 + place_loaned_ref = f : &!lt_1 mut Filter + + the rule "borrow of disjoint places" at (nll.rs) failed because + condition evaluated to false: `place_disjoint_from_place(&loan.place, &access.place)` + &loan.place = *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct] : u32 + &access.place = *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct] : u32 + + the rule "loan_cannot_outlive" at (nll.rs) failed because + condition evaluated to false: `!outlived_by_loan.contains(&lifetime.upcast())` + outlived_by_loan = {!lt_1, ?lt_2, ?lt_3, ?lt_4} + &lifetime.upcast() = !lt_1 + + the rule "loan_not_required_by_universal_regions" at (nll.rs) failed because + condition evaluated to false: `outlived_by_loan.iter().all(|p| match p + { + Parameter::Ty(_) => false, Parameter::Lt(lt) => match lt.as_ref() + { + Lt::Static => false, Lt::Variable(Variable::UniversalVar(_)) => false, + Lt::Variable(Variable::ExistentialVar(_)) => true, + Lt::Variable(Variable::BoundVar(_)) => + panic!("cannot outlive a bound var"), Lt::Erased => true, + }, Parameter::Const(_) => panic!("cannot outlive a constant"), + })` + + the rule "write-indirect" at (nll.rs) failed because + pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `*(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct]` + + the rule "write-indirect" at (nll.rs) failed because + pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `f` + + the rule "write-indirect" at (nll.rs) failed because + condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)` + place_accessed = *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct] : u32 + place_loaned_ref = f : &!lt_1 mut Filter + + the rule "fixed-point" at (nll.rs) failed because + condition evaluated to false: `state0 == state1` + state0 = flow_state([scope(some(U(1)), None, {}, None, [(f, &!lt_1 mut Filter)], [f : &!lt_1 mut Filter]), scope(some(U(1)), None, {}, None, [], []), scope(some(U(4)), None, {}, None, [], []), scope(some(U(4)), Some('l), {}, Some({(* f) . iter, (* f) . predicate}), [], [])], point_flow_state({pending_outlives(!lt_1, ?lt_2), pending_outlives(!lt_1, ?lt_3), pending_outlives(?lt_2, !lt_1), pending_outlives(?lt_2, ?lt_4)}, {}, {}), {}, {}, {pending_outlives(!lt_1, ?lt_2), pending_outlives(!lt_1, ?lt_3), pending_outlives(?lt_2, !lt_1), pending_outlives(?lt_2, ?lt_4)}) + state1 = flow_state([scope(some(U(1)), None, {}, None, [(f, &!lt_1 mut Filter)], [f : &!lt_1 mut Filter]), scope(some(U(1)), None, {}, None, [], []), scope(some(U(4)), None, {}, None, [], []), scope(some(U(4)), Some('l), {}, Some({(* f) . iter, (* f) . predicate}), [], [])], point_flow_state({pending_outlives(!lt_1, ?lt_2), pending_outlives(!lt_1, ?lt_3), pending_outlives(?lt_2, !lt_1), pending_outlives(?lt_2, ?lt_4)}, {loan(?lt_2, *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct] : u32, mut), loan(?lt_3, *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . predicate[Filter , struct] : u32, mut)}, {}), {labeled_flow_state('l, point_flow_state({pending_outlives(!lt_1, ?lt_2), pending_outlives(!lt_1, ?lt_3), pending_outlives(?lt_2, !lt_1), pending_outlives(?lt_2, ?lt_4)}, {loan(?lt_2, *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct] : u32, mut)}, {}))}, {}, {pending_outlives(!lt_1, ?lt_2), pending_outlives(!lt_1, ?lt_3), pending_outlives(?lt_2, !lt_1), pending_outlives(?lt_2, ?lt_4)}) + + the rule "borrow of disjoint places" at (nll.rs) failed because + condition evaluated to false: `place_disjoint_from_place(&loan.place, &access.place)` + &loan.place = *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct] : u32 + &access.place = *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct] : u32 + + the rule "loan_cannot_outlive" at (nll.rs) failed because + condition evaluated to false: `!outlived_by_loan.contains(&lifetime.upcast())` + outlived_by_loan = {!lt_1, ?lt_2, ?lt_3, ?lt_4} + &lifetime.upcast() = !lt_1 + + the rule "loan_not_required_by_universal_regions" at (nll.rs) failed because + condition evaluated to false: `outlived_by_loan.iter().all(|p| match p + { + Parameter::Ty(_) => false, Parameter::Lt(lt) => match lt.as_ref() + { + Lt::Static => false, Lt::Variable(Variable::UniversalVar(_)) => false, + Lt::Variable(Variable::ExistentialVar(_)) => true, + Lt::Variable(Variable::BoundVar(_)) => + panic!("cannot outlive a bound var"), Lt::Erased => true, + }, Parameter::Const(_) => panic!("cannot outlive a constant"), + })` + + the rule "write-indirect" at (nll.rs) failed because + pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `*(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct]` + + the rule "write-indirect" at (nll.rs) failed because + pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `f` + + the rule "write-indirect" at (nll.rs) failed because + condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)` + place_accessed = *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct] : u32 + place_loaned_ref = f : &!lt_1 mut Filter + + the rule "borrow of disjoint places" at (nll.rs) failed because + condition evaluated to false: `place_disjoint_from_place(&loan.place, &access.place)` + &loan.place = *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct] : u32 + &access.place = *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct] : u32 + + the rule "loan_cannot_outlive" at (nll.rs) failed because + condition evaluated to false: `!outlived_by_loan.contains(&lifetime.upcast())` + outlived_by_loan = {!lt_1, ?lt_2, ?lt_3, ?lt_4} + &lifetime.upcast() = !lt_1 + + the rule "loan_not_required_by_universal_regions" at (nll.rs) failed because + condition evaluated to false: `outlived_by_loan.iter().all(|p| match p + { + Parameter::Ty(_) => false, Parameter::Lt(lt) => match lt.as_ref() + { + Lt::Static => false, Lt::Variable(Variable::UniversalVar(_)) => false, + Lt::Variable(Variable::ExistentialVar(_)) => true, + Lt::Variable(Variable::BoundVar(_)) => + panic!("cannot outlive a bound var"), Lt::Erased => true, + }, Parameter::Const(_) => panic!("cannot outlive a constant"), + })` + + the rule "write-indirect" at (nll.rs) failed because + pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `*(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct]` + + the rule "write-indirect" at (nll.rs) failed because + pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `f` + the rule "write-indirect" at (nll.rs) failed because condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)` place_accessed = *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct] : u32 diff --git a/tests/implied_bounds.rs b/tests/implied_bounds.rs new file mode 100644 index 000000000..235998ad8 --- /dev/null +++ b/tests/implied_bounds.rs @@ -0,0 +1,81 @@ +use a_mir_formality::{crates, FormalityTest}; + +#[formality_core::test] +fn nested_borrow() { + FormalityTest::new(crates![crate Foo { + fn foo<'a, 'b>(x: &'a &'b u32) -> &'a &'b u32 + { + exists<> { + return x; + } + } + }]) + .skip_execute() + .ok() +} + +#[formality_core::test] +fn extra_nested_borrow() { + FormalityTest::new(crates![crate Foo { + fn foo<'a, 'b, 'c>(x: &'a &'b &'c u32) -> &'a &'b &'c u32 + { + exists<> { + return x; + } + } + }]) + .skip_execute() + .ok() +} + +#[formality_core::test] +fn indirect_nested_borrow() { + FormalityTest::new(crates![crate Foo { + fn foo<'a, 'b, 'c, 'd>(x: &'a &'b u32) -> &'c &'d u32 + where + 'a : 'c, + 'b : 'd + + { + exists<> { + return x; + } + } + }]) + .skip_execute() + .ok() +} + +#[test] +fn lifetime() { + FormalityTest::new(crates![crate Foo { + // fn one_lt_arg<'a, T>(_: &'a T) -> () {} + fn one_lt_arg<'a, T>(v0: &'a T) -> () + { trusted } + }]) + .skip_execute() + .ok() +} + +#[test] +#[ignore = "to be resolved by (#437)"] +fn implied_bound_for_normalized_ty() { + FormalityTest::new(crates![ + crate core { + trait A<'a> { + type Assoc : []; + } + impl<'a, T> A<'a> for T where T: 'a { + type Assoc = &'a T; + } + + fn outlives<'a, T>() -> () where T : 'a {} + + fn test<'a, T>(_: >::Assoc) -> () { + outlives::<'a, T>(); + } + } + ]) + .skip_execute() + .ok(); +} diff --git a/tests/references.rs b/tests/references.rs index 2f53e43e1..91294ac30 100644 --- a/tests/references.rs +++ b/tests/references.rs @@ -17,6 +17,21 @@ fn recursive_reference_validity() { crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: Trait(!ty_0), via: !ty_0 : !lt_1, assumptions: {!ty_0 : !lt_1}, env: Env { variables: [!lt_1, !ty_0], bias: Soundness, pending: [], allow_pending_outlives: false } } + the rule "trait implied bound" at (prove_wc.rs) failed because + expression evaluated to an empty collection: `decls.trait_invariants()` + + crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: @ wf(&!lt_1 A), via: !ty_0 : !lt_1, assumptions: {A : !lt_1, !ty_0 : !lt_1}, env: Env { variables: [!lt_1, !ty_0], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: @ wf(&!lt_1 A), via: A : !lt_1, assumptions: {A : !lt_1, !ty_0 : !lt_1}, env: Env { variables: [!lt_1, !ty_0], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: @ wf(A), via: !ty_0 : !lt_1, assumptions: {A : !lt_1, !ty_0 : !lt_1}, env: Env { variables: [!lt_1, !ty_0], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: @ wf(A), via: A : !lt_1, assumptions: {A : !lt_1, !ty_0 : !lt_1}, env: Env { variables: [!lt_1, !ty_0], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: Trait(!ty_0), via: !ty_0 : !lt_1, assumptions: {A : !lt_1, !ty_0 : !lt_1}, env: Env { variables: [!lt_1, !ty_0], bias: Soundness, pending: [], allow_pending_outlives: false } } + + crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: Trait(!ty_0), via: A : !lt_1, assumptions: {A : !lt_1, !ty_0 : !lt_1}, env: Env { variables: [!lt_1, !ty_0], bias: Soundness, pending: [], allow_pending_outlives: false } } + the rule "trait implied bound" at (prove_wc.rs) failed because expression evaluated to an empty collection: `decls.trait_invariants()`"#]]); }