[Agda] bug in definitions using "_"?
Martin Escardo
m.escardo at cs.bham.ac.uk
Thu Dec 19 11:31:47 CET 2013
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
More information about the Agda
mailing list