Excessively loose type inference

[Bersier]

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]

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]

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]

@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]

We can't change type inference rules.

[Bersier]

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

I see two main options:

1. The rules are specified somewhere.
2. 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]

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.

#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]

@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.