This shows the states of Idris source code that demonstrates a bug in the vim idris plugin support. predicates0.idr shows before the bug, predicates1.idr after.

predicates0.idr

module Predicates

import Data.Vect

isElem : DecEq a => (value : a) -> (xs : Vect n a) -> Dec (Elem value xs)
isElem value [] = ?bug -- with cursor over ?bug hole if you <Leader>p it will complete with `Yes ?bug1`
isElem value (x :: xs) = ?irrelevant

predicates1.idr

module Predicates

import Data.Vect

isElem : DecEq a => (value : a) -> (xs : Vect n a) -> Dec (Elem value xs)
isElem value [] = Yes ?bug1
isElem value (x :: xs) = Yes (There ?isElem_rhs_5)

versions.txt

$ idris --version
0.12.2

$ find /nix/store/ -name "*vimplugin-idris-vim*" -type d
/nix/store/ybqmvzp8mxpfz8hynzjh69a0qsqvhgkx-vimplugin-idris-vim-2016-07-15

$ vim --version
VIM - Vi IMproved 7.4 (2013 Aug 10, compiled Jan  1 1970 00:00:01)
Included patches: 1-826
Compiled by nixbld
Huge version with GTK2 GUI.  Features included (+) or not (-):
+acl             +farsi           +mouse_netterm   +syntax
+arabic          +file_in_path    +mouse_sgr       +tag_binary
+autocmd         +find_in_path    -mouse_sysmouse  +tag_old_static
+balloon_eval    +float           +mouse_urxvt     -tag_any_white
+browse          +folding         +mouse_xterm     -tcl
++builtin_terms  -footer          +multi_byte      +terminfo
+byte_offset     +fork()          +multi_lang      +termresponse
+cindent         -gettext         -mzscheme        +textobjects
+clientserver    -hangul_input    +netbeans_intg   +title
+clipboard       +iconv           +path_extra      +toolbar
+cmdline_compl   +insert_expand   -perl            +user_commands
+cmdline_hist    +jumplist        +persistent_undo +vertsplit
+cmdline_info    +keymap          +postscript      +virtualedit
+comments        +langmap         +printer         +visual
+conceal         +libcall         +profile         +visualextra
+cryptv          +linebreak       +python          +viminfo
+cscope          +lispindent      -python3         +vreplace
+cursorbind      +listcmds        +quickfix        +wildignore
+cursorshape     +localmap        +reltime         +wildmenu
+dialog_con_gui  +lua             +rightleft       +windows
+diff            +menu            +ruby            +writebackup
+digraphs        +mksession       +scrollbind      +X11
+dnd             +modify_fname    +signs           -xfontset
-ebcdic          +mouse           +smartindent     -xim
+emacs_tags      +mouseshape      -sniff           -xsmp
+eval            +mouse_dec       +startuptime     +xterm_clipboard
+ex_extra        -mouse_gpm       +statusline      -xterm_save
+extra_search    -mouse_jsbterm   -sun_workshop    +xpm
   system vimrc file: "$VIM/vimrc"
     user vimrc file: "$HOME/.vimrc"
 2nd user vimrc file: "~/.vim/vimrc"
      user exrc file: "$HOME/.exrc"
  system gvimrc file: "$VIM/gvimrc"
    user gvimrc file: "$HOME/.gvimrc"
2nd user gvimrc file: "~/.vim/gvimrc"
    system menu file: "$VIMRUNTIME/menu.vim"
  fall-back for $VIM: "
/nix/store/ngzs2i85m3zq5mq1rlpphqkbsfxgj78m-vim_configurable-7.4.826/share/vim
"
Compilation: gcc -c -I. -Iproto -DHAVE_CONFIG_H -DFEAT_GUI_GTK  -I/nix/store/gxvvjsad12hdmz8nfd02f2kq313z5671-gtk+-2.24.30-dev/include/gtk-2.0 -I/nix/store/gqh6v87hfl7qvwfmhk9srvmzd18an60p-gtk+-2.24.30/lib/gtk-2.0/include -I/nix/store/xrs0izclp1518ln6xffggf88gr723miq-glib-2.48.2-dev/include/glib-2.0 -I/nix/store/h2zq29hbjfy6a70swr7s3wr6vxcfbb1q-glib-2.48.2/lib/glib-2.0/include -I/nix/store/k3ld916nbwb2irx4jn45gm2qab9rcsvi-cairo-1.14.6-dev/include/cairo -I/nix/store/hdc765njs04kk0smp4klm33r231d9f3w-freetype-2.6.5-dev/include/freetype2 -I/nix/store/hdc765njs04kk0smp4klm33r231d9f3w-freetype-2.6.5-dev/include -I/nix/store/wig2c2mvwcspy6dkhjndqax98f93iy6h-fontconfig-2.11.1-dev/include -I/nix/store/3z1m9l32m44snwq1gznwydl1gqirq1rb-expat-2.2.0-dev/include -I/nix/store/hdc765njs04kk0smp4klm33r231d9f3w-freetype-2.6.5-dev/include/freetype2 -I/nix/store/qwg8sq15n3axp21iihkbkcmhix27mpq3-pango-1.40.1-dev/include/pango-1.0 -I/nix/store/9yb1645a7w3bdq7sizs90xdknckhz1sx-gdk-pixbuf-2.34.0-dev/include/gdk-pixbuf-2.0 -I/nix/store/hflv6ppqdbvl9plwzf6kpra45894f7ms-atk-2.20.0-dev/include/atk-1.0   -g -O2 -U_FORTIFY_SOURCE -D_FORTIFY_SOURCE=1
Linking: gcc -L/nix/store/gqh6v87hfl7qvwfmhk9srvmzd18an60p-gtk+-2.24.30/lib -L/nix/store/h2zq29hbjfy6a70swr7s3wr6vxcfbb1q-glib-2.48.2/lib -L/nix/store/yjll797lbx1m5jqrha2681701y73yg8g-cairo-1.14.6/lib -L/nix/store/w1dql6jq9fvcdfi43gp8r0xmwsffql4h-fontconfig-2.11.1-lib/lib -L/nix/store/n8xc1g27clhc2jy5fw0wkn3l75f2mijh-freetype-2.6.5/lib -L/nix/store/7v96d22r2pw777gwvws4dw65m653sx43-pango-1.40.1/lib -L/nix/store/aqwlwdrzdykwj37sv5s5nknfi0qba0md-gdk-pixbuf-2.34.0/lib -L/nix/store/nprd8snkllkhfra4l98652qzcnsbgxak-atk-2.20.0/lib  -L. -fstack-protector -rdynamic -Wl,-export-dynamic  -Wl,--as-needed -o vim   -L/nix/store/gqh6v87hfl7qvwfmhk9srvmzd18an60p-gtk+-2.24.30/lib -L/nix/store/h2zq29hbjfy6a70swr7s3wr6vxcfbb1q-glib-2.48.2/lib -L/nix/store/yjll797lbx1m5jqrha2681701y73yg8g-cairo-1.14.6/lib -L/nix/store/w1dql6jq9fvcdfi43gp8r0xmwsffql4h-fontconfig-2.11.1-lib/lib -L/nix/store/n8xc1g27clhc2jy5fw0wkn3l75f2mijh-freetype-2.6.5/lib -L/nix/store/7v96d22r2pw777gwvws4dw65m653sx43-pango-1.40.1/lib -L/nix/store/aqwlwdrzdykwj37sv5s5nknfi0qba0md-gdk-pixbuf-2.34.0/lib -L/nix/store/nprd8snkllkhfra4l98652qzcnsbgxak-atk-2.20.0/lib -lgtk-x11-2.0 -lgdk-x11-2.0 -lpangocairo-1.0 -latk-1.0 -lcairo -lgdk_pixbuf-2.0 -lgio-2.0 -lpangoft2-1.0 -lpango-1.0 -lgobject-2.0 -lglib-2.0 -lfontconfig -lfreetype -lSM -lICE -lXpm -lXt -lX11 -lSM -lICE  -lm -lncurses -lnsl   -ldl  -L/nix/store/0xknacazl7h7iz1xw7la15nz9i4rwak6-lua-5.1.5/lib -llua  -L/nix/store/4f3bazndmnsy3m16jghbsa69r4g5rn83-python-2.7.12/lib/python2.7/config -lpython2.7 -lpthread -ldl -lutil -lm -Xlinker -export-dynamic   -Wl,-R/nix/store/iasqv2scb71yv6ycqhskmkdq6g7apj5k-ruby-2.3.1-p0/lib -L/nix/store/iasqv2scb71yv6ycqhskmkdq6g7apj5k-ruby-2.3.1-p0/lib -lruby -lpthread -ldl -lcrypt -lm  -L/nix/store/iasqv2scb71yv6ycqhskmkdq6g7apj5k-ruby-2.3.1-p0/lib