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

[Andreas Abel]

True.  It certainly has no need for K.

Q: Would it also check (without my patch) and this definition of equality?

data _≡_ {A : Set} : A → A → Set where
   refl : ∀ {a} → a ≡ a

Or would it check if you wrote zero == bla instead of bla == zero?

If the answer to either of these questions is yes, then I have screwed 
something up (not unlikely).  If the answer is no, then the original 
criterion was screwed up already, since it treated the two sides of 
equality differently.

Cheers,
Andreas

On 30.05.13 6:12 PM, Andrés Sicard-Ramírez wrote:
> On 30 May 2013 09:54, Andreas Abel <andreas.abel at ifi.lmu.de> 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.
>>
>
> Before your patch this proof was accepted using the --without-K option:
>
> open import Data.Nat
> open import Data.Sum
> open import Relation.Binary.PropositionalEquality
>
> foo : ∀ m n → m * n ≡ zero → m ≡ zero ⊎ n ≡ zero
> foo zero     n      h = inj₁ refl
> foo (suc m) zero    h = inj₂ refl
> foo (suc m) (suc n) ()
>
> After your patch the proof is rejected:
>
> The indices
>    suc (n₁ + m₁ * suc n₁)
>    0
> are not constructors (or literals) applied to variables (note that
> parameters count as constructor arguments)
> when checking that the clause foo (suc m) (suc n) () has type
> (m n : ℕ) → m * n ≡ zero → m ≡ zero ⊎ n ≡ zero
>
> I don't think it is an expected behavior.
>

-- 
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/