Confusing error from trying to use memory restrictions on module types

[oskgo]

The following example emits an unknown symbol error, which seems to be caused by the use of {-F}, but doesn't appear until much later:

module type Foo = {}.

module type Bar(F: Foo) {-F} = {
}.

module (Baz: Bar) (F: Foo) = {}.

[strub]

Not sure whether we want to accept this or not.

[fdupress]

It would be neat to allow restrictions to be part of the module type. But we then need to allow them at all layers of the type. For a functor type, for example:

module type F {-M} (O : T) = {}.

is not the same as

module type F (O : T) {-M} = {}.

This may be more complex than we'd really like to make the module system at present?

[alleystoughton]

And * (initialization) was moved out of the module declarations and into (well it was always in) the logic.

[oskgo]

Personally I think it only makes sense to accept it if we also have implied bounds on lemmas. If not then we just have to repeat ourselves anyways.

If might seem like allowing these bounds would statically prevent some errors in definitions or statements, but I think in practice it won't because forgetting the bounds only makes the adversary more capable, which is fine.