+\begin{code}
+--------------------
+tc_lpats :: PatState
+ -> [LPat Name]
+ -> [BoxySigmaType]
+ -> (PatState -> TcM a)
+ -> TcM ([LPat TcId], [TcTyVar], a)
+
+tc_lpats pstate pats pat_tys thing_inside
+ = do { err_ctxt <- getErrCtxt
+ ; let loop pstate [] []
+ = do { res <- thing_inside pstate
+ ; return ([], [], res) }
+
+ loop pstate (p:ps) (ty:tys)
+ = do { (p', p_tvs, (ps', ps_tvs, res))
+ <- tc_lpat pstate p ty $ \ pstate' ->
+ setErrCtxt err_ctxt $
+ loop pstate' ps tys
+ -- setErrCtxt: restore context before doing the next pattern
+ -- See note [Nesting] above
+
+ ; return (p':ps', p_tvs ++ ps_tvs, res) }
+
+ loop _ _ _ = pprPanic "tc_lpats" (ppr pats $$ ppr pat_tys)
+
+ ; loop pstate pats pat_tys }
+
+--------------------
+tc_lpat :: PatState
+ -> LPat Name
+ -> BoxySigmaType
+ -> (PatState -> TcM a)
+ -> TcM (LPat TcId, [TcTyVar], a)
+tc_lpat pstate (L span pat) pat_ty thing_inside
+ = setSrcSpan span $
+ maybeAddErrCtxt (patCtxt pat) $
+ do { let pat_ty' = refineType (pat_reft pstate) pat_ty
+ -- Make sure the result type reflects the current refinement
+ ; (pat', tvs, res) <- tc_pat pstate pat pat_ty' thing_inside
+ ; return (L span pat', tvs, res) }
+
+
+--------------------
+tc_pat :: PatState
+ -> Pat Name -> BoxySigmaType -- Fully refined result type
+ -> (PatState -> TcM a) -- Thing inside
+ -> TcM (Pat TcId, -- Translated pattern
+ [TcTyVar], -- Existential binders
+ a) -- Result of thing inside
+
+tc_pat pstate (VarPat name) pat_ty thing_inside
+ = do { id <- tcPatBndr pstate name pat_ty
+ ; (res, binds) <- bindInstsOfPatId id $
+ tcExtendIdEnv1 name id $
+ (traceTc (text "binding" <+> ppr name <+> ppr (idType id))
+ >> thing_inside pstate)
+ ; let pat' | isEmptyLHsBinds binds = VarPat id
+ | otherwise = VarPatOut id binds
+ ; return (pat', [], res) }
+
+tc_pat pstate (ParPat pat) pat_ty thing_inside
+ = do { (pat', tvs, res) <- tc_lpat pstate pat pat_ty thing_inside
+ ; return (ParPat pat', tvs, res) }
+
+tc_pat pstate (BangPat pat) pat_ty thing_inside
+ = do { (pat', tvs, res) <- tc_lpat pstate pat pat_ty thing_inside
+ ; return (BangPat pat', tvs, res) }
+
+-- There's a wrinkle with irrefuatable patterns, namely that we
+-- must not propagate type refinement from them. For example
+-- data T a where { T1 :: Int -> T Int; ... }
+-- f :: T a -> Int -> a
+-- f ~(T1 i) y = y
+-- It's obviously not sound to refine a to Int in the right
+-- hand side, because the arugment might not match T1 at all!
+--
+-- Nor should a lazy pattern bind any existential type variables
+-- because they won't be in scope when we do the desugaring
+tc_pat pstate lpat@(LazyPat pat) pat_ty thing_inside
+ = do { (pat', pat_tvs, res) <- tc_lpat pstate pat pat_ty $ \ _ ->
+ thing_inside pstate
+ -- Ignore refined pstate',
+ -- revert to pstate
+ ; if (null pat_tvs) then return ()
+ else lazyPatErr lpat pat_tvs
+ ; return (LazyPat pat', [], res) }
+
+tc_pat pstate (WildPat _) pat_ty thing_inside
+ = do { pat_ty' <- unBox pat_ty -- Make sure it's filled in with monotypes
+ ; res <- thing_inside pstate
+ ; return (WildPat pat_ty', [], res) }
+
+tc_pat pstate (AsPat (L nm_loc name) pat) pat_ty thing_inside
+ = do { bndr_id <- setSrcSpan nm_loc (tcPatBndr pstate name pat_ty)
+ ; (pat', tvs, res) <- tcExtendIdEnv1 name bndr_id $
+ tc_lpat pstate pat (idType bndr_id) thing_inside
+ -- NB: if we do inference on:
+ -- \ (y@(x::forall a. a->a)) = e
+ -- we'll fail. The as-pattern infers a monotype for 'y', which then
+ -- fails to unify with the polymorphic type for 'x'. This could
+ -- perhaps be fixed, but only with a bit more work.
+ --
+ -- If you fix it, don't forget the bindInstsOfPatIds!
+ ; return (AsPat (L nm_loc bndr_id) pat', tvs, res) }
+
+-- Type signatures in patterns
+-- See Note [Pattern coercions] below
+tc_pat pstate (SigPatIn pat sig_ty) pat_ty thing_inside
+ = do { (inner_ty, tv_binds) <- tcPatSig (patSigCtxt pstate) sig_ty pat_ty
+ ; (pat', tvs, res) <- tcExtendTyVarEnv2 tv_binds $
+ tc_lpat pstate pat inner_ty thing_inside
+ ; return (SigPatOut pat' inner_ty, tvs, res) }
+
+tc_pat pstate pat@(TypePat ty) pat_ty thing_inside
+ = failWithTc (badTypePat pat)