[Agda] Allow cyclic module imports

[Martín Hötzel Escardó]

But of course still check that any cyclic definitions within the cyclic 
modules are well founded.

I don't want to put this as a feature request before we discuss this and 
see the (un)desirable consequences that I haven't seen on my own.

To some extent, breaking anything into modules is arbitrary and depends 
on taste. But, nevertheless, modules are useful to aid understanding 
(and compilation efficiency too).

However, I often find myself creating artificial modules to break module 
import cycles. And I am sure you do to.

Here is a concrete example.

I have four modules UF-Subsingletons*, two modules UF-Equiv*, two 
modules UF-Retracts* because

(1) in order to define equivalence, we need to know what subsingleton 
types are and some properties of them.

(2) in order to prove some properties about subsingletons, we need to 
use some properties of equivalences.

(3) in order to prove some more properties of equivalences, we need to 
prove some more properties of subsingletons.

(4) and then add retracts to the picture, and something analogous to 
(1)-(3) takes place.

My original development was monolitic because of that. In one (big) 
file, you develop things in the mathematical order they are needed.

Then I refactored it into "topics" (as above). But then the same topic 
needed several modules, as explained.

Couldn't we just allow cyclic module imports, provided the total set of 
definitions in all modules are well founded?

There are a number of things to consider:

(1) Is this easy to implement?

(2) Does it have conceptual / software engineering disadvantages?

Looking mathematically at the problem, I see things like this: we have a 
directed acyclic graph of definitions (or replace acyclic by well 
founded). Assigning them to modules amounts to quotienting this graph. 
Such quotients are seldom nice - they hardly ever reflect the structured 
of the unquotiented graph. In particular, in the development I am 
discussing, the module-picture of the development ( 
http://www.cs.bham.ac.uk/~mhe/agda-new/module-graph.pdf) clearly shows 
(to me) that most of the dependencies are artificial when particular 
definitions in particular modules are considered.

Martin