Allow modules to be extended

[lukaszcz]

The proposal is to allow declaring a module with an already used name with the effect of extending the module in the current scope.

For example,

module A;
  f : Nat -> Nat := ...;
end;

h : Nat -> Nat;

module A;
  g : Nat -> Nat := ...;
end;

should be equivalent to

h : Nat -> Nat;

module A;
  f : Nat -> Nat := ...;
  g : Nat -> Nat := ...;
end;

Perhaps the extension should be marked explicitly, to avoid an unintended extension.

extend module A;
  g : Nat -> Nat := ...;
end;

The motivation and use-case for this comes up when actually trying to use the import M as N public syntax. An example is the module Stdlib.Data.Nat:

module Stdlib.Data.Nat;

import Juvix.Builtin.V1.Nat open public;
import Stdlib.Data.Nat.Base open hiding {+; *; div; mod} public;
-- should be re-exported qualified
import Stdlib.Data.Nat.Base as Nat;
-- should be re-exported qualified
import Stdlib.Data.Nat.Ord as Nat;

We would like to put public after as Nat for both modules, but we can't because of name conflict. We can't even do it for one, because there is already a module Nat associated with the inductive type.

More seriously, it doesn't seem we can even get the desired behaviour "manually" by declaring appropriate modules.

Question: what to do with different extensions of the same module imported via different paths? Maybe just merge them.

[janmasrovira]

As discussed, another option is to not desugar public imports into local modules and instead add some special handling in the scoper, similar to non-public imports with alias (import A as B).