[Agda] bug in definitions using "_"?

[Martin Escardo]

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