Skip to content

Commit b1ceae9

Browse files
nikomatsakisnikomatsakis
committed
flesh out orphan check tests
1 parent 9f02071 commit b1ceae9

File tree

7 files changed

+199
-27
lines changed

7 files changed

+199
-27
lines changed

‎crates/formality-check/src/coherence.rs

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -32,6 +32,7 @@ impl Check<'_> {
3232
.iter()
3333
.cartesian_product(&all_crate_impls)
3434
.filter(|(impl_a, impl_b)| impl_a != impl_b)
35+
.filter(|(impl_a, impl_b)| impl_a.trait_id() == impl_b.trait_id())
3536
{
3637
self.overlap_check(impl_a, impl_b)?;
3738
}
@@ -72,6 +73,8 @@ impl Check<'_> {
7273
let trait_ref_a = a.trait_ref();
7374
let trait_ref_b = b.trait_ref();
7475

76+
assert_eq!(trait_ref_a.trait_id, trait_ref_b.trait_id);
77+
7578
// If the parameters from the two impls cannot be equal, then they do not overlap.
7679
//
7780
// If we can prove `∀P_a, ∀P_b. not (T_a = T_b, Wc_a, Wc_b)`, then they do not overlap.

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

Lines changed: 13 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -86,6 +86,13 @@ judgment_fn! {
8686
}
8787

8888
judgment_fn! {
89+
/// "not_downstream(..., P)" means that `P` cannot be instantiated with a type from
90+
/// a downstream crate (i.e., a crate that has us as a dependency).
91+
///
92+
/// NB. Since RFC 2451, the judgment applies to the outermost type only. In other words,
93+
/// the judgment holds for (e.g.) `Vec<T>`, which could be instantiated
94+
/// with something like `Vec<DownstreamType>`, but that is not considered downstream
95+
/// as the outermost type (`Vec`) is upstream.
8996
fn not_downstream(
9097
decls: Decls,
9198
env: Env,
@@ -95,17 +102,21 @@ judgment_fn! {
95102
debug(parameter, assumptions, env, decls)
96103

97104
(
98-
(for_all(&decls, &env, &assumptions, &parameters, &not_downstream) => c)
105+
// Since https://rust-lang.github.io/rfcs/2451-re-rebalancing-coherence.html,
106+
// any rigid type is adequate.
99107
--- ("rigid")
100-
(not_downstream(decls, env, assumptions, RigidTy { name: _, parameters }) => c)
108+
(not_downstream(_decls, env, _assumptions, RigidTy { .. }) => Constraints::none(env))
101109
)
102110

103111
(
112+
// Lifetimes are not relevant.
104113
--- ("lifetime")
105114
(not_downstream(_decls, env, _assumptions, _l: Lt) => Constraints::none(env))
106115
)
107116

108117
(
118+
// Inference variables *could* be inferred to downstream types; depends on the substitution
119+
// we ultimately have.
109120
--- ("type variable")
110121
(not_downstream(_decls, env, _assumptions, TyData::Variable(Variable::InferenceVar(_))) => Constraints::none(env).ambiguous())
111122
)

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

Lines changed: 8 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
11
use formality_types::{
2-
grammar::{Parameter, PlaceholderVar, Wcs},
2+
grammar::{Parameter, PlaceholderVar, RigidName, RigidTy, Wcs},
33
judgment_fn,
44
};
55

6-
use crate::decls::Decls;
6+
use crate::{decls::Decls, prove::combinators::for_all};
77

88
use super::{constraints::Constraints, env::Env};
99

@@ -26,5 +26,11 @@ judgment_fn! {
2626
--- ("universal variables")
2727
(prove_wf(_decls, env, _assumptions, PlaceholderVar { .. }) => Constraints::none(env))
2828
)
29+
30+
(
31+
(for_all(&decls, &env, &assumptions, &parameters, &prove_wf) => c)
32+
--- ("tuples")
33+
(prove_wf(decls, env, assumptions, RigidTy { name: RigidName::Tuple(_), parameters }) => c)
34+
)
2935
}
3036
}

‎crates/formality-rust/src/grammar.rs

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -247,6 +247,12 @@ pub struct TraitImpl {
247247
pub binder: Binder<TraitImplBoundData>,
248248
}
249249

250+
impl TraitImpl {
251+
pub fn trait_id(&self) -> &TraitId {
252+
&self.binder.peek().trait_id
253+
}
254+
}
255+
250256
#[term($trait_id < $,trait_parameters > for $self_ty where $where_clauses { $*impl_items })]
251257
pub struct TraitImplBoundData {
252258
pub trait_id: TraitId,

‎crates/formality-types/src/judgment.rs

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,13 +15,15 @@ struct InferenceRule<I, O> {
1515
#[macro_export]
1616
macro_rules! judgment_fn {
1717
(
18+
$(#[$attr:meta])*
1819
$v:vis fn $name:ident($($input_name:ident : $input_ty:ty),* $(,)?) => $output:ty {
1920
debug($($debug_input_name:ident),*)
2021
$(assert($assert_expr:expr))*
2122
$(trivial($trivial_expr:expr => $trivial_result:expr))*
2223
$(($($rule:tt)*))*
2324
}
2425
) => {
26+
$(#[$attr])*
2527
$v fn $name($($input_name : impl $crate::cast::Upcast<$input_ty>),*) -> $crate::collections::Set<$output> {
2628
#[derive(Ord, PartialOrd, Eq, PartialEq, Hash, Clone)]
2729
struct __JudgmentStruct($($input_ty),*);

‎tests/coherence.rs

Lines changed: 0 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -177,29 +177,6 @@ fn test_foo_crate_cannot_assume_CoreStruct_does_not_impl_CoreTrait() {
177177
));
178178
}
179179

180-
#[test]
181-
fn test_orphan_basic() {
182-
expect_test::expect![[r#"
183-
Err(
184-
Error {
185-
context: "orphan_check(impl <> CoreTrait < > for (rigid (adt CoreStruct)) where [] { })",
186-
source: "failed to prove {@ IsLocal(CoreTrait((rigid (adt CoreStruct))))} given {}, got {}",
187-
},
188-
)
189-
"#]]
190-
.assert_debug_eq(&test_program_ok(
191-
"[
192-
crate core {
193-
trait CoreTrait<> where [] {}
194-
struct CoreStruct<> where [] {}
195-
},
196-
crate foo {
197-
impl<> CoreTrait<> for CoreStruct<> where [] {}
198-
}
199-
]",
200-
));
201-
}
202-
203180
#[test]
204181
fn test_neg_CoreTrait_for_CoreStruct_implies_no_overlap() {
205182
// Variant of test_foo_crate_cannot_assume_CoreStruct_does_not_impl_CoreTrait

‎tests/coherence_orphan.rs

Lines changed: 167 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,167 @@
1+
#![allow(non_snake_case)] // we embed type names into the names for our test functions
2+
3+
use formality::test_program_ok;
4+
use formality_macros::test;
5+
6+
#[test]
7+
fn test_orphan_basic() {
8+
expect_test::expect![[r#"
9+
Err(
10+
Error {
11+
context: "orphan_check(impl <> CoreTrait < > for (rigid (adt CoreStruct)) where [] { })",
12+
source: "failed to prove {@ IsLocal(CoreTrait((rigid (adt CoreStruct))))} given {}, got {}",
13+
},
14+
)
15+
"#]]
16+
.assert_debug_eq(&test_program_ok(
17+
"[
18+
crate core {
19+
trait CoreTrait<> where [] {}
20+
struct CoreStruct<> where [] {}
21+
},
22+
crate foo {
23+
impl<> CoreTrait<> for CoreStruct<> where [] {}
24+
}
25+
]",
26+
));
27+
}
28+
29+
#[test]
30+
fn test_orphan_mirror_CoreStruct() {
31+
expect_test::expect![[r#"
32+
Err(
33+
Error {
34+
context: "orphan_check(impl <> CoreTrait < > for (alias (Mirror :: Assoc) (rigid (adt CoreStruct))) where [] { })",
35+
source: "failed to prove {@ IsLocal(CoreTrait((alias (Mirror :: Assoc) (rigid (adt CoreStruct)))))} given {}, got {}",
36+
},
37+
)
38+
"#]]
39+
.assert_debug_eq(&test_program_ok(
40+
"[
41+
crate core {
42+
trait CoreTrait<> where [] {}
43+
struct CoreStruct<> where [] {}
44+
45+
trait Mirror<> where [] {
46+
type Assoc<> : [] where [];
47+
}
48+
49+
impl<ty T> Mirror<> for T where [] {
50+
type Assoc<> = T where [];
51+
}
52+
},
53+
crate foo {
54+
impl<> CoreTrait<> for <CoreStruct<> as Mirror<>>::Assoc<> where [] {}
55+
}
56+
]",
57+
));
58+
}
59+
60+
#[test]
61+
fn test_orphan_mirror_FooStruct() {
62+
// We are able to normalize and see that the result is local.
63+
//
64+
// NB: rustc doesn't do this.
65+
expect_test::expect![[r#"
66+
Ok(
67+
(),
68+
)
69+
"#]]
70+
.assert_debug_eq(&test_program_ok(
71+
"[
72+
crate core {
73+
trait CoreTrait<> where [] {}
74+
75+
trait Mirror<> where [] {
76+
type Assoc<> : [] where [];
77+
}
78+
79+
impl<ty T> Mirror<> for T where [] {
80+
type Assoc<> = T where [];
81+
}
82+
},
83+
crate foo {
84+
struct FooStruct<> where [] {}
85+
impl<> CoreTrait<> for <FooStruct<> as Mirror<>>::Assoc<> where [] {}
86+
}
87+
]",
88+
));
89+
}
90+
91+
#[test]
92+
fn test_orphan_alias_to_unit() {
93+
// We are able to normalize and see that the result is local.
94+
//
95+
// NB: rustc doesn't do this.
96+
expect_test::expect![[r#"
97+
Err(
98+
Error {
99+
context: "orphan_check(impl <> CoreTrait < > for (alias (Unit :: Assoc) (rigid (adt FooStruct))) where [] { })",
100+
source: "failed to prove {@ IsLocal(CoreTrait((alias (Unit :: Assoc) (rigid (adt FooStruct)))))} given {}, got {}",
101+
},
102+
)
103+
"#]]
104+
.assert_debug_eq(&test_program_ok(
105+
"[
106+
crate core {
107+
trait CoreTrait<> where [] {}
108+
109+
trait Unit<> where [] {
110+
type Assoc<> : [] where [];
111+
}
112+
113+
impl<ty T> Unit<> for T where [] {
114+
type Assoc<> = () where [];
115+
}
116+
},
117+
crate foo {
118+
struct FooStruct<> where [] {}
119+
impl<> CoreTrait<> for <FooStruct<> as Unit<>>::Assoc<> where [] {}
120+
}
121+
]",
122+
));
123+
}
124+
125+
#[test]
126+
fn test_orphan_uncovered_T() {
127+
expect_test::expect![[r#"
128+
Err(
129+
Error {
130+
context: "orphan_check(impl <ty> CoreTrait < (rigid (adt FooStruct)) > for ^ty0_0 where [] { })",
131+
source: "failed to prove {@ IsLocal(CoreTrait(!ty_1, (rigid (adt FooStruct))))} given {}, got {}",
132+
},
133+
)
134+
"#]]
135+
.assert_debug_eq(&test_program_ok(
136+
"[
137+
crate core {
138+
trait CoreTrait<ty T> where [] {}
139+
},
140+
crate foo {
141+
struct FooStruct<> where [] {}
142+
impl<ty T> CoreTrait<FooStruct<>> for T where [] {}
143+
}
144+
]",
145+
));
146+
}
147+
148+
#[test]
149+
fn test_orphan_covered_VecT() {
150+
expect_test::expect![[r#"
151+
Ok(
152+
(),
153+
)
154+
"#]]
155+
.assert_debug_eq(&test_program_ok(
156+
"[
157+
crate core {
158+
trait CoreTrait<ty T> where [] {}
159+
struct Vec<ty T> where [] {}
160+
},
161+
crate foo {
162+
struct FooStruct<> where [] {}
163+
impl<ty T> CoreTrait<FooStruct<>> for Vec<T> where [] {}
164+
}
165+
]",
166+
));
167+
}

0 commit comments

Comments
 (0)