Flattening should not remove declarations from anonymous instantiations in the main module

[shonfeder]

The language spec describes "anonymous" instances as follows

https://github.com/informalsystems/quint/blob/393ec51329429ce8d99016921fea777b53ea357d/doc/lang.md#L2025-L2058

This makes it clear that the current intended semantics of instances of the form

import Foo(...).*

is that the contents of Foo should be treated as if it is included in surrounding module. We take advantage of this behavior currently, as it is the only way of configuring constant values. E.g., in

https://github.com/informalsystems/quint/blob/393ec51329429ce8d99016921fea777b53ea357d/examples/classic/distributed/ClockSync/clockSync3.qnt#L139-L145

Which is meant to define a module clockSync3 that has all the declarations of clockSync3Spec, except with the constants t_min and t_max replaced with the specified values.

However, the current behavior if the flattening phases undermine this intent, as they remove all declarations which are not referenced by a declaration in the main module. This has the result of leaving clockSync3 after flattening.

The verify command has added a hack to workaround this

https://github.com/informalsystems/quint/blob/393ec51329429ce8d99016921fea777b53ea357d/quint/src/cliCommands.ts#L695-L716

Whereas the compile command has not, meaning we compile a spec like clockSync3 into an empty module

https://github.com/informalsystems/quint/blob/393ec51329429ce8d99016921fea777b53ea357d/quint/apalache-tests.md#L254-L272

My proposal is that the declarations added by anonymous instances should be treated as inclusions into the instantiating module, and that all declarations included this way should be left in place after flattening.