agda - Agda はどのようにして `Vec.foldl` への暗黙の引数を推測していますか?

Question

foldl : ∀ {a b} {A : Set a} (B : ℕ → Set b) {m} →
        (∀ {n} → B n → A → B (suc n)) →
        B zero →
        Vec A m → B m
foldl b _⊕_ n []       = n
foldl b _⊕_ n (x ∷ xs) = foldl (λ n → b (suc n)) _⊕_ (n ⊕ x) xs

上記の関数をリーンに翻訳すると、その本当の形が実際には...

def foldl : ∀ (P : ℕ → Type a) {n : nat}
    (f : ∀ {n}, P n → α → P (n+1)) (s : P 0)
    (l : Vec α n), P n
| P 0 f s (nil _) := s
| P (n+1) f s (cons x xs) := foldl (fun n, P (n+1)) (λ n, @f (n+1)) (@f 0 s x) xs

fAgda が暗黙の引数を正しく推論できることは本当に印象的です。それはどのようにやっているのですか？