Arity analysis: `andArityType` is not monotone
As I discovered in the bottom half of #18793 (comment 308397), the
andArityType operation of the arity analyser is not monotone. That's really bad because that operation should compute the least upper bound of both arguments, which it completely fails to do. In particular, we have
ABot 1 < ATop [OneShotLam]
f l = andArityType l (ATop [NoOneShotInfo]) f (ABot 1) = ATop [NoOneShotInfo] > ATop [OneShotLam] = f (ATop [NoOneShotInfo])
So we found an example where we have
a < b, but
f a > f b, violating monotonicity.
The important point here is how we handle one-shot lambdas which have a bottoming body. I see two ways to fix it:
- We could simply "fix"
andArityType (ABot _) (ATop [NoOneShotInfo]) = ATop [OneShotLam]. I don't think that's a good idea, since we might eta-expand too much.
- We could record one-shot-ness by giving
ABota list of
OneShotInfo, like we do for
ATop. Then we can have
andArityType (ABot as) (ATop bs) = ATop (as ++ repeat NoOneShotInfo `combine` bs), very similar to what we do for
ATop, but with the bottom case supplying infinite non-one-shot arity.
I rather like 2.