Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Unsealed Proof class #190

Closed
sankalpgambhir opened this issue Nov 22, 2023 · 1 comment · Fixed by #225
Closed

Unsealed Proof class #190

sankalpgambhir opened this issue Nov 22, 2023 · 1 comment · Fixed by #225
Assignees
@sankalpgambhir
Labels
bug Something isn't working

Comments

@sankalpgambhir
Copy link
Member

sankalpgambhir commented Nov 22, 2023 •
edited
Loading

New:

Issue below was "fixed" by unsealing the Proof class. This should be reversed ASAP. But, this relies on the core pattern matching problem bring fixed in dotty.

Old:

Unable to Upgrade Scala Version

Unable to upgrade the Scala 3 version in the LISA build. Doing so (to 3.3.1 or higher) results in the compiler crashing due to a stack overflow.

[error] java.lang.StackOverflowError
[error] dotty.tools.dotc.core.TypeComparer.isSubType(TypeComparer.scala:210)
[error] dotty.tools.dotc.core.TypeComparer.isSubType(TypeComparer.scala:218)
[error] dotty.tools.dotc.core.TypeComparer.topLevelSubType(TypeComparer.scala:128)
[error] dotty.tools.dotc.core.TypeComparer$.topLevelSubType(TypeComparer.scala:2940)
[error] dotty.tools.dotc.core.Types$Type.$less$colon$less(Types.scala:1036)
[error] dotty.tools.dotc.core.TypeOps$.instantiateToSubType(TypeOps.scala:921)
[error] dotty.tools.dotc.core.TypeOps$.refineUsingParent(TypeOps.scala:757)
[error] dotty.tools.dotc.transform.patmat.SpaceEngine$.$anonfun$13(Space.scala:650)
[error] scala.collection.immutable.List.map(List.scala:246)
[error] dotty.tools.dotc.transform.patmat.SpaceEngine$.rec$1(Space.scala:661)
[error] dotty.tools.dotc.transform.patmat.SpaceEngine$.decompose(Space.scala:669)
[error] dotty.tools.dotc.transform.patmat.SpaceEngine$Parts$.unapply(Space.scala:689)
[error] dotty.tools.dotc.transform.patmat.SpaceEngine$.rec$1(Space.scala:624)
[error] dotty.tools.dotc.transform.patmat.SpaceEngine$.decompose(Space.scala:669)
[error] dotty.tools.dotc.transform.patmat.SpaceEngine$Parts$.unapply(Space.scala:689)
[error] dotty.tools.dotc.transform.patmat.SpaceEngine$.rec$1(Space.scala:624)

and some repetition...

I ran the compilation, taking the config from logs from sbt, as a debug configuration on lamp-epfl/dotty with the recent version (3.4.0-RC1 on main) and managed to locate the crash to when the compiler is working on the file WithTheorems.scala in lisa-utils.

The crash has at least existed since before the recent major Types updates, among others, so I don't expect it's related to those.

Debug information at the call sites was not the most helpful, as it seems some information has been erased already. The function making repeated calls, minus at compiler/src/dotty/tools/dotc/transform/patmat/Space.scala:236 seems to compute the difference of two sum types, so it may have something to do with our use of those.

The types in question Edit: see below

In any case, more investigation is required to isolate the issue, and hopefully file a report on the dotty repo once we have a better idea.

Edit: with some more targeted printing of types, these are some of the types seen towards teh end of the overflow:

// with the internal show(_)

// a: 
     _: InnerProof.InnerProof | _: InnerProof.InnerProof
// b:
     _

// with _.toString()

// a:

Or(List(Typ(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class prooflib)),trait WithTheorems)),class Proof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),true), Typ(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class prooflib)),trait WithTheorems)),class BaseProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),class InnerProof),true)))

// b:
Typ(TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class prooflib)),trait WithTheorems)),class BaseProof),false)
@sankalpgambhir sankalpgambhir self-assigned this Nov 22, 2023
@sankalpgambhir sankalpgambhir added the bug Something isn't working label Nov 22, 2023
@sankalpgambhir sankalpgambhir mentioned this issue Nov 23, 2023
Closed
@sankalpgambhir
Copy link
Member Author

Filed a dotty issue: scala/scala3#19031

Seems to be a problem with the way we declare an InnerProof inside Proof as extending it. Pattern match exhaustion checking seems to fail. Minimized code for reproduction:

sealed trait A:
  class B extends A

def compute(a: A): Boolean =
  a match
    case b: A#B => true

@sankalpgambhir sankalpgambhir mentioned this issue Dec 6, 2023
Merged
@sankalpgambhir sankalpgambhir changed the title Unable to upgrade Scala version Unsealed Proof trait Dec 7, 2023
@sankalpgambhir sankalpgambhir changed the title Unsealed Proof trait Unsealed Proof class Dec 7, 2023
@sankalpgambhir sankalpgambhir mentioned this issue Jul 23, 2024
Merged
@sankalpgambhir sankalpgambhir linked a pull request Jul 23, 2024 that will close this issue
Reseal Proof trait, upgrade to Scala 3.4.2 #225
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@sankalpgambhir sankalpgambhir

Labels
bug Something isn't working
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Reseal Proof trait, upgrade to Scala 3.4.2 sankalpgambhir/lisa
1 participant
@sankalpgambhir