Fix arity type of coerced types in CoreArity
Previously if we had
f |> co
where f
had arity type ABot N
and co
had arity M and M < N,
arityType
would return ABot M
which is wrong, because f
is only
known to diverge when applied to N
args, as described in Note
[ArityType]:
If at = ABot n, then (f x1..xn) definitely diverges. Partial
applications to fewer than n args may *or may not* diverge.
This caused incorrect eta expansion in the simplifier, causing #16066 (closed).
We now return ATop M
for the same expression so the simplifier can't
assume partial applications of f |> co
is divergent.
A regression test T16066 is also added.
Fixes #16066 (closed).