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

Andrés Sicard-Ramírez andres.sicard.ramirez at gmail.com
Thu May 30 18:12:14 CEST 2013

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₁)
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.


More information about the Agda mailing list