No, it will be ensured at run time, as all unboxing happens through pattern matches (which, btw, is EXACTLY what happens with a dynamically typed language).

For example, I can define...

  (+) :: Dyn -> Dyn -> Dyn
  (+) (I x) (I y) = I (x + y) -- integer addition
  (+) (S x) (S y) = S (x ++ y) -- string concat

So I can now use the + operator on variables of type Dyn. If a value has the wrong tag, then a pattern matching exception is thrown. Once I get enough primitive operations defined, I will never really have to manually unbox a value of Dyn type again.

The one difficulty is emulating objects, because we would not have good syntax for arbitrary method calls. We could take a Smalltalk-like or Erlang-like approach, where the object takes message... the message being of type Dyn.

We should really look at dynamically typed languages as subsets of statically typed languages. In other words, they are not untyped, they are unityped. In other words, statically typed, but with exactly one type. This is the relationship between typed and untyped lambda calculus (untyped lambda calculus is actually typed, where every term has type Mu X. X -> X)