What're the failings of elaborator reflection in providing this in your view? I haven't used it thoroughly, but I thought one could define custom binding forms with it (in Idris 1, at least).