Otherwise one is forced to think about the semantical consequences if the argument specification does not satisfy the parameter specification.
For example, in general, if the body of a generic specification is a conservative extension of the parameter specification and if the argument specification and the body only share symbols via the parameter signature then the result of the instantiation is a conservative extension of the argument specification.
But take the following specification:
GSpec (gen-extension [sort s, const a,b: s, a = b] [sort s'])GSpec is a persistent generic specification because the body does not restrict the models of the parameter specification. However,
GSpec([sort s, const a,b: s]) does not yield a
conservative extension of [sort s, const a,b: s] because the
semantics of instantiation imposes the restriction a = b on the
models of the argument specification.
One serious problem is that a user might deliberate write specifications that take advantage of this semantics of instantiation. This problem can be addressed by tools that warn the user about such situations and generate appropriate proof obligations. However, the best way to show our intend for tools to recognize such situations is by reflecting them in the semantics.
As a consequence of our proposal, the definedness of the semantics of instantiation is undecidable. However, well-formedness of instantiation still remains decidable, as well-formedness only requires the fitting-morphisms to be signature morphisms from the parameter specifications to the argument specifications.