WIP: Skip subtype tests for recursive bounds involving match types

[milessabin]

This is a WIP fix for #5535 ... it's almost certainly wrong, but it makes the problem go away without breaking anything else, so it's in the right general area. I'd appreciate a steer ...

Nb. the test is in the pickling blacklist because of #5680.

[odersky]

The subtype test is there to guarantee that the constraint set is satisfiable. If you omit it you create very likely a soundness bug. Typically no tests fail when a soundness hole is created, but that does not mean it's OK to do so 😉

[milessabin]

That's true of course, however the bounds are checked subsequently, after inference, so ill-typed instantiations are rejected.

I was really looking for some insight into what's going on here: the issue appears to be that the subtype check due to the recursive bound is causing reduction of the match type to loop.

[odersky]

That's true of course, however the bounds are checked subsequently, after inference, so ill-typed instantiations are rejected.

Unfortunately, that's not a given. An unsatisfiable constraint can prove anything, and it is a stretch to claim that we can detect any inconsistencies later. The only reliable way I can see that would do that would be to do a full typecheck later, but then we would run into the same problem with inconsistent bounds.

My take on it is: We should try to de-emphasize recursive bounds. I would love to find a way to outlaw them completely, and only allow to express these relationships with implicit evidence. Scala went further than every other language I know of to support complex recursive bounds. I believe we might already have gone too far.

[milessabin]

Leaving the general point about recursive bounds to one side for the moment, it seems fairly clear that it's dangerous for a match type to participate in solving type variables if some or all of it's arguments are themselves in the process of being solved and might still be refined. Using implicit evidence as an alternative to a bound recognizes that by postponing the check until all type variables have been solved.

If prohibiting such problematic match types is the way to go then we still have to check for them in bounds and report that explicitly (ie. something along the lines of "match type with unsolved type variable arguments unsupported in bounds, use implicit evidence instead"), otherwise users will see the kind of unfriendly errors reported in #5535.

But is that too pessimistic an option? It seems that we have a distinction between constraints which can participate in solving type variables during inference and constraints which can only be checked after inference has been completed. There's already logic to check bounds post-inference (which is what picks up the errors in the neg tests I've added to this PR), so perhaps a viable strategy would be to detect bounds which should be checked only (we would need to do this work anyway to produce a comprehensible error) and exclude them from solving?

On recursive bounds in general, I think that train left the station long ago ... there's a huge amount of Scala 2 code which depends on it.

[odersky]

After many bad surprises I have become a lot more conservative with soundness. Match types alone are already a formidable challenge. I don't dare to even start thinking about possible interactions with F-bounds. So, for the moment I believe exluding match types from recursive bounds is a reasonable option. You are right that simply issuing cyclic reference errors is not friendly.

[Blaisorblade]

(Assigned to @milessabin, as a quick guess, so we don't have unassigned PRs).

[Blaisorblade]

Is this PR still alive @milessabin, or should it be closed/converted to draft?

[milessabin]

No, I think it's long dead.