Unifier creates ill-formed telescope for pruned meta (de Bruijn index vs. level problem).

[Oinkium]

When type-checking some AGDA code the other day, I got the following message:

An internal error has occurred. Please report this as a bug.
Location of the error: src/full/Agda/TypeChecking/Telescope.hs:71

Type-checking the following code reproduces the bug:

module Bug where

open import Relation.Binary.PropositionalEquality
  using (_≡_; refl)
open import Data.Fin
  using (toℕ; zero; suc)

toℕ-injective : ∀ {m n a b} → toℕ a ≡ toℕ b → a ≡ b
toℕ-injective {m} {n} {zero} {zero} _ = refl
toℕ-injective {m} {n} {zero} {suc b} ()
toℕ-injective {m} {n} {suc a} {zero} ()
toℕ-injective {m} {n} {suc a} {suc b} p = toℕ-injective p

[UlfNorell]

The internal error is clearly a bug, but it's worth noting that the example as written is not type correct. Here's what you can get away with proving (which doesn't trigger the internal error):

open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; cong)
open import Data.Fin
  using (Fin; toℕ; zero; suc)
open import Data.Nat
  using (ℕ; zero; suc)

suc-injective : ∀ {m n} → ℕ.suc m ≡ suc n → m ≡ n
suc-injective refl = refl

toℕ-injective : ∀ {n} {a b : Fin n} → toℕ a ≡ toℕ b → a ≡ b
toℕ-injective {n} {zero} {zero} _ = refl
toℕ-injective {n} {zero} {suc b} ()
toℕ-injective {n} {suc a} {zero} ()
toℕ-injective {n} {suc a} {suc b} p = cong suc (toℕ-injective (suc-injective p))

[UlfNorell]

Here's a simplified example that exhibits the problem:

open import Agda.Builtin.Nat

data Fin : Nat → Set where
  zero : ∀ {n} → Fin (suc n)

postulate
  T     : Nat → Set
  mkT   : ∀ {n} → T n
  toNat : ∀ {n} → Fin n → Nat

toNat-injective : ∀ {X Y} a → T (toNat a)
toNat-injective zero = mkT

[UlfNorell]

It looks like a problem with mvPermutations triggered at Agda.TypeChecking.Rules.LHS.Unify.hs:765. Not sure if the permutation is wrong or the unifier is making incorrect assumptions.

[andreasabel]

Checks fine with 2.4.2.5, must be a regression introduced in 2.5.

[andreasabel]

It seems that the function permuteTel in Agda.TypeChecking.Telescope is buggy.

permuteTel :: Permutation -> Telescope -> Telescope
permuteTel perm tel =
  let names = permute perm $ teleNames tel
      types = permute perm $ renameP __IMPOSSIBLE__ perm $ flattenTel tel
  in  unflattenTel names types

Correct is renameP __IMPOSSIBLE__ (flipP perm), to turn the de Bruijn levels of perm into de Bruijn indices for the substitution. Here is the analysis:

     tel                     = (A : Set) (X : _18 A) (i : Fin (_m_23 A X))
     tel (de Bruijn)         = 2:Set, 1:_18 @0, 0:Fin(_m_23 @1 @0)
     flattenTel tel          = 2:Set, 1:_18 @0, 0:Fin(_m_23 @1 @0) |- [ Set, _18 @2, Fin (_m_23 @2 @1) ]
     perm                    = 0,1,2 -> 0,1  (picks the first two)
     renaming _ perm         = [var 0, var 1, error]  -- THE WRONG RENAMING!
     renaming _ (flipP perm) = [error, var 1, var 0]  -- The correct renaming!
     apply to flattened tel  = ... |- [ Set, _18 @1, Fin (_m_23 @1 @0) ]
     permute perm it         = ... |- [ Set, _18 @1 ]
     unflatten (de Bruijn)   = 1:Set, 0: _18 @0
     unflatten               = (A : Set) (X : _18 A)

[andreasabel]

@asr: could this be included in 2.5.2?

[asr]

@asr: could this be included in 2.5.2?

Done in 1c2a4ee12cc9b0bf72f0cfec9b056a867ad9f7a.

[andreasabel]

Thanks!