Compiler hangs on infinite match type reduction

[odersky]

class P[X, Y]

type Swap[X] = X match
  case P[x, y] => Swap[P[y, x]]

val z: P[String, Int] = ??? : Swap[P[Int, String]]

The compiler seems to hang when compiling the last line.

Expectation

The compiler should either report a stack overflow or detect the diverging expansion statically. My preference would be to try static divergence detection first. @milessabin implemented state of the art techniques for detecting divergent implicit searches - it seems that these techniques are transferable.

[OlivierBlanvillain]

@milessabin Do you know in which direction the implicit divergence checks are conservative? Either way, I think we would need to back them up with an upper bound on the number of reduction steps. If the checks are on the permissive side, we need to back them with a bound, or we would risk still running into divergence. If the checks are on the conservative side, we probably want a way to turn them off and fall back to a bound.

[milessabin]

There's a detailed description of the divergence checking algorithm along with a termination proof in the by-name implicits SIP. See here for what I implemented in dotty and scalac ... see also the descriptions just above of the previous scalac algorithm and the even earlier version described in the SLS.

I think a manually configured compile time option isn't a good idea because the user has no idea how to set it other than by increasing it until the compilation is successful or until they get bored. In the case of implicit resolution, deeply buried failures can be hidden by an overall failure, so an implicit resolution step limit would be extremely confusing for users. I'm not sure to what extent that would carry over to this case, but in general these sort of limits are unhelpful.

If you are able to use this algorithm for match type reduction, then we have a termination proof, so we're not trying to prevent an infinite loop. That being the case I think it's better to run without a manual bound and let users hit ctrl-c when they get tired of waiting.

[OlivierBlanvillain]

I still think that some sort of bound would be very beneficial for the end user. Hitting Ctrl+C is a pretty unfriendly workflow for IDE/sbt users...

How about we make the bound proportional to the maximum stack size? StackOverflowErrors are already used pretty much everywhere in typer to detect and report infinite loops, so we would be reusing reuse the de fact bound (and setting) to deal with very large types.

[odersky]

@OlivierBlanvillain Do you think that for implicits we should also have a bound? If not, why should the two scenarios be treated differently?

[odersky]

One question to ask is: Are there reasonably common situations where the divergence check shows termination but we blow the stack or the heap anyway? For stack, I don't see a common scenario. For heap, it could happen if the implicit search or match type reduction has a large fan out factor. But I think it would be very hard to tame that with a bound. Say we want to generate balanced binary trees of depth N in a match type. How do you bound that? You might want to go to a large fraction of the available heap and your heap might be very large...

[OlivierBlanvillain]

I don't have an opinion about implicits, if the current scheme is sufficient to compile the recursive programs that users write with implicit search, then it perfectly fits the bill. I also think it's reasonable to expect users to write more complicated programs with recursive match types compared to what they would want to write with implicit search.

One question to ask is: Are there reasonably common situations where the divergence check shows termination but we blow the stack or the heap anyway?

The answer is probably no, but I think that's asking the wrong question. Instead we should ask if (and why) we want to restrict recursive match types to be provably terminating? Unless we plan on using Scala's type system for theorem proving, I don't see any benefits...

[odersky]

The answer is probably no, but I think that's asking the wrong question. Instead we should ask if (and why) we want to restrict recursive match types to be provably terminating?

What is proposed is actually not provable termination of match types. What we should do instead is that during every match type reduction we detect a condition that with high-probability signals a divergence of that particular reduction. More precisely, we give up if during reduction we hit a selector type that has exactly the same set of class symbols and abstract types in its footprint as a type we have seen before and that is not smaller than that previous type.

One could also allow an override. I.e have this divergence test as a default and allow it to be overridden with a number of allowed reduction steps instead. My guess is that we would need the override only in very rare situations.

[OlivierBlanvillain]

If the checks in question can have false negative (i.e. they can fail to detect infinite reductions), then we probably want to back them up with a bound to catch those cases.

[odersky]

If the checks in question can have false negative (i.e. they can fail to detect infinite reductions), then we probably want to back them up with a bound to catch those cases.

I agree. It would be even nicer if the override could be provided by an annotation for a specific match type., Something like

@unfoldLimit(10000) type F[X] = X match ...

[milessabin]

I still think that some sort of bound would be very beneficial for the end user. Hitting Ctrl+C is a pretty unfriendly workflow for IDE/sbt users...

It's an even more unfriendly workflow to have to repeatedly increase a compile time limit until something compiles and potentially revisit regularly as code evolves. In practice I think you'll find people simply set the bound to a large arbitrary value so that it doesn't get in their way.

Maybe that's the answer? Have the default be "unbounded" and provide the option of setting a smaller bound for people who want it.

[odersky]

If the checks in question can have false negative (i.e. they can fail to detect infinite reductions), then we probably want to back them up with a bound to catch those cases.

Actually, no they do not have a false negative.