Supertrait loops are (still) unsound

@nikomatsakis

First reported in https://users.rust-lang.org/t/unexpected-behaviors-of-trait-bounds/12286/3

STR

pub trait Partial: Copy {
}

pub trait Complete: Partial {
}

impl<T> Partial for T where T: Complete {}
impl<T> Complete for T {}

fn copy<P: Partial>(p: P) -> (P, P) {
    (p, p)
}

fn main() {
    let (p, q) = copy("hello".to_string());
    drop(p);
    println!("{}", q);
}

cc @nikomatsakis - let's discuss this when you are back from vacation (unless @aturon can come up with a solution?)

Associated types variant, which bypasses some fixes based only on supertraits:

pub trait Partial<X: ?Sized>: Copy {
}

pub trait Complete {
    type Assoc: Partial<Self>;
}

impl<T> Partial<T> for T::Assoc where
    T: Complete
{
}

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

fn main() {
    let (p, q) = copy::<String>("hello".to_string());
    drop(p);
    println!("{}", q);
}

fn copy<P: Complete>(p: P::Assoc) -> (P::Assoc, P::Assoc) {
    copy2(p)
}

fn copy2<P: Partial<P>>(p: P) -> (P, P) {
    (p, p)
}

Chalk's strategy will solve this, but I guess that shouldn't be extremely difficult to fix even with the current strategy. The first impl is valid:

impl<T> Partial for T where T: Complete {}

since T: Complete indeed implies that T: Copy.

The second however, is not:

impl<T> Complete for T {}

the impl declaration should be able to prove that T: Partial holds (ok because of the first impl), but also that T: Partial is well-formed, i.e. that T: Copy holds.

Same thing in the second example, this impl declaration:

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

should prove that Self::Assoc: Partial<Self> (ok) and that Self::Assoc: Partial<Self> is well-formed, i.e. Self::Assoc: Copy. The latter is not being proved currently.

Fix for the supertrait example in rust-lang#43784

Elaborate trait obligations when typechecking impls

triage: P-high -- has pending fix

Auto merge of #43786 - scalexm:issue-43784, r=nikomatsakis

Rollup merge of rust-lang#81941 - c410-f3r:tests-tests-tests, r=petro…

Navigation Menu

Repository navigation

Supertrait loops are (still) unsound #43784

STR

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Supertrait loops are (still) unsound #43784

Description

STR

Activity

arielb1 commented on Aug 10, 2017

scalexm commented on Aug 10, 2017

nikomatsakis commented on Aug 24, 2017

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions