Should we have a "types-first-by-fiat" mode?

This is something that just came up in conversation between me and @georgefst. Should we add a mode where the student can't edit a definition's term until the definition's type no longer has any holes?
