Less restrictive --without-K [Re: [Agda] no longer type checks]

[Nils Anders Danielsson]

On 2013-05-30 16:54, Andreas Abel wrote:
> 1. Big parameters are now ignored.
>
>     Big are those that are in the same universe than the data type or
>     higher.  Size prevents information to flow from these parameters
>     into the type.
>
> 2. Non-linear parameters are treated just as indices.
>
>    This means that Id1 and Id2 are no longer distinguished in the analysis.

Are you aware that Agda accepts the following definition of equality?

   data _≡_ (A : Set) : Set → Set where
     refl : A ≡ A

Is A ignored (because its type is big), or treated as an index (because
it is mentioned in an index)?

(I think that the definition above should be rejected, at least when
--without-K is used.)

-- 
/NAD