I support this. It's very annoying to have to provide types even for things you don't care to type check for. Especially when the types you'd declare are not source of truth anyway because you are using third party code. Maybe an optional warning for traversing such "any" or "unknown" types would be useful as well

Another potential way to frame this syntax-wise is similarly to Rust's unsafe. Make it so any type errors within unsafe ... end are ignored. That's probably less ergonomic though, as usually most of the types are known, and it's just one or two values which are unknown

Thank you for the feedback!

A behavior similar (but not identical) to what you asked for currently exists in the unknown type, which is the implicit type of variables that are not annotated. When a file has a .lua extension, the compiler goes into "lax" mode, and anything about unknown variables is ignored, other than reporting their existence as warnings.

The idea was that one would take their .lua file, start running tl check on it, get a zillion unknown warnings, and start type-annotating them gradually, to the point where the file is fully annotated, then it becomes a .tl file, which can then be checked in the default "strict" mode. Of course, .lua files with partial annotations are not proper Lua files, so that was meant as a temporary state. But at least that makes the conversion process less grating than starting with a zillion errors (because in "strict" mode the errors due to insufficient annotation propagate a lot more).

What I didn't want is to be too lenient on missing annotations, to avoid the situation you see in TypeScript where people abuse any in places that could be typed trivially, so dissuading people from reaching out to any all the time is a constant concern in the TS world.

Note that in Teal, the any type has semantics that match TypeScript's unknown type: the only thing you can do with it is pass it around, or cast it. Effectively, the names any and unknown have opposite meanings in TS and Teal, with the difference that currently in Teal you cannot explicitly declare a variable as unknown. Another problem in TypeScript is that people often use TS any (their "do anything with it" type) in places where they really intended to use TS unknown (their "just pass it around" type). Teal started cautiously, by only exposing the "just pass it around" type.

In short, in lax mode, Teal's unknown type is the "do anything with it" type, and it does have the behavior you suggested for dynamic. I still don't like the idea of exposing unknown as a free-for-all and ending up in a situation like TypeScript's where it over-proliferates, but I'm taking your feedback as a sign that finding a middle ground should be considered. Perhaps allowing explicit unknown but triggering a warning by default? I'm not super happy with that option, but I'll keep thinking and I'm open to more ideas and feedback.

Regarding the source of truth in typing for third-party libraries, that's a common dilemma when going from untyped to typed code. The preferred approach is to declare .d.tl files with the typing info of those untyped Lua libraries, and having that be the clear boundary within the untyped and typed worlds, ideally producing reusable declarations like the ones we have in the teal-types repo (even if the DX ergonomics for that are not fully solved yet). I wouldn't want for people to stop contributing type declarations and just start to use unknown everywhere they use a Lua library instead.

I wanted to add provide a bit more context and feedback as someone looking to incorporate Teal into my existing Lua project. I recently learnt about Teal and was very excited because I had previously moved a project from Javascript to Typescript and the experience was great. However, when it comes to Teal I have greatly struggled to migrate.

My sense is that Teal is not really about gradual typing as much as TS is. Requiring .lua files into .tl files practically compels you to rewrite the code unless you write a .d.tl file for every .lua file and maintain them alongside your .lua code. I really like the suggestion mentioned above for adding unsafe blocks. Probably adding a require_unsafe() to require .lua code without having to provide type annotations can also be an interesting feature. I really believe focusing on gradual typing can make it much easier for developers like me who want to bring type checking into their lua codebases.