证明类型为Functor时出现类型推导错误的原因求解

• 核心错误是Functor类型的定义结构不符合函子的语义要求：你将原本属于fmap方法的多态参数{a b : Set}声明在了record的顶层参数位置，这会导致每个Functor实例只能对应固定的两个类型a、b，而不是函子要求的fmap可以对任意输入输出类型生效。
• 当你写functor_T : Functor T时，编译器会自动寻找Functor需要的两个隐式顶层参数a、b的填充值，但你没有提供任何可以推导这两个参数的上下文，因此编译器抛出了存在未确定元变量_a_22、_b_23的错误，这确实属于类型推导失败的情况，但根本诱因是Functor的定义逻辑错误。

将a、b从record的顶层参数移到fmap的内部多态参数位置即可，修改后的Functor定义如下：

record Functor (f : Set → Set) : Set where
  field
    fmap : ∀ {a b : Set} → (a → b) → f a → f b

修改后你原有的functor_T实现可以正常通过编译。

内容的提问来源于stack exchange，提问作者cstml