That rebuttal is confused and unconvincing. It's easy, although clumsy and verbose, to write a very close equivalent of his "impossible to type check" code example in a static language. Define a sum type that ranges over the necessary values, define a few functions over that type that perform a case analysis corresponding to dynamic type checks, etc. That it's possible to do this is exactly the basis of Harper's argument that dynamic languages are subsumed within static languages.
Here's an concrete didactic example of the approach:
http://okmij.org/ftp/Scheme/scheme.ml
Static languages are not good dynamic languages (as currently designed), but they do subsume them.
This is not precisely about Tratt's response, but there was a great discussion on another Bob Harper post where Matthias Felleisen argued that while dynamic languages are semantically unityped, at the level of pragmatics (in the linguistic sense) they allow the programmer to freely mix various implicit type disciplines (http://existentialtype.wordpress.com/2014/04/21/bellman-conf...). The cost is of course that the programmer gets essentially no assistance in verifying that their implicit types are consistent.
There's no reason to believe that you can't freely mix implicit type disciplines in "statically typed" languages, either!
It's just (a) oftentimes you can actually reify those implicit schemes into actual types and it's often worth the cost to do so and (b) if your compiler depends upon a choice of type semantics in order to function and your implicit system is inconsistent with that selected type semantics then your analysis may not guarantee compilation!
But again: dynamic types are a mode of use of static types.
---
To be clear, this is the brunt of Bob's response in the linked thread anyway.
Here's an concrete didactic example of the approach:
Static languages are not good dynamic languages (as currently designed), but they do subsume them.