UPDATE_EXPECT=1

Author: nikomatsakis

src/test/coherence_orphan.rs

@@ -25,7 +25,7 @@ fn u32_not_u32_impls() {
             Caused by:
                 judgment `negation_via_failure` failed at the following rule(s):
                   failed at (src/file.rs:LL:CC) because
-                    found an unconditionally true solution Constraints { env: Env { variables: [], bias: Completeness }, known_true: true, substitution: {} }"#]]
+                    found an unconditionally true solution Constraints { env: Env { variables: [], bias: Completeness, pending: [] }, known_true: true, substitution: {} }"#]]
     )
 }
 
@@ -103,7 +103,7 @@ fn T_where_Foo_not_u32_impls() {
             check_trait_impl(impl <ty> Foo for ^ty0_0 where ^ty0_0 : Foo { })
 
             Caused by:
-                failed to prove {! Foo(!ty_1)} given {Foo(!ty_1)}, got {Constraints { env: Env { variables: [!ty_1], bias: Soundness }, known_true: false, substitution: {} }}"#]]
+                failed to prove {! Foo(!ty_1)} given {Foo(!ty_1)}, got {Constraints { env: Env { variables: [!ty_1], bias: Soundness, pending: [] }, known_true: false, substitution: {} }}"#]]
     )
 }
 

src/test/coherence_overlap.rs

@@ -18,27 +18,27 @@ fn nonsense_rigid_const_bound() {
 
             Caused by:
                 0: prove_where_clauses_well_formed([type_of_const value(0, bool) is u32])
-                1: judgment `prove { goal: {u32 = bool, @ wf(u32), @ wf(const value(0, bool))}, assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo <ty> where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], {Foo}, {}) }` failed at the following rule(s):
+                1: judgment `prove { goal: {u32 = bool, @ wf(u32), @ wf(const value(0, bool))}, assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], bias: Soundness, pending: [] }, decls: decls(222, [trait Foo <ty> where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], {Foo}, {}) }` failed at the following rule(s):
                      failed at (src/file.rs:LL:CC) because
-                       judgment `prove_wc_list { goal: {u32 = bool, @ wf(u32), @ wf(const value(0, bool))}, assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s):
+                       judgment `prove_wc_list { goal: {u32 = bool, @ wf(u32), @ wf(const value(0, bool))}, assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], bias: Soundness, pending: [] } }` failed at the following rule(s):
                          the rule "some" failed at step #0 (src/file.rs:LL:CC) because
-                           judgment `prove_wc { goal: u32 = bool, assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s):
+                           judgment `prove_wc { goal: u32 = bool, assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], bias: Soundness, pending: [] } }` failed at the following rule(s):
                              the rule "assumption - relation" failed at step #1 (src/file.rs:LL:CC) because
-                               judgment had no applicable rules: `prove_via { goal: u32 = bool, via: @ ConstHasType(value(0, bool) , u32), assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], bias: Soundness } }`
+                               judgment had no applicable rules: `prove_via { goal: u32 = bool, via: @ ConstHasType(value(0, bool) , u32), assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], bias: Soundness, pending: [] } }`
                              the rule "eq" failed at step #0 (src/file.rs:LL:CC) because
-                               judgment `prove_eq { a: u32, b: bool, assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s):
+                               judgment `prove_eq { a: u32, b: bool, assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], bias: Soundness, pending: [] } }` failed at the following rule(s):
                                  the rule "normalize-l" failed at step #0 (src/file.rs:LL:CC) because
-                                   judgment `prove_normalize { p: u32, assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s):
+                                   judgment `prove_normalize { p: u32, assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], bias: Soundness, pending: [] } }` failed at the following rule(s):
                                      the rule "normalize-via-assumption" failed at step #1 (src/file.rs:LL:CC) because
-                                       judgment had no applicable rules: `prove_normalize_via { goal: u32, via: @ ConstHasType(value(0, bool) , u32), assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], bias: Soundness } }`
+                                       judgment had no applicable rules: `prove_normalize_via { goal: u32, via: @ ConstHasType(value(0, bool) , u32), assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], bias: Soundness, pending: [] } }`
                                  the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because
-                                   judgment `prove_eq { a: bool, b: u32, assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s):
+                                   judgment `prove_eq { a: bool, b: u32, assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], bias: Soundness, pending: [] } }` failed at the following rule(s):
                                      the rule "normalize-l" failed at step #0 (src/file.rs:LL:CC) because
-                                       judgment `prove_normalize { p: bool, assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s):
+                                       judgment `prove_normalize { p: bool, assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], bias: Soundness, pending: [] } }` failed at the following rule(s):
                                          the rule "normalize-via-assumption" failed at step #1 (src/file.rs:LL:CC) because
-                                           judgment had no applicable rules: `prove_normalize_via { goal: bool, via: @ ConstHasType(value(0, bool) , u32), assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], bias: Soundness } }`
+                                           judgment had no applicable rules: `prove_normalize_via { goal: bool, via: @ ConstHasType(value(0, bool) , u32), assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], bias: Soundness, pending: [] } }`
                                      the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because
-                                       cyclic proof attempt: `prove_eq { a: u32, b: bool, assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], bias: Soundness } }`"#]]
+                                       cyclic proof attempt: `prove_eq { a: u32, b: bool, assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], bias: Soundness, pending: [] } }`"#]]
     )
 }
 
@@ -76,11 +76,11 @@ fn mismatch() {
             check_trait_impl(impl Foo <const value(42, u32)> for u32 { })
 
             Caused by:
-                judgment `prove { goal: {Foo(u32, const value(42, u32))}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo <ty, const> where {@ ConstHasType(^const0_1 , bool)}], [impl Foo(u32, const value(42, u32))], [], [], [], [], {Foo}, {}) }` failed at the following rule(s):
+                judgment `prove { goal: {Foo(u32, const value(42, u32))}, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] }, decls: decls(222, [trait Foo <ty, const> where {@ ConstHasType(^const0_1 , bool)}], [impl Foo(u32, const value(42, u32))], [], [], [], [], {Foo}, {}) }` failed at the following rule(s):
                   failed at (src/file.rs:LL:CC) because
-                    judgment `prove_wc_list { goal: {Foo(u32, const value(42, u32))}, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s):
+                    judgment `prove_wc_list { goal: {Foo(u32, const value(42, u32))}, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] } }` failed at the following rule(s):
                       the rule "some" failed at step #0 (src/file.rs:LL:CC) because
-                        judgment `prove_wc { goal: Foo(u32, const value(42, u32)), assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s):
+                        judgment `prove_wc { goal: Foo(u32, const value(42, u32)), assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] } }` failed at the following rule(s):
                           the rule "trait implied bound" failed at step #0 (src/file.rs:LL:CC) because
                             expression evaluated to an empty collection: `decls.trait_invariants()`"#]]
     )
@@ -135,19 +135,19 @@ fn generic_mismatch() {
             check_trait_impl(impl <const> Foo <const ^const0_0> for u32 where type_of_const ^const0_0 is u32 { })
 
             Caused by:
-                judgment `prove { goal: {Foo(u32, const !const_0)}, assumptions: {@ ConstHasType(!const_0 , u32)}, env: Env { variables: [!const_0], bias: Soundness }, decls: decls(222, [trait Foo <ty, const> where {@ ConstHasType(^const0_1 , bool)}], [impl <const> Foo(u32, const ^const0_0) where {@ ConstHasType(^const0_0 , u32)}], [], [], [], [], {Foo}, {}) }` failed at the following rule(s):
+                judgment `prove { goal: {Foo(u32, const !const_0)}, assumptions: {@ ConstHasType(!const_0 , u32)}, env: Env { variables: [!const_0], bias: Soundness, pending: [] }, decls: decls(222, [trait Foo <ty, const> where {@ ConstHasType(^const0_1 , bool)}], [impl <const> Foo(u32, const ^const0_0) where {@ ConstHasType(^const0_0 , u32)}], [], [], [], [], {Foo}, {}) }` failed at the following rule(s):
                   failed at (src/file.rs:LL:CC) because
-                    judgment `prove_wc_list { goal: {Foo(u32, const !const_0)}, assumptions: {@ ConstHasType(!const_0 , u32)}, env: Env { variables: [!const_0], bias: Soundness } }` failed at the following rule(s):
+                    judgment `prove_wc_list { goal: {Foo(u32, const !const_0)}, assumptions: {@ ConstHasType(!const_0 , u32)}, env: Env { variables: [!const_0], bias: Soundness, pending: [] } }` failed at the following rule(s):
                       the rule "some" failed at step #0 (src/file.rs:LL:CC) because
-                        judgment `prove_wc { goal: Foo(u32, const !const_0), assumptions: {@ ConstHasType(!const_0 , u32)}, env: Env { variables: [!const_0], bias: Soundness } }` failed at the following rule(s):
+                        judgment `prove_wc { goal: Foo(u32, const !const_0), assumptions: {@ ConstHasType(!const_0 , u32)}, env: Env { variables: [!const_0], bias: Soundness, pending: [] } }` failed at the following rule(s):
                           the rule "positive impl" failed at step #7 (src/file.rs:LL:CC) because
-                            judgment `prove_after { constraints: Constraints { env: Env { variables: [!const_0, ?const_1], bias: Soundness }, known_true: true, substitution: {?const_1 => const !const_0} }, goal: {@ ConstHasType(?const_1 , bool)}, assumptions: {@ ConstHasType(!const_0 , u32)} }` failed at the following rule(s):
+                            judgment `prove_after { constraints: Constraints { env: Env { variables: [!const_0, ?const_1], bias: Soundness, pending: [] }, known_true: true, substitution: {?const_1 => const !const_0} }, goal: {@ ConstHasType(?const_1 , bool)}, assumptions: {@ ConstHasType(!const_0 , u32)} }` failed at the following rule(s):
                               the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because
-                                judgment `prove { goal: {@ ConstHasType(!const_0 , bool)}, assumptions: {@ ConstHasType(!const_0 , u32)}, env: Env { variables: [!const_0], bias: Soundness }, decls: decls(222, [trait Foo <ty, const> where {@ ConstHasType(^const0_1 , bool)}], [impl <const> Foo(u32, const ^const0_0) where {@ ConstHasType(^const0_0 , u32)}], [], [], [], [], {Foo}, {}) }` failed at the following rule(s):
+                                judgment `prove { goal: {@ ConstHasType(!const_0 , bool)}, assumptions: {@ ConstHasType(!const_0 , u32)}, env: Env { variables: [!const_0], bias: Soundness, pending: [] }, decls: decls(222, [trait Foo <ty, const> where {@ ConstHasType(^const0_1 , bool)}], [impl <const> Foo(u32, const ^const0_0) where {@ ConstHasType(^const0_0 , u32)}], [], [], [], [], {Foo}, {}) }` failed at the following rule(s):
                                   failed at (src/file.rs:LL:CC) because
-                                    judgment `prove_wc_list { goal: {@ ConstHasType(!const_0 , bool)}, assumptions: {@ ConstHasType(!const_0 , u32)}, env: Env { variables: [!const_0], bias: Soundness } }` failed at the following rule(s):
+                                    judgment `prove_wc_list { goal: {@ ConstHasType(!const_0 , bool)}, assumptions: {@ ConstHasType(!const_0 , u32)}, env: Env { variables: [!const_0], bias: Soundness, pending: [] } }` failed at the following rule(s):
                                       the rule "some" failed at step #0 (src/file.rs:LL:CC) because
-                                        judgment `prove_wc { goal: @ ConstHasType(!const_0 , bool), assumptions: {@ ConstHasType(!const_0 , u32)}, env: Env { variables: [!const_0], bias: Soundness } }` failed at the following rule(s):
+                                        judgment `prove_wc { goal: @ ConstHasType(!const_0 , bool), assumptions: {@ ConstHasType(!const_0 , u32)}, env: Env { variables: [!const_0], bias: Soundness, pending: [] } }` failed at the following rule(s):
                                           the rule "const has ty" failed at step #0 (src/file.rs:LL:CC) because
                                             pattern `Some((_, const_ty))` did not match value `None`
                           the rule "trait implied bound" failed at step #0 (src/file.rs:LL:CC) because

src/test/consts.rs

@@ -42,12 +42,12 @@ fn lifetime() {
         [ /* TODO */ ]
 
         expect_test::expect![[r#"
-            judgment `prove { goal: {@ wf(&!lt_0 !ty_1)}, assumptions: {}, env: Env { variables: [!lt_0, !ty_1], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s):
+            judgment `prove { goal: {@ wf(&!lt_0 !ty_1)}, assumptions: {}, env: Env { variables: [!lt_0, !ty_1], bias: Soundness, pending: [] }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s):
               failed at (src/file.rs:LL:CC) because
-                judgment `prove_wc_list { goal: {@ wf(&!lt_0 !ty_1)}, assumptions: {}, env: Env { variables: [!lt_0, !ty_1], bias: Soundness } }` failed at the following rule(s):
+                judgment `prove_wc_list { goal: {@ wf(&!lt_0 !ty_1)}, assumptions: {}, env: Env { variables: [!lt_0, !ty_1], bias: Soundness, pending: [] } }` failed at the following rule(s):
                   the rule "some" failed at step #0 (src/file.rs:LL:CC) because
-                    judgment `prove_wc { goal: @ wf(&!lt_0 !ty_1), assumptions: {}, env: Env { variables: [!lt_0, !ty_1], bias: Soundness } }` failed at the following rule(s):
+                    judgment `prove_wc { goal: @ wf(&!lt_0 !ty_1), assumptions: {}, env: Env { variables: [!lt_0, !ty_1], bias: Soundness, pending: [] } }` failed at the following rule(s):
                       the rule "parameter well formed" failed at step #0 (src/file.rs:LL:CC) because
-                        judgment had no applicable rules: `prove_wf { goal: &!lt_0 !ty_1, assumptions: {}, env: Env { variables: [!lt_0, !ty_1], bias: Soundness } }`"#]]
+                        judgment had no applicable rules: `prove_wf { goal: &!lt_0 !ty_1, assumptions: {}, env: Env { variables: [!lt_0, !ty_1], bias: Soundness, pending: [] } }`"#]]
     )
 }