cast.idr

x : Int
x = 1

y : String
y = "2"

gistfile1.txt

$ idris cast.idr
     ____    __     _                                          
    /  _/___/ /____(_)____                                     
    / // __  / ___/ / ___/     Version 0.9.12-git:5621005
  _/ // /_/ / /  / (__  )      http://www.idris-lang.org/      
 /___/\__,_/_/  /_/____/       Type :? for help                

*cast> x + cast(y)
3 : Int
*cast> cast(x) ++ y
"12" : String
*cast> cast(x) + cast(y)
When elaborating an application of constructor __infer:
        Can't disambiguate name: Prelude.Classes.+, Prelude.Fin.+
*cast> cast(x) ++ cast(y)
When elaborating an application of constructor __infer:
        Can't disambiguate name: Prelude.List.++, 
                                 Prelude.Strings.++, 
                                 Prelude.Vect.++
*cast> :q
Bye bye

The operator + is overloaded twice, while ++ is overloaded three times:

Idris> :doc (+)
+ : Num a => a -> a -> a

    infixl 8

+ : Fin n -> Fin m -> Fin (n + m)
    Add two Fins, extending the bound
    infixl 8

Idris> :doc (++)
++ : List a -> List a -> List a
    Append two lists
    infixr 7

++ : String -> String -> String
    Appends two strings together.

    Idris> "AB" ++ "C" "ABC" : String
    infixr 7

++ : Vect m a -> Vect n a -> Vect (m + n) a
    Append two vectors
    infixr 7