diff --git a/crates/formality-prove/src/prove.rs b/crates/formality-prove/src/prove.rs index 8b204d7c..315d7e1e 100644 --- a/crates/formality-prove/src/prove.rs +++ b/crates/formality-prove/src/prove.rs @@ -13,8 +13,9 @@ mod prove_wc_list; mod prove_wf; pub use constraints::Constraints; +use formality_core::judgment::{FailedRule, TryIntoIter}; use formality_core::visit::CoreVisit; -use formality_core::{ProvenSet, Upcast}; +use formality_core::{set, ProvenSet, Upcast}; use formality_types::grammar::Wcs; use tracing::Level; @@ -53,7 +54,20 @@ pub fn prove( assert!(env.encloses(term_in)); - let result_set = prove_wc_list(decls, &env, assumptions, goal); + struct ProveFailureLabel(String); + let label = ProveFailureLabel(format!( + "prove {{ goal: {goal:?}, assumptions: {assumptions:?}, env: {env:?}, decls: {decls:?} }}" + )); + impl std::fmt::Debug for ProveFailureLabel { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + f.write_str(&self.0) + } + } + let result_set = + match prove_wc_list(decls, &env, assumptions, goal).try_into_iter(|| "".to_string()) { + Ok(s) => ProvenSet::from_iter(s), + Err(e) => ProvenSet::failed_rules(label, set![FailedRule::new(e)]), + }; tracing::debug!(?result_set); diff --git a/crates/formality-prove/src/prove/is_local.rs b/crates/formality-prove/src/prove/is_local.rs index 9dd398ce..977d75e8 100644 --- a/crates/formality-prove/src/prove/is_local.rs +++ b/crates/formality-prove/src/prove/is_local.rs @@ -48,12 +48,12 @@ judgment_fn! { /// Note that per RFC #2451, upstream crates are not permitted to add blanket impls /// and so new upstream impls for local types cannot be added. pub fn may_be_remote( - decls: Decls, + _decls: Decls, env: Env, assumptions: Wcs, goal: TraitRef, ) => Constraints { - debug(assumptions, goal, decls, env) + debug(assumptions, goal, env) assert(env.bias() == Bias::Completeness) ( @@ -75,12 +75,12 @@ judgment_fn! { judgment_fn! { /// True if an impl defining this trait-reference could appear in a downstream crate. fn may_be_downstream_trait_ref( - decls: Decls, + _decls: Decls, env: Env, assumptions: Wcs, goal: TraitRef, ) => Constraints { - debug(goal, assumptions, env, decls) + debug(goal, assumptions, env) assert(env.bias() == Bias::Completeness) ( // There may be a downstream parameter at position i... @@ -94,12 +94,12 @@ judgment_fn! { judgment_fn! { fn may_be_downstream_parameter( - decls: Decls, + _decls: Decls, env: Env, assumptions: Wcs, parameter: Parameter, ) => Constraints { - debug(parameter, assumptions, env, decls) + debug(parameter, assumptions, env) assert(env.bias() == Bias::Completeness) ( // existential variables *could* be inferred to downstream types; depends on the substitution @@ -179,12 +179,12 @@ fn may_contain_downstream_type( judgment_fn! { fn normalizes_to_not_downstream( - decls: Decls, + _decls: Decls, env: Env, assumptions: Wcs, parameter: Parameter, ) => Constraints { - debug(parameter, assumptions, env, decls) + debug(parameter, assumptions, env) ( (prove_normalize(&decls, &env, &assumptions, parameter) => (c1, parameter)) @@ -198,12 +198,12 @@ judgment_fn! { judgment_fn! { pub fn is_local_trait_ref( - decls: Decls, + _decls: Decls, env: Env, assumptions: Wcs, goal: TraitRef, ) => Constraints { - debug(goal, assumptions, env, decls) + debug(goal, assumptions, env) assert(env.bias() == Bias::Soundness) ( (if decls.is_local_trait_id(&goal.trait_id)) @@ -235,12 +235,12 @@ judgment_fn! { /// with something like `Vec`, but that is not considered downstream /// as the outermost type (`Vec`) is upstream. fn is_not_downstream( - decls: Decls, + _decls: Decls, env: Env, assumptions: Wcs, parameter: Parameter, ) => Constraints { - debug(parameter, assumptions, env, decls) + debug(parameter, assumptions, env) assert(env.bias() == Bias::Soundness) ( @@ -276,12 +276,12 @@ judgment_fn! { judgment_fn! { fn is_local_parameter( - decls: Decls, + _decls: Decls, env: Env, assumptions: Wcs, goal: Parameter, ) => Constraints { - debug(goal, assumptions, env, decls) + debug(goal, assumptions, env) assert(env.bias() == Bias::Soundness) // If we can normalize `goal` to something else, check if that normalized form is local. diff --git a/crates/formality-prove/src/prove/prove_after.rs b/crates/formality-prove/src/prove/prove_after.rs index 3bdbe16b..df4d480c 100644 --- a/crates/formality-prove/src/prove/prove_after.rs +++ b/crates/formality-prove/src/prove/prove_after.rs @@ -7,12 +7,12 @@ use super::constraints::Constraints; judgment_fn! { pub fn prove_after( - decls: Decls, + _decls: Decls, constraints: Constraints, assumptions: Wcs, goal: Wcs, ) => Constraints { - debug(constraints, goal, assumptions, decls) + debug(constraints, goal, assumptions) ( (let (assumptions, goal) = c1.substitution().apply(&(assumptions, goal))) diff --git a/crates/formality-prove/src/prove/prove_eq.rs b/crates/formality-prove/src/prove/prove_eq.rs index 23c9d6e0..92dc3470 100644 --- a/crates/formality-prove/src/prove/prove_eq.rs +++ b/crates/formality-prove/src/prove/prove_eq.rs @@ -22,13 +22,13 @@ pub fn eq(a: impl Upcast, b: impl Upcast) -> Relation { judgment_fn! { pub fn prove_eq( - decls: Decls, + _decls: Decls, env: Env, assumptions: Wcs, a: Parameter, b: Parameter, ) => Constraints { - debug(a, b, assumptions, env, decls) + debug(a, b, assumptions, env) assert(a.kind() == b.kind()) @@ -75,13 +75,13 @@ judgment_fn! { judgment_fn! { pub fn prove_existential_var_eq( - decls: Decls, + _decls: Decls, env: Env, assumptions: Wcs, v: ExistentialVar, b: Parameter, ) => Constraints { - debug(v, b, assumptions, env, decls) + debug(v, b, assumptions, env) ( (if let None = t.downcast::()) diff --git a/crates/formality-prove/src/prove/prove_normalize.rs b/crates/formality-prove/src/prove/prove_normalize.rs index 0044435a..55bdbc06 100644 --- a/crates/formality-prove/src/prove/prove_normalize.rs +++ b/crates/formality-prove/src/prove/prove_normalize.rs @@ -15,12 +15,12 @@ use super::constraints::Constraints; judgment_fn! { pub fn prove_normalize( - decls: Decls, + _decls: Decls, env: Env, assumptions: Wcs, p: Parameter, ) => (Constraints, Parameter) { - debug(p, assumptions, env, decls) + debug(p, assumptions, env) ( (&assumptions => a)! @@ -48,13 +48,13 @@ judgment_fn! { judgment_fn! { fn prove_normalize_via( - decls: Decls, + _decls: Decls, env: Env, assumptions: Wcs, via: Wc, goal: Parameter, ) => (Constraints, Parameter) { - debug(goal, via, assumptions, env, decls) + debug(goal, via, assumptions, env) // The following 2 rules handle normalization of existential variables. We look specifically for // the case of a assumption `?X = Y`, which lets us normalize `?X` to `Y`, and ignore @@ -126,13 +126,13 @@ judgment_fn! { judgment_fn! { fn prove_syntactically_eq( - decls: Decls, + _decls: Decls, env: Env, assumptions: Wcs, a: Parameter, b: Parameter, ) => Constraints { - debug(a, b, assumptions, env, decls) + debug(a, b, assumptions, env) trivial(a == b => Constraints::none(env)) diff --git a/crates/formality-prove/src/prove/prove_via.rs b/crates/formality-prove/src/prove/prove_via.rs index 3ff339c5..c3c190a6 100644 --- a/crates/formality-prove/src/prove/prove_via.rs +++ b/crates/formality-prove/src/prove/prove_via.rs @@ -8,13 +8,13 @@ use crate::{ judgment_fn! { pub fn prove_via( - decls: Decls, + _decls: Decls, env: Env, assumptions: Wcs, via: WcData, goal: WcData, ) => Constraints { - debug(goal, via, assumptions, env, decls) + debug(goal, via, assumptions, env) ( (let (skel_c, parameters_c) = pred_1.debone()) diff --git a/crates/formality-prove/src/prove/prove_wc.rs b/crates/formality-prove/src/prove/prove_wc.rs index 134082e5..9a2c38f0 100644 --- a/crates/formality-prove/src/prove/prove_wc.rs +++ b/crates/formality-prove/src/prove/prove_wc.rs @@ -18,12 +18,12 @@ use super::constraints::Constraints; judgment_fn! { pub fn prove_wc( - decls: Decls, + _decls: Decls, env: Env, assumptions: Wcs, goal: Wc, ) => Constraints { - debug(goal, assumptions, env, decls) + debug(goal, assumptions, env) ( (let (env, subst) = env.universal_substitution(&binder)) diff --git a/crates/formality-prove/src/prove/prove_wc_list.rs b/crates/formality-prove/src/prove/prove_wc_list.rs index ed6be40d..c9d52de8 100644 --- a/crates/formality-prove/src/prove/prove_wc_list.rs +++ b/crates/formality-prove/src/prove/prove_wc_list.rs @@ -10,12 +10,12 @@ use super::{env::Env, prove_wc::prove_wc}; judgment_fn! { pub fn prove_wc_list( - decls: Decls, + _decls: Decls, env: Env, assumptions: Wcs, goal: Wcs, ) => Constraints { - debug(goal, assumptions, env, decls) + debug(goal, assumptions, env) assert(env.encloses((&assumptions, &goal))) diff --git a/crates/formality-prove/src/prove/prove_wf.rs b/crates/formality-prove/src/prove/prove_wf.rs index e6c816b6..97b7b550 100644 --- a/crates/formality-prove/src/prove/prove_wf.rs +++ b/crates/formality-prove/src/prove/prove_wf.rs @@ -12,12 +12,12 @@ use super::{constraints::Constraints, env::Env}; judgment_fn! { pub fn prove_wf( - decls: Decls, + _decls: Decls, env: Env, assumptions: Wcs, goal: Parameter, ) => Constraints { - debug(goal, assumptions, env, decls) + debug(goal, assumptions, env) assert(env.encloses((&assumptions, &goal))) diff --git a/crates/formality-prove/src/test/adt_wf.rs b/crates/formality-prove/src/test/adt_wf.rs index 9cb90867..98b86604 100644 --- a/crates/formality-prove/src/test/adt_wf.rs +++ b/crates/formality-prove/src/test/adt_wf.rs @@ -51,17 +51,21 @@ fn not_well_formed_adt() { assumptions, Relation::WellFormed(goal), ).assert_err(expect![[r#" - judgment `prove_wc_list { goal: {@ wf(X)}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo ], [impl Foo(u32)], [], [], [], [adt X where {Foo(^ty0_0)}], {}, {}) }` failed at the following rule(s): - the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: @ wf(X), assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo ], [impl Foo(u32)], [], [], [], [adt X where {Foo(^ty0_0)}], {}, {}) }` failed at the following rule(s): - the rule "parameter well formed" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wf { goal: X, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo ], [impl Foo(u32)], [], [], [], [adt X where {Foo(^ty0_0)}], {}, {}) }` failed at the following rule(s): - the rule "ADT" failed at step #3 (src/file.rs:LL:CC) because - judgment `prove_after { constraints: Constraints { env: Env { variables: [], bias: Soundness }, known_true: true, substitution: {} }, goal: {Foo(u64)}, assumptions: {}, decls: decls(222, [trait Foo ], [impl Foo(u32)], [], [], [], [adt X where {Foo(^ty0_0)}], {}, {}) }` failed at the following rule(s): - the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {Foo(u64)}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo ], [impl Foo(u32)], [], [], [], [adt X where {Foo(^ty0_0)}], {}, {}) }` failed at the following rule(s): - the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: Foo(u64), assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo ], [impl Foo(u32)], [], [], [], [adt X where {Foo(^ty0_0)}], {}, {}) }` 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()`"#]]); + judgment `prove { goal: {@ wf(X)}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo ], [impl Foo(u32)], [], [], [], [adt X where {Foo(^ty0_0)}], {}, {}) }` failed at the following rule(s): + failed at (src/file.rs:LL:CC) because + judgment `prove_wc_list { goal: {@ wf(X)}, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "some" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: @ wf(X), assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "parameter well formed" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_wf { goal: X, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "ADT" failed at step #3 (src/file.rs:LL:CC) because + judgment `prove_after { constraints: Constraints { env: Env { variables: [], bias: Soundness }, known_true: true, substitution: {} }, goal: {Foo(u64)}, assumptions: {} }` failed at the following rule(s): + the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because + judgment `prove { goal: {Foo(u64)}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo ], [impl Foo(u32)], [], [], [], [adt X where {Foo(^ty0_0)}], {}, {}) }` failed at the following rule(s): + failed at (src/file.rs:LL:CC) because + judgment `prove_wc_list { goal: {Foo(u64)}, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "some" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: Foo(u64), assumptions: {}, env: Env { variables: [], bias: Soundness } }` 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()`"#]]); } diff --git a/crates/formality-prove/src/test/eq_assumptions.rs b/crates/formality-prove/src/test/eq_assumptions.rs index abba6ed0..0c3e332e 100644 --- a/crates/formality-prove/src/test/eq_assumptions.rs +++ b/crates/formality-prove/src/test/eq_assumptions.rs @@ -52,147 +52,157 @@ fn test_normalize_assoc_ty_existential0() { term("exists {} => {for if { ::Item = u32 } ::Item = u32}"), ).assert_err( expect![[r#" - judgment `prove_wc_list { goal: {for if {<^ty0_0 as Iterator>::Item = u32} ::Item = u32}, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness }, 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: for if {<^ty0_0 as Iterator>::Item = u32} ::Item = u32, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "forall" failed at step #2 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: if {::Item = u32} ::Item = u32, assumptions: {}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness }, 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: ::Item = u32, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness }, 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: ::Item, b: u32, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness }, 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: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "normalize-via-assumption" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove_normalize_via { goal: ::Item, via: ::Item = u32, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "axiom-l" failed at step #2 (src/file.rs:LL:CC) because - judgment `prove_syntactically_eq { a: ::Item, b: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "alias" failed at step #3 (src/file.rs:LL:CC) because - judgment `prove_syntactically_eq { a: !ty_1, b: ?ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_syntactically_eq { a: ?ty_0, b: !ty_1, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "existential-nonvar" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_existential_var_eq { v: ?ty_0, b: !ty_1, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "existential-nonvar" failed at step #0 (src/file.rs:LL:CC) because - 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 "symmetric" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_syntactically_eq { a: ::Item, b: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove { goal: {for if {<^ty0_0 as Iterator>::Item = u32} ::Item = u32}, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + failed at (src/file.rs:LL:CC) because + judgment `prove_wc_list { goal: {for if {<^ty0_0 as Iterator>::Item = u32} ::Item = u32}, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness } }` failed at the following rule(s): + the rule "some" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: for if {<^ty0_0 as Iterator>::Item = u32} ::Item = u32, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness } }` failed at the following rule(s): + the rule "forall" failed at step #2 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: if {::Item = u32} ::Item = u32, assumptions: {}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness } }` failed at the following rule(s): + the rule "implies" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: ::Item = u32, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness } }` failed at the following rule(s): + the rule "eq" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_eq { a: ::Item, b: u32, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness } }` failed at the following rule(s): + the rule "normalize-l" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_normalize { p: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness } }` failed at the following rule(s): + the rule "normalize-via-assumption" failed at step #1 (src/file.rs:LL:CC) because + judgment `prove_normalize_via { goal: ::Item, via: ::Item = u32, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness } }` failed at the following rule(s): + the rule "axiom-l" failed at step #2 (src/file.rs:LL:CC) because + judgment `prove_syntactically_eq { a: ::Item, b: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness } }` failed at the following rule(s): the rule "alias" failed at step #3 (src/file.rs:LL:CC) because - judgment `prove_syntactically_eq { a: ?ty_0, b: !ty_1, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "existential-nonvar" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_existential_var_eq { v: ?ty_0, b: !ty_1, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_syntactically_eq { a: !ty_1, b: ?ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness } }` failed at the following rule(s): + the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_syntactically_eq { a: ?ty_0, b: !ty_1, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness } }` failed at the following rule(s): the rule "existential-nonvar" failed at step #0 (src/file.rs:LL:CC) because - 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-via-impl" failed at step #0 (src/file.rs:LL:CC) because - expression evaluated to an empty collection: `decls.alias_eq_decls(&a.name)` - the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_eq { a: u32, b: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "normalize-l" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove_after { constraints: Constraints { env: Env { variables: [?ty_0, !ty_1], bias: Soundness }, known_true: true, substitution: {} }, goal: {::Item = ::Item}, assumptions: {::Item = u32}, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {::Item = ::Item}, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, 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: ::Item = ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, 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: ::Item, b: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_existential_var_eq { v: ?ty_0, b: !ty_1, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness } }` failed at the following rule(s): + the rule "existential-nonvar" failed at step #0 (src/file.rs:LL:CC) because + 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 "symmetric" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_syntactically_eq { a: ::Item, b: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness } }` 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: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, 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: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, 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_0, b: ?ty_1, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_eq { a: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "existential" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_existential_var_eq { v: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "existential-nonvar" failed at step #0 (src/file.rs:LL:CC) because - pattern `None` did not match value `Some(!ty_0)` - 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 #1 (src/file.rs:LL:CC) because - judgment `prove_after { constraints: Constraints { env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, known_true: true, substitution: {} }, goal: {u32 = ::Item}, assumptions: {::Item = u32}, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {u32 = ::Item}, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, 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 = ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, 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: u32, b: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_eq { a: ::Item, b: u32, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, 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: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "normalize-via-assumption" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove_normalize_via { goal: ::Item, via: ::Item = u32, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "axiom-l" failed at step #2 (src/file.rs:LL:CC) because - judgment `prove_syntactically_eq { a: ::Item, b: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "alias" failed at step #3 (src/file.rs:LL:CC) because - judgment `prove_syntactically_eq { a: !ty_0, b: ?ty_1, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_syntactically_eq { a: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "existential-nonvar" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_existential_var_eq { v: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "existential-nonvar" failed at step #0 (src/file.rs:LL:CC) because - pattern `None` did not match value `Some(!ty_0)` - 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 "symmetric" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_syntactically_eq { a: ::Item, b: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "alias" failed at step #3 (src/file.rs:LL:CC) because - judgment `prove_syntactically_eq { a: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "existential-nonvar" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_existential_var_eq { v: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "existential-nonvar" failed at step #0 (src/file.rs:LL:CC) because - pattern `None` did not match value `Some(!ty_0)` - 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-via-impl" failed at step #0 (src/file.rs:LL:CC) because - expression evaluated to an empty collection: `decls.alias_eq_decls(&a.name)` - the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_eq { a: ::Item, b: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, 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_1 = !ty_0}, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, 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: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, 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: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "existential" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_existential_var_eq { v: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "existential-nonvar" failed at step #0 (src/file.rs:LL:CC) because - pattern `None` did not match value `Some(!ty_0)` - 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: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "normalize-via-assumption" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove_normalize_via { goal: ::Item, via: ::Item = u32, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "axiom-l" failed at step #2 (src/file.rs:LL:CC) because - judgment `prove_syntactically_eq { a: ::Item, b: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "alias" failed at step #3 (src/file.rs:LL:CC) because - judgment `prove_syntactically_eq { a: !ty_0, b: ?ty_1, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_syntactically_eq { a: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "existential-nonvar" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_existential_var_eq { v: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "existential-nonvar" failed at step #0 (src/file.rs:LL:CC) because - pattern `None` did not match value `Some(!ty_0)` - 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 "symmetric" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_syntactically_eq { a: ::Item, b: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "alias" failed at step #3 (src/file.rs:LL:CC) because - judgment `prove_syntactically_eq { a: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "existential-nonvar" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_existential_var_eq { v: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "existential-nonvar" failed at step #0 (src/file.rs:LL:CC) because - pattern `None` did not match value `Some(!ty_0)` - 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-via-impl" failed at step #0 (src/file.rs:LL:CC) because - expression evaluated to an empty collection: `decls.alias_eq_decls(&a.name)`"#]]); + judgment `prove_syntactically_eq { a: ?ty_0, b: !ty_1, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness } }` failed at the following rule(s): + the rule "existential-nonvar" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_existential_var_eq { v: ?ty_0, b: !ty_1, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness } }` failed at the following rule(s): + the rule "existential-nonvar" failed at step #0 (src/file.rs:LL:CC) because + 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-via-impl" failed at step #0 (src/file.rs:LL:CC) because + expression evaluated to an empty collection: `decls.alias_eq_decls(&a.name)` + the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_eq { a: u32, b: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness } }` failed at the following rule(s): + the rule "normalize-l" failed at step #1 (src/file.rs:LL:CC) because + judgment `prove_after { constraints: Constraints { env: Env { variables: [?ty_0, !ty_1], bias: Soundness }, known_true: true, substitution: {} }, goal: {::Item = ::Item}, assumptions: {::Item = u32} }` failed at the following rule(s): + the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because + judgment `prove { goal: {::Item = ::Item}, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + failed at (src/file.rs:LL:CC) because + judgment `prove_wc_list { goal: {::Item = ::Item}, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + the rule "some" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: ::Item = ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + the rule "eq" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_eq { a: ::Item, b: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + the rule "alias" failed at step #3 (src/file.rs:LL:CC) because + judgment `prove { goal: {!ty_0 = ?ty_1}, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + failed at (src/file.rs:LL:CC) because + judgment `prove_wc_list { goal: {!ty_0 = ?ty_1}, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` 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: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + the rule "eq" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_eq { a: !ty_0, b: ?ty_1, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_eq { a: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + the rule "existential" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_existential_var_eq { v: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + the rule "existential-nonvar" failed at step #0 (src/file.rs:LL:CC) because + pattern `None` did not match value `Some(!ty_0)` + 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 #1 (src/file.rs:LL:CC) because + judgment `prove_after { constraints: Constraints { env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, known_true: true, substitution: {} }, goal: {u32 = ::Item}, assumptions: {::Item = u32} }` failed at the following rule(s): + the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because + judgment `prove { goal: {u32 = ::Item}, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + failed at (src/file.rs:LL:CC) because + judgment `prove_wc_list { goal: {u32 = ::Item}, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + the rule "some" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: u32 = ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + the rule "eq" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_eq { a: u32, b: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_eq { a: ::Item, b: u32, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + the rule "normalize-l" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_normalize { p: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + the rule "normalize-via-assumption" failed at step #1 (src/file.rs:LL:CC) because + judgment `prove_normalize_via { goal: ::Item, via: ::Item = u32, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + the rule "axiom-l" failed at step #2 (src/file.rs:LL:CC) because + judgment `prove_syntactically_eq { a: ::Item, b: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + the rule "alias" failed at step #3 (src/file.rs:LL:CC) because + judgment `prove_syntactically_eq { a: !ty_0, b: ?ty_1, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_syntactically_eq { a: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + the rule "existential-nonvar" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_existential_var_eq { v: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + the rule "existential-nonvar" failed at step #0 (src/file.rs:LL:CC) because + pattern `None` did not match value `Some(!ty_0)` + 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 "symmetric" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_syntactically_eq { a: ::Item, b: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + the rule "alias" failed at step #3 (src/file.rs:LL:CC) because + judgment `prove_syntactically_eq { a: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + the rule "existential-nonvar" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_existential_var_eq { v: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + the rule "existential-nonvar" failed at step #0 (src/file.rs:LL:CC) because + pattern `None` did not match value `Some(!ty_0)` + 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-via-impl" failed at step #0 (src/file.rs:LL:CC) because + expression evaluated to an empty collection: `decls.alias_eq_decls(&a.name)` + the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_eq { a: ::Item, b: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + the rule "alias" failed at step #3 (src/file.rs:LL:CC) because + judgment `prove { goal: {?ty_1 = !ty_0}, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + failed at (src/file.rs:LL:CC) because + judgment `prove_wc_list { goal: {?ty_1 = !ty_0}, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` 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: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` 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: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + the rule "existential" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_existential_var_eq { v: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + the rule "existential-nonvar" failed at step #0 (src/file.rs:LL:CC) because + pattern `None` did not match value `Some(!ty_0)` + 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: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + the rule "normalize-via-assumption" failed at step #1 (src/file.rs:LL:CC) because + judgment `prove_normalize_via { goal: ::Item, via: ::Item = u32, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + the rule "axiom-l" failed at step #2 (src/file.rs:LL:CC) because + judgment `prove_syntactically_eq { a: ::Item, b: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + the rule "alias" failed at step #3 (src/file.rs:LL:CC) because + judgment `prove_syntactically_eq { a: !ty_0, b: ?ty_1, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_syntactically_eq { a: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + the rule "existential-nonvar" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_existential_var_eq { v: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + the rule "existential-nonvar" failed at step #0 (src/file.rs:LL:CC) because + pattern `None` did not match value `Some(!ty_0)` + 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 "symmetric" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_syntactically_eq { a: ::Item, b: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + the rule "alias" failed at step #3 (src/file.rs:LL:CC) because + judgment `prove_syntactically_eq { a: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + the rule "existential-nonvar" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_existential_var_eq { v: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + the rule "existential-nonvar" failed at step #0 (src/file.rs:LL:CC) because + pattern `None` did not match value `Some(!ty_0)` + 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-via-impl" failed at step #0 (src/file.rs:LL:CC) because + expression evaluated to an empty collection: `decls.alias_eq_decls(&a.name)`"#]]); } #[test] diff --git a/crates/formality-prove/src/test/eq_partial_eq.rs b/crates/formality-prove/src/test/eq_partial_eq.rs index d1c46c2c..7216d505 100644 --- a/crates/formality-prove/src/test/eq_partial_eq.rs +++ b/crates/formality-prove/src/test/eq_partial_eq.rs @@ -44,17 +44,19 @@ fn not_partial_eq_implies_eq() { prove(decls(), (), (), goal) .assert_err( expect![[r#" - judgment `prove_wc_list { goal: {for if {PartialEq(^ty0_0)} Eq(^ty0_0)}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: for if {PartialEq(^ty0_0)} Eq(^ty0_0), assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "forall" failed at step #2 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: if {PartialEq(!ty_1)} Eq(!ty_1), assumptions: {}, env: Env { variables: [!ty_1], bias: Soundness }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "implies" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: Eq(!ty_1), assumptions: {PartialEq(!ty_1)}, env: Env { variables: [!ty_1], bias: Soundness }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "assumption - predicate" failed at step #1 (src/file.rs:LL:CC) because - judgment had no applicable rules: `prove_via { goal: Eq(!ty_1), via: PartialEq(!ty_1), assumptions: {PartialEq(!ty_1)}, env: Env { variables: [!ty_1], bias: Soundness }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` - the rule "trait implied bound" failed at step #3 (src/file.rs:LL:CC) because - judgment had no applicable rules: `prove_via { goal: Eq(!ty_1), via: PartialEq(?ty_2), assumptions: {PartialEq(!ty_1)}, env: Env { variables: [!ty_1, ?ty_2], bias: Soundness }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }`"#]]); + judgment `prove { goal: {for if {PartialEq(^ty0_0)} Eq(^ty0_0)}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + failed at (src/file.rs:LL:CC) because + judgment `prove_wc_list { goal: {for if {PartialEq(^ty0_0)} Eq(^ty0_0)}, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "some" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: for if {PartialEq(^ty0_0)} Eq(^ty0_0), assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "forall" failed at step #2 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: if {PartialEq(!ty_1)} Eq(!ty_1), assumptions: {}, env: Env { variables: [!ty_1], bias: Soundness } }` failed at the following rule(s): + the rule "implies" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: Eq(!ty_1), assumptions: {PartialEq(!ty_1)}, env: Env { variables: [!ty_1], bias: Soundness } }` failed at the following rule(s): + the rule "assumption - predicate" failed at step #1 (src/file.rs:LL:CC) because + judgment had no applicable rules: `prove_via { goal: Eq(!ty_1), via: PartialEq(!ty_1), assumptions: {PartialEq(!ty_1)}, env: Env { variables: [!ty_1], bias: Soundness } }` + the rule "trait implied bound" failed at step #3 (src/file.rs:LL:CC) because + judgment had no applicable rules: `prove_via { goal: Eq(!ty_1), via: PartialEq(?ty_2), assumptions: {PartialEq(!ty_1)}, env: Env { variables: [!ty_1, ?ty_2], bias: Soundness } }`"#]]); } #[test] @@ -63,43 +65,49 @@ fn universals_not_eq() { prove(decls(), (), (), goal) .assert_err( expect![[r#" - judgment `prove_wc_list { goal: {for if {Eq(^ty0_0)} PartialEq(^ty0_1)}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: for if {Eq(^ty0_0)} PartialEq(^ty0_1), assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "forall" failed at step #2 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: if {Eq(!ty_1)} PartialEq(!ty_2), assumptions: {}, env: Env { variables: [!ty_1, !ty_2], bias: Soundness }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "implies" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: PartialEq(!ty_2), assumptions: {Eq(!ty_1)}, env: Env { variables: [!ty_1, !ty_2], bias: Soundness }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "assumption - predicate" failed at step #1 (src/file.rs:LL:CC) because - judgment had no applicable rules: `prove_via { goal: PartialEq(!ty_2), via: Eq(!ty_1), assumptions: {Eq(!ty_1)}, env: Env { variables: [!ty_1, !ty_2], bias: Soundness }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` - the rule "trait implied bound" failed at step #4 (src/file.rs:LL:CC) because - judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_1, !ty_2, ?ty_3], bias: Soundness }, known_true: true, substitution: {?ty_3 => !ty_2} }, goal: {Eq(?ty_3)}, assumptions: {Eq(!ty_1)}, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {Eq(!ty_1)}, assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: Eq(!ty_1), assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "assumption - predicate" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove_via { goal: Eq(!ty_1), via: Eq(!ty_0), assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "predicate-congruence-axiom" failed at step #3 (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {!ty_0 = !ty_1}, assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` 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: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` 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: !ty_0 = !ty_1, via: Eq(!ty_0), assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` - the rule "eq" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_eq { a: !ty_0, b: !ty_1, assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` 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_0, assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` 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: !ty_0, via: Eq(!ty_0), assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` - the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_eq { a: !ty_1, b: !ty_0, assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` 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: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` 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: !ty_1, via: Eq(!ty_0), assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` - the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because - cyclic proof attempt: `prove_eq { a: !ty_0, b: !ty_1, assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` - the rule "trait implied bound" failed at step #3 (src/file.rs:LL:CC) because - judgment had no applicable rules: `prove_via { goal: Eq(!ty_1), via: PartialEq(?ty_2), assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1, ?ty_2], bias: Soundness }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }`"#]]); + judgment `prove { goal: {for if {Eq(^ty0_0)} PartialEq(^ty0_1)}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + failed at (src/file.rs:LL:CC) because + judgment `prove_wc_list { goal: {for if {Eq(^ty0_0)} PartialEq(^ty0_1)}, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "some" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: for if {Eq(^ty0_0)} PartialEq(^ty0_1), assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "forall" failed at step #2 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: if {Eq(!ty_1)} PartialEq(!ty_2), assumptions: {}, env: Env { variables: [!ty_1, !ty_2], bias: Soundness } }` failed at the following rule(s): + the rule "implies" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: PartialEq(!ty_2), assumptions: {Eq(!ty_1)}, env: Env { variables: [!ty_1, !ty_2], bias: Soundness } }` failed at the following rule(s): + the rule "assumption - predicate" failed at step #1 (src/file.rs:LL:CC) because + judgment had no applicable rules: `prove_via { goal: PartialEq(!ty_2), via: Eq(!ty_1), assumptions: {Eq(!ty_1)}, env: Env { variables: [!ty_1, !ty_2], bias: Soundness } }` + the rule "trait implied bound" failed at step #4 (src/file.rs:LL:CC) because + judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_1, !ty_2, ?ty_3], bias: Soundness }, known_true: true, substitution: {?ty_3 => !ty_2} }, goal: {Eq(?ty_3)}, assumptions: {Eq(!ty_1)} }` failed at the following rule(s): + the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because + judgment `prove { goal: {Eq(!ty_1)}, assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + failed at (src/file.rs:LL:CC) because + judgment `prove_wc_list { goal: {Eq(!ty_1)}, assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness } }` failed at the following rule(s): + the rule "some" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: Eq(!ty_1), assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness } }` failed at the following rule(s): + the rule "assumption - predicate" failed at step #1 (src/file.rs:LL:CC) because + judgment `prove_via { goal: Eq(!ty_1), via: Eq(!ty_0), assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness } }` failed at the following rule(s): + the rule "predicate-congruence-axiom" failed at step #3 (src/file.rs:LL:CC) because + judgment `prove { goal: {!ty_0 = !ty_1}, assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + failed at (src/file.rs:LL:CC) because + judgment `prove_wc_list { goal: {!ty_0 = !ty_1}, assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness } }` 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: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness } }` 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: !ty_0 = !ty_1, via: Eq(!ty_0), assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness } }` + the rule "eq" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_eq { a: !ty_0, b: !ty_1, assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness } }` 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_0, assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness } }` 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: !ty_0, via: Eq(!ty_0), assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness } }` + the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_eq { a: !ty_1, b: !ty_0, assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness } }` 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: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness } }` 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: !ty_1, via: Eq(!ty_0), assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness } }` + the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because + cyclic proof attempt: `prove_eq { a: !ty_0, b: !ty_1, assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness } }` + the rule "trait implied bound" failed at step #3 (src/file.rs:LL:CC) because + judgment had no applicable rules: `prove_via { goal: Eq(!ty_1), via: PartialEq(?ty_2), assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1, ?ty_2], bias: Soundness } }`"#]]); } diff --git a/crates/formality-prove/src/test/is_local.rs b/crates/formality-prove/src/test/is_local.rs index 0c269e54..ed56bbcf 100644 --- a/crates/formality-prove/src/test/is_local.rs +++ b/crates/formality-prove/src/test/is_local.rs @@ -13,17 +13,19 @@ fn test_forall_not_local() { term("{} => {for @IsLocal(Debug(T))}"), ).assert_err( expect![[r#" - judgment `prove_wc_list { goal: {for @ IsLocal(Debug(^ty0_0))}, assumptions: {}, env: Env { variables: [], bias: Soundness }, 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: for @ IsLocal(Debug(^ty0_0)), assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "forall" failed at step #2 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: @ IsLocal(Debug(!ty_1)), assumptions: {}, env: Env { variables: [!ty_1], bias: Soundness }, 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], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): - 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)` - decls = decls(222, [], [], [], [], [], [], {}, {}) - &goal.trait_id = Debug"#]]); + judgment `prove { goal: {for @ IsLocal(Debug(^ty0_0))}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + failed at (src/file.rs:LL:CC) because + judgment `prove_wc_list { goal: {for @ IsLocal(Debug(^ty0_0))}, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "some" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: for @ IsLocal(Debug(^ty0_0)), assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "forall" failed at step #2 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: @ IsLocal(Debug(!ty_1)), assumptions: {}, env: Env { variables: [!ty_1], bias: Soundness } }` 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], bias: Soundness } }` failed at the following rule(s): + 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)` + decls = decls(222, [], [], [], [], [], [], {}, {}) + &goal.trait_id = Debug"#]]); } #[test] diff --git a/crates/formality-prove/src/test/magic_copy.rs b/crates/formality-prove/src/test/magic_copy.rs index 755a9ecd..4ab17a3c 100644 --- a/crates/formality-prove/src/test/magic_copy.rs +++ b/crates/formality-prove/src/test/magic_copy.rs @@ -25,118 +25,140 @@ fn decls() -> Decls { fn all_t_not_magic() { test_prove(decls(), term("{} => {for Magic(T)}")).assert_err( expect![[r#" - judgment `prove_wc_list { goal: {for Magic(^ty0_0)}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: for Magic(^ty0_0), assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "forall" failed at step #2 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: Magic(!ty_1), assumptions: {}, env: Env { variables: [!ty_1], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` 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: [!ty_1, ?ty_2], bias: Soundness }, known_true: true, substitution: {?ty_2 => !ty_1} }, goal: {Copy(?ty_2)}, assumptions: {}, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {Copy(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: Copy(!ty_0), assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "positive impl" failed at step #5 (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {!ty_0 = u32}, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove { goal: {for Magic(^ty0_0)}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): + failed at (src/file.rs:LL:CC) because + judgment `prove_wc_list { goal: {for Magic(^ty0_0)}, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "some" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: for Magic(^ty0_0), assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "forall" failed at step #2 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: Magic(!ty_1), assumptions: {}, env: Env { variables: [!ty_1], bias: Soundness } }` 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: [!ty_1, ?ty_2], bias: Soundness }, known_true: true, substitution: {?ty_2 => !ty_1} }, goal: {Copy(?ty_2)}, assumptions: {} }` failed at the following rule(s): + the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because + judgment `prove { goal: {Copy(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): + failed at (src/file.rs:LL:CC) because + judgment `prove_wc_list { goal: {Copy(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness } }` 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 = u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` 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: !ty_0 = u32, via: Copy(!ty_0), assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` - the rule "eq" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_eq { a: !ty_0, b: u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` 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_0, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` 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: !ty_0, via: Copy(!ty_0), assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` - the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_eq { a: u32, b: !ty_0, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` 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: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` 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: Copy(!ty_0), assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` - the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because - cyclic proof attempt: `prove_eq { a: !ty_0, b: u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` - the rule "trait implied bound" failed at step #4 (src/file.rs:LL:CC) because - judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_0, ?ty_1], bias: Soundness }, known_true: true, substitution: {?ty_1 => !ty_0} }, goal: {Magic(?ty_1)}, assumptions: {}, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {Magic(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: Magic(!ty_0), assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` 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: [!ty_0, ?ty_1], bias: Soundness }, known_true: true, substitution: {?ty_1 => !ty_0} }, goal: {Copy(?ty_1)}, assumptions: {}, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because - cyclic proof attempt: `prove_wc_list { goal: {Copy(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` - the rule "trait implied bound" failed at step #3 (src/file.rs:LL:CC) because - judgment had no applicable rules: `prove_via { goal: Magic(!ty_0), via: Copy(?ty_1), assumptions: {}, env: Env { variables: [!ty_0, ?ty_1], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` - the rule "trait implied bound" failed at step #3 (src/file.rs:LL:CC) because - judgment had no applicable rules: `prove_via { goal: Magic(!ty_1), via: Copy(?ty_2), assumptions: {}, env: Env { variables: [!ty_1, ?ty_2], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }`"#]]); -} - -#[test] -fn all_t_not_copy() { - test_prove(decls(), term("{} => {for Copy(T)}")).assert_err( - expect![[r#" - judgment `prove_wc_list { goal: {for Copy(^ty0_0)}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: for Copy(^ty0_0), assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "forall" failed at step #2 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: Copy(!ty_1), assumptions: {}, env: Env { variables: [!ty_1], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "positive impl" failed at step #5 (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {!ty_0 = u32}, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` 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 = u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` 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: !ty_0 = u32, via: Copy(!ty_0), assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` - the rule "eq" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_eq { a: !ty_0, b: u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` 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_0, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` 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: !ty_0, via: Copy(!ty_0), assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` - the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_eq { a: u32, b: !ty_0, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` 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: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` 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: Copy(!ty_0), assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` - the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because - cyclic proof attempt: `prove_eq { a: !ty_0, b: u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` - the rule "trait implied bound" failed at step #4 (src/file.rs:LL:CC) because - judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_1, ?ty_2], bias: Soundness }, known_true: true, substitution: {?ty_2 => !ty_1} }, goal: {Magic(?ty_2)}, assumptions: {}, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {Magic(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: Magic(!ty_0), assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` 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: [!ty_0, ?ty_1], bias: Soundness }, known_true: true, substitution: {?ty_1 => !ty_0} }, goal: {Copy(?ty_1)}, assumptions: {}, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {Copy(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: Copy(!ty_0), assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "positive impl" failed at step #5 (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {!ty_0 = u32}, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_wc { goal: Copy(!ty_0), assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s): + the rule "positive impl" failed at step #5 (src/file.rs:LL:CC) because + judgment `prove { goal: {!ty_0 = u32}, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): + failed at (src/file.rs:LL:CC) because + judgment `prove_wc_list { goal: {!ty_0 = u32}, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` 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 = u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_wc { goal: !ty_0 = u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` 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: !ty_0 = u32, via: Copy(!ty_0), assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` + judgment had no applicable rules: `prove_via { goal: !ty_0 = u32, via: Copy(!ty_0), assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` the rule "eq" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_eq { a: !ty_0, b: u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_eq { a: !ty_0, b: u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` 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_0, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_normalize { p: !ty_0, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` 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: !ty_0, via: Copy(!ty_0), assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` + judgment had no applicable rules: `prove_normalize_via { goal: !ty_0, via: Copy(!ty_0), assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_eq { a: u32, b: !ty_0, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_eq { a: u32, b: !ty_0, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` 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: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_normalize { p: u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` 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: Copy(!ty_0), assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` + judgment had no applicable rules: `prove_normalize_via { goal: u32, via: Copy(!ty_0), assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because - cyclic proof attempt: `prove_eq { a: !ty_0, b: u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` - the rule "trait implied bound" failed at step #4 (src/file.rs:LL:CC) because - judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_0, ?ty_1], bias: Soundness }, known_true: true, substitution: {?ty_1 => !ty_0} }, goal: {Magic(?ty_1)}, assumptions: {}, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because - cyclic proof attempt: `prove_wc_list { goal: {Magic(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` - the rule "trait implied bound" failed at step #3 (src/file.rs:LL:CC) because - judgment had no applicable rules: `prove_via { goal: Magic(!ty_0), via: Copy(?ty_1), assumptions: {}, env: Env { variables: [!ty_0, ?ty_1], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }`"#]]); + cyclic proof attempt: `prove_eq { a: !ty_0, b: u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` + the rule "trait implied bound" failed at step #4 (src/file.rs:LL:CC) because + judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_0, ?ty_1], bias: Soundness }, known_true: true, substitution: {?ty_1 => !ty_0} }, goal: {Magic(?ty_1)}, assumptions: {} }` failed at the following rule(s): + the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because + judgment `prove { goal: {Magic(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): + failed at (src/file.rs:LL:CC) because + judgment `prove_wc_list { goal: {Magic(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s): + the rule "some" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: Magic(!ty_0), assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness } }` 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: [!ty_0, ?ty_1], bias: Soundness }, known_true: true, substitution: {?ty_1 => !ty_0} }, goal: {Copy(?ty_1)}, assumptions: {} }` failed at the following rule(s): + the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because + judgment `prove { goal: {Copy(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): + failed at (src/file.rs:LL:CC) because + cyclic proof attempt: `prove_wc_list { goal: {Copy(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness } }` + the rule "trait implied bound" failed at step #3 (src/file.rs:LL:CC) because + judgment had no applicable rules: `prove_via { goal: Magic(!ty_0), via: Copy(?ty_1), assumptions: {}, env: Env { variables: [!ty_0, ?ty_1], bias: Soundness } }` + the rule "trait implied bound" failed at step #3 (src/file.rs:LL:CC) because + judgment had no applicable rules: `prove_via { goal: Magic(!ty_1), via: Copy(?ty_2), assumptions: {}, env: Env { variables: [!ty_1, ?ty_2], bias: Soundness } }`"#]]); +} + +#[test] +fn all_t_not_copy() { + test_prove(decls(), term("{} => {for Copy(T)}")).assert_err( + expect![[r#" + judgment `prove { goal: {for Copy(^ty0_0)}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): + failed at (src/file.rs:LL:CC) because + judgment `prove_wc_list { goal: {for Copy(^ty0_0)}, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "some" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: for Copy(^ty0_0), assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "forall" failed at step #2 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: Copy(!ty_1), assumptions: {}, env: Env { variables: [!ty_1], bias: Soundness } }` failed at the following rule(s): + the rule "positive impl" failed at step #5 (src/file.rs:LL:CC) because + judgment `prove { goal: {!ty_0 = u32}, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): + failed at (src/file.rs:LL:CC) because + judgment `prove_wc_list { goal: {!ty_0 = u32}, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` 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 = u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` 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: !ty_0 = u32, via: Copy(!ty_0), assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` + the rule "eq" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_eq { a: !ty_0, b: u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` 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_0, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` 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: !ty_0, via: Copy(!ty_0), assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` + the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_eq { a: u32, b: !ty_0, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` 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: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` 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: Copy(!ty_0), assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` + the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because + cyclic proof attempt: `prove_eq { a: !ty_0, b: u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` + the rule "trait implied bound" failed at step #4 (src/file.rs:LL:CC) because + judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_1, ?ty_2], bias: Soundness }, known_true: true, substitution: {?ty_2 => !ty_1} }, goal: {Magic(?ty_2)}, assumptions: {} }` failed at the following rule(s): + the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because + judgment `prove { goal: {Magic(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): + failed at (src/file.rs:LL:CC) because + judgment `prove_wc_list { goal: {Magic(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s): + the rule "some" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: Magic(!ty_0), assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness } }` 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: [!ty_0, ?ty_1], bias: Soundness }, known_true: true, substitution: {?ty_1 => !ty_0} }, goal: {Copy(?ty_1)}, assumptions: {} }` failed at the following rule(s): + the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because + judgment `prove { goal: {Copy(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): + failed at (src/file.rs:LL:CC) because + judgment `prove_wc_list { goal: {Copy(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s): + the rule "some" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: Copy(!ty_0), assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s): + the rule "positive impl" failed at step #5 (src/file.rs:LL:CC) because + judgment `prove { goal: {!ty_0 = u32}, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): + failed at (src/file.rs:LL:CC) because + judgment `prove_wc_list { goal: {!ty_0 = u32}, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` 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 = u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` 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: !ty_0 = u32, via: Copy(!ty_0), assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` + the rule "eq" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_eq { a: !ty_0, b: u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` 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_0, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` 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: !ty_0, via: Copy(!ty_0), assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` + the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_eq { a: u32, b: !ty_0, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` 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: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` 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: Copy(!ty_0), assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` + the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because + cyclic proof attempt: `prove_eq { a: !ty_0, b: u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` + the rule "trait implied bound" failed at step #4 (src/file.rs:LL:CC) because + judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_0, ?ty_1], bias: Soundness }, known_true: true, substitution: {?ty_1 => !ty_0} }, goal: {Magic(?ty_1)}, assumptions: {} }` failed at the following rule(s): + the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because + judgment `prove { goal: {Magic(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): + failed at (src/file.rs:LL:CC) because + cyclic proof attempt: `prove_wc_list { goal: {Magic(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness } }` + the rule "trait implied bound" failed at step #3 (src/file.rs:LL:CC) because + judgment had no applicable rules: `prove_via { goal: Magic(!ty_0), via: Copy(?ty_1), assumptions: {}, env: Env { variables: [!ty_0, ?ty_1], bias: Soundness } }`"#]]); } diff --git a/crates/formality-prove/src/test/occurs_check.rs b/crates/formality-prove/src/test/occurs_check.rs index f44e0666..5b9012aa 100644 --- a/crates/formality-prove/src/test/occurs_check.rs +++ b/crates/formality-prove/src/test/occurs_check.rs @@ -20,17 +20,19 @@ fn decls() -> Decls { fn direct_cycle() { test_prove(decls(), term("exists {} => {A = Vec}")).assert_err( expect![[r#" - judgment `prove_wc_list { goal: {?ty_0 = Vec}, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness }, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` 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 = Vec, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness }, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "eq" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_eq { a: ?ty_0, b: Vec, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness }, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "existential" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_existential_var_eq { v: ?ty_0, b: Vec, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness }, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "existential-nonvar" failed at step #1 (src/file.rs:LL:CC) because - judgment `equate_variable` failed at the following rule(s): - failed at (src/file.rs:LL:CC) because - `?ty_0` occurs in `Vec`"#]]); + judgment `prove { goal: {?ty_0 = Vec}, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness }, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s): + failed at (src/file.rs:LL:CC) because + judgment `prove_wc_list { goal: {?ty_0 = Vec}, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness } }` 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 = Vec, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness } }` failed at the following rule(s): + the rule "eq" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_eq { a: ?ty_0, b: Vec, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness } }` failed at the following rule(s): + the rule "existential" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_existential_var_eq { v: ?ty_0, b: Vec, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness } }` failed at the following rule(s): + the rule "existential-nonvar" failed at step #1 (src/file.rs:LL:CC) because + judgment `equate_variable` failed at the following rule(s): + failed at (src/file.rs:LL:CC) because + `?ty_0` occurs in `Vec`"#]]); } /// Test that `X = Vec` can be solved @@ -61,21 +63,25 @@ fn indirect_cycle_1() { term("exists {} => {A = Vec, B = A}"), ).assert_err( expect![[r#" - judgment `prove_wc_list { goal: {?ty_0 = Vec, ?ty_1 = ?ty_0}, assumptions: {}, env: Env { variables: [?ty_0, ?ty_1], bias: Soundness }, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "some" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove_after { constraints: Constraints { env: Env { variables: [?ty_2, ?ty_0, ?ty_1], bias: Soundness }, known_true: true, substitution: {?ty_0 => Vec, ?ty_1 => ?ty_2} }, goal: {?ty_1 = ?ty_0}, assumptions: {}, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {?ty_0 = Vec}, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness }, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` 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 = Vec, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness }, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "eq" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_eq { a: ?ty_0, b: Vec, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness }, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "existential" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_existential_var_eq { v: ?ty_0, b: Vec, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness }, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "existential-nonvar" failed at step #1 (src/file.rs:LL:CC) because - judgment `equate_variable` failed at the following rule(s): - failed at (src/file.rs:LL:CC) because - `?ty_0` occurs in `Vec`"#]]); + judgment `prove { goal: {?ty_0 = Vec, ?ty_1 = ?ty_0}, assumptions: {}, env: Env { variables: [?ty_0, ?ty_1], bias: Soundness }, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s): + failed at (src/file.rs:LL:CC) because + judgment `prove_wc_list { goal: {?ty_0 = Vec, ?ty_1 = ?ty_0}, assumptions: {}, env: Env { variables: [?ty_0, ?ty_1], bias: Soundness } }` failed at the following rule(s): + the rule "some" failed at step #1 (src/file.rs:LL:CC) because + judgment `prove_after { constraints: Constraints { env: Env { variables: [?ty_2, ?ty_0, ?ty_1], bias: Soundness }, known_true: true, substitution: {?ty_0 => Vec, ?ty_1 => ?ty_2} }, goal: {?ty_1 = ?ty_0}, assumptions: {} }` failed at the following rule(s): + the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because + judgment `prove { goal: {?ty_0 = Vec}, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness }, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s): + failed at (src/file.rs:LL:CC) because + judgment `prove_wc_list { goal: {?ty_0 = Vec}, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness } }` 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 = Vec, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness } }` failed at the following rule(s): + the rule "eq" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_eq { a: ?ty_0, b: Vec, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness } }` failed at the following rule(s): + the rule "existential" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_existential_var_eq { v: ?ty_0, b: Vec, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness } }` failed at the following rule(s): + the rule "existential-nonvar" failed at step #1 (src/file.rs:LL:CC) because + judgment `equate_variable` failed at the following rule(s): + failed at (src/file.rs:LL:CC) because + `?ty_0` occurs in `Vec`"#]]); } /// Test that `X = Vec` cannot be solved (when constructed over several steps) @@ -86,19 +92,23 @@ fn indirect_cycle_2() { term("exists {} => {B = A, A = Vec}"), ).assert_err( expect![[r#" - judgment `prove_wc_list { goal: {?ty_0 = Vec, ?ty_1 = ?ty_0}, assumptions: {}, env: Env { variables: [?ty_0, ?ty_1], bias: Soundness }, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "some" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove_after { constraints: Constraints { env: Env { variables: [?ty_2, ?ty_0, ?ty_1], bias: Soundness }, known_true: true, substitution: {?ty_0 => Vec, ?ty_1 => ?ty_2} }, goal: {?ty_1 = ?ty_0}, assumptions: {}, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {?ty_0 = Vec}, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness }, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` 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 = Vec, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness }, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "eq" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_eq { a: ?ty_0, b: Vec, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness }, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "existential" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_existential_var_eq { v: ?ty_0, b: Vec, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness }, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "existential-nonvar" failed at step #1 (src/file.rs:LL:CC) because - judgment `equate_variable` failed at the following rule(s): - failed at (src/file.rs:LL:CC) because - `?ty_0` occurs in `Vec`"#]]); + judgment `prove { goal: {?ty_0 = Vec, ?ty_1 = ?ty_0}, assumptions: {}, env: Env { variables: [?ty_0, ?ty_1], bias: Soundness }, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s): + failed at (src/file.rs:LL:CC) because + judgment `prove_wc_list { goal: {?ty_0 = Vec, ?ty_1 = ?ty_0}, assumptions: {}, env: Env { variables: [?ty_0, ?ty_1], bias: Soundness } }` failed at the following rule(s): + the rule "some" failed at step #1 (src/file.rs:LL:CC) because + judgment `prove_after { constraints: Constraints { env: Env { variables: [?ty_2, ?ty_0, ?ty_1], bias: Soundness }, known_true: true, substitution: {?ty_0 => Vec, ?ty_1 => ?ty_2} }, goal: {?ty_1 = ?ty_0}, assumptions: {} }` failed at the following rule(s): + the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because + judgment `prove { goal: {?ty_0 = Vec}, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness }, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s): + failed at (src/file.rs:LL:CC) because + judgment `prove_wc_list { goal: {?ty_0 = Vec}, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness } }` 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 = Vec, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness } }` failed at the following rule(s): + the rule "eq" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_eq { a: ?ty_0, b: Vec, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness } }` failed at the following rule(s): + the rule "existential" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_existential_var_eq { v: ?ty_0, b: Vec, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness } }` failed at the following rule(s): + the rule "existential-nonvar" failed at step #1 (src/file.rs:LL:CC) because + judgment `equate_variable` failed at the following rule(s): + failed at (src/file.rs:LL:CC) because + `?ty_0` occurs in `Vec`"#]]); } diff --git a/crates/formality-prove/src/test/universes.rs b/crates/formality-prove/src/test/universes.rs index 88511bd1..2686ff03 100644 --- a/crates/formality-prove/src/test/universes.rs +++ b/crates/formality-prove/src/test/universes.rs @@ -12,21 +12,23 @@ fn exists_u_for_t() { let decls = Decls::empty(); test_prove(decls, term("exists {} => {for T = U}")).assert_err( expect![[r#" - judgment `prove_wc_list { goal: {for ^ty0_0 = ?ty_0}, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness }, 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: for ^ty0_0 = ?ty_0, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "forall" failed at step #2 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: !ty_1 = ?ty_0, assumptions: {}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness }, 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], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): - 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], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "existential" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_existential_var_eq { v: ?ty_0, b: !ty_1, assumptions: {}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "existential-nonvar" failed at step #0 (src/file.rs:LL:CC) because - 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)`"#]]); + judgment `prove { goal: {for ^ty0_0 = ?ty_0}, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + failed at (src/file.rs:LL:CC) because + judgment `prove_wc_list { goal: {for ^ty0_0 = ?ty_0}, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness } }` failed at the following rule(s): + the rule "some" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: for ^ty0_0 = ?ty_0, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness } }` failed at the following rule(s): + the rule "forall" failed at step #2 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: !ty_1 = ?ty_0, assumptions: {}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness } }` 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], bias: Soundness } }` failed at the following rule(s): + 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], bias: Soundness } }` failed at the following rule(s): + the rule "existential" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_existential_var_eq { v: ?ty_0, b: !ty_1, assumptions: {}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness } }` failed at the following rule(s): + the rule "existential-nonvar" failed at step #0 (src/file.rs:LL:CC) because + 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)`"#]]); } /// There is U that is equal to some T. diff --git a/src/test/coherence_orphan.rs b/src/test/coherence_orphan.rs index a4e1807b..b8cf61a6 100644 --- a/src/test/coherence_orphan.rs +++ b/src/test/coherence_orphan.rs @@ -19,25 +19,27 @@ fn neg_CoreTrait_for_CoreStruct_in_Foo() { orphan_check_neg(impl ! CoreTrait for CoreStruct {}) Caused by: - judgment `prove_wc_list { goal: {@ IsLocal(CoreTrait(CoreStruct))}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait CoreTrait ], [], [impl ! CoreTrait(CoreStruct)], [], [], [adt CoreStruct ], {}, {}) }` failed at the following rule(s): - the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: @ IsLocal(CoreTrait(CoreStruct)), assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait CoreTrait ], [], [impl ! CoreTrait(CoreStruct)], [], [], [adt CoreStruct ], {}, {}) }` 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: CoreTrait(CoreStruct), assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait CoreTrait ], [], [impl ! CoreTrait(CoreStruct)], [], [], [adt CoreStruct ], {}, {}) }` 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: CoreStruct, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait CoreTrait ], [], [impl ! CoreTrait(CoreStruct)], [], [], [adt CoreStruct ], {}, {}) }` failed at the following rule(s): - the rule "fundamental rigid type" failed at step #0 (src/file.rs:LL:CC) because - condition evaluted to false: `is_fundamental(&decls, &name)` - &decls = decls(222, [trait CoreTrait ], [], [impl ! CoreTrait(CoreStruct)], [], [], [adt CoreStruct ], {}, {}) - &name = (adt CoreStruct) - the rule "local rigid type" failed at step #0 (src/file.rs:LL:CC) because - condition evaluted to false: `decls.is_local_adt_id(&a)` + judgment `prove { goal: {@ IsLocal(CoreTrait(CoreStruct))}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait CoreTrait ], [], [impl ! CoreTrait(CoreStruct)], [], [], [adt CoreStruct ], {}, {}) }` failed at the following rule(s): + failed at (src/file.rs:LL:CC) because + judgment `prove_wc_list { goal: {@ IsLocal(CoreTrait(CoreStruct))}, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "some" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: @ IsLocal(CoreTrait(CoreStruct)), assumptions: {}, env: Env { variables: [], bias: Soundness } }` 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: CoreTrait(CoreStruct), assumptions: {}, env: Env { variables: [], bias: Soundness } }` 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: CoreStruct, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "fundamental rigid type" failed at step #0 (src/file.rs:LL:CC) because + condition evaluted to false: `is_fundamental(&decls, &name)` + &decls = decls(222, [trait CoreTrait ], [], [impl ! CoreTrait(CoreStruct)], [], [], [adt CoreStruct ], {}, {}) + &name = (adt CoreStruct) + the rule "local rigid type" failed at step #0 (src/file.rs:LL:CC) because + condition evaluted to false: `decls.is_local_adt_id(&a)` + decls = decls(222, [trait CoreTrait ], [], [impl ! CoreTrait(CoreStruct)], [], [], [adt CoreStruct ], {}, {}) + &a = CoreStruct + 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)` decls = decls(222, [trait CoreTrait ], [], [impl ! CoreTrait(CoreStruct)], [], [], [adt CoreStruct ], {}, {}) - &a = CoreStruct - 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)` - decls = decls(222, [trait CoreTrait ], [], [impl ! CoreTrait(CoreStruct)], [], [], [adt CoreStruct ], {}, {}) - &goal.trait_id = CoreTrait"#]] + &goal.trait_id = CoreTrait"#]] ) } @@ -68,27 +70,29 @@ fn mirror_CoreStruct() { orphan_check(impl CoreTrait for ::Assoc { }) Caused by: - judgment `prove_wc_list { goal: {@ IsLocal(CoreTrait(::Assoc))}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait CoreTrait , trait Mirror ], [impl Mirror(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Mirror>::Assoc = ^ty0_0], [], [adt CoreStruct ], {}, {}) }` failed at the following rule(s): - the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: @ IsLocal(CoreTrait(::Assoc)), assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait CoreTrait , trait Mirror ], [impl Mirror(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Mirror>::Assoc = ^ty0_0], [], [adt CoreStruct ], {}, {}) }` 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: CoreTrait(::Assoc), assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait CoreTrait , trait Mirror ], [impl Mirror(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Mirror>::Assoc = ^ty0_0], [], [adt CoreStruct ], {}, {}) }` 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: ::Assoc, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait CoreTrait , trait Mirror ], [impl Mirror(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Mirror>::Assoc = ^ty0_0], [], [adt CoreStruct ], {}, {}) }` failed at the following rule(s): - the rule "local parameter" failed at step #2 (src/file.rs:LL:CC) because - judgment `is_local_parameter { goal: CoreStruct, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait CoreTrait , trait Mirror ], [impl Mirror(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Mirror>::Assoc = ^ty0_0], [], [adt CoreStruct ], {}, {}) }` failed at the following rule(s): - the rule "fundamental rigid type" failed at step #0 (src/file.rs:LL:CC) because - condition evaluted to false: `is_fundamental(&decls, &name)` - &decls = decls(222, [trait CoreTrait , trait Mirror ], [impl Mirror(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Mirror>::Assoc = ^ty0_0], [], [adt CoreStruct ], {}, {}) - &name = (adt CoreStruct) - the rule "local rigid type" failed at step #0 (src/file.rs:LL:CC) because - condition evaluted to false: `decls.is_local_adt_id(&a)` - decls = decls(222, [trait CoreTrait , trait Mirror ], [impl Mirror(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Mirror>::Assoc = ^ty0_0], [], [adt CoreStruct ], {}, {}) - &a = CoreStruct - 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)` - decls = decls(222, [trait CoreTrait , trait Mirror ], [impl Mirror(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Mirror>::Assoc = ^ty0_0], [], [adt CoreStruct ], {}, {}) - &goal.trait_id = CoreTrait"#]] + judgment `prove { goal: {@ IsLocal(CoreTrait(::Assoc))}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait CoreTrait , trait Mirror ], [impl Mirror(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Mirror>::Assoc = ^ty0_0], [], [adt CoreStruct ], {}, {}) }` failed at the following rule(s): + failed at (src/file.rs:LL:CC) because + judgment `prove_wc_list { goal: {@ IsLocal(CoreTrait(::Assoc))}, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "some" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: @ IsLocal(CoreTrait(::Assoc)), assumptions: {}, env: Env { variables: [], bias: Soundness } }` 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: CoreTrait(::Assoc), assumptions: {}, env: Env { variables: [], bias: Soundness } }` 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: ::Assoc, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "local parameter" failed at step #2 (src/file.rs:LL:CC) because + judgment `is_local_parameter { goal: CoreStruct, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "fundamental rigid type" failed at step #0 (src/file.rs:LL:CC) because + condition evaluted to false: `is_fundamental(&decls, &name)` + &decls = decls(222, [trait CoreTrait , trait Mirror ], [impl Mirror(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Mirror>::Assoc = ^ty0_0], [], [adt CoreStruct ], {}, {}) + &name = (adt CoreStruct) + the rule "local rigid type" failed at step #0 (src/file.rs:LL:CC) because + condition evaluted to false: `decls.is_local_adt_id(&a)` + decls = decls(222, [trait CoreTrait , trait Mirror ], [impl Mirror(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Mirror>::Assoc = ^ty0_0], [], [adt CoreStruct ], {}, {}) + &a = CoreStruct + 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)` + decls = decls(222, [trait CoreTrait , trait Mirror ], [impl Mirror(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Mirror>::Assoc = ^ty0_0], [], [adt CoreStruct ], {}, {}) + &goal.trait_id = CoreTrait"#]] ) } @@ -154,15 +158,17 @@ fn uncovered_T() { orphan_check(impl CoreTrait for ^ty0_0 { }) Caused by: - judgment `prove_wc_list { goal: {@ IsLocal(CoreTrait(!ty_0, FooStruct))}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait CoreTrait ], [impl CoreTrait(^ty0_0, FooStruct)], [], [], [], [adt FooStruct ], {}, {FooStruct}) }` failed at the following rule(s): - the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: @ IsLocal(CoreTrait(!ty_0, FooStruct)), assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait CoreTrait ], [impl CoreTrait(^ty0_0, FooStruct)], [], [], [], [adt FooStruct ], {}, {FooStruct}) }` 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: CoreTrait(!ty_0, FooStruct), assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait CoreTrait ], [impl CoreTrait(^ty0_0, FooStruct)], [], [], [], [adt FooStruct ], {}, {FooStruct}) }` failed at the following rule(s): - 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)` - decls = decls(222, [trait CoreTrait ], [impl CoreTrait(^ty0_0, FooStruct)], [], [], [], [adt FooStruct ], {}, {FooStruct}) - &goal.trait_id = CoreTrait"#]] + judgment `prove { goal: {@ IsLocal(CoreTrait(!ty_0, FooStruct))}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait CoreTrait ], [impl CoreTrait(^ty0_0, FooStruct)], [], [], [], [adt FooStruct ], {}, {FooStruct}) }` failed at the following rule(s): + failed at (src/file.rs:LL:CC) because + judgment `prove_wc_list { goal: {@ IsLocal(CoreTrait(!ty_0, FooStruct))}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s): + the rule "some" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: @ IsLocal(CoreTrait(!ty_0, FooStruct)), assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness } }` 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: CoreTrait(!ty_0, FooStruct), assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s): + 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)` + decls = decls(222, [trait CoreTrait ], [impl CoreTrait(^ty0_0, FooStruct)], [], [], [], [adt FooStruct ], {}, {FooStruct}) + &goal.trait_id = CoreTrait"#]] ) } @@ -193,23 +199,25 @@ fn alias_to_unit() { orphan_check(impl CoreTrait for ::Assoc { }) Caused by: - judgment `prove_wc_list { goal: {@ IsLocal(CoreTrait(::Assoc))}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait CoreTrait , trait Unit ], [impl Unit(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Unit>::Assoc = ()], [], [adt FooStruct ], {}, {FooStruct}) }` failed at the following rule(s): - the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: @ IsLocal(CoreTrait(::Assoc)), assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait CoreTrait , trait Unit ], [impl Unit(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Unit>::Assoc = ()], [], [adt FooStruct ], {}, {FooStruct}) }` 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: CoreTrait(::Assoc), assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait CoreTrait , trait Unit ], [impl Unit(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Unit>::Assoc = ()], [], [adt FooStruct ], {}, {FooStruct}) }` 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: ::Assoc, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait CoreTrait , trait Unit ], [impl Unit(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Unit>::Assoc = ()], [], [adt FooStruct ], {}, {FooStruct}) }` failed at the following rule(s): - the rule "local parameter" failed at step #2 (src/file.rs:LL:CC) because - judgment `is_local_parameter { goal: (), assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait CoreTrait , trait Unit ], [impl Unit(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Unit>::Assoc = ()], [], [adt FooStruct ], {}, {FooStruct}) }` failed at the following rule(s): - the rule "fundamental rigid type" failed at step #0 (src/file.rs:LL:CC) because - condition evaluted to false: `is_fundamental(&decls, &name)` - &decls = decls(222, [trait CoreTrait , trait Unit ], [impl Unit(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Unit>::Assoc = ()], [], [adt FooStruct ], {}, {FooStruct}) - &name = tuple(0) - 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)` - decls = decls(222, [trait CoreTrait , trait Unit ], [impl Unit(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Unit>::Assoc = ()], [], [adt FooStruct ], {}, {FooStruct}) - &goal.trait_id = CoreTrait"#]] + judgment `prove { goal: {@ IsLocal(CoreTrait(::Assoc))}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait CoreTrait , trait Unit ], [impl Unit(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Unit>::Assoc = ()], [], [adt FooStruct ], {}, {FooStruct}) }` failed at the following rule(s): + failed at (src/file.rs:LL:CC) because + judgment `prove_wc_list { goal: {@ IsLocal(CoreTrait(::Assoc))}, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "some" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: @ IsLocal(CoreTrait(::Assoc)), assumptions: {}, env: Env { variables: [], bias: Soundness } }` 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: CoreTrait(::Assoc), assumptions: {}, env: Env { variables: [], bias: Soundness } }` 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: ::Assoc, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "local parameter" failed at step #2 (src/file.rs:LL:CC) because + judgment `is_local_parameter { goal: (), assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "fundamental rigid type" failed at step #0 (src/file.rs:LL:CC) because + condition evaluted to false: `is_fundamental(&decls, &name)` + &decls = decls(222, [trait CoreTrait , trait Unit ], [impl Unit(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Unit>::Assoc = ()], [], [adt FooStruct ], {}, {FooStruct}) + &name = tuple(0) + 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)` + decls = decls(222, [trait CoreTrait , trait Unit ], [impl Unit(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Unit>::Assoc = ()], [], [adt FooStruct ], {}, {FooStruct}) + &goal.trait_id = CoreTrait"#]] ) } @@ -232,25 +240,27 @@ fn CoreTrait_for_CoreStruct_in_Foo() { orphan_check(impl CoreTrait for CoreStruct { }) Caused by: - judgment `prove_wc_list { goal: {@ IsLocal(CoreTrait(CoreStruct))}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait CoreTrait ], [impl CoreTrait(CoreStruct)], [], [], [], [adt CoreStruct ], {}, {}) }` failed at the following rule(s): - the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: @ IsLocal(CoreTrait(CoreStruct)), assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait CoreTrait ], [impl CoreTrait(CoreStruct)], [], [], [], [adt CoreStruct ], {}, {}) }` 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: CoreTrait(CoreStruct), assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait CoreTrait ], [impl CoreTrait(CoreStruct)], [], [], [], [adt CoreStruct ], {}, {}) }` 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: CoreStruct, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait CoreTrait ], [impl CoreTrait(CoreStruct)], [], [], [], [adt CoreStruct ], {}, {}) }` failed at the following rule(s): - the rule "fundamental rigid type" failed at step #0 (src/file.rs:LL:CC) because - condition evaluted to false: `is_fundamental(&decls, &name)` - &decls = decls(222, [trait CoreTrait ], [impl CoreTrait(CoreStruct)], [], [], [], [adt CoreStruct ], {}, {}) - &name = (adt CoreStruct) - the rule "local rigid type" failed at step #0 (src/file.rs:LL:CC) because - condition evaluted to false: `decls.is_local_adt_id(&a)` + judgment `prove { goal: {@ IsLocal(CoreTrait(CoreStruct))}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait CoreTrait ], [impl CoreTrait(CoreStruct)], [], [], [], [adt CoreStruct ], {}, {}) }` failed at the following rule(s): + failed at (src/file.rs:LL:CC) because + judgment `prove_wc_list { goal: {@ IsLocal(CoreTrait(CoreStruct))}, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "some" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: @ IsLocal(CoreTrait(CoreStruct)), assumptions: {}, env: Env { variables: [], bias: Soundness } }` 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: CoreTrait(CoreStruct), assumptions: {}, env: Env { variables: [], bias: Soundness } }` 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: CoreStruct, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "fundamental rigid type" failed at step #0 (src/file.rs:LL:CC) because + condition evaluted to false: `is_fundamental(&decls, &name)` + &decls = decls(222, [trait CoreTrait ], [impl CoreTrait(CoreStruct)], [], [], [], [adt CoreStruct ], {}, {}) + &name = (adt CoreStruct) + the rule "local rigid type" failed at step #0 (src/file.rs:LL:CC) because + condition evaluted to false: `decls.is_local_adt_id(&a)` + decls = decls(222, [trait CoreTrait ], [impl CoreTrait(CoreStruct)], [], [], [], [adt CoreStruct ], {}, {}) + &a = CoreStruct + 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)` decls = decls(222, [trait CoreTrait ], [impl CoreTrait(CoreStruct)], [], [], [], [adt CoreStruct ], {}, {}) - &a = CoreStruct - 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)` - decls = decls(222, [trait CoreTrait ], [impl CoreTrait(CoreStruct)], [], [], [], [adt CoreStruct ], {}, {}) - &goal.trait_id = CoreTrait"#]] + &goal.trait_id = CoreTrait"#]] ) } diff --git a/src/test/consts.rs b/src/test/consts.rs index 1409ae25..730d6651 100644 --- a/src/test/consts.rs +++ b/src/test/consts.rs @@ -18,25 +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_wc_list { 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 where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], {Foo}, {}) }` 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 }, decls: decls(222, [trait Foo where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], {Foo}, {}) }` 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 }, decls: decls(222, [trait Foo where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], {Foo}, {}) }` - 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 }, decls: decls(222, [trait Foo where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], {Foo}, {}) }` 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 }, decls: decls(222, [trait Foo where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], {Foo}, {}) }` 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 }, decls: decls(222, [trait Foo where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], {Foo}, {}) }` - 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 }, decls: decls(222, [trait Foo 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 }, decls: decls(222, [trait Foo 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): + 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): + 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 } }` + 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): 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 }, decls: decls(222, [trait Foo where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): + judgment `prove_normalize { p: u32, assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], bias: Soundness } }` 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 }, decls: decls(222, [trait Foo where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], {Foo}, {}) }` + 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 } }` 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 }, decls: decls(222, [trait Foo where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], {Foo}, {}) }`"#]] + judgment `prove_eq { a: bool, b: u32, assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], bias: Soundness } }` 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): + 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 } }` + 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 } }`"#]] ) } @@ -74,11 +76,13 @@ fn mismatch() { check_trait_impl(impl Foo for u32 { }) Caused by: - judgment `prove_wc_list { goal: {Foo(u32, const value(42, u32))}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo where {@ ConstHasType(^const0_1 , bool)}], [impl Foo(u32, const value(42, u32))], [], [], [], [], {Foo}, {}) }` 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 }, decls: decls(222, [trait Foo where {@ ConstHasType(^const0_1 , bool)}], [impl Foo(u32, const value(42, u32))], [], [], [], [], {Foo}, {}) }` 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()`"#]] + judgment `prove { goal: {Foo(u32, const value(42, u32))}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo 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): + 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): + the rule "trait implied bound" failed at step #0 (src/file.rs:LL:CC) because + expression evaluated to an empty collection: `decls.trait_invariants()`"#]] ) } @@ -131,19 +135,23 @@ fn generic_mismatch() { check_trait_impl(impl Foo for u32 where type_of_const ^const0_0 is u32 { }) Caused by: - judgment `prove_wc_list { goal: {Foo(u32, const !const_0)}, assumptions: {@ ConstHasType(!const_0 , u32)}, env: Env { variables: [!const_0], bias: Soundness }, decls: decls(222, [trait Foo where {@ ConstHasType(^const0_1 , bool)}], [impl Foo(u32, const ^const0_0) where {@ ConstHasType(^const0_0 , u32)}], [], [], [], [], {Foo}, {}) }` 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 }, decls: decls(222, [trait Foo where {@ ConstHasType(^const0_1 , bool)}], [impl Foo(u32, const ^const0_0) where {@ ConstHasType(^const0_0 , u32)}], [], [], [], [], {Foo}, {}) }` 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)}, decls: decls(222, [trait Foo where {@ ConstHasType(^const0_1 , bool)}], [impl Foo(u32, const ^const0_0) where {@ ConstHasType(^const0_0 , u32)}], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): - the rule "prove_after" failed at step #1 (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 }, decls: decls(222, [trait Foo where {@ ConstHasType(^const0_1 , bool)}], [impl Foo(u32, const ^const0_0) where {@ ConstHasType(^const0_0 , u32)}], [], [], [], [], {Foo}, {}) }` 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 }, decls: decls(222, [trait Foo where {@ ConstHasType(^const0_1 , bool)}], [impl Foo(u32, const ^const0_0) where {@ ConstHasType(^const0_0 , u32)}], [], [], [], [], {Foo}, {}) }` 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 - expression evaluated to an empty collection: `decls.trait_invariants()`"#]] + 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 where {@ ConstHasType(^const0_1 , bool)}], [impl 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): + 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): + 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): + 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 where {@ ConstHasType(^const0_1 , bool)}], [impl 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): + 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): + 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 + expression evaluated to an empty collection: `decls.trait_invariants()`"#]] ) } diff --git a/src/test/functions.rs b/src/test/functions.rs index ac4eabda..07c21766 100644 --- a/src/test/functions.rs +++ b/src/test/functions.rs @@ -42,10 +42,12 @@ fn lifetime() { [ /* TODO */ ] expect_test::expect![[r#" - judgment `prove_wc_list { 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): - 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 }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` 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 }, decls: decls(222, [], [], [], [], [], [], {}, {}) }`"#]] + 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): + 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): + 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): + 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 } }`"#]] ) } diff --git a/src/test/mod.rs b/src/test/mod.rs index 593fa85f..0a71b906 100644 --- a/src/test/mod.rs +++ b/src/test/mod.rs @@ -46,15 +46,19 @@ fn hello_world_fail() { Caused by: 0: prove_where_clauses_well_formed([!ty_2 : Bar ]) - 1: judgment `prove_wc_list { goal: {@ WellFormedTraitRef(Bar(!ty_0, !ty_1))}, assumptions: {Bar(!ty_0, !ty_1)}, env: Env { variables: [!ty_1, !ty_0], bias: Soundness }, decls: decls(222, [trait Foo where {Bar(^ty0_1, ^ty0_0)}, trait Bar where {Baz(^ty0_1)}, trait Baz ], [], [], [], [], [], {Bar, Baz, Foo}, {}) }` failed at the following rule(s): - the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: @ WellFormedTraitRef(Bar(!ty_0, !ty_1)), assumptions: {Bar(!ty_0, !ty_1)}, env: Env { variables: [!ty_1, !ty_0], bias: Soundness }, decls: decls(222, [trait Foo where {Bar(^ty0_1, ^ty0_0)}, trait Bar where {Baz(^ty0_1)}, trait Baz ], [], [], [], [], [], {Bar, Baz, Foo}, {}) }` failed at the following rule(s): - the rule "trait well formed" failed at step #2 (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {Baz(!ty_1)}, assumptions: {Bar(!ty_0, !ty_1)}, env: Env { variables: [!ty_1, !ty_0], bias: Soundness }, decls: decls(222, [trait Foo where {Bar(^ty0_1, ^ty0_0)}, trait Bar where {Baz(^ty0_1)}, trait Baz ], [], [], [], [], [], {Bar, Baz, Foo}, {}) }` failed at the following rule(s): - the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: Baz(!ty_1), assumptions: {Bar(!ty_0, !ty_1)}, env: Env { variables: [!ty_1, !ty_0], bias: Soundness }, decls: decls(222, [trait Foo where {Bar(^ty0_1, ^ty0_0)}, trait Bar where {Baz(^ty0_1)}, trait Baz ], [], [], [], [], [], {Bar, Baz, Foo}, {}) }` 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()`"#]] + 1: judgment `prove { goal: {@ WellFormedTraitRef(Bar(!ty_0, !ty_1))}, assumptions: {Bar(!ty_0, !ty_1)}, env: Env { variables: [!ty_1, !ty_0], bias: Soundness }, decls: decls(222, [trait Foo where {Bar(^ty0_1, ^ty0_0)}, trait Bar where {Baz(^ty0_1)}, trait Baz ], [], [], [], [], [], {Bar, Baz, Foo}, {}) }` failed at the following rule(s): + failed at (src/file.rs:LL:CC) because + judgment `prove_wc_list { goal: {@ WellFormedTraitRef(Bar(!ty_0, !ty_1))}, assumptions: {Bar(!ty_0, !ty_1)}, env: Env { variables: [!ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + the rule "some" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: @ WellFormedTraitRef(Bar(!ty_0, !ty_1)), assumptions: {Bar(!ty_0, !ty_1)}, env: Env { variables: [!ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + the rule "trait well formed" failed at step #2 (src/file.rs:LL:CC) because + judgment `prove { goal: {Baz(!ty_1)}, assumptions: {Bar(!ty_0, !ty_1)}, env: Env { variables: [!ty_1, !ty_0], bias: Soundness }, decls: decls(222, [trait Foo where {Bar(^ty0_1, ^ty0_0)}, trait Bar where {Baz(^ty0_1)}, trait Baz ], [], [], [], [], [], {Bar, Baz, Foo}, {}) }` failed at the following rule(s): + failed at (src/file.rs:LL:CC) because + judgment `prove_wc_list { goal: {Baz(!ty_1)}, assumptions: {Bar(!ty_0, !ty_1)}, env: Env { variables: [!ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + the rule "some" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: Baz(!ty_1), assumptions: {Bar(!ty_0, !ty_1)}, env: Env { variables: [!ty_1, !ty_0], bias: Soundness } }` 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()`"#]] ) } @@ -121,17 +125,21 @@ fn basic_where_clauses_fail() { Caused by: 0: prove_where_clauses_well_formed([for u32 : A <^ty0_0>]) - 1: judgment `prove_wc_list { goal: {for @ WellFormedTraitRef(A(u32, ^ty0_0))}, assumptions: {for A(u32, ^ty0_0)}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait A where {B(^ty0_1)}, trait B , trait WellFormed where {for A(u32, ^ty0_0)}], [], [], [], [], [], {A, B, WellFormed}, {}) }` failed at the following rule(s): - the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: for @ WellFormedTraitRef(A(u32, ^ty0_0)), assumptions: {for A(u32, ^ty0_0)}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait A where {B(^ty0_1)}, trait B , trait WellFormed where {for A(u32, ^ty0_0)}], [], [], [], [], [], {A, B, WellFormed}, {}) }` failed at the following rule(s): - the rule "forall" failed at step #2 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: @ WellFormedTraitRef(A(u32, !ty_1)), assumptions: {for A(u32, ^ty0_0)}, env: Env { variables: [!ty_1], bias: Soundness }, decls: decls(222, [trait A where {B(^ty0_1)}, trait B , trait WellFormed where {for A(u32, ^ty0_0)}], [], [], [], [], [], {A, B, WellFormed}, {}) }` failed at the following rule(s): - the rule "trait well formed" failed at step #2 (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {B(!ty_0)}, assumptions: {for A(u32, ^ty0_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait A where {B(^ty0_1)}, trait B , trait WellFormed where {for A(u32, ^ty0_0)}], [], [], [], [], [], {A, B, WellFormed}, {}) }` failed at the following rule(s): - the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: B(!ty_0), assumptions: {for A(u32, ^ty0_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait A where {B(^ty0_1)}, trait B , trait WellFormed where {for A(u32, ^ty0_0)}], [], [], [], [], [], {A, B, WellFormed}, {}) }` 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()`"#]] + 1: judgment `prove { goal: {for @ WellFormedTraitRef(A(u32, ^ty0_0))}, assumptions: {for A(u32, ^ty0_0)}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait A where {B(^ty0_1)}, trait B , trait WellFormed where {for A(u32, ^ty0_0)}], [], [], [], [], [], {A, B, WellFormed}, {}) }` failed at the following rule(s): + failed at (src/file.rs:LL:CC) because + judgment `prove_wc_list { goal: {for @ WellFormedTraitRef(A(u32, ^ty0_0))}, assumptions: {for A(u32, ^ty0_0)}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "some" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: for @ WellFormedTraitRef(A(u32, ^ty0_0)), assumptions: {for A(u32, ^ty0_0)}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "forall" failed at step #2 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: @ WellFormedTraitRef(A(u32, !ty_1)), assumptions: {for A(u32, ^ty0_0)}, env: Env { variables: [!ty_1], bias: Soundness } }` failed at the following rule(s): + the rule "trait well formed" failed at step #2 (src/file.rs:LL:CC) because + judgment `prove { goal: {B(!ty_0)}, assumptions: {for A(u32, ^ty0_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait A where {B(^ty0_1)}, trait B , trait WellFormed where {for A(u32, ^ty0_0)}], [], [], [], [], [], {A, B, WellFormed}, {}) }` failed at the following rule(s): + failed at (src/file.rs:LL:CC) because + judgment `prove_wc_list { goal: {B(!ty_0)}, assumptions: {for A(u32, ^ty0_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s): + the rule "some" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: B(!ty_0), assumptions: {for A(u32, ^ty0_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` 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()`"#]] ) }