[Agda] --without-K option too restrictive?

[Andreas Abel]

The error comes from universe polymorphism: Agda complains about 
Level.zero not being pattern, although Level.zero is only visible in the 
debug printing -v tc.lhs.split.well-formed:20.

I don't think that levels should keep one from matching on refl here. 
--without-K seems overly strict here.

If I remove universe polymorphism by hand (see attached file), I see a 
different error:

The variables
   A
which are used (perhaps as constructor parameters) in the index
expressions
   x ∷ xs
are free in the parameters
   {List A}
   ys
when checking that the pattern refl has type
_≡_ {List A} ys (x ∷ xs)

This one is more comprehensible.  However, still --without-K is too 
restrictive.

Have not we discussed this before?  I am having a dejavu here, but 
cannot find traces of this discussion in my email archive.

Cheers,
Andreas

On 29.05.13 10:23 PM, Andreas Abel wrote:
> The error message is confusing:
>
> The indices
>    x ∷ xs
> are not constructors (or literals) applied to variables (note that
> parameters count as constructor arguments)
>
> First, it uses plural for a single index (I am changing this right now).
>   Further, it is not a true statement, because x :: xs  _is_ a
> constructor applied to variables.  Whatever it wants to tell me, I do
> not get it.
>
> On 29.05.13 8:59 PM, Nils Anders Danielsson wrote:
>> On 2013-05-29 17:26, Andrés Sicard-Ramírez wrote:
>>> Why the --without-K option rejects the following proof
>>>
>>> foo : {A : Set}(xs ys : List A) → P xs ys → Q xs ys
>>> foo xs .(x ∷ xs) (x , refl) = helper x xs
>>>
>>> if I can prove foo using only subst
>>>
>>> foo' : {A : Set}(xs ys : List A) → P xs ys → Q xs ys
>>> foo' xs ys (x , h) =
>>>    subst (λ ys' → length xs < length ys') (sym h) (helper x xs)
>>>
>>> ?
>>
>> The --without-K flag is documented in the release notes of Agda 2.3.2:
>>
>>
>> http://wiki.portal.chalmers.se/agda/uploads/Main.Download/release-notes-2-3-2.txt
>>
>>
>>
>

-- 
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/
-------------- next part --------------
{-# OPTIONS --without-K --show-implicit #-}
{-# OPTIONS -v tc.lhs.split.well-formed:100 #-}
-- Andres Sicard, 2013-05-29
module WithoutKRestrictiveNoUniPoly where

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

data _≤_ : ℕ → ℕ → Set where
  z≤n : ∀ {n} → zero ≤ n
  s≤s : ∀ {n m} → n ≤ m → suc n ≤ suc m

_<_ : ℕ → ℕ → Set
n < m = suc n ≤ m

refl≤ : ∀ (n : ℕ) → n ≤ n
refl≤ zero    = z≤n
refl≤ (suc n) = s≤s (refl≤ n)

data List (A : Set) : Set where
  []  : List A
  _∷_ : (x : A) (xs : List A) → List A

length : {A : Set} → List A → ℕ
length []       = zero
length (x ∷ xs) = suc (length xs)

record Σ (A : Set) (B : A → Set) : Set where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B proj₁

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

subst : {A : Set}(P : A → Set){a b : A} → a ≡ b → P a → P b
subst P refl x = x

sym : {A : Set}{a b : A} → a ≡ b → b ≡ a
sym refl = refl

P : {A : Set} → List A → List A → Set
P xs ys = Σ _ (λ x → ys ≡ (x ∷ xs))

Q : {A : Set} → List A → List A → Set
Q xs ys = (length xs) < (length ys)

helper : {A : Set}(y : A)(xs : List A) → (length xs) < (length (y ∷ xs))
helper y []       = s≤s z≤n
helper y (x ∷ xs) = s≤s (refl≤ _)

-- Why the --without-K option rejects the following proof

foo : {A : Set}(xs ys : List A) → P xs ys → Q xs ys
foo xs .(x ∷ xs) (x , refl) = helper x xs

-- if I can prove foo using only subst

foo' : {A : Set}(xs ys : List A) → P xs ys → Q xs ys
foo' xs ys (x , h) =
  subst (λ ys' → length xs < length ys') (sym h) (helper x xs)