I have the same question... if a type is used by the type-checker to verify the consistency of the data it’s annotating, then I don’t see how a recursive definition could provide anything new, other than potentially making type checking run forever...

Although maybe there’s something conceptually satisfying about defining bottom as the only type that refers to itself?