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

[Nils Anders Danielsson]

On 2013-05-30 16:54, Andreas Abel wrote:
> I implemented the ideas below to make --without-K less restrictive. Maybe the pendulum has to swing back after this once more.
>
> 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.

Did you also implement a third change related to universe levels?

Without your patch:

   Reconstructed parameters:
     _∷_ (: {a : .Level.Level} {A : Set a} →
            A → List {a} A → List {a} A) << [{.Level.zero}, A] >> [x, xs]

With your patch:

   Reconstructed parameters:
     _∷_ (: {a : .Level.Level} {A : Set a} →
            A → List {a} A → List {a} A) << [] >> [x, xs]

-- 
/NAD