actually type-level integers are easier to work with than type-level naturals (e.g., one can cancel things by subtracting at will).   I agree that ideally we want to have both integers and naturals (probably as separate kinds).  I just don't know what notation to use to distinguish the two. 

-Iavor