Open goal inside record causes internal error (eta-contraction)

[mr-ohman]

The following code produces an internal error:

open import Agda.Builtin.Sigma

record R1 (A : Set) : Set where

instance
  prodR1 : {A : Set} {B : A → Set} → ⦃ {a : A} → R1 (B a) ⦄ → R1 (Σ A B)
  prodR1 = record {}

record R2 (A : Set) ⦃ aR1 : R1 A ⦄ : Set₁ where
  field
    f : A → Set
open R2 ⦃...⦄ public

record R3 (A : Set) (B : A → Set) : Set₁ where
  instance
    bR1 : {a : A} → R1 (B a)
    bR1 = {!!} -- record {}
  field
    ⦃ r2 ⦄ : R2 (Σ A B)
    fab : ∀ {a} {b : B a} → f (a , b)

An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE__, called at src/full/Agda/TypeChecking/Records.hs:734:11 in Agda-2.6.3-D2V0PkTCBiXC7IJuWrP7mz:Agda.TypeChecking.Records

If the goal of bR1 is replaced with record {} then the code type checks. This error occurred with Agda versions 2.6.2 and master branch at commit 23e07c0.

[andreasabel]

The error already occurs with

record ⊤ : Set where

record R : Set₁ where
  foo : ⊤
  foo = ?  -- works with _ instead of ?
  field X : Set

[andreasabel]

Bisection says: 56c804c is the first bad commit.

Date:   Fri Jul 8 20:09:47 2016 +0100

    Add warnings machinery

(Patch comprises 14 changed files with 380 additions and 97 deletions - sigh...)
Ping @fredrikNordvallForsberg @gallais .

UPDATE: This patch isn't the problem, maybe it exposed the problem, or it is a false alarm.

[andreasabel]

It seems like the crashing eta-reduction happens during this instantiateFull:

agda/src/full/Agda/TypeChecking/Rules/Def.hs

Line 342 in 8e4a198

cs <- instantiateFull {- =<< mapM rebindClause -} cs

It is called on foo r = _1 r and I supposed _1 := record{} so we end up with the ill-formed record{} r.
I suppose when the meta is created during computing the type of the constructor (hello #434) there is no record variable r in the context, but when we check the declaration foo there is. This would explain why the problem does not surface with _ instead of ?. With an interaction meta, we are trying to not create two metas (one an in each path), and instead reuse the meta created on the first run-through, which happens to be created in a context without record variable r.

[andreasabel]

I suppose the heuristics here:

agda/src/full/Agda/TypeChecking/MetaVars.hs

Lines 365 to 375 in 8e4a198

	newQuestionMark'
	:: (Comparison -> Type -> TCM (MetaId, Term))
	-> InteractionId -> Comparison -> Type -> TCM (MetaId, Term)
	newQuestionMark' new ii cmp t = do
	-- Andreas, 2016-07-29, issue 1720-2
	-- This is slightly risky, as the same interaction id
	-- maybe be shared between different contexts.
	-- Blame goes to the record processing hack, see issue #424
	-- and @ConcreteToAbstract.recordConstructorType@.
	let existing x = (x,) . MetaV x . map Apply <$> getContextArgs
	flip (caseMaybeM $ lookupInteractionMeta ii) existing $ {-else-} do

blows up in this case. We need to use a meta-variable created in one context (without the r variable) in an extended extension (with the r variable)? Is this something we can do with checkpoints @jespercockx @UlfNorell ?

[andreasabel]

While #5483 fixed my shrunk MWE, the OP still produces an internal error (but a new one):

record R3 (A : Set) (B : A → Set) : Set₁ where
  instance
    bR1 : {a : A} → R1 (B a)
    bR1 = {!!} 

expecting meta-creation context (with fields instead of record var)
  [B, A]
to be an expansion of the meta-reuse context (with record var)
  [a, r, B, A]
  glen  = 2
  g1len = 1
  g0len = 2
  frontMatch = False
  rearMatch  = True

It seems that on the first pass, Agda did not insert the hidden binding {a}, but on the second pass.