Thanks for reporting. This is known problem (#4647) which we decided not to fix (#4959). You already describe the correct workaround.

I think some kind of change is needed. I remember using parametrized modules before, encountering this issue and then abandoning parametrized modules. I believe that parametrized modules could be used more and would support well generic modules and more generic programming, but this issue might discourage using them.

I don't fully understand the technical details in the discussion I but have the feeling what Ulf Norell suggested was a good idea:
#4647 (comment)

What about Alt B, but we add an emacs command to switch between "evaluation mode" (not using the interface for the current file) and "regular mode" (the normal behaviour). This should solve the drawback when switching files, if we reset the to regular mode when changing buffer.

I can see that the idea by Andreas in reply to this, to make this automatic when executing C-c C-n, might not be a good idea, but having a switch between modes rather than creating an artificial goal might be a better solution. One could as well add a hint to C-c C-n about using such a switch. At least some documentation in the section on parametrized modules would be good (and I don't think it would look well if one wrote in the documentation: if you want to evaluate an expression in a parametrized module you first need to create an artificial goal. At the moment one gets some quite cryptic error-messages.

I implemented #4647 (comment) but had to rip it out again since there were additional reloads which caused UX problems in large projects.

Btw, this issue has nothing to do with parametrized modules vs. non-parametrized modules.
If you import module1as public you should not have the not-in-scope issues.

open import basis
module module2 (x : Bool) where
open import module1 x public

I'm sorry, it's always unsatisfactory if you do some changes and then have to undo it (I was just going through such a loop in my own Agda code).

I have the feeling the problem is how to do it in such a way that it applies only to the current buffer. In some sense, all one needs to do is get the system in the same state as it would happen if one added an artificial goal. My guess is that it could have a knock-on effect on any other files which refer to the current one (it's almost like that they need to be treated as having flag --allow-unsolved-metas). So if any other file refers to it and one retype check it, one would revert the buffer where this change was made back to its original state first. It's almost like the following workflow: normalising the goal - change buffer as if it had an open goal. Typchecking any other buffer referring to it - change buffer back to as if there was no open goal.

I reopen this issue so others can reply.

I don't think the reopening succeeded, it still shows as "closed".