Writing pure predicates is pretty difficult and a pretty convincing argument was made recently that typestate predicates don't need to be pure. Removing the pred concept would simplify things a lot.