> Better type information. Because the program is always in a valid state the type checker can always run and give meaningful feedback.
Note that programs can be syntactically well-formed but ill-typed. For example `let x = true + 1` has valid syntax but produces an "undefined" type for the variable `x`, if the type system does not support type error recovery.
Note that programs can be syntactically well-formed but ill-typed. For example `let x = true + 1` has valid syntax but produces an "undefined" type for the variable `x`, if the type system does not support type error recovery.
A quote from the great paper from POPL 2024, https://hazel.org/papers/marking-popl24.pdf
> If a type error appears _anywhere_, the program is formally meaningless _everywhere_