[Experiment] Introduce hard ConstantTypes

[mbovel]

As other precise types, constant types are currently often widened away. For example:

val a: 3 = 3
val b /* : Int */ = a

For union types, there exists a concept of softeness: hard unions are union types explicitly written by the user, while soft unions are created by the compiler (for example as the result of a condition or a match). The former are not widened, while the later are:

val bool: Boolean = true
val str: String = "hello"
val int: Int = 42
val c /* : Matchable */ = if bool then str else int // Soft union String | Int widened to Matchable
val d: String | Int = if bool then str else int // Explicitly typed as hard union String | Int
val e /* : String | Int */ = d // Hard unions are not widened

This PR adds the same softeness concept to constant types, such that constant types explicitly typed by the user are not widened:

val a: 3 = 3 // Now, this is a hard constant type
val b /* : 3 */ = a // Not widened

Previous attempt: #14347, which was only handling singletons inside hard unions.

[mbovel]

With this change, "a" |<hard> String would not be widened to String anymore. I could add something like || tp1w <:< tp2w || tp2w <:< tp1w here if we want that.

[mbovel]

Do we need a trait for that? Or could isSoft be a method of Type directly, returning true by default?

To do:

• Find a better name
• Documentation

[dwijnand]

It's never consumed as its upper type, and there's no "shared implementation". So I'd just define/redefine it on SingletonType/ConstantType, and maybe link the docs if they're extensive. Just IMO 😄

Oh, otherwise I'd call it Softness or just IsSoft.

[mbovel]

test performance please

[dottybot]

performance test scheduled: 4 job(s) in queue, 1 running.

[dottybot]

Performance test finished successfully:

Visit https://dotty-bench.epfl.ch/14360/ to see the changes.

Benchmarks is based on merging with master (8ae2962)

[soronpo]

Could you please describe a little more what this PR is about?
I may have some relevant input, but I do not know what the scope of this PR is.

[mbovel]

Could you please describe a little more what this PR is about?
I may have some relevant input, but I do not know what the scope of this PR is.

Description updated 😄 Note: my PRs in draft state are generally just experiments or work in progress and not ready to be reviewed. There are still some tests not passing on this one, but I'd be happy to have your feedback on the idea already!

[soronpo]

OK, now that I know what this PR is about, here is a feedback regarding the idea (not a review).
To get around widening in Scala is not very simple.
There are several issues. One is regarding what you're trying to solve here.
Another when covariance and contravariance is introduced: #8231
More related discussions:
scala/bug#10838
https://contributors.scala-lang.org/t/singleton-subtyping-and-can-we-mark-scala-singleton-as-experimental/2797

I think there are various ways we've come to live with widening and rely on it without realizing them, so changing this behavior without things breaking is risky business (sadly, because my use-cases suffer from this).

Questions you should be able to answer before proceeding:

1. What do you do with tuples:

  val x = (2, 2) //is the type (2,2) or (Int, Int)
  val y = (1 | 2, 4) //what is the type here?
  class Foo
  val foo = new Foo
  val z = (1, foo) //is the type (Int, Foo) or (1, foo.type) 

2. What do you in if expressions:

  val x = if (cond) 1 else 1 //is the type Int or 1
  val y = if (cond) 1 else 2 //is the type Int or (1 | 2)

3. Do you change the widening default when assigning arguments?

  def foo[X <: Int](x : X) : X = x
  val x = foo(5) //is the type Int or 5? No need for `& Singleton` ?

[mbovel]

@soronpo thanks for the pointers! I am starting to see how much various parts of the compiler depend on widening and how tricky it is to change it.

This PR tries to address a narrower problem than the general problem of precise types, which is only to preserve constant types explicitly written by the user. For example, we currently have:

val x: String | Int = ???
val y /* : String | Int */ = x

But:

val x2: "a" | 1 = ???
val y2 /*: Matchable */ = x2

Said otherwise, a more precise type is widened to a more general type, which is counter-intuitive. It seems to me that this could be solved independently of the general problem of precise types.

Note that singleton types in type applications and tuples such as in your first example are preserved:

val x3: (2, 2) = ???
val y3 /* : (2, 2) */ = x3

[mbovel]

@soronpo for your examples 2 and 3, it seems like doing less widening in these situations in general would break too much existing code. However, I started experiencing with a precise modifier that would among other things turn off widening:

precise def f() =
  val b: Boolean
  val x /* : 1 | 2 */ = if b then 1 else 2

This could be an opt-in way to get more precise types in general and inference in particular. What would you think about something like that? I'll post my early-stage experiment soon so that we can discuss with more material.

[mbovel]

In the current state, there at least two problems with this PR:

1. It is assumed in the snippet below (and maybe in other places) that recursively widening a singleton type yields a non-singleton type. This is not true if some singletons are not widened and it results in an infinite loop. https://github.com/lampepfl/dotty/blob/18e3cac34bf397ebb180812b5cb90af2066922f7/compiler/src/dotty/tools/dotc/typer/Implicits.scala#L938-L939
2. ConstantTypes hashes are used both for hash consing and equality. For the first case, isSoft field should be included but not for the later. Doing so breaks atoms comparison for example: https://github.com/lampepfl/dotty/blob/ef25672ed2ce13e6f882f3d59ac8439562458b7c/compiler/src/dotty/tools/dotc/core/TypeComparer.scala#L1426

[soronpo]

@soronpo for your examples 2 and 3, it seems like doing less widening in these situations in general would break too much existing code. However, I started experiencing with a precise modifier that would among other things turn off widening:

precise def f() =
  val b: Boolean
  val x /* : 1 | 2 */ = if b then 1 else 2

This could be an opt-in way to get more precise types in general and inference in particular. What would you think about something like that? I'll post my early-stage experiment soon so that we can discuss with more material.

I think exact instead of precise is the better term. I also think it should be a type annotation/modifier and not a term modifier.

[mbovel]

• The specific problem of union types loosing their "hardness" described above has been fixed by Keep softness when widening unions #14399.
• For the question of singletons widening, we need something more general, maybe with an explicit annotation, either at the term or type level. More experiments coming soon.