Oh cool, it's amazing how quickly you can stand up a language now, I love it. I'd love to exchange ideas, I really like what you're doing.

How are you doing resolution of your dependent(refined?) types? I've been using Z3, but you're clearly doing something else here.