How would specialisation (if a sound implementation was ever found) prevent itself from allowing negative trait reasoning?

1

from my (very limited) understanding of specialisation something like the following should be allowed by it:

trait Baz {}

trait Foo {
    fn bar();
}

impl<T> Foo for T {
    fn bar() {
        // slow path
    }
}

impl<T: Baz> Foo for T {
    fn bar() {
        // fast path
    }
}

but then you could also do:

type True;
type False;

trait Foo {}

trait ImplsFoo {
    type Answer;
}

impl<T> ImplsFoo for T {
    // some of the specialization blog posts i read say that
    // specializing a associated type should require a special keyword to
    // not break Iterator, which makes sense to me,
    // none of them said anything else against specializing associated types.
    bikeshed type Answer = False;
}

impl<T: Foo> ImplsFoo for T {
    bikeshed type Answer = True;
}

trait NotFoo {}

// negative trait reasoning :D
impl<T: ImplsFoo<Answer = False>> NotFoo for T {}

some of the answers i could think off are:

  • Disallow specializing associated types: probably too strict
  • Make associated type bounds not just need to hold for the implementation that was chosen for T, but for all implementations that could have applied to T: less extreme than the first, but confusing.
1 Like
2

Specialization is fundamentally related to negative reasoning, you cannot really prevent it.

Your proposals could prevent implementing traits based on such negative reasoning, but they won't prevent the negative reasoning in the first place: for example the code in // slow path in the first example can pretty much assume T: !Baz

1 Like