Qualified constructors

[janmasrovira]

Consider this issue an unfinished draft.

• It has been brought up in https://github.com/anoma/juvix/issues/2074, that it would be useful to have the option to refer to constructors by their type. E.g. List.nil, Maybe.nothing, etc.

I see two approaches:

1. Add special rules to the scoper.
2. Implicitly declare a local module after each type definition. (Agda's approach). For instance the implicit module defined for the List type would be:

module List;
  nil : {A : Type} -> List A;
  nil := nil (the constructor); 

  :: :  {A : Type} -> List A;
  :: h hs := h :: (the constructor) hs; 
end;

Now, this module would still require some special rules (I assume #2110). See the following example:

module Example;
module M;
  type Unit := unit : Unit;
end;

-- we can import Unit as a normal module (nothing special)
open M using {module Unit};

u1 : M.Unit;
u1 := Unit.unit;

-- Special rule: If the type is brought into scope, the associated module needs
-- to be brought into scope with the same name. 
open M using {Unit as Unit2};

u2 : Unit2;
u2 := Unit2.unit;

open Unit2;
open M;

-- Special rule: This should not cause an ambiguity error. 
-- Note that `unit` could refer to both the constructor and the 
-- auxilliary function defined in the implicit module.
u3 : Unit2;
u3 := unit;

Some of the advantages of the implicit module approach is that it plays more nicely with module features. (TODO explain)