[Agda] without-K problem
Andreas Abel
andreas.abel at ifi.lmu.de
Wed Jun 20 14:00:48 CEST 2012
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/
More information about the Agda
mailing list