无法消除名称的歧义：Idris中的Prelude.List。++，Prelude.Strings。++错误

Question

目前我正在尝试创建一个函数，它将（a - > a - > a）的类型作为Idris中的参数，而正确的函数是idris的列表的++命令，不幸的是我得到了这个错误

ListMonoid：（A：Type） - > RawMonoid ListMonoid A =（A **（[]，（++）））

当使用期望类型RawMonoid检查ListMonoid的右侧时

无法消除名称的歧义：Prelude.List。++，Prelude.Strings。++

Raw Monoid是下面的数据类型

RawMonoid：输入RawMonoid =（M **（M，M - > M - > M））infixl 6＆

在我看来，它不知道使用哪个++，有没有办法在通话中指定这个？

Answer 1

您可以限定对（++）的引用，例如

ListMonoid A = (A ** ([], List.(++)) )

并且还有with关键字，它将模块名称作为其第一个参数 - 它基本上意味着，“在下面的表达式中，首先查看此模块以解析名称”，例如

ListMonoid A = (A ** ([], with List (++)) )

但是，这两个代码都会给我带来以下类型错误：

    Type mismatch between
            List a -> List a -> List a (Type of (++))
    and
            A -> A -> A (Expected type)

如果我写：

ListMonoid A = (List A ** ([], (++)) )

它能够根据周围的类型约束选择正确的(++)。