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).