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

Question

目前我正在尝试创建一个采用以下类型的函数 (a -> a -> a) 作为 Idris 中的参数，正确的功能是 ++ 命令用于 idris 中的列表，不幸的是我收到了这个错误

ListMonoid : (A : Type) -> RawMonoid ListMonoid A = (A ** ([], (++)) )

检查 ListMonoid 右侧的预期类型时 RawMonoid

无法消除名称歧义：Prelude.List.++, Prelude.Strings.++

Raw Monoid 是下面的一种数据类型

RawMonoid : 类型 RawMonoid = (M ** (M , M -> M -> M)) 中缀 6 &

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

Answer 1

您可以限定对 (++) 的引用，例如

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

还有 with 关键字，它将模块名称作为第一个参数 - 它基本上意味着 "in the following expression, look in this module first to resolve names"，例如

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 ** ([], (++)) )

它能够根据周围的类型限制选择出正确的(++)。

Can't disambiguate name: Prelude.List.++, Prelude.Strings.++ error in Idris