Lambda the Ultimate

I'm working on a compiler for a Scheme-like language, 'Irken'. The purpose of Irken is to generate a VM for a (yet to be designed) python-like language. I intend for Irken to be the implementation language for the VM, and also to be the language by which the language is extended - similar to the role of pre-scheme in scheme48.

http://www.nightmare.com/rushing/irken/

One goal here is to eliminate the need for end users to program in C.

Another reason for the roundabout approach: I want massively scalable cooperative threads (think 100,000+ threads, think Erlang)... so using the C stack is out (as is BitC, which I've recently learned about here).

Irken is a whole-program compiler that generates one large C function - 'vm()'. Irken uses the gcc address-of-label extension and 'goto' to implement closures. The current continuation (i.e., 'stack') is heap-allocated.

A couple of months ago my desire for a speedy VM got the best of me and I decided to dabble with type inference - mostly so I could get rid of runtime type checks. It's also nice to get the type safety. 8^)

I now have ML-style let-polymorphism - the algebraic data types. I can implement nice polymorphic data structures like red-black trees, parsers, etc. I've been pleasantly surprised at how little trouble the type inference has been. I've been able to write well-typed generators using call/cc, for example.

I put off thinking about records for a while, assuming that it would be a sugary detail. Now I'm seeing that it's more of a tar pit.

So I'm asking for advice - given the purpose of Irken, what approach should I take in adding a record type? Depending on the amount of work and complexity involved, I could accept anything in the range of 'all records require type annotation' to 'everything is figured out magically by the compiler and has no run-time cost'. Leaning toward the latter direction, though. Also, it'd be nice if I could sugar it up to support some simple OO features.

I've read Wand's "Type Inference for Record Concatenation..." and a bunch of stuff by Remy related to OCaml's row polymorphism. I've also been reading Ohori's "A Polymorphic Record Calculus...".

The impression I have right now is:

Wand: simple monomorphic records + recursive types.
Remy: less simple polymorphic records + recursive types.
Ohori: really cool polymorphic records but no recursive types?

The Ohori approach also looks like I'd have to throw my existing code away - it seems to replace products and sums with labeled records?

Thanks for any and all advice!