[WIP] Allow applicative idioms when solving tactics

[isovector]

This PR introduces applicative idioms, by way of the following tactic combinator:

------------------------------------------------------------------------------
-- | 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 ()

Currently WIP because it doesn't ensure an applicative instance exists.

[isovector]

@wz1000 do you know how I can lookup whether an Applicative instance exists for a given type in HLS?