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

Test ref_CoreStruct_is_not_local

Source location: tests/coherence_orphan.rs:375

#[test]
fn ref_CoreStruct_is_not_local() {
    FormalityTest::new(crates![crate core {
        trait CoreTrait {}
        struct CoreStruct {}
    },
    crate foo {
        impl CoreTrait for &'static CoreStruct {}
    }])
    .rustc_err(expect_test::expect![[r#"
        error[E0117]: only traits defined in the current crate can be implemented for arbitrary types
         --> lib.rs
          |
        3 | impl CoreTrait for &'static CoreStruct {}
          | ^^^^^^^^^^^^^^^^^^^-------------------
          |                    |
          |                    `mycore::CoreStruct` is not defined in the current crate
          |
          = note: impl doesn't have any local type before any uncovered type parameters
          = note: for more information see https://doc.rust-lang.org/reference/items/implementations.html#orphan-rules
          = note: define and implement a trait or new type instead

        For more information about this error, try `rustc --explain E0117`.
        error: could not compile `foo` (lib) due to 1 previous error
    "#]])
    .err(expect_test::expect![[r#"
        the rule "fundamental rigid type" at (is_local.rs) failed because
          condition evaluated to false: `is_fundamental(decls, name)`
            decls = program([crate core { trait CoreTrait <ty> { } struct CoreStruct { } }, crate foo { impl CoreTrait for &' static CoreStruct { } }], 222)
            name = (adt CoreStruct)

        crates/formality-rust/src/prove/prove_normalize.rs:22:1: no applicable rules for prove_normalize { p: CoreStruct, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }

        the rule "local rigid type" at (is_local.rs) failed because
          condition evaluated to false: `decls.is_local_adt_id(a)`
            decls = program([crate core { trait CoreTrait <ty> { } struct CoreStruct { } }, crate foo { impl CoreTrait for &' static CoreStruct { } }], 222)
            a = CoreStruct

        crates/formality-rust/src/prove/prove_normalize.rs:22:1: no applicable rules for prove_normalize { p: &' static CoreStruct, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }

        the rule "local trait" at (is_local.rs) failed because
          condition evaluated to false: `decls.is_local_trait_id(&goal.trait_id)`
            decls = program([crate core { trait CoreTrait <ty> { } struct CoreStruct { } }, crate foo { impl CoreTrait for &' static CoreStruct { } }], 222)
            &goal.trait_id = CoreTrait"#]])
}

Rules proved (0)

This test records no positive coverage.

Premises failed (12)

The last column links to the premise’s page when the judgment view counts this failure against that premise. It does not when the premise is read as infallible, or when the failure was blamed inside a multi-line premise that carries no record on its own first line.

JudgmentRulePremiseAll tests of this premise
check_coherencecheck_coherencefor_all(trait_impl in current_crate_impls) (orph… (line 19, blamed at line 20)not counted by the judgment view
orphan_checkorphan_checkscope(enter_universally(Env::default(), &impl_a.… (line 35, blamed at line 37)not counted by the judgment view
check_all_cratescheck all prefixesfor_all(i in 0..crates.len()) (let program = cra… (line 52, blamed at line 54)not counted by the judgment view
check_cratecheck cratecheck_coherence(program, c) => () (line 75)20 tests
is_local_trait_reflocal traitif decls.is_local_trait_id(&goal.trait_id) (line 216)12 tests
is_local_trait_reflocal parameteris_local_parameter(decls, env, assumptions, &goa… (line 224)12 tests
is_local_parameterlocal parameterprove_normalize(decls, env, assumptions, goal) =… (line 305)12 tests
is_local_parameterfundamental rigid typeif is_fundamental(decls, name) (line 314)7 tests
is_local_parameterfundamental rigid typefor_all(decls, env, assumptions, type_params, &i… (line 316)5 tests
is_local_parameterlocal rigid typeif decls.is_local_adt_id(a) (line 323)5 tests
prove_predicatetrait ref is localis_local_trait_ref(decls, env, assumptions, trai… (line 136)12 tests
prove_predicate_listsomeprove_predicate(decls, env, assumptions, wc0) =>… (line 26)67 tests

Proof trees

Failed proof tree

How to read this page