[Agda] without-K problem

[Andreas Abel]

On 18.06.12 9:18 PM, Guillaume Brunerie wrote:
> Hi all,
>
> For what it’s worth, I cannot reproduce the bug using the following
> definition of the identity types:
>
> data _≡_ {A : Set} : A → A → Set where
>    refl : {x : A} → x ≡ x
>
> But I can reproduce it using the following definition (which is the one
> used in the standard library):
>
> data _≡_ {A : Set} (x : A) : A → Set where
>    refl : x ≡ x

Yes, it seems --without-K should also forbid data definitions where a 
parameter variable ("x") is free in a index position.

Otherwise, index variables can be "hidden" in parameter positions and 
are not spotted by --without-K when it checks whether a split is legal.

But then, of course, --without-K is no longer a local check and 
--without-K modules may only import --without-K modules.

Cheers,
Andreas

> 2012/6/18 Altenkirch Thorsten <psztxa at exmail.nottingham.ac.uk
> <mailto:psztxa at exmail.nottingham.ac.uk>>
>
>     Hi Nisse,
>
>     I noticed that a weak version of K is provable even though the
>     without-K flag is set:
>
>     {-# OPTIONS --without-K #-}
>     module K-bug where
>
>     open import Relation.Binary.PropositionalEquality
>
>     weakK : {A : Set}{a b : A}(p q : a ≡ b)(α β : p ≡ q) → α ≡ β
>     weakK refl .refl refl refl = refl
>
>     This would imply that all types have dimension of at most 3. I don't
>     think it is provable with J.
>
>     A simpler term which is provable but shouldn't was found by my
>     student Nicolai:
>
>     weak2 : {A : Set} {a : A} (α : refl {x = a} ≡ refl) → α ≡ refl
>     weak2 refl = refl
>
>     It seems to me that these patterns satisfy the specification of
>     without-K (I.e. the condition is too weak).
>
>     Do you see a fix?
>
>     Cheers,
>     Thorsten
>

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