Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Negative coverage: check_crate / check crate / premise check_for_non_lifetime_binders(c) => ()

Premise at line 71. Observed failure causes: inapplicable.

check crate
LineCoverageSource
706(check_for_duplicate_items(program) => ())
716(check_for_non_lifetime_binders(c) => ())
72✗(for_all(item in &c.items)
(check_crate_item(program, item, &c.id) => ()))
7411(check_coherence(program, c) => ())
──────── ("check crate")
76114(check_crate(program, Crate { id: _id, items: _items }) => ())

6 tests failed proving this premise:

Source location: tests/basic_tests.rs:103

#[test]
fn basic_where_clauses_without_lifetime_binders_feature_flag_fail() {
    FormalityTest::new(crates![crate core {
        trait A<T> where T: B { }

        trait B { }

        trait WellFormed where for<T> u32: A<T> { }
    }])
    .err(expect_test::expect![[r#"
        the rule "check crate" at (mod.rs) failed because
          non lifetime binders require #![feature(non_lifetime_binders)]"#]])
}
Failed proof tree

Source location: tests/basic_tests.rs:133

fn foo() -> () where for<T> u32: A<T> { trusted }
}])
(expect_test::expect![[r#"
the rule "check crate" at (mod.rs) failed because
  non lifetime binders require #![feature(non_lifetime_binders)]"#]])
}

#[test]
ifetime_binder_in_trait_impl_where_clause_pass() {
alityTest::new(crates![crate core {
#![feature(non_lifetime_binders)]
trait A<T> where T: B { }

trait B { }

impl<T> B for T where for<U> u32: A<U> { }
}])
p_execute()
)
}

#[test]
ifetime_binder_in_trait_impl_where_clause_fail() {
alityTest::new(crates![crate core {
trait A<T> where T: B { }

trait B { }

impl<T> B for T where for<U> u32: A<U> { }
}])
(expect_test::expect![[r#"
the rule "check crate" at (mod.rs) failed because
  non lifetime binders require #![feature(non_lifetime_binders)]"#]])
}

#[test]
ifetime_binder_in_neg_trait_impl_where_clause_pass() {
alityTest::new(crates![crate core {
#![feature(non_lifetime_binders)]
trait A<T> where T: B { }

trait B { }

impl<T> !A<T> for u32 where for<U> u32: A<U> { }

impl <T> B for T {}
}])
p_execute()
)
}

#[test]
ifetime_binder_in_neg_trait_impl_where_clause_fail() {
alityTest::new(crates![crate core {
trait A<T> where T: B { }

trait B { }

impl<T> !A<T> for u32 where for<U> u32: A<U> { }
}])
(expect_test::expect![[r#"
the rule "check crate" at (mod.rs) failed because
  non lifetime binders require #![feature(non_lifetime_binders)]"#]])
}

#[test]
ifetime_binder_in_enum_where_clause_pass() {
alityTest::new(crates![crate core {
#![feature(non_lifetime_binders)]
trait A<T> where T: B { }

trait B { }

enum E where for<U> u32: A<U> { }

impl <T> B for T {}
}])
p_execute()
)
}

#[test]
ifetime_binder_in_enum_where_clause_fail() {
alityTest::new(crates![crate core {
trait A<T> where T: B { }

trait B { }

enum E where for<U> u32: A<U> { }
}])
(expect_test::expect![[r#"
the rule "check crate" at (mod.rs) failed because
  non lifetime binders require #![feature(non_lifetime_binders)]"#]])
}

#[test]
ifetime_binder_in_struct_where_clause_pass() {
alityTest::new(crates![crate core {
#![feature(non_lifetime_binders)]
trait A<T> where T: B { }

trait B { }

struct S<T> where for<U> u32: A<U> { }

impl <T> B for T {}
}])
p_execute()
)
}

#[test]
ifetime_binder_in_struct_where_clause_fail() {
alityTest::new(crates![crate core {
trait A<T> where T: B { }

trait B { }

struct S<T> where for<U> u32: A<U> { }
}])
(expect_test::expect![[r#"
the rule "check crate" at (mod.rs) failed because
  non lifetime binders require #![feature(non_lifetime_binders)]"#]])
}

#[test]
ime_binder_in_where_clause_without_feature_pass() {
alityTest::new(crates![crate core {
trait A<'b> { }

impl<'b> A<'b> for u32 { }

trait WellFormed where for<'b> u32: A<'b> { }
}])
p_execute()
)
}

#[test]
_adt_variant_dup() {
alityTest::new(crates![crate Foo {
enum Bar {
    Baz{},
    Baz{},
}
Failed proof tree

Source location: tests/basic_tests.rs:161

#[test]
fn non_lifetime_binder_in_trait_impl_where_clause_fail() {
    FormalityTest::new(crates![crate core {
        trait A<T> where T: B { }

        trait B { }

        impl<T> B for T where for<U> u32: A<U> { }
    }])
    .err(expect_test::expect![[r#"
        the rule "check crate" at (mod.rs) failed because
          non lifetime binders require #![feature(non_lifetime_binders)]"#]])
}
Failed proof tree

Source location: tests/basic_tests.rs:191

#[test]
fn non_lifetime_binder_in_neg_trait_impl_where_clause_fail() {
    FormalityTest::new(crates![crate core {
        trait A<T> where T: B { }

        trait B { }

        impl<T> !A<T> for u32 where for<U> u32: A<U> { }
    }])
    .err(expect_test::expect![[r#"
        the rule "check crate" at (mod.rs) failed because
          non lifetime binders require #![feature(non_lifetime_binders)]"#]])
}
Failed proof tree

Source location: tests/basic_tests.rs:221

#[test]
fn non_lifetime_binder_in_enum_where_clause_fail() {
    FormalityTest::new(crates![crate core {
        trait A<T> where T: B { }

        trait B { }

        enum E where for<U> u32: A<U> { }
    }])
    .err(expect_test::expect![[r#"
        the rule "check crate" at (mod.rs) failed because
          non lifetime binders require #![feature(non_lifetime_binders)]"#]])
}
Failed proof tree

Source location: tests/basic_tests.rs:251

#[test]
fn non_lifetime_binder_in_struct_where_clause_fail() {
    FormalityTest::new(crates![crate core {
        trait A<T> where T: B { }

        trait B { }

        struct S<T> where for<U> u32: A<U> { }
    }])
    .err(expect_test::expect![[r#"
        the rule "check crate" at (mod.rs) failed because
          non lifetime binders require #![feature(non_lifetime_binders)]"#]])
}
Failed proof tree