Why does a self annotated trait is not assignable to the type of self?

Question

trait Base

trait Plugin { base: Base =>
    def asBase: Base & Plugin = this
}

class Mix extends Base, Plugin

val plug: Plugin = new Mix
val baseA: Base= plug.asBase
val baseB: Base = plug // snorts with "Found: Plugin. Required: Base

Why? If I am correct, the Liskov substitution principle is complied because all instances of Plugin are of a concrete type that is a mix that include a subtype of Base. Therefore, objects of type Basecan be replaced with objects of type Plugin without affecting the correctness of the program.

Answer 1

Liskov principle says

https://en.wikipedia.org/wiki/Liskov_substitution_principle

Subtype Requirement: Let ϕ(x) be a property provable about objects x of type T. Then ϕ(y) should be true for objects y of type S where S is a subtype of T.

Preconditions cannot be strengthened in the subtype.

Postconditions cannot be weakened in the subtype.

Invariants must be preserved in the subtype.

Liskov principle is about subtyping. Liskov principle is now not applicable because Plugin is not a subtype of Base

implicitly[Plugin <:< Base] // doesn't compile

(<:< is weaker than <: https://stackoverflow.com/a/75762663/5249621 but this is ok for us; if Plugin were a subtype of Base i.e. Plugin <: Base then moreover implicitly[Plugin <:< Base] would be).

I guess you're confusing either trait Plugin { base: Base => } with trait Plugin extends Base or subclasses (inheritance) with subtypes

What is the difference between a class and a type in Scala (and Java)?

What is the difference between Type and Class?

https://typelevel.org/blog/2017/02/13/more-types-than-classes.html

How to distinguish parameteric types?

What is a difference between refinement type and anonymous subclass in Scala 3?

trait Plugin extends Base means that Plugin is a subclass of Base. In particular, this means that Plugin is a subtype of Base, so all subtypes of Plugin are subtypes of Base. But trait Plugin { base: Base => } means that all subclasses of Plugin must be subclasses of Base. This doesn't mean that all subtypes of Plugin must be subtypes of Base (moreover, this doesn't mean that Plugin is a subtype of Base). Indeed, it's easy to declare a type

type SubPlugin <: Plugin

which is not a subtype of Base

implicitly[SubPlugin <:< Base] // doesn't compile

all instances of Plugin are of a concrete type that is a mix that include a subtype of Base.

Even if it's true that all values (OOP instances) of Plugin are values (instances) of Base this doesn't make Plugin a subtype of Base and this doesn't mean that all terms of type Plugin are terms of type Base. For example the term x in val x: Plugin = ??? is not a term of type Base.

You shouldn't think of a type as (only) a set of all values of the type (especially this becomes important in type-level programming where values are not so interesting at all). Sets can be a model (in logical sense: https://en.wikipedia.org/wiki/Model_theory) for types. But sets and types are different

https://cs.stackexchange.com/questions/91330/what-exactly-is-the-semantic-difference-between-set-and-type

https://math.stackexchange.com/questions/489369/difference-between-a-type-and-a-set

https://planetmath.org/11typetheoryversussettheory

For example if we define two abstract types

type A

type B

then there are no values of these types. So these sets would be equal in set-theoretic sense (an empty set). But these types are different. In homotopy type theory (HoTT, https://en.wikipedia.org/wiki/Homotopy_type_theory) 1 = 2 and 1 = 3 are two types without any values but two different types.

Therefore, objects of type Base can be replaced with objects of type Plugin without affecting the correctness of the program.

There are always programs that can't fail at runtime but that are rejected at compile time. For example if true then 1 else "a" can't fail at runtime but can be rejected by a language without subtyping e.g. Haskell (but not by Scala which thinks that this is Any). Scala rejects val x: Int = if (true) 1 else "a" although this can't fail at runtime either. Rich enough type system can't be sound and complete at the same time. Normally soundness is preferred over completeness

What is a sound programming language?

https://math.stackexchange.com/questions/105575/what-is-the-difference-between-completeness-and-soundness-in-first-order-logic

You may ask why wouldn't always trait Plugin { base: Base => } mean the same as trait Plugin extends Base. Well, this was design decision of Scala type-system creators. In particular, if this would be the same then two different traits trait A {this: B =>}, trait B {this: A =>} would have the same type.

Also in trait Plugin extends Base, Base must be a class/trait. But in trait Plugin { base: Base => }, Base can be a type.

Why scala self type is not a subtype of its requirement

What is the difference between self-types and trait subclasses?

Difference between trait inheritance and self type annotation

What is more Scala idiomatic: trait TraitA extends TraitB or trait TraitA { self: TraitB => }