To Iavor's email: I think the design you describe makes good sense, but only for a language without dependent types. A language with dependent types could be imagined with "languages above" and "languages below", but I think the "above"/"below" switching would introduce friction with little self-sustaining benefit. By "self-sustaining" there, I mean that a dependently typed language often has no need for different languages above or below, and so making that distinction in a dependently typed language is awkward. However, one could imagine a dependently typed Haskell that retains the distinction, essentially for philosophical backward compatibility. ("Philosophical" because I believe we can design dependent types in Haskell to be fully backward compatible, but it might require a new way of thinking about what phrases in the language mean.)

Perhaps even more directly, avoiding a distinction between languages above/below is a key component of what I require in an ergonomic interpretation of dependent types. Keeping the distinction would, unless I'm convinced otherwise, appear un-ergonomic.

Richard