考虑以下agda模块签名：

module EqList {a ℓ} {A : Set a} {_≈_ : Rel A ℓ} (eq≈ : IsEquivalence _≈_) where

我们可以定义列表中的成员资格，列表包含和列表等效性：

_∈_ : REL A (List A) _
_∈_ x = Any (x ≈_)

_⊑_ : Rel (List A) _
_⊑_ = _⊆_ on flip _∈_

_≋_ : Rel (List A) _
_≋_ = _⊑_ -[ _×_ ]- flip _⊑_

然后我们可以继续证明最后一个关系确实是等价关系：

isEq≋ : IsEquivalence _≋_
isEq≋ = record {
  refl = id,id ;
  sym = swap ;
  trans = zip (λ f g → g ∘ f) λ f g → f ∘ g }

传递性的证据是使我的问题产生的原因。 Agda接受先前的定义，而拒绝以下定义：

trans = zip (flip _∘_) _∘_

错误如下：

({x : A} → Any (_≈_ x) i → Any (_≈_ x) j) !=
((x : A) → Any (_≈_ x) j) because one is an implicit function type
and the other is an explicit function type
when checking that the expression _∘_ has type
(x : j ⊑ k) (y : i ⊑ j) → i ⊑ k

虽然这个错误感觉很奇怪，因为两个证明都应该是等效的（用表达式f替换表达式λ x → f x总是产生相同的结果）我可以有点理解它为什么如此行事：如何实例化_∘_的各种隐式参数是一个麻烦。但是，这种解释只是直观的，并不是非常确定的，因此我的问题是：

有人可以详细解释为什么类型检查器在第一种情况下成功而不在第二种情况下成功吗？

作为旁注，以下是模块的标题，以便使此示例自包含：

open import Relation.Binary.Core
open import Data.List hiding (zip)
open import Data.List.Any
open import Relation.Unary using (_⊆_)
open import Function
open import Data.Product

作为第二点，我知道已经回答了类似的问题：

How to get around the implicit vs explicit function type error?

但是所说的答案没有对这种令人惊讶的行为做任何深入的解释。