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

[Andrés Sicard-Ramírez]

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.

-- 
Andrés