I have another argument to present.
It’s well known with higher rank types (or system-f more generally), you can perform Scott encoding to embed algebraic data into functions. This gives us a isomorphism between algebraic data and it’s encoded correspondence.
Here’s a simple example that encodes a pair of integers.
data Point = Point Int Int
newtype Point' = Point' (forall r. (Int -> Int -> r) -> r)
to (Point x y) = Point' (\f -> f x y)
from (Point' f) = f Point
However, if any of a record’s fields are strict, the correspondence is gone, since Haskell does not support strict functions (levity on the arrow), the new arguments of the function now permit bottoms.
data Point = Point !Int !Int
newtype Point' = Point' (forall r. (Int -> Int -> r) -> r)
-- not surjective, `x`, `and `y` cannot be bottom, but the function can accept bottom
to (Point x y) = Point' (\f -> f x y)
-- not injective, `f` lazily takes two arguments, but it evaluates them
from (Point' f) = f Point
This can be fixed with strict functions.
data Point = Point !Int !Int
newtype Point' = Point' (forall r. (!Int -> !Int -> r) -> r)
to (Point x y) = Point' (\f -> f x y)
from (Point' f) = f Point
Now these functions are proper bijections again. Hence the existence of strict fields hint toward the existence of strict functions and levity on the arrow, not the kind.