[Agda] Resolving a universe level problem

[Jesper Cockx]

Hi Marco,

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 *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.

-- Jesper

On Wed, Sep 9, 2020 at 9:01 AM Marko Dimjašević <marko at dimjasevic.net>
wrote:

> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200909/6eac483b/attachment.html>