Then maybe all this conflict really is "a problem of grammar", as Harper himself asserts. For me, the word type has a differenn meaning than for you. Maybe we should instead be using the expressions static type (compile-time proof) and dynamic type (runtime properties of data, which Harper calls class, though I prefer not to use this word as its meaning is already too overloaded in CS).
What you're calling a dynamic type is what he'd call a canonical form. If your typing system has product types, then you should be able to prove that anything with a product type evaluates down to an ordered pair.
