[Agda] Allow cyclic module imports

[Nils Anders Danielsson]

On 2018-04-25 22:01, Martín Hötzel Escardó wrote:
> There are a number of things to consider:
> 
> (1) Is this easy to implement?
> 
> (2) Does it have conceptual / software engineering disadvantages?

I'm not quite sure what you are proposing. Is the idea to treat
everything in a module cycle as one big mutual block? Or is the idea to
still require mutual blocks for things that are mutually recursive, but
sort the mutual blocks topologically? In the latter case, should this
sorting be done after meta-variables have been resolved (in which case I
wonder how they are resolved), or based only on what the user has
written in the code? And how should independent definitions be ordered?
Or should the signature be modified so that it is no longer a list (of
mutual blocks), but some kind of DAG?

-- 
/NAD