Hi idris-lang,
Suppose I've got
concatList : Monoid a => List a -> a
Then I can define sumList using:
sumList : Num a => List a -> a
sumList = concatList @{Additive}
But what if I want to write:
sumAndConcat : Monoid a, Num b => List (a, b) -> (a, b)
sumAndConcat = concatList @{???}
Is there anything I can replace "???" with that will make it work?
According to
this "Auto implicit arguments" section, the compiler tries "Local variables, i.e. names bound in pattern matches or let bindings, with exactly the right type.". So, I tried this:
sumAndConcat : Monoid a => Num b => List (a, b) -> (a, b)
sumAndConcat =
let monoidImpl : Monoid b
monoidImpl = Additive
in concatList
My hope was that since monoidImpl is available to search, Idris2 will be able to combine that with the default Monoid (a, b) implementation. But it didn't work: Idris2 says "Can't find an implementation for Monoid (a, b)".
I found this in Prelude:
sum : (Foldable t, Num a) => t a -> a
sum = concat @{(%search, Additive)}
Is "%search" documented anywhere? Can it be used to accomplish what I want?
My actual use case is slightly more complicated. I've implemented a mapping type with a default value, called "DefaultMap", and have a default implementation:
Ord k => Monoid v => DecEq v => (d : v) => (d = Prelude.Interfaces.neutral) => Monoid (DefaultMap k v d) where
but I am having trouble getting Idris2 to use it when v = Int.