In principle, the type checker could be pluggable. That would mean the language isn't burdened by the limitations of any particular type checker, although it w

In principle, the type checker could be pluggable. That would mean the language isn't burdened by the limitations of any particular type checker, although it would almost certainly be burdened by complications at the boundaries of where one type checker is used versus another. It also might be reasonable to insist that such a system represents a family of languages rather than a single one.