Infinite loop in subtyping check

[samuelgruetter]

While looking for counterexamples to narrowing in DOT, I found this example:

object subtypcycle {
  trait Y {
    type A <: { type T >: B }
    type B >: { type T >: A }
  }

  val y: Y = ???
  val a: y.A = ???
  val b: y.B = a
}

Which sends dotty into an infinite loop checking if y.A <: y.B.

scalac has the same problem, see SI-9056.

[odersky]

Good example! We do know that subtyping proof search can lead to infinite
expansions. See the paper by Kennedy and Pierce at a previous FOOL.

http://research.microsoft.com/apps/pubs/default.aspx?id=64041

But when we deal with just classes this can be handled by making all
expansions of the class graph finitary (that's an extra condition on
inheritance which one can impose) and then doing a cycle detection during
subtyping.

If I remember correctly, in essence the condition excluded deep F-bounds of
the form

class C[T <: D[D[T]]]

It strikes me that your example can be also seen as a deep F-bound. Both A
and B depend on themselves but indirectly so.

So, maybe we need a finitary condition for abstract types, similar to the
one for classes?

• Martin

On Sun, Dec 21, 2014 at 11:43 PM, Samuel Gruetter [email protected]
wrote:

While looking for counterexamples to narrowing in DOT, I found this
example:

object subtypcycle {
trait Y {
type A <: { type T >: B }
type B >: { type T >: A }
}

val y: Y = ???
val a: y.A = ???
val b: y.B = a
}

Which sends dotty into an infinite loop checking if y.A <: y.B.

scalac has the same problem, see SI-9056
https://issues.scala-lang.org/browse/SI-9056.

—
Reply to this email directly or view it on GitHub
#318.

Martin Odersky
EPFL

[samuelgruetter]

This is a very interesting paper, especially section 5.2. Btw I found the commit where you implemented this for scalac: scala/scala@152563b

But now that type parameters are encoded as abstract type members, we should adapt this "finitary condition" to abstract types, as you suggest.

Here's my attempt to adapt the definitions:

A set S of types is closed under bounds and decomposition (or bd-closed for short) if

a) For all p.L in S, its lower and upper bound are in S as well.
b) For all { z => Ds } in S, all types which are contained in Ds are in S as well.

Note that the same way as "closed under inheritance and decomposition" in the paper is with respect to a class table, "bd-closed" is with respect to a context G (because otherwise we don't know what the bounds of p.L are).

The bd-closure of a set S of types, written as cl(S), is the smallest bd-closed superset of S.

A context G is finitary if any finite set of types which are well-formed in G has a finite bd-closure.

With these definitions, we can claim that a derivation of T <: U only involves types in cl({T, U}).

Then we would need to adapt their procedure which checks if a class table is finitary to get a procedure which checks if a context is finitary. The subtyping algorithm to decide G |- T <: U would first run this procedure on G, and if it succeeds, do the subtype check, and abort if a previously seen subgoal is encountered again (cycle detection). And since the set of types which can possibly be involved in the proof of G |- T <: U is cl({T, U}), which is finite, the set of possible subgoals is finite, so the algorithm would always terminate.

That sounds like a nice plan, except that the condition (b) looks a bit fishy to me: If the types in Ds use the self reference z, we put types into S which are not well-formed in the original context G...

If I remember correctly, in essence the condition excluded deep F-bounds of the form

class C[T <: D[D[T]]]

Unfortunately, the types used in the paper don't allow bounds for type parameters, which makes it a bit harder to adapt to DOT. You probably meant that in essence, the condition excludes class C[T] extends Something[C[C[T]]] ?

It strikes me that your example can be also seen as a deep F-bound.

So you mean by "inlining" the definitions of A and B?

trait Y {
  type A <: { type T >: { type T >: A } }
  type B >: { type T >: { type T >: B } }
}

If we do this, both scalac and dotty detect an "illegal cyclic reference".

[newca12]

FYI this is not (or not anymore) an infinite loop
After a certain amount of time (< 1min) dotc terminate with a Type Mismatch Error

-- [E007] Type Mismatch Error: <console> -----------------------------
9 |  val b: y.B = a
  |               ^
  |               found:    subtypcycle.y.A(subtypcycle.a)
  |               required: subtypcycle.y.B
  |

[newca12]

The fix for #2397 in PR #2402 turn #318 in an infinite loop again.
This example found by @samuelgruetter is referenced as a pending test : https://github.com/lampepfl/dotty/blob/master/tests/pending/pos/subtypcycle.scala

[felixmulder]

Hi @newca12 - thanks for reporting and pointing us to the pending file. We'll try to get to this during the week!

Cheers,
Felix

[nicolasstucki]

The infinite loop is still there. (pending/pos/subtypcycle.scala)

[newca12]

Since dotty 0.6.0-RC1, this now fail immediately with a stack overflow.

Stack trace

Exception in thread "main" java.lang.StackOverflowError at java.util.Arrays.copyOfRange(Arrays.java:3484) at java.util.Arrays.copyOfRange(Arrays.java:3441) at java.lang.invoke.MethodType.insertParameterTypes(MethodType.java:396) at java.lang.invoke.MemberName.getInvocationType(MemberName.java:168) at java.lang.invoke.DirectMethodHandle.preparedLambdaForm(DirectMethodHandle.java:167) at java.lang.invoke.DirectMethodHandle.make(DirectMethodHandle.java:81) at java.lang.invoke.MethodHandles$Lookup.getDirectMethodCommon(MethodHandles.java:1660) at java.lang.invoke.MethodHandles$Lookup.getDirectMethodNoSecurityManager(MethodHandles.java:1617) at java.lang.invoke.MethodHandles$Lookup.getDirectMethodForConstant(MethodHandles.java:1802) at java.lang.invoke.MethodHandles$Lookup.linkMethodHandleConstant(MethodHandles.java:1751) at java.lang.invoke.MethodHandleNatives.linkMethodHandleConstant(MethodHandleNatives.java:477) at dotty.tools.dotc.core.Types$Type.findMember(Types.scala:661) at dotty.tools.dotc.core.Types$Type.memberExcluding(Types.scala:497) at dotty.tools.dotc.core.Types$Type.nonPrivateMember(Types.scala:487) at dotty.tools.dotc.core.Types$NamedType.memberDenot(Types.scala:1742) at dotty.tools.dotc.core.Types$NamedType.reload$1(Types.scala:1988) at dotty.tools.dotc.core.Types$NamedType.withPrefix(Types.scala:2000) at dotty.tools.dotc.core.Types$NamedType.derivedSelect(Types.scala:1956) at dotty.tools.dotc.core.Types$TypeMap.derivedSelect(Types.scala:3755) at dotty.tools.dotc.core.Types$ApproximatingTypeMap.derivedSelect(Types.scala:4022) at dotty.tools.dotc.core.TypeOps$AsSeenFromMap.op1$1(TypeOps.scala:61) at dotty.tools.dotc.core.TypeOps$AsSeenFromMap.apply(TypeOps.scala:54) at dotty.tools.dotc.core.Types$TypeMap.mapOver(Types.scala:3829) at dotty.tools.dotc.core.TypeOps$AsSeenFromMap.op1$1(TypeOps.scala:67) at dotty.tools.dotc.core.TypeOps$AsSeenFromMap.apply(TypeOps.scala:54) at dotty.tools.dotc.core.Types$TypeMap.mapOver(Types.scala:3822) at dotty.tools.dotc.core.TypeOps$AsSeenFromMap.op1$1(TypeOps.scala:67) at dotty.tools.dotc.core.TypeOps$AsSeenFromMap.apply(TypeOps.scala:54) at dotty.tools.dotc.core.Types$TypeMap.mapOver(Types.scala:3831) at dotty.tools.dotc.core.TypeOps$AsSeenFromMap.op1$1(TypeOps.scala:67) at dotty.tools.dotc.core.TypeOps$AsSeenFromMap.apply(TypeOps.scala:54) at dotty.tools.dotc.core.TypeOps.asSeenFrom(TypeOps.scala:28) at dotty.tools.dotc.core.Types$Type.asSeenFrom(Types.scala:760) at dotty.tools.dotc.core.Denotations$SingleDenotation.computeAsSeenFrom(Denotations.scala:1073) at dotty.tools.dotc.core.Denotations$SingleDenotation.computeAsSeenFrom(Denotations.scala:1066) at dotty.tools.dotc.core.Denotations$PreDenotation.asSeenFrom(Denotations.scala:131) at dotty.tools.dotc.core.SymDenotations$ClassDenotation.findMember(SymDenotations.scala:1599) at dotty.tools.dotc.core.Types$Type.go$1(Types.scala:514) at dotty.tools.dotc.core.Types$Type.findMember(Types.scala:658) at dotty.tools.dotc.core.Types$Type.memberExcluding(Types.scala:497) at dotty.tools.dotc.core.Types$Type.nonPrivateMember(Types.scala:487) at dotty.tools.dotc.core.Types$NamedType.memberDenot(Types.scala:1742) at dotty.tools.dotc.core.Types$NamedType.reload$1(Types.scala:1988) at dotty.tools.dotc.core.Types$NamedType.withPrefix(Types.scala:2000) at dotty.tools.dotc.core.Types$NamedType.derivedSelect(Types.scala:1956) at dotty.tools.dotc.core.Types$TypeMap.derivedSelect(Types.scala:3755) at dotty.tools.dotc.core.Types$ApproximatingTypeMap.derivedSelect(Types.scala:4022) ...

[Blaisorblade]

#4385 was meant to cover this too, so closing. I added stat:revisit because the behavior is still not ideal, but making progress here would require fundamental research.