He may be one of the world's top researchers in the field, but on this point his view is not the consensus view of PLs researchers; other top researchers in the field think that Harper is wrong on the subject. On the other hand it's mostly a semantic dispute over who owns the word "type", which has historically come from multiple sources in mathematics and engineering. The C view of types is closer to the comp-arch view of "typed registers", which isn't really a proof so much as a statement about data-representation capabilities ("this register can hold floats").

It's unsurprising Harper doesn't like that view, because he objects to the entire line of machine-oriented CS thinking, on both the engineering and the theory sides. For example, he thinks computational complexity theory should ditch Turing machines and be refounded on the basis of functional programming.