Dotty: Drop `transparent`

[odersky]

I'd like to go back from transparent to the earlier scheme where we used _ <: T to indicate an upper bound for a result type. So it would be

inline def f: _ <: T = ...
inline given g: _ <: T = ...

for whitebox macros. At the same time, I'd like to allow _ <: T as an upper bound of other result types as well. E.g.

inline val x: _ <: Byte = 1

would produce a Byte constant, which was not possible before. Similarly, if we assume #9028,

case object a extends B with C with D
def f: _ <: Product = a

f would get type B with C with D with Product, so there's not need anymore to list all supertypes.

The rules for this are straightforward

• When inferring the type of a val or def with _ <: R result type, R is taken as the expected type of the right hand side.
• The inferred type is then the type of the RHS, widened as usual, with upper bound R

[joroKr21]

Is it possible to drop the wildcard as in def f <: Product or was that ruled out as too subtle?

[odersky]

The wildcard is needed for the given case so for consistency we should have it everywhere.

[nicolasstucki]

Not sure about the second rule. We have to be careful with when widening types in vals

inline val x = 1 // should be: val x: 1 = 1 
inline val y: _ <: Int = 1 // should be: val y: 1 = 1 
inline val z: Int = 1 // error

With inline vals we have the additional restriction that the type must be a content type. Otherwise we would need to change the way we inline vals.

[nicolasstucki]

This is related to #8850. There we tried to use this same typing scheme for vals but using transparent.

[nicolasstucki]

Is it possible to drop the wildcard as in def f <: Product or was that ruled out as too subtle?

That was the previous syntax. It caused too much confusion in several situations.

[nicolasstucki]

Shouldn't we have the following to align with the normal given syntax?

inline given g as _ <: T = ...
inline given _ <: T = ...

[nicolasstucki]

Maybe something like

type Precise[T] <: T // magical type
inline def f: Precise[T] = ...
inline given g as Precise[T] = ...

[liufengyun]

What about introduced Refined, tell the compiler it's white-box:

type Refined[T] = T

inline given g as Refined[T] = ...
inline val x: Refined[Byte] = 1

[odersky]

@liufengyun @nicolasstucki The problem with normal types is that you then have to explain why these _cannot_ be used in other places.

One compromise would be to use <: and brackets:

inline given g as <:[T] = ...
inline val x: <:[Byte] = 1
inline def f(x: S): <:[T] = ...

The <: is syntax since <: is a keyword, but it looks like a type.

But that might be even more surprising , so I am not sure it's better than _ <: T.

[nicolasstucki]

_ <: T looks more natural

[liufengyun]

What about regarding it as a generalization of type ascriptions? The typing rule for a type ascription expression is like the following:

    Γ ⊢ e : T
------------------
  Γ ⊢ (e : T) : T

If we introduce e: T @refine, we could give the following typing rule:

   Γ ⊢ e : S     S <: T
--------------------------
  Γ ⊢ (e : T @refine) : S

We could introduce a short-hand for @refined:

type Refined[T] = T @refined

Updated: seen from the perspective of type ascriptions, it seems to suggest the following:

e <: T   // syntax for refinable type ascription 

inline given g = e <: T
inline val x = 1 <: Byte
inline def f() = e <: T

[LPTK]

Could this be used as a general syntax for expressing "do not widen here"?

This would solve the long-lasting issue of https://github.com/lampepfl/dotty/issues/3964 (and its predecessors https://github.com/lampepfl/dotty/issues/3920, https://github.com/lampepfl/dotty/issues/1262).

trait Context {
  type Tree
}

class Helper(val ctx: _ <: Context) {
  def f(x: Int): ctx.Tree = ???
}

val ctx  : Context   =  ???
val tree : ctx.Tree  =  new Helper(ctx).f(5)

[soronpo]

I probably missed a discussion somewhere, but what was the problem with directly writing x <: Int instead of x : _ <: Int?

[odersky]

@soronpo x <: Int does not work for givens.

In the end I have found it's not worth it. I tried to implement it in #9048, but that introuced more complexity than I have liked. Others at LAMP were not keen on the change either, so we'll leave it as it is.