@charlag @amiloradovsky They do have annotations, and I think what Théophane meant is that type errors should not prevent from typechecking the rest or running the code.
I'm more disturbed by the enormous complexity of the type system, and that all the examples shown seem to be code that no one reasonable would want to write. I wonder if there couldn't be a simpler type system with the same objectives. But I really am illiterate in gradual typing.
functional.cafe is an instance for people interested in functional programming and languages.