# How to convince Agda that definition is terminating in the presence of unapplied recursion?

In the following, termination check fails for Df:

open import Agda.Builtin.Nat  using (Nat; zero; suc)
open import Agda.Builtin.Unit using (⊤; tt)

data A (P : Nat → Set) : Set where
a : A P

Df : Nat → Set
Df zero    = ⊤
Df (suc n) = A Df -- Problematic call "Df"


Can Df be changed to pass termination checker? I know that Df can alternatively be defined as a data type:

data Di : Nat → Set where
d  : Di zero
ds : ∀{x} → A Di → Di (suc x)


But what are the implications of using Di instead of Df? And it doesn't work with functions returning not a Set:

g : (⊤ → ⊤) → ⊤
g f = tt

f : ⊤ → ⊤
f tt = g f -- Problematic call "f"


My actual use-case is a Value : Type → Set function, where Type is either a constant or struct : List Type → Type. Termination check fails in Value (struct xs) = All Value xs.

open import Agda.Builtin.Bool using (Bool)
open import Agda.Builtin.List using (List; _∷_; [])
open import Agda.Builtin.Nat  using (Nat)

data All {A : Set} (P : A → Set) : List A → Set where
[]  : All P []
_∷_ : ∀{x xs} → P x → All P xs → All P (x ∷ xs)

data Type : Set where
nat    : Type
bool   : Type
struct : List Type → Type

Value : Type → Set
Value nat         = Nat
Value bool        = Bool
Value (struct ts) = All Value ts -- Problematic calls: "Value"

• A naive solution would be to unroll the definition of All in a recursive form, by defining branches of Value (struct []) = ⊤, Value (struct (x ∷ xs)) = Value x × Value (struct xs), but that might not be the solution you are looking for. A naive well-founded recursion would fail in your Df case, as Df takes no arguments in the recursive call and similarly in the Value case, you would have to essentially construct a proof about equivalence of the All definition to some well-founded recursive call, but the proof might allow you to use preexisting facts about All.
– Timo
Oct 14, 2022 at 0:56
• The code examples here are perhaps too simplified, making it hard to see which solutions are acceptable. For example, A P always has 1 inhabitant, so Df n could just be ⊤ in all cases. Maybe you want to make A a postulate or parameter, but, as I say, it's hard to know. Oct 14, 2022 at 7:32
• Can you give an example that is not trivially fixed by avoiding the recursion, and gives an equivalent result? Oct 14, 2022 at 8:44
• @AndrejBauer I've updated the post with an example. I don't know how recursion can be avoided there. Oct 14, 2022 at 12:00
• At first I tried making a "depth" metric which allowed to define Value : ∀{n T} → Depth n T → Set. To remove the depth argument I made a function that calculates depth for any Type and then passes it to Value, but this function suffered the original problem. As @Nift suggested, unrolling All in plain Value or All.tabulate in my function allows them to pass termination checker. It doesn't seem to pose any problems besides disallowing to use Alls properties which I probably don't need anyway. Oct 14, 2022 at 17:52

I can think of two ways of solving the problem.

First, make All and Value mutually recursive so that you don't have to pass Value around:

open import Agda.Builtin.Bool using (Bool)
open import Data.List using (List; _∷_; []; map)
open import Agda.Builtin.Nat  using (Nat)

data Type : Set where
nat    : Type
bool   : Type
struct : List Type → Type

Value : Type → Set
data All : List Type → Set

data All where
[]  : All []
_∷_ : ∀ {t ts} → Value t → All ts → All (t ∷ ts)

Value nat         = Nat
Value bool        = Bool
Value (struct ts) = All ts


Second, map Value before you pass the arguments to All (here I renamed All to Struct), but now we need an auxiliary map-Value:

open import Agda.Builtin.Bool using (Bool)
open import Data.List using (List; _∷_; []; map)
open import Agda.Builtin.Nat  using (Nat)

data Type : Set where
nat    : Type
bool   : Type
struct : List Type → Type

data Struct : List Set → Set where
[]  : Struct []
_∷_ : ∀ {t ts} → t → Struct ts → Struct (t ∷ ts)

Value : Type → Set
map-Value : List Type → List Set

Value nat         = Nat
Value bool        = Bool
Value (struct ts) = Struct (map-Value ts)

map-Value [] = []
map-Value (t ∷ ts) = Value t ∷ map-Value ts


The silly thing is that replacing map-Value ts with map Value ts brings back the problem.

• I tried writing mappings between Value (struct ts) and All Value ts using both your solutions, fully inlined All and a Value defined as a data type. Your second solution and full inlining required to match on (implicit) ts, while the others allowed to directly match on Value (which is maybe convenient? at least less verbose). Since I don't know if GADT approach will bring any advantages, I'll go with your first solution for now since it doesn't require casts between Value nat and Nat. Thanks for an answer. Oct 14, 2022 at 19:57
• Requiring some kind of mutual definition here is a pretty well-known shortcoming of Agda's termination checker. The check is just not very compositional, and recursive definitions can't just be inlined for the checker to 'see through' them. This is the reason that sized types were invented, and although I'm not a great fan of them, I'm also not aware of any other promising solutions. Oct 15, 2022 at 18:48
• On the flip side: most rigorous specifications of inductive definitions I'm aware of would say that Type is not an actual specification, and it must be compiled into essentially a mutual definition between Type and List Type. Then it is no surprise that recursive definitions on Type require a mutual definition on List Type. The foundational accounts for inductive definitions themselves fail to be compositional in the same way as Agda's termination checker. (Possibly recent work by Henning Basold does not have this problem.) Oct 15, 2022 at 19:04