search

owickstrom / idris-vimscript

Compile Idris to Vimscript, like you always wanted.
Other
130 stars 5 forks source link

"No such variable a" #2

Open mrkgnao opened 6 years ago

mrkgnao commented 6 years ago

This has to be raised upstream, but since I don't have the time to find a minimal example right away, I'll put it here.

module Vimscript.Examples 

import Vimscript.Builtins
import Vimscript.FFI
import Vimscript.List

data Line = First | Last | LineNum Int

goTo : Line -> VIM_IO ()
goTo l = goTo' l *> pure ()
  where
    goTo' Last = line "$"
    goTo' First = line "0"
    goTo' (LineNum n) = line (show n)

Without a type annotation on goTo', we get a "No such variable a" error, even though we haven't introduced any binding with that name. This looks like an elaborator error, but I might be wrong.