[Agda] without-K problem

[Andreas Abel]

On 20.06.2012 12:32, Altenkirch Thorsten wrote:
> On 20/06/2012 08:39, "Andreas Abel"<andreas.abel at ifi.lmu.de>  wrote:
>> 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.
> 
> Yes, and this is what it says in the specification of without-K
> http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Version-2-2-10
> (I checked this with Nisse yesterday).

Aeh, I cannot find it in the specification in the release notes (where
the link points to).  I tried hard, but it only says stuff about
*pattern matching* and about the split type

  D pars ixs

As far as I can tell, the implementation
(Agda.TypeChecking.Rules.LHS.Split.wellformedIndices) matches the
specification.
Which does not say anything about restrictions on data type *definitions*.

(That Nisse uses Guillaumes version of equality of course hints that he
finds the std-lib definition is problematic...)

> Hence this seems to be a bug in the implementation only.

Rather that the specification (and hence, implementation) is incomplete?!

Cheers,
Andreas

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