A precise definition of what it means to be an instance of an abstract type

Well, it is a graph, and intransitivities are view as bugs, but it would be inaccurate to call (X , <:) a tree. In fact, it is not even intended to be a tree. I think it is intended to be a bounded lattice (with Any and the top and Union{} at the bottom). Thus, unlike a tree, the induced undirected graph therefore has cycles everywhere (even if we rule out intransitive bugs).

But seeing a Type outside a method signature is code smell, and integrating Type and DataType into your mental map of Julia types is just a recipe for a headache.

I have a proof that concrete types form tree though. (Thanks to that mathematical mindset.) So actually, the only part of the type structure that doesn’t give me a headache is the concrete type tree (which has DataType at as its root and is formed via compositions of typeof).

PS. Unfortunately, when you have that mindset, there is nothing you can do to give it up. It usually pays off in the end though.