never executed always true always false
    1 
    2 {-# LANGUAGE FlexibleContexts #-}
    3 {-# LANGUAGE LambdaCase #-}
    4 {-# LANGUAGE RankNTypes #-}
    5 {-# LANGUAGE TupleSections #-}
    6 {-# LANGUAGE TypeFamilies #-}
    7 
    8 {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
    9 
   10 {-
   11 (c) The University of Glasgow 2006
   12 (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
   13 
   14 -}
   15 
   16 -- | Typechecking patterns
   17 module GHC.Tc.Gen.Pat
   18    ( tcLetPat
   19    , newLetBndr
   20    , LetBndrSpec(..)
   21    , tcCheckPat, tcCheckPat_O, tcInferPat
   22    , tcPats
   23    , addDataConStupidTheta
   24    , badFieldCon
   25    , polyPatSig
   26    )
   27 where
   28 
   29 import GHC.Prelude
   30 
   31 import {-# SOURCE #-}   GHC.Tc.Gen.Expr( tcSyntaxOp, tcSyntaxOpGen, tcInferRho )
   32 
   33 import GHC.Hs
   34 import GHC.Hs.Syn.Type
   35 import GHC.Rename.Utils
   36 import GHC.Tc.Errors.Types
   37 import GHC.Tc.Utils.Zonk
   38 import GHC.Tc.Gen.Sig( TcPragEnv, lookupPragEnv, addInlinePrags )
   39 import GHC.Tc.Utils.Concrete ( mkWpFun )
   40 import GHC.Tc.Utils.Monad
   41 import GHC.Tc.Utils.Instantiate
   42 import GHC.Types.Error
   43 import GHC.Types.Id
   44 import GHC.Types.Var
   45 import GHC.Types.Name
   46 import GHC.Types.Name.Reader
   47 import GHC.Core.Multiplicity
   48 import GHC.Tc.Utils.Env
   49 import GHC.Tc.Utils.TcMType
   50 import GHC.Tc.Validity( arityErr )
   51 import GHC.Core.TyCo.Ppr ( pprTyVars )
   52 import GHC.Tc.Utils.TcType
   53 import GHC.Tc.Utils.Unify
   54 import GHC.Tc.Gen.HsType
   55 import GHC.Builtin.Types
   56 import GHC.Tc.Types.Evidence
   57 import GHC.Tc.Types.Origin
   58 import GHC.Core.TyCon
   59 import GHC.Core.Type
   60 import GHC.Core.DataCon
   61 import GHC.Core.PatSyn
   62 import GHC.Core.ConLike
   63 import GHC.Builtin.Names
   64 import GHC.Types.Basic hiding (SuccessFlag(..))
   65 import GHC.Driver.Session
   66 import GHC.Types.SrcLoc
   67 import GHC.Types.Var.Set
   68 import GHC.Utils.Misc
   69 import GHC.Utils.Outputable as Outputable
   70 import GHC.Utils.Panic
   71 import GHC.Utils.Panic.Plain
   72 import qualified GHC.LanguageExtensions as LangExt
   73 import Control.Arrow  ( second )
   74 import Control.Monad
   75 import GHC.Data.List.SetOps ( getNth )
   76 
   77 {-
   78 ************************************************************************
   79 *                                                                      *
   80                 External interface
   81 *                                                                      *
   82 ************************************************************************
   83 -}
   84 
   85 tcLetPat :: (Name -> Maybe TcId)
   86          -> LetBndrSpec
   87          -> LPat GhcRn -> Scaled ExpSigmaType
   88          -> TcM a
   89          -> TcM (LPat GhcTc, a)
   90 tcLetPat sig_fn no_gen pat pat_ty thing_inside
   91   = do { bind_lvl <- getTcLevel
   92        ; let ctxt = LetPat { pc_lvl    = bind_lvl
   93                            , pc_sig_fn = sig_fn
   94                            , pc_new    = no_gen }
   95              penv = PE { pe_lazy = True
   96                        , pe_ctxt = ctxt
   97                        , pe_orig = PatOrigin }
   98 
   99        ; tc_lpat pat_ty penv pat thing_inside }
  100 
  101 -----------------
  102 tcPats :: HsMatchContext GhcTc
  103        -> [LPat GhcRn]            -- Patterns,
  104        -> [Scaled ExpSigmaType]         --   and their types
  105        -> TcM a                  --   and the checker for the body
  106        -> TcM ([LPat GhcTc], a)
  107 
  108 -- This is the externally-callable wrapper function
  109 -- Typecheck the patterns, extend the environment to bind the variables,
  110 -- do the thing inside, use any existentially-bound dictionaries to
  111 -- discharge parts of the returning LIE, and deal with pattern type
  112 -- signatures
  113 
  114 --   1. Initialise the PatState
  115 --   2. Check the patterns
  116 --   3. Check the body
  117 --   4. Check that no existentials escape
  118 
  119 tcPats ctxt pats pat_tys thing_inside
  120   = tc_lpats pat_tys penv pats thing_inside
  121   where
  122     penv = PE { pe_lazy = False, pe_ctxt = LamPat ctxt, pe_orig = PatOrigin }
  123 
  124 tcInferPat :: HsMatchContext GhcTc -> LPat GhcRn
  125            -> TcM a
  126            -> TcM ((LPat GhcTc, a), TcSigmaType)
  127 tcInferPat ctxt pat thing_inside
  128   = tcInfer $ \ exp_ty ->
  129     tc_lpat (unrestricted exp_ty) penv pat thing_inside
  130  where
  131     penv = PE { pe_lazy = False, pe_ctxt = LamPat ctxt, pe_orig = PatOrigin }
  132 
  133 tcCheckPat :: HsMatchContext GhcTc
  134            -> LPat GhcRn -> Scaled TcSigmaType
  135            -> TcM a                     -- Checker for body
  136            -> TcM (LPat GhcTc, a)
  137 tcCheckPat ctxt = tcCheckPat_O ctxt PatOrigin
  138 
  139 -- | A variant of 'tcPat' that takes a custom origin
  140 tcCheckPat_O :: HsMatchContext GhcTc
  141              -> CtOrigin              -- ^ origin to use if the type needs inst'ing
  142              -> LPat GhcRn -> Scaled TcSigmaType
  143              -> TcM a                 -- Checker for body
  144              -> TcM (LPat GhcTc, a)
  145 tcCheckPat_O ctxt orig pat (Scaled pat_mult pat_ty) thing_inside
  146   = tc_lpat (Scaled pat_mult (mkCheckExpType pat_ty)) penv pat thing_inside
  147   where
  148     penv = PE { pe_lazy = False, pe_ctxt = LamPat ctxt, pe_orig = orig }
  149 
  150 
  151 {-
  152 ************************************************************************
  153 *                                                                      *
  154                 PatEnv, PatCtxt, LetBndrSpec
  155 *                                                                      *
  156 ************************************************************************
  157 -}
  158 
  159 data PatEnv
  160   = PE { pe_lazy :: Bool        -- True <=> lazy context, so no existentials allowed
  161        , pe_ctxt :: PatCtxt     -- Context in which the whole pattern appears
  162        , pe_orig :: CtOrigin    -- origin to use if the pat_ty needs inst'ing
  163        }
  164 
  165 data PatCtxt
  166   = LamPat   -- Used for lambdas, case etc
  167        (HsMatchContext GhcTc)
  168 
  169   | LetPat   -- Used only for let(rec) pattern bindings
  170              -- See Note [Typing patterns in pattern bindings]
  171        { pc_lvl    :: TcLevel
  172                    -- Level of the binding group
  173 
  174        , pc_sig_fn :: Name -> Maybe TcId
  175                    -- Tells the expected type
  176                    -- for binders with a signature
  177 
  178        , pc_new :: LetBndrSpec
  179                 -- How to make a new binder
  180        }        -- for binders without signatures
  181 
  182 data LetBndrSpec
  183   = LetLclBndr            -- We are going to generalise, and wrap in an AbsBinds
  184                           -- so clone a fresh binder for the local monomorphic Id
  185 
  186   | LetGblBndr TcPragEnv  -- Generalisation plan is NoGen, so there isn't going
  187                           -- to be an AbsBinds; So we must bind the global version
  188                           -- of the binder right away.
  189                           -- And here is the inline-pragma information
  190 
  191 instance Outputable LetBndrSpec where
  192   ppr LetLclBndr      = text "LetLclBndr"
  193   ppr (LetGblBndr {}) = text "LetGblBndr"
  194 
  195 makeLazy :: PatEnv -> PatEnv
  196 makeLazy penv = penv { pe_lazy = True }
  197 
  198 inPatBind :: PatEnv -> Bool
  199 inPatBind (PE { pe_ctxt = LetPat {} }) = True
  200 inPatBind (PE { pe_ctxt = LamPat {} }) = False
  201 
  202 {- *********************************************************************
  203 *                                                                      *
  204                 Binders
  205 *                                                                      *
  206 ********************************************************************* -}
  207 
  208 tcPatBndr :: PatEnv -> Name -> Scaled ExpSigmaType -> TcM (HsWrapper, TcId)
  209 -- (coi, xp) = tcPatBndr penv x pat_ty
  210 -- Then coi : pat_ty ~ typeof(xp)
  211 --
  212 tcPatBndr penv@(PE { pe_ctxt = LetPat { pc_lvl    = bind_lvl
  213                                       , pc_sig_fn = sig_fn
  214                                       , pc_new    = no_gen } })
  215           bndr_name exp_pat_ty
  216   -- For the LetPat cases, see
  217   -- Note [Typechecking pattern bindings] in GHC.Tc.Gen.Bind
  218 
  219   | Just bndr_id <- sig_fn bndr_name   -- There is a signature
  220   = do { wrap <- tc_sub_type penv (scaledThing exp_pat_ty) (idType bndr_id)
  221            -- See Note [Subsumption check at pattern variables]
  222        ; traceTc "tcPatBndr(sig)" (ppr bndr_id $$ ppr (idType bndr_id) $$ ppr exp_pat_ty)
  223        ; return (wrap, bndr_id) }
  224 
  225   | otherwise                          -- No signature
  226   = do { (co, bndr_ty) <- case scaledThing exp_pat_ty of
  227              Check pat_ty    -> promoteTcType bind_lvl pat_ty
  228              Infer infer_res -> assert (bind_lvl == ir_lvl infer_res) $
  229                                 -- If we were under a constructor that bumped the
  230                                 -- level, we'd be in checking mode (see tcConArg)
  231                                 -- hence this assertion
  232                                 do { bndr_ty <- inferResultToType infer_res
  233                                    ; return (mkTcNomReflCo bndr_ty, bndr_ty) }
  234        ; let bndr_mult = scaledMult exp_pat_ty
  235        ; bndr_id <- newLetBndr no_gen bndr_name bndr_mult bndr_ty
  236        ; traceTc "tcPatBndr(nosig)" (vcat [ ppr bind_lvl
  237                                           , ppr exp_pat_ty, ppr bndr_ty, ppr co
  238                                           , ppr bndr_id ])
  239        ; return (mkWpCastN co, bndr_id) }
  240 
  241 tcPatBndr _ bndr_name pat_ty
  242   = do { let pat_mult = scaledMult pat_ty
  243        ; pat_ty <- expTypeToType (scaledThing pat_ty)
  244        ; traceTc "tcPatBndr(not let)" (ppr bndr_name $$ ppr pat_ty)
  245        ; return (idHsWrapper, mkLocalIdOrCoVar bndr_name pat_mult pat_ty) }
  246                -- We should not have "OrCoVar" here, this is a bug (#17545)
  247                -- Whether or not there is a sig is irrelevant,
  248                -- as this is local
  249 
  250 newLetBndr :: LetBndrSpec -> Name -> Mult -> TcType -> TcM TcId
  251 -- Make up a suitable Id for the pattern-binder.
  252 -- See Note [Typechecking pattern bindings], item (4) in GHC.Tc.Gen.Bind
  253 --
  254 -- In the polymorphic case when we are going to generalise
  255 --    (plan InferGen, no_gen = LetLclBndr), generate a "monomorphic version"
  256 --    of the Id; the original name will be bound to the polymorphic version
  257 --    by the AbsBinds
  258 -- In the monomorphic case when we are not going to generalise
  259 --    (plan NoGen, no_gen = LetGblBndr) there is no AbsBinds,
  260 --    and we use the original name directly
  261 newLetBndr LetLclBndr name w ty
  262   = do { mono_name <- cloneLocalName name
  263        ; return (mkLocalId mono_name w ty) }
  264 newLetBndr (LetGblBndr prags) name w ty
  265   = addInlinePrags (mkLocalId name w ty) (lookupPragEnv prags name)
  266 
  267 tc_sub_type :: PatEnv -> ExpSigmaType -> TcSigmaType -> TcM HsWrapper
  268 -- tcSubTypeET with the UserTypeCtxt specialised to GenSigCtxt
  269 -- Used during typechecking patterns
  270 tc_sub_type penv t1 t2 = tcSubTypePat (pe_orig penv) GenSigCtxt t1 t2
  271 
  272 {- Note [Subsumption check at pattern variables]
  273 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  274 When we come across a variable with a type signature, we need to do a
  275 subsumption, not equality, check against the context type.  e.g.
  276 
  277     data T = MkT (forall a. a->a)
  278       f :: forall b. [b]->[b]
  279       MkT f = blah
  280 
  281 Since 'blah' returns a value of type T, its payload is a polymorphic
  282 function of type (forall a. a->a).  And that's enough to bind the
  283 less-polymorphic function 'f', but we need some impedance matching
  284 to witness the instantiation.
  285 
  286 
  287 ************************************************************************
  288 *                                                                      *
  289                 The main worker functions
  290 *                                                                      *
  291 ************************************************************************
  292 
  293 Note [Nesting]
  294 ~~~~~~~~~~~~~~
  295 tcPat takes a "thing inside" over which the pattern scopes.  This is partly
  296 so that tcPat can extend the environment for the thing_inside, but also
  297 so that constraints arising in the thing_inside can be discharged by the
  298 pattern.
  299 
  300 This does not work so well for the ErrCtxt carried by the monad: we don't
  301 want the error-context for the pattern to scope over the RHS.
  302 Hence the getErrCtxt/setErrCtxt stuff in tcMultiple
  303 -}
  304 
  305 --------------------
  306 
  307 type Checker inp out =  forall r.
  308                           PatEnv
  309                        -> inp
  310                        -> TcM r      -- Thing inside
  311                        -> TcM ( out
  312                               , r    -- Result of thing inside
  313                               )
  314 
  315 tcMultiple :: Checker inp out -> Checker [inp] [out]
  316 tcMultiple tc_pat penv args thing_inside
  317   = do  { err_ctxt <- getErrCtxt
  318         ; let loop _ []
  319                 = do { res <- thing_inside
  320                      ; return ([], res) }
  321 
  322               loop penv (arg:args)
  323                 = do { (p', (ps', res))
  324                                 <- tc_pat penv arg $
  325                                    setErrCtxt err_ctxt $
  326                                    loop penv args
  327                 -- setErrCtxt: restore context before doing the next pattern
  328                 -- See note [Nesting] above
  329 
  330                      ; return (p':ps', res) }
  331 
  332         ; loop penv args }
  333 
  334 --------------------
  335 tc_lpat :: Scaled ExpSigmaType
  336         -> Checker (LPat GhcRn) (LPat GhcTc)
  337 tc_lpat pat_ty penv (L span pat) thing_inside
  338   = setSrcSpanA span $
  339     do  { (pat', res) <- maybeWrapPatCtxt pat (tc_pat pat_ty penv pat)
  340                                           thing_inside
  341         ; return (L span pat', res) }
  342 
  343 tc_lpats :: [Scaled ExpSigmaType]
  344          -> Checker [LPat GhcRn] [LPat GhcTc]
  345 tc_lpats tys penv pats
  346   = assertPpr (equalLength pats tys) (ppr pats $$ ppr tys) $
  347     tcMultiple (\ penv' (p,t) -> tc_lpat t penv' p)
  348                penv
  349                (zipEqual "tc_lpats" pats tys)
  350 
  351 --------------------
  352 -- See Note [Wrapper returned from tcSubMult] in GHC.Tc.Utils.Unify.
  353 checkManyPattern :: Scaled a -> TcM HsWrapper
  354 checkManyPattern pat_ty = tcSubMult NonLinearPatternOrigin Many (scaledMult pat_ty)
  355 
  356 tc_pat  :: Scaled ExpSigmaType
  357         -- ^ Fully refined result type
  358         -> Checker (Pat GhcRn) (Pat GhcTc)
  359         -- ^ Translated pattern
  360 
  361 tc_pat pat_ty penv ps_pat thing_inside = case ps_pat of
  362 
  363   VarPat x (L l name) -> do
  364         { (wrap, id) <- tcPatBndr penv name pat_ty
  365         ; (res, mult_wrap) <- tcCheckUsage name (scaledMult pat_ty) $
  366                               tcExtendIdEnv1 name id thing_inside
  367             -- See Note [Wrapper returned from tcSubMult] in GHC.Tc.Utils.Unify.
  368         ; pat_ty <- readExpType (scaledThing pat_ty)
  369         ; return (mkHsWrapPat (wrap <.> mult_wrap) (VarPat x (L l id)) pat_ty, res) }
  370 
  371   ParPat x lpar pat rpar -> do
  372         { (pat', res) <- tc_lpat pat_ty penv pat thing_inside
  373         ; return (ParPat x lpar pat' rpar, res) }
  374 
  375   BangPat x pat -> do
  376         { (pat', res) <- tc_lpat pat_ty penv pat thing_inside
  377         ; return (BangPat x pat', res) }
  378 
  379   LazyPat x pat -> do
  380         { mult_wrap <- checkManyPattern pat_ty
  381             -- See Note [Wrapper returned from tcSubMult] in GHC.Tc.Utils.Unify.
  382         ; (pat', (res, pat_ct))
  383                 <- tc_lpat pat_ty (makeLazy penv) pat $
  384                    captureConstraints thing_inside
  385                 -- Ignore refined penv', revert to penv
  386 
  387         ; emitConstraints pat_ct
  388         -- captureConstraints/extendConstraints:
  389         --   see Note [Hopping the LIE in lazy patterns]
  390 
  391         -- Check that the expected pattern type is itself lifted
  392         ; pat_ty <- readExpType (scaledThing pat_ty)
  393         ; _ <- unifyType Nothing (tcTypeKind pat_ty) liftedTypeKind
  394 
  395         ; return (mkHsWrapPat mult_wrap (LazyPat x pat') pat_ty, res) }
  396 
  397   WildPat _ -> do
  398         { mult_wrap <- checkManyPattern pat_ty
  399             -- See Note [Wrapper returned from tcSubMult] in GHC.Tc.Utils.Unify.
  400         ; res <- thing_inside
  401         ; pat_ty <- expTypeToType (scaledThing pat_ty)
  402         ; return (mkHsWrapPat mult_wrap (WildPat pat_ty) pat_ty, res) }
  403 
  404   AsPat x (L nm_loc name) pat -> do
  405         { mult_wrap <- checkManyPattern pat_ty
  406             -- See Note [Wrapper returned from tcSubMult] in GHC.Tc.Utils.Unify.
  407         ; (wrap, bndr_id) <- setSrcSpanA nm_loc (tcPatBndr penv name pat_ty)
  408         ; (pat', res) <- tcExtendIdEnv1 name bndr_id $
  409                          tc_lpat (pat_ty `scaledSet`(mkCheckExpType $ idType bndr_id))
  410                                  penv pat thing_inside
  411             -- NB: if we do inference on:
  412             --          \ (y@(x::forall a. a->a)) = e
  413             -- we'll fail.  The as-pattern infers a monotype for 'y', which then
  414             -- fails to unify with the polymorphic type for 'x'.  This could
  415             -- perhaps be fixed, but only with a bit more work.
  416             --
  417             -- If you fix it, don't forget the bindInstsOfPatIds!
  418         ; pat_ty <- readExpType (scaledThing pat_ty)
  419         ; return (mkHsWrapPat (wrap <.> mult_wrap) (AsPat x (L nm_loc bndr_id) pat') pat_ty, res) }
  420 
  421   ViewPat _ expr pat -> do
  422         { mult_wrap <- checkManyPattern pat_ty
  423          -- See Note [Wrapper returned from tcSubMult] in GHC.Tc.Utils.Unify.
  424          --
  425          -- It should be possible to have view patterns at linear (or otherwise
  426          -- non-Many) multiplicity. But it is not clear at the moment what
  427          -- restriction need to be put in place, if any, for linear view
  428          -- patterns to desugar to type-correct Core.
  429 
  430         ; (expr',expr_ty) <- tcInferRho expr
  431                -- Note [View patterns and polymorphism]
  432 
  433          -- Expression must be a function
  434         ; let herald = text "A view pattern expression expects"
  435         ; (expr_wrap1, Scaled _mult inf_arg_ty, inf_res_sigma)
  436             <- matchActualFunTySigma herald (Just (ppr expr)) (1,[]) expr_ty
  437                -- See Note [View patterns and polymorphism]
  438                -- expr_wrap1 :: expr_ty "->" (inf_arg_ty -> inf_res_sigma)
  439 
  440          -- Check that overall pattern is more polymorphic than arg type
  441         ; expr_wrap2 <- tc_sub_type penv (scaledThing pat_ty) inf_arg_ty
  442             -- expr_wrap2 :: pat_ty "->" inf_arg_ty
  443 
  444          -- Pattern must have inf_res_sigma
  445         ; (pat', res) <- tc_lpat (pat_ty `scaledSet` mkCheckExpType inf_res_sigma) penv pat thing_inside
  446 
  447         ; let Scaled w h_pat_ty = pat_ty
  448         ; pat_ty <- readExpType h_pat_ty
  449         ; expr_wrap2' <- mkWpFun expr_wrap2 idHsWrapper
  450                             (Scaled w pat_ty) inf_res_sigma (WpFunViewPat $ unLoc expr)
  451         -- expr_wrap2' :: (inf_arg_ty -> inf_res_sigma) "->"
  452         --                (pat_ty -> inf_res_sigma)
  453         ; let
  454               expr_wrap = expr_wrap2' <.> expr_wrap1 <.> mult_wrap
  455 
  456         ; return $ (ViewPat pat_ty (mkLHsWrap expr_wrap expr') pat', res) }
  457 
  458 {- Note [View patterns and polymorphism]
  459 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  460 Consider this exotic example:
  461    pair :: forall a. Bool -> a -> forall b. b -> (a,b)
  462 
  463    f :: Int -> blah
  464    f (pair True -> x) = ...here (x :: forall b. b -> (Int,b))
  465 
  466 The expression (pair True) should have type
  467     pair True :: Int -> forall b. b -> (Int,b)
  468 so that it is ready to consume the incoming Int. It should be an
  469 arrow type (t1 -> t2); hence using (tcInferRho expr).
  470 
  471 Then, when taking that arrow apart we want to get a *sigma* type
  472 (forall b. b->(Int,b)), because that's what we want to bind 'x' to.
  473 Fortunately that's what matchExpectedFunTySigma returns anyway.
  474 -}
  475 
  476 -- Type signatures in patterns
  477 -- See Note [Pattern coercions] below
  478   SigPat _ pat sig_ty -> do
  479         { (inner_ty, tv_binds, wcs, wrap) <- tcPatSig (inPatBind penv)
  480                                                             sig_ty (scaledThing pat_ty)
  481                 -- Using tcExtendNameTyVarEnv is appropriate here
  482                 -- because we're not really bringing fresh tyvars into scope.
  483                 -- We're *naming* existing tyvars. Note that it is OK for a tyvar
  484                 -- from an outer scope to mention one of these tyvars in its kind.
  485         ; (pat', res) <- tcExtendNameTyVarEnv wcs      $
  486                          tcExtendNameTyVarEnv tv_binds $
  487                          tc_lpat (pat_ty `scaledSet` mkCheckExpType inner_ty) penv pat thing_inside
  488         ; pat_ty <- readExpType (scaledThing pat_ty)
  489         ; return (mkHsWrapPat wrap (SigPat inner_ty pat' sig_ty) pat_ty, res) }
  490 
  491 ------------------------
  492 -- Lists, tuples, arrays
  493 
  494   -- Necessarily a built-in list pattern, not an overloaded list pattern.
  495   -- See Note [Desugaring overloaded list patterns].
  496   ListPat _ pats -> do
  497         { (coi, elt_ty) <- matchExpectedPatTy matchExpectedListTy penv (scaledThing pat_ty)
  498         ; (pats', res) <- tcMultiple (tc_lpat (pat_ty `scaledSet` mkCheckExpType elt_ty))
  499                                      penv pats thing_inside
  500         ; pat_ty <- readExpType (scaledThing pat_ty)
  501         ; return (mkHsWrapPat coi
  502                          (ListPat elt_ty pats') pat_ty, res)
  503 }
  504 
  505   TuplePat _ pats boxity -> do
  506         { let arity = length pats
  507               tc = tupleTyCon boxity arity
  508               -- NB: tupleTyCon does not flatten 1-tuples
  509               -- See Note [Don't flatten tuples from HsSyn] in GHC.Core.Make
  510         ; checkTupSize arity
  511         ; (coi, arg_tys) <- matchExpectedPatTy (matchExpectedTyConApp tc)
  512                                                penv (scaledThing pat_ty)
  513                      -- Unboxed tuples have RuntimeRep vars, which we discard:
  514                      -- See Note [Unboxed tuple RuntimeRep vars] in GHC.Core.TyCon
  515         ; let con_arg_tys = case boxity of Unboxed -> drop arity arg_tys
  516                                            Boxed   -> arg_tys
  517         ; (pats', res) <- tc_lpats (map (scaledSet pat_ty . mkCheckExpType) con_arg_tys)
  518                                    penv pats thing_inside
  519 
  520         ; dflags <- getDynFlags
  521 
  522         -- Under flag control turn a pattern (x,y,z) into ~(x,y,z)
  523         -- so that we can experiment with lazy tuple-matching.
  524         -- This is a pretty odd place to make the switch, but
  525         -- it was easy to do.
  526         ; let
  527               unmangled_result = TuplePat con_arg_tys pats' boxity
  528                                  -- pat_ty /= pat_ty iff coi /= IdCo
  529               possibly_mangled_result
  530                 | gopt Opt_IrrefutableTuples dflags &&
  531                   isBoxed boxity   = LazyPat noExtField (noLocA unmangled_result)
  532                 | otherwise        = unmangled_result
  533 
  534         ; pat_ty <- readExpType (scaledThing pat_ty)
  535         ; massert (con_arg_tys `equalLength` pats) -- Syntactically enforced
  536         ; return (mkHsWrapPat coi possibly_mangled_result pat_ty, res)
  537         }
  538 
  539   SumPat _ pat alt arity  -> do
  540         { let tc = sumTyCon arity
  541         ; (coi, arg_tys) <- matchExpectedPatTy (matchExpectedTyConApp tc)
  542                                                penv (scaledThing pat_ty)
  543         ; -- Drop levity vars, we don't care about them here
  544           let con_arg_tys = drop arity arg_tys
  545         ; (pat', res) <- tc_lpat (pat_ty `scaledSet` mkCheckExpType (con_arg_tys `getNth` (alt - 1)))
  546                                  penv pat thing_inside
  547         ; pat_ty <- readExpType (scaledThing pat_ty)
  548         ; return (mkHsWrapPat coi (SumPat con_arg_tys pat' alt arity) pat_ty
  549                  , res)
  550         }
  551 
  552 ------------------------
  553 -- Data constructors
  554   ConPat _ con arg_pats ->
  555     tcConPat penv con pat_ty arg_pats thing_inside
  556 
  557 ------------------------
  558 -- Literal patterns
  559   LitPat x simple_lit -> do
  560         { let lit_ty = hsLitType simple_lit
  561         ; wrap   <- tc_sub_type penv (scaledThing pat_ty) lit_ty
  562         ; res    <- thing_inside
  563         ; pat_ty <- readExpType (scaledThing pat_ty)
  564         ; return ( mkHsWrapPat wrap (LitPat x (convertLit simple_lit)) pat_ty
  565                  , res) }
  566 
  567 ------------------------
  568 -- Overloaded patterns: n, and n+k
  569 
  570 -- In the case of a negative literal (the more complicated case),
  571 -- we get
  572 --
  573 --   case v of (-5) -> blah
  574 --
  575 -- becoming
  576 --
  577 --   if v == (negate (fromInteger 5)) then blah else ...
  578 --
  579 -- There are two bits of rebindable syntax:
  580 --   (==)   :: pat_ty -> neg_lit_ty -> Bool
  581 --   negate :: lit_ty -> neg_lit_ty
  582 -- where lit_ty is the type of the overloaded literal 5.
  583 --
  584 -- When there is no negation, neg_lit_ty and lit_ty are the same
  585   NPat _ (L l over_lit) mb_neg eq -> do
  586         { mult_wrap <- checkManyPattern pat_ty
  587           -- See Note [Wrapper returned from tcSubMult] in GHC.Tc.Utils.Unify.
  588           --
  589           -- It may be possible to refine linear pattern so that they work in
  590           -- linear environments. But it is not clear how useful this is.
  591         ; let orig = LiteralOrigin over_lit
  592         ; ((lit', mb_neg'), eq')
  593             <- tcSyntaxOp orig eq [SynType (scaledThing pat_ty), SynAny]
  594                           (mkCheckExpType boolTy) $
  595                \ [neg_lit_ty] _ ->
  596                let new_over_lit lit_ty = newOverloadedLit over_lit
  597                                            (mkCheckExpType lit_ty)
  598                in case mb_neg of
  599                  Nothing  -> (, Nothing) <$> new_over_lit neg_lit_ty
  600                  Just neg -> -- Negative literal
  601                              -- The 'negate' is re-mappable syntax
  602                    second Just <$>
  603                    (tcSyntaxOp orig neg [SynRho] (mkCheckExpType neg_lit_ty) $
  604                     \ [lit_ty] _ -> new_over_lit lit_ty)
  605                      -- applied to a closed literal: linearity doesn't matter as
  606                      -- literals are typed in an empty environment, hence have
  607                      -- all multiplicities.
  608 
  609         ; res <- thing_inside
  610         ; pat_ty <- readExpType (scaledThing pat_ty)
  611         ; return (mkHsWrapPat mult_wrap (NPat pat_ty (L l lit') mb_neg' eq') pat_ty, res) }
  612 
  613 {-
  614 Note [NPlusK patterns]
  615 ~~~~~~~~~~~~~~~~~~~~~~
  616 From
  617 
  618   case v of x + 5 -> blah
  619 
  620 we get
  621 
  622   if v >= 5 then (\x -> blah) (v - 5) else ...
  623 
  624 There are two bits of rebindable syntax:
  625   (>=) :: pat_ty -> lit1_ty -> Bool
  626   (-)  :: pat_ty -> lit2_ty -> var_ty
  627 
  628 lit1_ty and lit2_ty could conceivably be different.
  629 var_ty is the type inferred for x, the variable in the pattern.
  630 
  631 Note that we need to type-check the literal twice, because it is used
  632 twice, and may be used at different types. The second HsOverLit stored in the
  633 AST is used for the subtraction operation.
  634 -}
  635 
  636 -- See Note [NPlusK patterns]
  637   NPlusKPat _ (L nm_loc name)
  638                (L loc lit) _ ge minus -> do
  639         { mult_wrap <- checkManyPattern pat_ty
  640             -- See Note [Wrapper returned from tcSubMult] in GHC.Tc.Utils.Unify.
  641         ; let pat_exp_ty = scaledThing pat_ty
  642               orig = LiteralOrigin lit
  643         ; (lit1', ge')
  644             <- tcSyntaxOp orig ge [SynType pat_exp_ty, SynRho]
  645                                   (mkCheckExpType boolTy) $
  646                \ [lit1_ty] _ ->
  647                newOverloadedLit lit (mkCheckExpType lit1_ty)
  648         ; ((lit2', minus_wrap, bndr_id), minus')
  649             <- tcSyntaxOpGen orig minus [SynType pat_exp_ty, SynRho] SynAny $
  650                \ [lit2_ty, var_ty] _ ->
  651                do { lit2' <- newOverloadedLit lit (mkCheckExpType lit2_ty)
  652                   ; (wrap, bndr_id) <- setSrcSpanA nm_loc $
  653                                      tcPatBndr penv name (unrestricted $ mkCheckExpType var_ty)
  654                            -- co :: var_ty ~ idType bndr_id
  655 
  656                            -- minus_wrap is applicable to minus'
  657                   ; return (lit2', wrap, bndr_id) }
  658 
  659         ; pat_ty <- readExpType pat_exp_ty
  660 
  661         -- The Report says that n+k patterns must be in Integral
  662         -- but it's silly to insist on this in the RebindableSyntax case
  663         ; unlessM (xoptM LangExt.RebindableSyntax) $
  664           do { icls <- tcLookupClass integralClassName
  665              ; instStupidTheta orig [mkClassPred icls [pat_ty]] }
  666 
  667         ; res <- tcExtendIdEnv1 name bndr_id thing_inside
  668 
  669         ; let minus'' = case minus' of
  670                           NoSyntaxExprTc -> pprPanic "tc_pat NoSyntaxExprTc" (ppr minus')
  671                                    -- this should be statically avoidable
  672                                    -- Case (3) from Note [NoSyntaxExpr] in "GHC.Hs.Expr"
  673                           SyntaxExprTc { syn_expr = minus'_expr
  674                                        , syn_arg_wraps = minus'_arg_wraps
  675                                        , syn_res_wrap = minus'_res_wrap }
  676                             -> SyntaxExprTc { syn_expr = minus'_expr
  677                                             , syn_arg_wraps = minus'_arg_wraps
  678                                             , syn_res_wrap = minus_wrap <.> minus'_res_wrap }
  679                              -- Oy. This should really be a record update, but
  680                              -- we get warnings if we try. #17783
  681               pat' = NPlusKPat pat_ty (L nm_loc bndr_id) (L loc lit1') lit2'
  682                                ge' minus''
  683         ; return (mkHsWrapPat mult_wrap pat' pat_ty, res) }
  684 
  685 -- HsSpliced is an annotation produced by 'GHC.Rename.Splice.rnSplicePat'.
  686 -- Here we get rid of it and add the finalizers to the global environment.
  687 --
  688 -- See Note [Delaying modFinalizers in untyped splices] in GHC.Rename.Splice.
  689   SplicePat _ splice -> case splice of
  690     (HsSpliced _ mod_finalizers (HsSplicedPat pat)) -> do
  691       { addModFinalizersWithLclEnv mod_finalizers
  692       ; tc_pat pat_ty penv pat thing_inside }
  693     _ -> panic "invalid splice in splice pat"
  694 
  695   XPat (HsPatExpanded lpat rpat) -> do
  696     { (rpat', res) <- tc_pat pat_ty penv rpat thing_inside
  697     ; return (XPat $ ExpansionPat lpat rpat', res) }
  698 
  699 {-
  700 Note [Hopping the LIE in lazy patterns]
  701 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  702 In a lazy pattern, we must *not* discharge constraints from the RHS
  703 from dictionaries bound in the pattern.  E.g.
  704         f ~(C x) = 3
  705 We can't discharge the Num constraint from dictionaries bound by
  706 the pattern C!
  707 
  708 So we have to make the constraints from thing_inside "hop around"
  709 the pattern.  Hence the captureConstraints and emitConstraints.
  710 
  711 The same thing ensures that equality constraints in a lazy match
  712 are not made available in the RHS of the match. For example
  713         data T a where { T1 :: Int -> T Int; ... }
  714         f :: T a -> Int -> a
  715         f ~(T1 i) y = y
  716 It's obviously not sound to refine a to Int in the right
  717 hand side, because the argument might not match T1 at all!
  718 
  719 Finally, a lazy pattern should not bind any existential type variables
  720 because they won't be in scope when we do the desugaring
  721 
  722 
  723 ************************************************************************
  724 *                                                                      *
  725             Pattern signatures   (pat :: type)
  726 *                                                                      *
  727 ************************************************************************
  728 -}
  729 
  730 tcPatSig :: Bool                    -- True <=> pattern binding
  731          -> HsPatSigType GhcRn
  732          -> ExpSigmaType
  733          -> TcM (TcType,            -- The type to use for "inside" the signature
  734                  [(Name,TcTyVar)],  -- The new bit of type environment, binding
  735                                     -- the scoped type variables
  736                  [(Name,TcTyVar)],  -- The wildcards
  737                  HsWrapper)         -- Coercion due to unification with actual ty
  738                                     -- Of shape:  res_ty ~ sig_ty
  739 tcPatSig in_pat_bind sig res_ty
  740  = do  { (sig_wcs, sig_tvs, sig_ty) <- tcHsPatSigType PatSigCtxt HM_Sig sig OpenKind
  741         -- sig_tvs are the type variables free in 'sig',
  742         -- and not already in scope. These are the ones
  743         -- that should be brought into scope
  744 
  745         ; if null sig_tvs then do {
  746                 -- Just do the subsumption check and return
  747                   wrap <- addErrCtxtM (mk_msg sig_ty) $
  748                           tcSubTypePat PatSigOrigin PatSigCtxt res_ty sig_ty
  749                 ; return (sig_ty, [], sig_wcs, wrap)
  750         } else do
  751                 -- Type signature binds at least one scoped type variable
  752 
  753                 -- A pattern binding cannot bind scoped type variables
  754                 -- It is more convenient to make the test here
  755                 -- than in the renamer
  756         { when in_pat_bind (addErr (patBindSigErr sig_tvs))
  757 
  758         -- Now do a subsumption check of the pattern signature against res_ty
  759         ; wrap <- addErrCtxtM (mk_msg sig_ty) $
  760                   tcSubTypePat PatSigOrigin PatSigCtxt res_ty sig_ty
  761 
  762         -- Phew!
  763         ; return (sig_ty, sig_tvs, sig_wcs, wrap)
  764         } }
  765   where
  766     mk_msg sig_ty tidy_env
  767        = do { (tidy_env, sig_ty) <- zonkTidyTcType tidy_env sig_ty
  768             ; res_ty <- readExpType res_ty   -- should be filled in by now
  769             ; (tidy_env, res_ty) <- zonkTidyTcType tidy_env res_ty
  770             ; let msg = vcat [ hang (text "When checking that the pattern signature:")
  771                                   4 (ppr sig_ty)
  772                              , nest 2 (hang (text "fits the type of its context:")
  773                                           2 (ppr res_ty)) ]
  774             ; return (tidy_env, msg) }
  775 
  776 patBindSigErr :: [(Name,TcTyVar)] -> TcRnMessage
  777 patBindSigErr sig_tvs
  778   = TcRnUnknownMessage $ mkPlainError noHints $
  779     hang (text "You cannot bind scoped type variable" <> plural sig_tvs
  780           <+> pprQuotedList (map fst sig_tvs))
  781        2 (text "in a pattern binding signature")
  782 
  783 
  784 {- *********************************************************************
  785 *                                                                      *
  786         Most of the work for constructors is here
  787         (the rest is in the ConPatIn case of tc_pat)
  788 *                                                                      *
  789 ************************************************************************
  790 
  791 [Pattern matching indexed data types]
  792 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  793 Consider the following declarations:
  794 
  795   data family Map k :: * -> *
  796   data instance Map (a, b) v = MapPair (Map a (Pair b v))
  797 
  798 and a case expression
  799 
  800   case x :: Map (Int, c) w of MapPair m -> ...
  801 
  802 As explained by [Wrappers for data instance tycons] in GHC.Types.Id.Make, the
  803 worker/wrapper types for MapPair are
  804 
  805   $WMapPair :: forall a b v. Map a (Map a b v) -> Map (a, b) v
  806   $wMapPair :: forall a b v. Map a (Map a b v) -> :R123Map a b v
  807 
  808 So, the type of the scrutinee is Map (Int, c) w, but the tycon of MapPair is
  809 :R123Map, which means the straight use of boxySplitTyConApp would give a type
  810 error.  Hence, the smart wrapper function boxySplitTyConAppWithFamily calls
  811 boxySplitTyConApp with the family tycon Map instead, which gives us the family
  812 type list {(Int, c), w}.  To get the correct split for :R123Map, we need to
  813 unify the family type list {(Int, c), w} with the instance types {(a, b), v}
  814 (provided by tyConFamInst_maybe together with the family tycon).  This
  815 unification yields the substitution [a -> Int, b -> c, v -> w], which gives us
  816 the split arguments for the representation tycon :R123Map as {Int, c, w}
  817 
  818 In other words, boxySplitTyConAppWithFamily implicitly takes the coercion
  819 
  820   Co123Map a b v :: {Map (a, b) v ~ :R123Map a b v}
  821 
  822 moving between representation and family type into account.  To produce type
  823 correct Core, this coercion needs to be used to case the type of the scrutinee
  824 from the family to the representation type.  This is achieved by
  825 unwrapFamInstScrutinee using a CoPat around the result pattern.
  826 
  827 Now it might appear seem as if we could have used the previous GADT type
  828 refinement infrastructure of refineAlt and friends instead of the explicit
  829 unification and CoPat generation.  However, that would be wrong.  Why?  The
  830 whole point of GADT refinement is that the refinement is local to the case
  831 alternative.  In contrast, the substitution generated by the unification of
  832 the family type list and instance types needs to be propagated to the outside.
  833 Imagine that in the above example, the type of the scrutinee would have been
  834 (Map x w), then we would have unified {x, w} with {(a, b), v}, yielding the
  835 substitution [x -> (a, b), v -> w].  In contrast to GADT matching, the
  836 instantiation of x with (a, b) must be global; ie, it must be valid in *all*
  837 alternatives of the case expression, whereas in the GADT case it might vary
  838 between alternatives.
  839 
  840 RIP GADT refinement: refinements have been replaced by the use of explicit
  841 equality constraints that are used in conjunction with implication constraints
  842 to express the local scope of GADT refinements.
  843 
  844 Note [Freshen existentials]
  845 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
  846 It is essential that these existentials are freshened.
  847 Otherwise, if we have something like
  848   case (a :: Ex, b :: Ex) of (MkEx ..., MkEx ...) -> ...
  849 we'll give both unpacked existential variables the
  850 same name, leading to shadowing.
  851 
  852 -}
  853 
  854 --      Running example:
  855 -- MkT :: forall a b c. (a~[b]) => b -> c -> T a
  856 --       with scrutinee of type (T ty)
  857 
  858 tcConPat :: PatEnv -> LocatedN Name
  859          -> Scaled ExpSigmaType    -- Type of the pattern
  860          -> HsConPatDetails GhcRn -> TcM a
  861          -> TcM (Pat GhcTc, a)
  862 tcConPat penv con_lname@(L _ con_name) pat_ty arg_pats thing_inside
  863   = do  { con_like <- tcLookupConLike con_name
  864         ; case con_like of
  865             RealDataCon data_con -> tcDataConPat penv con_lname data_con
  866                                                  pat_ty arg_pats thing_inside
  867             PatSynCon pat_syn -> tcPatSynPat penv con_lname pat_syn
  868                                              pat_ty arg_pats thing_inside
  869         }
  870 
  871 tcDataConPat :: PatEnv -> LocatedN Name -> DataCon
  872              -> Scaled ExpSigmaType        -- Type of the pattern
  873              -> HsConPatDetails GhcRn -> TcM a
  874              -> TcM (Pat GhcTc, a)
  875 tcDataConPat penv (L con_span con_name) data_con pat_ty_scaled
  876              arg_pats thing_inside
  877   = do  { let tycon = dataConTyCon data_con
  878                   -- For data families this is the representation tycon
  879               (univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _)
  880                 = dataConFullSig data_con
  881               header = L con_span (RealDataCon data_con)
  882 
  883           -- Instantiate the constructor type variables [a->ty]
  884           -- This may involve doing a family-instance coercion,
  885           -- and building a wrapper
  886         ; (wrap, ctxt_res_tys) <- matchExpectedConTy penv tycon pat_ty_scaled
  887         ; pat_ty <- readExpType (scaledThing pat_ty_scaled)
  888 
  889           -- Add the stupid theta
  890         ; setSrcSpanA con_span $ addDataConStupidTheta data_con ctxt_res_tys
  891 
  892         -- Check that this isn't a GADT pattern match
  893         -- in situations in which that isn't allowed.
  894         ; let all_arg_tys = eqSpecPreds eq_spec ++ theta ++ (map scaledThing arg_tys)
  895         ; checkGADT (RealDataCon data_con) ex_tvs all_arg_tys penv
  896 
  897         ; tenv1 <- instTyVarsWith PatOrigin univ_tvs ctxt_res_tys
  898                   -- NB: Do not use zipTvSubst!  See #14154
  899                   -- We want to create a well-kinded substitution, so
  900                   -- that the instantiated type is well-kinded
  901 
  902         ; (tenv, ex_tvs') <- tcInstSuperSkolTyVarsX tenv1 ex_tvs
  903                      -- Get location from monad, not from ex_tvs
  904                      -- This freshens: See Note [Freshen existentials]
  905                      -- Why "super"? See Note [Binding when lookup up instances]
  906                      -- in GHC.Core.InstEnv.
  907 
  908         ; let arg_tys' = substScaledTys tenv arg_tys
  909               pat_mult = scaledMult pat_ty_scaled
  910               arg_tys_scaled = map (scaleScaled pat_mult) arg_tys'
  911 
  912         ; traceTc "tcConPat" (vcat [ ppr con_name
  913                                    , pprTyVars univ_tvs
  914                                    , pprTyVars ex_tvs
  915                                    , ppr eq_spec
  916                                    , ppr theta
  917                                    , pprTyVars ex_tvs'
  918                                    , ppr ctxt_res_tys
  919                                    , ppr arg_tys'
  920                                    , ppr arg_pats ])
  921         ; if null ex_tvs && null eq_spec && null theta
  922           then do { -- The common case; no class bindings etc
  923                     -- (see Note [Arrows and patterns])
  924                     (arg_pats', res) <- tcConArgs (RealDataCon data_con) arg_tys_scaled
  925                                                   tenv penv arg_pats thing_inside
  926                   ; let res_pat = ConPat { pat_con = header
  927                                          , pat_args = arg_pats'
  928                                          , pat_con_ext = ConPatTc
  929                                            { cpt_tvs = [], cpt_dicts = []
  930                                            , cpt_binds = emptyTcEvBinds
  931                                            , cpt_arg_tys = ctxt_res_tys
  932                                            , cpt_wrap = idHsWrapper
  933                                            }
  934                                          }
  935 
  936                   ; return (mkHsWrapPat wrap res_pat pat_ty, res) }
  937 
  938           else do   -- The general case, with existential,
  939                     -- and local equality constraints
  940         { let theta'     = substTheta tenv (eqSpecPreds eq_spec ++ theta)
  941                            -- order is *important* as we generate the list of
  942                            -- dictionary binders from theta'
  943               no_equalities = null eq_spec && not (any isEqPred theta)
  944               skol_info = PatSkol (RealDataCon data_con) mc
  945               mc = case pe_ctxt penv of
  946                      LamPat mc -> mc
  947                      LetPat {} -> PatBindRhs
  948 
  949         ; gadts_on    <- xoptM LangExt.GADTs
  950         ; families_on <- xoptM LangExt.TypeFamilies
  951         ; checkTc (no_equalities || gadts_on || families_on)
  952                   (TcRnUnknownMessage $ mkPlainError noHints $
  953                    text "A pattern match on a GADT requires the" <+>
  954                    text "GADTs or TypeFamilies language extension")
  955                   -- #2905 decided that a *pattern-match* of a GADT
  956                   -- should require the GADT language flag.
  957                   -- Re TypeFamilies see also #7156
  958 
  959         ; given <- newEvVars theta'
  960         ; (ev_binds, (arg_pats', res))
  961              <- checkConstraints skol_info ex_tvs' given $
  962                 tcConArgs (RealDataCon data_con) arg_tys_scaled tenv penv arg_pats thing_inside
  963 
  964         ; let res_pat = ConPat
  965                 { pat_con   = header
  966                 , pat_args  = arg_pats'
  967                 , pat_con_ext = ConPatTc
  968                   { cpt_tvs   = ex_tvs'
  969                   , cpt_dicts = given
  970                   , cpt_binds = ev_binds
  971                   , cpt_arg_tys = ctxt_res_tys
  972                   , cpt_wrap  = idHsWrapper
  973                   }
  974                 }
  975         ; return (mkHsWrapPat wrap res_pat pat_ty, res)
  976         } }
  977 
  978 tcPatSynPat :: PatEnv -> LocatedN Name -> PatSyn
  979             -> Scaled ExpSigmaType         -- Type of the pattern
  980             -> HsConPatDetails GhcRn -> TcM a
  981             -> TcM (Pat GhcTc, a)
  982 tcPatSynPat penv (L con_span con_name) pat_syn pat_ty arg_pats thing_inside
  983   = do  { let (univ_tvs, req_theta, ex_tvs, prov_theta, arg_tys, ty) = patSynSig pat_syn
  984 
  985         ; (subst, univ_tvs') <- newMetaTyVars univ_tvs
  986 
  987         -- Check that we aren't matching on a GADT-like pattern synonym
  988         -- in situations in which that isn't allowed.
  989         ; let all_arg_tys = ty : prov_theta ++ (map scaledThing arg_tys)
  990         ; checkGADT (PatSynCon pat_syn) ex_tvs all_arg_tys penv
  991 
  992         ; (tenv, ex_tvs') <- tcInstSuperSkolTyVarsX subst ex_tvs
  993            -- This freshens: Note [Freshen existentials]
  994 
  995         ; let ty'         = substTy tenv ty
  996               arg_tys'    = substScaledTys tenv arg_tys
  997               pat_mult    = scaledMult pat_ty
  998               arg_tys_scaled = map (scaleScaled pat_mult) arg_tys'
  999               prov_theta' = substTheta tenv prov_theta
 1000               req_theta'  = substTheta tenv req_theta
 1001 
 1002         ; mult_wrap <- checkManyPattern pat_ty
 1003             -- See Note [Wrapper returned from tcSubMult] in GHC.Tc.Utils.Unify.
 1004 
 1005         ; wrap <- tc_sub_type penv (scaledThing pat_ty) ty'
 1006         ; traceTc "tcPatSynPat" (ppr pat_syn $$
 1007                                  ppr pat_ty $$
 1008                                  ppr ty' $$
 1009                                  ppr ex_tvs' $$
 1010                                  ppr prov_theta' $$
 1011                                  ppr req_theta' $$
 1012                                  ppr arg_tys')
 1013 
 1014         ; prov_dicts' <- newEvVars prov_theta'
 1015 
 1016         ; let skol_info = case pe_ctxt penv of
 1017                             LamPat mc -> PatSkol (PatSynCon pat_syn) mc
 1018                             LetPat {} -> UnkSkol -- Doesn't matter
 1019 
 1020         ; req_wrap <- instCall (OccurrenceOf con_name) (mkTyVarTys univ_tvs') req_theta'
 1021                       -- Origin (OccurrenceOf con_name):
 1022                       -- see Note [Call-stack tracing of pattern synonyms]
 1023         ; traceTc "instCall" (ppr req_wrap)
 1024 
 1025         ; traceTc "checkConstraints {" Outputable.empty
 1026         ; (ev_binds, (arg_pats', res))
 1027              <- checkConstraints skol_info ex_tvs' prov_dicts' $
 1028                 tcConArgs (PatSynCon pat_syn) arg_tys_scaled tenv penv arg_pats thing_inside
 1029 
 1030         ; traceTc "checkConstraints }" (ppr ev_binds)
 1031         ; let res_pat = ConPat { pat_con   = L con_span $ PatSynCon pat_syn
 1032                                , pat_args  = arg_pats'
 1033                                , pat_con_ext = ConPatTc
 1034                                  { cpt_tvs   = ex_tvs'
 1035                                  , cpt_dicts = prov_dicts'
 1036                                  , cpt_binds = ev_binds
 1037                                  , cpt_arg_tys = mkTyVarTys univ_tvs'
 1038                                  , cpt_wrap  = req_wrap
 1039                                  }
 1040                                }
 1041         ; pat_ty <- readExpType (scaledThing pat_ty)
 1042         ; return (mkHsWrapPat (wrap <.> mult_wrap) res_pat pat_ty, res) }
 1043 
 1044 {- Note [Call-stack tracing of pattern synonyms]
 1045 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1046 Consider
 1047    f :: HasCallStack => blah
 1048 
 1049    pattern Annotated :: HasCallStack => (CallStack, a) -> a
 1050    pattern Annotated x <- (f -> x)
 1051 
 1052 When we pattern-match against `Annotated` we will call `f`, and must
 1053 pass a call-stack.  We may want `Annotated` itself to propagate the call
 1054 stack, so we give it a HasCallStack constraint too.  But then we expect
 1055 to see `Annotated` in the call stack.
 1056 
 1057 This is achieve easily, but a bit trickily.  When we instantiate
 1058 Annotated's "required" constraints, in tcPatSynPat, give them a
 1059 CtOrigin of (OccurrenceOf "Annotated"). That way the special magic
 1060 in GHC.Tc.Solver.Canonical.canClassNC which deals with CallStack
 1061 constraints will kick in: that logic only fires on constraints
 1062 whose Origin is (OccurrenceOf f).
 1063 
 1064 See also Note [Overview of implicit CallStacks] in GHC.Tc.Types.Evidence
 1065 and Note [Solving CallStack constraints] in GHC.Tc.Solver.Types
 1066 -}
 1067 ----------------------------
 1068 -- | Convenient wrapper for calling a matchExpectedXXX function
 1069 matchExpectedPatTy :: (TcRhoType -> TcM (TcCoercionN, a))
 1070                     -> PatEnv -> ExpSigmaType -> TcM (HsWrapper, a)
 1071 -- See Note [Matching polytyped patterns]
 1072 -- Returns a wrapper : pat_ty ~R inner_ty
 1073 matchExpectedPatTy inner_match (PE { pe_orig = orig }) pat_ty
 1074   = do { pat_ty <- expTypeToType pat_ty
 1075        ; (wrap, pat_rho) <- topInstantiate orig pat_ty
 1076        ; (co, res) <- inner_match pat_rho
 1077        ; traceTc "matchExpectedPatTy" (ppr pat_ty $$ ppr wrap)
 1078        ; return (mkWpCastN (mkTcSymCo co) <.> wrap, res) }
 1079 
 1080 ----------------------------
 1081 matchExpectedConTy :: PatEnv
 1082                    -> TyCon      -- The TyCon that this data
 1083                                  -- constructor actually returns
 1084                                  -- In the case of a data family this is
 1085                                  -- the /representation/ TyCon
 1086                    -> Scaled ExpSigmaType  -- The type of the pattern; in the
 1087                                            -- case of a data family this would
 1088                                            -- mention the /family/ TyCon
 1089                    -> TcM (HsWrapper, [TcSigmaType])
 1090 -- See Note [Matching constructor patterns]
 1091 -- Returns a wrapper : pat_ty "->" T ty1 ... tyn
 1092 matchExpectedConTy (PE { pe_orig = orig }) data_tc exp_pat_ty
 1093   | Just (fam_tc, fam_args, co_tc) <- tyConFamInstSig_maybe data_tc
 1094          -- Comments refer to Note [Matching constructor patterns]
 1095          -- co_tc :: forall a. T [a] ~ T7 a
 1096   = do { pat_ty <- expTypeToType (scaledThing exp_pat_ty)
 1097        ; (wrap, pat_rho) <- topInstantiate orig pat_ty
 1098 
 1099        ; (subst, tvs') <- newMetaTyVars (tyConTyVars data_tc)
 1100              -- tys = [ty1,ty2]
 1101 
 1102        ; traceTc "matchExpectedConTy" (vcat [ppr data_tc,
 1103                                              ppr (tyConTyVars data_tc),
 1104                                              ppr fam_tc, ppr fam_args,
 1105                                              ppr exp_pat_ty,
 1106                                              ppr pat_ty,
 1107                                              ppr pat_rho, ppr wrap])
 1108        ; co1 <- unifyType Nothing (mkTyConApp fam_tc (substTys subst fam_args)) pat_rho
 1109              -- co1 : T (ty1,ty2) ~N pat_rho
 1110              -- could use tcSubType here... but it's the wrong way round
 1111              -- for actual vs. expected in error messages.
 1112 
 1113        ; let tys' = mkTyVarTys tvs'
 1114              co2 = mkTcUnbranchedAxInstCo co_tc tys' []
 1115              -- co2 : T (ty1,ty2) ~R T7 ty1 ty2
 1116 
 1117              full_co = mkTcSubCo (mkTcSymCo co1) `mkTcTransCo` co2
 1118              -- full_co :: pat_rho ~R T7 ty1 ty2
 1119 
 1120        ; return ( mkWpCastR full_co <.> wrap, tys') }
 1121 
 1122   | otherwise
 1123   = do { pat_ty <- expTypeToType (scaledThing exp_pat_ty)
 1124        ; (wrap, pat_rho) <- topInstantiate orig pat_ty
 1125        ; (coi, tys) <- matchExpectedTyConApp data_tc pat_rho
 1126        ; return (mkWpCastN (mkTcSymCo coi) <.> wrap, tys) }
 1127 
 1128 {-
 1129 Note [Matching constructor patterns]
 1130 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1131 Suppose (coi, tys) = matchExpectedConType data_tc pat_ty
 1132 
 1133  * In the simple case, pat_ty = tc tys
 1134 
 1135  * If pat_ty is a polytype, we want to instantiate it
 1136    This is like part of a subsumption check.  Eg
 1137       f :: (forall a. [a]) -> blah
 1138       f [] = blah
 1139 
 1140  * In a type family case, suppose we have
 1141           data family T a
 1142           data instance T (p,q) = A p | B q
 1143        Then we'll have internally generated
 1144               data T7 p q = A p | B q
 1145               axiom coT7 p q :: T (p,q) ~ T7 p q
 1146 
 1147        So if pat_ty = T (ty1,ty2), we return (coi, [ty1,ty2]) such that
 1148            coi = coi2 . coi1 : T7 t ~ pat_ty
 1149            coi1 : T (ty1,ty2) ~ pat_ty
 1150            coi2 : T7 ty1 ty2 ~ T (ty1,ty2)
 1151 
 1152    For families we do all this matching here, not in the unifier,
 1153    because we never want a whisper of the data_tycon to appear in
 1154    error messages; it's a purely internal thing
 1155 -}
 1156 
 1157 {-
 1158 Note [Typechecking type applications in patterns]
 1159 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1160 How should we typecheck type applications in patterns, such as
 1161    f :: Either (Maybe a) [b] -> blah
 1162    f (Left @x @[y] (v::Maybe x)) = blah
 1163 
 1164 It's quite straightforward, and very similar to the treatment of
 1165 pattern signatures.
 1166 
 1167 * Step 1: bind the newly-in-scope type variables x and y to fresh
 1168   unification variables, say x0 and y0.
 1169 
 1170 * Step 2: typecheck those type arguments, @x and @[y], to get the
 1171   types x0 and [y0].
 1172 
 1173 * Step 3: Unify those types with the type arguments we expect,
 1174   in this case (Maybe a) and [b].  These unifications will
 1175   (perhaps after the constraint solver has done its work)
 1176   unify   x0 := Maybe a
 1177           y0 := b
 1178   Thus we learn that x stands for (Maybe a) and y for b.
 1179 
 1180 Wrinkles:
 1181 
 1182 * Surprisingly, we can discard the coercions arising from
 1183   these unifications.  The *only* thing the unification does is
 1184   to side-effect those unification variables, so that we know
 1185   what type x and y stand for; and cause an error if the equality
 1186   is not soluble.  It's a bit like a Derived constraint arising
 1187   from a functional dependency.
 1188 
 1189 * Exactly the same works for existential arguments
 1190      data T where
 1191         MkT :: a -> a -> T
 1192      f :: T -> blah
 1193      f (MkT @x v w) = ...
 1194    Here we create a fresh unification variable x0 for x, and
 1195    unify it with the fresh existential variable bound by the pattern.
 1196 
 1197 * Note that both here and in pattern signatures the unification may
 1198   not even end up unifying the variable.  For example
 1199      type S a b = a
 1200      f :: Maybe a -> Bool
 1201      f (Just @(S a b) x) = True :: b
 1202    In Step 3 we will unify (S a0 b0 ~ a), which succeeds, but has no
 1203    effect on the unification variable b0, to which 'b' is bound.
 1204    Later, in the RHS, we find that b0 must be Bool, and unify it there.
 1205    All is fine.
 1206 -}
 1207 
 1208 tcConArgs :: ConLike
 1209           -> [Scaled TcSigmaType]
 1210           -> TCvSubst            -- Instantiating substitution for constructor type
 1211           -> Checker (HsConPatDetails GhcRn) (HsConPatDetails GhcTc)
 1212 tcConArgs con_like arg_tys tenv penv con_args thing_inside = case con_args of
 1213   PrefixCon type_args arg_pats -> do
 1214         { checkTc (con_arity == no_of_args)     -- Check correct arity
 1215                   (arityErr (text "constructor") con_like con_arity no_of_args)
 1216 
 1217               -- forgetting to filter out inferred binders led to #20443
 1218         ; let con_spec_binders = filter ((== SpecifiedSpec) . binderArgFlag) $
 1219                                  conLikeUserTyVarBinders con_like
 1220         ; checkTc (type_args `leLength` con_spec_binders)
 1221                   (conTyArgArityErr con_like (length con_spec_binders) (length type_args))
 1222 
 1223         ; let pats_w_tys = zipEqual "tcConArgs" arg_pats arg_tys
 1224         ; (type_args', (arg_pats', res))
 1225             <- tcMultiple tcConTyArg penv type_args $
 1226                tcMultiple tcConArg penv pats_w_tys thing_inside
 1227 
 1228           -- This unification is straight from Figure 7 of
 1229           -- "Type Variables in Patterns", Haskell'18
 1230         ; _ <- zipWithM (unifyType Nothing) type_args' (substTyVars tenv $
 1231                                                         binderVars con_spec_binders)
 1232           -- OK to drop coercions here. These unifications are all about
 1233           -- guiding inference based on a user-written type annotation
 1234           -- See Note [Typechecking type applications in patterns]
 1235 
 1236         ; return (PrefixCon type_args arg_pats', res) }
 1237     where
 1238       con_arity  = conLikeArity con_like
 1239       no_of_args = length arg_pats
 1240 
 1241   InfixCon p1 p2 -> do
 1242         { checkTc (con_arity == 2)      -- Check correct arity
 1243                   (arityErr (text "constructor") con_like con_arity 2)
 1244         ; let [arg_ty1,arg_ty2] = arg_tys       -- This can't fail after the arity check
 1245         ; ([p1',p2'], res) <- tcMultiple tcConArg penv [(p1,arg_ty1),(p2,arg_ty2)]
 1246                                                   thing_inside
 1247         ; return (InfixCon p1' p2', res) }
 1248     where
 1249       con_arity  = conLikeArity con_like
 1250 
 1251   RecCon (HsRecFields rpats dd) -> do
 1252         { (rpats', res) <- tcMultiple tc_field penv rpats thing_inside
 1253         ; return (RecCon (HsRecFields rpats' dd), res) }
 1254     where
 1255       tc_field :: Checker (LHsRecField GhcRn (LPat GhcRn))
 1256                           (LHsRecField GhcTc (LPat GhcTc))
 1257       tc_field penv
 1258                (L l (HsFieldBind ann (L loc (FieldOcc sel (L lr rdr))) pat pun))
 1259                thing_inside
 1260         = do { sel'   <- tcLookupId sel
 1261              ; pat_ty <- setSrcSpanA loc $ find_field_ty sel
 1262                                             (occNameFS $ rdrNameOcc rdr)
 1263              ; (pat', res) <- tcConArg penv (pat, pat_ty) thing_inside
 1264              ; return (L l (HsFieldBind ann (L loc (FieldOcc sel' (L lr rdr))) pat'
 1265                                                                         pun), res) }
 1266 
 1267 
 1268       find_field_ty :: Name -> FieldLabelString -> TcM (Scaled TcType)
 1269       find_field_ty sel lbl
 1270         = case [ty | (fl, ty) <- field_tys, flSelector fl == sel ] of
 1271 
 1272                 -- No matching field; chances are this field label comes from some
 1273                 -- other record type (or maybe none).  If this happens, just fail,
 1274                 -- otherwise we get crashes later (#8570), and similar:
 1275                 --      f (R { foo = (a,b) }) = a+b
 1276                 -- If foo isn't one of R's fields, we don't want to crash when
 1277                 -- typechecking the "a+b".
 1278            [] -> failWith (badFieldCon con_like lbl)
 1279 
 1280                 -- The normal case, when the field comes from the right constructor
 1281            (pat_ty : extras) -> do
 1282                 traceTc "find_field" (ppr pat_ty <+> ppr extras)
 1283                 assert (null extras) (return pat_ty)
 1284 
 1285       field_tys :: [(FieldLabel, Scaled TcType)]
 1286       field_tys = zip (conLikeFieldLabels con_like) arg_tys
 1287           -- Don't use zipEqual! If the constructor isn't really a record, then
 1288           -- dataConFieldLabels will be empty (and each field in the pattern
 1289           -- will generate an error below).
 1290 
 1291 tcConTyArg :: Checker (HsPatSigType GhcRn) TcType
 1292 tcConTyArg penv rn_ty thing_inside
 1293   = do { (sig_wcs, sig_ibs, arg_ty) <- tcHsPatSigType TypeAppCtxt HM_TyAppPat rn_ty AnyKind
 1294                -- AnyKind is a bit suspect: it really should be the kind gotten
 1295                -- from instantiating the constructor type. But this would be
 1296                -- hard to get right, because earlier type patterns might influence
 1297                -- the kinds of later patterns. In any case, it all gets checked
 1298                -- by the calls to unifyType in tcConArgs, which will also unify
 1299                -- kinds.
 1300        ; when (not (null sig_ibs) && inPatBind penv) $
 1301            addErr (TcRnUnknownMessage $ mkPlainError noHints $
 1302                      text "Binding type variables is not allowed in pattern bindings")
 1303        ; result <- tcExtendNameTyVarEnv sig_wcs $
 1304                    tcExtendNameTyVarEnv sig_ibs $
 1305                    thing_inside
 1306        ; return (arg_ty, result) }
 1307 
 1308 tcConArg :: Checker (LPat GhcRn, Scaled TcSigmaType) (LPat GhcTc)
 1309 tcConArg penv (arg_pat, Scaled arg_mult arg_ty)
 1310   = tc_lpat (Scaled arg_mult (mkCheckExpType arg_ty)) penv arg_pat
 1311 
 1312 addDataConStupidTheta :: DataCon -> [TcType] -> TcM ()
 1313 -- Instantiate the "stupid theta" of the data con, and throw
 1314 -- the constraints into the constraint set
 1315 addDataConStupidTheta data_con inst_tys
 1316   | null stupid_theta = return ()
 1317   | otherwise         = instStupidTheta origin inst_theta
 1318   where
 1319     origin = OccurrenceOf (dataConName data_con)
 1320         -- The origin should always report "occurrence of C"
 1321         -- even when C occurs in a pattern
 1322     stupid_theta = dataConStupidTheta data_con
 1323     univ_tvs     = dataConUnivTyVars data_con
 1324     tenv = zipTvSubst univ_tvs (takeList univ_tvs inst_tys)
 1325          -- NB: inst_tys can be longer than the univ tyvars
 1326          --     because the constructor might have existentials
 1327     inst_theta = substTheta tenv stupid_theta
 1328 
 1329 conTyArgArityErr :: ConLike
 1330                  -> Int   -- expected # of arguments
 1331                  -> Int   -- actual # of arguments
 1332                  -> TcRnMessage
 1333 conTyArgArityErr con_like expected_number actual_number
 1334   = TcRnUnknownMessage $ mkPlainError noHints $
 1335     text "Too many type arguments in constructor pattern for" <+> quotes (ppr con_like) $$
 1336     text "Expected no more than" <+> ppr expected_number <> semi <+> text "got" <+> ppr actual_number
 1337 
 1338 {-
 1339 Note [Arrows and patterns]
 1340 ~~~~~~~~~~~~~~~~~~~~~~~~~~
 1341 (Oct 07) Arrow notation has the odd property that it involves
 1342 "holes in the scope". For example:
 1343   expr :: Arrow a => a () Int
 1344   expr = proc (y,z) -> do
 1345           x <- term -< y
 1346           expr' -< x
 1347 
 1348 Here the 'proc (y,z)' binding scopes over the arrow tails but not the
 1349 arrow body (e.g 'term').  As things stand (bogusly) all the
 1350 constraints from the proc body are gathered together, so constraints
 1351 from 'term' will be seen by the tcPat for (y,z).  But we must *not*
 1352 bind constraints from 'term' here, because the desugarer will not make
 1353 these bindings scope over 'term'.
 1354 
 1355 The Right Thing is not to confuse these constraints together. But for
 1356 now the Easy Thing is to ensure that we do not have existential or
 1357 GADT constraints in a 'proc', which we do by disallowing any
 1358 non-vanilla pattern match (i.e. one that introduces existential
 1359 variables or provided constraints), in tcDataConPat and tcPatSynPat.
 1360 
 1361 We also short-cut the constraint simplification for such vanilla patterns,
 1362 so that we bind no constraints. Hence the 'fast path' in tcDataConPat;
 1363 which applies more generally (not just within 'proc'), as it's a good
 1364 plan in general to bypass the constraint simplification step entirely
 1365 when it's not needed.
 1366 
 1367 ************************************************************************
 1368 *                                                                      *
 1369                 Note [Pattern coercions]
 1370 *                                                                      *
 1371 ************************************************************************
 1372 
 1373 In principle, these program would be reasonable:
 1374 
 1375         f :: (forall a. a->a) -> Int
 1376         f (x :: Int->Int) = x 3
 1377 
 1378         g :: (forall a. [a]) -> Bool
 1379         g [] = True
 1380 
 1381 In both cases, the function type signature restricts what arguments can be passed
 1382 in a call (to polymorphic ones).  The pattern type signature then instantiates this
 1383 type.  For example, in the first case,  (forall a. a->a) <= Int -> Int, and we
 1384 generate the translated term
 1385         f = \x' :: (forall a. a->a).  let x = x' Int in x 3
 1386 
 1387 From a type-system point of view, this is perfectly fine, but it's *very* seldom useful.
 1388 And it requires a significant amount of code to implement, because we need to decorate
 1389 the translated pattern with coercion functions (generated from the subsumption check
 1390 by tcSub).
 1391 
 1392 So for now I'm just insisting on type *equality* in patterns.  No subsumption.
 1393 
 1394 Old notes about desugaring, at a time when pattern coercions were handled:
 1395 
 1396 A SigPat is a type coercion and must be handled one at a time.  We can't
 1397 combine them unless the type of the pattern inside is identical, and we don't
 1398 bother to check for that.  For example:
 1399 
 1400         data T = T1 Int | T2 Bool
 1401         f :: (forall a. a -> a) -> T -> t
 1402         f (g::Int->Int)   (T1 i) = T1 (g i)
 1403         f (g::Bool->Bool) (T2 b) = T2 (g b)
 1404 
 1405 We desugar this as follows:
 1406 
 1407         f = \ g::(forall a. a->a) t::T ->
 1408             let gi = g Int
 1409             in case t of { T1 i -> T1 (gi i)
 1410                            other ->
 1411             let gb = g Bool
 1412             in case t of { T2 b -> T2 (gb b)
 1413                            other -> fail }}
 1414 
 1415 Note that we do not treat the first column of patterns as a
 1416 column of variables, because the coerced variables (gi, gb)
 1417 would be of different types.  So we get rather grotty code.
 1418 But I don't think this is a common case, and if it was we could
 1419 doubtless improve it.
 1420 
 1421 Meanwhile, the strategy is:
 1422         * treat each SigPat coercion (always non-identity coercions)
 1423                 as a separate block
 1424         * deal with the stuff inside, and then wrap a binding round
 1425                 the result to bind the new variable (gi, gb, etc)
 1426 
 1427 
 1428 ************************************************************************
 1429 *                                                                      *
 1430 \subsection{Errors and contexts}
 1431 *                                                                      *
 1432 ************************************************************************
 1433 
 1434 Note [Existential check]
 1435 ~~~~~~~~~~~~~~~~~~~~~~~~
 1436 Lazy patterns can't bind existentials.  They arise in two ways:
 1437   * Let bindings      let { C a b = e } in b
 1438   * Twiddle patterns  f ~(C a b) = e
 1439 The pe_lazy field of PatEnv says whether we are inside a lazy
 1440 pattern (perhaps deeply)
 1441 
 1442 See also Note [Typechecking pattern bindings] in GHC.Tc.Gen.Bind
 1443 -}
 1444 
 1445 maybeWrapPatCtxt :: Pat GhcRn -> (TcM a -> TcM b) -> TcM a -> TcM b
 1446 -- Not all patterns are worth pushing a context
 1447 maybeWrapPatCtxt pat tcm thing_inside
 1448   | not (worth_wrapping pat) = tcm thing_inside
 1449   | otherwise                = addErrCtxt msg $ tcm $ popErrCtxt thing_inside
 1450                                -- Remember to pop before doing thing_inside
 1451   where
 1452    worth_wrapping (VarPat {}) = False
 1453    worth_wrapping (ParPat {}) = False
 1454    worth_wrapping (AsPat {})  = False
 1455    worth_wrapping _           = True
 1456    msg = hang (text "In the pattern:") 2 (ppr pat)
 1457 
 1458 -----------------------------------------------
 1459 
 1460 -- | Check that a pattern isn't a GADT, or doesn't have existential variables,
 1461 -- in a situation in which that is not permitted (inside a lazy pattern, or
 1462 -- in arrow notation).
 1463 checkGADT :: ConLike
 1464           -> [TyVar] -- ^ existentials
 1465           -> [Type]  -- ^ argument types
 1466           -> PatEnv
 1467           -> TcM ()
 1468 checkGADT conlike ex_tvs arg_tys = \case
 1469   PE { pe_ctxt = LetPat {} }
 1470     -> return ()
 1471   PE { pe_ctxt = LamPat (ArrowMatchCtxt {}) }
 1472     | not $ isVanillaConLike conlike
 1473     -- See Note [Arrows and patterns]
 1474     -> failWithTc TcRnArrowProcGADTPattern
 1475   PE { pe_lazy = True }
 1476     | has_existentials
 1477     -- See Note [Existential check]
 1478     -> failWithTc TcRnLazyGADTPattern
 1479   _ -> return ()
 1480   where
 1481     has_existentials :: Bool
 1482     has_existentials = any (`elemVarSet` tyCoVarsOfTypes arg_tys) ex_tvs
 1483 
 1484 badFieldCon :: ConLike -> FieldLabelString -> TcRnMessage
 1485 badFieldCon con field
 1486   = TcRnUnknownMessage $ mkPlainError noHints $
 1487     hsep [text "Constructor" <+> quotes (ppr con),
 1488           text "does not have field", quotes (ppr field)]
 1489 
 1490 polyPatSig :: TcType -> SDoc
 1491 polyPatSig sig_ty
 1492   = hang (text "Illegal polymorphic type signature in pattern:")
 1493        2 (ppr sig_ty)