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

Positive coverage: prove_predicate / trait well formed

trait well formed
LineCoverageSource
1271(for_all(decls, env, assumptions, &trait_ref.parameters, &prove_wf) => c)
128N/A(let t = decls.trait_decl(&trait_ref.trait_id))
129N/A(let t = t.binder.instantiate_with(&trait_ref.parameters).unwrap())
1302(prove_after(decls, c, assumptions, &t.where_clause) => c)
──────── ("trait well formed")
13230(prove_predicate(decls, env, assumptions, AtomicPredicate::WellFormedTraitRef(trait_ref)) => c)

30 tests exercised this rule:

Source location: tests/basic_tests.rs:58 (all coverage from this test)

#[test]
fn hello_world() {
    FormalityTest::new(crates![crate Foo {
        trait Foo<T> where T: Bar<Self>, Self: Baz {}

        trait Bar<T> where T: Baz {}

        trait Baz {}

        impl Baz for u32 {}

        impl Bar<u32> for u32 {}
        impl<T> Bar<T> for () where T: Baz {}
    }])
    .skip_execute()
    .ok()
}
Proof tree
… (200 of 3755 nodes shown)

Source location: tests/basic_tests.rs:74 (all coverage from this test)

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

        trait B { }

        trait WellFormed where for<T> u32: A<T> { }

        impl <T> B for T {}
    }])
    .skip_execute()
    .ok()
}
Proof tree

Source location: tests/basic_tests.rs:121 (all coverage from this test)

fn foo() -> () where for<T> u32: A<T> { trusted }

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

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

trait B { }

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{},
}
Proof tree

Source location: tests/basic_tests.rs:149 (all coverage from this test)

#[test]
fn non_lifetime_binder_in_trait_impl_where_clause_pass() {
    FormalityTest::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> { }
    }])
    .skip_execute()
    .ok()
}
Proof tree

Source location: tests/basic_tests.rs:179 (all coverage from this test)

#[test]
fn non_lifetime_binder_in_neg_trait_impl_where_clause_pass() {
    FormalityTest::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 {}
    }])
    .skip_execute()
    .ok()
}
Proof tree

Source location: tests/basic_tests.rs:209 (all coverage from this test)

#[test]
fn non_lifetime_binder_in_enum_where_clause_pass() {
    FormalityTest::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 {}
    }])
    .skip_execute()
    .ok()
}
Proof tree

Source location: tests/basic_tests.rs:239 (all coverage from this test)

#[test]
fn non_lifetime_binder_in_struct_where_clause_pass() {
    FormalityTest::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 {}
    }])
    .skip_execute()
    .ok()
}
Proof tree

Source location: tests/basic_tests.rs:266 (all coverage from this test)

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

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

        trait WellFormed where for<'b> u32: A<'b> { }
    }])
    .skip_execute()
    .ok()
}
Proof tree

Source location: tests/codegen.rs:628 (all coverage from this test)

fn main() -> () {
    println!(identity::<S>(7_u32));
}
Proof tree
… (200 of 3615 nodes shown)

Source location: tests/codegen.rs:927 (all coverage from this test)

fn main() -> () {
    println!(identity::<Number>(7_u32));
    println!(identity::<Flag>(true));
    println!(identity::<Number>(9_u32));
}
Proof tree
… (200 of 3845 nodes shown)

Source location: tests/coherence_overlap.rs:237 (all coverage from this test)

#[test]
fn neg_CoreTrait_for_CoreStruct_implies_no_overlap() {
    FormalityTest::new(crates![crate core {
        #![feature(negative_impls)]
        trait CoreTrait {}
        struct CoreStruct {}
        impl !CoreTrait for CoreStruct {}
    },
    crate foo {
        trait FooTrait {}
        impl<T> FooTrait for T where T: CoreTrait {}
        impl FooTrait for CoreStruct {}
    }])
    .skip_execute()
    .ok()
}

Proof trees omitted for the remaining 20 tests; each one is on its test’s page in Coverage by test.

Source location: tests/coherence_overlap.rs:322 (all coverage from this test)

#[test]
fn u32_T_where_T_Not_impls() {
    FormalityTest::new(crates![crate core {
        trait Foo {}
        impl Foo for u32 {}
        impl<T> Foo for T where T: Not {}

        trait Not {}
    }])
    .skip_execute()
    .ok()
}

Source location: tests/coherence_overlap.rs:587 (all coverage from this test)

#[test]
fn is_local_unknowable_trait_ref() {
    FormalityTest::new(crates![crate core {
        trait Project {
            type Assoc: [];
        }

        impl<T> Project for T {
            type Assoc = T;
        }

        trait Foo<U> { }
    },
    crate foo {
        struct LocalType {}

        trait Overlap<U> {}
        impl<T, U> Overlap<U> for T
        where
            <T as Project>::Assoc: Foo<U> {}
        impl<T> Overlap<LocalType> for () {}
    }])
    .skip_execute()
    .ok()
}

Source location: tests/drop.rs:43 (all coverage from this test)

Source location: tests/mir_typeck.rs:987 (all coverage from this test)

fn foo<'a, T>(v1: &'a T) -> T
where
    T: Copy,
    T: 'a,
{
    exists<'r0> {
        let v2: T = *v1;
        return v2;
    }
}

Source location: tests/mir_typeck.rs:1453 (all coverage from this test)

fn main() -> () { require_marker::<u32>; }
}])
tc_ok()
);
}

#[test]
fn_value_with_forwarded_trait_bound() {
alityTest::new(crates![crate Foo {
trait Marker {}
impl Marker for u32 {}
fn require<T>() -> () where T: Marker {}
fn outer<T>() -> () where T: Marker { require::<T>; }
fn main() -> () { outer::<u32>(); }
}])
tc_ok()
);
}

#[test]
bare_fn_value_with_satisfied_where_clause() {
alityTest::new(crates![crate Foo {
trait Marker {}
impl Marker for u32 {}
fn require() -> () where u32: Marker {}
fn main() -> () { require; }
}])
tc_ok()
);
}

#[test]
fn_value_with_forwarded_lifetime_bound() {
alityTest::new(crates![crate Foo {
fn require<'a, 'b>() -> () where 'a: 'b {}
fn outer<'a, 'b>() -> () where 'a: 'b { require::<'a, 'b>; }
fn main() -> () { outer::<'static, 'static>(); }
}])
tc_ok()
);
}

#[test]
fn_value_with_unsatisfied_lifetime_bound() {
alityTest::new(crates![crate Foo {
fn require<'a, 'b>() -> () where 'a: 'b {}
fn outer<'a, 'b>() -> () { require::<'a, 'b>; }
fn main() -> () {}
}])
tc_err(expect_test::expect![[r#"
error: lifetime may not live long enough
 --> lib.rs
  |
7 | pub fn outer<'a00, 'a01>() -> () {
  |              ----  ---- lifetime `'a01` defined here
  |              |
  |              lifetime `'a00` defined here
8 |     require::<'a00, 'a01>;
  |     ^^^^^^^^^^^^^^^^^^^^^ requires that `'a00` must outlive `'a01`
  |
  = help: consider adding the following bound: `'a00: 'a01`

error: could not compile `Foo` (lib) due to 1 previous error
)
(expect_test::expect!["crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_0, b: !lt_1, assumptions: {}, env: Env { variables: [!lt_0, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } }"]);
}

ound assignment of an integer of a different type should fail.
#[test]
compound_add_mismatched_int_types() {
alityTest::new(crates![crate Foo {
fn foo() -> () {
    let x: u32 = 1_u32;
    x += 2_u8;
}

Source location: tests/mir_typeck.rs:1466 (all coverage from this test)

fn main() -> () { outer::<u32>(); }
}])
tc_ok()
);
}

#[test]
bare_fn_value_with_satisfied_where_clause() {
alityTest::new(crates![crate Foo {
trait Marker {}
impl Marker for u32 {}
fn require() -> () where u32: Marker {}
fn main() -> () { require; }
}])
tc_ok()
);
}

#[test]
fn_value_with_forwarded_lifetime_bound() {
alityTest::new(crates![crate Foo {
fn require<'a, 'b>() -> () where 'a: 'b {}
fn outer<'a, 'b>() -> () where 'a: 'b { require::<'a, 'b>; }
fn main() -> () { outer::<'static, 'static>(); }
}])
tc_ok()
);
}

#[test]
fn_value_with_unsatisfied_lifetime_bound() {
alityTest::new(crates![crate Foo {
fn require<'a, 'b>() -> () where 'a: 'b {}
fn outer<'a, 'b>() -> () { require::<'a, 'b>; }
fn main() -> () {}
}])
tc_err(expect_test::expect![[r#"
error: lifetime may not live long enough
 --> lib.rs
  |
7 | pub fn outer<'a00, 'a01>() -> () {
  |              ----  ---- lifetime `'a01` defined here
  |              |
  |              lifetime `'a00` defined here
8 |     require::<'a00, 'a01>;
  |     ^^^^^^^^^^^^^^^^^^^^^ requires that `'a00` must outlive `'a01`
  |
  = help: consider adding the following bound: `'a00: 'a01`

error: could not compile `Foo` (lib) due to 1 previous error
)
(expect_test::expect!["crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_0, b: !lt_1, assumptions: {}, env: Env { variables: [!lt_0, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } }"]);
}

ound assignment of an integer of a different type should fail.
#[test]
compound_add_mismatched_int_types() {
alityTest::new(crates![crate Foo {
fn foo() -> () {
    let x: u32 = 1_u32;
    x += 2_u8;
}

Source location: tests/mir_typeck.rs:1478 (all coverage from this test)

fn main() -> () { require; }
}])
tc_ok()
);
}

#[test]
fn_value_with_forwarded_lifetime_bound() {
alityTest::new(crates![crate Foo {
fn require<'a, 'b>() -> () where 'a: 'b {}
fn outer<'a, 'b>() -> () where 'a: 'b { require::<'a, 'b>; }
fn main() -> () { outer::<'static, 'static>(); }
}])
tc_ok()
);
}

#[test]
fn_value_with_unsatisfied_lifetime_bound() {
alityTest::new(crates![crate Foo {
fn require<'a, 'b>() -> () where 'a: 'b {}
fn outer<'a, 'b>() -> () { require::<'a, 'b>; }
fn main() -> () {}
}])
tc_err(expect_test::expect![[r#"
error: lifetime may not live long enough
 --> lib.rs
  |
7 | pub fn outer<'a00, 'a01>() -> () {
  |              ----  ---- lifetime `'a01` defined here
  |              |
  |              lifetime `'a00` defined here
8 |     require::<'a00, 'a01>;
  |     ^^^^^^^^^^^^^^^^^^^^^ requires that `'a00` must outlive `'a01`
  |
  = help: consider adding the following bound: `'a00: 'a01`

error: could not compile `Foo` (lib) due to 1 previous error
)
(expect_test::expect!["crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_0, b: !lt_1, assumptions: {}, env: Env { variables: [!lt_0, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } }"]);
}

ound assignment of an integer of a different type should fail.
#[test]
compound_add_mismatched_int_types() {
alityTest::new(crates![crate Foo {
fn foo() -> () {
    let x: u32 = 1_u32;
    x += 2_u8;
}

Source location: tests/references.rs:36 (all coverage from this test)

Source location: tests/sized_trait.rs:14 (all coverage from this test)

fn main() -> () {}
}])
tc_ok()
)
}

: ADT Sized support is deferred; rustc accepts this empty struct.
test records the current limitation, not the intended Sized semantics.
#[test]
_bound_not_met_by_unimplemented_type() {
alityTest::new(crates![crate Foo {
struct S {}
trait Needs<T> where T: Sized {}
impl Needs<S> for u32 {}
}])
tc_ok()
(expect_test::expect![[r#"
crates/formality-rust/src/prove/prove_via.rs:9:1: no applicable rules for prove_via { goal: S = &?lt_0 ?ty_1, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [?lt_0, ?ty_1], bias: Soundness, pending: [], allow_pending_outlives: false } }

crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: S, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [?lt_0, ?ty_1], bias: Soundness, pending: [], allow_pending_outlives: false } }

crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: &?lt_0 ?ty_1, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [?lt_0, ?ty_1], bias: Soundness, pending: [], allow_pending_outlives: false } }

crates/formality-rust/src/prove/prove_via.rs:9:1: no applicable rules for prove_via { goal: S = &?lt_0 mut ?ty_1, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [?lt_0, ?ty_1], bias: Soundness, pending: [], allow_pending_outlives: false } }

crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: S, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [?lt_0, ?ty_1], bias: Soundness, pending: [], allow_pending_outlives: false } }

crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: &?lt_0 mut ?ty_1, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [?lt_0, ?ty_1], bias: Soundness, pending: [], allow_pending_outlives: false } }

crates/formality-rust/src/prove/prove_via.rs:9:1: no applicable rules for prove_via { goal: S = (), via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }

crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: S, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }

crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: (), via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }

crates/formality-rust/src/prove/prove_via.rs:9:1: no applicable rules for prove_via { goal: S = bool, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }

crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: S, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }

crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: bool, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }

crates/formality-rust/src/prove/prove_via.rs:9:1: no applicable rules for prove_via { goal: S = i128, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }

crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: S, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }

crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: i128, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }

crates/formality-rust/src/prove/prove_via.rs:9:1: no applicable rules for prove_via { goal: S = i16, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }

crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: S, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }

crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: i16, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }

crates/formality-rust/src/prove/prove_via.rs:9:1: no applicable rules for prove_via { goal: S = i32, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }

crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: S, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }

crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: i32, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }

crates/formality-rust/src/prove/prove_via.rs:9:1: no applicable rules for prove_via { goal: S = i64, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }

crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: S, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }

crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: i64, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }

crates/formality-rust/src/prove/prove_via.rs:9:1: no applicable rules for prove_via { goal: S = i8, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }

crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: S, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }

crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: i8, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }

crates/formality-rust/src/prove/prove_via.rs:9:1: no applicable rules for prove_via { goal: S = isize, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }

crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: S, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }

crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: isize, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }

crates/formality-rust/src/prove/prove_via.rs:9:1: no applicable rules for prove_via { goal: S = u128, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }

crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: S, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }

crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: u128, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }

crates/formality-rust/src/prove/prove_via.rs:9:1: no applicable rules for prove_via { goal: S = u16, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }

crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: S, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }

crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: u16, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }

crates/formality-rust/src/prove/prove_via.rs:9:1: no applicable rules for prove_via { goal: S = u32, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }

crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: S, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }

crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: u32, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }

crates/formality-rust/src/prove/prove_via.rs:9:1: no applicable rules for prove_via { goal: S = u64, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }

crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: S, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }

crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: u64, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }

crates/formality-rust/src/prove/prove_via.rs:9:1: no applicable rules for prove_via { goal: S = u8, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }

crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: S, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }

crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: u8, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }

crates/formality-rust/src/prove/prove_via.rs:9:1: no applicable rules for prove_via { goal: S = usize, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }

crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: S, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }

crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: usize, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }

the rule "trait implied bound" at (prove_predicate.rs) failed because
  expression evaluated to an empty collection: `decls.trait_invariants()`

the rule "trait implied bound" at (prove_predicate.rs) failed because
  expression evaluated to an empty collection: `decls.trait_invariants()`"#]]);
}

#[test]
lue_trait_param_with_sized_bound_compiles_with_rustc() {
alityTest::new(crates![crate Foo {
fn consume<T>(value: T) -> () where T: Sized {}

trait Consumer<T> where T: Sized {
    fn consume_value(value: T) -> () {}
}

Source location: tests/sized_trait.rs:142 (all coverage from this test)

Source location: tests/sized_trait.rs:153 (all coverage from this test)

Source location: tests/sized_trait.rs:164 (all coverage from this test)

Source location: tests/sized_trait.rs:175 (all coverage from this test)

Source location: tests/traits.rs:11 (all coverage from this test)

fn main() -> () { require_copy::<i128>(); }
}])
p_execute()
tc_ok()
);
}

#[test]
is_copy() {
alityTest::new(crates![crate test {
fn require_copy<T>() -> () where T: Copy { trusted }
fn main() -> () { require_copy::<u128>(); }
}])
p_execute()
tc_ok()
);
}

#[test]
_with_valid_fn() {
alityTest::new(crates![
crate core {
    trait A {
        fn a() -> ();
    }
}

Source location: tests/traits.rs:22 (all coverage from this test)

fn main() -> () { require_copy::<u128>(); }
}])
p_execute()
tc_ok()
);
}

#[test]
_with_valid_fn() {
alityTest::new(crates![
crate core {
    trait A {
        fn a() -> ();
    }
}

Source location: tests/well_formed_trait_ref.rs:19 (all coverage from this test)

#[test]
fn dependent_where_clause() {
    FormalityTest::new(crates![crate foo {
        trait Trait1 {}

        trait Trait2 {}

        struct S1<T> where T: Trait1 {
            dummy: T,
        }

        struct S2<T> where T: Trait1, S1<T> : Trait2 {
            dummy: T,
        }
    }])
    .skip_execute()
    .ok()
}

Source location: tests/well_formed_trait_ref.rs:56 (all coverage from this test)

#[test]
fn lifetime_param() {
    FormalityTest::new(crates![crate foo {
        trait Trait1<'a> {}

        struct S1 {}

        struct S2<'a> where S1: Trait1<'a> {}
    }])
    .skip_execute()
    .ok()
}

Source location: tests/well_formed_trait_ref.rs:71 (all coverage from this test)

#[test]
fn static_lifetime_param() {
    FormalityTest::new(crates![crate foo {
        trait Trait1<'a> {}

        struct S1 {}

        impl Trait1<'static> for S1 {}

        struct S2 where S1: Trait1<'static> {}
    }])
    .skip_execute()
    .ok()
}

Source location: tests/well_formed_trait_ref.rs:86 (all coverage from this test)

#[test]
fn const_param() {
    FormalityTest::new(crates![crate foo {
        trait Trait1<const C> where type_of_const C is u32 {}

        struct S1 {}

        impl Trait1<u32(3)> for S1 {}

        struct S2 where S1: Trait1<u32(3)> {}
    }])
    .skip_execute()
    .ok()
}

How to read this page