Internal error at Agda/TypeChecking/Substitute.hs:140:33

[kubaneko]

On agda 2.6.4.1 and 2.6.4.3

module Bug {a}
  where

open import Agda.Primitive using (lsuc; _⊔_)
open import Agda.Builtin.Sigma using (Σ; _,_)
open import Agda.Builtin.Nat using (Nat; suc)

data _≤′_ (m : Nat) : Nat → Set where
  ≤′-refl :                         m ≤′ m
  ≤′-step : ∀ {n} (m≤′n : m ≤′ n) → m ≤′ (suc n)

_<′_ : (m n : Nat) → Set
m <′ n = (suc m) ≤′ n

data Product {n : Nat} : Set a where
  ne    : Product

record LogRelKit : Set (lsuc a) where
  constructor Kit
  field
    ⊩U : Set a
    ⊩B : Set a
    ⊩ : Set a
    ⊩/_ : ⊩ → Set a

module LogRel (l : Nat) (rec : ∀ {l′} → l′ <′ l → LogRelKit) where

  record ⊩₁U : Set a where
    constructor Uᵣ
    field
      l′  : Nat
      l<  : l′ <′ l

  record ⊩₁U/ : Set a where
    constructor Uₜ₌

  record ⊩ₗB : Set a where
    constructor Bᵣ
    eta-equality

  ⊩ₗΣ/_ :
    ([A] : ⊩ₗB) → Set a
  ⊩ₗΣ/_
    Bᵣ = Σ Product λ pProd → Nat

  data ⊩ₗ : Set a where
    Uᵣ  : ⊩₁U → ⊩ₗ
    Bᵣ  : ⊩ₗB → ⊩ₗ

  ⊩ₗ/_ : ⊩ₗ → Set a
  ⊩ₗ/ Uᵣ (Uᵣ l′ l<) = ⊩₁U/
  ⊩ₗ/ Bᵣ ΣA  = ⊩ₗΣ/ ΣA

  kit : LogRelKit
  kit = Kit ⊩₁U ⊩ₗB
            ⊩ₗ ⊩ₗ/_

open LogRel public
  using
    (Uᵣ; Bᵣ; Uₜ₌;
     module ⊩₁U; module ⊩₁U/;
     module ⊩ₗB)

pattern Σₜ₌ pProd prop = pProd , prop

pattern Uᵣ′ a b = Uᵣ (Uᵣ a b)

mutual
  kit : Nat → LogRelKit
  kit ℓ = LogRel.kit ℓ kit-helper

  kit-helper : {n m : Nat} → m <′ n → LogRelKit
  kit-helper {m = m} ≤′-refl = kit m
  kit-helper (≤′-step p) = kit-helper p

⊩⟨_⟩ : (l : Nat) → Set a
⊩⟨ l ⟩ = ⊩ where open LogRelKit (kit l)

⊩⟨_⟩∷/_ : (l : Nat) → ⊩⟨ l ⟩ → Set a
⊩⟨ l ⟩∷/ [A] = ⊩/ [A] where open LogRelKit (kit l)

transEqTerm :  {l : Nat}
              ([A] : ⊩⟨ l ⟩)
            → ⊩⟨ l ⟩∷/ [A]
            → ⊩⟨ l ⟩∷/ [A]
transEqTerm (Uᵣ′ l′ (≤′-step s)) _ =
              lemma (transEqTerm
              ? ?)
            where
              lemma : {l′ n : Nat} {s : l′ <′ n} →
                ⊩⟨ n ⟩∷/ Uᵣ′ _ s → ⊩⟨ suc n ⟩∷/ Uᵣ′ _ (≤′-step s)
              lemma = {!!}
transEqTerm
  (Bᵣ Bᵣ)
  (Σₜ₌ ne p~r) = {!!}
transEqTerm = ?

Throws the error:

An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE__, called at src/full/Agda/TypeChecking/Substitute.hs:140:33 in Agda-2.6.4.1-7xG50m7UQLK4krJEY6TPg:Agda.TypeChecking.Substitute

The error no longer happens if one adds {l = suc l} in the U case. Like this:

transEqTerm {l = suc l} (Uᵣ′ l′ (≤′-step s)) _ =

[UlfNorell]

Reproduces on recent master. The impossible is triggered trying to project a field from a constructor application of the wrong type.

[UlfNorell]

What happens (for reasons I don't know) is that we're trying to match the Bᵣ clause against an application to Uᵣ and Uₜ₌. This all takes place in the clause evaluator and runs into this case:

https://github.com/agda/agda/blob/4abc209542404c378541a27a57bded746fe4e68f/src/full/Agda/TypeChecking/Patterns/Match.hs#L123-L127

Here the comment (referring to #2964) says that we should keep matching even though Uᵣ doesn't match Bᵣ. The problem is that the Σₜ₌ pattern is on an eta-record and thus doesn't block evaluation. Instead we try to project from the value, but in this case it has the wrong type causing the impossible. Cc @jespercockx.

[andreasabel]

Here the comment (referring to #2964)

N.B.: This issues was closed for 2.6.0 but the regression is in 2.6.2.

[UlfNorell]

The test case is extremely brittle, so I don't think it's accurate to say it's a regression in 2.6.2. I feel quite confident in saying that the problem is the fix of #2964.

[andreasabel]

Yeah, you are probably right about this, bisection only returns the generic commit:

2f212bf5568a8d408f3b3a8d3cb87a6fa6e6b3a1 is the first bad commit Author: Ulf Norell ulf.norell@gmail.com Date: Thu May 28 09:54:29 2020 +0200

Add --auto-inline and make it off by default

4681