Less restrictive --without-K [Re: [Agda] no longer type checks]
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:
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