From 68b412aafb8c8b86705f2c4c4a86a871b944a1dd Mon Sep 17 00:00:00 2001 From: shua Date: Tue, 2 Jul 2024 18:05:58 +0200 Subject: [PATCH] add some wf checks for fn types --- crates/formality-prove/src/decls.rs | 31 ++++- crates/formality-prove/src/prove/prove_wf.rs | 22 ++++ crates/formality-prove/src/test/adt_wf.rs | 12 +- .../src/test/eq_assumptions.rs | 104 ++++++++--------- .../formality-prove/src/test/eq_partial_eq.rs | 52 ++++----- crates/formality-prove/src/test/is_local.rs | 10 +- crates/formality-prove/src/test/magic_copy.rs | 110 +++++++++--------- .../formality-prove/src/test/occurs_check.rs | 32 ++--- crates/formality-prove/src/test/universes.rs | 12 +- crates/formality-rust/src/prove.rs | 36 +++++- crates/formality-types/src/grammar/ty.rs | 8 ++ .../src/grammar/ty/debug_impls.rs | 19 +++ .../src/grammar/ty/parse_impls.rs | 33 +++++- crates/formality-types/src/lib.rs | 1 + src/test/coherence_orphan.rs | 66 +++++------ src/test/consts.rs | 34 +++--- src/test/functions.rs | 23 ++-- src/test/mod.rs | 18 +-- 18 files changed, 384 insertions(+), 239 deletions(-) diff --git a/crates/formality-prove/src/decls.rs b/crates/formality-prove/src/decls.rs index 00bd5222..6fc36ece 100644 --- a/crates/formality-prove/src/decls.rs +++ b/crates/formality-prove/src/decls.rs @@ -1,8 +1,8 @@ use formality_core::{set, Set, Upcast}; use formality_macros::term; use formality_types::grammar::{ - AdtId, AliasName, AliasTy, Binder, Parameter, Predicate, Relation, TraitId, TraitRef, Ty, Wc, - Wcs, + AdtId, AliasName, AliasTy, Binder, FnId, Parameter, Predicate, Relation, TraitId, TraitRef, Ty, + Wc, Wcs, }; #[term] @@ -16,6 +16,7 @@ pub struct Decls { pub alias_eq_decls: Vec, pub alias_bound_decls: Vec, pub adt_decls: Vec, + pub fn_decls: Vec, pub local_trait_ids: Set, pub local_adt_ids: Set, } @@ -78,6 +79,13 @@ impl Decls { v.pop().unwrap() } + pub fn fn_decl(&self, fn_id: &FnId) -> &FnDecl { + let mut v: Vec<_> = self.fn_decls.iter().filter(|t| t.id == *fn_id).collect(); + assert!(!v.is_empty(), "no fn named `{fn_id:?}`"); + assert!(v.len() <= 1, "multiple fns named `{fn_id:?}`"); + v.pop().unwrap() + } + /// Return the set of "trait invariants" for all traits. /// See [`TraitDecl::trait_invariants`]. pub fn trait_invariants(&self) -> Set { @@ -96,6 +104,7 @@ impl Decls { alias_eq_decls: vec![], alias_bound_decls: vec![], adt_decls: vec![], + fn_decls: vec![], local_trait_ids: set![], local_adt_ids: set![], } @@ -304,3 +313,21 @@ pub struct AdtDeclBoundData { /// The where-clauses declared on the ADT, pub where_clause: Wcs, } + +/// A "function declaration" declares a function name, its generics, its input and ouput types, and its where-clauses. +/// It doesn't currently capture the function body, or input argument names. +/// +/// In Rust syntax, it covers the `fn foo(_: T) -> U where T: Bar` +#[term(fn $id $binder)] +pub struct FnDecl { + pub id: FnId, + pub binder: Binder, +} + +/// The "bound data" for a [`FnDecl`][]. +#[term(($input_tys) -> $output_ty $:where $where_clause)] +pub struct FnDeclBoundData { + pub input_tys: Vec, + pub output_ty: Ty, + pub where_clause: Wcs, +} diff --git a/crates/formality-prove/src/prove/prove_wf.rs b/crates/formality-prove/src/prove/prove_wf.rs index e6c816b6..790b9d92 100644 --- a/crates/formality-prove/src/prove/prove_wf.rs +++ b/crates/formality-prove/src/prove/prove_wf.rs @@ -42,6 +42,13 @@ judgment_fn! { (prove_wf(decls, env, assumptions, RigidTy { name: RigidName::ScalarId(_), parameters }) => c) ) + ( + // only checks that type is well-formed, does not do any lifetime or borrow check + (for_all(&decls, &env, &assumptions, ¶meters, &prove_wf) => c) + --- ("ref") + (prove_wf(decls, env, assumptions, RigidTy { name: RigidName::Ref(_), parameters }) => c) + ) + ( (for_all(&decls, &env, &assumptions, ¶meters, &prove_wf) => c) (let t = decls.adt_decl(&adt_id)) @@ -51,6 +58,21 @@ judgment_fn! { (prove_wf(decls, env, assumptions, RigidTy { name: RigidName::AdtId(adt_id), parameters }) => c) ) + ( + (for_all(&decls, &env, &assumptions, ¶meters, &prove_wf) => c) + (let t = decls.fn_decl(&fn_id)) + (let t = t.binder.instantiate_with(¶meters).unwrap()) + (prove_after(&decls, c, &assumptions, t.where_clause) => c) + --- ("fn-defs") + (prove_wf(decls, env, assumptions, RigidTy { name: RigidName::FnDef(fn_id), parameters }) => c) + ) + + ( + (for_all(&decls, &env, &assumptions, ¶meters, &prove_wf) => c) + --- ("fn-ptr") + (prove_wf(decls, env, assumptions, RigidTy { name: RigidName::FnPtr(_), parameters }) => c) + ) + ( (prove_wf(&decls, &env, &assumptions, ty) => c) --- ("rigid constants") diff --git a/crates/formality-prove/src/test/adt_wf.rs b/crates/formality-prove/src/test/adt_wf.rs index 9cb90867..ea238fda 100644 --- a/crates/formality-prove/src/test/adt_wf.rs +++ b/crates/formality-prove/src/test/adt_wf.rs @@ -51,17 +51,17 @@ 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): + 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): + 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): + 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): + 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): + 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): + 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()`"#]]); } diff --git a/crates/formality-prove/src/test/eq_assumptions.rs b/crates/formality-prove/src/test/eq_assumptions.rs index abba6ed0..ab562f3c 100644 --- a/crates/formality-prove/src/test/eq_assumptions.rs +++ b/crates/formality-prove/src/test/eq_assumptions.rs @@ -52,37 +52,37 @@ 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): + 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): + 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): + 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): + 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): + 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): + 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): + 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): + 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): + 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): + 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_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_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_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_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_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 @@ -90,61 +90,61 @@ fn test_normalize_assoc_ty_existential0() { 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): + 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): + 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): + 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): + 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_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_0 = ?ty_1}, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + 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): + 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): + 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): + 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): + 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): + 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): + 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): + 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): + 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): + 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): + 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): + 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): + 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): + 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): + 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): + 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): + 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): + 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): + 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 @@ -152,41 +152,41 @@ fn test_normalize_assoc_ty_existential0() { 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): + 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): + 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): + 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): + 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): + 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): + 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): + 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): + 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): + 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): + 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): + 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): + 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): + 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): + 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 diff --git a/crates/formality-prove/src/test/eq_partial_eq.rs b/crates/formality-prove/src/test/eq_partial_eq.rs index d1c46c2c..1241dcc4 100644 --- a/crates/formality-prove/src/test/eq_partial_eq.rs +++ b/crates/formality-prove/src/test/eq_partial_eq.rs @@ -44,17 +44,17 @@ 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): + 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): + 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): + 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): + 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 ], [], [], [], [], [], {}, {}) }` + 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 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 ], [], [], [], [], [], [], {}, {}) }`"#]]); } #[test] @@ -63,43 +63,43 @@ 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): + 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): + 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): + 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): + 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 ], [], [], [], [], [], {}, {}) }` + 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): + 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): + 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): + 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): + 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): + 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): + 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 ], [], [], [], [], [], {}, {}) }` + 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): + 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): + 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 ], [], [], [], [], [], {}, {}) }` + 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): + 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): + 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 ], [], [], [], [], [], {}, {}) }` + 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 ], [], [], [], [], [], {}, {}) }` + 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 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 ], [], [], [], [], [], [], {}, {}) }`"#]]); } diff --git a/crates/formality-prove/src/test/is_local.rs b/crates/formality-prove/src/test/is_local.rs index 0c269e54..a1911fa3 100644 --- a/crates/formality-prove/src/test/is_local.rs +++ b/crates/formality-prove/src/test/is_local.rs @@ -13,16 +13,16 @@ 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): + 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): + 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): + 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): + 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, [], [], [], [], [], [], {}, {}) + decls = decls(222, [], [], [], [], [], [], [], {}, {}) &goal.trait_id = Debug"#]]); } diff --git a/crates/formality-prove/src/test/magic_copy.rs b/crates/formality-prove/src/test/magic_copy.rs index 755a9ecd..5d882d08 100644 --- a/crates/formality-prove/src/test/magic_copy.rs +++ b/crates/formality-prove/src/test/magic_copy.rs @@ -25,118 +25,118 @@ 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): + 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): + 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): + 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): + 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): + 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): + 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_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): + 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)], [], [], [], [], {}, {}) }` + 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): + 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): + 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)], [], [], [], [], {}, {}) }` + 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): + 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): + 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)], [], [], [], [], {}, {}) }` + 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)], [], [], [], [], {}, {}) }` + 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): + 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): + 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): + 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): + 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)], [], [], [], [], {}, {}) }` + 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)], [], [], [], [], {}, {}) }` + 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)], [], [], [], [], {}, {}) }`"#]]); + 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): + 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): + 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): + 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): + 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): + 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)], [], [], [], [], {}, {}) }` + 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): + 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): + 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)], [], [], [], [], {}, {}) }` + 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): + 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): + 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)], [], [], [], [], {}, {}) }` + 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)], [], [], [], [], {}, {}) }` + 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): + 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): + 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): + 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): + 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): + 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): + 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_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): + 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)], [], [], [], [], {}, {}) }` + 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): + 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): + 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)], [], [], [], [], {}, {}) }` + 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): + 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): + 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)], [], [], [], [], {}, {}) }` + 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)], [], [], [], [], {}, {}) }` + 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): + 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)], [], [], [], [], {}, {}) }` + 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)], [], [], [], [], {}, {}) }`"#]]); + 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)], [], [], [], [], [], {}, {}) }`"#]]); } diff --git a/crates/formality-prove/src/test/occurs_check.rs b/crates/formality-prove/src/test/occurs_check.rs index f44e0666..7e909a2d 100644 --- a/crates/formality-prove/src/test/occurs_check.rs +++ b/crates/formality-prove/src/test/occurs_check.rs @@ -20,13 +20,13 @@ 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): + 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): + 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): + 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): + 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 @@ -61,17 +61,17 @@ 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): + 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): + 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): + 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): + 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): + 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): + 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 @@ -86,17 +86,17 @@ 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): + 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): + 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): + 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): + 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): + 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): + 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 diff --git a/crates/formality-prove/src/test/universes.rs b/crates/formality-prove/src/test/universes.rs index 88511bd1..a00ea846 100644 --- a/crates/formality-prove/src/test/universes.rs +++ b/crates/formality-prove/src/test/universes.rs @@ -12,17 +12,17 @@ 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): + 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): + 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): + 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): + 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): + 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): + 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 diff --git a/crates/formality-rust/src/prove.rs b/crates/formality-rust/src/prove.rs index e62cbd4d..7ca9e600 100644 --- a/crates/formality-rust/src/prove.rs +++ b/crates/formality-rust/src/prove.rs @@ -1,8 +1,8 @@ use crate::grammar::{ Adt, AdtBoundData, AssociatedTy, AssociatedTyBoundData, AssociatedTyValue, - AssociatedTyValueBoundData, Crate, CrateItem, ImplItem, NegTraitImpl, NegTraitImplBoundData, - Program, Trait, TraitBoundData, TraitImpl, TraitImplBoundData, TraitItem, WhereBound, - WhereBoundData, WhereClause, WhereClauseData, + AssociatedTyValueBoundData, Crate, CrateItem, Fn, FnBoundData, ImplItem, NegTraitImpl, + NegTraitImplBoundData, Program, Trait, TraitBoundData, TraitImpl, TraitImplBoundData, + TraitItem, WhereBound, WhereBoundData, WhereClause, WhereClauseData, }; use formality_core::{seq, Set, To, Upcast, Upcasted}; use formality_prove as prove; @@ -20,6 +20,7 @@ impl Program { alias_eq_decls: self.alias_eq_decls(), alias_bound_decls: self.alias_bound_decls(), adt_decls: self.adt_decls(), + fn_decls: self.fn_decls(), local_trait_ids: self.local_trait_ids(), local_adt_ids: self.local_adt_ids(), } @@ -58,6 +59,10 @@ impl Program { self.crates.iter().flat_map(|c| c.adt_decls()).collect() } + fn fn_decls(&self) -> Vec { + self.crates.iter().flat_map(|c| c.fn_decls()).collect() + } + fn local_trait_ids(&self) -> Set { self.crates .last() @@ -330,6 +335,31 @@ impl Crate { }) .collect() } + + fn fn_decls(&self) -> Vec { + self.items + .iter() + .flat_map(|item| match item { + CrateItem::Fn(f) => Some(f), + _ => None, + }) + .map(|Fn { id, binder }| prove::FnDecl { + id: id.clone(), + binder: binder.map( + |FnBoundData { + input_tys, + output_ty, + where_clauses, + body: _, + }| prove::FnDeclBoundData { + input_tys, + output_ty, + where_clause: where_clauses.to_wcs(), + }, + ), + }) + .collect() + } } pub trait ToWcs { diff --git a/crates/formality-types/src/grammar/ty.rs b/crates/formality-types/src/grammar/ty.rs index 8284e10e..a74f0edb 100644 --- a/crates/formality-types/src/grammar/ty.rs +++ b/crates/formality-types/src/grammar/ty.rs @@ -83,6 +83,14 @@ impl Ty { } .upcast() } + + pub fn unit() -> Ty { + RigidTy { + name: RigidName::Tuple(0), + parameters: vec![], + } + .upcast() + } } impl UpcastFrom for Ty { diff --git a/crates/formality-types/src/grammar/ty/debug_impls.rs b/crates/formality-types/src/grammar/ty/debug_impls.rs index 3b45c435..dd4c535e 100644 --- a/crates/formality-types/src/grammar/ty/debug_impls.rs +++ b/crates/formality-types/src/grammar/ty/debug_impls.rs @@ -32,6 +32,25 @@ impl Debug for RigidTy { write!(f, "()") } } + RigidName::FnDef(name) => { + let parameters = PrettyParameters::new("<", ">", parameters); + write!(f, "{name:?}{parameters:?}",) + } + RigidName::FnPtr(arity) if parameters.len() == *arity + 1 => { + let len = parameters.len(); + if *arity != 0 { + write!( + f, + "{:?}", + PrettyParameters::new("(", ")", ¶meters[..len - 1]) + )?; + } else { + // PrettyParameters would skip the separators + // for 0 arity + write!(f, "()")?; + } + write!(f, "-> {:?}", parameters[len - 1]) + } _ => { write!(f, "{:?}{:?}", name, PrettyParameters::angle(parameters)) } diff --git a/crates/formality-types/src/grammar/ty/parse_impls.rs b/crates/formality-types/src/grammar/ty/parse_impls.rs index 119bd801..f0177f91 100644 --- a/crates/formality-types/src/grammar/ty/parse_impls.rs +++ b/crates/formality-types/src/grammar/ty/parse_impls.rs @@ -7,7 +7,7 @@ use formality_core::Upcast; use formality_core::{seq, Set}; use crate::grammar::{ - AdtId, AssociatedItemId, Bool, ConstData, RefKind, RigidName, Scalar, TraitId, + AdtId, AssociatedItemId, Bool, ConstData, FnId, RefKind, RigidName, Scalar, TraitId, }; use super::{AliasTy, AssociatedTyName, Lt, Parameter, ParameterKind, RigidTy, ScalarId, Ty}; @@ -70,6 +70,37 @@ impl CoreParse for RigidTy { parameters: types.upcast(), }) }); + + parser.parse_variant("Fn", Precedence::default(), |p| { + // parses 'fn name' as fn-def + // or 'fn(params) -> ty' as fn-ptr + p.expect_keyword("fn")?; + + if p.expect_char('(').is_ok() { + p.reject_custom_keywords(&["alias", "rigid", "predicate"])?; + let mut types: Vec = p.comma_nonterminal()?; + p.expect_char(')')?; + let name = RigidName::FnPtr(types.len()); + if p.expect_char('-').is_ok() { + p.expect_char('>')?; + let ret = p.nonterminal()?; + types.push(ret); + } else { + types.push(Ty::unit()); + } + Ok(RigidTy { + name, + parameters: types.upcast(), + }) + } else { + let name: FnId = p.nonterminal()?; + let parameters: Vec = parse_parameters(p)?; + Ok(RigidTy { + name: RigidName::FnDef(name), + parameters, + }) + } + }) }) } } diff --git a/crates/formality-types/src/lib.rs b/crates/formality-types/src/lib.rs index 89adb25c..bc85aa1f 100644 --- a/crates/formality-types/src/lib.rs +++ b/crates/formality-types/src/lib.rs @@ -12,6 +12,7 @@ formality_core::declare_language! { const BINDING_CLOSE = '>'; const KEYWORDS = [ "mut", + "fn", "struct", "enum", "union", diff --git a/src/test/coherence_orphan.rs b/src/test/coherence_orphan.rs index a4e1807b..d8209a50 100644 --- a/src/test/coherence_orphan.rs +++ b/src/test/coherence_orphan.rs @@ -19,24 +19,24 @@ 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): + 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): + 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): + 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): + 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 ], {}, {}) + &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 ], {}, {}) + 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 ], {}, {}) + decls = decls(222, [trait CoreTrait ], [], [impl ! CoreTrait(CoreStruct)], [], [], [adt CoreStruct ], [], {}, {}) &goal.trait_id = CoreTrait"#]] ) } @@ -68,26 +68,26 @@ 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): + 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): + 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): + 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): + 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): + 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 ], {}, {}) + &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 ], {}, {}) + 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 ], {}, {}) + 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,14 +154,14 @@ 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): + 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): + 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): + 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}) + decls = decls(222, [trait CoreTrait ], [impl CoreTrait(^ty0_0, FooStruct)], [], [], [], [adt FooStruct ], [], {}, {FooStruct}) &goal.trait_id = CoreTrait"#]] ) } @@ -193,22 +193,22 @@ 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): + 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): + 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): + 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): + 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): + 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}) + &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}) + 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,24 +232,24 @@ 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): + 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): + 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): + 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): + 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 ], {}, {}) + &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 ], {}, {}) + 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 ], {}, {}) + decls = decls(222, [trait CoreTrait ], [impl CoreTrait(CoreStruct)], [], [], [], [adt CoreStruct ], [], {}, {}) &goal.trait_id = CoreTrait"#]] ) } diff --git a/src/test/consts.rs b/src/test/consts.rs index 1409ae25..81ef5787 100644 --- a/src/test/consts.rs +++ b/src/test/consts.rs @@ -18,25 +18,25 @@ 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): + 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): + 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}, {}) }` + 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): + 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): + 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}, {}) }` + 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): + 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): 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: 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-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: 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 "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}, {}) }`"#]] + 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}, {}) }`"#]] ) } @@ -74,9 +74,9 @@ 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): + 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): + 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()`"#]] ) @@ -131,15 +131,15 @@ 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): + 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): + 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): + 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): + 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): + 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 diff --git a/src/test/functions.rs b/src/test/functions.rs index ac4eabda..2ccb156d 100644 --- a/src/test/functions.rs +++ b/src/test/functions.rs @@ -30,7 +30,7 @@ fn ok() { #[test] fn lifetime() { - crate::assert_err!( + crate::assert_ok!( // Test lifetimes on function [ crate Foo { @@ -39,13 +39,20 @@ fn lifetime() { } ] - [ /* TODO */ ] + expect_test::expect!["()"] + ) +} + +#[test] +fn wf() { + crate::assert_ok!( + [ + crate Foo { + fn foo() -> T { trusted } + fn bar(fn foo, fn(u32) -> (), fn(bool)) -> () { trusted } + } + ] - 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, [], [], [], [], [], [], {}, {}) }`"#]] + expect_test::expect!["()"] ) } diff --git a/src/test/mod.rs b/src/test/mod.rs index 593fa85f..f47e2c95 100644 --- a/src/test/mod.rs +++ b/src/test/mod.rs @@ -46,13 +46,13 @@ 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): + 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): + 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): + 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): + 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()`"#]] ) @@ -121,15 +121,15 @@ 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): + 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): + 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): + 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): + 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): + 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()`"#]] )