[Agda] Why is propositional equality "Set a" instead of just Set?

[Jonathan Leivent]

On 08/17/2013 11:56 PM, Wolfram Kahl wrote:
> ...
> I have a module |Relation.Binary.PropositionalEquality.Generalised| containing:
>
> ----------------------------------------------------------------------------
> We define a fully |Level|-polymorphic variant of propositional equality
> in order to be able to define fully |Level|-polymorphic identity relations.
> (Thorsten Altenkirch%
> \footnote{at AIM XIII, April 2011}
>   and others
>   have expressed reservations whether such a definition
>   at levels |k| lower than |a| should be legal.)
>
> \begin{code}
>    data _≡≡_  {k a : Level} {A : Set a} (x : A) : A → Set k where
>      ≡≡-refl : x ≡≡ x
> \end{code}
> ----------------------------------------------------------------------------
>
> Because of those comments, I use it only in isolated contexts,
> because one day somebody might come along and prove that I am using an
> unsafe feature of Agda, which might then get removed...
>
>
> Wolfram
>

I didn't expect a controversial aspect of type theory to turn up in such 
a ubiquitous case.  I was just basing my level assignments on the 
constraints that the type checker finds.

Is there some expectation as to what legal behavior Agda would 
eventually adopt?  Would every definition have to have a level at least 
as high as all of its parameters/indexes?

-- Jonathan