Skip to content

Avoid interpolating to Nothing in a special case #16328

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
wants to merge 2 commits into from

Conversation

odersky
Copy link
Contributor

@odersky odersky commented Nov 12, 2022

If we have an selection e.m where e's type is a type variable T that does not have a lower bound in the current constraint, avoid interpolating T to Nothing. Doing this would make the section ill-typed. Not interpolating T leaves the possibility open to instantiate it to its upper bound later in couldInstantiateTypeVar.

Fixes #16323

If we have an selection `e.m` where e's type is a type variable T that does not
have a lower bound in the current constraint, avoid interpolating `T` to nothing.
Doing this would make the section ill-typed. By both interpolating `T` we leave
the possibility open to instantiate it to its upper bound in couldInstantiateTypeVar.
@odersky
Copy link
Contributor Author

odersky commented Nov 12, 2022

Note: I tried to avoid interpolating to Nothing in general, but that gives test failures.

@adampauls
Copy link
Contributor

I suppose it's asking too much to also avoid Nothing outside the context of a selection? It's still quite surprising if T comes out as Nothing instead of Foo in that case.

@adampauls
Copy link
Contributor

adampauls commented Nov 13, 2022

Sorry, that's probably what you meant by "in general", which you said gave test failures. I would have thought that with a non-trivial upper bound you could always instantiate to that instead of Nothing, but perhaps that's what you tried.

@odersky
Copy link
Contributor Author

odersky commented Nov 13, 2022

In fact I am no longer sure this PR is a good idea. It's a very special case. We don't interpolate T to Nothing if

  • the type of the expression is exactly T, and
  • the expected type is a selection.

If we drop either of these side conditions, tests go wrong. It's unsatisfactory that

method(y).member

now works but

val x = method(y)
x.member

doesn't. Another shortcoming is that

 def method2[T](c: T => Boolean): (T, T) = ???
 val y: Foo => Boolean = _ => true
 method2(y)._1.member // error

still does not work, because here T is only part of the type we return. So, I have the impression this PR just patches one particular symptom. We need to dig deeper to see whether we can generalize this in some way.

@odersky odersky marked this pull request as draft November 13, 2022 09:55
@adampauls
Copy link
Contributor

adampauls commented Nov 14, 2022

I don't really know what I'm doing here, but this one-line diff

diff --git a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala
index 1dfa048227..2f6093bcc5 100644
--- a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala
+++ b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala
@@ -537,7 +537,7 @@ trait ConstraintHandling {
   final def approximation(param: TypeParamRef, fromBelow: Boolean, maxLevel: Int)(using Context): Type =
     constraint.entry(param) match
       case entry: TypeBounds =>
-        val useLowerBound = fromBelow || param.occursIn(entry.hi)
+        val useLowerBound = (fromBelow && !(entry.lo.isBottomType && !entry.hi.isTopType)) || param.occursIn(entry.hi)
         val rawInst = withUntrustedBounds(
           if useLowerBound then fullLowerBound(param) else fullUpperBound(param))
         val levelInst = fixLevels(rawInst, fromBelow, maxLevel, param)

makes both the tested case and

 val tmp = method(y)
 tmp.member

pass. It only fails two tests:

tests/neg/i15525.scala failed
tests/pos/i864.scala failed

But I didn't really know how to debug from there. I looked a little at i864 and it seemed like A and B were coming out of approximation as Nothing without my fix, which didn't seem right to me.

@smarter
Copy link
Member

smarter commented Nov 14, 2022

It's unsatisfactory that

method(y).member

now works but

val x = method(y)
x.member

doesn't.

This is already the case in various situations where we defer instantiation of a type variable in a prefix (e.g., ListBuffer() += 1), so it's not especially shocking to me.

I suppose it's asking too much to also avoid Nothing outside the context of a selection? It's still quite surprising if T comes out as Nothing instead of Foo in that case.

@adampauls Could you share a concrete example of code you'd like to see typecheck? It's hard to think of a useful implementation of def method[T](c: T => Boolean): T, so the exact choice of T doesn't seem like it'd be important there, but more concrete examples might help.

@adampauls
Copy link
Contributor

It's true that with erasure, method as defined in this example is kind of silly. Realistically, you need T: ClassTag, which of course infers just fine. Still, it did not seem to me like inferring Nothing here is the right thing.

@smarter
Copy link
Member

smarter commented Nov 14, 2022

Still, it did not seem to me like inferring Nothing here is the right thing.

But how do we define what the right thing is? If we care about having the largest amount of meaningful programs infer correctly, then we don't really need to worry about def method[T](c: T => Boolean): T.
On the other hand, we do need to worry about how complex the type inference logic gets, since that makes it harder to reason about and to improve. I have a talk that goes into some details on how things work you might find interesting: https://www.youtube.com/watch?v=lMvOykNQ4zs

@adampauls
Copy link
Contributor

Of course I understand and agree. There are already several places in the code that check whether a lower bound is non-trivial before inferring Nothing and I suspect/hope that this is not any further complication, just an effort to make things consistent.

Nothing is quite strange in that it is in principle the "most specific" type possible because it is a subtype of all types, but unlike normal subtypes, it has fewer methods that its super types. I think it makes sense to avoid inferring it unless necessary, but agree this case isn't very motivating.

@dwijnand
Copy link
Member

Nothing is quite strange in that it is in principle the "most specific" type possible because it is a subtype of all types, but unlike normal subtypes, it has fewer methods that its super types. I think it makes sense to avoid inferring it unless necessary, but agree this case isn't very motivating.

I was going to say that Nothing has all the methods, but your example proves that's not true. Makes me think whether there should be something like a lazy "Sub" type. As in, instead of lubbing A and B, we can defer with A | B. Perhaps there should be a Sub(Foo), which is a little like Nothing, but you can still, for instance, select Foo methods on it.

@adampauls
Copy link
Contributor

A more realistic example that still fails with the ClassTag workaround:

class Foo
trait Typeclass[T] {
  def someString(x: T): String
}
given Typeclass[Foo] with {
  def someString(x: Foo): String = "Foo impl"
}
class Bar(val foo: Foo)
given (Foo => Boolean) = _ => true

val latestTable: Map[scala.reflect.ClassTag[_], Seq[_]] = Map(summon[scala.reflect.ClassTag[Foo]] -> Seq(new Foo))

def typeclassConstrained[T](x: T)(using Typeclass[T]): String = summon[Typeclass[T]].someString(x)
def latest[T: scala.reflect.ClassTag](constraint: T => Boolean): T = {
  latestTable(summon[scala.reflect.ClassTag[T]]).asInstanceOf[Seq[T]].filter(constraint).head
}
typeclassConstrained(latest((x: Foo) => true))

Works fine if latest is called explicitly with [Foo]. In this case, latest (replacing member in the original example) has a reasonable implementation: it tries to find some value of a particular type that satisfies a constraint. This is a simplified version of the real use case we are targeting.

@smarter
Copy link
Member

smarter commented Nov 16, 2022

Thanks for the example! This sort of pattern with ClassTag came up before, but I thought we handled it correctly. In fact, I had a very similar example 7 years ago (!) (#718 (comment)):

import scala.reflect.ClassTag
import scala.reflect.classTag

object Test {
  def getParamType[T: ClassTag](x: T => Int) = println(classTag[T])

  def main(args: Array[String]): Unit = {
    getParamType((x: Int) => x) // dotty: Nothing, scalac: Int
  }
}

But this example infers Int now as expected, so it'd be interesting to figure out what exactly is the critical difference between your example and this simplified one.

@smarter
Copy link
Member

smarter commented Nov 18, 2022

A minimal example that reproduces the problem is:

import scala.reflect.ClassTag
import scala.reflect.classTag

object Test {
  def getParamType[T: ClassTag](x: T => Int): T = ???

  def id[S](x: S): S = x
  
  def main(args: Array[String]) = {
    val x = id(getParamType((x: Int) => x))
    val y: Int = x // error
  }
}

id(getParamType((x: Int) => x)) expands to id[?S](getParamType[?T]((x: Int) => x)), and when we look for an implicit of type ClassTag[?T] the constraints are as follow:

?T <: ?S
?T <: Int

Before doing the implicit search, we instantiate ClassTag[?T] (otherwise we'd have ambiguity errors). This means we need to instantiate ?T and the most general instantiation is ?T := Int & ?S, but this means that ?S is now completely unconstrained since Int & ?S <: ?S is trivially satisfied, so ?S may be instantiated to any type and the compiler chooses Nothing (if it chose Any instead, it wouldn't solve the problem).

I'm not sure if there's anything we can change here that wouldn't break something else, unless our changes are specific to classtag synthesis. This could make sense for improved compatibility with Scala 2, but since ClassTag are already problematic in various ways (#1730, zio/zio#3136 (comment), #7554), so rather than adding more fragile special cases in inference, we might want to encourage replacements instead (e.g. usage of inline def/match).

@soronpo
Copy link
Contributor

soronpo commented Nov 18, 2022

A minimal example that reproduces the problem is:

In which Scala version do you get an error?

@soronpo
Copy link
Contributor

soronpo commented Nov 18, 2022

In fact I am no longer sure this PR is a good idea. It's a very special case. We don't interpolate T to Nothing if

* the type of the expression is exactly T, and

* the expected type is a selection.

If we drop either of these side conditions, tests go wrong. It's unsatisfactory that

method(y).member

now works but

val x = method(y)
x.member

doesn't. Another shortcoming is that

 def method2[T](c: T => Boolean): (T, T) = ???
 val y: Foo => Boolean = _ => true
 method2(y)._1.member // error

still does not work, because here T is only part of the type we return. So, I have the impression this PR just patches one particular symptom. We need to dig deeper to see whether we can generalize this in some way.

Maybe we can handle this via the precise type SIP, to avoid breaking existing code.
If a wildcard is precise then we can prevent it from being inferred as Nothing.

def method[precise T](c: T => Boolean): T

@adampauls
Copy link
Contributor

so ?S may be instantiated to any type and the compiler chooses Nothing (if it chose Any instead, it wouldn't solve the problem).

I'm not sure if there's anything we can change here that wouldn't break something else

Do you really think a lot would break if ?S was instantiated to Int? Perhaps it's worth a shot?

smarter added a commit to smarter/dotty that referenced this pull request Dec 9, 2022
Type variable are normally either instantiated to their lower bound (after some
widening in `widenInferred`) or upper bound. This commit changes this behavior
when the type variable instantiation is forced (which happens in particular
before doing an implicit search, but also when typing the parameters of a
lambda). We now use the "nonParam" bound instead where other type parameters
have been stripped. For example in i16328.scala, when typing

    id(fromParam((x: Base) => x))

we end up with

    id[?S](getParamType[?T]((x: Int) => x))

where
    ?T <: ?S
    ?T <: Base

Before this commit, ?T was then instantiated to ?S & Base (via
Typer#adaptNoArgsImplicitMethod#instantiate), which lead
to an implicit search failure since ?S was left unconstrained.

With this commit, we instead instantiate ?T to its non-param bound `Base`
and propagate this to `?S` itself:

   ?T := Base
   ?S >: Base

The idea is that this leads to constraints being propagated in a more intuitive
way (?S will now be instantiated to Base rather than Nothing or Any), however
this also means that we're adding a whole new way of instantiating type
variables for a seemingly limited number of usecases (see also the discussion
starting at
scala#16328 (comment)).

It's not clear if this won't end up breaking as many things as it fixes, and it
would increase our maintenance burden, so I recommend holding off on this change
for now.
smarter added a commit to dotty-staging/dotty that referenced this pull request Dec 9, 2022
The previous commit ensures that `ClassTag[Int & Nothing]` doesn't compile
anymore so this isn't a soundness issue anymore, but since intersections can
arise out of type inference, it's worth adding a special-case here for
convenience. In particular, this fixes
scala#16328 (comment)
smarter added a commit to dotty-staging/dotty that referenced this pull request Dec 9, 2022
The previous commit ensures that `ClassTag[Int & Nothing]` doesn't compile
anymore so this isn't a soundness issue anymore, but since intersections can
arise out of type inference, it's worth adding a special-case here for
convenience. In particular, this fixes
scala#16328 (comment)
@smarter
Copy link
Member

smarter commented Dec 9, 2022

I tried out an alternative strategy for type variable instantiation in smarter@39b33f5 but I decided to not go forward with it since I wasn't sure the complexity increase was worth it. Instead, I've opened #16492 which special-cases ClassTag instantiation to deal with the examples we discussed.

@odersky odersky closed this in f216ca2 Dec 12, 2022
odersky added a commit that referenced this pull request Dec 12, 2022
…ference failure (#16492)

The first commit generalizes the fix for #1730, the second commit
improves inference in a common situation to generate a valid ClassTag
rather than emitting an error, fixing the example from
#16328 (comment).
little-inferno pushed a commit to little-inferno/dotty that referenced this pull request Jan 25, 2023
The previous commit ensures that `ClassTag[Int & Nothing]` doesn't compile
anymore so this isn't a soundness issue anymore, but since intersections can
arise out of type inference, it's worth adding a special-case here for
convenience. In particular, this fixes
scala#16328 (comment)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Nothing inferred when unexpected
5 participants