Nils Anders Danielsson

> […] there is currently no way to preserve your module's interface […] I think it would be good if the module language could be based on some simple, orthogonal...

This is supposed to work: https://github.com/agda/agda/blob/4392e74b88de51c8bbb5a26f307e1a3047c14073/src/data/emacs-mode/agda2-mode.el#L441-L444

Can you construct a reproducible test case?

I saw now that this feature is only supposed to work for cached interface files: https://github.com/agda/agda/blob/856415f51b60171f9799912cfc89622913783f88/src/full/Agda/Interaction/InteractionTop.hs#L565-L595

I seem to recall that the reason for this restriction is that I did not want Agda to automatically purge the cache if a file outside of the current project...

> Agda should allow declarations in inner scopes to shadow declarations in outer scopes I agree.

Can someone summarise the pros and cons of the two approaches? Should one ideally always use one approach, or does it make sense to use different approaches for different things?

Here is a shorter test case: ```agda open import Agda.Builtin.Size data D : (i : Size) → Set where c : (i : Size) → D i → D i...

Do you think you could create a smaller test case? How do you know that Agda does not terminate (given enough time and space)?

Apparently the problem causing #1386 was that Agda treated things as rigid even if they were not, and this was fixed by making the analysis more precise. An alternative might...