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-checkin

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.