The type checker can only prove what is known at compile time and only if you're disciplined.

To bridge runtime and compile time (as your application will likely get some external data) you've got to use a proper parser such as zod[1] or if you want to stretch it even further effect-schema[2].

[1] https://zod.dev/

[2] https://effect.website/docs/schema/introduction/