"putStrLn (show [1,2])" causes "Can't unify Vect Int (S (S O)) with Int" about idris-dev HOT 2 CLOSED

apparently it has something to do with [1,2]'s type since the following works as expected :

main = putStrLn (show (add [1,2] [3,4]))

add : (Num a) => Vect a n -> Vect a n -> Vect a n
add [] [] = []
add (x::xs) (y::ys) = (x+y)::(add xs ys)

from idris-dev.

In HEAD, I get "listo.idr:4:Can't disambiguate name: Prelude.List.::, Prelude.Vect.::"
which is what I'd expect.

Overloading is type directed - so you need some way of knowing what type is actually intended by the list [1,2].

On 27 Nov 2012, at 17:37, "Ashkan Kh. Nazary" [email protected] wrote:

module Main

main : IO ()
main = putStrLn (show [1,2])

Idris version 0.9.5.1

—
Reply to this email directly or view it on GitHub.

from idris-dev.