Skip to content

Commit 20ebe8c

Browse files
committed
add soundness, backwards-incompat test cases
`call-forall` shows the expected behavior: the where-clause proves too much, so we can't prove it. `backwards-incompat` shows the problem with that: we can construct types that we ought not to be able to construct.
1 parent a5888a2 commit 20ebe8c

File tree

3 files changed

+87
-0
lines changed

3 files changed

+87
-0
lines changed
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
// known-bug
2+
// check-pass
3+
4+
#![feature(generic_associated_types)]
5+
6+
trait LendingIterator {
7+
type Item<'a>
8+
where
9+
Self: 'a;
10+
}
11+
12+
impl<'slice> LendingIterator for &'slice [u32] {
13+
type Item<'a> = &'a [u32]
14+
where
15+
Self: 'a;
16+
}
17+
18+
impl<'slice> LendingIterator for [u32] {
19+
type Item<'a> = &'a [u32]
20+
where
21+
Self: 'a;
22+
}
23+
24+
fn broke<T: ?Sized>() -> Option<&'static [u32]>
25+
where
26+
for<'a> T: LendingIterator<Item<'a> = &'a [u32]>,
27+
{
28+
None::<<T as LendingIterator>::Item<'static>>
29+
// FIXME: Should not compile, but does, because we are trusting the where-clauses
30+
// and don't have implied bounds.
31+
}
32+
33+
fn main() {}
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,43 @@
1+
#![feature(generic_associated_types)]
2+
3+
trait LendingIterator {
4+
type Item<'a>
5+
where
6+
Self: 'a;
7+
}
8+
9+
impl<'slice> LendingIterator for &'slice [u32] {
10+
type Item<'a> = &'a [u32]
11+
where
12+
Self: 'a;
13+
}
14+
15+
impl<'slice> LendingIterator for [u32] {
16+
type Item<'a> = &'a [u32]
17+
where
18+
Self: 'a;
19+
}
20+
21+
fn call_me<T: ?Sized>()
22+
where
23+
for<'a> T: LendingIterator<Item<'a> = &'a [u32]>,
24+
{
25+
if false {
26+
call_me::<T>();
27+
}
28+
}
29+
30+
fn ok_i_will1<'test>() {
31+
// Gets an error because we cannot prove that, for all 'a, `&'test [u32]: 'a`.
32+
//
33+
// This is a bug -- what should happen is that there is an implied bound
34+
// so that `for<'a>` really means "for all `'a` that make sense", in which case
35+
// this ought to be provable.
36+
call_me::<&'test [u32]>; //~ ERROR lifetime may not live long enough
37+
}
38+
39+
fn ok_i_will2() {
40+
// OK because, for all 'a, `[u32]: 'a`.
41+
call_me::<[u32]>;
42+
}
43+
fn main() {}
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
error: lifetime may not live long enough
2+
--> $DIR/call-forall.rs:36:5
3+
|
4+
LL | fn ok_i_will1<'test>() {
5+
| ----- lifetime `'test` defined here
6+
...
7+
LL | call_me::<&'test [u32]>;
8+
| ^^^^^^^^^^^^^^^^^^^^^^^ requires that `'test` must outlive `'static`
9+
10+
error: aborting due to previous error
11+

0 commit comments

Comments
 (0)