EtaExpansion object extractor seems to record constraints

[mario-bucev]

Hello,
I have a question regarding the EtaExpansion object extractor, and more
specifically, its weakerBounds private method (from line 45):
https://github.com/lampepfl/dotty/blob/0a9b48fba3a4e120ae4cd123b1ac1f9311d10182/compiler/src/dotty/tools/dotc/core/TypeApplications.scala#L27-L68

At line 56, <:< is employed which performs subtyping check with constraints recording whenever necessary (if I understand correctly).
Is this the expected behavior? Shouldn't we instead perform a subtyping check in a frozen context?

For example, in RefinedPrinter#toText, the extractor is used at line 229:
https://github.com/lampepfl/dotty/blob/0a9b48fba3a4e120ae4cd123b1ac1f9311d10182/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala#L244-L247

This can cause constraints to be recorded while printing a type, which is a bit surprising.

Thank you

[odersky]

Shouldn't we instead perform a subtyping check in a frozen context?

It looks like an error to me. Can you try to change it and make a PR if it succeeds?

[mario-bucev]

Corresponding PR: #13229