------------------------------------------------------------------------------
-- | Attempt to run the given tactic in "idiom bracket" mode. For example, if
-- the current goal is
--
--    (_ :: [r])
--
-- then @idiom apply@ will remove the applicative context, resulting in a hole:
--
--    (_ :: r)
--
-- and then use @apply@ to solve it. Let's say this results in:
--
--    (f (_ :: a) (_ :: b))
--
-- Finally, @idiom@ lifts this back into the original applicative:
--
--    (f <$> (_ :: [a]) <*> (_ :: [b]))
--
-- Idiom will fail fast if the current goal doesn't have an applicative
-- instance.
idiom :: TacticsM () -> TacticsM ()