I think the argument is that when every value inhabits the sole type and everything accepts that type, you get a system that works the way "untyped" languages d

I think the argument is that when every value inhabits the sole type and everything accepts that type, you get a system that works the way "untyped" languages do. Why have two separate concepts when you can gain some true conclusions by unifying? I think Harper would take issue with it being explained this way, but one can think of Ruby and Python being languages where everything is a pointer to a HashMap and everything else is just sugar on top of that (similar to the above argument about Java and the sugar with the pointers). I don't think Harper would like that way of explaining it because it's over-focused on an example instead of sticking to the concept and because it conflates (statically-knowable) types with (runtime) classes, which is big no-no with him.