Have we agreed that `auto` is OK?  I thought we concluded that we weren't (and there are no other instances of it in the code).  If you think we should, feel free to reopen the discussion.