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: is_local_parameter / fundamental rigid type

fundamental rigid type
LineCoverageSource
3147(if is_fundamental(decls, name))
315N/A(let type_params: Vec<Parameter> = parameters.iter().filter(|p| !matches!(p, Parameter::Lt(_))).cloned().collect())
3165(for_all(decls, env, assumptions, type_params, &is_local_parameter) => c)
──────── ("fundamental rigid type")
3182(is_local_parameter(decls, env, assumptions, RigidTy { name, parameters }) => c)

2 tests exercised this rule:


Source location: tests/coherence_orphan.rs:286 (all coverage from this test)

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

#[test]
d_ref_FooStruct_is_local() {
alityTest::new(crates![crate core {
trait CoreTrait {}
},
e foo {
struct FooStruct {}
impl<'a, 'b> CoreTrait for &'a &'b mut FooStruct where 'b: 'a {}
fn main() -> () {}
}])
tc_ok()
)
}

#[test]
oreign_wrapper_of_local_is_not_local() {
alityTest::new(crates![crate core {
trait CoreTrait {}
struct ForeignWrapper<T> { value: T }
},
e foo {
struct FooStruct {}
impl<'a> CoreTrait for &'a ForeignWrapper<FooStruct> {}
}])
tc_err(expect_test::expect![[r#"
error[E0117]: only traits defined in the current crate can be implemented for arbitrary types
 --> lib.rs
  |
5 | impl<'a00> CoreTrait for &'a00 ForeignWrapper<FooStruct> {}
  | ^^^^^^^^^^^^^^^^^^^^^^^^^-------------------------------
  |                          |
  |                          `mycore::ForeignWrapper` 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
)
(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 ForeignWrapper <ty> { value : ^ty0_0 } }, crate foo { struct FooStruct { } impl <lt> CoreTrait for &^lt0_0 ForeignWrapper<FooStruct> { } }], 222)
    name = (adt ForeignWrapper)

crates/formality-rust/src/prove/prove_normalize.rs:22:1: no applicable rules for prove_normalize { p: ForeignWrapper<FooStruct>, assumptions: {}, env: Env { variables: [!lt_0], 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 ForeignWrapper <ty> { value : ^ty0_0 } }, crate foo { struct FooStruct { } impl <lt> CoreTrait for &^lt0_0 ForeignWrapper<FooStruct> { } }], 222)
    a = ForeignWrapper

crates/formality-rust/src/prove/prove_normalize.rs:22:1: no applicable rules for prove_normalize { p: &!lt_0 ForeignWrapper<FooStruct>, assumptions: {}, env: Env { variables: [!lt_0], 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 ForeignWrapper <ty> { value : ^ty0_0 } }, crate foo { struct FooStruct { } impl <lt> CoreTrait for &^lt0_0 ForeignWrapper<FooStruct> { } }], 222)
    &goal.trait_id = CoreTrait"#]])
}

#[test]
oreStruct_is_not_local() {
alityTest::new(crates![crate core {
trait CoreTrait {}
struct CoreStruct {}
},
e foo {
impl CoreTrait for &'static CoreStruct {}
}])
tc_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
)
(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"#]])
}

#[test]
_to_unit() {
alityTest::new(crates![crate core {
        trait CoreTrait {}

        trait Unit {
            type Assoc : [];
        }

        impl<T> Unit for T {
            type Assoc = ();
        }
    },
    crate foo {
        struct FooStruct {}
        impl CoreTrait for <FooStruct as Unit>::Assoc {}
    }]).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> { } trait Unit <ty> { type Assoc : [] ; } impl <ty> Unit for ^ty0_0 { type Assoc = () ; } }, crate foo { struct FooStruct { } impl CoreTrait for <FooStruct as Unit>::Assoc { } }], 222)
            name = tuple(0)

        crates/formality-rust/src/prove/prove_normalize.rs:22:1: no applicable rules for prove_normalize { p: (), 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> { } trait Unit <ty> { type Assoc : [] ; } impl <ty> Unit for ^ty0_0 { type Assoc = () ; } }, crate foo { struct FooStruct { } impl CoreTrait for <FooStruct as Unit>::Assoc { } }], 222)
            &goal.trait_id = CoreTrait"#]])
}

#[test]
rait_for_CoreStruct_in_Foo() {
alityTest::new(crates![crate core {
        trait CoreTrait {}
        struct CoreStruct {}
    },
    crate foo {
        impl CoreTrait for CoreStruct {}
    }]).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 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 CoreStruct { } }], 222)
            a = CoreStruct

        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 CoreStruct { } }], 222)
            &goal.trait_id = CoreTrait"#]])
}

#[test]
raitLocal_for_AliasToKnown_in_Foo() {
ODO: see comment in `orphan_check` from prev commit
alityTest::new(crates![crate core {
trait CoreTrait<T> {}

trait Unit {
    type Assoc : [];
}
Proof tree

Source location: tests/coherence_orphan.rs:300 (all coverage from this test)

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

#[test]
oreign_wrapper_of_local_is_not_local() {
alityTest::new(crates![crate core {
trait CoreTrait {}
struct ForeignWrapper<T> { value: T }
},
e foo {
struct FooStruct {}
impl<'a> CoreTrait for &'a ForeignWrapper<FooStruct> {}
}])
tc_err(expect_test::expect![[r#"
error[E0117]: only traits defined in the current crate can be implemented for arbitrary types
 --> lib.rs
  |
5 | impl<'a00> CoreTrait for &'a00 ForeignWrapper<FooStruct> {}
  | ^^^^^^^^^^^^^^^^^^^^^^^^^-------------------------------
  |                          |
  |                          `mycore::ForeignWrapper` 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
)
(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 ForeignWrapper <ty> { value : ^ty0_0 } }, crate foo { struct FooStruct { } impl <lt> CoreTrait for &^lt0_0 ForeignWrapper<FooStruct> { } }], 222)
    name = (adt ForeignWrapper)

crates/formality-rust/src/prove/prove_normalize.rs:22:1: no applicable rules for prove_normalize { p: ForeignWrapper<FooStruct>, assumptions: {}, env: Env { variables: [!lt_0], 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 ForeignWrapper <ty> { value : ^ty0_0 } }, crate foo { struct FooStruct { } impl <lt> CoreTrait for &^lt0_0 ForeignWrapper<FooStruct> { } }], 222)
    a = ForeignWrapper

crates/formality-rust/src/prove/prove_normalize.rs:22:1: no applicable rules for prove_normalize { p: &!lt_0 ForeignWrapper<FooStruct>, assumptions: {}, env: Env { variables: [!lt_0], 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 ForeignWrapper <ty> { value : ^ty0_0 } }, crate foo { struct FooStruct { } impl <lt> CoreTrait for &^lt0_0 ForeignWrapper<FooStruct> { } }], 222)
    &goal.trait_id = CoreTrait"#]])
}

#[test]
oreStruct_is_not_local() {
alityTest::new(crates![crate core {
trait CoreTrait {}
struct CoreStruct {}
},
e foo {
impl CoreTrait for &'static CoreStruct {}
}])
tc_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
)
(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"#]])
}

#[test]
_to_unit() {
alityTest::new(crates![crate core {
        trait CoreTrait {}

        trait Unit {
            type Assoc : [];
        }

        impl<T> Unit for T {
            type Assoc = ();
        }
    },
    crate foo {
        struct FooStruct {}
        impl CoreTrait for <FooStruct as Unit>::Assoc {}
    }]).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> { } trait Unit <ty> { type Assoc : [] ; } impl <ty> Unit for ^ty0_0 { type Assoc = () ; } }, crate foo { struct FooStruct { } impl CoreTrait for <FooStruct as Unit>::Assoc { } }], 222)
            name = tuple(0)

        crates/formality-rust/src/prove/prove_normalize.rs:22:1: no applicable rules for prove_normalize { p: (), 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> { } trait Unit <ty> { type Assoc : [] ; } impl <ty> Unit for ^ty0_0 { type Assoc = () ; } }, crate foo { struct FooStruct { } impl CoreTrait for <FooStruct as Unit>::Assoc { } }], 222)
            &goal.trait_id = CoreTrait"#]])
}

#[test]
rait_for_CoreStruct_in_Foo() {
alityTest::new(crates![crate core {
        trait CoreTrait {}
        struct CoreStruct {}
    },
    crate foo {
        impl CoreTrait for CoreStruct {}
    }]).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 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 CoreStruct { } }], 222)
            a = CoreStruct

        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 CoreStruct { } }], 222)
            &goal.trait_id = CoreTrait"#]])
}

#[test]
raitLocal_for_AliasToKnown_in_Foo() {
ODO: see comment in `orphan_check` from prev commit
alityTest::new(crates![crate core {
trait CoreTrait<T> {}

trait Unit {
    type Assoc : [];
}
Proof tree

How to read this page