remove some distracting errors

still room to do better!

Author: nikomatsakis

crates/formality-prove/src/prove/prove_normalize.rs

@@ -23,7 +23,7 @@ judgment_fn! {
         debug(p, assumptions, env, decls)
 
         (
-            (&assumptions => a)
+            (&assumptions => a)!
             (prove_normalize_via(&decls, &env, &assumptions, a, &goal) => c)
             ----------------------------- ("normalize-via-assumption")
             (prove_normalize(decls, env, assumptions, goal) => c)

crates/formality-prove/src/prove/prove_via.rs

@@ -28,8 +28,8 @@ judgment_fn! {
         (
             (let (skel_c, parameters_c) = relation.debone())
             (let (skel_g, parameters_g) = goal.debone())
-            (if skel_c == skel_g)!
-            (if parameters_c == parameters_g) // for relations, we require 100% match
+            (if skel_c == skel_g)
+            (if parameters_c == parameters_g)! // for relations, we require 100% match
             ----------------------------- ("relation-axiom")
             (prove_via(_decls, env, _assumptions, PR::Relation(relation), goal) => Constraints::none(env))
         )

crates/formality-prove/src/test/eq_assumptions.rs

@@ -59,10 +59,6 @@ fn test_normalize_assoc_ty_existential0() {
                 judgment `prove_wc { goal: if {<!ty_1 as Iterator>::Item = u32} <?ty_0 as Iterator>::Item = u32, assumptions: {}, env: Env { variables: [?ty_0, !ty_1], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s):
                   the rule "implies" failed at step #0 (src/file.rs:LL:CC) because
                     judgment `prove_wc { goal: <?ty_0 as Iterator>::Item = u32, assumptions: {<!ty_1 as Iterator>::Item = u32}, env: Env { variables: [?ty_0, !ty_1], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s):
-                      the rule "assumption" failed at step #1 (src/file.rs:LL:CC) because
-                        judgment `prove_via { goal: <?ty_0 as Iterator>::Item = u32, via: <!ty_1 as Iterator>::Item = u32, assumptions: {<!ty_1 as Iterator>::Item = u32}, env: Env { variables: [?ty_0, !ty_1], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s):
-                          the rule "relation-axiom" failed at step #3 (src/file.rs:LL:CC) because
-                            condition evaluted to false: `parameters_c == parameters_g`
                       the rule "eq" failed at step #0 (src/file.rs:LL:CC) because
                         judgment `prove_eq { a: <?ty_0 as Iterator>::Item, b: u32, assumptions: {<!ty_1 as Iterator>::Item = u32}, env: Env { variables: [?ty_0, !ty_1], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s):
                           the rule "normalize-l" failed at step #0 (src/file.rs:LL:CC) because
@@ -101,20 +97,12 @@ fn test_normalize_assoc_ty_existential0() {
                                     judgment `prove_wc_list { goal: {<!ty_0 as Iterator>::Item = <?ty_1 as Iterator>::Item}, assumptions: {<!ty_0 as Iterator>::Item = u32}, env: Env { variables: [?ty_1, !ty_0], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s):
                                       the rule "some" failed at step #0 (src/file.rs:LL:CC) because
                                         judgment `prove_wc { goal: <!ty_0 as Iterator>::Item = <?ty_1 as Iterator>::Item, assumptions: {<!ty_0 as Iterator>::Item = u32}, env: Env { variables: [?ty_1, !ty_0], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s):
-                                          the rule "assumption" failed at step #1 (src/file.rs:LL:CC) because
-                                            judgment `prove_via { goal: <!ty_0 as Iterator>::Item = <?ty_1 as Iterator>::Item, via: <!ty_0 as Iterator>::Item = u32, assumptions: {<!ty_0 as Iterator>::Item = u32}, env: Env { variables: [?ty_1, !ty_0], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s):
-                                              the rule "relation-axiom" failed at step #3 (src/file.rs:LL:CC) because
-                                                condition evaluted to false: `parameters_c == parameters_g`
                                           the rule "eq" failed at step #0 (src/file.rs:LL:CC) because
                                             judgment `prove_eq { a: <!ty_0 as Iterator>::Item, b: <?ty_1 as Iterator>::Item, assumptions: {<!ty_0 as Iterator>::Item = u32}, env: Env { variables: [?ty_1, !ty_0], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s):
                                               the rule "alias" failed at step #3 (src/file.rs:LL:CC) because
                                                 judgment `prove_wc_list { goal: {!ty_0 = ?ty_1}, assumptions: {<!ty_0 as Iterator>::Item = u32}, env: Env { variables: [?ty_1, !ty_0], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s):
                                                   the rule "some" failed at step #0 (src/file.rs:LL:CC) because
                                                     judgment `prove_wc { goal: !ty_0 = ?ty_1, assumptions: {<!ty_0 as Iterator>::Item = u32}, env: Env { variables: [?ty_1, !ty_0], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s):
-                                                      the rule "assumption" failed at step #1 (src/file.rs:LL:CC) because
-                                                        judgment `prove_via { goal: !ty_0 = ?ty_1, via: <!ty_0 as Iterator>::Item = u32, assumptions: {<!ty_0 as Iterator>::Item = u32}, env: Env { variables: [?ty_1, !ty_0], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s):
-                                                          the rule "relation-axiom" failed at step #3 (src/file.rs:LL:CC) because
-                                                            condition evaluted to false: `parameters_c == parameters_g`
                                                       the rule "eq" failed at step #0 (src/file.rs:LL:CC) because
                                                         judgment `prove_eq { a: !ty_0, b: ?ty_1, assumptions: {<!ty_0 as Iterator>::Item = u32}, env: Env { variables: [?ty_1, !ty_0], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s):
                                                           the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because
@@ -131,10 +119,6 @@ fn test_normalize_assoc_ty_existential0() {
                                                     judgment `prove_wc_list { goal: {u32 = <?ty_1 as Iterator>::Item}, assumptions: {<!ty_0 as Iterator>::Item = u32}, env: Env { variables: [?ty_1, !ty_0], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s):
                                                       the rule "some" failed at step #0 (src/file.rs:LL:CC) because
                                                         judgment `prove_wc { goal: u32 = <?ty_1 as Iterator>::Item, assumptions: {<!ty_0 as Iterator>::Item = u32}, env: Env { variables: [?ty_1, !ty_0], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s):
-                                                          the rule "assumption" failed at step #1 (src/file.rs:LL:CC) because
-                                                            judgment `prove_via { goal: u32 = <?ty_1 as Iterator>::Item, via: <!ty_0 as Iterator>::Item = u32, assumptions: {<!ty_0 as Iterator>::Item = u32}, env: Env { variables: [?ty_1, !ty_0], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s):
-                                                              the rule "relation-axiom" failed at step #3 (src/file.rs:LL:CC) because
-                                                                condition evaluted to false: `parameters_c == parameters_g`
                                                           the rule "eq" failed at step #0 (src/file.rs:LL:CC) because
                                                             judgment `prove_eq { a: u32, b: <?ty_1 as Iterator>::Item, assumptions: {<!ty_0 as Iterator>::Item = u32}, env: Env { variables: [?ty_1, !ty_0], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s):
                                                               the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because
@@ -173,10 +157,6 @@ fn test_normalize_assoc_ty_existential0() {
                                                     judgment `prove_wc_list { goal: {?ty_1 = !ty_0}, assumptions: {<!ty_0 as Iterator>::Item = u32}, env: Env { variables: [?ty_1, !ty_0], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s):
                                                       the rule "some" failed at step #0 (src/file.rs:LL:CC) because
                                                         judgment `prove_wc { goal: ?ty_1 = !ty_0, assumptions: {<!ty_0 as Iterator>::Item = u32}, env: Env { variables: [?ty_1, !ty_0], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s):
-                                                          the rule "assumption" failed at step #1 (src/file.rs:LL:CC) because
-                                                            judgment `prove_via { goal: ?ty_1 = !ty_0, via: <!ty_0 as Iterator>::Item = u32, assumptions: {<!ty_0 as Iterator>::Item = u32}, env: Env { variables: [?ty_1, !ty_0], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s):
-                                                              the rule "relation-axiom" failed at step #3 (src/file.rs:LL:CC) because
-                                                                condition evaluted to false: `parameters_c == parameters_g`
                                                           the rule "eq" failed at step #0 (src/file.rs:LL:CC) because
                                                             judgment `prove_eq { a: ?ty_1, b: !ty_0, assumptions: {<!ty_0 as Iterator>::Item = u32}, env: Env { variables: [?ty_1, !ty_0], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s):
                                                               the rule "existential" failed at step #0 (src/file.rs:LL:CC) because

crates/formality-prove/src/test/is_local.rs

@@ -20,12 +20,6 @@ fn test_forall_not_local() {
                 judgment `prove_wc { goal: @ IsLocal(Debug(!ty_1)), assumptions: {}, env: Env { variables: [!ty_1], coherence_mode: true }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s):
                   the rule "trait ref is local" failed at step #0 (src/file.rs:LL:CC) because
                     judgment `is_local_trait_ref { goal: Debug(!ty_1), assumptions: {}, env: Env { variables: [!ty_1], coherence_mode: true }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s):
-                      the rule "local parameter" failed at step #1 (src/file.rs:LL:CC) because
-                        judgment `is_local_parameter { goal: !ty_1, assumptions: {}, env: Env { variables: [!ty_1], coherence_mode: true }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s):
-                          the rule "local parameter" failed at step #0 (src/file.rs:LL:CC) because
-                            judgment `prove_normalize { p: !ty_1, assumptions: {}, env: Env { variables: [!ty_1], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s):
-                              the rule "normalize-via-assumption" failed at step #0 (src/file.rs:LL:CC) because
-                                expression evaluated to an empty collection: `&assumptions`
                       the rule "local trait" failed at step #0 (src/file.rs:LL:CC) because
                         condition evaluted to false: `decls.is_local_trait_id(&goal.trait_id)`
     "#]]);

crates/formality-prove/src/test/occurs_check.rs

@@ -31,16 +31,6 @@ fn direct_cycle() {
                                 judgment `equate_variable` failed at the following rule(s):
                                   failed at (src/file.rs:LL:CC) because
                                     `?ty_0` occurs in `Vec<?ty_0>`
-                          the rule "normalize-l" failed at step #0 (src/file.rs:LL:CC) because
-                            judgment `prove_normalize { p: ?ty_0, assumptions: {}, env: Env { variables: [?ty_0], coherence_mode: false }, decls: decls(222, [trait Foo <ty> ], [impl <ty> Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s):
-                              the rule "normalize-via-assumption" failed at step #0 (src/file.rs:LL:CC) because
-                                expression evaluated to an empty collection: `&assumptions`
-                          the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because
-                            judgment `prove_eq { a: Vec<?ty_0>, b: ?ty_0, assumptions: {}, env: Env { variables: [?ty_0], coherence_mode: false }, decls: decls(222, [trait Foo <ty> ], [impl <ty> Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s):
-                              the rule "normalize-l" failed at step #0 (src/file.rs:LL:CC) because
-                                judgment `prove_normalize { p: Vec<?ty_0>, assumptions: {}, env: Env { variables: [?ty_0], coherence_mode: false }, decls: decls(222, [trait Foo <ty> ], [impl <ty> Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s):
-                                  the rule "normalize-via-assumption" failed at step #0 (src/file.rs:LL:CC) because
-                                    expression evaluated to an empty collection: `&assumptions`
             "#]]);
 }
 
@@ -87,16 +77,6 @@ fn indirect_cycle_1() {
                                 judgment `equate_variable` failed at the following rule(s):
                                   failed at (src/file.rs:LL:CC) because
                                     `?ty_0` occurs in `Vec<?ty_0>`
-                          the rule "normalize-l" failed at step #0 (src/file.rs:LL:CC) because
-                            judgment `prove_normalize { p: ?ty_0, assumptions: {}, env: Env { variables: [?ty_0], coherence_mode: false }, decls: decls(222, [trait Foo <ty> ], [impl <ty> Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s):
-                              the rule "normalize-via-assumption" failed at step #0 (src/file.rs:LL:CC) because
-                                expression evaluated to an empty collection: `&assumptions`
-                          the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because
-                            judgment `prove_eq { a: Vec<?ty_0>, b: ?ty_0, assumptions: {}, env: Env { variables: [?ty_0], coherence_mode: false }, decls: decls(222, [trait Foo <ty> ], [impl <ty> Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s):
-                              the rule "normalize-l" failed at step #0 (src/file.rs:LL:CC) because
-                                judgment `prove_normalize { p: Vec<?ty_0>, assumptions: {}, env: Env { variables: [?ty_0], coherence_mode: false }, decls: decls(222, [trait Foo <ty> ], [impl <ty> Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s):
-                                  the rule "normalize-via-assumption" failed at step #0 (src/file.rs:LL:CC) because
-                                    expression evaluated to an empty collection: `&assumptions`
     "#]]);
 }
 
@@ -123,15 +103,5 @@ fn indirect_cycle_2() {
                                 judgment `equate_variable` failed at the following rule(s):
                                   failed at (src/file.rs:LL:CC) because
                                     `?ty_0` occurs in `Vec<?ty_0>`
-                          the rule "normalize-l" failed at step #0 (src/file.rs:LL:CC) because
-                            judgment `prove_normalize { p: ?ty_0, assumptions: {}, env: Env { variables: [?ty_0], coherence_mode: false }, decls: decls(222, [trait Foo <ty> ], [impl <ty> Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s):
-                              the rule "normalize-via-assumption" failed at step #0 (src/file.rs:LL:CC) because
-                                expression evaluated to an empty collection: `&assumptions`
-                          the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because
-                            judgment `prove_eq { a: Vec<?ty_0>, b: ?ty_0, assumptions: {}, env: Env { variables: [?ty_0], coherence_mode: false }, decls: decls(222, [trait Foo <ty> ], [impl <ty> Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s):
-                              the rule "normalize-l" failed at step #0 (src/file.rs:LL:CC) because
-                                judgment `prove_normalize { p: Vec<?ty_0>, assumptions: {}, env: Env { variables: [?ty_0], coherence_mode: false }, decls: decls(222, [trait Foo <ty> ], [impl <ty> Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s):
-                                  the rule "normalize-via-assumption" failed at step #0 (src/file.rs:LL:CC) because
-                                    expression evaluated to an empty collection: `&assumptions`
     "#]]);
 }

crates/formality-prove/src/test/universes.rs

@@ -19,10 +19,6 @@ fn exists_u_for_t() {
                 judgment `prove_wc { goal: !ty_1 = ?ty_0, assumptions: {}, env: Env { variables: [?ty_0, !ty_1], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s):
                   the rule "eq" failed at step #0 (src/file.rs:LL:CC) because
                     judgment `prove_eq { a: !ty_1, b: ?ty_0, assumptions: {}, env: Env { variables: [?ty_0, !ty_1], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s):
-                      the rule "normalize-l" failed at step #0 (src/file.rs:LL:CC) because
-                        judgment `prove_normalize { p: !ty_1, assumptions: {}, env: Env { variables: [?ty_0, !ty_1], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s):
-                          the rule "normalize-via-assumption" failed at step #0 (src/file.rs:LL:CC) because
-                            expression evaluated to an empty collection: `&assumptions`
                       the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because
                         judgment `prove_eq { a: ?ty_0, b: !ty_1, assumptions: {}, env: Env { variables: [?ty_0, !ty_1], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s):
                           the rule "existential" failed at step #0 (src/file.rs:LL:CC) because
@@ -31,10 +27,6 @@ fn exists_u_for_t() {
                                 pattern `None` did not match value `Some(!ty_1)`
                               the rule "existential-universal" failed at step #0 (src/file.rs:LL:CC) because
                                 condition evaluted to false: `env.universe(p) < env.universe(v)`
-                          the rule "normalize-l" failed at step #0 (src/file.rs:LL:CC) because
-                            judgment `prove_normalize { p: ?ty_0, assumptions: {}, env: Env { variables: [?ty_0, !ty_1], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s):
-                              the rule "normalize-via-assumption" failed at step #0 (src/file.rs:LL:CC) because
-                                expression evaluated to an empty collection: `&assumptions`
     "#]]);
 }