Does Church encoding allow us to define recursive types with non-strictly positive pattern functor?

[winitzki]

This question is about https://counterexamples.org/strict-positivity.html

Define F t = (t → p) → p. Then F is positive but not strictly positive.

Now use the Church encoding to define T = ∀ (a : Type). (F a → a) → a. The type T is the Church encoding of the least fixpoint of F. Using parametricity (as indicated in Wadler's "Recursive types for free") we can prove that there exist mutually inverse functions fix : F T → T and unfix : T → F T.

These functions appear to provide the axioms introA, matchA, and beta in the text. Then we can derive a contradiction.

Why is this not a problem? Is this because we cannot prove that fix and unfix are inverses without parametricity, and parametricity is somehow not encodable in Coq without further axioms that are somehow bad? Or is this because the Church encoding is itself somehow ill-typed?