Internal error with generalized variable in definition inside record

[szumixie]

I get an internal error with the following code:

postulate
  P : (A : Set) → A → Set
  F : Set → Set
  g : (A : Set) → F A

variable A : Set

record R : Set₁ where
  h : A → P ? (g ?)
  h = ?

  field B : Set

conApp: constructor Temp.R..mkGeneralizeTel with fields
  Temp.R..generalizedField-A
 and args
  {@0}
 projected by Temp..generalizedField-A
An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE__, called at src/full/Agda/TypeChecking/Substitute.hs:145:33 in Agda-2.9.0-9us0L8SqiHiLjIfhQSrY07:Agda.TypeChecking.Substitute

If I fill in the first hole, then I get a nonsensical error:

  h : A → P (F A) (g ?)

error: [UnequalTerms]
A != A
(although these terms are looking the same, they contain different
 but identically rendered identifiers somewhere)
when checking that the expression g ? has type F A

If I replace the holes with underscores, then the errors disappear.

[andreasabel]

The root of the problem is how we type-check records (#434), and a similar issue was #5478:

• #434
• #5478

Let's follow along with this slightly modified version of the OP, where I renamed the generalized variable to G:

{-# OPTIONS --show-implicit #-}
{-# OPTIONS -v tc.generalize:10 #-}
{-# OPTIONS -v tc.rec:40 #-}
{-# OPTIONS -v tc.interaction:30 #-}

postulate
  P : (A : Set) → A → Set
  F : Set → Set
  g : (A : Set) → F A

variable G : Set

record R : Set₁ where
  h : G → P ? (g ?)
  h = {!!}

  field B : Set

The problem is that Agda has already allocated the metas for the ?s during construction of the record constructor. This triggered already a generalization even though the final constructor type (Set -> R) does not mention any generalized variables.

checking record def R
  ps = []
  contel = (let h : G → P ? (g ?)
                h = ?)
           (B : Set) →
           Set
  fields = mutual
             syntax h ...
             postulate h : G → P ? (g ?)
             h = ?
           syntax B ...
checking fields
Found interaction point ConcreteDef ?0 : Set
Found interaction point ConcreteDef ?1 : Set
computing generalization for type _3
we're generalizing over _G_4

We then insert the record "self" variable r to check the declarations in the record (a second time, first time was during construction of the constructor):

record section: R (r : R) [], [Issue8182.R.B]
  field tel = (B : Set)

We encounter the interaction points a second time, triggering a heuristics that tries to reuse the meta we created for them the first time:

Found interaction point ConcreteDef ?0 : Set
reusing meta
  creation context: [(genTel : Issue8182..GeneralizeTel)]
  reusage  context: [(genTel : _11 (r = genTel)), (r : R)]

This goes well for ?0 because they share the context [genTel].

meta reuse arguments: [genTel]

It does not go well for ?1 though:

Found interaction point ConcreteDef ?1 : Set
reusing meta
  creation context: [{G : Set}]
  reusage  context: [(genTel : _11 (r = genTel)), (r : R)]

Here we strangely have [G] as original context and not [genTel]. I don't know why this is so, looks like a problem with generalization. Things go awry. Agda does not recognize G and thinks it must be a record field. Subsequently it produces garbage meta reuse arguments, leading to an internal error.

What I did for now (#8185) is another sanity check that checks the validity of supposed fields by their concrete name. This mismatch will now trigger an internal error in a more suitable place.

  fs    = [(Issue8182.R.B)]
  gfs   = [G]

However, to fix the issue one would have to understand why we see G instead of genTel for ?1. Also, the "meta reuse heuristics" is a terrible hack I wish we did not need in the first place, so the proper fix would be to rewrite the scope and type checker for record declarations (as outlined in #434).