I’m not sure I buy this definition of type even in theory.

From a category theoretic point of view a type would be nothing more then the constraints on how terms may be composed.

Either you simply view types as as objects in some category or, perhaps a bit more interesting, as a functor. See f.ex http://noamz.org/papers/funts.pdf

Or rather it seems to be a common theme in language design to conflate these two notions of types, and we should probably stop doing that.