Type-level hole misnamed in premise

[hubbards]

Consider the following (incomplete) function with holes in the type and definition:

myFun : ?ArgType -> String
myFun x = ?myFun_rhs

Inspecting the type of the hole myFun_rhs using interactive editing commands in Atom result in

  x : ?ArgType?ArgType
--------------------------------------
myFun_rhs : String

In the premise, the type of x is shown as ?ArgType?ArgType but it should be ?ArgType.

Inspecting the type of the hole myFun_rhs in the Idris (v1.1.1) REPL gives the correct results

  x : ?ArgType
--------------------------------------
myFun_rhs : String

[justjoheinz]

Thanks for reporting this. I think this is most likely an error in the idris ide protocol. I will check with emacs if it exhibits the same behavior.