In record declarations, meta variables are messed up

[andreasabel]

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

record _×_ (A B : Set) : Set where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B
open _×_

postulate A : Set

mutual
  record R : Set where

    foo : A → A
    foo = λ x → {!!}

    field bar : A  -- with this field, the meta is not longer solved

    inst : ∀ (p : A × A) → foo (proj₁ p) ≡ proj₁ p
    inst p = refl

Without the field, the meta is solved by ?0 := x. When the field is present, the internal representation of the meta seems to be messed up such that the expandProjectedVar magic no longer works.

  _21 := λ p → refl [blocked on problem 29]
  [29, 32] ?0 (proj₁ p) = proj₁ p : A

This issue should be fixed along with #2500.
Also, the fix for #707 does not do the correct thing for this example (see #2257). However, even if we replace the interaction meta by an underscore, it is not solved in the presence of the field.

[UlfNorell]

Some observations:

Adding another field makes it fail even harder:

record R : Set where

  foo : A → A
  foo = λ x → {!!}

  field bar : A  -- with this field, the meta is not longer solved

  inst : ∀ (p : A × A) → foo (proj₁ p) ≡ proj₁ p
  inst p = refl  -- (proj₁ p) != proj₁ p of type A

  field boo : A

But the corresponding field telescope checks without problems:

no-record : (let foo : A → A; foo = λ x → {!!}) (bar : A)
            (let inst : (p : A × A) → (proj₁ p) ≡ proj₁ p
                 inst = λ p → refl) (boo : A) → A
no-record bar boo = boo

[jespercockx]

This is part of a set of related issues with record types that require a major overhaul of how we handle definitions inside a record module. Attempting a quick fix would likely be a waste of time, so I'm bumping this to the next milestone.