Skip to content

Commit 68cec5b

Browse files
committed
Fix comparison of dependent function types
Dependent function types are expressed as refinements over regular function types. These refinements need to be compared with the standard arrow rule for function subtyping. But comparison of method refinements so far demanded equal parameter types. The solution is tricky since refined types lead to selections via reflection still cannot tolerate differing parameter types since reflexive method dispatch uses precise parameter types. That's why we apply standard arrow rule only for refinements where the refined method exists in the underlying class. Fixes #12211
1 parent aadc10f commit 68cec5b

File tree

3 files changed

+59
-6
lines changed

3 files changed

+59
-6
lines changed

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

Lines changed: 29 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1698,8 +1698,6 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
16981698
*/
16991699
protected def hasMatchingMember(name: Name, tp1: Type, tp2: RefinedType): Boolean =
17001700
trace(i"hasMatchingMember($tp1 . $name :? ${tp2.refinedInfo}), mbr: ${tp1.member(name).info}", subtyping) {
1701-
val rinfo2 = tp2.refinedInfo
1702-
17031701
// If the member is an abstract type and the prefix is a path, compare the member itself
17041702
// instead of its bounds. This case is needed situations like:
17051703
//
@@ -1725,8 +1723,28 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
17251723
case _ => false
17261724
}
17271725

1726+
// A relaxed version of isSubType, which compares method types
1727+
// under the standard arrow rule which is contravarient in the parameter types,
1728+
// but only if `tp2.refinedName` is also defined in the underlying class of tp2.
1729+
// The reason for the "but only" retriction is that if `tp2.refinedName`
1730+
// is not otherwise defined, we will have to resort to reflection to invoke
1731+
// the member. And reflection needs to know exact parameter types. The relaxation is
1732+
// needed to correctly compare dependent function types.
1733+
// See {pos,neg}/i12211.scala as test cases.
1734+
def isSubInfo(info1: Type, info2: Type): Boolean =
1735+
info2 match
1736+
case info2: MethodType
1737+
if tp2.underlyingClassRef(refinementOK = true).member(tp2.refinedName).exists =>
1738+
info1 match
1739+
case info1: MethodType =>
1740+
matchingMethodParams(info1, info2, precise = false)
1741+
&& isSubInfo(info1.resultType, info2.resultType.subst(info2, info1))
1742+
case _ => isSubType(info1, info2)
1743+
case _ => isSubType(info1, info2)
1744+
17281745
def qualifies(m: SingleDenotation) =
1729-
isSubType(m.info.widenExpr, rinfo2.widenExpr) || matchAbstractTypeMember(m.info)
1746+
isSubInfo(m.info.widenExpr, tp2.refinedInfo.widenExpr)
1747+
|| matchAbstractTypeMember(m.info)
17301748

17311749
tp1.member(name) match { // inlined hasAltWith for performance
17321750
case mbr: SingleDenotation => qualifies(mbr)
@@ -1841,15 +1859,20 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
18411859
}
18421860

18431861
/** Do the parameter types of `tp1` and `tp2` match in a way that allows `tp1`
1844-
* to override `tp2` ? This is the case if they're pairwise `=:=`.
1862+
* to override `tp2` ? Two modes: precise or not.
1863+
* If `precise` is set (which is the default) this is the case if they're pairwise `=:=`.
1864+
* Otherwise parameters in `tp2` must be subtypes of corresponding parameters in `tp1`.
18451865
*/
1846-
def matchingMethodParams(tp1: MethodType, tp2: MethodType): Boolean = {
1866+
def matchingMethodParams(tp1: MethodType, tp2: MethodType, precise: Boolean = true): Boolean = {
18471867
def loop(formals1: List[Type], formals2: List[Type]): Boolean = formals1 match {
18481868
case formal1 :: rest1 =>
18491869
formals2 match {
18501870
case formal2 :: rest2 =>
18511871
val formal2a = if (tp2.isParamDependent) formal2.subst(tp2, tp1) else formal2
1852-
isSameTypeWhenFrozen(formal1, formal2a) && loop(rest1, rest2)
1872+
val paramsMatch =
1873+
if precise then isSameTypeWhenFrozen(formal1, formal2a)
1874+
else isSubTypeWhenFrozen(formal2a, formal1)
1875+
paramsMatch && loop(rest1, rest2)
18531876
case nil =>
18541877
false
18551878
}

tests/neg/i12211.scala

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
2+
import reflect.Selectable.*
3+
4+
val x: { def f(x: Any): String } = new { def f(x: Any) = x.toString }
5+
val y: { def f(x: String): String } = x // error: type mismatch (no arrow rule since `f` is not defined in parent)
6+
7+
@main def Test =
8+
println(y.f("abc"))
9+

tests/pos/i12211.scala

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
2+
def fst0[A, B[_]](a: A)(b: B[a.type]): a.type = a
3+
4+
def fst[A, B[_]]: (a: A) => (b: B[a.type]) => a.type =
5+
(a: A) => (b: B[a.type]) => a
6+
7+
def snd[A, B[_]]: (a: A) => () => (b: B[a.type]) => b.type =
8+
(a: A) => () => (b: B[a.type]) => b
9+
10+
def fst1[A, B[_]]: (a: A) => (b: B[a.type]) => a.type = fst0
11+
12+
def test1[A, B[_]]: (a: A) => () => (b: B[a.type]) => Any =
13+
snd[A, B]
14+
15+
def test2[A, B[_]]: (a: A) => (b: B[a.type]) => A = fst[A, B]
16+
17+
class AA
18+
class BB[T]
19+
20+
def test3: (a: AA) => (b: BB[a.type]) => BB[?] =
21+
(a: AA) => (b: BB[a.type]) => b

0 commit comments

Comments
 (0)