Opaque by default (aka abstract by default)

[fmease]

Make all bindings opaque (formerly abstract) by default. In case of data declarations, restrict access to constructors to the module the type is defined in. In case of function declarations, make the binding irreducible/neutral for type-level evaluation/normalization/computation. Make bindings transparent (the opposite of opaque) with the attribute @transparent (alternative name floating around: @open (but what would its antonym and its hypernym be?)).
Nomenclature: Data type and function bindings are associated with a transparency: They are either opaque or transparent.

Intuitively, @public means making the type of a binding accessible to other modules and @public @transparent means making (the type and) the definition (constructors or expression) accessible to other modules.

Further, the type of @public bindings is not allowed to contain private bindings and the definition (the constructors or the expression) of @public @transparent bindings is not allowed to contain private or @public opaque bindings.

It should be an error to specify @transparent without @public (I think).

This is basically a copy of public in Idris (via):

• Lushui: @public, Idris: export
• Lushui: @public @transparent, Idris: public export

Implementation Steps

• Remove @abstract
• Add @transparent and implement constructor-hiding in the name resolver
• Implement opaques-are-neutrals in the type checker

Open questions

• Should @transparent be called @open?
• Should we support restricted transparency e.g. @public @(transparent topmost)?