In polymorphic and dependently typed languages, there is a tension between checking conversion as efficiently as possible, and preserving unfoldings of definitions. The latter is desirable in user interaction, and also critically important in unification, where metavariable solutions tend to blow up in size if definitions are unfolded all the time. Additionally, conversion checking and scope checking can benefit from speculative shortcuts, where we attempt to check something without unfolding certain definitions, and possibly retry with unfolding, on failure. We describe a design for efficient open evaluation with preserved unfoldings. The simplest setup distinguishes top-level and local definitions, and only preserves top-level unfoldings; we describe this version, although preserving arbitrary unfoldings is also possible with a moderate increase in complexity.