[Agda] without-K problem

[Nils Anders Danielsson]

On 2012-06-20 14:00, Andreas Abel wrote:
> 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:

>>>> 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, the problem is that constructors are not applied to their
parameters. We can fix the problem in several ways:

* Don't allow any constructors: force the indices to be distinct
   variables that are not free in the parameters. I tried this once, and
   found it rather crippling.

* Only allow constructors from parameter-free data types (natural
   numbers but not lists). This is easy to implement, but also quite
   annoying.

* Reconstruct the parameters when applying the check. This sounds like
   the way to go. Is there some kind of parameter-reconstructing function
   somewhere in the code base?

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

I don't.

-- 
/NAD