What are the semantics of your macros? If they are FEXPRs, then you won't be able to do much in the way of static typing for your language.<p>You could take a look at Alan Bawden's first-class macros [1].<p>Either system F or type dependency will require type annotations, although the type systems literature contains a number of workarounds to keep the overhead low. I'd recommend a simpler type system if you don't have a clear need for impredicative or dependent typing.<p>[1]: <a href="http://lambda-the-ultimate.org/node/2987" rel="nofollow">http://lambda-the-ultimate.org/node/2987</a>