make read monadic

This fixes some issues with Coq permitting non-CBV reductions in the embedding.