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

Mistake in explanation in "Under false pretenses"

Suggestion: overloading is exponential

Suggestion: add definitional floating point equality

Distinctness II: Recursion is also applicable to Rust

Eventually, nothing: factually inaccuracy about the C standard

Please add Rust's bug, which is reverse of "Runtime type misinformation"