[Agda] Resolving a universe level problem

[Marko Dimjašević]

Dear Agda community,

I've been working out an alternative formalisation of De Bruijn indices to
that of provided in a book Programming Language Foundations in Agda:

https://plfa.github.io/DeBruijn/#13523

#_ : ∀ {Γ} → (n : ℕ) → Γ ⊢ lookup Γ n
# n  =  ` count n

My goal is to define an alternative #_ under the name #'_ such that it
relies on no postulates, which are used in functions count and lookup that
#_ depends on. I guess it should be possible to check statically that the
index provided does not go out of context bounds. However, I am stuck with
a universe level problem that I could use your help with.


In my attempt I end up with an error reading:

  /home/marko/projects/agda/plfa-exercises/plfa/DeBruijn.agda:104,42-60
  Set !=< suc n Nat.≤ Context-size Γ of type Set₁
  when checking that the expression n < Context-size Γ has type
  n < Context-size Γ

with the first line of #'_ highlighted in yellow, indicating the problem in
the return type of #'_.

Here is a self-contained code excerpt that leads to the error (my apologies
for not having a shorter snippet):


module DeBruijn where

open import Data.Empty using (⊥)
open import Data.Nat as Nat using (ℕ; zero; suc; _<_; s≤s; z≤n)
open import Data.Nat.Properties using (≤-pred)
open import Data.Unit using (⊤; tt)

infix  4 _⊢_
infix  4 _∋_
infixl 5 _,_

infixr 7 _⇒_

infix  5 ƛ_
infix  5 μ_
infixl 7 _·_
infix  8 `suc_
infix  9 `_
infix  9 S_

-- Types
data Type : Set where
  _⇒_ : Type → Type → Type
  `ℕ  : Type

-- Contexts
data Context : Set where
  ∅   : Context
  _,_ : Context → Type → Context

Context-size : Context → ℕ
Context-size ∅        =  zero
Context-size (c , _)  =  suc (Context-size c)

-- Variables and the lookup judgment
data _∋_ : Context → Type → Set where

  Z : ∀ {Γ A}
      ---------
    → Γ , A ∋ A

  S_ : ∀ {Γ A B}
    → Γ ∋ A
      ---------
    → Γ , B ∋ A

-- Terms and the typing judgment
data _⊢_ : Context → Type → Set where

  `_ : ∀ {Γ A}
    → Γ ∋ A
      -----
    → Γ ⊢ A

  ƛ_  : ∀ {Γ A B}
    → Γ , A ⊢ B
      ---------
    → Γ ⊢ A ⇒ B

  _·_ : ∀ {Γ A B}
    → Γ ⊢ A ⇒ B
    → Γ ⊢ A
      ---------
    → Γ ⊢ B

  `zero : ∀ {Γ}
      ---------
    → Γ ⊢ `ℕ

  `suc_ : ∀ {Γ}
    → Γ ⊢ `ℕ
      ------
    → Γ ⊢ `ℕ

  case : ∀ {Γ A}
    → Γ ⊢ `ℕ
    → Γ ⊢ A
    → Γ , `ℕ ⊢ A
      ----------
    → Γ ⊢ A

  μ_ : ∀ {Γ A}
    → Γ , A ⊢ A
      ---------
    → Γ ⊢ A

lookup' : (c : Context) → (n : ℕ) → (n < Context-size c) → Type
lookup' (_ , A) zero _         =  A
lookup' (Γ , _) (suc n) ≤-suc  =  lookup' Γ n (≤-pred ≤-suc)

count' : ∀ {Γ} → (n : ℕ) → (s : n < Context-size Γ) → Γ ∋ lookup' Γ n s
count' {_ , _} zero _         =  Z
count' {Γ , A} (suc n) ≤-suc  =  S (count' n (≤-pred ≤-suc))

_≤?_ : ∀ (m n : ℕ) → Set
zero  ≤? n      =  ⊤
suc m ≤? zero   =  ⊥
suc m ≤? suc n  =  m ≤? n

soundness-< : ∀(m n : ℕ) → suc m ≤? n → m < n
soundness-< zero    (suc n) tt    =  s≤s z≤n
soundness-< (suc m) (suc n) m≤?n  =  s≤s (soundness-< m n m≤?n)

#'_ : ∀ {Γ} → (n : ℕ) → Γ ⊢ lookup' Γ n (n < Context-size Γ)
#'_ {Γ} n  =  ` count' n (soundness-< n (Context-size Γ) tt)


-- 
Regards,
Marko Dimjašević <marko at dimjasevic.net>
https://dimjasevic.net/marko
Mastodon: https://mamot.fr/@mdimjasevic
PGP key ID:       056E61A6F3B6C9323049DBF9565EE9641503F0AA
Learn email self-defense! https://emailselfdefense.fsf.org
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: This is a digitally signed message part
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200909/e77950ae/attachment.sig>