Pattern-bound types with bad bounds lead to unsoundness

[abgruszecki]

trait Foo[X >: Any <: Nothing]

@main def Test = (None: Option[Foo[?]]) match {
  case _: Option[Foo[t]] =>
    val unsound: Nothing = (5 : Any) : t
    (unsound : Unit => Unit).apply(())
}

The problem seems to be that pattern matching lets us name a type argument which does not correspond to a type member with known good bounds. In DOT, we would not be able to refer to t, so the issue would not show up.

Fixes we have thought of so far:

1. Disallowing classes with bad bounds on type parameters
2. Disallowing pat-mat from naming types with bad bounds / only letting pat-mat name types with bounds that are known to be good
3. Disallowing pat-mat from naming type arguments which are not top-level

See also the discussion in #15571 and related PR #15577.

[dwijnand]

I like @odersky's choice of option 4 in #15577: let PostTyper reject the definition of named (ie non-wildcard) type bindings that have bad bounds!

[Linyxus]

It feels that option 3 is the most logical choice. If we represent type parameters as type members, then binding non-toplevel type arguments would be equivalent to having a type projection.

[odersky]

Note that the problem is more general than pattern bound types. For every pattern bound type t with bad bounds L, R, I can also simply write a local type definition

type t >: L <: R

with the same effect. In DOT we can't do either since every type has to be a member of an object. So in DOT I'd have to write

val p = {
  type t >: L <: R
}

and then use p.t instead of t. But the definition of p would be rejected since t has bad bounds. It seems most in the spirit of DOT then to also reject the definition of t with bad bounds at the top-level. And likewise for pattern-bound types.

[Linyxus]

Ah, yes. This solution is indeed more logical and consistent. Thanks for your explanation! :)

[smarter]

A type bound as a type parameter in a pattern like trait Foo[A]; ... case x: Foo[t] => ... t can be seen as syntactic sugar for case x: Foo[_] => ... x.A. The latter cannot be written down by the user because A is a type parameter and not a type member, but the compiler will infer types of this form (e.g., when using wildcards), so I think it'd make sense to not require them to have good bounds.

[smarter]

In fact, I think ideally the compiler should define the pattern-bound symbol t to be an alias of x.A instead of an abstract type with some specific bounds, that way we don't have to special-case them in the checking logic.

[abgruszecki]

A type bound as a type parameter in a pattern like trait Foo[A]; ... case x: Foo[t] => ... t can be seen as syntactic sugar for case x: Foo[_] => ... x.A. The latter cannot be written down by the user because A is a type parameter and not a type member, but the compiler will infer types of this form (e.g., when using wildcards), so I think it'd make sense to not require them to have good bounds.

One important thing here is that we will reconstruct subtype relationships / infer GADT constraints from the bounds of top-level type parameters, so ideally we should never reject them (their bounds cannot be bad).

[abgruszecki]

In fact, I think ideally the compiler should define the pattern-bound symbol t to be an alias of x.A instead of an abstract type with some specific bounds, that way we don't have to special-case them in the checking logic.

1. What's x here?
2. Can we refer to type members representing type parameters? My vague impression is that Dotty has such a concept internally, but such references are meant to be replaced when a class type is applied to some type arguments.

[smarter]

What's x here?

The bound variable, I was referring to the example in my previous message with case x: Foo[t] =>

Can we refer to type members representing type parameters? My vague impression is that Dotty has such a concept internally, but such references are meant to be replaced when a class type is applied to some type arguments.

If you write

trait Box[T]:
  val unbox: T

class A:
  def foo(box: Box[?]) =
    box.unbox

Then the inferred result type of foo is box.T according to -Xprint:typer.

[abgruszecki]

What's x here?

The bound variable, I was referring to the example in my previous message with case x: Foo[t] =>

OK, just wanted to point out that in patterns like _: Option[Foo[t]], there's no variable with which we can reference t.

[smarter]

Yes, to be precise I was talking about patterns of the form case x: C[t] => where C is a class or trait type (or dealiases to such a type).