A higher-level answer, after thinking a bit more about this problem.
The high-level intuition of the finite-model result in my work is that neutrals subterms correspond to how the terms "observe" their context. Even if an atomic type $\alpha$ may be instantiated by a type with an arbitrary number of inhabitants, to distinguish two specific terms $t, u$ you need at most as many elements in $\alpha$ as they make observations of this type $\alpha$ (so: counting the neutral subterms of type $\alpha$ occurring in either of those terms).
This reasoning relies on having a focused normal form, which is stronger than being a $\beta$-short normal form. Focusing prevents "breaking" a neutral with elimination constructs (
(match x with inl () -> n | inr -> lam y. y) v, which "hides" the neutral subterm
n v), which you could get with commuting conversion rules. In addition, it forces neutral subterms occurring in non-neutral subterms to be of atomic type. For an example of the latter restriction, you cannot write $x : \alpha \to \beta \vdash x : \alpha \to \beta$, you have to write $x : \alpha \to \beta \vdash \lambda (y : \alpha). x~y$. This corresponds, in the sequent calculus, to restricting the axiom rule to atomic types.
In absence of empty types, my intuition is that you cannot get more than TOWER-many neutral subterms in the normal form of a term. (You provided Church naturals as as an example where we can effectively get this many neutral subterms.) Putting a term in focused form may expand its size, but again, not by more than an exponential factor, so we remain TOWER. So the intuition is that the atomic types are instantiated with TOWER-sized finite types.
Then term-based approaches to decide equivalence use different notions of normal forms, often stronger than focusing (in my work: canonical forms, which are a sort of maximal multi-focusing). They can be thought of as approximating, in the syntax of terms, the extensional representation of inhabitants in the set-theoretic model. (For example: Böhm trees are doing exactly this.) You could consider instead, as a concrete syntax for elements in the set-theoretic model, their representations as finite trees, where trees at atomic types $\alpha$ (instantiated by a finite type) are just a natural number, trees for $A*B$ are pairs of trees, trees of $A+B$ are a pair of a boolean and a tree, and trees of $A \to B$ are one node with $A$-many children that are trees of $B$.
You can compare two such trees in time linear over their size (obviously), and this gives you an equivalence algorithm, an upper bound. The size of those trees is, in the worst case, an exponential tower over the size of the atomic type(s). If I understand this right, this suggests that the size of the tree is an exponential tower over an exponential tower over the initial, non-reduced term, which remains an exponential tower.
Now about the empty type: canonical forms in presence of the empty type are a bit strange, because they need to search for proofs that the context is inconsistent. But if you have this extensional view of the elements of the set-theoretic model, adding the empty type does not increase the size of the trees, on the contrary it makes some sub-trees trivial when it appears on the left of an arrow. So my intuition would be that you get the same upper bound.