ErrorT

The Idris monad now includes an explicit ErrorT to force the types of errors. This is a preliminary step to error reflection.