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"
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 yourDf
case, asDf
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. $\endgroup$A P
always has 1 inhabitant, soDf n
could just be⊤
in all cases. Maybe you want to makeA
a postulate or parameter, but, as I say, it's hard to know. $\endgroup$Value : ∀{n T} → Depth n T → Set
. To remove the depth argument I made a function that calculates depth for anyType
and then passes it toValue
, but this function suffered the original problem. As @Nift suggested, unrollingAll
in plainValue
orAll.tabulate
in my function allows them to pass termination checker. It doesn't seem to pose any problems besides disallowing to useAll
s properties which I probably don't need anyway. $\endgroup$