Fix logic when comparing var/def bindings with val refinements

compiler/src/dotty/tools/dotc/core/TypeComparer.scala

@@ -1971,7 +1971,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
       def tp1IsSingleton: Boolean = tp1.isInstanceOf[SingletonType]
 
       // A relaxed version of isSubType, which compares method types
-      // under the standard arrow rule which is contravarient in the parameter types,
+      // under the standard arrow rule which is contravariant in the parameter types,
       // but under the condition that signatures might have to match (see sigsOK)
       // This relaxed version is needed to correctly compare dependent function types.
       // See pos/i12211.scala.
@@ -1988,10 +1988,21 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
           case _ => inFrozenGadtIf(tp1IsSingleton) { isSubType(info1, info2) }
 
       def qualifies(m: SingleDenotation): Boolean =
-        val info1 = m.info.widenExpr
-        isSubInfo(info1, tp2.refinedInfo.widenExpr, m.symbol.info.orElse(info1))
+        val info2 = tp2.refinedInfo
+        val isExpr2 = info2.isInstanceOf[ExprType]
+        val info1 = m.info match
+          case info1: ValueType if isExpr2 || m.symbol.is(Mutable) =>
+            // OK: { val x: T } <: { def x: T }
+            // OK: { var x: T } <: { def x: T }
+            // NO: { var x: T } <: { val x: T }
+            ExprType(info1)
+          case info1 @ MethodType(Nil) if isExpr2 && m.symbol.is(JavaDefined) =>
+            // OK{ { def x(): T } <: { def x: T} // if x is Java defined
+            ExprType(info1.resType)
+          case info1 => info1
+        isSubInfo(info1, info2, m.symbol.info.orElse(info1))
         || matchAbstractTypeMember(m.info)
-        || (tp1.isStable && isSubType(TermRef(tp1, m.symbol), tp2.refinedInfo))
+        || (tp1.isStable && m.symbol.isStableMember && isSubType(TermRef(tp1, m.symbol), tp2.refinedInfo))
 
       tp1.member(name) match // inlined hasAltWith for performance
         case mbr: SingleDenotation => qualifies(mbr)

tests/neg/i13703.check

@@ -3,3 +3,10 @@
   |             ^^^^^^^^^^
   |             refinement cannot be a mutable var.
   |             You can use an explicit getter i and setter i_= instead
+-- [E007] Type Mismatch Error: tests/neg/i13703.scala:5:78 -------------------------------------------------------------
+5 |val f2: Foo { val i: Int; def i_=(x: Int): Unit } = new Foo { var i: Int = 0 } // error
+  |                                                                              ^
+  |                                                                  Found:    Object with Foo {...}
+  |                                                                  Required: Foo{val i: Int; def i_=(x: Int): Unit}
+  |
+  | longer explanation available when compiling with `-explain`

tests/neg/i13703.scala

@@ -2,4 +2,6 @@ trait Foo extends reflect.Selectable
 
 val f: Foo { var i: Int } = new Foo { var i: Int = 0 } // error
 
-val f2: Foo { val i: Int; def i_=(x: Int): Unit } = new Foo { var i: Int = 0 } // OK
+val f2: Foo { val i: Int; def i_=(x: Int): Unit } = new Foo { var i: Int = 0 } // error
+
+val f3: Foo { def i: Int; def i_=(x: Int): Unit } = new Foo { var i: Int = 0 } // OK

tests/neg/i18047.scala

@@ -0,0 +1,15 @@
+def foo(x: Any { def foo: Int }): Any { val foo: Int } = x // error
+def foo1(x: Any { val foo: Int }): Any { def foo: Int } = x // ok
+def foo2(x: Any { val foo: Int }): Any { val foo: Int } = x // ok
+def foo3(x: Any { def foo: Int }): Any { def foo: Int } = x // ok
+
+class Foo:
+  val foo: Int = 1
+class Foo1:
+  def foo: Int = 1
+class Foo2:
+  var foo: Int = 1
+
+def foo4(x: Foo): Any { val foo: Int } = x // ok
+def foo4(x: Foo1): Any { val foo: Int } = x // error
+def foo4(x: Foo2): Any { val foo: Int } = x // error

tests/neg/i4496b.scala

@@ -10,7 +10,7 @@ object TestStructuralVar {
     type T = {val a: Int; def a_=(x: Int): Unit}
     def upcast1(v: Foo1): T = v // error
     def upcast2(v: Foo2): T = v // error
-    def upcast3(v: Foo3): T = v
+    def upcast3(v: Foo3): T = v // error
     def verify(v: T) = ()
     def test(): Unit = {
       verify(upcast1(new Foo1 { val a = 10 }))

tests/run/i4496a.scala

@@ -5,7 +5,7 @@ class Foo3 { var a: Int = 10 }
 object Test {
   def main(args: Array[String]): Unit = {
     assert((new Foo1 : {val a: Int}).a == 10)
-    assert((new Foo2 : {val a: Int}).a == 10)
-    assert((new Foo3 : {val a: Int}).a == 10)
+    assert((new Foo2 : {def a: Int}).a == 10)
+    assert((new Foo3 : {def a: Int}).a == 10)
   }
 }

tests/run/i4496b.scala

@@ -18,9 +18,10 @@ object Test {
 
     // Consider one module upcasting all these instances to T. These casts are clearly well-typed.
     type T = {val a: Int}
+    type T2 = {def a: Int}
     def upcast1(v: Foo1): T = v
-    def upcast2(v: Foo2): T = v
-    def upcast3(v: Foo3): T = v
+    def upcast2(v: Foo2): T2 = v
+    def upcast3(v: Foo3): T2 = v
 
     // These accesses are also clearly well-typed
     def consume(v: T) = v.a
@@ -31,24 +32,32 @@ object Test {
       assert(v.a == 10)
     }
 
+    def consume2(v: T2) = v.a
+    inline def consumeInl2(v: T2) = v.a
+    def verify2(v: T2) = {
+      assert(consume2(v) == 10)
+      assert(consumeInl2(v) == 10)
+      assert(v.a == 10)
+    }
+
     def test(): Unit = {
       // These calls are also clearly well-typed, hence can't be rejected.
       verify(upcast1(new Foo1 { val a = 10 }))
-      verify(upcast2(new Foo2 { val a = 10 }))
-      verify(upcast3(new Foo3 { var a = 10 }))
+      verify2(upcast2(new Foo2 { val a = 10 }))
+      verify2(upcast3(new Foo3 { var a = 10 }))
       // Ditto, so we must override access control to the class.
       verify(upcast1(new FooBar1))
-      verify(upcast2(new FooBar2))
-      verify(upcast3(new FooBar3))
+      verify2(upcast2(new FooBar2))
+      verify2(upcast3(new FooBar3))
 
       // Other testcases
       verify(new {val a = 10} : T)
-      verify(new {var a = 10} : T)
-      verify(new {def a = 10} : T)
+      verify2(new {var a = 10} : T2)
+      verify2(new {def a = 10} : T2)
 
       verify(new Bar1 : T)
-      verify(new Bar2 : T)
-      verify(new Bar3 : T)
+      verify2(new Bar2 : T2)
+      verify2(new Bar3 : T2)
     }
   }
 
@@ -85,7 +94,7 @@ object Test {
   }
 
   object TestStructuralVar {
-    type T = {val a: Int; def a_=(x: Int): Unit}
+    type T = {def a: Int; def a_=(x: Int): Unit}
     def upcast3(v: Foo3): T = v
     def consume(v: T) = v.a
     inline def consumeInl(v: T) = v.a