Skip to content

Arity: Rework `ArityType` to fix monotonicity (#18870)

Sebastian Graf requested to merge wip/T18870 into master

As we found out in #18870 (closed), andArityType is not monotone, with potentially severe consequences for termination of fixed-point iteration. That showed in an abundance of "Exciting arity" DEBUG messages that are emitted whenever we do more than one step in fixed-point iteration.

The solution necessitates also recording OneShotInfo info for ABot arity type. Thus we get the following definition for ArityType:

data ArityType = AT [OneShotInfo] Divergence

The majority of changes in this patch are the result of refactoring use sites of ArityType to match the new definition.

The regression test T18870 asserts that we indeed don't emit any DEBUG output anymore for a function where we previously would have. Similarly, there's a regression test T18937 for #18937 (closed), which we expect to be broken for now.

Fixes #18870 (closed).

And also we emit the Exciting arity warning only after the second iteration now.

Fixes #18937 (closed).

Edited by Sebastian Graf

Merge request reports