"Wrong" documentation

[justjoheinz]

Given the following method:

times: (n: Nat) -> {auto prf: n >= 1 = True} -> Vect m Note -> Vect (m*n) Note
times n xs = concat $ explode n xs where
                explode: (l: Nat) -> Vect k Note -> Vect k (Vect l Note)
                explode l xs = do
                                         elem <- xs
                                         return (replicate l elem)

When I point the cursor on replicate and ask for documentation I get the documentation for Prelude.List.replicate : (n : Nat) -> (x : a) -> List a

I would have expected the documentation for Data.Vect.replicate : (n : Nat) -> (x : a) -> Vect n a

The repl :doc command outputs both.

[archaeron]

thanks for reporting this

@david-christiansen I just tested this in emacs and see the same behaviour. Is there a way to fix this? There is a fully contained test case here: https://github.com/archaeron/atom-language-idris-tests/blob/master/bare-files/issue83.idr

[archaeron]

If you open the new repl with ctrl-alt-enter and type :doc replicate you get the documentation of both functions.

[david-christiansen]

@archaeron I can't replicate this in Emacs - for me, both the Eldoc summary at the bottom of the screen and the tooltip show the version for Vect: What were you seeing?

[david-christiansen]

Also, in Emacs, right-clicking "replicate" and picking "Get docs" from the menu shows the correct docs (for the Vect version), and so does the key shortcut C-c C-d d.

[david-christiansen]

In Atom, the way I'd solve it is to listen for the semantic highlighting information from the compiler, even though Atom won't actually let you highlight with it. Then, remember which regions of the source corresponded to which underlying fully-qualified names, and when the user issues the "ask for docs" command, check whether that information is up-to-date for the current region (that is, is the name in the source a suffix of a semantic name from the compiler at that location) and if so, ask for those docs. This is basically how it works in Emacs, except we're using the Emacs overlay system to keep track of which regions are which names.

[archaeron]

@david-christiansen thanks a lot for your explanation

This is what happens for me in emacs.

I have probably an old version of the emacs-mode though.