Quickly fix HKT GADT unsoundness issue #9138
Conversation
Check that the result of GADT approximation is actually a subtype of what we're approximating.
|
@smarter so it turns out that the issue was with GADT member healing! Can you take a look at the code? The relevant test passes on my local machine. I'm just surprised that |
TreeChecker should check that but doesn't, I have a branch which fixes that but it needs more work because it revealed situations where this isn't true currently. |
| // otherwise fail with the error that would have been reported without the GADT recovery | ||
| err.typeMismatch(tree, pt, failure) | ||
| val approximated = Inferencing.approximateGADT(wtp)(using nestedCtx) | ||
| if (tree.tpe <:< approximated) { |
There was a problem hiding this comment.
Shouldn't that check be done in the nestedCtx?
There was a problem hiding this comment.
That's sadly not the part that's making it explode. Not even making the check frozen and doing it in nestedCtx helps. I have no idea why, seems that we will need to take a more scorched-earth type of approach.
Check that the result of GADT approximation is actually a subtype of what we're approximating.
Fixes #9044.