Internal error when interactively checking expression with new meta-variables

[jashug]

In emacs with the Agda mode, pressing C-u C-c C-; in the hole (in the definition of baz) gives the error

An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE_VERBOSE__, called at src/full/Agda/TypeChecking/Reduce.hs:224:18 in Agda-2.7.0.1-6273180bd9b53a251e88a8912e7909d128fe0195585b527f0efc07f60cb86e79:Agda.TypeChecking.Reduce

Agda file below, no flags.

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

record Foo {ℓ} (X : Set ℓ) : Set ℓ where
  field
    foo : X
open Foo {{...}}

instance
  bar : ∀ {ℓ} {X : Set ℓ} {x : X} → Foo (x ≡ x)
  bar .foo = refl

baz : ∀ {X : Set} → X ≡ X
baz = {! foo {{bar}} !}

Agda version 2.7.0.1, recently installed with cabal.

[andreasabel]

Agda version 2.7.0.1, recently installed with cabal.

I can confirm the bug on 2.7.0.1.
On current master, however, both C-c C-; and C-c C-, are simply doing nothing, which is a more worrisome bug...

On 2.6.2.2, the OP triggers this error:

no such meta variable _27
CallStack (from HasCallStack):
  error, called at src/full/Agda/TypeChecking/Monad/Base.hs:3954:10

Similar error in 2.6.1.

In 2.6.0, it worked:

Goal: X ≡ X
Elaborates to: Wrap.wrapped inst-refl
————————————————————————————————————————————————————————————
X : Set  (not in scope)

[andreasabel]

On current master, however, both C-c C-; and C-c C-, are simply doing nothing, which is a more worrisome bug...

Fixed hopefully by:

• Fixup #7610: update emacs mode to new Interval type #7625

[gallais]

I trigger the same bug on 2.7.0 with the following code (again using C-c C-;):

_∘′_ : ∀ {A B C : Set} → (B → C) → (A → B) → (A → C)
(f ∘′ g) x = f (g x)

_ : {A B C : Set} → (A → C) → (B → C)
_ = λ notA → {!notA ∘′ ?!}

Is it fixed on master too (this one has nothing to do with instances)?

[szumixie]

The error appears just by having a hole in a hole:

_ : Set
_ = {! ? !} -- C-c C-;

[andreasabel]

agda/src/full/Agda/Interaction/InteractionTop.hs

Lines 737 to 745 in 49a12ea

	interpret (Cmd_goal_type_context_check norm ii rng s) = do
	term <- liftLocalState $ withInteractionId ii $ do
	expr <- B.parseExprIn ii rng s
	goal <- B.typeOfMeta AsIs ii
	term <- case goal of
	OfType _ ty -> checkExpr expr =<< isType_ ty
	_ -> __IMPOSSIBLE__
	B.normalForm norm term
	cmd_goal_type_context_and (GoalAndElaboration term) norm ii rng s

I think the problem is that term is living in a state that has an additional meta created by the ?, but this state is restricted by liftLocalState, and then we are using term outside of the state in which it makes sense.
GoalAndElaboration should not take a naked Term but either its Closure or its reification.

Looks like this regression was introduced by:

• Delay serialization of Response #3811

Confirmed by numerology since this issue number is 7-6-24 and the PR was merged 2019-6-24.
And since this was my birthday anniversary I am fixing the issue!