Deep subtype failure when comparing types involving recursive references #14713
Comments
Linyxus
added
itype:bug
stat:needs triage
Why not? This looks exactly like the kind of recursive program that can trigger a deep subtype assertion. Note that there's nothing wrong with deep subtypes, the -Yno-deep-subtypes is just a plausibility check that they don't pop up where we do not expect them. |
odersky
added
stat:needs info
and removed
itype:bug
stat:needs triage
|
Here's the bottom recursions of the deep subtype check (to be read from bottom to top) To classify this as a bug we'd have to argue that some of these steps should not be taken. |
|
I found that I wrongly understood the meaning of deep subtype before. I thought that if a deep subtype failure happens then there would be infinite loops in type comparison. But after taking a deeper look into the code I figure out that it checks whether the recursion level exceeds a threshold (if so, either start monitoring or issue a failure), which may be a sign of infinite loops, but does not necessarily mean something bad happens. Back to the issue here. I found that after turning off the Sorry for the misunderstanding and thanks a lot for checking this! |
|
No problem! So i think we can close the issue now. |
Uh oh!
There was an error while loading. Please reload this page.
Compiler version
3.1.2-RC2Minimized code
The following code snippet will trigger the deep subtype assertion failure when
-Yno-deep-subtypesis turned on.I encountered this issue when I was trying to merge the path-dependent GADT support (previous PRs #13364, #13475) into the latest main branch. I found that my changes break the pos test i2941 by triggering a deep subtype failure. Then I managed to reproduce the problem without path-dependent GADTs.
In the above snippet, we are trying to narrow the lower bound of the type parameter
AtoFooBase { type This <: foo.This }by destructing the subtyping evidencee. During this, the GADT solver will try to check whether the new bounds are good (the subtyping relation between lower and upper boundsFooBase { type This <: foo.This } <: FooBase { type This <: foo.This }should hold), which is true by reflexivity but triggers the deep subtyping problem.And I found that this problem may not be directly related to GADT reasoning. The following snippet causes deep subtyping failure too without involving GADTs.
Output
Expectation
The code snippet should not trigger the deep subtype assertion.
The text was updated successfully, but these errors were encountered: