AFAIUI: "Void -> a" means that the function cannot be called, because there no way to conjure a Void value. In Haskell, you can do it by (ab)using 'undefined',

AFAIUI: "Void -> a" means that the function cannot be called, because there no way to conjure a Void value. In Haskell, you can do it by (ab)using 'undefined', but that's kind of cheating. However, if you're using Idris with totality checking, I don't think you'll actually get any code calling such a function compile. The "a -> Void" means that the function can never return.