--------------------
type Checker inp out =  forall r.
			  inp
		       -> PatEnv
		       -> TcM r
		       -> TcM (out, r)

tcMultiple :: Checker inp out -> Checker [inp] [out]
tcMultiple tc_pat args penv thing_inside
  = do	{ err_ctxt <- getErrCtxt
	; let loop _ []
		= do { res <- thing_inside
		     ; return ([], res) }

	      loop penv (arg:args)
		= do { (p', (ps', res)) 
				<- tc_pat arg penv $ 
				   setErrCtxt err_ctxt $
				   loop penv args
		-- setErrCtxt: restore context before doing the next pattern
		-- See note [Nesting] above
				
		     ; return (p':ps', res) }

	; loop penv args }

--------------------
tc_lpat :: LPat Name 
	-> TcSigmaType
	-> PatEnv
	-> TcM a
	-> TcM (LPat TcId, a)
tc_lpat (L span pat) pat_ty penv thing_inside
  = setSrcSpan span $
    do	{ (pat', res) <- maybeWrapPatCtxt pat (tc_pat penv pat pat_ty)
                                          thing_inside
	; return (L span pat', res) }

tc_lpats :: PatEnv
	 -> [LPat Name] -> [TcSigmaType]
       	 -> TcM a	
       	 -> TcM ([LPat TcId], a)
tc_lpats penv pats tys thing_inside 
  = ASSERT2( equalLength pats tys, ppr pats $$ ppr tys )
    tcMultiple (\(p,t) -> tc_lpat p t) 
                (zipEqual "tc_lpats" pats tys)
                penv thing_inside 

--------------------
tc_pat	:: PatEnv
        -> Pat Name 
        -> TcSigmaType	-- Fully refined result type
        -> TcM a		-- Thing inside
        -> TcM (Pat TcId, 	-- Translated pattern
                a)		-- Result of thing inside

tc_pat penv (VarPat name) pat_ty thing_inside
  = do	{ (co, id) <- tcPatBndr penv name pat_ty
        ; res <- tcExtendIdEnv1 name id thing_inside
        ; return (mkHsWrapPatCo co (VarPat id) pat_ty, res) }

tc_pat penv (ParPat pat) pat_ty thing_inside
  = do	{ (pat', res) <- tc_lpat pat pat_ty penv thing_inside
	; return (ParPat pat', res) }

tc_pat penv (BangPat pat) pat_ty thing_inside
  = do	{ (pat', res) <- tc_lpat pat pat_ty penv thing_inside
	; return (BangPat pat', res) }

tc_pat penv lpat@(LazyPat pat) pat_ty thing_inside
  = do	{ (pat', (res, pat_ct)) 
		<- tc_lpat pat pat_ty (makeLazy penv) $ 
		   captureConstraints thing_inside
		-- Ignore refined penv', revert to penv

	; emitConstraints pat_ct
	-- captureConstraints/extendConstraints: 
        --   see Note [Hopping the LIE in lazy patterns]

	-- Check there are no unlifted types under the lazy pattern
	; when (any (isUnLiftedType . idType) $ collectPatBinders pat') $
               lazyUnliftedPatErr lpat

	-- Check that the expected pattern type is itself lifted
	; pat_ty' <- newFlexiTyVarTy liftedTypeKind
	; _ <- unifyType pat_ty pat_ty'

	; return (LazyPat pat', res) }

tc_pat _ p@(QuasiQuotePat _) _ _
  = pprPanic "Should never see QuasiQuotePat in type checker" (ppr p)

tc_pat _ (WildPat _) pat_ty thing_inside
  = do	{ res <- thing_inside 
	; return (WildPat pat_ty, res) }

tc_pat penv (AsPat (L nm_loc name) pat) pat_ty thing_inside
  = do	{ (co, bndr_id) <- setSrcSpan nm_loc (tcPatBndr penv name pat_ty)
        ; (pat', res) <- tcExtendIdEnv1 name bndr_id $
			 tc_lpat pat (idType bndr_id) penv 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 (mkHsWrapPatCo co (AsPat (L nm_loc bndr_id) pat') pat_ty, res) }

tc_pat penv (ViewPat expr pat _) overall_pat_ty thing_inside 
  = do	{
         -- Morally, expr must have type `forall a1...aN. OPT' -> B` 
         -- where overall_pat_ty is an instance of OPT'.
         -- Here, we infer a rho type for it,
         -- which replaces the leading foralls and constraints
         -- with fresh unification variables.
        ; (expr',expr'_inferred) <- tcInferRho expr

         -- next, we check that expr is coercible to `overall_pat_ty -> pat_ty`
         -- NOTE: this forces pat_ty to be a monotype (because we use a unification 
         -- variable to find it).  this means that in an example like
         -- (view -> f)    where view :: _ -> forall b. b
         -- we will only be able to use view at one instantation in the
         -- rest of the view
	; (expr_co, pat_ty) <- tcInfer $ \ pat_ty -> 
		unifyType expr'_inferred (mkFunTy overall_pat_ty pat_ty)
        
         -- pattern must have pat_ty
        ; (pat', res) <- tc_lpat pat pat_ty penv thing_inside

	; return (ViewPat (mkLHsWrapCo expr_co expr') pat' overall_pat_ty, res) }

-- Type signatures in patterns
-- See Note [Pattern coercions] below
tc_pat penv (SigPatIn pat sig_ty) pat_ty thing_inside
  = do	{ (inner_ty, tv_binds, wrap) <- tcPatSig (patSigCtxt penv) sig_ty pat_ty
	; (pat', res) <- tcExtendTyVarEnv2 tv_binds $
			 tc_lpat pat inner_ty penv thing_inside

        ; return (mkHsWrapPat wrap (SigPatOut pat' inner_ty) pat_ty, res) }

------------------------
-- Lists, tuples, arrays
tc_pat penv (ListPat pats _ Nothing) pat_ty thing_inside
  = do	{ (coi, elt_ty) <- matchExpectedPatTy matchExpectedListTy pat_ty      
        ; (pats', res) <- tcMultiple (\p -> tc_lpat p elt_ty)
				     pats penv thing_inside
 	; return (mkHsWrapPat coi (ListPat pats' elt_ty Nothing) pat_ty, res) 
        }

tc_pat penv (ListPat pats _ (Just (_,e))) pat_ty thing_inside
  = do	{ list_pat_ty <- newFlexiTyVarTy liftedTypeKind
        ; e' <- tcSyntaxOp ListOrigin e (mkFunTy pat_ty list_pat_ty)
        ; (coi, elt_ty) <- matchExpectedPatTy matchExpectedListTy list_pat_ty
        ; (pats', res) <- tcMultiple (\p -> tc_lpat p elt_ty)
				     pats penv thing_inside
 	; return (mkHsWrapPat coi (ListPat pats' elt_ty (Just (pat_ty,e'))) list_pat_ty, res) 
        }

tc_pat penv (PArrPat pats _) pat_ty thing_inside
  = do	{ (coi, elt_ty) <- matchExpectedPatTy matchExpectedPArrTy pat_ty
	; (pats', res) <- tcMultiple (\p -> tc_lpat p elt_ty)
				     pats penv thing_inside 
	; return (mkHsWrapPat coi (PArrPat pats' elt_ty) pat_ty, res)
        }

tc_pat penv (TuplePat pats boxity _) pat_ty thing_inside
  = do	{ let tc = tupleTyCon (boxityNormalTupleSort boxity) (length pats)
        ; (coi, arg_tys) <- matchExpectedPatTy (matchExpectedTyConApp tc) pat_ty
	; (pats', res) <- tc_lpats penv pats arg_tys thing_inside

	; dflags <- getDynFlags

	-- Under flag control turn a pattern (x,y,z) into ~(x,y,z)
	-- so that we can experiment with lazy tuple-matching.
	-- This is a pretty odd place to make the switch, but
	-- it was easy to do.
	; let pat_ty'          = mkTyConApp tc arg_tys
                                     -- pat_ty /= pat_ty iff coi /= IdCo
              unmangled_result = TuplePat pats' boxity pat_ty'
	      possibly_mangled_result
	        | gopt Opt_IrrefutableTuples dflags &&
                  isBoxed boxity            = LazyPat (noLoc unmangled_result)
	        | otherwise		    = unmangled_result

 	; ASSERT( length arg_tys == length pats )      -- Syntactically enforced
	  return (mkHsWrapPat coi possibly_mangled_result pat_ty, res)
        }

------------------------
-- Data constructors
tc_pat penv (ConPatIn con arg_pats) pat_ty thing_inside
  = tcConPat penv con pat_ty arg_pats thing_inside

------------------------
-- Literal patterns
tc_pat _ (LitPat simple_lit) pat_ty thing_inside
  = do	{ let lit_ty = hsLitType simple_lit
	; co <- unifyPatType lit_ty pat_ty
		-- coi is of kind: pat_ty ~ lit_ty
	; res <- thing_inside 
	; return ( mkHsWrapPatCo co (LitPat simple_lit) pat_ty 
                 , res) }

------------------------
-- Overloaded patterns: n, and n+k
tc_pat _ (NPat over_lit mb_neg eq) pat_ty thing_inside
  = do	{ let orig = LiteralOrigin over_lit
	; lit'    <- newOverloadedLit orig over_lit pat_ty
	; eq'     <- tcSyntaxOp orig eq (mkFunTys [pat_ty, pat_ty] boolTy)
	; mb_neg' <- case mb_neg of
			Nothing  -> return Nothing	-- Positive literal
			Just neg -> 	-- Negative literal
					-- The 'negate' is re-mappable syntax
 			    do { neg' <- tcSyntaxOp orig neg (mkFunTy pat_ty pat_ty)
			       ; return (Just neg') }
	; res <- thing_inside 
	; return (NPat lit' mb_neg' eq', res) }

tc_pat penv (NPlusKPat (L nm_loc name) lit ge minus) pat_ty thing_inside
  = do	{ (co, bndr_id) <- setSrcSpan nm_loc (tcPatBndr penv name pat_ty)
        ; let pat_ty' = idType bndr_id
	      orig    = LiteralOrigin lit
	; lit' <- newOverloadedLit orig lit pat_ty'

	-- The '>=' and '-' parts are re-mappable syntax
	; ge'    <- tcSyntaxOp orig ge    (mkFunTys [pat_ty', pat_ty'] boolTy)
	; minus' <- tcSyntaxOp orig minus (mkFunTys [pat_ty', pat_ty'] pat_ty')
        ; let pat' = NPlusKPat (L nm_loc bndr_id) lit' ge' minus'

	-- The Report says that n+k patterns must be in Integral
	-- We may not want this when using re-mappable syntax, though (ToDo?)
	; icls <- tcLookupClass integralClassName
	; instStupidTheta orig [mkClassPred icls [pat_ty']]	
    
	; res <- tcExtendIdEnv1 name bndr_id thing_inside
	; return (mkHsWrapPatCo co pat' pat_ty, res) }

tc_pat _ _other_pat _ _ = panic "tc_pat" 	-- ConPatOut, SigPatOut

----------------
unifyPatType :: TcType -> TcType -> TcM TcCoercion
-- In patterns we want a coercion from the
-- context type (expected) to the actual pattern type
-- But we don't want to reverse the args to unifyType because
-- that controls the actual/expected stuff in error messages
unifyPatType actual_ty expected_ty
  = do { coi <- unifyType actual_ty expected_ty
       ; return (mkTcSymCo coi) }

--	Running example:
-- MkT :: forall a b c. (a~[b]) => b -> c -> T a
-- 	 with scrutinee of type (T ty)

tcConPat :: PatEnv -> Located Name 
	 -> TcRhoType  	       	-- Type of the pattern
	 -> HsConPatDetails Name -> TcM a
	 -> TcM (Pat TcId, a)
tcConPat penv (L con_span con_name) pat_ty arg_pats thing_inside
  = do	{ data_con <- tcLookupDataCon con_name
	; let tycon = dataConTyCon data_con
         	  -- For data families this is the representation tycon
	      (univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _)
                = dataConFullSig data_con

	  -- Instantiate the constructor type variables [a->ty]
	  -- This may involve doing a family-instance coercion, 
	  -- and building a wrapper 
	; (wrap, ctxt_res_tys) <- matchExpectedPatTy (matchExpectedConTy tycon) pat_ty

	  -- Add the stupid theta
	; setSrcSpan con_span $ addDataConStupidTheta data_con ctxt_res_tys

	; checkExistentials ex_tvs penv 
        ; (tenv, ex_tvs') <- tcInstSuperSkolTyVarsX
                               (zipTopTvSubst univ_tvs ctxt_res_tys) ex_tvs
                     -- Get location from monad, not from ex_tvs

        ; let pat_ty' = mkTyConApp tycon ctxt_res_tys
	      -- pat_ty' is type of the actual constructor application
              -- pat_ty' /= pat_ty iff coi /= IdCo
              
	      arg_tys' = substTys tenv arg_tys

        ; traceTc "tcConPat" (ppr con_name $$ ppr ex_tvs' $$ ppr pat_ty' $$ ppr arg_tys')
	; if null ex_tvs && null eq_spec && null theta
	  then do { -- The common case; no class bindings etc 
                    -- (see Note [Arrows and patterns])
		    (arg_pats', res) <- tcConArgs data_con arg_tys' 
						  arg_pats penv thing_inside
		  ; let res_pat = ConPatOut { pat_con = L con_span data_con, 
			            	      pat_tvs = [], pat_dicts = [], 
                                              pat_binds = emptyTcEvBinds,
					      pat_args = arg_pats', 
                                              pat_ty = pat_ty' }

		  ; return (mkHsWrapPat wrap res_pat pat_ty, res) }

	  else do   -- The general case, with existential, 
                    -- and local equality constraints
	{ let theta'   = substTheta tenv (eqSpecPreds eq_spec ++ theta)
                           -- order is *important* as we generate the list of
                           -- dictionary binders from theta'
	      no_equalities = not (any isEqPred theta')
              skol_info = case pe_ctxt penv of
                            LamPat mc -> PatSkol data_con mc
                            LetPat {} -> UnkSkol -- Doesn't matter
 
        ; gadts_on    <- xoptM Opt_GADTs
        ; families_on <- xoptM Opt_TypeFamilies
	; checkTc (no_equalities || gadts_on || families_on)
	  	  (ptext (sLit "A pattern match on a GADT requires -XGADTs or -XTypeFamilies"))
		  -- Trac #2905 decided that a *pattern-match* of a GADT
		  -- should require the GADT language flag.  
                  -- Re TypeFamilies see also #7156 

        ; given <- newEvVars theta'
        ; (ev_binds, (arg_pats', res))
	     <- checkConstraints skol_info ex_tvs' given $
                tcConArgs data_con arg_tys' arg_pats penv thing_inside

        ; let res_pat = ConPatOut { pat_con   = L con_span data_con, 
			            pat_tvs   = ex_tvs',
			            pat_dicts = given,
			            pat_binds = ev_binds,
			            pat_args  = arg_pats', 
                                    pat_ty    = pat_ty' }
	; return (mkHsWrapPat wrap res_pat pat_ty, res)
	} }

----------------------------
matchExpectedPatTy :: (TcRhoType -> TcM (TcCoercion, a))
                    -> TcRhoType -> TcM (HsWrapper, a) 
-- See Note [Matching polytyped patterns]
-- Returns a wrapper : pat_ty ~ inner_ty
matchExpectedPatTy inner_match pat_ty
  | null tvs && null theta
  = do { (co, res) <- inner_match pat_ty
       ; return (coToHsWrapper (mkTcSymCo co), res) }
       	 -- The Sym is because the inner_match returns a coercion
	 -- that is the other way round to matchExpectedPatTy

  | otherwise
  = do { (_, tys, subst) <- tcInstTyVars tvs
       ; wrap1 <- instCall PatOrigin tys (substTheta subst theta)
       ; (wrap2, arg_tys) <- matchExpectedPatTy inner_match (TcType.substTy subst tau)
       ; return (wrap2 <.> wrap1 , arg_tys) }
  where
    (tvs, theta, tau) = tcSplitSigmaTy pat_ty

----------------------------
matchExpectedConTy :: TyCon  	 -- The TyCon that this data 
		    		 -- constructor actually returns
		   -> TcRhoType  -- The type of the pattern
		   -> TcM (TcCoercion, [TcSigmaType])
-- See Note [Matching constructor patterns]
-- Returns a coercion : T ty1 ... tyn ~ pat_ty
-- This is the same way round as matchExpectedListTy etc
-- but the other way round to matchExpectedPatTy
matchExpectedConTy data_tc pat_ty
  | Just (fam_tc, fam_args, co_tc) <- tyConFamInstSig_maybe data_tc
    	 -- Comments refer to Note [Matching constructor patterns]
     	 -- co_tc :: forall a. T [a] ~ T7 a
  = do { (_, tys, subst) <- tcInstTyVars (tyConTyVars data_tc)
       	     -- tys = [ty1,ty2]

       ; traceTc "matchExpectedConTy" (vcat [ppr data_tc, 
                                             ppr (tyConTyVars data_tc),
                                             ppr fam_tc, ppr fam_args])
       ; co1 <- unifyType (mkTyConApp fam_tc (substTys subst fam_args)) pat_ty
       	     -- co1 : T (ty1,ty2) ~ pat_ty

       ; let co2 = mkTcUnbranchedAxInstCo co_tc tys
       	     -- co2 : T (ty1,ty2) ~ T7 ty1 ty2

       ; return (mkTcSymCo co2 `mkTcTransCo` co1, tys) }

  | otherwise
  = matchExpectedTyConApp data_tc pat_ty
       	     -- coi : T tys ~ pat_ty

tcConArgs :: DataCon -> [TcSigmaType]
	  -> Checker (HsConPatDetails Name) (HsConPatDetails Id)

tcConArgs data_con arg_tys (PrefixCon arg_pats) penv thing_inside
  = do	{ checkTc (con_arity == no_of_args)	-- Check correct arity
		  (arityErr "Constructor" data_con con_arity no_of_args)
	; let pats_w_tys = zipEqual "tcConArgs" arg_pats arg_tys
	; (arg_pats', res) <- tcMultiple tcConArg pats_w_tys
					      penv thing_inside 
	; return (PrefixCon arg_pats', res) }
  where
    con_arity  = dataConSourceArity data_con
    no_of_args = length arg_pats

tcConArgs data_con arg_tys (InfixCon p1 p2) penv thing_inside
  = do	{ checkTc (con_arity == 2)	-- Check correct arity
	 	  (arityErr "Constructor" data_con con_arity 2)
	; let [arg_ty1,arg_ty2] = arg_tys	-- This can't fail after the arity check
	; ([p1',p2'], res) <- tcMultiple tcConArg [(p1,arg_ty1),(p2,arg_ty2)]
					      penv thing_inside
	; return (InfixCon p1' p2', res) }
  where
    con_arity  = dataConSourceArity data_con

tcConArgs data_con arg_tys (RecCon (HsRecFields rpats dd)) penv thing_inside
  = do	{ (rpats', res) <- tcMultiple tc_field rpats penv thing_inside
	; return (RecCon (HsRecFields rpats' dd), res) }
  where
    tc_field :: Checker (HsRecField FieldLabel (LPat Name)) (HsRecField TcId (LPat TcId))
    tc_field (HsRecField field_lbl pat pun) penv thing_inside
      = do { (sel_id, pat_ty) <- wrapLocFstM find_field_ty field_lbl
	   ; (pat', res) <- tcConArg (pat, pat_ty) penv thing_inside
	   ; return (HsRecField sel_id pat' pun, res) }

    find_field_ty :: FieldLabel -> TcM (Id, TcType)
    find_field_ty field_lbl
	= case [ty | (f,ty) <- field_tys, f == field_lbl] of

		-- No matching field; chances are this field label comes from some
		-- other record type (or maybe none).  As well as reporting an
		-- error we still want to typecheck the pattern, principally to
		-- make sure that all the variables it binds are put into the
		-- environment, else the type checker crashes later:
		--	f (R { foo = (a,b) }) = a+b
		-- If foo isn't one of R's fields, we don't want to crash when
		-- typechecking the "a+b".
	   [] -> do { addErrTc (badFieldCon data_con field_lbl)
		    ; bogus_ty <- newFlexiTyVarTy liftedTypeKind
		    ; return (error "Bogus selector Id", bogus_ty) }

		-- The normal case, when the field comes from the right constructor
	   (pat_ty : extras) -> 
		ASSERT( null extras )
		do { sel_id <- tcLookupField field_lbl
		   ; return (sel_id, pat_ty) }

    field_tys :: [(FieldLabel, TcType)]
    field_tys = zip (dataConFieldLabels data_con) arg_tys
	-- Don't use zipEqual! If the constructor isn't really a record, then
	-- dataConFieldLabels will be empty (and each field in the pattern
	-- will generate an error below).

tcConArg :: Checker (LPat Name, TcSigmaType) (LPat Id)
tcConArg (arg_pat, arg_ty) penv thing_inside
  = tc_lpat arg_pat arg_ty penv thing_inside

addDataConStupidTheta :: DataCon -> [TcType] -> TcM ()
-- Instantiate the "stupid theta" of the data con, and throw 
-- the constraints into the constraint set
addDataConStupidTheta data_con inst_tys
  | null stupid_theta = return ()
  | otherwise	      = instStupidTheta origin inst_theta
  where
    origin = OccurrenceOf (dataConName data_con)
	-- The origin should always report "occurrence of C"
	-- even when C occurs in a pattern
    stupid_theta = dataConStupidTheta data_con
    tenv = mkTopTvSubst (dataConUnivTyVars data_con `zip` inst_tys)
    	 -- NB: inst_tys can be longer than the univ tyvars
	 --     because the constructor might have existentials
    inst_theta = substTheta tenv stupid_theta

maybeWrapPatCtxt :: Pat Name -> (TcM a -> TcM b) -> TcM a -> TcM b
-- Not all patterns are worth pushing a context
maybeWrapPatCtxt pat tcm thing_inside 
  | not (worth_wrapping pat) = tcm thing_inside
  | otherwise                = addErrCtxt msg $ tcm $ popErrCtxt thing_inside
    			       -- Remember to pop before doing thing_inside
  where
   worth_wrapping (VarPat {}) = False
   worth_wrapping (ParPat {}) = False
   worth_wrapping (AsPat {})  = False
   worth_wrapping _  	      = True
   msg = hang (ptext (sLit "In the pattern:")) 2 (ppr pat)

-----------------------------------------------
checkExistentials :: [TyVar] -> PatEnv -> TcM ()
	  -- See Note [Arrows and patterns]
checkExistentials [] _                                 = return ()
checkExistentials _ (PE { pe_ctxt = LetPat {}})        = failWithTc existentialLetPat
checkExistentials _ (PE { pe_ctxt = LamPat ProcExpr }) = failWithTc existentialProcPat
checkExistentials _ (PE { pe_lazy = True })            = failWithTc existentialLazyPat
checkExistentials _ _                                  = return ()

existentialLazyPat :: SDoc
existentialLazyPat
  = hang (ptext (sLit "An existential or GADT data constructor cannot be used"))
       2 (ptext (sLit "inside a lazy (~) pattern"))

existentialProcPat :: SDoc
existentialProcPat 
  = ptext (sLit "Proc patterns cannot use existential or GADT data constructors")

existentialLetPat :: SDoc
existentialLetPat
  = vcat [text "My brain just exploded",
	  text "I can't handle pattern bindings for existential or GADT data constructors.",
	  text "Instead, use a case-expression, or do-notation, to unpack the constructor."]

badFieldCon :: DataCon -> Name -> SDoc
badFieldCon con field
  = hsep [ptext (sLit "Constructor") <+> quotes (ppr con),
	  ptext (sLit "does not have field"), quotes (ppr field)]

polyPatSig :: TcType -> SDoc
polyPatSig sig_ty
  = hang (ptext (sLit "Illegal polymorphic type signature in pattern:"))
       2 (ppr sig_ty)

lazyUnliftedPatErr :: OutputableBndr name => Pat name -> TcM ()
lazyUnliftedPatErr pat
  = failWithTc $
    hang (ptext (sLit "A lazy (~) pattern cannot contain unlifted types:"))
       2 (ppr pat)