Why does a method with type parameter bound >: all

Consider the following simple implementation of a stack in Scala:

abstract class Stack[+A] {
  def top: A
  def pop: Stack[A]
}

case object EmptyStack extends Stack[Nothing] {
  def top = error("EmptyStack.top")
  def pop = error("EmptyStack.pop")
}

case class NonEmptyStack[A](elem: A, rest: Stack[A]) extends Stack[A] {
  def top = elem
  def pop = rest
}

Now suppose we want to add a push method to Stack. The naive attempt

abstract class Stack[+A] {
  def push(x: A): Stack[A] = new NonEmptyStack[A](x, this)
  ...
}

fails because the A in (x: A) is a contravariant position. In Scala by Example page 58, the author suggests

def push[B >: A](x: B): Stack[B] = new NonEmptyStack[B](x, this)

The type bound here means that given a stack of a certain type, we can push objects of an equal or more general type to that stack, and the result is a stack of the more general type.

For example,

class Fruit
class Apple extends Fruit
class Banana extends Fruit

val apple = new Apple
val banana = new Banana

val stack1 = EmptyStack.push(apple)  // Stack[Apple]
val stack2 = stack1.push(banana)     // Stack[Fruit]

I think the point of this choice is that it truly maintains the covariance of Stack: if piece of code expects a Stack[Fruit] onto which it will push any fruit (banana or apple), then it can still push those fruits onto a Stack[Apple].

Surprisingly, we can also push subtypes:

class Honeycrisp extends Apple

val honeycrisp = Honeycrisp
val stack1 = EmptyStack.push(apple)  // Stack[Apple]
val stack2 = stack1.push(honeycrisp) // Stack[Apple], why does this work?

Why is this allowed? Doesn't the type bound >: mean that only supertypes should be allowed?

def push[B >: A](x: B): Stack[B] = ...
...

Why is this allowed? Doesn't the type bound >: mean that only supertypes should be allowed?

Only super-types are allowed as B, in your example Apple. But x: B is in a contravariant (input) position, and as such you can always pass a more specific value as an argument. That has nothing to do with the definition of B. What you will see however is that the inferred type for honeycrisp is Apple not Honeycrisp.

This is indeed perplexing, and I remember having wondered about this once. But if you go through the implications, it really preserves the type soundness. Of course as a consequence, from the point of view of the body of push, x is really Any without specific capabilities it could count on.

Possibly related: