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

Question

Currently I am trying to create a function that takes the type of (a -> a -> a) as a parameter in Idris and the right function to do is the ++ command for lists in idris unfortunately I am getting this error

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

When checking right hand side of ListMonoid with expected type RawMonoid

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

Raw Monoid is a data type below

RawMonoid : Type RawMonoid = (M ** (M , M -> M -> M)) infixl 6 &

It seems to me that it does not know which ++ to use, is there a way to specify this in the call?

Answer 1

You can qualify the reference to (++), e.g.

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

And there's also the with keyword, which takes a module name as its first argument - it basically means, "in the following expression, look in this module first to resolve names", e.g.

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

However, both of those give me the following type error with your code:

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

If I write:

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

It's able to pick out the correct (++) based on the surrounding type constraints.