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

Question

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"

Answer 1

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.