Agda won't let me fill typed hole with term of matching type due to definitional equality constraint

Question

This is a stripped-down version of the program that has this error:

open import Data.Empty using (⊥-elim)
open import Data.Nat using (ℕ; zero; suc)
open import Data.Fin using (Fin; punchOut; punchIn; _≟_)
  renaming (zero to fzero; suc to fsuc)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; sym)
open import Relation.Nullary using (yes; no; ¬_)

private
  variable
    n : ℕ

data Type : Set where
  _⇒_ : Type → Type → Type
  T : Type

data Term : ℕ → Set where
  abs : Type → Term (suc n) → Term n
  app : Term n → Term n → Term n
  var : Fin n → Term n

data Ctx : ℕ → Set where
  ● : Ctx 0
  _,-_ : Ctx n → Type → Ctx (suc n)

-- | Increments the variables that are free relative to the inserted "pivot" variable.
lift : Term n → Fin (suc n) → Term (suc n)
lift (abs ty body) v = abs ty (lift body (fsuc v))
lift (app f x) v = app (lift f v) (lift x v)
lift (var n) v = var (punchIn v n)

_[_≔_] : Term (suc n) → Fin (suc n) → Term n → Term n
(abs ty body) [ v ≔ def ] = abs ty (body [ fsuc v ≔ lift def fzero ])
(app f x)     [ v ≔ def ] = app (f [ v ≔ def ]) (x [ v ≔ def ])
(var n)       [ v ≔ def ] with v ≟ n
... | yes refl = def
... | no neq = var (punchOut {i = v} {j = n} λ { refl → neq (sym refl)})

find : Ctx n → Fin n → Type
find (Γ ,- A) fzero = A
find (Γ ,- A) (fsuc n) = find Γ n

private
  variable
    Γ : Ctx n
    a b c f x : Term n
    A B C : Type
    v : Fin n

data _∋_⦂_ : Ctx n → Fin n → Type → Set where
  vzero : (Γ ,- A) ∋ fzero ⦂ A
  vsuc : (Γ ∋ v ⦂ A) → (Γ ,- B) ∋ fsuc v ⦂ A

lookup : (Γ : Ctx n) → (v : Fin n) → Γ ∋ v ⦂ find Γ v
lookup (Γ ,- A) fzero = vzero
lookup (Γ ,- B) (fsuc v) = vsuc (lookup Γ v)

data _⊢_⦂_ : Ctx n → Term n → Type → Set where
  ty-abs : (Γ ,- A) ⊢ b ⦂ B → Γ ⊢ abs A b ⦂ (A ⇒ B)
  ty-app : Γ ⊢ f ⦂ (A ⇒ B) → Γ ⊢ x ⦂ A → Γ ⊢ app f x ⦂ B
  ty-var : Γ ∋ v ⦂ A → Γ ⊢ var v ⦂ A

-- | Inserts a binding in the middle of the context.
liftΓ : Ctx n → Fin (suc n) → Type → Ctx (suc n)
liftΓ Γ fzero t = Γ ,- t
liftΓ (Γ ,- A) (fsuc v) t = (liftΓ Γ v t) ,- A

weakening-var
  : ∀ {Γ : Ctx n} {v' : Fin (suc n)} → Γ ∋ v ⦂ A → liftΓ Γ v' B ∋ Data.Fin.punchIn v' v ⦂ A
weakening-var {v' = fzero} vzero = vsuc vzero
weakening-var {v' = fsuc n} vzero = vzero
weakening-var {v' = fzero} (vsuc v) = vsuc (vsuc v)
weakening-var {v' = fsuc n} (vsuc v) = vsuc (weakening-var v)

weakening
  : ∀ {Γ : Ctx n} {v : Fin (suc n)} {t : Type} → Γ ⊢ a ⦂ A → liftΓ Γ v t ⊢ lift a v ⦂ A
weakening (ty-abs body) = ty-abs (weakening body)
weakening (ty-app f x) = ty-app (weakening f) (weakening x)
weakening (ty-var v) = ty-var (weakening-var v)

lemma : ∀ {Γ : Ctx n} → (v : Fin (suc n)) → liftΓ Γ v B ∋ v ⦂ A → A ≡ B
lemma fzero vzero = refl
lemma {Γ = _ ,- _} (fsuc fin) (vsuc v) = lemma fin v

subst-eq
  : (v : Fin (suc n))
  → liftΓ Γ v B ∋ v ⦂ A
  → Γ ⊢ b ⦂ B
  → Γ ⊢ var v [ v ≔ b ] ⦂ A
subst-eq fzero vzero typing = typing
subst-eq {Γ = Γ ,- C} (fsuc fin) (vsuc v) typing with fin ≟ fin
... | yes refl rewrite lemma fin v = typing
... | no neq = ⊥-elim (neq refl)

subst-neq
  : (v v' : Fin (suc n))
  → liftΓ Γ v B ∋ v' ⦂ A
  → (prf : ¬ v ≡ v')
  → Γ ∋ (Data.Fin.punchOut prf) ⦂ A
subst-neq v v' v-typing neq with v ≟ v'
... | yes refl = ⊥-elim (neq refl)
subst-neq fzero fzero _ _ | no neq = ⊥-elim (neq refl)
subst-neq {Γ = Γ ,- C} fzero (fsuc fin) (vsuc v-typing) _ | no neq = v-typing
subst-neq {Γ = Γ ,- C} (fsuc fin) fzero vzero _ | no neq = vzero
subst-neq {Γ = Γ ,- C} (fsuc fin) (fsuc fin') (vsuc v-typing) neq | no _ =
  vsuc (subst-neq fin fin' v-typing λ { assump → neq (cong fsuc assump) })

subst
  : ∀ {Γ : Ctx n}
  → liftΓ Γ v B ⊢ a ⦂ A → Γ ⊢ b ⦂ B
  → Γ ⊢ a [ v ≔ b ] ⦂ A
subst (ty-abs body) typing = ty-abs (subst body (weakening typing))
subst (ty-app f x) typing = ty-app (subst f typing) (subst x typing)
subst {v = v} {Γ = _} (ty-var {v = v'} v-typing) typing with v' ≟ v
... | yes refl = subst-eq v v-typing typing
subst {v = fzero} (ty-var {v = fzero} v-typing) typing | no neq = ⊥-elim (neq refl)
subst {v = fzero} (ty-var {v = fsuc v'} (vsuc v-typing)) typing | no neq = ty-var v-typing
subst {v = fsuc v} {Γ = Γ ,- C} (ty-var {v = fzero} vzero) typing | no neq = ty-var vzero
subst {v = fsuc v} {Γ = Γ ,- C} (ty-var {v = fsuc v'} (vsuc v-typing)) typing | no neq
  with v ≟ v'
... | yes eq = ⊥-elim (neq (cong fsuc (sym eq)))
... | no neq' = ty-var (vsuc (subst-neq v v' v-typing {!neq'!}))

Because I don't know the cause of the error, I'm not sure how to reproduce it in a simpler program.

Focusing on the typed hole gives:

Goal: ¬ v ≡ v'
————————————————————————————————————————————————————————————
typing   : (Γ ,- C) ⊢ b ⦂ B
v-typing : liftΓ Γ v B ∋ v' ⦂ A
neq      : fsuc v' ≡ fsuc v → Data.Empty.⊥
C        : Type
Γ        : Ctx n
b        : Term (suc n)   (not in scope)
A        : Type   (not in scope)
B        : Type   (not in scope)
neq'     : ¬ v ≡ v'
v'       : Fin (suc n)
v        : Fin (suc n)
n        : ℕ   (not in scope)

neq' clearly has the same type as the hole, and no equalities are listed.

However, when I try to fill the hole with neq', I get the following error:

(neq' x) !=
((λ { refl
        → Relation.Nullary.Reflects.invert (Relation.Nullary.ofⁿ neq')
          (Data.Fin.Properties.suc-injective (sym refl))
    })
 (cong fsuc x))
of type Data.Empty.⊥
when checking that the expression neq' has type ¬ v ≡ v'

What gives?

• Where is this equality constraint coming from?
• Since Data.Empty.⊥ is uninhabited, isn't it vacuously true that all inhabitants are equal? Why does the equality constraint matter?

I am using Agda version 2.6.1 and standard library version 1.3.

Answer 1

The equality constraints comes from the goal of the whole right hand side being of the form

(Γ ,- C) ⊢ 
  var (fsuc (punchOut 
             (λ x →
                (λ { refl → neq' (Data.Fin.Properties.suc-injective (sym refl)) })
                (cong fsuc x))))
  ⦂ A

While the inferred type for your suggested proof is

(Γ ,- _B_480) ⊢ var (fsuc (punchOut neq')) ⦂ A

Agda figured out that the only way those types could match is for neq' to equal the more complicated proof, that's why you are getting the error.

Regarding equality of function from ⊥, Agda does not assume they are all definitionally equal, because that would lead to undecidable typechecking in general.

The good news is that Agda already knows what the proof should be here! so if you replace your goal with _ it will infer what should go there.

... | no neq' = ty-var (vsuc {B = C} (subst-neq v v' v-typing _))