Closed types as a simple approach to safe imperative multi-stage programming