Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Check type arguments for bad bounds #15571

Merged
merged 5 commits into from
Jul 4, 2022
Merged

Conversation

odersky
Copy link
Contributor

@odersky odersky commented Jul 2, 2022

Fixes #15569

Also: Check for good bounds before reporting other bounds violations

Fixes #15568

Fix ZIO tests that fail because of tightening of bounds checks
Copy link
Contributor

@abgruszecki abgruszecki left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This PR LGTM, but the problem is unfortunately trickier. Take a look at this snippet:

trait Foo[X >: Any <: Nothing]

def andThenSub[A, B, C](f: A <:< B, g: B <:< C): A <:< C =
  f.andThen(g)

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

Since we can't prevent type arguments in general from having bad bounds, I'm wondering if we should disallow naming type arguments other than those at the "top level" of the pattern. I.e. Option[t] would be allowed, Option[Foo[t]] would be disallowed. WDYT, Martin?

@odersky
Copy link
Contributor Author

odersky commented Jul 3, 2022

Can't we instead either disallow

trait Foo[X >: Any <: Nothing]

or disallow pattern matching to discover a type variable with bad bounds?

@abgruszecki
Copy link
Contributor

How would we handle classes like class Bar[A, B, C >: A <: B]? It seems that when we're checking if the bounds are good, the bounds don't need to be completely concrete, neither in class definitions nor in patterns. Bar could be a class defined locally right before the match, so its bounds can reference any abstract type in scope.

Perhaps we should only allow naming type arguments with bounds that are known to certainly be good? (Is that what you meant?)

@odersky
Copy link
Contributor Author

odersky commented Jul 3, 2022

How would we handle classes like class Bar[A, B, C >: A <: B]? It seems that when we're checking if the bounds are good, the bounds don't need to be completely concrete, neither in class definitions nor in patterns. Bar could be a class defined locally right before the match, so its bounds can reference any abstract type in scope.

I think it would be really good if you (or somebody else) would figure out an answer to that.

@s5bug
Copy link

s5bug commented Jul 4, 2022

Could one say that a bound of C >: A <: B is unsafe without A <: B or B >: A? For example,

scala> trait Bar[A, B, C >: A <: B]
// defined trait Bar

could fail because A and B are unrelated.

That would leave this weird asymmetry though:

scala> trait Bar[A <: B, B, C >: A <: B]
// defined trait Bar

scala> trait Bar[A, B >: A, C >: A <: B]
// defined trait Bar

scala> trait Bar[A <: B, B >: A, C >: A <: B]
-- [E140] Cyclic Error: --------------------------------------------------------
1 |trait Bar[A <: B, B >: A, C >: A <: B]
  |          ^
  |illegal cyclic type reference: upper bound B of type A refers back to the type itself
1 error found

@abgruszecki
Copy link
Contributor

OK, I can add it to the list of issues I'll take a look this summer, while we're working on the GADT issues together with Yichen. In the meantime, I think we should merge this PR anyway.

@abgruszecki
Copy link
Contributor

Could one say that a bound of C >: A <: B is unsafe without A <: B or B >: A? For example,

scala> trait Bar[A, B, C >: A <: B]
// defined trait Bar

could fail because A and B are unrelated.

That would leave this weird asymmetry though:

scala> trait Bar[A <: B, B, C >: A <: B]
// defined trait Bar

scala> trait Bar[A, B >: A, C >: A <: B]
// defined trait Bar

scala> trait Bar[A <: B, B >: A, C >: A <: B]
-- [E140] Cyclic Error: --------------------------------------------------------
1 |trait Bar[A <: B, B >: A, C >: A <: B]
  |          ^
  |illegal cyclic type reference: upper bound B of type A refers back to the type itself
1 error found

Your intuition is good. Defining trait Bar[A, B, C >: A <: B] means that we must have A <: B for any instance of Bar. We could require the definition to manually mention that, but I'm not sure if it would solve other issues. The problem I see with being able to name the C parameter in pattern matching is that it seems very close to referencing a path-dependent type. Naming a "top-level" type argument should be OK, since we understand them to correspond to type members which (essentially) can be named with a path-dependent type. But in a pattern like Option[Foo[t]], there is no path by which we can reach t, so something seems to be off.

@abgruszecki abgruszecki merged commit 298ef15 into scala:main Jul 4, 2022
@abgruszecki abgruszecki deleted the fix-15569 branch July 4, 2022 07:23
@odersky
Copy link
Contributor Author

odersky commented Jul 4, 2022

I found two more test cases:

@main def Test4 =
  type t >: Any <: Nothing
  val unsound: Nothing = (5 : Any) : t
  (unsound : Unit => Unit).apply(())

@main def Test5 =
  type t >: Any <: Nothing
  val unsound: List[Nothing] = List(5 : Any) : List[t]
  (unsound.head : Unit => Unit).apply(())

Both compile, but should be rejected. I think it's the explicit usage of a type reference t with conflicting bounds that
should be rejected. If we can refer to such a type, we can construct a transitivity subtyping between two types which should be incomparable.

As @abgruszecki writes, in DOT we cannot express such references. We can only write p.T where p is a path. But then there must be at runtime an actual value p, and when p is created it is checked that T has good bounds. But that argument falls flat when we can just write or infer a t with bad bounds.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
4 participants