That said, it's a completely true point in the notion of "static-types-as-type-theory-defines-them" that dynamic typing is a mode of use of static typing which is completely captured in large (potentially infinite/anonymous) sums. Doing this gives dynamic languages a rich calculus.
Refusing to doesn't strip them of that calculus, it just declares that you're either not willing to use it or not willing to admit you're using it. Both of which are fine by me, but occasionally treated pejoratively because... well, it's not quite clear why you would do such a thing. There's benefit with no cost.
Then sometimes people extend this to a lack of clarity about why you don't adopt richer types. Here, at least, there's a clear line to cross as you begin to have to pay.
The "Church view" and "Curry view" are psychological—the Wikipedia article even stresses this! So, sure, you can take whatever view you like.
But at the end of the day type systems satisfy theories. Or they don't. That satisfaction/proof is an essential detail extrinsic to your Churchiness or Curritude.