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

[kubaneko]

trafficstars

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 [email protected] Date: Thu May 28 09:54:29 2020 +0200

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

#4681

[jespercockx]

Here is a minimized test case:

open import Agda.Builtin.Bool
open import Agda.Builtin.Sigma
open import Agda.Builtin.Unit

P : Bool → Set
P true = ⊤
P false = Σ Bool λ _ → Bool

f : (A : Bool) → P A → P A
f true _ = f _ _
f false (true , _) = _

Error is still the same:

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

[jespercockx]

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ₜ₌

It seems like this is the termination checker, specifically the function tryReduceNonRecursiveClause in Termination.TermCheck tries to get rid of the recursive call in the first clause by applying the second clause to it.

The actual problem is indeed what @UlfNorell already diagnosed: when we fail a match we brazenly continue matching the (potentially remaining) ill-typed patterns, which is problematic in the case of eta-record constructors. I'm fixing this in the stupidest way, i.e. by checking that the constructor names match before projecting. We can also think about whether we actually want to do potentially ill-typed matching and/or whether we should have clause-based matching at all, but that's for another day.