[Agda] bug in definitions using "_"?

[Ulf Norell]

It looks like this has been fixed. In the development version I get yellow
on all variants of the example.

/ Ulf


On Thu, Dec 19, 2013 at 11:31 AM, Martin Escardo <m.escardo at cs.bham.ac.uk>wrote:

>
> I think this is a bug (found together with Chuangjie Xu). Is it known?
> If not I will report it.
>
> This type checks both with and without K, with Agda 2.3.2.1:
>
> {-# OPTIONS --without-K #-}
>
> module bug where
>
> data _≡_ {X : Set} : X → X → Set where
>  refl : {x : X} → x ≡ x
>
> transport : {X : Set}{P : X → Set}{x₀ x₁ : X} → x₀ ≡ x₁ → P x₀ → P x₁
> transport refl p = p
>
> proposition :
>       {X Y : Set}
>       {P : X → Set}
>       (f : (x : X) → P x → Y)
>       (g : (x : X) → (p q : P x) → f x p ≡ f x q)
>       (x₀ x₁ : X)
>       (p₀ : P x₀)
>       (p₁ : P x₁)
>       (r : x₀ ≡ x₁)
>     →
>        f x₀ p₀ ≡ f x₁ p₁
> proposition {X} f g x₀ x₁ p₀ p₁ r
>     = transport {X} {λ x → f x₀ p₀ ≡ f x _} r (g x₀ p₀ _)
>
> The problem is that the underscores cannot really be filled with
> any proof. The given proof is wrong (but the proposition does have a
> proof, although this is not important here).
>
> The first underscore has type P x. But how are you going to find
> something in P x for an arbitrary given x : X?
>
> The second one has type P x₀. However, you can't plug p₀ or a
> transported version of p₁.
>
> This bug should be easy to fix, because if we instead do the
> following, then we get "yellow" unsolved metas rather than a
> type-checked proof of the proposition:
>
> module not-bug where
>
> data _≡_ {X : Set} : X → X → Set where
>  refl : {x : X} → x ≡ x
>
> transport : {X : Set}{P : X → Set}{x₀ x₁ : X} → x₀ ≡ x₁ → P x₀ → P x₁
> transport refl p = p
>
> postulate
>  X Y : Set
>  P : X → Set
>  f : (x : X) → P x → Y
>  g : (x : X) → (p q : P x) → f x p ≡ f x q
>  x₀ x₁ : X
>  p₀ : P x₀
>  p₁ : P x₁
>  r : x₀ ≡ x₁
>
> proposition : f x₀ p₀ ≡ f x₁ p₁ -- get yellow here:
> proposition = transport {X} {λ x → f x₀ p₀ ≡ f x _} r (g x₀ p₀ _)
>
> However, notice that the following type checks:
>
> module still-bug where
>
> data _≡_ {X : Set} : X → X → Set where
>  refl : {x : X} → x ≡ x
>
> transport : {X : Set}{P : X → Set}{x₀ x₁ : X} → x₀ ≡ x₁ → P x₀ → P x₁
> transport refl p = p
>
> module hypotheses
>       (X Y : Set)
>       (P : X → Set)
>       (f : (x : X) → P x → Y)
>       (g : (x : X) → (p q : P x) → f x p ≡ f x q)
>       (x₀ x₁ : X)
>       (p₀ : P x₀)
>       (p₁ : P x₁)
>       (r : x₀ ≡ x₁)
>  where
>   proposition : f x₀ p₀ ≡ f x₁ p₁ -- this type checks:
>   proposition = transport {X} {λ x → f x₀ p₀ ≡ f x _} r (g x₀ p₀ _)
>
> Martin
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20131219/268e0a4e/attachment-0001.html