Avoid bidirectional GADT typebounds from fullBounds

[dwijnand]

No description provided.

[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)

[smarter]

Very nice fix! Thanks a lot for doing all the hard work on this!

[smarter]

Can we use tp.symbol.isPatternBound instead of relying on the name kind?

[smarter]

Also, would checking self =:= tp.info.hiBound be enough for all our test cases? That would remove the need for isExactlyAny which I'm a bit wary of (what if the symbols involved have another common upper-bound like AnyRef?)

[smarter]

hmm looks like we still need to update the comment after changing <:< to =:=