Merge of sorted lists with sized types

Question

Suppose we have a datatype of sorted lists, with proof-irrelevant sorting witnesses. We'll use Agda's experimental sized types feature, so that we can hopefully get some recursive functions over the datatype to pass Agda's termination checker.

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

open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P

module ListMerge
   {𝒂 ℓ}
   (A : Set 𝒂)
   {_<_ : Rel A ℓ}
   (isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_) where

   open import Level
   open import Size

   data SortedList (l u : A) : {ι : _} → Set (𝒂 ⊔ ℓ) where
      [] : {ι : _} → .(l < u) → SortedList l u {↑ ι}
      _∷[_]_ : {ι : _} (x : A) → .(l < x) → (xs : SortedList x u {ι}) → 
               SortedList l u {↑ ι}

Now, a classic function one would like to define over such a data structure is merge, which takes two sorted lists, and outputs a sorted list containing exactly the elements of the input lists.

   open IsStrictTotalOrder isStrictTotalOrder

   merge : ∀ {l u} → SortedList l u → SortedList l u → SortedList l u
   merge xs ([] _) = xs
   merge ([] _) ys = ys
   merge (x ∷[ l<x ] xs) (y ∷[ l<y ] ys) with compare x y
   ... | tri< _ _ _ = x ∷[ l<x ] (merge xs (y ∷[ _ ] ys))
   merge (x ∷[ l<x ] xs) (.x ∷[ _ ] ys) | tri≈ _ P.refl _ = 
      x ∷[ l<x ] (merge xs ys)
   ... | tri> _ _ _ = y ∷[ l<y ] (merge (x ∷[ _ ] xs) ys)

This function seems innocuous enough, except that it can be tricky to convince Agda that it's total. Indeed, without any explicit size indices, the function fails to termination-check. One option is to split the function into two mutually recursive definitions. This works, but adds a certain amount of redundancy to both the definition and associated proofs.

But equally, I'm not sure whether it is even possible to give size indices explicitly so that merge has signature that Agda will accept. These slides discuss mergesort explicitly; the signature given there suggests that the following should work:

   merge′ : ∀ {l u} → {ι : _} → SortedList l u {ι} → 
                      {ι′ : _} → SortedList l u {ι′} → SortedList l u
   merge′ xs ([] _) = xs
   merge′ ([] _) ys = ys
   merge′ (x ∷[ l<x ] xs) (y ∷[ l<y ] ys) with compare x y
   ... | tri< _ _ _ = x ∷[ l<x ] (merge′ xs (y ∷[ _ ] ys))
   merge′ (x ∷[ l<x ] xs) (.x ∷[ _ ] ys) | tri≈ _ P.refl _ = 
      x ∷[ l<x ] (merge′ xs ys)
   ... | tri> _ _ _ = y ∷[ l<y ] (merge' (x ∷[ _ ] xs) ys)

Here what we're doing is allowing the inputs to have arbitrary (and different) sizes, and specifying that the output has size ∞.

Unfortunately, with this signature, Agda complains that .ι != ∞ of type Size, when checking the body xs of the first clause of the definition. I don't claim to understand sized types very well, but I was under the impression that any size ι would unify with ∞. Perhaps the semantics of sized types have changed since those slides were written.

So, is my scenario a use-case for which sized type were intended? If so, how should I should use them? If sized types aren't appropriate here, why does the first version of merge above not termination-check, given that the following does:

open import Data.Nat
open import Data.List
open import Relation.Nullary

merge : List ℕ → List ℕ → List ℕ
merge (x ∷ xs) (y ∷ ys) with x ≤? y
... | yes p = x ∷ merge xs (y ∷ ys)
... | _     = y ∷ merge (x ∷ xs) ys 
merge xs ys = xs ++ ys

Answer 1

Interestingly enough, your first version is actually correct. I mentioned that Agda enables few extra rules considering Size, one of them being ↑ ∞ ≡ ∞. By the way, you can confirm it via:

↑inf : ↑ ∞ ≡ ∞
↑inf = refl

Well, this led me to investigate what the other rules are. I found the rest of them inside Andreas Abel's slides on sized types (can be found here):

• ↑ ∞ ≡ ∞
• i ≤ ↑ i ≤ ∞
• T {i} <: T {↑ i} <: T {∞}

The <: relation is the subtyping relation, which you might know from object oriented languages. There's also a rule associated with this relation, the subsumption rule:

Γ ⊢ x : A   Γ ⊢ A <: B
────────────────────── (sub)
      Γ ⊢ x : B

So, if you have a value x of type A and you know that A is a subtype of B, you can treat x as being of type B as well. This seemed strange, because following the subtyping rule for sized types, you should be able to treat a value of type SortedList l u {ι} as SortedList l u.

So I did bit of a digging and found this bug report. And indeed, the problem is just that Agda doesn't correctly recognize the size and the rule doesn't fire. All I needed to do was to rewrite the definition of SortedList to:

data SortedList (l u : A) : {ι : Size} → Set (𝒂 ⊔ ℓ) where
  -- ...

And that's it!

---

As an addendum, here's the code I used for testing:

data ℕ : {ι : _} → Set where         -- does not work
-- data ℕ : {ι : Size} → Set where   -- works
  zero : ∀ {ι} →         ℕ {↑ ι}
  suc  : ∀ {ι} → ℕ {ι} → ℕ {↑ ι}

test : ∀ {ι} → ℕ {ι} → ℕ
test n = n