Your blog posts (that I read a few weeks ago) and your comment here are the best explanations I've ever read on this topic. You're not just looking at the surface of the problem, but diving in the why it is like that, semantically. I really like that you mentioned dependent typing in your conclusion.