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

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?