It’s being discussed in various places already and seems to be something which won’t happen until this or as part of it The lack of formal definitions has been a pain point for other things already.
This was intended as a point to how better definitions can enable tooling to take on more for users and don’t necessarily conflict with making it easier for users under the general sentiment of the original post that we should be working towards a future for typing that enables and considers all audiences and figure out how we can best do that.
The tangential bit on smarter inference based on results from set-theoretic typing has a way of working already (it’s a solved problem in academia) that has a reasonable runtime for any non-infinitely recursive types or program structures. I imagine this would lead to an implementation that if it got to a certain recursion depth, it told the user why it gave up on detecting the type of that variable and which variable it needs more information about. Outside of the actual correct type of json/toml etc., I can’t think of much that’s actually infinitely recursive in that manner, and each of these is built up of a few base types that providing would be enough, and that it would be detectable what the type checker needs more info about (unless we also add Higher Kinded types, then we’re in unproven territory again).
I’ll break that tangent out into another post though, as even though it could help with typing being more accessible and less intrusive while getting more accurate (hence bringing it up here), it’s a “big idea” even if it’s conceptually simple in why it would be useful.