在Idris中如何明确函数引用的接口成员所属接口？

你遇到的错误是因为Idris无法自动确定x所属的I a b实例——接口I有两个类型参数a和b，但成员x只依赖a，所以当你直接写x时，Idris会将b推断为未知的?b，导致找不到对应的接口实现。

有两种简单的解决方式：

方法一：显式限定接口成员的参数 #

直接在引用x时，指明它属于当前上下文的I a b实例，通过指定b参数消除歧义：

x' : I a b => a
x' = I.x {b=b}

这里I.x是接口成员的全称引用，{b=b}明确告诉Idris使用当前约束中指定的b类型，而非推断未知的?b。如果需要更严谨，也可以同时指定a参数：

x' : I a b => a
x' = I.x {a=a} {b=b}

方法二：通过类型注解辅助推断 #

如果场景允许，也可以在表达式中添加类型注解，让Idris明确x的类型对应I a b的约束：

x' : I a b => a
x' = x : a

不过这种方式不如第一种直接，因为核心歧义是接口实例的参数而非x的类型本身，更推荐使用第一种方法。

内容的提问来源于stack exchange，提问作者דניאל פ.ח.