Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Idris in ide-mode sends wrong sexp expression (make case clause) #4553

Open
justjoheinz opened this issue Sep 6, 2018 · 0 comments
Open

Comments

@justjoheinz
Copy link
Contributor

Steps to Reproduce

Given the following program:

module Main

myFun : ?hole -> String
myFun x = ?myFun_rhs
  • move your cursor to ?myFun_rhs and get the type of the hole (Atom: Ctrl-Alt-t)

Expected Behavior

idris sends correct s-exp expression with no duplicates.

Observed Behavior

idris responds with the s-exp expression:

(
(2 1 ((:name "x") (:decor :bound) (:implicit :False)))
-> (7 4 ((:name "Main.hole") (:implicit :False) (:key "a==") (:decor :metavar) (:type "Type") (:namespace "Main")))
-> (6 5 ((:name "Main.hole") (:implicit :False) (:key "a==") (:decor :metavar) (:type "Type") (:namespace "Main")))
(51 9 ((:name "myFun_rhs") (:implicit :False) (:key "AAAAAAAAAAAJbXlGdW5fcmhz") (:decor :metavar) (:type "?hole -> String")))
(63 6 ((:decor :type) (:type "Type") (:doc-overview "Strings in some unspecified encoding") (:name "String"))))) 3)

which contains two overlapping definitions of the metavar hole (marked by ->)
this leads to problems in IDEs such as Atom, which try to implement a reasonable UI for this.

See idris-hackers/atom-language-idris#195 for screenshots

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant