Экземпляры функтора и монады, которые проверяют завершение

Question

Это следует за другим вопросом от нескольких месяцев назад. Проблема связана с проверкой завершения в Agda с использованием типоразмеров.

Вот преамбула:

{-# OPTIONS --sized-types #-}

module Term where

   open import Data.Empty
   open import Function
   open import Relation.Binary.PropositionalEquality
   open import Size

   data Type : Set where
       : Type
      _+_ _⇾_ : Type → Type → Type

   Cxt : Set₁
   Cxt = Type → Set

   -- Adapted from "Names for free: polymorphic views of names and binders",
   -- by Bernardy and Pouillard.
   data _∷ʳ_ (Γ : Cxt) (V : Cxt) (A : Type) : Set where
      here : V A → (Γ ∷ʳ V) A
      there : Γ A → (Γ ∷ʳ V) A

   -- A renaming from Γ to Γ′.
   _⇢_ : Cxt → Cxt → Set
   Γ ⇢ Γ′ = ∀ {A} → Γ A → Γ′ A

   infixr 19 _⇢_

   -- Extend a renaming under a binder.
   extend₁ : ∀ {Γ Γ′} → Γ ⇢ Γ′ → ∀ {A} → Γ ∷ʳ (_≡_ A) ⇢ Γ′ ∷ʳ (_≡_ A)
   extend₁ f (here x) = here x
   extend₁ f (there x) = there (f x)

   data Trie (Γs : Cxt → Cxt) (C : Type) : {ι : Size} → Type → Set where

   postulate
      _ᵀ<$>_ : ∀ {Γs Γs′ : Cxt → Cxt} →
              (∀ {C Γ} → (Γs Γ C → Γs′ Γ C)) →
              ∀ {ι C} → (λ A → Trie Γs A {ι} C) ⇢ (λ A → Trie Γs′ A {ι} C)

Контексты представлены полиморфно с использованием индексов де Брюина. Детали попыток не важны, поэтому я оставил тип пустым и просто постулирую ᵀ<$>, fmap-подобная операция для попыток.

Что я хотел бы сделать, так это выполнить следующую проверку завершения. Приведенные здесь индексы размера - моя грубая первая попытка, но проверка завершения все еще отклоняет код.

   data Term (Γ : Type → Set) : {ι : Size} → Type → Set where
      var : ∀ {ι A} → Γ A → Term Γ {↑ ι} A
      match_as_ : ∀ {ι A A′} → Term Γ {ι} A →
                  Trie (λ Γ′ → Term (Γ ∷ʳ Γ′) {ι}) A′ A → Term Γ {↑ ι} A′
      fun : ∀ {ι A B} → Term (Γ ∷ʳ (_≡_ A)) {ι} B → Term Γ {↑ ι} (A ⇾ B)

   _<$>_ : ∀ {ι} {Γ Γ′ : Type → Set} → Γ ⇢ Γ′ → Term Γ {ι} ⇢ Term Γ′ {ι}
   _*_ : ∀ {ι Γ Γ′} → (∀ {ι} → Γ ⇢ Term Γ′ {↑ ι}) → Term Γ {ι} ⇢ Term Γ′ {ι}
   extend : ∀ {ι Γ Γ′ A} → (∀ {ι} → Γ ⇢ Term Γ′ {↑ ι}) → 
            (Γ ∷ʳ A) ⇢ Term (Γ′ ∷ʳ A) {↑ ι}

   -- Functoriality.
   f <$> var x = var (f x)
   f <$> match e as m = match f <$> e as (_*_ (extend (var ∘ f)) ᵀ<$> m)
   f <$> fun e = fun (extend₁ f <$> e)

   -- Monadic bind, a.k.a. substitution.
   θ * var x = θ x
   θ * (match e as m) = match θ * e as (_*_ (extend θ) ᵀ<$> m)
   θ * fun e = fun (extend θ * e)

   -- Extend a substitution under a binder.
   extend θ (here x) = var (here x)
   extend θ (there x) = there <$> θ x

Как мне исправить свои показатели? Я также был бы признателен за помощь в понимании проблемы. Например, я предполагаю, что имея

∀ {ι} → Γ ⇢ Term Γ′ {↑ ι}

так как тип замен может быть проблематичным из-за ↑, но мне кажется, это нужно для того, чтобы var ∘ f быть подходящим аргументом extend, (Также любопытно, почему это не приводит к противоречивым ограничениям, а скорее к коду, который не проходит обычную проверку завершения Agda.)

Answer 1

Если вы обобщаете extend₁ в extend′Вы можете определить функториальность без ссылки на подстановку, и все проверки завершаются нормально:

extend′ : ∀ {Γ Γ′} → Γ ⇢ Γ′ → ∀ {Δ} → Γ ∷ʳ Δ ⇢ Γ′ ∷ʳ Δ
extend′ f (here  x) = here  x
extend′ f (there x) = there (f x)

_<$>_  : ∀ {ι} {Γ Γ′ : Type → Set}
         → Γ ⇢ Γ′
         → Term Γ {ι} ⇢ Term Γ′ {ι}

_*_    : ∀ {ι Γ Γ′}
         → (∀ {ι} → Γ ⇢ Term Γ′ {↑ ι})
         → Term Γ {ι} ⇢ Term Γ′ {ι}

extend : ∀ {ι Γ Γ′ A}
         → (∀ {ι} → Γ ⇢ Term Γ′ {↑ ι})
         → (Γ ∷ʳ A) ⇢ Term (Γ′ ∷ʳ A) {↑ ι}

-- Functoriality.
f <$> var x = var (f x)
f <$> fun e = fun (extend′ f <$> e)
f <$> match e as m =  match f <$> e as (_<$>_ (extend′ f) ᵀ<$> m)

-- Monadic bind, a.k.a. substitution.
θ * var x = θ x
θ * fun e = fun (extend θ * e)
θ * (match e as m) = match θ * e as (_*_ (extend θ) ᵀ<$> m)

-- Extend a substitution under a binder.
extend θ (here  x) = var (here x)
extend θ (there x) = there <$> θ x