Internal error caused by abstracting variables

[dolio]

The following code causes an internal error:

    module Bug where

    record ⊤ : Set where
    record Σ-stx (A : Set) (B : A → Set) : Set where
      constructor _,_
      field
        fst : A
        snd : B fst

    syntax Σ-stx A (λ x → B) = Σ[ x ∈ A ] B

    module V (X : Set) (El : X → Set) where
      data V : Set where
        el : X → V
        Π : (i : X) → (El i → V) → V

      Sem : V → Set
      Sem (el S) = El S
      Sem (Π S T) = (s : El S) → Sem (T s)

      data Ctx : Set
      Env : Ctx → Set

      data Ctx where
        [] : Ctx
        _∷_ : (Γ : Ctx) → (T : Env Γ → X) → Ctx

      Env [] = ⊤
      Env (Γ ∷ T) = Σ[ γ ∈ Env Γ ] El (T γ)

      variable
        Γ : Ctx
        A B : Env Γ → X
        S T : Env Γ → V

    module L (X : Set) (El : X → Set) where
      open V X El

      Π̂ : (A : Env Γ → X) (B : Env (Γ ∷ A) → V) → Env Γ → V
      Π̂ A B γ = Π (A γ) (λ a → B (γ , a))

      data Tm : (Γ : Ctx) → (T : Env Γ → V) → Set
      eval : Tm Γ T → (γ : Env Γ) → Sem (T γ)

      data Tm where
        lam : Tm (Γ ∷ A) T → Tm Γ (Π̂ A T)

      eval tm = {!!}

It seems to be related to quantifying the variables for lam. The error message is:

An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE__, called at src/full/Agda/TypeChecking/Generalize.hs:301:38 in ...

Latest version from the master branch as of this comment.

[andreasabel]

Running a bisect...

[UlfNorell]

It's #3667. The check for constrained metas is missing a meta for some reason. The "regression" is that I put an __IMPOSSIBLE__ when this happens rather than generating an ill formed type.

Prediction: bisect will blame baf79f9

[andreasabel]

Bisection yields:
Checking Issue5845 (/Users/abel/tmp/agda/Issue5845.agda).
An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE__, called at src/full/Agda/TypeChecking/Generalize.hs:285:38 in Agda-2.6.2-inplace:Agda.TypeChecking.Generalize
Verdict: Bad
d1a9d7d is the first bad commit @jespercockx
Date: Fri Oct 16 16:52:33 2020 +0200
[ re #4727 ] Promote metavariable from irrelevant to relevant or from erased to non-erased during Occurs check

[jespercockx]

Here is a minimized example:

open import Agda.Builtin.Sigma

data Ctx : Set₁
Env : Ctx → Set

data Ctx where
  _∷_ : (Γ : Ctx) → (T : Env Γ → Set) → Ctx

Env (Γ ∷ T) = Σ (Env Γ) T

variable
  Γ : Ctx
  A T : Env _ → Set

data Tm : (Γ : Ctx) → (T : Env Γ → Set) → Set₁ where
  lam : Tm (Γ ∷ A) T