Are Bad churches inhabited?
No, it is not sufficient to check that the 'Church encoding' is uninhabited.

Consider the type:

$$\mathsf{data} \;U = L\ (U → U)\;  |\; A\ U\ U$$

The idea is that $U$ is the type of untyped lambda terms. If you allow this as a data type into your language, it causes problems. At the very least, you can write loops in $U$ if you are allowed to inspect its values by case analysis.

δ : U -&gt; U
δ (L f) = f (L f)
δ x = x

ω : U
ω = δ (L δ)

-- ω ==&gt; δ (L δ) ==&gt; δ (L δ) ==&gt; ...


If you are also allowed to do recursion on the presumption that $U$ is well-founded, these loops leak into every other type.

However, the 'Church encoding' of $U$ is not uninhabited:

$$U' = ∀ R. ((R → R) → R) → (R → R → R) → R$$

In fact, this is a somewhat well-known representation of untyped lambda terms in a sort of higher-order abstract syntax. You can write down (an encoding of) any untyped lambda term you want:

$$id : U' = λ L. λA. L (λ x. x)$$
$$comp : U' = λ L. λA. L (λ g. L (λ f. L (λ x. A\ g\ (A\ f\ x))))$$
$$δ' : U' = λ L. λ A. L (λ x. A\ x \ x)$$
$$ω' : U' = λ L. λ A. A\ (L (λ x. A\ x\ x))\ (L (λ x. A\ x\ x))$$

So, this encoding is certainly inhabited. But, the reason I was using scare quotes earlier is that is clearly still not what we expect the original data type to mean, so it's rather unclear whether this should be considered the Church encoding of that data type. For instance, you will be unable to exhibit the equivalence:

$$U' \cong (U' → U') + U' × U'$$

which is expected of the data definition. Also, $U'$ is arguably a more faithful representation of the syntax of untyped lambda terms, because all we can do is abstract and apply, as those are the only things we know about the abstract $R$ type. $U$, at least presuming the usual semantics of data, allows us to write, "exotic terms," which is what δ and ω actually are (note that they're not the same as $δ'$ and $ω'$). And this makes sense, because these exotic terms are what allow us to write loops using the data type, whereas $U'$ is a perfectly acceptable System F type, and System F is strongly normalizing.

So, clearly, some more thorough check is necessary than mere habitation. You must check that the 'encoding' actually models the properties you're going to allow your data type to have.