Right. In fact, this phrase from Harper's blog was one of the inspirations for my post:

In Carollian style there are types called naturals and lists, but that’s only what they’re called, it’s not what they are.

ETA: it seems you slightly misunderstood Harper's point. The problem with defining "data Nat = Zero | Succ Nat" is not that bottom is in Nat, but rather that laziness allows you to write the circular definition "omega = Succ omega" (note that pattern-matching on omega doesn't hang), which is similar to the unary example in my post.