Pattern synonyms:

pattern Successor :: Natural -> Natural
pattern Successor n <- (precMaybe -> Just n)
  where
    Successor n = n + 1

precMaybe :: Natural -> Maybe Natural
precMaybe 0 = Nothing
precMaybe n = Just (n - 1)

pattern Zero :: Natural
pattern Zero = 0

Eliminator:

toChurch :: Natural -> (a -> a) -> a -> a
toChurch 0 _ b = b
toChurch n f b = f (toChurch (n-1) f b)

There are several other possible argument orders, the most natural of which is probably

natural :: a -> (a -> a) -> Natural

I don't have particularly strong feelings about whether we should pick one or offer both.

There are two strictly accumulating versions, corresponding to different versions of foldl'. But toChurch/natural is sufficient to define them:

toChurch', toChurch'' :: Natural -> (a -> a) -> a -> a
toChurch' n f = toChurch n (\r acc -> r $! f acc) id

toChurch'' n f = toChurch n (\r !acc -> r $ f acc) id

So we shouldn't necessarily feel obligated to include those. I doubt the time is ripe for a dependent eliminator.