Template creation via <LocalLeader>d not adding patterns for parameters

[apriori]

Test case:

append : Vect n a -> Vect m a -> Vect (n + m) a

Apply \d on append.

Expected something like:

append : Vect n a -> Vect m a -> Vect (n + m) a
append xs ys = ?append_rhs

Got that instead:

append : Vect n a -> Vect m a -> Vect (n + m) a
append = ?append_rhs

Version info:

idris 0.9.12 (cabal)
idris-vim 2586645 (current HEAD)

[victoredwardocallaghan]

Still occurs in 7a0f64d idris-0.9.15 when did this break, has someone bisected yet?

[edwinb]

What are the steps to reproduce this? Does it happen every time? Have you tried, for example, deleting all .ibcs and checking that there's no other idris running?

I know there are some issues with interactive editing, but I can't reproduce this one as it is, so I think there must be something different in your environment, and if we can work out what it is then we might be able to fix this. In any case, it is likely an Idris issue rather than a vim mode issue.

[raichoo]

This could be related to another plugin interfering with idris-vim. I had a similar issue with syntastic, I fixed it by adding let g:syntastic_check_on_wq = 0 to my .vimrc.

[victoredwardocallaghan]

Hopefully fixed in vim-syntastic/syntastic#1215

[victoredwardocallaghan]

OK, after some research this seems to be related to calling idris --check while another idris instance is running. Essentially it looks like non-atomic updates to IBC files from idris --check and idris --client racing one another. Unfortunately I was quickly lost while trying to trace back the function calls in Idris. :/

Hope this is helpful