Regression related to fix of #3027

[nad]

The following code is accepted by Agda 2.6.0.1, but rejected by a recent development version:

comp :
  (A : Set)
  (B : A → Set)
  (C : (x : A) → B x → Set) →
  ((x : A) (y : B x) → C x y) →
  (g : (x : A) → B x) →
  ((x : A) → C x (g x))
comp _ _ _ f g x = f x (g x)

data Unit : Set where
  unit : Unit

P : Unit → Set
P unit = Unit

Q : Unit → Set → Set
Q unit = λ _ → Unit

f : (x : Unit) → P x → P x
f unit x = x

g :
  (A : Set) →
  ((x : Unit) → Q x A → P x) →
  ((x : Unit) → Q x A → P x)
g A h x = comp _ _ _ (λ _ → f _) (h _)

Bisection points towards 3c6482b ("[ fix #3027 ] block bound variable on right side of constraint (#4392)"). @vlopezj, you might want to take a look at this.

[vlopezj]

Thanks for finding this example! For the record, this is the error message I get when I typecheck it
(Issue4408.agda)

Failed to solve the following constraints:
  _x_26 (A = A) (h = h) (x = x) (x = x₁) = x : Unit
  Q x A =< Q _x_27 A
  P _x_27 =< P (_x_26 (A = A) (h = h) (x = x) (x = x₁))
Unsolved metas at the following locations:
  .../Issue4408.agda:28,32-33
  .../Issue4408.agda:28,38-39
  .../Issue4408.agda:28,36-39
  .../Issue4408.agda:28,11-40

I don't know what the (A = A), (h = h) (x = x) (x = x₁) are… (perhaps blocked terms?).
I will mention this to @UlfNorell tomorrow to see how this could be fixed.
(FWIW, Tog⁺ seems to deal with the example just fine).

[jespercockx]

The (A = A) etc denote the arguments to the metavariable, i.e. how to instantiate the variables from the context where the metavariable was created. They are usually not shown when it is the identity substitution, but here I think the pretty-printer gets confused by the fact that there are two variables named x in scope of the metavariable.

[vlopezj]

I see...
But then I'm very surprised… "_x_26 A h x x₁ = x : Unit" lies squarely in the pattern fragment.
If any of A, h, x and x₁ were blocked terms on some constraint, would this be visible when pretty printing?

[jespercockx]

Internally, the constraint is _x_26 (A = A) (h = h) (x = x) (x = (_31 (A = h) (h = x) (x = x₁))) = x : Unit, so the term that is printed as x₁ is actually a metavariable _31 is a blocked term that is to be instantiated to x₁ once a different problem is solved. Looking a bit further at the debug output, the instantiation of _31 to λ A h x → x is blocked on Q x A =< Q _x_27 A. So that one is the real reason why the constraints are unsolved.

There also seems to be something wrong in the arguments of the metavariable _31, I'm not sure if it's just the printing that's broken or if the indices are actually off by 1.

[nad]

Here is another regression that seems to have been caused by the same commit:

open import Agda.Builtin.Equality
open import Agda.Builtin.Sigma
open import Agda.Primitive

id : ∀ {a} {A : Set a} → A → A
id x = x

_∘_ : ∀ {a b c}
        {A : Set a} {B : A → Set b} {C : {x : A} → B x → Set c} →
      (∀ {x} (y : B x) → C y) → (g : (x : A) → B x) →
      ((x : A) → C (g x))
f ∘ g = λ x → f (g x)

infix 0 _↔_

record _↔_ {f t} (From : Set f) (To : Set t) : Set (f ⊔ t) where
  field
    to               : From → To
    from             : To → From
    right-inverse-of : ∀ x → to (from x) ≡ x
    left-inverse-of  : ∀ x → from (to x) ≡ x

infixr 1 _⊎_

data _⊎_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
  inj₁ : (x : A) → A ⊎ B
  inj₂ : (y : B) → A ⊎ B

[_,_] : ∀ {a b c} {A : Set a} {B : Set b} {C : A ⊎ B → Set c} →
        ((x : A) → C (inj₁ x)) → ((x : B) → C (inj₂ x)) →
        ((x : A ⊎ B) → C x)
[ f , g ] (inj₁ x) = f x
[ f , g ] (inj₂ y) = g y

Σ-map : ∀ {a b p q}
          {A : Set a} {B : Set b} {P : A → Set p} {Q : B → Set q} →
        (f : A → B) → (∀ {x} → P x → Q (f x)) →
        Σ A P → Σ B Q
Σ-map f g = λ p → (f (fst p) , g (snd p))

∃-⊎-distrib-right :
  ∀ {a b c} {A : Set a} {B : Set b} {C : A ⊎ B → Set c} →
  Σ (A ⊎ B) C ↔ Σ A (C ∘ inj₁) ⊎ Σ B (C ∘ inj₂)
∃-⊎-distrib-right {A = A} {B} {C} = record
  { to               = to
  ; from             = from
  ; right-inverse-of = [ (λ _ → refl) , (λ _ → refl) ]
  ; left-inverse-of  = from∘to
  }
  where
  to : Σ (A ⊎ B) C → Σ A (C ∘ inj₁) ⊎ Σ B (C ∘ inj₂)
  to (inj₁ x , y) = inj₁ (x , y)
  to (inj₂ x , y) = inj₂ (x , y)

  from = [ Σ-map inj₁ id , Σ-map inj₂ id ]

  from∘to : ∀ p → from (to p) ≡ p
  from∘to (inj₁ x , y) = refl
  from∘to (inj₂ x , y) = refl

[andreasabel]

Maybe the problem is that addContext comes only after the reference to var 0, see the comment at 3c6482b#r37034059 ?