Why not change the sticking character instead of being "_" it could be something like '#' or '$' ?
We have already discussed having "##" for builtin constructs. It might make it even more consistent to use it for everything the compiler uses under the hood.
##; ##+ ##let_in ##| ##cons ##inductive