The rules for where blocks of mutually recursive definitions end are unclear and confusing

[lukaszcz]

We should reconsider them. Ideally, we wouldn't have any restrictions, but it seems difficult to implement with the current concept.

[janmasrovira]

currently we separate definitions in two categories:

1. Non-definitions: import, open and local module.
2. Definitions: The rest (type definitions, function definitions, etc.).

The idea behind this categorization is that Non-definitions have imperative-like semantics. I.e. an import or an open statement should only affect definitions that come after it. Whereas a function definition should be able to be forward referenced.

Currently local modules also fall in the Non-definition category, but I don't see a reason why it should be this way. In fact, I think that most confusions would be solved by moving local modules to the Definitions category.

The following example highlights the crux of the issue:

module Example1;

axiom a : Type;

type T :=
  mkT@{
    t : R;
  };

-- POINT A

-- x1 : T -> a := T.t1;

type R :=
  mkR@{
    r : T;
  };

-- POINT B

y1 : R -> a := R.r1;

1. With the x1 definition commented out the example typechecks. The generated local modules for types T and R are put at POINT B, making it possible for the field t : R to forward reference R.
2. However, if we uncomment the x1 definition then it fails to typecheck. The reason is that the generated local module for T is put at POINT A, making it impossible for t : R to reference R.

If we treated local modules as forward-referenceable definitions we wouldn't have this issue.