[Agda] Some problems with termination checker

[v0ιd]

Dear list,
I try to define a zip-with function without pattern matching through
universal constructor eliminator for Lists.

id : {a : _} → {A : Set a} → A → A
id x = x

data List {a} (A : Set a) : Set a where
 nil : List A
 cons : A → List A → List A

fold : {a b c : _} → {A : Set a} → {B : Set b} → {C : Set c} → List A → (A
→ List A → ((B → C) → B → C) → (B → C) → B → C) → (B → C) → B → C
fold nil _ fs s = fs s
fold (cons x xs) f = f x xs (fold xs f)

zip-with : {a b c : _} → {A : Set a} → {B : Set b} → {C : Set c} → (A → B →
C) → List A → List B → List C
zip-with f x y = fold x (λ ξ ξs _ _ _ → fold y (λ η ηs _ _ _ → cons (f ξ η)
(zip-with f ξs ηs)) id nil) id nil

But it fails termination checking.

Termination checking failed for the following functions:
  zip-with
Problematic calls:
  zip-with f ξs ηs

I would not want to suppress termination checking at all with {-#
TERMINATING #-}.
What can I do here? Maybe it makes sense somehow to improve termination
checker for so obvious cases?
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180217/9a85fc20/attachment.html>