Using zipWith with addition like following code, works fine:
zipWith (\x,y => x + y) [1,2,3] [4,5,6]
However, using concatenation instead with two lists of lists fails:
zipWith (\xs,ys => xs ++ ys) [[1],[2],[3]] [[4],[5],[6]]
with error:
When checking argument x to constructor Prelude.List.:::
No such variable a
I have observed that it is possible to do following without errors:
zipWith (++) [[1],[2],[3]] [[4],[5],[6]]
However, I am confused why the concatenation with lambda expression fails..?
Idris> :t (++)
Prelude.List.(++) : List a -> List a -> List a
This is where the compiler cannot determine the value of a. If you just type [1,2,3] in the REPL, it will give it the type List Integer. But [1,2,3] could also be of type List Int, List Nat or any other List of some numbers. If you try your example with ['a','b','c'], this ambiguity vanishes and the repl will accept it happily:
Idris> zipWith (\xs, ys => xs ++ ys) [['a'],['b'],['c']] [['a'],['b'],['c']]
[['a', 'a'], ['b', 'b'], ['c', 'c']] : List (List Char)
You can solve the initial problem by giving information to the type checker:
zipWith (\xs, ys => (++) xs ys {a=Integer}) [[1],[2],[3]] [[4],[5],[6]]
zipWith (\xs, ys => the (List Integer) (xs ++ ys)) [[1],[2],[3]] [[4],[5],[6]]
the (List (List Integer)) (zipWith (\xs, ys => xs ++ ys) [[1],[2],[3]] [[4],[5],[6]])
In most but the simplest cases some type declarations are needed for unification. That is why (++) works but not the lambda expression. The former is easier and the latter has an abstraction more to it (i.e. an extra function).
But when writing actual code in a file, the compiler wouldn't be as friendly as the REPL and would demand a type declaration anyway:
-- test : List (List Integer)
test = zipWith (\xs, ys => xs ++ ys) [[1],[2],[3]] [[4],[5],[6]]
Type checking ./test.idr
test.idr:1:1:No type declaration for Main.test