[Agda] Allow cyclic module imports

[Nils Anders Danielsson]

On 2018-04-26 10:36, Martin Escardo wrote:
> In my example, I have a sets A, B, C of code for certain mathematical
> concepts a,b,c. At the moment, I have to break things e,g. in modules
> A1-A3, B1-B3, C1-C2
> 
>      A1
>          B1
>              C1
>          B2
>      A2
>              C2
>      A3
>          B3
> 
> where the modules in each line depend on the modules in the previous
> lines. I would rather have only three modules A=A1+A2+A3, B=B1+B2+B3,
> and C=C1+C2, each of them cyclically importing each other, but Agda
> figuring out that there is no real cyclic dependency.

What about instances? Consider the following code:

   data D : Set where
     d₁ d₂ : D

   abstract
     instance
       x : D
       x = d₁

   f : ⦃ _ : D ⦄ → D
   f ⦃ y ⦄ = y

   z : D
   z = f

Here we have a dependency from z to x. However, one cannot see this
simply by analysing the symbols occurring in the source code. Should the
following code be accepted?

   data D : Set where
     d₁ d₂ : D

   f : ⦃ _ : D ⦄ → D
   f ⦃ y ⦄ = y

   z : D
   z = f

   abstract
     instance
       x : D
       x = d₁

-- 
/NAD