CODEWITHSUNDEEP
agdatermination
Camelid
Camelid

Reputation: 1575

How to pass termination checking when recursing using map?

I have some Agda code like the following (trimmed down to focus on what I believe is the issue, which is the recursion using map):

open import Data.List using (List; map)

data Foo : Set where
  Bar : List Foo → Foo

data Foo2 : Set where
  Bar2 : List Foo2 → Foo2

process : Foo → Foo2
process (Bar x) = Bar2 (map process x)

{...}/Foo.agda:9,1-10,39
Termination checking failed for the following functions:
  process
Problematic calls:
  process
    (at {...}/Foo.agda:10,29-36)

How do I convince Agda that this function terminates (ideally in a simple way)?

Upvotes: 4

Views: 123

Answers (1)

gallais
gallais

Reputation: 12103

Unfortunately currently the only safe solution is to add a mutually defined version of map that is specialised.

{-# OPTIONS --safe --without-K #-}

open import Agda.Builtin.List

data Foo : Set where
  Bar : List Foo → Foo

data Foo2 : Set where
  Bar2 : List Foo2 → Foo2

process : Foo → Foo2
process′ : List Foo → List Foo2

process (Bar x) = Bar2 (process′ x)

process′ [] = []
process′ (f ∷ fs) = process f ∷ process′ fs

Upvotes: 3

Related Questions