Lambda the Ultimate

I've been reading papers about Ωmega, and I'm very fascinated by them.

At the same time, I'm invested in untyped, dynamically type-checked programming. I'm not sure I want to give it up - it has some conveniences in interactive programming that I consider essential.

But is there actually a reason why GADTs wouldn't work in a dynamically type-checked language? FGJ_ω and an extension of C# show that you can encode (some?) uses of GADTs once you have type operators/higher kinds or equational type constraints, respectively. Couple that with exact runtime types as in the CLR and it seems to me that theoretically you could enforce GADT properties even in a dynamically type-checked language.

Now, you might ask, what's the point? Let's take the type-safe AST evaluator (yeah, I know... ;)). Well, of course, you'd lose the ability to prevent the construction of ill-formed AST objects at compile-time, but you'd still have these guarantees at run-time. And that would be an improvement over plain dynamically type-checked languages, no?