By the way, we just changed ??:: to ??!! for various reasons, the most important of which is to avoid visual confusion with :: as a name separator. But it also has a nice correspondence with the relationship of unary ? and ! operators. (Plus it discourages people from defining their own !! infix operator, which was deemed to be confusing in various ways.)