Unbound de Bruijn indices show up in error message of unifier

From andreas....@gmail.com on November 30, 2013 18:07:01

open import Common.Prelude renaming (Nat to ℕ) open import Common.Equality

infix 3 ¬_

¬_ : Set → Set ¬ P = P → ⊥

-- Decidable relations.

data Dec (P : Set) : Set where yes : ( p : P) → Dec P no : (¬p : ¬ P) → Dec P

≟ : (m n : ℕ) → Dec (m ≡ n) zero ≟ zero = yes refl zero ≟ suc n = no λ() suc m ≟ zero = no λ() suc m ≟ suc n with m ≟ n suc m ≟ suc .m | yes refl = yes refl suc m ≟ suc n | no prf = no (λ x → prf (cong pred x))

data Ty : Set where

data Cxt : Set where ε : Cxt , : (Γ : Cxt) (a : Ty) → Cxt

len : Cxt → ℕ len ε = 0 len (Γ , _) = suc (len Γ)

-- De Bruijn index

mutual Var : Cxt → Ty → Set Var Γ a = Var' a Γ

data Var' (a : Ty) : (Γ : Cxt) → Set where zero : ∀ {Γ} → Var (Γ , a) a suc : ∀ {Γ b} (x : Var Γ a) → Var (Γ , b) a

-- De Bruijn Level

Lev = ℕ

-- Valid de Bruijn levels.

data LookupLev : (x : Lev) (Γ : Cxt) (a : Ty) (i : Var Γ a) → Set where lookupZero : ∀ {Γ a} → LookupLev (len Γ) (Γ , a) a zero

lookupSuc : ∀ {Γ a b x i} → LookupLev x Γ a i → LookupLev x (Γ , b) a (suc i)

record ValidLev (x : Lev) (Γ : Cxt) : Set where constructor validLev field {type } : Ty {index} : Var Γ type valid : LookupLev x Γ type index

weakLev : ∀ {x Γ a} → ValidLev x Γ → ValidLev x (Γ , a) weakLev (validLev d) = validLev (lookupSuc d)

-- Looking up a de Bruijn level.

lookupLev : ∀ (x : Lev) (Γ : Cxt) → Dec (ValidLev x Γ) lookupLev x ε = no λ { (validLev ()) } lookupLev x (Γ , a) with x ≟ len Γ lookupLev . (Γ , a) | yes refl = yes (validLev lookupZero) lookupLev x (Γ , a) | no with lookupLev x Γ lookupLev x (Γ , a) | no ¬p | yes d = yes (weakLev d) lookupLev x (Γ , a) | no ¬p | no ¬d = no contra where contra : ¬ ValidLev x (Γ , a) contra (validLev (lookupSuc valid)) = ?

{- Unbound indices showing up in error message:

I'm not sure if there should be a case for the constructor lookupZero, because I get stuck when trying to solve the following unification problems (inferred index ≟ expected index): len Γ ≟ @8 Γ , a ≟ @7 , @4 a ≟ type zero ≟ index when checking the definition of contra -}

Original issue: http://code.google.com/p/agda/issues/detail?id=985

UlfNorell / agda-test

Unbound de Bruijn indices show up in error message of unifier #985