How to create an empty list in Idris REPL?

Question

I want to create myEmptyList and myNonemptyList in REPL. However Idris reported a type mismatch error for myEmptyList. Why?

     ____    __     _                                          
    /  _/___/ /____(_)____                                     
    / // __  / ___/ / ___/     Version 1.3.0
  _/ // /_/ / /  / (__  )      http://www.idris-lang.org/      
 /___/\__,_/_/  /_/____/       Type :? for help               

Idris is free software with ABSOLUTELY NO WARRANTY.            
For details type :warranty.
Idris> :let myEmptyList : List Integer = []
(input):1:33: When checking type of myEmptyList:
When checking argument y to type constructor =:
        Type mismatch between
                List elem (Type of [])
        and
                Type (Expected type)
(input):1:18:No type declaration for myEmptyList
Idris> :let myNonemptyList : List Integer = [42]

Answer 1

The mismatch is because :let myEmptyList : List Integer = [] does not define myEmptyList, it only declares its type as List Integer = [], an equality type, which is ill-typed because [] and List Integer have different types.

You can define myEmptyList as follows: :let myEmptyList : List Integer; myEmptyList = [], or alternatively :let myEmptyList = the (List Integer) [].