Excessively loose type inference

Bersier commented 7 months ago

Compiler version

3.3.1 3.4.0-RC4

Minimized code

// Error: Cannot prove that A[U] <:< A[N].
Wrap(new A[N]{})

// Adding the obvious type argument to Wrap makes it compile just fine.
Wrap[N](new A[N]{})

final case class Wrap[T <: U](first: A[T])(using A[T] <:< A[N])

sealed trait A[+T]

type U = Any
type N = Nothing

Compiler output

Cannot prove that A[U] <:< A[N].

Expectation

No error, similarly to when U is inlined, or N is not set to Nothing.

Gedochao commented 7 months ago

Tweaked minimised code (this can be passed to the compiler raw for reproduction, the original post's code is in script format)

final case class Wrap[T <: U](first: A[T])(using A[T] <:< A[N])
sealed trait A[+T]
type U = Any
type N = Nothing

@main def main = {
  // Error: Cannot prove that A[U] <:< A[N].
  Wrap(new A[N] {})
}

Raw output:

-- [E172] Type Error: /Users/pchabelski/IdeaProjects/dotty2/repro.scala:8:19 ---
8 |  Wrap(new A[N] {})
  |                   ^
  |                   Cannot prove that A[U] <:< A[N].
1 error found
Compilation failed

odersky commented 7 months ago

If we forget about the implicit parameter and just write:

final case class Wrap[T <: U](first: A[T])
sealed trait A[+T]
type U = Any
type N = Nothing
def main = Wrap(new A[N] {})

we get as expansion

    type U = Any
    type N = Nothing
    def main: Wrap[Any] =
      {
        Wrap.apply[Any](
          {
            final class $anon() extends Object(), A[N] {}
            new $anon():A[N]
          }
        )
      }

That's what is intended. If a type variable X with an upper bound needs to be instantiated, and the lower bound is Nothing, the upper bound is taken instead. And A counts as an upper bound here. This could be useful and might be used already elsewhere to influence type inference. So tweaking the rules as #19735 does just to make this test pass is out.

Bersier commented 3 months ago

@dwijnand Could the closure of this issue be reconsidered, based on the arguments I put forth in this thread?

Violation of general principles is often worth investigating carefully.

P.S.: See also this issue.

dwijnand commented 3 months ago

We can't change type inference rules.

Bersier commented 3 months ago

@dwijnand What are these type inference rules? And why can they not be amended?

I see two main options:

The rules are specified somewhere.
The compiler itself represents the rules.

If 1 is the case:

Where are these rules specified? (I could find only a few rules in the spec, and no SIP about inference.)
How would fixing this issue change the rules? Which of the specified rules would have to change?
What about this principle? Shouldn't type inference satisfy it? If the rules can lead to its violation, couldn't it indicate an issue with the rules themselves? Spec bugs have happened before, and some have been fixed (see this issue, for example).

If 2 is the case:

Wouldn’t fixing any bug about type inference change the rules?
How is this issue different?

Perhaps it really does not make sense to fix this issue, but "We can't change type inference rules." seems like an insufficient reason in any case.

dwijnand commented 3 months ago

The rules aren't specified, so, yes, fixing bugs changes the behaviour and thus the unspecified rules, and this issue is no different. We've basically moved to not changing them any more.

https://github.com/scala/scala3/pull/19735 is, by the way, my proposed change that fixes your issue, but it could, potentially, affect some other existing inference, so it was rejected. I argued that specifying an alias of Any as the upper bound (equally for Nothing/lower) should behave as if it were omitted.

Bersier commented 3 months ago

@dwijnand Why are all of these issues (and more unlabeled ones) open, then? Shouldn't they all be closed as well?

I was aware of your proposed change. It only seems to address type alias transparency violation.

Might there not possibly be some (complete) fix to this issue that does not affect existing intended inference much? In that case, shouldn't this issue remain open, even if there is no fix for it yet?

Also, I would love to see any valid uses of the current undocumented ad-hoc inference logic for Nothing. I doubt it is used much intentionally, as it violating monotonicity makes it highly counterintuitive, if not flat-out fundamentally wrong.

@odersky wrote

This could be useful and might be used already elsewhere to influence type inference.

That sounds rather hypothetical and unsubstantiated, particularly when compared to the concrete example I gave showing how the current logic is detrimental, as well as the general principles I gave which the current logic violates. It seemed like an acceptable argument against

tweaking the rules as #19735 does just to make this test pass

, but the situation has been shown to be quite different now; the test is just an example of a far more general issue.

SIP-56 was a much larger breaking change (which of course also solved a much more severe issue) to a non-experimental feature of Scala. Even still, it got amended after launch to fix an additional overlooked minor issue.

The amount of breakage that could potentially be incurred by a fix to this issue seems comparatively benign (note it would strictly tighten type inference), even when taking into account that monotonicity is much less important than soundness. One could even argue that monotonicity was an (overlooked) implicit goal of the existing rules all along, in a similar vein to this argument.

Bersier commented 2 months ago

How am I to interpret the lack of response?

Is it due to a lack of resources and low priority? In that case, could the issue be reopened (it can be closed again once someone answers)?

It is still unclear to me how tightening type inference (in a sound way) could possibly cause incompatibilities or other negative consequences. By the Liskov substitution principle, which is partially enforced in Scala's variance system, it should not be possible for such a change to cause issues. Moreover, this change would only affect inference at the type parameter level, so should not affect runtime semantics (due to erasure).

som-snytt commented 2 months ago

The project has Discussions enabled for discussions. https://github.com/scala/scala3/discussions

Usually, tickets are kept open for actionable bugs. Dotty used to have feature-requests for improvements.

Maybe it would be satisfying to have a label for "out of scope".

Bersier commented 1 month ago

@som-snytt How is it not actionable or out of scope? I'm not trying to be difficult. I'd be happy to accept valid arguments showing why this is not an actionable bug. So far, the arguments I have seen seem to be little more than reflexive responses trying to shut down an annoyance (but I might be missing a key point, leading me to misinterpret them). They do not seem to hold up to scrutiny, and seem ignorant of my own detailed arguments. For example, I was told that

The rules aren't specified, so, yes, fixing bugs changes the behaviour and thus the unspecified rules, and this issue is no different. We've basically moved to not changing them any more.

But then, why are other issues regarding inference open? I have trouble believing that no clearly suboptimal behavior of the type inference system is to be fixed from now on, particularly when it would not cause any compatibility issues.

I also wonder how starting a discussion on Dotty Discussions would yield different results from the discussion I led on Scala contributors.

som-snytt commented 1 month ago

Previously, Discussions was visited more by "core" contributors, but that may not be as true any more, since the cast of characters is rotating. (I find the forum less easy to search, and stale topics tend to stay stale.)

Discussions side-steps your questions, in that it is the place for open-ended (not to say non-terminal) discussions. On Scala 2, they added "bug reports are not questions" to the issue template. I have seen concern here that excessive open tickets makes it harder to triage and plan. I think you're right that resource constraints are a deciding factor on tickets. I am failing so far in my own determination to make sure tickets I open are closed, one way or another. One may say, Closed but not forgotten.

SethTisue commented 1 month ago

@Bersier In an ideal world, project maintainers would exist in sufficient numbers that we would have time to write comprehensive responses to every ticket. We don't live in that world. Project maintainers have to constantly choose about what engineering work is best deserving of their time, and they also have to weigh that against how much of their time to spend writing detailed responses to all the tickets that come in — even tickets that we, because of our deep experience and long commitment to the project, have strong reason to believe are unlikely to progress. We're balancing that as best we can, just as all maintainers of all open source projects do, because we must.

I would add that — here and on every open source project — there is a strong bias towards spending time responding to pull requests, rather than to issues. Wishing type inference behaved differently is one thing. Being willing to pour substantial engineering effort into actually improving it, including providing sufficient justification to convince others that the changes are correct and desirable and the right thing and will continue to be the right thing for the years and decades of project work that lie ahead of us, is something else entirely. Ultimately it's that willingness and commitment that drives open source projects. Willingness and commitment both from individual contributors, and from the Center’s member companies and other funding sources that make it possible for the project to exist at all.

Regardless, a great many improvements to Scala have begun because someone such as yourself opened a ticket like this. They're worth opening. But they don't all go anywhere and that's normal.

Bersier commented 1 month ago

@SethTisue Thank you for that detailed answer. It is appreciated, and I agree with all your points. I entirely understand that this might not be of high enough priority to argue about any time soon, if ever.

However, I still think that, as I have provided what I believe are strong arguments supporting the status of this issue as a bug, rather than a feature request, it should remain open until such a time that someone refutes those arguments. That time might never come, in which case this issue would remain open, like many others. And that would be fine.

I would also like to point out that I spent a substantial amount of effort explaining this bug and its significance. In your words:

sufficient justification to convince others that the changes are correct and desirable and the right thing and will continue to be the right thing for the years and decades of project work that lie ahead of us

Though whether the justification provided is actually sufficient is moot if it is unread.

I do not have the expertise to submit a pull request with a fix, unfortunately, but would be open to being taught. It would also be rather pointless to submit a fix before the proposed change is recognized as positive. A closed ticket indicates the contrary.

SethTisue commented 1 month ago

I would also like to point out that I spent a substantial amount of effort explaining this bug and its significance.

Acknowledged, and thank you.

If you consider the open bit crucially important, then if you like, I could convert the closed issue to an open discussion (GitHub allows this). Personally, I take the view is that every closed issue is also an open discussion. It's very rare that we actually lock an issue, so discussion is always free to continue.

I'm afraid we're strict about reserving open issues for clearly actionable bugs rather than potential design changes under discussion. At present, the status is that this is working as designed, and thus the issue is definitely going to stay closed unless new information comes to light. That's just how we roll in this repo.

SethTisue commented 1 month ago

I do not have the expertise to submit a pull request with a fix, unfortunately, but would be open to being taught.

Type inference is quite complicated, so that would require a substantial time commitment. If you or anyone else is interested in getting up to speed, the main pathway we offer is the Scala 3 Compiler Issue Sprees, https://www.scala-lang.org/blog/2022/11/02/compiler-academy.html#logistics — that's a place anyone interested can get a start on tackling smaller issues, regardless of whether they're interested in eventually working up to bigger ones like this one.

dwijnand commented 1 month ago

However, I still think that, as I have provided what I believe are strong arguments supporting the status of this issue as a bug, rather than a feature request, it should remain open until such a time that someone refutes those arguments. That time might never come, in which case this issue would remain open, like many others. And that would be fine.

I agreed and continue to agree to your strong arguments, and I agreed to your issue even before you gave them, submitting #19735 on the 19 Feb. But the change and the argument for the change were rejected, on grounds that I can see how you find to be too hollow.

But I also don't think that this change is a hill to die on, which is why I personally chose not to spent further time trying to advocate for the change, and also why I eventually chose to not keep responding to comments - not because the comments weren't valid, but because the issue is niche and not a priority (at least, to my estimation).

But keeping the issue closed isn't a hill to die on either. Part of the reason why all those inferencing issues are still open is because closing them causes arguments, so we leave them to open, but only in name.

SethTisue commented 1 month ago

I guess we can all agree these distinctions are inherently somewhat blurry :-)

scala / scala3