Skip to content

Commit 7c11e92

Browse files
committed
Port coherence_overlap mostly to ui_test
1 parent 5918fa8 commit 7c11e92

16 files changed

+107
-200
lines changed

tests/coherence_overlap.rs

Lines changed: 0 additions & 200 deletions
Original file line numberDiff line numberDiff line change
@@ -3,206 +3,6 @@
33
use formality::test_program_ok;
44
use formality_macros::test;
55

6-
#[test]
7-
fn test_u32_i32_impls() {
8-
// Test that we permit impls for distinct types.
9-
expect_test::expect![[r#"
10-
Ok(
11-
(),
12-
)
13-
"#]]
14-
.assert_debug_eq(&test_program_ok(
15-
"[
16-
crate core {
17-
trait Foo<> where [] {}
18-
impl<> Foo<> for u32 where [] {}
19-
impl<> Foo<> for i32 where [] {}
20-
}
21-
]",
22-
));
23-
}
24-
25-
#[test]
26-
fn test_u32_u32_impls() {
27-
// Test that we detect duplicate impls.
28-
expect_test::expect![[r#"
29-
Err(
30-
"duplicate impl in current crate: impl <> Foo < > for (rigid (scalar u32)) where [] { }",
31-
)
32-
"#]]
33-
.assert_debug_eq(&test_program_ok(
34-
"[
35-
crate core {
36-
trait Foo<> where [] {}
37-
impl<> Foo<> for u32 where [] {}
38-
impl<> Foo<> for u32 where [] {}
39-
}
40-
]",
41-
));
42-
}
43-
44-
#[test]
45-
fn test_u32_T_impls() {
46-
// Test that we detect overlap involving generic parameters.
47-
expect_test::expect![[r#"
48-
Err(
49-
"impls may overlap: `impl <> Foo < > for (rigid (scalar u32)) where [] { }` vs `impl <ty> Foo < > for ^ty0_0 where [] { }`",
50-
)
51-
"#]]
52-
.assert_debug_eq(&test_program_ok(
53-
"[
54-
crate core {
55-
trait Foo<> where [] {}
56-
impl<> Foo<> for u32 where [] {}
57-
impl<ty T> Foo<> for T where [] {}
58-
}
59-
]",
60-
));
61-
}
62-
63-
#[test]
64-
fn test_u32_T_where_T_Not_impls() {
65-
// Test that, within a crate, we are able to rely on the fact
66-
// that `u32: Not` is not implemented.
67-
//
68-
// See also test_foo_crate_cannot_assume_CoreStruct_does_not_impl_CoreTrait
69-
expect_test::expect![[r#"
70-
Ok(
71-
(),
72-
)
73-
"#]]
74-
.assert_debug_eq(&test_program_ok(
75-
"[
76-
crate core {
77-
trait Foo<> where [] {}
78-
impl<> Foo<> for u32 where [] {}
79-
impl<ty T> Foo<> for T where [T: Not<>] {}
80-
81-
trait Not<> where [] {}
82-
}
83-
]",
84-
));
85-
}
86-
87-
#[test]
88-
fn test_u32_T_where_T_Is_impls() {
89-
// Test that we detect "indirect" overlap -- here `Foo` is implemented for `u32`
90-
// and also all `T: Is`, and `u32: Is`.
91-
expect_test::expect![[r#"
92-
Err(
93-
"impls may overlap: `impl <> Foo < > for (rigid (scalar u32)) where [] { }` vs `impl <ty> Foo < > for ^ty0_0 where [^ty0_0 : Is < >] { }`",
94-
)
95-
"#]]
96-
.assert_debug_eq(&test_program_ok(
97-
"[
98-
crate core {
99-
trait Foo<> where [] {}
100-
impl<> Foo<> for u32 where [] {}
101-
impl<ty T> Foo<> for T where [T: Is<>] {}
102-
103-
trait Is<> where [] {}
104-
impl<> Is<> for u32 where [] {}
105-
}
106-
]",
107-
));
108-
}
109-
110-
#[test]
111-
fn test_u32_not_u32_impls() {
112-
// Test that a positive and negative impl for the same type (`u32`, here) is rejected.
113-
expect_test::expect![[r#"
114-
Err(
115-
Error {
116-
context: "check_trait_impl(impl <> Foo < > for (rigid (scalar u32)) where [] { })",
117-
source: "failed to disprove {! Foo((rigid (scalar u32)))} given {}, got {Constraints { env: Env { variables: [], coherence_mode: false }, known_true: true, substitution: {} }}",
118-
},
119-
)
120-
"#]]
121-
.assert_debug_eq(&test_program_ok(
122-
"[
123-
crate core {
124-
trait Foo<> where [] {}
125-
impl<> Foo<> for u32 where [] {}
126-
impl<> !Foo<> for u32 where [] {}
127-
}
128-
]",
129-
));
130-
}
131-
132-
#[test]
133-
fn test_T_where_Foo_not_u32_impls() {
134-
// Test positive impl that has a where-clause which checks for itself,
135-
// i.e., `T: Foo where T: Foo`. This `T: Foo` where-clause isn't harmful
136-
// in the coinductive interpretation of trait matching, it actually
137-
// doesn't change the meaning of the impl at all. However, this formulation
138-
// was erroneously accepted by an earlier variant of negative impls.
139-
expect_test::expect![[r#"
140-
Err(
141-
Error {
142-
context: "check_trait_impl(impl <ty> Foo < > for ^ty0_0 where [^ty0_0 : Foo < >] { })",
143-
source: "failed to disprove {! Foo(!ty_1)} given {Foo(!ty_1)}, got {Constraints { env: Env { variables: [?ty_1], coherence_mode: false }, known_true: true, substitution: {?ty_1 => (rigid (scalar u32))} }}",
144-
},
145-
)
146-
"#]]
147-
.assert_debug_eq(&test_program_ok(
148-
"[
149-
crate core {
150-
trait Foo<> where [] {}
151-
impl<ty T> Foo<> for T where [T: Foo<>] {}
152-
impl<> !Foo<> for u32 where [] {}
153-
}
154-
]",
155-
));
156-
}
157-
158-
#[test]
159-
fn test_foo_crate_cannot_assume_CoreStruct_does_not_impl_CoreTrait() {
160-
expect_test::expect![[r#"
161-
Err(
162-
"impls may overlap: `impl <ty> FooTrait < > for ^ty0_0 where [^ty0_0 : CoreTrait < >] { }` vs `impl <> FooTrait < > for (rigid (adt CoreStruct)) where [] { }`",
163-
)
164-
"#]]
165-
.assert_debug_eq(&test_program_ok(
166-
"[
167-
crate core {
168-
trait CoreTrait<> where [] {}
169-
struct CoreStruct<> where [] {}
170-
},
171-
crate foo {
172-
trait FooTrait<> where [] {}
173-
impl<ty T> FooTrait<> for T where [T: CoreTrait<>] {}
174-
impl<> FooTrait<> for CoreStruct<> where [] {}
175-
}
176-
]",
177-
));
178-
}
179-
180-
#[test]
181-
fn test_neg_CoreTrait_for_CoreStruct_implies_no_overlap() {
182-
// Variant of test_foo_crate_cannot_assume_CoreStruct_does_not_impl_CoreTrait
183-
// where there is a negative impl, so it is accepted.
184-
185-
expect_test::expect![[r#"
186-
Ok(
187-
(),
188-
)
189-
"#]]
190-
.assert_debug_eq(&test_program_ok(
191-
"[
192-
crate core {
193-
trait CoreTrait<> where [] {}
194-
struct CoreStruct<> where [] {}
195-
impl<> !CoreTrait<> for CoreStruct<> where [] {}
196-
},
197-
crate foo {
198-
trait FooTrait<> where [] {}
199-
impl<ty T> FooTrait<> for T where [T: CoreTrait<>] {}
200-
impl<> FooTrait<> for CoreStruct<> where [] {}
201-
}
202-
]",
203-
));
204-
}
205-
2066
#[test]
2077
fn test_overlap_normalize_alias_to_LocalType() {
2088
// `LocalTrait` has a blanket impl for all `T: Iterator`
Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
Error: check_trait_impl(impl <ty> Foo < > for ^ty0_0 where [^ty0_0 : Foo < >] { })
2+
3+
Caused by:
4+
failed to disprove {! Foo(!ty_1)} given {Foo(!ty_1)}, got {Constraints { env: Env { variables: [?ty_1], coherence_mode: false }, known_true: true, substitution: {?ty_1 => (rigid (scalar u32))} }}
Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
// Test positive impl that has a where-clause which checks for itself,
2+
// i.e., `T: Foo where T: Foo`. This `T: Foo` where-clause isn't harmful
3+
// in the coinductive interpretation of trait matching, it actually
4+
// doesn't change the meaning of the impl at all. However, this formulation
5+
// was erroneously accepted by an earlier variant of negative impls.
6+
[
7+
crate core {
8+
trait Foo<> where [] {}
9+
impl<ty T> Foo<> for T where [T: Foo<>] {}
10+
impl<> !Foo<> for u32 where [] {}
11+
}
12+
]
Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
Error: impls may overlap: `impl <ty> FooTrait < > for ^ty0_0 where [^ty0_0 : CoreTrait < >] { }` vs `impl <> FooTrait < > for (rigid (adt CoreStruct)) where [] { }`
Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
[
2+
crate core {
3+
trait CoreTrait<> where [] {}
4+
struct CoreStruct<> where [] {}
5+
},
6+
crate foo {
7+
trait FooTrait<> where [] {}
8+
impl<ty T> FooTrait<> for T where [T: CoreTrait<>] {}
9+
impl<> FooTrait<> for CoreStruct<> where [] {}
10+
}
11+
]
Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
//@check-pass
2+
// Variant of foo_crate_cannot_assume_CoreStruct_does_not_impl_CoreTrait
3+
// where there is a negative impl, so it is accepted.
4+
[
5+
crate core {
6+
trait CoreTrait<> where [] {}
7+
struct CoreStruct<> where [] {}
8+
impl<> !CoreTrait<> for CoreStruct<> where [] {}
9+
},
10+
crate foo {
11+
trait FooTrait<> where [] {}
12+
impl<ty T> FooTrait<> for T where [T: CoreTrait<>] {}
13+
impl<> FooTrait<> for CoreStruct<> where [] {}
14+
}
15+
]
Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
Error: impls may overlap: `impl <> Foo < > for (rigid (scalar u32)) where [] { }` vs `impl <ty> Foo < > for ^ty0_0 where [] { }`
Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
[
2+
crate core {
3+
trait Foo<> where [] {}
4+
impl<> Foo<> for u32 where [] {}
5+
impl<ty T> Foo<> for T where [] {}
6+
}
7+
]
Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
Error: impls may overlap: `impl <> Foo < > for (rigid (scalar u32)) where [] { }` vs `impl <ty> Foo < > for ^ty0_0 where [^ty0_0 : Is < >] { }`
Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
// Test that we detect "indirect" overlap -- here `Foo` is implemented for `u32`
2+
// and also all `T: Is`, and `u32: Is`.
3+
[
4+
crate core {
5+
trait Foo<> where [] {}
6+
impl<> Foo<> for u32 where [] {}
7+
impl<ty T> Foo<> for T where [T: Is<>] {}
8+
9+
trait Is<> where [] {}
10+
impl<> Is<> for u32 where [] {}
11+
}
12+
]

0 commit comments

Comments
 (0)