Posting this on behalf of someone who came into the help channel with this problem.
When "/ban -k #channel hidden-nick" is used against a nick not showing in the nicklist, it doesn't issue the KICK command after setting the +b mode.
On Undernet there's a +D mode. It's some kind of auditorium mode which hides a nick from the NAMES command until they 'do' something, even hidden from the viewpoint of the @ops. When combined with +m mode it means they're hidden until they're voiced. People there were calling it 'deaf mode', but that's different than the deaf mode I've heard of before, which is a +d mode which can be set on a nick which means they can't see channel or query messages.
Because the nicks get hidden from "/names #channel", it doesn't appear in the nicklist, though the list of hidden nicks can be revealed by doing "/names -D #channel" at occasional intervals, with the reply coming at raw 355. The ops don't even know that a hidden nick has left until a new '/names -d' doesn't list them anymore.
Even though they don't appear in the nicklist or $ial or $ialchan, the hidden nicks can be /ban'ed, because mIRC issues a USERHOST command to check if someone is currently connected using that nick, and uses the answer to ban their mask, regardless if they're actually in the channel - hidden or not. The /kick command also can kick a user because mIRC issues the KICK command to the server even if they're not in the ial or in the nicklist, or even if there's no such nick.
However "/ban -k #channel hidden-nick" doesn't issue the kick command unless the nick appears in the nicklist, even though "/kick nosuchnick" does issue a KICK command to the server. When a hidden nick gets kicked or given op, there's an immediate fake join message in order to kick them or add them to the nicklist.
I realize that a workaround is to issue a separate KICK command, but since /kick will issue the kick command regardless if the nick exists, /ban -k should probably do the same KICK, unless it should do so only in the situations such as detecting modes where nicks can be hidden. This kind of auditorium mode is different than the ones I've seen before, because under +D the nicks get hidden from the @ops too.