Informally, what I see as the defining rule for "closed world" is:

But that would break existing programs. You would need a language extension so the feature could be selectively enabled. There are plenty of proposals for how to do this (from closed class keywords to 'kind' statements)... I think however that you can get the benefits of better improvement rules without going all the way to a closed world. My question in the last post was: what if we assume an open world whilst type-checking and generating function type signatures, but assume closed world when resolving instances? Keean.