A (counter)example from the recent research literature: almost every simply typed $\lambda$-calculus term has a long $\beta$-reduction sequence (Asada et al., 2019), but this property is very hard to test, even if P = NP!
Asymptotically, almost every STLC term of order $k$ and length $n$ has reduction sequence length $(2\uparrow \uparrow (k - 1))^{\Theta(n)}$, where $2 \uparrow \uparrow n = 2^{2^{2^{...}}}$ is the exponential function iterated $n$ times. However, to test this property, the only way is to $\beta$-reduce this term and check the reduction sequence length. STLC is strongly normalizing, so it is certainly decidable, but apparently this will take at least $O((2\uparrow \uparrow (k-1))^{\Theta(n)})$ time in the worst case, assuming that each reduction step takes $O(1)$ time. Deciding this property is apparently not in P. In fact, it is in $k$-EXPTIME, so it is not in P even if P=NP!
In the other direction, it's trivial to show that the implication doesn't hold: it is easy to check if a STLC term has a polynomial-length reduction sequence, but almost no term has such a short reduction sequence.