The problem is more the former (nobody has gotten around to it yet), but also a bit of the opposite of the latter, i.e. the type system is so rich, type-checking may be undecidable in too many contexts.

Julia's parametric types are incredibly rich. You can look up 'dependant types' which are similar in the static world and see the sorts of hoops static language designers jump through to have dependant types and still be able to reliably prove theorems.

What you can do with Julia types is far more advance than I think you can do with any statically typed language.

I can add a type annotation in Julia which is a function call which returns a type e.g. This function can be of any complexity.

I think a better approach is simply a Linter. You report type problems you can find and ignore the rest. Not point trying to figure out the more advance Julia cases.

I would assume 90% of Julia code will use types in a pretty straightforward manner and thus would be able to be analyzed by some sort of Linter. Lint.jl e.g.

You're describing optional type systems; in this regard, Julia is on par with Python or TypeScript. The linter you're describing is also a type checker (like Python's Mypy). That said, it would be really interesting if someone would make a type checker that would evaluate/resolve those more complex types, at least those that can be guaranteed to terminate.

Optional typing and what Julia does is quite different. Julia type system is nothing like Python or TypeScript.

In Julia type annotations are not just a sprinkle of sugar. It has a very concrete use beyond asserting type consistency.

Julia types are used to decide what code gets run and memory layout of data.

I wrote an article showing a (probably naive) way how it could be done, but also discussing some of the limitations. At the end I think it would be better to think about these kind of tool as partial, automated tests rather than full-blown static type checkers.

https://nextjournal.com/jbieler/adding-static-type-checking-...