SIP-48 - Precise Type Modifier

[soronpo]

Currently the Scala compiler is eager to widen types in various situations to minimize entropy.
We propose adding a precise modifier (soft keyword) that the user can apply on type parameter declaration to indicate to the compiler that the most precise type must be inferred.

[soronpo]

@julienrf can you please assign reviewers for this SIP?

[sjrd]

@julienrf has been on vacation this week, and is still on vacation next week.

I'll take it upon myself to assign @odersky , @lrytz and @gabro, based on the current "load" of open proposals.

[raulraja]

Thanks @soronpo , this looks great!

I think supporting this at the class level may be confusing because of subclassing and how we can depend on third-party base classes.
If classes are allowed, I think subclasses would need to carry the annotation. If it inferred automatically different rules of typing without being explicit in the annotation, the user might be left wondering what's causing the methods not to type as usual.

If some code depends on a base class that is not in the local module, the user may not understand why after a release of a library, their @precise typing affects their local scope. They'd have to visit and inspect the dependency sources manually.

[julienrf]

Dear reviewers, this is a kind reminder to leave a review on this proposal.

[julienrf]

This is another kind reminder, @lrytz, @gabro, and @odersky, please review the submission.

[lrytz]

I think this proposal is well motivated and addresses a real problem. It's not very easy to evaluate because the problem is due to a set of ad-hoc rules (widening), and the solution is to overlay another set of ad-hoc rules (@precise mode handling). It seems to me a lot of work went into finding these rules and make them work well for real examples, which is probably the best that can be done.

IIUC, the risk for breaking changes is very low, and refining the rules in the future is possible.

So support accepting this proposal - but I'm interested to hear other opinions, and other ideas how this could be addressed.

[odersky]

This is an interesting approach to solve some difficulties with dependent typing in Scala. Scala's current term-depending constructs are:

• Path dependent types such as p.T
• Singleton types such as p.type
• Constant types such as 2, "abc"
• Inlining to expose more values as constants or paths

One push to generalize this is to put more and more term operations into the types. compiletime.ops is an example.
So, if A and B are singleton types, A + B would also be a singleton type. This approach hits the problem that singletons are currently widened too easily and that problem is addressed with the @precise annotation.

The annotation is quite sweeping, as explained in the proposal. It gets propagated to new types and serves as a mode switch for the typing of whole expressions (in precise mode or not). It has many feature interactions with the rest of the typer.

One small remark is that I think such a sweeping change should not be indicated by an annotation. If we do that, we lower the barrier for all sorts of other sweeping changes in the typer since after all it's easy to add annotations. So this should be at least a soft modifier, keeping to the principle that annotations should not affect typing.

But I have also two fundamental concerns about the strategy proposed in the SIP:

1. This would put us on a very definite path how dependent typing is organized in operations over singleton types. I find that way to do dependent typing a bit obscure and artificial.
2. In the end this will cause a lot of duplication in the language since every major term level operation will be duplicated on the type level, now working on singleton types with fallbacks if type arguments are not singletons. I fear that there will be a long period where we need to add more and more stuff to typelevel ops and in the end we will have two versions of almost everything, which will feel clunky.

I believe before going down that road, we should have a thorough exploration what our options are. For instance, one radical alternative would be to embrace more generalized dependent typing. Starting with the Vec example in the proposal, here is an alternative way to write it:

dependent class Vec(size: S):
  def ++ (that: Vec(s)): Vec(size + s) =
    Vec(size + that.size)  // Vec(size + s) would work as well
val v1 = Vec(1)
val v1T: Vec(1) = v1
val v2 = Vec(2)
val v2T: Vec(2) = v2
val v3 = v1T ++ v2T
val v3T: Vec(3) = v3
assert(v3T.size == 3)
val one = 1
val vOne = Vec(one)
val vOneT: Vec(one) = vOne
val vTwo = Vec(one + 1)
val vTwoT: Vec = vTwo
val vThree = vOneT ++ vTwoT
val vThreeT: Vec = vThree
assert(vThreeT.size == 3)

In that approach, all values are kept in terms, instead of being injected in types. By contrast, we generalize the concept of a "path" to also include pure terms that are computed, I think this in the end much more natural. To give an example, when we use path dependent types we write p.T, i.e. p is treated as a term. If we followed the philosophy of this pre SIP, it would be more logical to write p.type # T instead. (i.e. use the singleton mechanism to inject a term into a type, then work on the types). But we don't do that since it feels artificial.

Of course much more work is needed to actually work out what richer dependent typing in Scala should mean and to implement it. This won't be done by tomorrow. But I fear that if we go down the singleton road, we effectively block the possibility of adopting the more natural dependent typing road later. First, a lot of effort will be put in making the singleton type system expressive enough, which is effort which could have been spent on brining general dependent typing to life. Second, we will afterwards have a lot of code that uses singletons, all of which would become legacy code once we introduce dependent typing. This will be a problem for the adoption of dependent typing since then there would be two ways to do anything, and the other way was already established.

I realize this is a frustrating position to take. We have something that solves a real problem, why delay it for something else that is not even worked out yet? To address this, I think we should prioritize an open exploration what dependent typing in Scala should look like. What are the use cases that we want to support? What would different solutions look like? I think it would be good to have a small group that looks at these issues. @soronpo and @mbovel should be part fo the group. I'd like to participate as well, and we should also invite anybody else who has an interest of dependent typing in Scala and is willing to put in some work to make it happen.

[odersky]

A completely separate question is whether we want something like precise as a replacement for Singleton bounds. Singleton bounds are unsound in the presence of union types and precise is a possible replacement. But then it should be a priori much more restricted. I.e. it should not propagate and it should not create a mode for typing a whole expression.

[soronpo]

Proper disclosure: My (company's) project is highly dependent on precise typing

---

Thank you for the review. Here are my thoughts:

One small remark is that I think such a sweeping change should not be indicated by an annotation. If we do that, we lower the barrier for all sorts of other sweeping changes in the typer since after all it's easy to add annotations. So this should be at least a soft modifier, keeping to the principle that annotations should not affect typing.

I will modify the proposal to be modifier-based

1. This would put us on a very definite path how dependent typing is organized in operations over singleton types. I find that way to do dependent typing a bit obscure and artificial.

I don't agree. All this proposal does is specifying where the widening rules are changing. Widened vs. precise typing is not directly correlated with dependent typing. People have been using dependent typing thus far without a problem except for specific use-cases such as described in this proposal.

2. In the end this will cause a lot of duplication in the language since every major term level operation will be duplicated on the type level, now working on singleton types with fallbacks if type arguments are not singletons. I fear that there will be a long period where we need to add more and more stuff to typelevel ops and in the end we will have two versions of almost everything, which will feel clunky.

Again, not part of this proposal. Compiletime-ops are part of the language, and this proposal does not do anything to expand on them. If we can go back in time, maybe it is something worth revisiting, but even without compiletime-ops this proposal has merit.

dependent class Vec(size: S):
  def ++ (that: Vec(s)): Vec(size + s) =
    Vec(size + that.size)  // Vec(size + s) would work as well

Something about this syntax does not make sense. Where does S come from?
In any case, the dependent class modifier affects the whole class and is dedicated to dependent typing. The precise modifier is no directly related, IMO.

I realize this is a frustrating position to take. We have something that solves a real problem, why delay it for something else that is not even worked out yet?

THIS. Yes, I understand the long-term motivation, but this proposal, despite the dependent-type motivation, solves real problems. Those problems are even often perceived to be bugs, before learning that they are (undocumented?) rules that could just as easily been otherwise decided earlier on in the language and someone would have come up with a @widen annotation instead.

Exploring dependent classes or other solutions is important, and I would gladly participate in the related discussions/working group, but as I see it, it is a VERY long process that may even require a major language change. I don't see any reason to hold this change up for that.

[soronpo]

A completely separate question is whether we want something like precise as a replacement for Singleton bounds. Singleton bounds are unsound in the presence of union types and precise is a possible replacement. But then it should be a priori much more restricted. I.e. it should not propagate and it should not create a mode for typing a whole expression.

I agree. It sounds like in this case we need a singleton type modifier and deprecate Singleton as an upper-bound. That's a separate proposal.

[odersky]

Something about this syntax does not make sense. Where does S come from?

I thought it would be introduced as a fresh variable. I wanted to have some way to distinguish a Vec argument with unknown size from a Vec argument with known size. But in fact, that might be unnecessary. Altermatively, we might want to formulate it this way:

dependent class Vec(size: S):
  def ++ (that: Vec): Vec(size + that.size) =
    Vec(size + that.size) 

The question is how to type xs ++ ys if ys is of type Vec with unknown size. We'd need some sort of computation with bottom in this case. I.e. that.size is bottom (undefined), hence, size + that.size is also undefined, hence the type of the operation's result is Vec without a size refinement. That might be ultimately simpler.

[odersky]

Exploring dependent classes or other solutions is important, and I would gladly participate in the related discussions/working group, but as I see it, it is a VERY long process that may even require a major language change. I don't see any reason to hold this change up for that.

To be clear: I believe adding @precise is a major language change as well. It influences quite fundamentally the typing for whole expressions in a kind of mode switch. We never had that for Scala, and my first reaction to it is fairly negative. Generally, modes should be avoided.

[soronpo]

I changed the proposal to adding a precise modifier instead of a @precise annotation.
Please recommend either to accept or reject so we can move on.

[odersky]

I see two levels in the proposal which could be treated separately.

1. The introduction of a precise modifier for a single type variable and how it is propagated.
2. The introduction of a "precise typing mode".

For the first level, the current propagation rules don't really correspond to anything in the spec or the compiler that we have already defined. A lot more effort would be needed to make them unambiguous wrt all possible feature interactions and to ensure they are implementable. My hunch is that it would ultimately be simpler to extend the design we have for hard unions to singleton types.

This part of the proposal also overlaps with Singleton bounds. Singleton bounds are unsound and we urgently need a replacement. I would argue that anything we do on this topic should also fix the problem with Singleton bounds.

For the second level (precise typing mode), I am quite skeptical. This is a very significant language change that will have lots of interactions with everything. And it's a mode, which does not feel very Scala-ish to me. It's not excluded that this could still be the best way to introduce dependent typing in Scala. But before we settle on that we should at least have explored all the alternatives.

[odersky]

This would need to be defined in more detail. What if a type variable appears in a union or intersection of an instance? If it is an alias of an instance? One would need to enumerate all possibilities as so far the concept of "origin" is not defined in Scala type inference.

[odersky]

One could also consider what's done for union types: distinguish hard and soft singleton types. A hard singleton type is never widened. Hard singleton types arise from explicit declaration:

val x: y.type = y    // `y.type` is a hard singleton type

and they could arise from instantiating precise type variables. That would avoid the definition of "origin".

[soronpo]

This would need to be defined in more detail. What if a type variable appears in a union or intersection of an instance? If it is an alias of an instance? One would need to enumerate all possibilities as so far the concept of "origin" is not defined in Scala type inference.

All the cases that are considered are explicitly specified, so union/intersection/aliases of precise type parameters are not considered. I'll gladly change "origin" to the proper terminology. Any suggestion to modify the spec will be appreciated.

[odersky]

I think you will find that this will be really hard to specify and implement correctly.

[soronpo]

I think you will find that this will be really hard to specify and implement correctly.

Let's assume we can. There are far more complex things in the compiler inference system.
You can review the attempted covering of various feature interactions in the implementation:
https://github.com/lampepfl/dotty/blob/1824ad827f620b6946d56fcbeeeb5a1fe340f26c/tests/neg/precise-typecheck.scala
(there are additional test files, but this is the primary one)

[odersky]

Again, how does this interact with unions and intersections?

[soronpo]

As specified, the term is only precise when applied in a position annotated by a precise type, so the unions/intersections ruling are deferred to that earlier definition (and thus won't be precise, since unions/intersections are not).

[odersky]

Why are tuples special? Should this not apply to any pure constructor?

[odersky]

This is the part where I am very skeptical. I don't think that introducing a typing mode is a good idea. It's a sweeping change that will have lots of interactions with everything.

Some problems:

• Say you want to pass an expression to a precise type variable to avoid widening a union type. But now everywhere in the expression do singleton types are kept precise. What if that's not what you wanted?
• Let abstracting things changes type inference since it might move a sub-expression out of the scope of an expected type.
• The cause for the difference in typing is invisible. There could be some expected type anywhere further out that is propagated by the proposed rules of propagation from a far away place that changes how types are inferred. How to troubleshoot that?

[soronpo]

I'll begin with properly motivating the reasoning behind the precise typing mode. Singletons are non-issue, but when we have expression compositions then we need to consider whether or not we want to support precise typing of such expressions. Tuples are a good example because we cannot change their definition due to backward compatibility (add precise annotation on their parameters), but we still need precise tuples, so what can we do? We can just special-case tuples, but from the discussion thread on contributors I understand that's undesired. So we end up with the only option (I could think about) - an ability to define any applied expression as precise. That is where precise typing (mode) comes in.

[soronpo]

• Say you want to pass an expression to a precise type variable to avoid widening a union type. But now everywhere in the expression do singleton types are kept precise. What if that's not what you wanted?

Known limitation, but without a use-case this is purely academic discussion.

• Let abstracting things changes type inference since it might move a sub-expression out of the scope of an expected type.

Can you please clarify your meaning here?

• The cause for the difference in typing is invisible. There could be some expected type anywhere further out that is propagated by the proposed rules of propagation from a far away place that changes how types are inferred. How to troubleshoot that?

The mode is not that far reaching. It's only active within an expression composition (and some minor exceptions).

[odersky]

One intriguing alternative is to make precise and singleton look like type classes. I.e.

def f[X: precise] 
def g[Y: singleton]

: singleton would be like <: Singleton now, but would exclude unions. : precise would mean no widening for unions or singletons or unions of singletons. The result of an instantiation of such a type variable would be "hard", i..e would not be widened further.

[bjornregnell]

One intriguing alternative is to make precise and singleton look like type classes. I.e.

I like that. Perhaps we even don't need new soft keywords but could have the type classes as marker traits?

def f[X: Precise] 
def g[Y: Singleton]

[odersky]

I like that. Perhaps we even don't need new soft keywords but could have the type classes as marker traits?

That was my first attempt as well. Maybe it's still possible but there are a number of complexities

• If these things are marker traits, they should not generate code for dictionaries (this could be solved by erased definitions).
• There's an issue with how to define type inference. If we say, a type variable's instance type I does not get widened if the implicit search for Singleton[I] and Precise[I] succeeds, that mixes basic type inference with implicit search, which will be very complicated and will probably have bad consequences such as new sources of cyclic reference errors.
• Singleton with upper case is already taken.

[bjornregnell]

Would it then be generalizable to allow e.g.:

val x = (42: Int): precise

?
I mean: perhaps it can be more like a magic type annotation rather than a magic type class?

[odersky]

Would it then be generalizable to allow e.g.:

 val x = (42: Int): precise

No that's actually two different uses of :. The first is a context bound on a type variable. The second is somehow a supertype, but if we apply that to singleton we'd get back the unsoundness.

[mbovel]

Coming back to this comment I posted on the original discussion (July 26):

A general question: it looks to me that type parameters that could be instantiated to singleton types only and that could appear only once look similar in purpose to term-reference types (x.type) which do exactly that: give you a singleton type for a given parameter.

Answer from @soronpo:

.type cannot always be applied. It’s like having a Singleton upper-bound. Some values are not singletons and I want to use them as arguments.

An argument for having separate precise and singleton concepts was that not all expression can be typed as singletons. But I think this should be the case: a satisfying replacement for Singleton should include the ability to precisely track arbitrary values at the type-level. Typing Vec using the proposal in its current state does not enable it:

import annotation.precise
case class Vec[@precise  S <: Int](n: S)
def makeVec[@precise S <: Int]() =
    val m: Int = ???
    Vec(m)
def copy[@precise S <: Int](v: Vec[S]): Vec[S] = v

@main def test() =
    val v /*: Vec[Int]*/ = makeVec()
    val v2 /*: Vec[Int]*/ = makeVec()
    val v3 /*: Vec[Int]*/ = copy(v)
    summon[v.n.type =:= v2.n.type] // Fails, as expected
    summon[v.n.type =:= v3.n.type] // Fails, but would be nice to have

That's one of the reasons I currently favor refinements and path-dependent types to type parameters for such use-cases:

case class Vec(n: Int)
def vec(m: Int) = Vec(m).asInstanceOf[Vec {val n: m.type}]
def makeVec() =
    val m: Int = ???
    vec(m)
def copy(v: Vec) = vec(v.n)

@main def test() =
    val v /*: Vec{n: Int}*/ = makeVec()
    val v2 /*: Vec{n: Int}*/ = makeVec()
    val v3 /*: Vec{n: (v.n : Int)}*/ = copy(v)
    summon[v.n.type =:= v2.n.type] // Fails, as expected
    summon[v.n.type =:= v3.n.type] // Works!

Said otherwise, using field reference types gives us “existential values“ for free. In opposition, we would need something more to support it with type parameters (such as a mechanism to instantiate skolems on function application).

By the way, typing this using <: Singleton is Scala 3.1.3 and following leaks local references 🫠

//> using scala "3.1.3"
case class Vec[S <: Singleton & Int](n: S)
def makeVec[S <: Singleton & Int]() =
    val m: Int = ???
    Vec(m)
def copy[S <: Singleton & Int](v: Vec[S]): Vec[S] = v

@main def test() =
    val v /*: Vec[(m : Int)]*/ = makeVec()
    val v2 /*: Vec[(m : Int)]*/  = makeVec()
    val v3 /*: Vec[(m : Int)]*/  = copy(v)
    summon[v.n.type =:= v2.n.type] // Wait waat
    summon[v.n.type =:= v3.n.type] // Works

[soronpo]

def makeVec[@precise S <: Int]() =
    val m: Int = ???
    Vec(m)

Can you show a use-case where this is actually needed. I fail to see it ATM.
Also, how can dependent classes enable precise tuple support?

[mbovel]

Can you show a use-case where this is actually needed.

makeVec could be called readVec and read a vector from a file for example. In that case, I still would like to track the size, even if it is not constant, such that the following would hold:

val v1 = readVec
val v2 = readVec
v1.tail.zip(v1.init) // Should work
v1.tail.zip(v2.init) // Should fail

[julienrf]

@soronpo What is the status of the proposal? Based on the comments, it seems that the reviewers are not yet fully convinced by the proposed approach. Do you want to keep working on it? Would you like any additional input to move forward?

[soronpo]

@soronpo What is the status of the proposal? Based on the comments, it seems that the reviewers are not yet fully convinced by the proposed approach. Do you want to keep working on it? Would you like any additional input to move forward?

So far I got open-ended reviews and did not yet get replies to my queries in order to resolve the situation.

[soronpo]

@odersky There is a lot of open-ended review here, which prevents me from delivering a finished proposal.
I need to bring this proposal to a binary REJECT/ACCEPT decision.
IIUC, the main two issues are:

• Avoiding a "Precise" mode. While I understand the reluctance, I still don't understand how you would apply a precise modifier on existing constructs like tuples without a precise mode?

def  id[precise T](t: T): T = t
val a = id((1, 2, (3, 4)) //How to make the type ((1, 2, (3, 4)) without a precise mode?

We cannot change the signature of tuples and make them more precise for compatibility reasons.

• How to annotate the precise type argument. We need just to choose a method and not leave this open: a modifier or a marker trait.

Regarding the potential dependent classes, there was a suggestion of a working group but nothing has happened for months and this proposal remains idle. I see no reason for further delay.

[soronpo]

Update:
As agreed in the last SIP meeting, I had a call with @smarter and we went through the current implementation and he showed me the recent hardening of union types. I checked this hardening mechanism against all the feature interaction tests I made for this SIP, and it works very well in most cases. The hardening is dropped in two minor cases and I opened scala/scala3#16818 and scala/scala3#16819 for them.

So from my point of view, I will modify this proposal and implementation to rely on the hardening mechanism and expand it to singletons. The hardening will be enabled using the precise modifier.

[smarter]

So from my point of view, I will modify this proposal and implementation to rely on the hardening mechanism and expand it to singletons. The hardening will be enabled using the precise modifier.

/cc @mbovel who I believe looked into similar stuff

[hmf]

I thought long and hard before I wrote this, but I think maybe a perspective from a simple user may provide useful feedback. I am also interested in your thoughts on what I describe here. Please note that I am not knowledgeable in language design and type inference, so take this with a grain of salt.

First and foremost, I am not the "sharpest tool in the shed", but I do have some experience and yet I still struggle with a "simple" use case that may serve as a test case here. I find that I need to know many rules and details to get this working, including the use of macros. Adding one more annotation or soft modifier is simply increasing to this complexity.

The use case is this: I want to have a class Table[IMap] where IMap is sort of HList map (ICons[K,V,T <: IMap] where K is a key and V is a value). The goal is to represent a data table were each column is kept in the IMap, which is fully typed (in this respect, I think it is similar to the Tuple issue discussed here). The library client should be able to select and/or operate on a column by a key or position. At compile time selecting an invalid column should result in an error. All operations will use the specific column type to operate on that column.

I assume (naively) that all I needed was to use the inline methods to code this. Later I learned about the transparent inline because of typing issues. During this phase I also learned that the types are widened and the use of Singleton. Use of inline showed that I needed to use match types and instanceOf. Then I realized that in order to access the constant keys, I needed to use macros. During this phase I also learned that the types are widened in macros, so in the macros I have to explicitly type the expression to retain the narrowed types. Later I learned that uses of inline and macros have some additional rules and restrictions such as transparent are called first, we cannot summon on generic type parameters in macros, among other things. I think this journey explains what I am trying to get at.

I confess that I don't have an inkling of all the typing issues this involves or if it is feasible, but I believe that if the typing is maintained as narrow a possible throughout the system, simple invariant cases, like the one described above, would be trivial (or al least much simpler) to implement. Alternatively, would it not suffice to use transparent inline to indicate that a user wants to retain narrowing? Or better yet, have only a inline that is always transparent.

In my experience I feel there are too many details for us programmers to grapple with. Please note this is not meant as a diatribe. I believe that simplifying these issues is important, even if it means delaying changes to a major version. Just trying to contribute.

[odersky]

I agree that these are very hairy issues already. I am not sure what the right response is, though. My experience would tell me that it's probably best to back out and declare that one should not try to push things too far since it gets messy. Almost no other language let's you do this because it requires a very complicated type system. Why should Scala be different? Is that really where we want to spend our complexity budget? Or maybe we should look at better error messages and tooling instead?

And, to be clear, any introduction of a mode for precise vs non-precise typing would be a huge complexity booster since it will interact with everything else.

[ftucky]

Here is an example directly translated from local selectable instances:

trait Vehicle extends Selectable:
  def selectDynamic(key:String) : Any 
  val wheels: Int

trait Fleet:
  val vehicle : Vehicle

class MyFleet extends Fleet :
  val vehicle = new Vehicle:  // vehicle : Vehicle ** UNREFINED ** 
    val wheels = 4
    val range = 240

  def foo =
    vehicle.range  // Does not compile

The construction looks natural:

• Seen form Fleet, val vehicle is a Vehicle.
• val vehicle is abstract in Fleet (Fleet enforces its implementations do define a Vehicle`)
• As Vehicle is a Selectable, as such it may manipulate its content in a programmatic way, through a direct call to selectDynamic()
• Seen from MyFleet, val vehicle is (expected to be) a Vehicle { val range : Int }. This is purpose of local selectable instances feature.
• Accessing to vehicle.range from method foo in MyFleet is expected to work.

However, the widening of val vehicle in MyFleet to its abstract val vehicle:Vehicle in Fleet defeats the purpose.
Worse, no workaround looks straight:

• type ascription val vehicle: Vehicle { val range : Int } = new Vehicle: . Heavy, redundant and error-prone (likely to add a field into the anonymous class, and forget to write it back. The anonymous class may be itself deported further away)
• final val. final val vehicle = new Vehicle: . Happen to work. But final val are expected to be phased out at some point.

Furthermore:

• inline val vehicle = new Vehicle: is not legal. ("Inline value must contain a literal constant")
• inline def vehicle = new Vehicle: is not the intended behavior.
• A precise type-modifer or type-annotation would not help. More looking for member-modifier precise val vehicle = ...
• The type-not-to-be-widened is a refinement-type, not a Singleton.

I am absolutely not a compiler expert, consider the following remark as an humble contribution.
It looks like the existing final val / final def is what we are looking for precise val / precise def:

• On the one hand, it prevents the undesired widening.
• On the other hand, it kills any propagation issue in the egg by preventing overload.

This seems decent, as it decides of member type root of trust.
The default is to place the trust in the class hierarchy. Type defined locally, possibly by ascription, and possibly widened to its abstract definition.
The final modifier shifts the trust into to the right-hand-side definition. ( a macro, a transparent inline, a selectable local instance ...). By shifting the trust, the class also yields its authority. The definition of the type is not its responsibility anymore, and it cannot guarantee the conformance with unknown overloads.

[soronpo]

After further thought, I see no possible avenues to escape the need for a precise mode. Not only that, in case of overloading, an argument may be needed to be typed twice (once imprecisely, and then precisely). So I first need a tentative acceptance of these before there is any point in reimplementing the SIP based on the hardened unions concept and adding a singleton modifier. I'll be happy to be wrong about this, so I'll now explain why and feel free to chime in and contradict any assumption or deduction.

Assumption 1
We must support precise tuples, e.g.:

def id[precise T](t: T): T = t
val tpl = id(((1, 2L), "3"))
summon[tpl.type =:= ((1, 2L), "3")]

Assumption 2

We must preserve backward compatibility so that methods/classes without a precise modifier will act the same.

Assumption 3

We must support overloading where some functions have precise type modifiers and some do not.

Deduction 1: We need a precise mode

From Assumptions 1 & 2, I infer that we must have a precise mode. Let's assume that we do not have a precise mode, and see what happens. When we apply ((1, 2L), "3") as an argument to id, the internal tuple composition typecheck will be (Int, Long) before the typecheck of the entire tuple. So without precise mode, the typer would only apply precise typing when it sets the type for the entire tuple as ((Int, Long), "3"), so too late as we already lost the precise information of the internal (1, 2L) tuple. The only way to propagate that information throughout the type composition is using a flag (mode) that is raised as a result of hitting the precise modifier, AFAIK.

What about hard unions, can that technique prevent requirement of precise mode?

No. Hard unions are already marked as hard at their definition-site, so it cannot help a general literal tuple composition that is applied as an argument in a im/precise argument position.

Deduction 2: In some situation we need to typecheck precise arguments twice

Consider the following example:

@targetName("idTuple")
def id[precise T <: Tuple](t: T): T = t
@targetName("idInt")
def id[T <: Int](t: T): T = t

val tpl = id(((1, 2L), "3"))
summon[tpl.type =:= ((1, 2L), "3")]
val one = id(1)
summon[one.type =:= Int]

Due to overloading (Assumption 3), the typechecker must first choose the proper function according to the applied arguments types and only then it can typecheck the arguments correctly according to the precise modifier (or its absence). Since by default most arguments are imprecise, then the most straightforward implementation is to leave the overloading typechecking as-is. Once overloading is done and we have a concrete function chosen, then the typer looks for the precise modifier and runs type checking again for those arguments.

[soronpo]

After further thought, I see no possible avenues to escape the need for a precise mode.

@odersky @smarter please respond to this.

[smarter]

I'm on vacation currently, I can only look into this SIP again sometimes next month.

[soronpo]

I'm on vacation currently, I can only look into this SIP again sometimes next month.

OK, maybe we'll just discuss this during the meeting in Madrid. Enjoy your vacation!

[soronpo]

After further thought, I see no possible avenues to escape the need for a precise mode. Not only that, in case of overloading, an argument may be needed to be typed twice (once imprecisely, and then precisely). So I first need a tentative acceptance of these before there is any point in reimplementing the SIP based on the hardened unions concept and adding a singleton modifier. I'll be happy to be wrong about this, so I'll now explain why and feel free to chime in and contradict any assumption or deduction.

Assumption 1 We must support precise tuples, e.g.:

def id[precise T](t: T): T = t
val tpl = id(((1, 2L), "3"))
summon[tpl.type =:= ((1, 2L), "3")]

Assumption 2

We must preserve backward compatibility so that methods/classes without a precise modifier will act the same.

Assumption 3

We must support overloading where some functions have precise type modifiers and some do not.

Deduction 1: We need a precise mode

From Assumptions 1 & 2, I infer that we must have a precise mode. Let's assume that we do not have a precise mode, and see what happens. When we apply ((1, 2L), "3") as an argument to id, the internal tuple composition typecheck will be (Int, Long) before the typecheck of the entire tuple. So without precise mode, the typer would only apply precise typing when it sets the type for the entire tuple as ((Int, Long), "3"), so too late as we already lost the precise information of the internal (1, 2L) tuple. The only way to propagate that information throughout the type composition is using a flag (mode) that is raised as a result of hitting the precise modifier, AFAIK.

What about hard unions, can that technique prevent requirement of precise mode?

No. Hard unions are already marked as hard at their definition-site, so it cannot help a general literal tuple composition that is applied as an argument in a im/precise argument position.

Deduction 2: In some situation we need to typecheck precise arguments twice

Consider the following example:

@targetName("idTuple")
def id[precise T <: Tuple](t: T): T = t
@targetName("idInt")
def id[T <: Int](t: T): T = t

val tpl = id(((1, 2L), "3"))
summon[tpl.type =:= ((1, 2L), "3")]
val one = id(1)
summon[one.type =:= Int]

Due to overloading (Assumption 3), the typechecker must first choose the proper function according to the applied arguments types and only then it can typecheck the arguments correctly according to the precise modifier (or its absence). Since by default most arguments are imprecise, then the most straightforward implementation is to leave the overloading typechecking as-is. Once overloading is done and we have a concrete function chosen, then the typer looks for the precise modifier and runs type checking again for those arguments.

We discussed this during the SIP meeting on Sep. 11th 2023, and indeed it was recognized that there is no way around precise mode and double typing in some cases. It was also mentioned that there is no apparent enough community/industry request for this to merit the possible complication and it's not necessarily the right direction for Scala.
In light of all the above, I'm withdrawing the SIP, at least until there is enough examples from the community of a need for this SIP.