implicit issue

README.md

error for line 9 in check-minimal.agda

Failed to solve the following constraints:
  lsuc (_ℓ₀_52 ℓ₂) ⊔ (lsuc (_ℓ₁_53 ℓ₂) ⊔ lsuc (lsuc ℓ₂))
  = lsuc (_ℓ₀_52 ℓ₂) ⊔
    (lsuc (_ℓ₁_53 ℓ₂) ⊔ (lsuc (lsuc ℓ₂) ⊔ (lsuc .ℓ₁ ⊔ .ℓ₀)))
  lsuc .ℓ₁ ⊔ .ℓ₀ = _ℓ₀_52 ℓ₂ ⊔ lsuc (_ℓ₁_53 ℓ₂)
  _47 := λ {ℓ₀} {ℓ₁} ℓ₂ P₀ → P₀ → Set ℓ₁ [blocked on problem 26]
  [26] _P₀_41 ℓ₂ =< Set ℓ₀ : Set (lsuc ℓ₀)
  Is not empty type of sizes: _P₀_41 ℓ₂
  Is not empty type of sizes: _P₀_36 ℓ₂

check-level.agda

module check-level where

open import Agda.Primitive using (_⊔_)
  renaming (Level to 𝕃; lzero to 0ᴸ; lsuc to _+1ᴸ)

--
-- naked function types
--
module _ where

  -- context length = 0
  TP₀ : ∀ ℓ₀ → Set (ℓ₀ +1ᴸ)
  TP₀ ℓ₀ = Set ℓ₀
  id₀ : ∀ {ℓ₀} → TP₀ ℓ₀ → TP₀ ℓ₀
  id₀ P₀ = P₀
  TP₀' : ∀ ℓ₀ → id₀ (TP₀ (ℓ₀ +1ᴸ))
  TP₀' ℓ₀ = TP₀ ℓ₀

  -- context length = 1
  TP₁ : ∀ {ℓ₀} ℓ₁ → (P₀ : TP₀ ℓ₀) → Set (ℓ₀ ⊔ (ℓ₁ +1ᴸ))
  TP₁ ℓ₁ P₀ = (p₀ : P₀) → Set ℓ₁
  id₁ : ∀ {ℓ₀ ℓ₁} → {P₀ : TP₀ ℓ₀} → TP₁ ℓ₁ P₀ → TP₁ ℓ₁ P₀
  id₁ P₁ = P₁
  TP₁' : ∀ {ℓ₀} ℓ₁ → id₁ (TP₁ (ℓ₀ ⊔ (ℓ₁ +1ᴸ))) (TP₀ ℓ₀)
  TP₁' ℓ₁ = TP₁ ℓ₁

  -- context length = 2
  TP₂ : ∀ {ℓ₀ ℓ₁} ℓ₂ → {P₀ : TP₀ ℓ₀} → (P₁ : TP₁ ℓ₁ P₀) → Set (ℓ₀ ⊔ ℓ₁ ⊔ (ℓ₂ +1ᴸ))
  TP₂ ℓ₂ {P₀} P₁ = {p₀ : P₀} → (p₁ : P₁ p₀) → Set ℓ₂
  id₂ : ∀ {ℓ₀ ℓ₁ ℓ₂} → {P₀ : TP₀ ℓ₀} → {P₁ : TP₁ ℓ₁ P₀} → TP₂ ℓ₂ P₁ → TP₂ ℓ₂ P₁
  id₂ P₂ = P₂
  TP₂' : ∀ {ℓ₀ ℓ₁} ℓ₂ → id₂ {P₁ = TP₁ _} (TP₂ (ℓ₀ ⊔ ℓ₁ ⊔ (ℓ₂ +1ᴸ))) (TP₁ {ℓ₀} ℓ₁)
  TP₂' ℓ₂ = TP₂ ℓ₂

--
-- nominal record types
--
module _ where
  -- record identity wrapper
  record Id {ℓ} (It : Set ℓ) : Set ℓ where
    constructor ↑
    field ↓ : It
  open Id

  -- context length = 0
  WP₀ : ∀ ℓ₀ → TP₀ (ℓ₀ +1ᴸ)
  WP₀ ℓ₀ = Id (TP₀ ℓ₀)
  RP₀ : ∀ ℓ₀ → WP₀ (ℓ₀ +1ᴸ)
  RP₀ ℓ₀ = ↑ (WP₀ ℓ₀)
  _$₀ : ∀ {ℓ₀} → WP₀ ℓ₀ → TP₀ ℓ₀
  _$₀ = ↓
  RP₀' : ∀ ℓ₀ → (RP₀ (ℓ₀ +1ᴸ)) $₀
  RP₀' ℓ₀ = RP₀ ℓ₀

  -- context length = 1
  WP₁ : ∀ {ℓ₀} ℓ₁ → TP₁ (ℓ₀ ⊔ (ℓ₁ +1ᴸ)) (WP₀ ℓ₀)
  WP₁ ℓ₁ wP₀ = Id (TP₁ ℓ₁ (↓ wP₀))
  RP₁ : ∀ {ℓ₀} ℓ₁ → WP₁ (ℓ₀ ⊔ (ℓ₁ +1ᴸ)) (RP₀ ℓ₀)
  RP₁ ℓ₁ = ↑ (WP₁ ℓ₁)
  _$₁_ : ∀ {ℓ₀ ℓ₁} → {wP₀ : WP₀ ℓ₀} → WP₁ ℓ₁ wP₀ → TP₁ ℓ₁ (↓ wP₀)
  _$₁_ = ↓
  RP₁' : ∀ {ℓ₀} ℓ₁ → RP₁ (ℓ₀ ⊔ (ℓ₁ +1ᴸ)) $₁ RP₀ ℓ₀
  RP₁' ℓ₁ = RP₁ ℓ₁

  -- context length = 2
  WP₂ : ∀ {ℓ₀ ℓ₁} ℓ₂ → TP₂ (ℓ₀ ⊔ ℓ₁ ⊔ (ℓ₂ +1ᴸ)) (WP₁ {ℓ₀} ℓ₁)
  WP₂ ℓ₂ wP₁ = Id (TP₂ ℓ₂ (↓ wP₁))
  RP₂ : ∀ {ℓ₀ ℓ₁} ℓ₂ → WP₂ (ℓ₀ ⊔ ℓ₁ ⊔ (ℓ₂ +1ᴸ)) (RP₁ {ℓ₀} ℓ₁)
  RP₂ ℓ₂ = ↑ (WP₂ ℓ₂)
  _$₂_ : ∀ {ℓ₀ ℓ₁ ℓ₂} → {wP₀ : WP₀ ℓ₀} → {wP₁ : WP₁ ℓ₁ wP₀} → WP₂ ℓ₂ wP₁ → TP₂ ℓ₂ (↓ wP₁)
  _$₂_ = ↓
  RP₂' : ∀ {ℓ₀ ℓ₁} ℓ₂ → RP₂ (ℓ₀ ⊔ ℓ₁ ⊔ (ℓ₂ +1ᴸ)) $₂ RP₁ {ℓ₀} ℓ₁
  RP₂' ℓ₂ = RP₂ ℓ₂
--

check-minimal.agda

module check-minimal where

open import Agda.Primitive

TP₂ : ∀ {ℓ₀ ℓ₁} ℓ₂ → {P₀ : Set ℓ₀} → (P₁ : P₀ → Set ℓ₁) → Set _
TP₂ ℓ₂ {P₀} P₁ = {p₀ : P₀} → (p₁ : P₁ p₀) → Set ℓ₂
id₂ : ∀ {ℓ₀ ℓ₁ ℓ₂} → {P₀ : Set ℓ₀} → {P₁ : P₀ → Set ℓ₁} → TP₂ ℓ₂ P₁ → TP₂ ℓ₂ P₁
id₂ P₂ = P₂
TP₂' : ∀ {ℓ₀ ℓ₁} ℓ₂ → id₂ -- {P₁ = λ P₀ → P₀ → Set _}
    (TP₂ _) (λ (P₀ : Set ℓ₀) → P₀ → Set ℓ₁)
TP₂' ℓ₂ = TP₂ ℓ₂

check.agda

{-# OPTIONS --type-in-type #-}

module check where

--
-- naked function types
--
module _ where

  -- context length = 0
  TP₀ : Set
  TP₀ = Set
  id₀ : TP₀ → TP₀
  id₀ P₀ = P₀
  TP₀' : id₀ TP₀
  TP₀' = TP₀

  -- context length = 1
  TP₁ : (P₀ : TP₀) → Set
  TP₁ P₀ = (p₀ : P₀) → Set
  id₁ : {P₀ : TP₀} → TP₁ P₀ → TP₁ P₀
  id₁ P₁ = P₁
  TP₁' : id₁ TP₁ TP₀
  TP₁' = TP₁

  -- context length = 2
  TP₂ : {P₀ : TP₀} → (P₁ : TP₁ P₀) → Set
  TP₂ {P₀} P₁ = {p₀ : P₀} → (p₁ : P₁ p₀) → Set
  id₂ : {P₀ : TP₀} → {P₁ : TP₁ P₀} → TP₂ P₁ → TP₂ P₁
  id₂ P₂ = P₂
  TP₂' : id₂ {P₁ = TP₁} TP₂ TP₁ -- NO, can NOT infer implicit
  TP₂' = TP₂

--
-- nominal record types
--
module _ where

  -- record identity wrapper
  record Id (It : Set) : Set where
    constructor ↑
    field ↓ : It
  open Id

  -- context length = 0
  WP₀ : TP₀
  WP₀ = Id TP₀
  RP₀ : WP₀
  RP₀ = ↑ WP₀
  _$₀ : WP₀ → TP₀
  _$₀ = ↓
  RP₀' : RP₀ $₀
  RP₀' = RP₀

  -- context length = 1
  WP₁ : TP₁ WP₀
  WP₁ P₀ = Id (TP₁ (↓ P₀))
  RP₁ : WP₁ RP₀
  RP₁ = ↑ WP₁
  _$₁_ : {wP₀ : WP₀} → WP₁ wP₀ → TP₁ (↓ wP₀)
  _$₁_ = ↓
  RP₁' : RP₁ $₁ RP₀
  RP₁' = RP₁

  -- context length = 2
  WP₂ : TP₂ WP₁
  WP₂ wP₁ = Id (TP₂ (↓ wP₁))
  RP₂ : WP₂ RP₁
  RP₂ = ↑ WP₂
  _$₂_ : {wP₀ : WP₀} → {wP₁ : WP₁ wP₀} → WP₂ wP₁ → TP₂ (↓ wP₁)
  _$₂_ = ↓
  RP₂' : RP₂ $₂ RP₁ -- YES, can infer implicits
  RP₂' = RP₂

--