[Agda] Level constraints

[Wolfram Kahl]

On Thu, Nov 14, 2013 at 07:53:29PM +0000, Martin Escardo wrote:
> There is one more option, which I favour: Feferman's "typical 
> ambiguity", with Harper's algorithm or similar.
> 
> The idea is that you just write "Set", perhaps many times in the same 
> definition, and then Agda adds (different) indices as appropriate. This 
> feels like working with type-in-type, but it is actually working with 
> what we already have, with the difference that the universe levels are 
> inferred rather than written down.
> 
> Moreover, it should be possible to be compatible with what we already 
> have (perhaps writing e.g. Set_0 rather than Set if that's what you 
> really mean). So, if you put levels i,j,k in your context and write 
> Set_i, Set_{i \sqcup j}, etc. then it would work as it does now, but if 
> you write Set in several places in the same definition, then it would 
> invoke the typical ambiguity conventions and algorithm to fill in the 
> missing indices and the missing indices. This should make things much 
> easier, very much in the spirit of implicit arguments.

Some of this can of course already be had by just writing ``Set _'',
as it occurs quite frequently in the standard library.
(I must admit that I do it rarely --- although I do have a definition
 that takes over 30 (implicit) Level parameters.)

Making the underlying metavariable instantiation even more intelligent
would expand the opportunities for writing ``Set _''
without any change to the language ---
perhaps that could be one avenue for experimentation...


Wolfram