Less restrictive --without-K [Re: [Agda] no longer type checks]
Nils Anders Danielsson
nad at cse.gu.se
Tue Jun 4 10:52:20 CEST 2013
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.)
More information about the Agda