There's some significant sense to what you're talking about, so I'll share some pointers into deeper waters. The idea of a value being a type is the nature of

There's some significant sense to what you're talking about, so I'll share some pointers into deeper waters. The idea of a value being a type is the nature of "dependently typed" languages. However, they do it the other way around: types are merely values. This is very similar to what you're saying except DT languages would not have that 5 : 5 Instead, we introduce the idea of a singleton type. It works like this: for any type A and any value (x : A), we have a type (Sing A x) with exactly one value, (TheSing x : Sing A x). The other thing to keep in mind is that subtyping is kind of a rocky place to lay your type semantics. This is rough because most people are used to subtyping in their types. Instead, we note that whenever we have that (A :> B) then we have a function (A -> B) which is injective (really, an "epimorphism"). This broaden's our view to consider any injective function between types instead of merely some subtyping relation. Immediately it ought to be clear that (a) this is intractable automatically and (b) it's far more rich. Then it turns out that subtyping itself is fairly intractable (which subtypes are the right ones? there are many types intermediate between (Sing Integer 5) and (Integer)). So throw away automatic subsumption and require explicit coercions. This is workable and indeed in use today.