Break circularity in TypeBounds with LazyRef wraps

[dwijnand]

No description provided.

[dwijnand]

@smarter do you have any better ideas on how to avoid the circular problem here?

[smarter]

What are we recursing on here that leads to a cycle exactly?

[dwijnand]

enum Foo[+H[_]]:
  case Bar[F[_]](f: Foo[F]) extends Foo[F]
  case Baz()

  def test: Foo[H] = this match
    case Bar(Bar(f)) => Bar(f)
    case _           => this

It's a case of TypeBounds with circular infos:

avoid F$1 #18787  >: F$2 <: F
avoid F$2 #18891  <: F$1
avoid F$1 #18787  >: F$2 <: F
avoid F$2 #18891  <: F$1

[smarter]

Seems weird. I don't even see how we can construct TypeBounds with circular info, I assume there are actually type variables in the info somewhere? (print without using .show/i"..." to see the types that are actually involved)

[smarter]

If type variables turn out to be involved, this is likely caused by the handling of TypeVar in avoid (https://github.com/lampepfl/dotty/blob/9e14f5fba1acd993b8fcd99e4afe64fc17d37d30/compiler/src/dotty/tools/dotc/core/TypeOps.scala#L508-L512) which maps a type variable to one of its bound without actually instantiating the type variable which I always found weird.

[dwijnand]

Nope, no variables, just type refs:

• F$1 >: F$2 <: H is TypeRef(NoPrefix,type F$1) with bounds TypeRef(NoPrefix,type F$2) and TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class <empty>)),class Foo)),type H)), and
• F$2 <: F$1 is TypeRef(NoPrefix,type F$2) with upperbound TypeRef(NoPrefix,type F$1))

[smarter]

Sounds like a problem with the gadt logic that generates these types then?

[dwijnand]

Oh yeah? Why, what should they be instead? I thought the types seemed legitimate, just tricky to traverse.

[smarter]

I don't have a good enough grasp of the gadt logic to say, but as far as I can tell no code outside of it can produce type bounds like that so it's natural that the compiler isn't setup to deal with them (and there might be many more type maps where this would be a problem):

scala> def foo[A >: B, B <: A] = {}
-- Error:
1 |def foo[A >: B, B <: A] = {}
  |        ^
  |illegal cyclic type reference: lower bound B of type A refers back to the type itself

scala> class X { type A >: B; type B <: A }
-- Error:
1 |class X { type A >: B; type B <: A }
  |               ^
  |illegal cyclic type reference: lower bound X.this.B of type A refers back to the type itself

[odersky]

There should be no circular info in type bounds. Circular upper bounds are allowed (i.e. that's what an F-bound is), but internally they must be protected with a LazyRef. So we should find out how and where these illegal bounds are generated.

[smarter]

This is likely still not the correct place to fix this, constraints shouldn't be cyclic (although the assert for this is disabled by default for performance: https://github.com/lampepfl/dotty/blob/3c8200671995ea75b97b493081cc4e51109cfd04/compiler/src/dotty/tools/dotc/config/Config.scala#L21-L24), it's possible the logic in GadtConstraint.scala violates this.

[dwijnand]

Thanks, I'll check.

[dwijnand]

Enabling doesn't seem to trigger anything. Either it fails without my "half answer" workaround or it passes with - no check error. Are we sure it's a cycle in the constraints? Need to investigate more.

[dwijnand]

So inference first creates the type refs while typing the patterns (in maximizeType via typedUnApply) as F$1 <: F and F$2 <: F$1. Just a little later runs over the patterns again in indexPattern where it calls fullBounds leading to F$1(param)1 >: F$2 <: F and F$2(param)1 <: F$1.

So is it circular constraints? 🤔

[smarter]

Yeah, either gadt.fullBounds should not produce cycles like this, or we shouldn't use it here, wdyt @abgruszecki ?

[dwijnand]

The way I see it, fullLowerBound aren't wrong in their answers. But put together they lead to a mutual reference. So fixing this in fullBounds by inspecting the results seems reasonable to me.

Hopefully I've fixed the test suite now.

[smarter]

But can this be triggered with non-gadt constraints?

[dwijnand]

I don't know. 🤷🏼‍♂️ But GadtConstraint redefines its fullLowerBound and fullUpperBound so possibly not?

[smarter]

I don't think this should get in until we actually understand if this is specific to gadt and if it's working around a bug or the correct thing to do.

[dwijnand]

I'm concerned that those answers might not come readily. Would you be happy to get the fix in even if we don't have those answers in, let's say, a month? I don't know the answers to your questions, I'm sorry. But it's peeving to put effort into fixing a user-reported bug to then the PR blocked like so.

[smarter]

I'm not comfortable merging code no one understand, and I don't have the time to try to understand it myself, this is why I asked for Alex's input but someone else could fill in too.

[dwijnand]

I'm now not happy with this fix either.