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

[Andreas Abel]

On 04.06.2013 10:52, Nils Anders Danielsson wrote:
> 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)?

It is treated as index.  I will clarify the release notes.

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

Yes, we have to be careful about big indices.  At least they cannot be 
explained by equality proofs embedded in the constructors (unless we 
allow equality between big things to be small, which is most certainly a 
bad idea).  However, they could be explained by unification.

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/