I mean, Haskell has compile-time checking all over the place and it's dynamic.

Hm. Perhaps we are at crossed threads after all. The concept of Haskell being a dynamic language goes right over my head. Indeed, if that article is anything to go by, I'd say that it was damn nearly impossible for Haskell to:

• extend the program, by adding new code;
• extend objects and definitions;
• modify the type system;

all during program execution.

I would say that it runs exactly contrary to the entire motivation of Haskell.

It's interesting to conceive of what it would take, and the processing power it would require, for Haskell to eval generated statements at runtime and cross-reference (and inference) the types generated, with whatever remains of the type annotations that where present in the source code of the original program.

AFAIK, the whole basis of term rewriting is that once type compatibility has been verified, the expansion and/or reductions of terms can be directly substituted for the terms they rewrite, and so large chunks of the definitions in the original source code don't make it into the object code in a recognisible form whatsoever. It would therefore be impossible to extend the compile-time type system at runtime.

I realise that a Haskell program can be written to parse, compile and run (or interpret) a different type system (language; ala. pugs), but a Haskell program that could eval code at runtime and then extends its own type system on the fly, is a whole different ball of wax.