Handle bidirectional typebounds in AvoidMap

[dwijnand]

An example of a bidirectional TypeBounds is i15523: [A, B >: A], as an ordering: A <: B, as types and their bounds: A >: Nothing <: B and B >: A <: Any. It's not an fatal cycle, such as A <: B <: A. It's more like "My father is DJ, DJ's son is me" - if you then go ask who DJ's son's father is... you might never get an answer back.

Also, freeze the bounds.hi <:< bounds.lo check, so it doesn't instantiate any type variables: in the original (tests/pos/i15523.scala) it was causing A and B to be Nothing, which is wrong.

[SethTisue]

(...but also the bounds.hi frozen_<:< bounds.lo change...)

[odersky]

I'd prefer if @smarter could take a look when he has time

[dwijnand]

This now fixes 3 bugs. Can we merge it?

[smarter]

I can review it this week.

[dwijnand]

@smarter Sorry, I slightly misrepresented what I said. I said that I knew, loosely, how reproduce the problem with regular type variables. But what I had found is that if you change maximizeType to return the full bounds before instantiating the type variables, then you'll create the same bidirectional type bounds. IsFullyDefinedAccumulator is also set up to delay maximising type variables, at least the "difficult" ones, while minimising is done eagerly, so that avoids the problem (by being lossy).

[smarter]

Sorry, I'm not sure I understand what changes you have in mind that would lead to the same issue with non-gadt type variables. To me, it still seems like this is purely an issue with gadt handling. The whole point of having an ordering between type variables in OrderingConstraint is to avoid cyclic bounds, in fact if I print ctx.gadt.constraint.show in tests/pos/i15523.avoid.scala I see:

uninstantiated variables: A$1(param)1, B$1(param)1
 constrained types: [A$1(param)1 <: B$1(param)1, B$1(param)1]: Any
 bounds:
     A$1(param)1
     B$1(param)1
 ordering:
     A$1(param)1 <: B$1(param)1
 co-deps:
 contra-deps:

But then, we end up setting the bounds of GADT symbols using ctx.gadt.fullBounds, so A is upper-bounded by B and B is upper-bounded by A. Even if we fix this particular TypeMap to detect this, this could blow up in any TypeMap in the compiler (and possible other places like TypeComparer, although TypeComparer already has logic to deal with infinite subtype checks via pendingSubTypes).

We could change TypeMap itself to handle this, but to me the real issue is the way we set the info of GADT symbols. It should be morally equivalent to something the user could write if we don't want to end up with more puzzling bugs. For example I can write:

def foo =
  type A
  type B >: A
  val a: A = ???
  val b: B = a

or:

def foo =
  type B
  type A <: B
  val a: A = ???
  val b: B = a

and both will be handled gracefully by the compiler and compile as expected, because TypeComparer knows it needs to check the bounds of both abstract types involved to determine whether they're in a subtyping relationship (fun fact: this means it's possible for subtype checking to take an amount of time exponential in the number of abstract types in your program [Abel 2017, p.4]).

I think we could achieve something similar if we replaced fullBounds in https://github.com/lampepfl/dotty/blob/main/compiler/src/dotty/tools/dotc/typer/Typer.scala#L1767 by something like "fullBounds, but drop ordering constraints for type variables corresponding to symbols we already set the info of" (which might be achievable by instantiating a variable in ctx.gadt after it's been used to set the info of a symbol?), but I haven't tried it.

[dwijnand]

I think we could achieve something similar if we replaced fullBounds in main/compiler/src/dotty/tools/dotc/typer/Typer.scala#L1767 by something like "fullBounds, but drop ordering constraints for type variables corresponding to symbols we already set the info of" (which might be achievable by instantiating a variable in ctx.gadt after it's been used to set the info of a symbol?), but I haven't tried it.

I wasn't able to find a solution based on that. I also know that removing GADT information about symbols changes type comparing, because we trust GADT info, but not abstract symbol info, because we can't distinguish it from unsound, user-defined, info.

But I found a solution based on using and tweaking checkNonCyclic. WDYT?

[dwijnand]

I wasn't able to find a solution based on that.

Nevermind, found a solution! (finally)