Functor and monad instances that termination-check

Question

This follows up on another question from several months ago. The problem relates to termination-checking in Agda using sized types.

Here's the preamble:

{-# 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)

Contexts are represented polymorphically using de Bruijn indices. The details of tries aren't important, so I've left the type empty, and simply postulate ᵀ<$>, an fmap-like operation for tries.

What I'd like to do is have the following termination-check. The size indices given here are my crude first attempt, but the termination-checker still rejects the code.

   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

How should I fix my indices? I'd also appreciate some help understanding the problem. For example I'm guessing that having

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

as the type of substitutions may be problematic because of the ↑, but I seem to need this in order to allow var ∘ f to be a suitable argument to extend. (Also curious as to why this doesn't lead to inconsistent constraints, but rather to code that fails the regular Agda termination-checker.)

Answer 1

If you generalize extend₁ to extend′, you can define functoriality without reference to substitution, and everything termination checks fine:

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