Skip to content

Commit 3d53247

Browse files
nikomatsakisnikomatsakis
authored
Merge pull request #190 from mattheww/2025-01_well_formed_trait_ref
When proving WellFormedTraitRef, require the parameters to be well-formed
2 parents 0e53834 + ffcdf88 commit 3d53247

File tree

4 files changed

+192
-19
lines changed

4 files changed

+192
-19
lines changed

‎crates/formality-prove/src/prove/prove_wc.rs

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@ use formality_types::grammar::{Predicate, Relation, Wc, WcData, Wcs};
44
use crate::{
55
decls::Decls,
66
prove::{
7+
combinators::for_all,
78
env::{Bias, Env},
89
is_local::{is_local_trait_ref, may_be_remote},
910
prove,
@@ -105,9 +106,10 @@ judgment_fn! {
105106
)
106107

107108
(
108-
(let t = decls.trait_decl(&trait_ref.trait_id))
109+
(for_all(&decls, &env, &assumptions, &trait_ref.parameters, &prove_wf) => c)
110+
(let t = &decls.trait_decl(&trait_ref.trait_id))
109111
(let t = t.binder.instantiate_with(&trait_ref.parameters).unwrap())
110-
(prove(decls, env, assumptions, t.where_clause) => c)
112+
(prove_after(&decls, c, &assumptions, t.where_clause) => c)
111113
----------------------------- ("trait well formed")
112114
(prove_wc(decls, env, assumptions, Predicate::WellFormedTraitRef(trait_ref)) => c)
113115
)

‎crates/formality-prove/src/prove/prove_wf.rs

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
use formality_core::{judgment_fn, ProvenSet};
22
use formality_types::grammar::{
3-
AliasName, AliasTy, ConstData, Parameter, Parameters, RigidName, RigidTy, UniversalVar, Wcs,
3+
AliasName, AliasTy, ConstData, LtData, Parameter, Parameters, RigidName, RigidTy, UniversalVar,
4+
Wcs,
45
};
56

67
use crate::{
@@ -51,6 +52,11 @@ judgment_fn! {
5152
(prove_wf(decls, env, assumptions, RigidTy { name: RigidName::AdtId(adt_id), parameters }) => c)
5253
)
5354

55+
(
56+
--- ("static lifetime")
57+
(prove_wf(_decls, env, _assumptions, LtData::Static) => Constraints::none(env))
58+
)
59+
5460
(
5561
(prove_wf(&decls, &env, &assumptions, ty) => c)
5662
--- ("rigid constants")

‎src/test/mod.rs

Lines changed: 21 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ mod coherence_overlap;
55
mod consts;
66
mod decl_safety;
77
mod functions;
8+
mod well_formed_trait_ref;
89

910
#[test]
1011
fn parser() {
@@ -51,14 +52,16 @@ fn hello_world_fail() {
5152
judgment `prove_wc_list { goal: {@ WellFormedTraitRef(Bar(!ty_0, !ty_1))}, assumptions: {Bar(!ty_0, !ty_1)}, env: Env { variables: [!ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s):
5253
the rule "some" failed at step #0 (src/file.rs:LL:CC) because
5354
judgment `prove_wc { goal: @ WellFormedTraitRef(Bar(!ty_0, !ty_1)), assumptions: {Bar(!ty_0, !ty_1)}, env: Env { variables: [!ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s):
54-
the rule "trait well formed" failed at step #2 (src/file.rs:LL:CC) because
55-
judgment `prove { goal: {Baz(!ty_1)}, assumptions: {Bar(!ty_0, !ty_1)}, env: Env { variables: [!ty_1, !ty_0], bias: Soundness }, decls: decls(222, [trait Foo <ty, ty> where {Bar(^ty0_1, ^ty0_0)}, trait Bar <ty, ty> where {Baz(^ty0_1)}, trait Baz <ty> ], [], [], [], [], [], {Bar, Baz, Foo}, {}) }` failed at the following rule(s):
56-
failed at (src/file.rs:LL:CC) because
57-
judgment `prove_wc_list { goal: {Baz(!ty_1)}, assumptions: {Bar(!ty_0, !ty_1)}, env: Env { variables: [!ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s):
58-
the rule "some" failed at step #0 (src/file.rs:LL:CC) because
59-
judgment `prove_wc { goal: Baz(!ty_1), assumptions: {Bar(!ty_0, !ty_1)}, env: Env { variables: [!ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s):
60-
the rule "trait implied bound" failed at step #0 (src/file.rs:LL:CC) because
61-
expression evaluated to an empty collection: `decls.trait_invariants()`"#]]
55+
the rule "trait well formed" failed at step #3 (src/file.rs:LL:CC) because
56+
judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_1, !ty_0], bias: Soundness }, known_true: true, substitution: {} }, goal: {Baz(!ty_1)}, assumptions: {Bar(!ty_0, !ty_1)} }` failed at the following rule(s):
57+
the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because
58+
judgment `prove { goal: {Baz(!ty_1)}, assumptions: {Bar(!ty_0, !ty_1)}, env: Env { variables: [!ty_1, !ty_0], bias: Soundness }, decls: decls(222, [trait Foo <ty, ty> where {Bar(^ty0_1, ^ty0_0)}, trait Bar <ty, ty> where {Baz(^ty0_1)}, trait Baz <ty> ], [], [], [], [], [], {Bar, Baz, Foo}, {}) }` failed at the following rule(s):
59+
failed at (src/file.rs:LL:CC) because
60+
judgment `prove_wc_list { goal: {Baz(!ty_1)}, assumptions: {Bar(!ty_0, !ty_1)}, env: Env { variables: [!ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s):
61+
the rule "some" failed at step #0 (src/file.rs:LL:CC) because
62+
judgment `prove_wc { goal: Baz(!ty_1), assumptions: {Bar(!ty_0, !ty_1)}, env: Env { variables: [!ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s):
63+
the rule "trait implied bound" failed at step #0 (src/file.rs:LL:CC) because
64+
expression evaluated to an empty collection: `decls.trait_invariants()`"#]]
6265
)
6366
}
6467

@@ -132,14 +135,16 @@ fn basic_where_clauses_fail() {
132135
judgment `prove_wc { goal: for <ty> @ WellFormedTraitRef(A(u32, ^ty0_0)), assumptions: {for <ty> A(u32, ^ty0_0)}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s):
133136
the rule "forall" failed at step #2 (src/file.rs:LL:CC) because
134137
judgment `prove_wc { goal: @ WellFormedTraitRef(A(u32, !ty_1)), assumptions: {for <ty> A(u32, ^ty0_0)}, env: Env { variables: [!ty_1], bias: Soundness } }` failed at the following rule(s):
135-
the rule "trait well formed" failed at step #2 (src/file.rs:LL:CC) because
136-
judgment `prove { goal: {B(!ty_0)}, assumptions: {for <ty> A(u32, ^ty0_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait A <ty, ty> where {B(^ty0_1)}, trait B <ty> , trait WellFormed <ty> where {for <ty> A(u32, ^ty0_0)}], [], [], [], [], [], {A, B, WellFormed}, {}) }` failed at the following rule(s):
137-
failed at (src/file.rs:LL:CC) because
138-
judgment `prove_wc_list { goal: {B(!ty_0)}, assumptions: {for <ty> A(u32, ^ty0_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s):
139-
the rule "some" failed at step #0 (src/file.rs:LL:CC) because
140-
judgment `prove_wc { goal: B(!ty_0), assumptions: {for <ty> A(u32, ^ty0_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s):
141-
the rule "trait implied bound" failed at step #0 (src/file.rs:LL:CC) because
142-
expression evaluated to an empty collection: `decls.trait_invariants()`"#]]
138+
the rule "trait well formed" failed at step #3 (src/file.rs:LL:CC) because
139+
judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_1], bias: Soundness }, known_true: true, substitution: {} }, goal: {B(!ty_1)}, assumptions: {for <ty> A(u32, ^ty0_0)} }` failed at the following rule(s):
140+
the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because
141+
judgment `prove { goal: {B(!ty_0)}, assumptions: {for <ty> A(u32, ^ty0_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait A <ty, ty> where {B(^ty0_1)}, trait B <ty> , trait WellFormed <ty> where {for <ty> A(u32, ^ty0_0)}], [], [], [], [], [], {A, B, WellFormed}, {}) }` failed at the following rule(s):
142+
failed at (src/file.rs:LL:CC) because
143+
judgment `prove_wc_list { goal: {B(!ty_0)}, assumptions: {for <ty> A(u32, ^ty0_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s):
144+
the rule "some" failed at step #0 (src/file.rs:LL:CC) because
145+
judgment `prove_wc { goal: B(!ty_0), assumptions: {for <ty> A(u32, ^ty0_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s):
146+
the rule "trait implied bound" failed at step #0 (src/file.rs:LL:CC) because
147+
expression evaluated to an empty collection: `decls.trait_invariants()`"#]]
143148
)
144149
}
145150

‎src/test/well_formed_trait_ref.rs

Lines changed: 160 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,160 @@
1+
#[test]
2+
fn dependent_where_clause() {
3+
crate::assert_ok!(
4+
//@check-pass
5+
[
6+
crate foo {
7+
trait Trait1 {}
8+
9+
trait Trait2 {}
10+
11+
struct S1<ty T> where T: Trait1 {
12+
dummy: T,
13+
}
14+
15+
struct S2<ty T> where T: Trait1, S1<T> : Trait2 {
16+
dummy: T,
17+
}
18+
}
19+
]
20+
21+
expect_test::expect!["()"]
22+
)
23+
}
24+
25+
#[test]
26+
fn missing_dependent_where_clause() {
27+
crate::assert_err!(
28+
[
29+
crate foo {
30+
trait Trait1 {}
31+
32+
trait Trait2 {}
33+
34+
struct S1<ty T> where T: Trait1 {
35+
dummy: T,
36+
}
37+
38+
struct S2<ty T> where S1<T> : Trait2 {
39+
dummy: T,
40+
}
41+
}
42+
]
43+
44+
[ /* TODO */ ]
45+
46+
expect_test::expect![[r#"
47+
prove_where_clauses_well_formed([S1<!ty_1> : Trait2])
48+
49+
Caused by:
50+
judgment `prove { goal: {@ WellFormedTraitRef(Trait2(S1<!ty_0>))}, assumptions: {Trait2(S1<!ty_0>)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Trait1 <ty> , trait Trait2 <ty> ], [], [], [], [], [adt S1 <ty> where {Trait1(^ty0_0)}, adt S2 <ty> where {Trait2(S1<^ty0_0>)}], {Trait1, Trait2}, {S1, S2}) }` failed at the following rule(s):
51+
failed at (src/file.rs:LL:CC) because
52+
judgment `prove_wc_list { goal: {@ WellFormedTraitRef(Trait2(S1<!ty_0>))}, assumptions: {Trait2(S1<!ty_0>)}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s):
53+
the rule "some" failed at step #0 (src/file.rs:LL:CC) because
54+
judgment `prove_wc { goal: @ WellFormedTraitRef(Trait2(S1<!ty_0>)), assumptions: {Trait2(S1<!ty_0>)}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s):
55+
the rule "trait well formed" failed at step #0 (src/file.rs:LL:CC) because
56+
judgment `prove_wf { goal: S1<!ty_0>, assumptions: {Trait2(S1<!ty_0>)}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s):
57+
the rule "ADT" failed at step #3 (src/file.rs:LL:CC) because
58+
judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_0], bias: Soundness }, known_true: true, substitution: {} }, goal: {Trait1(!ty_0)}, assumptions: {Trait2(S1<!ty_0>)} }` failed at the following rule(s):
59+
the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because
60+
judgment `prove { goal: {Trait1(!ty_0)}, assumptions: {Trait2(S1<!ty_0>)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Trait1 <ty> , trait Trait2 <ty> ], [], [], [], [], [adt S1 <ty> where {Trait1(^ty0_0)}, adt S2 <ty> where {Trait2(S1<^ty0_0>)}], {Trait1, Trait2}, {S1, S2}) }` failed at the following rule(s):
61+
failed at (src/file.rs:LL:CC) because
62+
judgment `prove_wc_list { goal: {Trait1(!ty_0)}, assumptions: {Trait2(S1<!ty_0>)}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s):
63+
the rule "some" failed at step #0 (src/file.rs:LL:CC) because
64+
judgment `prove_wc { goal: Trait1(!ty_0), assumptions: {Trait2(S1<!ty_0>)}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s):
65+
the rule "trait implied bound" failed at step #0 (src/file.rs:LL:CC) because
66+
expression evaluated to an empty collection: `decls.trait_invariants()`"#]]
67+
)
68+
}
69+
70+
#[test]
71+
fn lifetime_param() {
72+
crate::assert_ok!(
73+
//@check-pass
74+
[
75+
crate foo {
76+
trait Trait1<lt a> {}
77+
78+
struct S1 {}
79+
80+
struct S2<lt a> where S1: Trait1<a> {}
81+
}
82+
]
83+
84+
expect_test::expect!["()"]
85+
)
86+
}
87+
88+
#[test]
89+
fn static_lifetime_param() {
90+
crate::assert_ok!(
91+
//@check-pass
92+
[
93+
crate foo {
94+
trait Trait1<lt a> {}
95+
96+
struct S1 {}
97+
98+
impl Trait1<static> for S1 {}
99+
100+
struct S2 where S1: Trait1<static> {}
101+
}
102+
]
103+
104+
expect_test::expect!["()"]
105+
)
106+
}
107+
108+
#[test]
109+
fn const_param() {
110+
crate::assert_ok!(
111+
//@check-pass
112+
[
113+
crate foo {
114+
trait Trait1<const C> where type_of_const C is u32 {}
115+
116+
struct S1 {}
117+
118+
impl Trait1<const 3_u32> for S1 {}
119+
120+
struct S2 where S1: Trait1<const 3_u32> {}
121+
}
122+
]
123+
124+
expect_test::expect!["()"]
125+
)
126+
}
127+
128+
#[test]
129+
#[should_panic(expected = "wrong number of parameters")]
130+
fn type_with_wrong_number_of_parameters() {
131+
crate::test_program_ok(
132+
" [
133+
crate foo {
134+
trait Trait1 {}
135+
136+
struct S1 {}
137+
138+
struct S2<ty T> where S1<T> : Trait1 {
139+
dummy: T,
140+
}
141+
}
142+
] ",
143+
)
144+
.unwrap();
145+
}
146+
147+
#[test]
148+
#[should_panic(expected = "no ADT named `Nonex`")]
149+
fn where_clause_with_nonexistent_type() {
150+
crate::test_program_ok(
151+
" [
152+
crate foo {
153+
trait Trait1 {}
154+
155+
struct S1 where Nonex: Trait1 {}
156+
}
157+
] ",
158+
)
159+
.unwrap();
160+
}

0 commit comments

Comments
 (0)