__IMPOSSIBLE__ at src/full/Agda/TypeChecking/Reduce/Fast.hs:1394:20

[zilinc]

Produced on MacOs, with Agda version 2.6.3-b4e5b7a (also with 2.6.2.1 but on Line 1380).

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/Reduce/Fast.hs:1394:20 in Agda-2.6.3-inplace:Agda.TypeChecking.Reduce.Fast

There are two places that can trigger the bug. To reproduce, load the following program (which I haven't been able to reduce to a smaller one, sorry), and in the holes in invˡ and the one in All/Fresh′→Fresh, follow the comments to reproduce.

open import Agda.Builtin.Unit using (⊤; tt)
open import Data.Bool hiding (T)
open import Data.Nat.Base
open import Data.Product using (Σ; proj₁; proj₂; _,_; <_,_>; uncurry; curry; _×_; ∃; ∃-syntax)
open import Function using (_∘_; _$_; case_of_; id; flip)
open import Function.Bundles
open Inverse
open import Relation.Binary.PropositionalEquality hiding ([_]; Extensionality; ∀-extensionality; cong₂)
open ≡-Reasoning

module _ where

  open Data.Bool using (T)

  data DList : Set
  Fresh : (a : ℕ) → (l : DList) → Set

  data DList where
    dnil  : DList
    dcons : (a : ℕ) → (l : DList) → Fresh a l → DList

  Fresh a dnil = ⊤
  Fresh a (dcons b l _) = a ≢ b × Fresh a l

  data List′ : Set where
    nil′  : List′
    cons′ : ℕ → List′ → List′

  Fresh′ : ℕ → List′ → Set
  Fresh′ a nil′ = ⊤
  Fresh′ a (cons′ b l) = a ≢ b × Fresh′ a l
  
  AllFresh : List′ → Set
  AllFresh nil′ = ⊤
  AllFresh (cons′ a l) = Fresh′ a l × AllFresh l

  data DList′ : List′ → Set → Set₁ where
    dnil′  : DList′ nil′ ⊤
    dcons′ : ∀{l}{prf} → (a : ℕ) → DList′ l prf → DList′ (cons′ a l) ((Fresh′ a l) × prf)


  data DList″ : Set where
    dl″ : (l : List′) → AllFresh l → DList″

  undl″-l : DList″ → List′
  undl″-l (dl″ l _) = l

  undl″-p : DList″ → ∃[ l ] AllFresh l
  undl″-p (dl″ l p) = l , p

  dl-iso : DList ↔ DList″

  Fresh→Fresh′ : ∀{a}{l}{l″}
               → (f dl-iso l ≡ l″)
               → Fresh a l
               → Fresh′ a (undl″-l l″)

  Fresh→AllFresh : ∀{a}{l}{l″}
                 → (f dl-iso l ≡ l″)
                 → Fresh a l
                 → AllFresh (undl″-l l″)

  All/Fresh′→Fresh : ∀{a}{l}{l″}
         → (l ≡ f⁻¹ dl-iso l″)
         → Fresh′ a (undl″-l l″) × AllFresh (undl″-l l″)
         → Fresh a l

  f dl-iso dnil = dl″ nil′ tt
  f dl-iso (dcons a l p)
    = dl″ (cons′ a (undl″-l (f dl-iso l)))
          ((Fresh→Fresh′ {l = l}{l″ = f dl-iso l} refl p) ,
           (Fresh→AllFresh {a = a}{l = l}{l″ = f dl-iso l} refl p))

  f⁻¹ dl-iso (dl″ nil′ p) = dnil
  f⁻¹ dl-iso (dl″ (cons′ a l′) p)
    = dcons a (f⁻¹ dl-iso (dl″ l′ (proj₂ p)))
              (All/Fresh′→Fresh {l″ = dl″ l′ (proj₂ p)} refl p)

  cong₁ dl-iso refl = refl

  cong₂ dl-iso refl = refl

  -- Can't do any further, otherwise an Agda bug occurs.
  inverse dl-iso = (λ x → invˡ) , (λ x → invʳ)
    where invˡ : ∀{x} → f dl-iso (f⁻¹ dl-iso x) ≡ x
          invˡ {dl″ nil′ _} = refl
          invˡ {dl″ (cons′ a l) p}  = {!!}  -- add "rewrite invˡ {dl″ l ?}" (w/o quotes) to the left of the = sign and C-c C-l

          invʳ : ∀{x} → f⁻¹ dl-iso (f dl-iso x) ≡ x
          invʳ {dnil} = refl
          invʳ {dcons a l p} = {!!}

  Fresh→Fresh′ {a} {dnil} eq p rewrite sym eq = tt
  Fresh→Fresh′ {a} {dcons a₁ l x} eq p rewrite sym eq
    = proj₁ p ,  Fresh→Fresh′ {l″ = f dl-iso l} refl (proj₂ p)

  Fresh→AllFresh {l = dnil} eq p rewrite sym eq = tt
  Fresh→AllFresh {l = dcons a l x} eq p rewrite sym eq
    = (Fresh→Fresh′ {l″ = f dl-iso l} refl x) , Fresh→AllFresh {a = a}{l = l}{l″ = f dl-iso l} refl x

  All/Fresh′→Fresh {a} {l″ = dl″ nil′ x} eq p rewrite eq = tt
  All/Fresh′→Fresh {a} {l″ = dl″ (cons′ b l) x} eq p rewrite eq
    = (proj₁ ∘ proj₁ $ p) , {!!}  -- put "All/Fresh′→Fresh" in the hole and C-c C-r

[andreasabel]

It is not too hard to shrink the standard-library away from this test case:

open import Agda.Builtin.Unit using (⊤; tt)
open import Agda.Builtin.Nat renaming (Nat to ℕ)
open import Agda.Builtin.Equality
open import Agda.Builtin.Sigma renaming (fst to proj₁; snd to proj₂)

data ⊥ : Set where

∃ : {A : Set} (B : A → Set) → Set
∃ B = Σ _ B

_×_ : (A B : Set) → Set
A × B = Σ A λ _ → B

sym : {A : Set} {x y : A} → x ≡ y → y ≡ x
sym refl = refl

_≢_ : {A : Set} (x y : A) → Set
x ≢ y = x ≡ y → ⊥

record Inverse (A B : Set) : Set where
  field
    f         : A → B
    f⁻¹       : B → A
    inverse   : ∀ x → f (f⁻¹ x) ≡ x
open Inverse

data DList : Set
Fresh : (a : ℕ) → (l : DList) → Set

data DList where
  dnil  : DList
  dcons : (a : ℕ) → (l : DList) → Fresh a l → DList

Fresh a dnil = ⊤
Fresh a (dcons b l _) = (a ≢ b) × Fresh a l

data List′ : Set where
  nil′  : List′
  cons′ : ℕ → List′ → List′

Fresh′ : ℕ → List′ → Set
Fresh′ a nil′ = ⊤
Fresh′ a (cons′ b l) = (a ≢ b) × Fresh′ a l

AllFresh : List′ → Set
AllFresh nil′ = ⊤
AllFresh (cons′ a l) = Fresh′ a l × AllFresh l

data DList′ : List′ → Set → Set₁ where
  dnil′  : DList′ nil′ ⊤
  dcons′ : ∀{l}{prf} → (a : ℕ) → DList′ l prf → DList′ (cons′ a l) (Fresh′ a l × prf)


data DList″ : Set where
  dl″ : (l : List′) → AllFresh l → DList″

undl″-l : DList″ → List′
undl″-l (dl″ l _) = l

undl″-p : DList″ → ∃ AllFresh
undl″-p (dl″ l p) = l , p

-- dl-iso : DList ↔ DList″
dl-iso : Inverse DList DList″
-- f-dl-iso : DList → DList″
-- g-dl-iso : DList″ → DList
-- inverse-dl-iso : ∀ x → f-dl-iso (g-dl-iso x) ≡ x

Fresh→Fresh′ : ∀{a}{l}{l″}
             → (f dl-iso l ≡ l″)
             → Fresh a l
             → Fresh′ a (undl″-l l″)

Fresh→AllFresh : ∀{a}{l}{l″}
               → (f dl-iso l ≡ l″)
               → Fresh a l
               → AllFresh (undl″-l l″)

All/Fresh′→Fresh : ∀{a}{l}{l″}
       → (l ≡ f⁻¹ dl-iso l″)
       → Fresh′ a (undl″-l l″) × AllFresh (undl″-l l″)
       → Fresh a l

f dl-iso dnil = dl″ nil′ tt
f dl-iso (dcons a l p)
  = dl″ (cons′ a (undl″-l (f dl-iso l)))
        ((Fresh→Fresh′ {l = l}{l″ = f dl-iso l} refl p) ,
         (Fresh→AllFresh {a = a}{l = l}{l″ = f dl-iso l} refl p))

f⁻¹ dl-iso (dl″ nil′ p) = dnil
f⁻¹ dl-iso (dl″ (cons′ a l′) p)
  = dcons a (f⁻¹ dl-iso (dl″ l′ (proj₂ p)))
            (All/Fresh′→Fresh {l″ = dl″ l′ (proj₂ p)} refl p)

-- Can't do any further, otherwise an Agda bug occurs.
inverse dl-iso x = invˡ
  where
  invˡ : ∀{x} → f dl-iso (f⁻¹ dl-iso x) ≡ x
  invˡ {dl″ nil′ _} = refl
  invˡ {dl″ (cons′ a l) p} rewrite invˡ {dl″ l ?} = {!!}  -- the "rewrite invˡ {dl″ l ?}" causes the internal error

Fresh→Fresh′ {a} {dnil} eq p rewrite sym eq = tt
Fresh→Fresh′ {a} {dcons a₁ l x} eq p rewrite sym eq
  = proj₁ p ,  Fresh→Fresh′ {l″ = f dl-iso l} refl (proj₂ p)

Fresh→AllFresh {l = dnil} eq p rewrite sym eq = tt
Fresh→AllFresh {l = dcons a l x} eq p rewrite sym eq
  = (Fresh→Fresh′ {l″ = f dl-iso l} refl x) , Fresh→AllFresh {a = a}{l = l}{l″ = f dl-iso l} refl x

All/Fresh′→Fresh {a} {l″ = dl″ nil′ x} eq p rewrite eq = tt
All/Fresh′→Fresh {a} {l″ = dl″ (cons′ b l) x} eq p rewrite eq
  = (proj₁ (proj₁ p)) , {!All/Fresh′→Fresh!}  -- put "All/Fresh′→Fresh" in the hole and C-c C-r

Crash site:

agda/src/full/Agda/TypeChecking/Reduce/Fast.hs

Lines 1277 to 1280 in 5401dc1

	evalPointerAM :: Pointer s -> Spine s -> ControlStack s -> ST s (Blocked Term)
	evalPointerAM (Pure cl) spine ctrl = runAM (Eval (clApply cl spine) ctrl)
	evalPointerAM (Pointer p) spine ctrl = readPointer p >>= \ case
	BlackHole -> __IMPOSSIBLE__

In Agda 2.6.1 you get a termination error, so this is a regression.

The internal error goes away if I label dl-iso as one of these:

• {-# TERMINATING #-}
• {-# NON_TERMINATING #-}
• {-# NO_TERMINATION_CHECK #-}

The error persists with {-# OPTIONS --no-fast-reduce #-}, with crash site:

agda/src/full/Agda/TypeChecking/CompiledClause/Match.hs

Lines 205 to 207 in 5401dc1

	{-else-} $ traceSLn "impossible" 10
	("Incomplete pattern matching when applying " ++ prettyShow f)
	__IMPOSSIBLE__

Last words:

termination checking body of Issue5819.-rewrite276
...
termClause
  tel = {l : DList} (b : ℕ) (l₁ : List′) (x : AllFresh (cons′ b l₁))
        (eq : l ≡ f⁻¹ dl-iso (dl″ (cons′ b l₁) x)) {a : ℕ}
        (p
         : Σ (Σ (a ≡ b → ⊥) (λ _ → Fresh′ a l₁))
           (λ _ → Σ (Fresh′ b l₁) (λ _ → AllFresh l₁)))
  ps  = [{l = _}, b, l, x, eq, _, refl, {a = a}, p]
Incomplete pattern matching when applying Issue5819.dl-iso

[andreasabel]

Bisection blames commit 8e0fca8 (ping @jespercockx)

Date: Sun Apr 5 10:02:44 2020 +0200
[ perf ] Avoid normalisation in termToDBP function

[andreasabel]

Fixed by reverting the blamed commit, which tried to optimize termination checking by getting rid of a normalize. Unfortunately, it introduced a reduce on a term that went through the hack stripAllProjections and thus wasn't wellformed anymore. Hence, the pattern matching failures during reduction.