With how much LLMs do nowadays, I'm waiting for the time when specifying types is unnecessary. Like, it if can write code, shouldn't we also be able to have an AI type checker?

Systematic checking like that is pretty much LLM's worst case. They're really bad at it. Definitely better to use them to suggest types.

Correctness is a key characteristic of a compiler.

To have something that sometimes checks the types and some times does is not a feasible solution.

It writes better when correct type is specified beforehand. So chicken and egg problem you have.