<div dir="ltr"><div>Hi Marco,</div><div><br></div><div>Here Agda is complaining that you gave it a type (something of type `Set`), but it expected something of type `suc n Nat.≤ Context-size Γ`. Indeed, you gave `n < Context-size Γ` in the type of #'_, but you should've given a<i> </i>*proof* of that type. One way to fix the problem is by adding an extra argument of this type to the function `#'_`. By adding an argument of this type, you make explicit the precondition that the number `n` should not be greater than the length of the context, which was implicit in the plfa version.</div><div><br></div><div>-- Jesper<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, Sep 9, 2020 at 9:01 AM Marko Dimjašević <<a href="mailto:marko@dimjasevic.net">marko@dimjasevic.net</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Dear Agda community,<br>
<br>
I've been working out an alternative formalisation of De Bruijn indices to<br>
that of provided in a book Programming Language Foundations in Agda:<br>
<br>
<a href="https://plfa.github.io/DeBruijn/#13523" rel="noreferrer" target="_blank">https://plfa.github.io/DeBruijn/#13523</a><br>
<br>
#_ : ∀ {Γ} → (n : ℕ) → Γ ⊢ lookup Γ n<br>
# n  =  ` count n<br>
<br>
My goal is to define an alternative #_ under the name #'_ such that it<br>
relies on no postulates, which are used in functions count and lookup that<br>
#_ depends on. I guess it should be possible to check statically that the<br>
index provided does not go out of context bounds. However, I am stuck with<br>
a universe level problem that I could use your help with.<br>
<br>
<br>
In my attempt I end up with an error reading:<br>
<br>
  /home/marko/projects/agda/plfa-exercises/plfa/DeBruijn.agda:104,42-60<br>
  Set !=< suc n Nat.≤ Context-size Γ of type Set₁<br>
  when checking that the expression n < Context-size Γ has type<br>
  n < Context-size Γ<br>
<br>
with the first line of #'_ highlighted in yellow, indicating the problem in<br>
the return type of #'_.<br>
<br>
Here is a self-contained code excerpt that leads to the error (my apologies<br>
for not having a shorter snippet):<br>
<br>
<br>
module DeBruijn where<br>
<br>
open import Data.Empty using (⊥)<br>
open import Data.Nat as Nat using (ℕ; zero; suc; _<_; s≤s; z≤n)<br>
open import Data.Nat.Properties using (≤-pred)<br>
open import Data.Unit using (⊤; tt)<br>
<br>
infix  4 _⊢_<br>
infix  4 _∋_<br>
infixl 5 _,_<br>
<br>
infixr 7 _⇒_<br>
<br>
infix  5 ƛ_<br>
infix  5 μ_<br>
infixl 7 _·_<br>
infix  8 `suc_<br>
infix  9 `_<br>
infix  9 S_<br>
<br>
-- Types<br>
data Type : Set where<br>
  _⇒_ : Type → Type → Type<br>
  `ℕ  : Type<br>
<br>
-- Contexts<br>
data Context : Set where<br>
  ∅   : Context<br>
  _,_ : Context → Type → Context<br>
<br>
Context-size : Context → ℕ<br>
Context-size ∅        =  zero<br>
Context-size (c , _)  =  suc (Context-size c)<br>
<br>
-- Variables and the lookup judgment<br>
data _∋_ : Context → Type → Set where<br>
<br>
  Z : ∀ {Γ A}<br>
      ---------<br>
    → Γ , A ∋ A<br>
<br>
  S_ : ∀ {Γ A B}<br>
    → Γ ∋ A<br>
      ---------<br>
    → Γ , B ∋ A<br>
<br>
-- Terms and the typing judgment<br>
data _⊢_ : Context → Type → Set where<br>
<br>
  `_ : ∀ {Γ A}<br>
    → Γ ∋ A<br>
      -----<br>
    → Γ ⊢ A<br>
<br>
  ƛ_  : ∀ {Γ A B}<br>
    → Γ , A ⊢ B<br>
      ---------<br>
    → Γ ⊢ A ⇒ B<br>
<br>
  _·_ : ∀ {Γ A B}<br>
    → Γ ⊢ A ⇒ B<br>
    → Γ ⊢ A<br>
      ---------<br>
    → Γ ⊢ B<br>
<br>
  `zero : ∀ {Γ}<br>
      ---------<br>
    → Γ ⊢ `ℕ<br>
<br>
  `suc_ : ∀ {Γ}<br>
    → Γ ⊢ `ℕ<br>
      ------<br>
    → Γ ⊢ `ℕ<br>
<br>
  case : ∀ {Γ A}<br>
    → Γ ⊢ `ℕ<br>
    → Γ ⊢ A<br>
    → Γ , `ℕ ⊢ A<br>
      ----------<br>
    → Γ ⊢ A<br>
<br>
  μ_ : ∀ {Γ A}<br>
    → Γ , A ⊢ A<br>
      ---------<br>
    → Γ ⊢ A<br>
<br>
lookup' : (c : Context) → (n : ℕ) → (n < Context-size c) → Type<br>
lookup' (_ , A) zero _         =  A<br>
lookup' (Γ , _) (suc n) ≤-suc  =  lookup' Γ n (≤-pred ≤-suc)<br>
<br>
count' : ∀ {Γ} → (n : ℕ) → (s : n < Context-size Γ) → Γ ∋ lookup' Γ n s<br>
count' {_ , _} zero _         =  Z<br>
count' {Γ , A} (suc n) ≤-suc  =  S (count' n (≤-pred ≤-suc))<br>
<br>
_≤?_ : ∀ (m n : ℕ) → Set<br>
zero  ≤? n      =  ⊤<br>
suc m ≤? zero   =  ⊥<br>
suc m ≤? suc n  =  m ≤? n<br>
<br>
soundness-< : ∀(m n : ℕ) → suc m ≤? n → m < n<br>
soundness-< zero    (suc n) tt    =  s≤s z≤n<br>
soundness-< (suc m) (suc n) m≤?n  =  s≤s (soundness-< m n m≤?n)<br>
<br>
#'_ : ∀ {Γ} → (n : ℕ) → Γ ⊢ lookup' Γ n (n < Context-size Γ)<br>
#'_ {Γ} n  =  ` count' n (soundness-< n (Context-size Γ) tt)<br>
<br>
<br>
-- <br>
Regards,<br>
Marko Dimjašević <<a href="mailto:marko@dimjasevic.net" target="_blank">marko@dimjasevic.net</a>><br>
<a href="https://dimjasevic.net/marko" rel="noreferrer" target="_blank">https://dimjasevic.net/marko</a><br>
Mastodon: <a href="https://mamot.fr/@mdimjasevic" rel="noreferrer" target="_blank">https://mamot.fr/@mdimjasevic</a><br>
PGP key ID:       056E61A6F3B6C9323049DBF9565EE9641503F0AA<br>
Learn email self-defense! <a href="https://emailselfdefense.fsf.org" rel="noreferrer" target="_blank">https://emailselfdefense.fsf.org</a><br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>