Agda panic: Pattern match failure

[alexarice]

I seem to have managed to trigger a panic in the Agda codebase. I've reduced it down to this code:

{-# OPTIONS --safe --without-K --exact-split #-}

module Catt.Broken where


open import Data.Nat
open import Data.Fin
open import Data.Fin.Patterns

variable
  n m d d′ submax : ℕ

data Ctx : ℕ → ℕ → Set
data Ty : Ctx n d → ℕ → Set
data Tm : Ctx n d → ℕ → Set
data Sub : Ctx n d → Ctx m d′ → Set

variable
  Γ Δ : Ctx n d
  A : Ty Γ n
  s t  : Tm Γ n
  σ  : Sub Γ Δ

infixl 25 _,_
data Ctx where
  ∅ : Ctx 0 0
  _,_ : (Γ : Ctx m d) → (A : Ty Γ n) → Ctx (suc m) (d ⊔ n)

ctxLength : (Γ : Ctx n d) → ℕ
ctxLength {n} Γ = n

ty-dim : Ty Γ n → ℕ
ty-dim {n = n} A = n

ctx-dim : Ctx n d → ℕ
ctx-dim {d = d} Γ = d

tm-dim : Tm Γ n → ℕ
tm-dim {n = n} t = n

lookupDim : (Γ : Ctx n d) → Fin n → ℕ
lookupDim (Γ , A) zero = ty-dim A
lookupDim (Γ , A) (suc i) = lookupDim Γ i

infix 30 _─⟨_⟩⟶_
data Ty where
  ⋆ : Ty Γ 1
  _─⟨_⟩⟶_ : (s : Tm Γ (suc n)) → (A : Ty Γ n) → (t : Tm Γ (suc n)) → Ty Γ (suc n)

data Sub where
  ⟨⟩ : Sub ∅ Δ
  ⟨_,_⟩ : (σ : Sub Γ Δ) → {A : Ty Γ m} → (t : Tm Δ (suc m)) → Sub (Γ , A) Δ

data Tm where
  Var : (i : (Fin (ctxLength Γ))) → Tm Γ (suc (lookupDim Γ i))
  Coh : (Δ : Ctx n d) → (A : Ty Δ m) → (σ : Sub Δ Γ) → Tm Γ (suc (ctx-dim Δ) ⊔ suc m)

liftTerm : Tm Γ n → Tm (Γ , A) n
liftSub : Sub Δ Γ → Sub Δ (Γ , A)
liftType : Ty Γ n → Ty (Γ , A) n

liftTerm (Var i) = Var (suc i)
liftTerm (Coh Δ A σ) = Coh Δ A (liftSub σ)

liftSub ⟨⟩ = ⟨⟩
liftSub ⟨ σ , t ⟩ = ⟨ liftSub σ , liftTerm t ⟩

liftType ⋆ = ⋆
liftType (s ─⟨ A ⟩⟶ t) = liftTerm s ─⟨ liftType A ⟩⟶ liftTerm t

data _⊢pd[_][_]_∶_ : (Γ : Ctx n d) → ℕ → (d : ℕ) → Tm Γ (suc (suc d)) → Ty Γ (suc d) → Set


getFocusTerm : Γ ⊢pd[ submax ][ d ] t ∶ A → Tm Γ (suc (suc d))
getFocusTerm {t = t} pdb = t

getFocusType : Γ ⊢pd[ submax ][ d ] t ∶ A → Ty Γ (suc d)
getFocusType {A = A} pdb = A

-- Uniquely extend a pasting context
extend : {Γ : Ctx n m} {t : Tm Γ (suc (suc d))} {A : Ty Γ (suc d)} → Γ ⊢pd[ submax ][ d ] t ∶ A → Ctx (suc (suc n)) (m ⊔ suc d ⊔ suc (suc d))
extend {Γ = Γ} pdb = Γ , getFocusType pdb , liftTerm (getFocusTerm pdb) ─⟨ liftType (getFocusType pdb) ⟩⟶ Var 0F

data _⊢pd[_][_]_∶_ where
  ExtendM : {Γ : Ctx n m}
          → {t : Tm Γ (suc (suc d))}
          → {A : Ty Γ (suc d)}
          → (pdb : Γ ⊢pd[ 0 ][ d ] t ∶ A) →
            extend pdb ⊢pd[ 0 ][ suc d ] Var 0F ∶ liftTerm (liftTerm t) ─⟨ liftType (liftType A) ⟩⟶ Var 1F


test : Γ ⊢pd[ submax ][ d ] t ∶ A → Set
test (ExtendM pdb) = ?

Which gives the following error with agda version 2.6.2:

Panic: Pattern match failure in do expression at
src/full/Agda/TypeChecking/Rules/LHS/Unify.hs:1313:7-14
when checking that the pattern ExtendM pdb has type
Γ ⊢pd[ submax ][ d ] t ∶ A

Inlining the call to extend pdb in the constructor type seems to fix the issue, though I'm guessing it is not ideal that agda is doing this.

[andreasabel]

This is a bug in the forcing optimization, you can work around it with {-# OPTIONS --no-forcing #-}.

Error location is here:

agda/src/full/Agda/TypeChecking/Rules/LHS/Unify.hs

Line 1313 in 8aec1e6

Just md' <- gets $ IntMap.lookup i

[andreasabel]

Here is a version without the standard library (probably not minimal yet):

{-# OPTIONS --without-K --exact-split #-}
-- {-# OPTIONS --no-forcing #-}

open import Agda.Builtin.Nat renaming (Nat to ℕ)

infixl 8  _⊔_
postulate _⊔_ : (n m : ℕ) → ℕ

variable
  n m d d′ submax : ℕ

data Fin : ℕ → Set where
  zero : Fin (suc n)
  suc  : (i : Fin n) → Fin (suc n)

data Ctx : ℕ → ℕ → Set
data Ty : Ctx n d → ℕ → Set
data Tm : Ctx n d → ℕ → Set
data Sub : Ctx n d → Ctx m d′ → Set

variable
  Γ Δ : Ctx n d
  A : Ty Γ n
  s t  : Tm Γ n
  σ  : Sub Γ Δ

infixl 25 _,_
data Ctx where
  ∅ : Ctx 0 0
  _,_ : (Γ : Ctx m d) → (A : Ty Γ n) → Ctx (suc m) (d ⊔ n)

ctxLength : (Γ : Ctx n d) → ℕ
ctxLength {n} Γ = n

ty-dim : Ty Γ n → ℕ
ty-dim {n = n} A = n

ctx-dim : Ctx n d → ℕ
ctx-dim {d = d} Γ = d

tm-dim : Tm Γ n → ℕ
tm-dim {n = n} t = n

lookupDim : (Γ : Ctx n d) → Fin n → ℕ
lookupDim (Γ , A) zero = ty-dim A
lookupDim (Γ , A) (suc i) = lookupDim Γ i

infix 30 _─⟨_⟩⟶_
data Ty where
  ⋆ : Ty Γ 1
  _─⟨_⟩⟶_ : (s : Tm Γ (suc n)) → (A : Ty Γ n) → (t : Tm Γ (suc n)) → Ty Γ (suc n)

data Sub where
  ⟨⟩ : Sub ∅ Δ
  ⟨_,_⟩ : (σ : Sub Γ Δ) → {A : Ty Γ m} → (t : Tm Δ (suc m)) → Sub (Γ , A) Δ

data Tm where
  Var : (i : (Fin (ctxLength Γ))) → Tm Γ (suc (lookupDim Γ i))
  Coh : (Δ : Ctx n d) → (A : Ty Δ m) → (σ : Sub Δ Γ) → Tm Γ (suc (ctx-dim Δ) ⊔ suc m)

liftTerm : Tm Γ n → Tm (Γ , A) n
liftSub : Sub Δ Γ → Sub Δ (Γ , A)
liftType : Ty Γ n → Ty (Γ , A) n

liftTerm (Var i) = Var (suc i)
liftTerm (Coh Δ A σ) = Coh Δ A (liftSub σ)

liftSub ⟨⟩ = ⟨⟩
liftSub ⟨ σ , t ⟩ = ⟨ liftSub σ , liftTerm t ⟩

liftType ⋆ = ⋆
liftType (s ─⟨ A ⟩⟶ t) = liftTerm s ─⟨ liftType A ⟩⟶ liftTerm t

data _⊢pd[_][_]_∶_ : (Γ : Ctx n d) → ℕ → (d : ℕ) → Tm Γ (suc (suc d)) → Ty Γ (suc d) → Set


getFocusTerm : Γ ⊢pd[ submax ][ d ] t ∶ A → Tm Γ (suc (suc d))
getFocusTerm {t = t} pdb = t

getFocusType : Γ ⊢pd[ submax ][ d ] t ∶ A → Ty Γ (suc d)
getFocusType {A = A} pdb = A

-- Uniquely extend a pasting context
extend : {Γ : Ctx n m} {t : Tm Γ (suc (suc d))} {A : Ty Γ (suc d)} → Γ ⊢pd[ submax ][ d ] t ∶ A → Ctx (suc (suc n)) (m ⊔ suc d ⊔ suc (suc d))
extend {Γ = Γ} pdb = Γ , getFocusType pdb , liftTerm (getFocusTerm pdb) ─⟨ liftType (getFocusType pdb) ⟩⟶ Var zero

data _⊢pd[_][_]_∶_ where
  ExtendM : {Γ : Ctx n m}
          → {t : Tm Γ (suc (suc d))}
          → {A : Ty Γ (suc d)}
          → (pdb : Γ ⊢pd[ 0 ][ d ] t ∶ A) →
            extend pdb ⊢pd[ 0 ][ suc d ] Var zero ∶ liftTerm (liftTerm t) ─⟨ liftType (liftType A) ⟩⟶ Var (suc zero)


test : Γ ⊢pd[ submax ][ d ] t ∶ A → Set
test (ExtendM pdb) = {!!}

It works in 2.6.1, so it is a regression in 2.6.2.

[andreasabel]

Bisection points to commit 2f212bf by @UlfNorell

Date:   Thu May 28 09:54:29 2020 +0200

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

#4681

Inlining the call to extend pdb in the constructor type seems to fix the issue

Likely, Agda did that before the above commit. But this commit only brings the bug to surface, I suppose.

[andreasabel]

I shrank this to:

open import Agda.Builtin.Nat

data Unit : Set where
  unit : Unit

data Ctx : Nat → Set where  -- index needed
  cons : (m : Nat) (A : Unit) → Ctx (suc m)

mutual

  data P : (n : Nat) (Γ : Ctx n) → Set

  -- Needs to be mutual
  {-# NOINLINE getFocus #-}
  getFocus : (n : Nat) (A : Unit) → Unit
  getFocus n A = A  -- needs to be A, not unit

  data P where
    c : (n : Nat) (A : Unit)
      → P (suc n) (cons n (getFocus n A))

test : (n : Nat) (Γ : Ctx n) → P n Γ → Set1
test n Γ (c m A) = Set
  -- ^ n := suc m fixes the issue

This version already crashes with 2.6.1 (and passes in 2.6.0), so we can restart bisection!

[andreasabel]

There is a new blamed commit: 8760d15 (ping @UlfNorell)

Date:   Fri Oct 18 12:08:40 2019 +0200

    Handle modalities when moving binding site of forced variables

 src/full/Agda/TypeChecking/Rules/LHS/Problem.hs |  5 ++-
 src/full/Agda/TypeChecking/Rules/LHS/Unify.hs   | 54 ++++++++++++++++---------
 test/Succeed/ForcingRelevance.agda              | 23 +++++++++++