Adding IsNat constraint to Vec functions

This change is kind of pervasive, requiring that any Vec operations to carry an IsNat constraint. But on the other hand, it seems to avoid the binary branching issue for circuit programs that I wrote. You can play with it and see if it solves your problem. 

Also I removed dependencies on Typeable, which seemed to crash Hermit on my program. Feel free to add it back if you need it.