TcLevel invariants are being violated

The TcLevel invariants are clearly being violated in tcMatchesInfer and tcMatchesCheck:

-- | Rule: Match-Infer
tcMatchInfer gamma (MkMatch aps e) irs ir = do
  ps <- getPats aps
  (dlt, qs) <- tcPatsInfer gamma (zipWith (\i p -> (p, Infer i)) irs ps)
  traceTc "tcMatch - Delta returened by tcPatsInfer:" (pretty dlt)
  let givens = map (mkCt CtGiven) qs
      skols  = skolems dlt
  buildImplicIfNeeded skols givens
      $ tcExpr (modifyDelta (dlt <>) gamma) e (Infer ir)

-- | Rule: Match-Check
tcMatchCheck gamma (MkMatch aps e) psis rho = do
  (patSigmaPairs, lcl_ctxt, qs,subst) <- tcSkolAPats gamma psis aps
  (lcl_ctxt', qs') <- tcPatsCheck (modifyDelta (lcl_ctxt <>) gamma) patSigmaPairs
  let givens = map (mkCt CtGiven) (qs ++ qs')
      skols  = skolems lcl_ctxt
  buildImplicIfNeeded skols givens $
    tcExpr (modifyDelta ((lcl_ctxt' <> lcl_ctxt) <>) gamma) e
        $ Check (appTvSubstTau subst (rhoToSigma rho))

The problem is that the function that pushes the ambient TcLevel by one -- pushLevelAndCaptureCts -- is in buildImplicIfNeeded, which is clearly called after the functions that are responsible for typechecking patterns. i.e tcPatsInfer, tcPatsCheck, and tcSkolemiseAPats.

Here are the implications built for ./typechecker/test/cases/should-typecheck/myMap-infer.hs:

buildImplicIfNeeded {
 implTcLvl   = 1
 implSkolems = sk25[0] : Type
 implGivens  = []
 implStatus  = Unsolved
 implWanteds = wcImplics = []
               wcSimples = [W] mv-t36[0]:Type ~ (mv-t40[1]:Type -> mv-t41[1]:Type)
                           [W] Type ~ Type
                           [W] mv-t35[0]:Type ~ (mv-t42[1]:Type -> mv-t43[1]:Type)
                           [W] mv-t43[1]:Type ~ (mv-t44[1]:Type -> mv-t45[1]:Type)
                           [W] mv-t46[0]:Type ~ List mv-t41[1]:Type
                           [W] mv-t36[0]:Type ~ (mv-t47[1]:Type -> mv-t48[1]:Type)
                           [W] mv-t41[1]:Type ~ mv-t48[1]:Type
                           [W] mv-t47[1]:Type ~ mv-t38[0]:Type
                           [W] mv-t35[0]:Type ~ (mv-t49[1]:Type -> mv-t50[1]:Type)
                           [W] mv-t50[1]:Type ~ (mv-t51[1]:Type -> mv-t52[1]:Type)
                           [W] List mv-t41[1]:Type ~ mv-t52[1]:Type
                           [W] mv-t49[1]:Type ~ mv-t36[0]:Type
                           [W] mv-t51[1]:Type ~ List mv-t38[0]:Type
} 

buildImplicIfNeeded {
 implTcLvl   = 1
 implSkolems = sk24[0] : Type
 implGivens  = []
 implStatus  = Unsolved
 implWanteds = wcImplics = []
               wcSimples = [W] mv-t46[0]:Type ~ List mv-t57[1]:Type
}