Outdated commentary in solveNestedImplications?

GHC.Tc.Solver.solveNestedImplications looks like this:

solveNestedImplications :: Bag Implication
                        -> TcS (Cts, Bag Implication)
-- Precondition: the TcS inerts may contain unsolved simples which have
-- to be converted to givens before we go inside a nested implication.
solveNestedImplications implics
  | isEmptyBag implics
  = return (emptyBag, emptyBag)
  | otherwise
  = do { traceTcS "solveNestedImplications starting {" empty
       ; (floated_eqs_s, unsolved_implics) <- mapAndUnzipBagM solveImplication implics
       ; let floated_eqs = concatBag floated_eqs_s

       -- ... and we are back in the original TcS inerts
       -- Notice that the original includes the _insoluble_simples so it was safe to ignore
       -- them in the beginning of this function.
       ; traceTcS "solveNestedImplications end }" $
                  vcat [ text "all floated_eqs ="  <+> ppr floated_eqs
                       , text "unsolved_implics =" <+> ppr unsolved_implics ]

       ; return (floated_eqs, catBagMaybes unsolved_implics) }

I believe that both the Precondition: and the ... and we are back comments are out of date. If they are not, they should be clarified, as I have no idea what they mean.

Also:

solveImplication :: Implication    -- Wanted
                 -> TcS (Cts,      -- All wanted or derived floated equalities: var = type
                         Maybe Implication) -- Simplified implication (empty or singleton)
-- Precondition: The TcS monad contains an empty worklist and given-only inerts
-- which after trying to solve this implication we must restore to their original value

The empty-worklist precondition seems reasonable, but the "given-only inerts" bit is as mysterious as (and sounds quite related to) the previous problem.

@simonpj help?