Skip to content
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

Fix bounds propagation #232

Closed
wants to merge 2 commits into from

Conversation

odersky
Copy link
Contributor

@odersky odersky commented Nov 17, 2014

When instantiating with a wildcard argument, take formal parameter
bounds into account. Review by @adriaanm @DarkDimius

When instantiating with a wildcard argument, take formal parameter
bounds into account.
@DarkDimius
Copy link
Member

LGTM, but needs rebasing.
Also conflicts with #213

@retronym
Copy link
Member

Here's a tougher example. I was motivated to try out when I saw the call to tparam.info, which should always beg the question, "are we accounting for the prefix?".

// sandbox/test.scala
class Base {
  type N

  class Tree[-T >: N]

  def f(x: Any): Tree[N] = x match {
    case y: Tree[_] => y
  }
}
class Derived extends Base {
  def g(x: Any): Tree[N] = x match {
    case y: Tree[_] => y // fails in both scalac and dotc
  }
}
% scalac-hash v2.11.4 ./tests/neg/boundspropagation.scala
./tests/neg/boundspropagation.scala:14: error: type mismatch;
 found   : Derived.this.Tree[_]
 required: Derived.this.Tree[Derived.this.N]
    case y: Tree[_] => y
                       ^
one error found

% scalac-hash v2.11.4 -explaintypes ./tests/neg/boundspropagation.scala
./tests/neg/boundspropagation.scala:14: error: type mismatch;
 found   : Derived.this.Tree[_]
 required: Derived.this.Tree[Derived.this.N]
    case y: Tree[_] => y
                       ^
Derived.this.Tree[_] <: Derived.this.Tree[Derived.this.N]?
  Derived.this.type = Base.this.type?
  false
false
one error found
(remotes/origin/pr/232) ~/code/dotty ./bin/dotc -explaintypes ./tests/neg/boundspropagation.scala
./tests/neg/boundspropagation.scala:14: error: type mismatch:
 found   : Derived.this.Tree[Base.this.N](y)
 required: Derived.this.Tree[Derived.this.N]
Constraint(
 uninstVars = ;
 constrained types = ;
 constraint = )
Subtype trace:
  ==> Derived.this.Tree[Base.this.N](y) <:< Derived.this.Tree[Derived.this.N] class dotty.tools.dotc.core.Types$TermRefWithFixedSym class dotty.tools.dotc.core.Types$PreHashedRefinedType
    ==>  >: Base.this.N <:<  =- Derived.this.N class dotty.tools.dotc.core.Types$CachedTypeBounds class dotty.tools.dotc.core.Types$ContraTypeBounds
      ==> Derived.this.N <:< Base.this.N class dotty.tools.dotc.core.Types$CachedTypeRef class dotty.tools.dotc.core.Types$CachedTypeRef
        ==> Derived(Derived.this) <:< Base(Base.this) class dotty.tools.dotc.core.Types$CachedThisType class dotty.tools.dotc.core.Types$CachedThisType
        <== Derived(Derived.this) <:< Base(Base.this) class dotty.tools.dotc.core.Types$CachedThisType class dotty.tools.dotc.core.Types$CachedThisType = false
        ==> Derived.this.N <:< Nothing class dotty.tools.dotc.core.Types$CachedTypeRef class dotty.tools.dotc.core.Types$CachedTypeRef
          ==> Any <:< Nothing class dotty.tools.dotc.core.Types$CachedTypeRef class dotty.tools.dotc.core.Types$CachedTypeRef
          <== Any <:< Nothing class dotty.tools.dotc.core.Types$CachedTypeRef class dotty.tools.dotc.core.Types$CachedTypeRef = false
        <== Derived.this.N <:< Nothing class dotty.tools.dotc.core.Types$CachedTypeRef class dotty.tools.dotc.core.Types$CachedTypeRef = false
        ==> Any <:< Base.this.N class dotty.tools.dotc.core.Types$CachedTypeRef class dotty.tools.dotc.core.Types$CachedTypeRef
          ==> Any <:< Nothing class dotty.tools.dotc.core.Types$CachedTypeRef class dotty.tools.dotc.core.Types$CachedTypeRef
          <== Any <:< Nothing class dotty.tools.dotc.core.Types$CachedTypeRef class dotty.tools.dotc.core.Types$CachedTypeRef = false
        <== Any <:< Base.this.N class dotty.tools.dotc.core.Types$CachedTypeRef class dotty.tools.dotc.core.Types$CachedTypeRef = false
      <== Derived.this.N <:< Base.this.N class dotty.tools.dotc.core.Types$CachedTypeRef class dotty.tools.dotc.core.Types$CachedTypeRef = false
    <==  >: Base.this.N <:<  =- Derived.this.N class dotty.tools.dotc.core.Types$CachedTypeBounds class dotty.tools.dotc.core.Types$ContraTypeBounds = false
  <== Derived.this.Tree[Base.this.N](y) <:< Derived.this.Tree[Derived.this.N] class dotty.tools.dotc.core.Types$TermRefWithFixedSym class dotty.tools.dotc.core.Types$PreHashedRefinedType = false
Implicit search failure summary:
  No implicit candidates were found that convert from Derived.this.Tree[Base.this.N](y) to Derived.this.Tree[Derived.this.N]
    case y: Tree[_] => y
                       ^
one error found

@retronym
Copy link
Member

Here's patch that makes this typecheck under scalac. I was using a bit of trial and error to get the right clazz to pass to asSeenFrom, and the result looks ad hoc. In the test case, it must be class Base, so starting from type param T we can get there with tparam.enclClass.owner.enclClass.

diff --git a/src/compiler/scala/tools/nsc/typechecker/Typers.scala b/src/compiler/scala/tools/nsc/typechecker/Typers.scala
index a182a2e..dffed83 100644
--- a/src/compiler/scala/tools/nsc/typechecker/Typers.scala
+++ b/src/compiler/scala/tools/nsc/typechecker/Typers.scala
@@ -4923,8 +4923,10 @@ trait Typers extends Adaptations with Tags with TypersTracking with PatternTyper
                 val TypeBounds(lo1, hi1) = tbounds.subst(tparams, argtypes)
                 val lo = lub(List(lo0, lo1))
                 val hi = glb(List(hi0, hi1))
-                if (!(lo =:= lo0 && hi =:= hi0))
-                  asym setInfo logResult(s"Updating bounds of ${asym.fullLocationString} in $tree from '$abounds' to")(TypeBounds(lo, hi))
+                if (!(lo =:= lo0 && hi =:= hi0)) {
+                  val boundsSeenFrom = TypeBounds(lo, hi).asSeenFrom(tpt1.tpe.prefix, tparam.enclClass.owner.enclClass)
+                  asym setInfo logResult(s"Updating bounds of ${asym.fullLocationString} in $tree from '$abounds' to")(boundsSeenFrom)
+                }
               }
               if (asym != null && asym.isAbstractType) {
                 arg match {

/cc @adriaanm

@retronym
Copy link
Member

I've logged this as https://issues.scala-lang.org/browse/SI-8991

@retronym
Copy link
Member

Here is an example that typechecks in scalac but fails to do so in dotc.

class Base {
  type N

  class Tree[-S, -T >: Option[S]]

  def g(x: Any): Tree[_, _ <: Option[N]] = x match {
    case y: Tree[_, _] => y
  }
}
% scalac-hash v2.11.4 -deprecation ./sandbox/test.scala
% ./bin/dotc ./sandbox/test.scala
./sandbox/test.scala:7: error: type mismatch:
 found   : Base.this.Tree[Nothing, Option[Base$Tree$$S]](y)
 required: Base.this.Tree[Nothing, _ >: Option[Base$Tree$$S] <: Option[Base.this.N]]
    case y: Tree[_, _] => y
                          ^

I believe this is due to a missing substitution, as is done in scalac:

val TypeBounds(lo1, hi1) = tbounds.subst(tparams, argtypes)

@retronym
Copy link
Member

I would also be pretty cautious in propagating bounds to wildcards in non-pattern contexts. Paul tried that in the lead up to 2.11, but we ended up reverting in scala/scala#3509.

IIRC, there were two problems.

First, the propagation was conditional on the type parameter having a complete info to avoid cycles. This leads to compilation-order dependent instability of inferred types.

Second, inferring more specific types was not source compatible. Here's an example of that which uses the forSome syntax for the existential.

% cat sandbox/test.scala
trait ShapeLevel

object X {
  trait T[X <: ShapeLevel]
  def t: T[A] forSome { type A } = ???

  private[this] val g: T[_] = t
}

% scalac-hash v2.10.4 sandbox/test.scala

% scalac-hash v2.11.0-M8  sandbox/test.scala
sandbox/test.scala:7: error: type mismatch;
 found   : X.T[A] where type A
 required: X.T[_ <: ShapeLevel]
  private[this] val g: T[_] = t
                              ^
one error found

@odersky
Copy link
Contributor Author

odersky commented Nov 19, 2014

@retronym: "Here is an example that typechecks in scalac but fails to do so in dotc." I don't see why it should typecheck. The Tree bound is a lower bound but the required bound is an upper bound. Why would the x argument conform to the upper bound?

@odersky
Copy link
Contributor Author

odersky commented Nov 19, 2014

@retronym I think you are right about the dangers of &'ing with the bound eagerly. I'll abandon the current approach and open a new PR with a different scheme.

@odersky odersky closed this Nov 19, 2014
@retronym
Copy link
Member

I don't see why it should typecheck

@odersky This example is less cluttered.

class Tree[S, T <: S]

class Base {
  def g(x: Any): Tree[_, _ <: Int] = x match {
    case y: Tree[Int @unchecked, _] => y
  }
}
% scalac-hash v2.11.4 sandbox/test.scala

% ../dotty/bin/dotc -explaintypes sandbox/test.scala
sandbox/test.scala:5: error: type mismatch:
 found   : Tree[Int @unchecked, _ <: Tree$$S](y)
 required: Tree[_, _ <: Int & Tree$$S]
Constraint(
 uninstVars = ;
 constrained types = ;
 constraint = )
Subtype trace:
  ==> Tree[Int @unchecked, _ <: Tree$$S](y) <:< Tree[_, _ <: Int & Tree$$S] class dotty.tools.dotc.core.Types$TermRefWithFixedSym class dotty.tools.dotc.core.Types$PreHashedRefinedType
    ==>  <: Tree$$S <:<  <: Int & Tree$$S class dotty.tools.dotc.core.Types$CachedTypeBounds class dotty.tools.dotc.core.Types$CachedTypeBounds
      ==> Nothing <:< Nothing class dotty.tools.dotc.core.Types$CachedTypeRef class dotty.tools.dotc.core.Types$CachedTypeRef
      <== Nothing <:< Nothing class dotty.tools.dotc.core.Types$CachedTypeRef class dotty.tools.dotc.core.Types$CachedTypeRef = true
      ==> Tree$$S <:< Int & Tree$$S class dotty.tools.dotc.core.Types$CachedTypeRef class dotty.tools.dotc.core.Types$CachedAndType
        ==> Tree$$S <:< Int class dotty.tools.dotc.core.Types$CachedTypeRef class dotty.tools.dotc.core.Types$CachedTypeRef
          ==> Any <:< Int class dotty.tools.dotc.core.Types$CachedTypeRef class dotty.tools.dotc.core.Types$CachedTypeRef
          <== Any <:< Int class dotty.tools.dotc.core.Types$CachedTypeRef class dotty.tools.dotc.core.Types$CachedTypeRef = false
        <== Tree$$S <:< Int class dotty.tools.dotc.core.Types$CachedTypeRef class dotty.tools.dotc.core.Types$CachedTypeRef = false
      <== Tree$$S <:< Int & Tree$$S class dotty.tools.dotc.core.Types$CachedTypeRef class dotty.tools.dotc.core.Types$CachedAndType = false
    <==  <: Tree$$S <:<  <: Int & Tree$$S class dotty.tools.dotc.core.Types$CachedTypeBounds class dotty.tools.dotc.core.Types$CachedTypeBounds = false
  <== Tree[Int @unchecked, _ <: Tree$$S](y) <:< Tree[_, _ <: Int & Tree$$S] class dotty.tools.dotc.core.Types$TermRefWithFixedSym class dotty.tools.dotc.core.Types$PreHashedRefinedType = false
Implicit search failure summary:
  No implicit candidates were found that convert from Tree[Int @unchecked, _ <: Tree$$S](y) to Tree[_, _ <: Int & Tree$$S]
    case y: Tree[Int @unchecked, _] => y
                                       ^
one error found

This was referenced Nov 21, 2014
odersky added a commit to dotty-staging/dotty that referenced this pull request Nov 26, 2014
Previously, a double definition errorfor `T` was produced in a case like this:

     type T1 = C { T <: A }
     type T2 = T1 { T <: B }

This was caused by the way T1 was treated in the refinement class
that is used to typecheck the type. Desugaring of T2 with `refinedTypeToClass`
would give

     trait <refinement> extends T1 { type T <: B }

and `normalizeToClassRefs` would transform this to:

     trait <refinement> extends C { type T <: A; type T <: B }

Hence the double definition. The new scheme desugars the rhs of `T2` to:

     trait <refinement> extends C { this: T1 => type T <: B }

which avoids the problem.

Also, added tests that scala#232 (fix/boundsPropagation) indeed considers all refinements
together when comparing refined types.
odersky added a commit to dotty-staging/dotty that referenced this pull request Nov 26, 2014
Previously, a double definition errorfor `T` was produced in a case like this:

     type T1 = C { T <: A }
     type T2 = T1 { T <: B }

This was caused by the way T1 was treated in the refinement class
that is used to typecheck the type. Desugaring of T2 with `refinedTypeToClass`
would give

     trait <refinement> extends T1 { type T <: B }

and `normalizeToClassRefs` would transform this to:

     trait <refinement> extends C { type T <: A; type T <: B }

Hence the double definition. The new scheme desugars the rhs of `T2` to:

     trait <refinement> extends C { this: T1 => type T <: B }

which avoids the problem.

Also, added tests that scala#232 (fix/boundsPropagation) indeed considers all refinements
together when comparing refined types.
OlivierBlanvillain pushed a commit to OlivierBlanvillain/dotty that referenced this pull request Dec 8, 2016
OlivierBlanvillain pushed a commit to OlivierBlanvillain/dotty that referenced this pull request Dec 12, 2016
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.

None yet

3 participants