<div dir="ltr">It looks like this has been fixed. In the development version I get yellow on all variants of the example.<div><br></div><div>/ Ulf</div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Thu, Dec 19, 2013 at 11:31 AM, Martin Escardo <span dir="ltr">&lt;<a href="mailto:m.escardo@cs.bham.ac.uk" target="_blank">m.escardo@cs.bham.ac.uk</a>&gt;</span> wrote:<br>

<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><br>
I think this is a bug (found together with Chuangjie Xu). Is it known?<br>
If not I will report it.<br>
<br>
This type checks both with and without K, with Agda <a href="http://2.3.2.1" target="_blank">2.3.2.1</a>:<br>
<br>
{-# OPTIONS --without-K #-}<br>
<br>
module bug where<br>
<br>
data _≡_ {X : Set} : X → X → Set where<br>
 refl : {x : X} → x ≡ x<br>
<br>
transport : {X : Set}{P : X → Set}{x₀ x₁ : X} → x₀ ≡ x₁ → P x₀ → P x₁<br>
transport refl p = p<br>
<br>
proposition :<br>
      {X Y : Set}<br>
      {P : X → Set}<br>
      (f : (x : X) → P x → Y)<br>
      (g : (x : X) → (p q : P x) → f x p ≡ f x q)<br>
      (x₀ x₁ : X)<br>
      (p₀ : P x₀)<br>
      (p₁ : P x₁)<br>
      (r : x₀ ≡ x₁)<br>
    →<br>
       f x₀ p₀ ≡ f x₁ p₁<br>
proposition {X} f g x₀ x₁ p₀ p₁ r<br>
    = transport {X} {λ x → f x₀ p₀ ≡ f x _} r (g x₀ p₀ _)<br>
<br>
The problem is that the underscores cannot really be filled with<br>
any proof. The given proof is wrong (but the proposition does have a<br>
proof, although this is not important here).<br>
<br>
The first underscore has type P x. But how are you going to find<br>
something in P x for an arbitrary given x : X?<br>
<br>
The second one has type P x₀. However, you can&#39;t plug p₀ or a<br>
transported version of p₁.<br>
<br>
This bug should be easy to fix, because if we instead do the<br>
following, then we get &quot;yellow&quot; unsolved metas rather than a<br>
type-checked proof of the proposition:<br>
<br>
module not-bug where<br>
<br>
data _≡_ {X : Set} : X → X → Set where<br>
 refl : {x : X} → x ≡ x<br>
<br>
transport : {X : Set}{P : X → Set}{x₀ x₁ : X} → x₀ ≡ x₁ → P x₀ → P x₁<br>
transport refl p = p<br>
<br>
postulate<br>
 X Y : Set<br>
 P : X → Set<br>
 f : (x : X) → P x → Y<br>
 g : (x : X) → (p q : P x) → f x p ≡ f x q<br>
 x₀ x₁ : X<br>
 p₀ : P x₀<br>
 p₁ : P x₁<br>
 r : x₀ ≡ x₁<br>
<br>
proposition : f x₀ p₀ ≡ f x₁ p₁ -- get yellow here:<br>
proposition = transport {X} {λ x → f x₀ p₀ ≡ f x _} r (g x₀ p₀ _)<br>
<br>
However, notice that the following type checks:<br>
<br>
module still-bug where<br>
<br>
data _≡_ {X : Set} : X → X → Set where<br>
 refl : {x : X} → x ≡ x<br>
<br>
transport : {X : Set}{P : X → Set}{x₀ x₁ : X} → x₀ ≡ x₁ → P x₀ → P x₁<br>
transport refl p = p<br>
<br>
module hypotheses<br>
      (X Y : Set)<br>
      (P : X → Set)<br>
      (f : (x : X) → P x → Y)<br>
      (g : (x : X) → (p q : P x) → f x p ≡ f x q)<br>
      (x₀ x₁ : X)<br>
      (p₀ : P x₀)<br>
      (p₁ : P x₁)<br>
      (r : x₀ ≡ x₁)<br>
 where<br>
  proposition : f x₀ p₀ ≡ f x₁ p₁ -- this type checks:<br>
  proposition = transport {X} {λ x → f x₀ p₀ ≡ f x _} r (g x₀ p₀ _)<br>
<br>
Martin<br>
<br>
<br>
______________________________<u></u>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><br>
</blockquote></div><br></div>