summaryrefslogtreecommitdiff
path: root/compiler/GHC/Tc/Gen/Pat.hs
diff options
context:
space:
mode:
Diffstat (limited to 'compiler/GHC/Tc/Gen/Pat.hs')
-rw-r--r--compiler/GHC/Tc/Gen/Pat.hs1214
1 files changed, 1214 insertions, 0 deletions
diff --git a/compiler/GHC/Tc/Gen/Pat.hs b/compiler/GHC/Tc/Gen/Pat.hs
new file mode 100644
index 0000000000..0fa2b74c14
--- /dev/null
+++ b/compiler/GHC/Tc/Gen/Pat.hs
@@ -0,0 +1,1214 @@
+{-
+(c) The University of Glasgow 2006
+(c) The GRASP/AQUA Project, Glasgow University, 1992-1998
+
+-}
+
+{-# LANGUAGE CPP, RankNTypes, TupleSections #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE ViewPatterns #-}
+
+{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
+
+-- | Typechecking patterns
+module GHC.Tc.Gen.Pat
+ ( tcLetPat
+ , newLetBndr
+ , LetBndrSpec(..)
+ , tcPat
+ , tcPat_O
+ , tcPats
+ , addDataConStupidTheta
+ , badFieldCon
+ , polyPatSig
+ )
+where
+
+#include "HsVersions.h"
+
+import GhcPrelude
+
+import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcSyntaxOp, tcSyntaxOpGen, tcInferSigma )
+
+import GHC.Hs
+import GHC.Tc.Utils.Zonk
+import GHC.Tc.Gen.Sig( TcPragEnv, lookupPragEnv, addInlinePrags )
+import GHC.Tc.Utils.Monad
+import GHC.Tc.Utils.Instantiate
+import GHC.Types.Id
+import GHC.Types.Var
+import GHC.Types.Name
+import GHC.Types.Name.Reader
+import GHC.Tc.Utils.Env
+import GHC.Tc.Utils.TcMType
+import GHC.Tc.Validity( arityErr )
+import GHC.Core.TyCo.Ppr ( pprTyVars )
+import GHC.Tc.Utils.TcType
+import GHC.Tc.Utils.Unify
+import GHC.Tc.Gen.HsType
+import TysWiredIn
+import GHC.Tc.Types.Evidence
+import GHC.Tc.Types.Origin
+import GHC.Core.TyCon
+import GHC.Core.DataCon
+import GHC.Core.PatSyn
+import GHC.Core.ConLike
+import PrelNames
+import GHC.Types.Basic hiding (SuccessFlag(..))
+import GHC.Driver.Session
+import GHC.Types.SrcLoc
+import GHC.Types.Var.Set
+import Util
+import Outputable
+import qualified GHC.LanguageExtensions as LangExt
+import Control.Arrow ( second )
+import ListSetOps ( getNth )
+
+{-
+************************************************************************
+* *
+ External interface
+* *
+************************************************************************
+-}
+
+tcLetPat :: (Name -> Maybe TcId)
+ -> LetBndrSpec
+ -> LPat GhcRn -> ExpSigmaType
+ -> TcM a
+ -> TcM (LPat GhcTcId, a)
+tcLetPat sig_fn no_gen pat pat_ty thing_inside
+ = do { bind_lvl <- getTcLevel
+ ; let ctxt = LetPat { pc_lvl = bind_lvl
+ , pc_sig_fn = sig_fn
+ , pc_new = no_gen }
+ penv = PE { pe_lazy = True
+ , pe_ctxt = ctxt
+ , pe_orig = PatOrigin }
+
+ ; tc_lpat pat pat_ty penv thing_inside }
+
+-----------------
+tcPats :: HsMatchContext GhcRn
+ -> [LPat GhcRn] -- Patterns,
+ -> [ExpSigmaType] -- and their types
+ -> TcM a -- and the checker for the body
+ -> TcM ([LPat GhcTcId], a)
+
+-- This is the externally-callable wrapper function
+-- Typecheck the patterns, extend the environment to bind the variables,
+-- do the thing inside, use any existentially-bound dictionaries to
+-- discharge parts of the returning LIE, and deal with pattern type
+-- signatures
+
+-- 1. Initialise the PatState
+-- 2. Check the patterns
+-- 3. Check the body
+-- 4. Check that no existentials escape
+
+tcPats ctxt pats pat_tys thing_inside
+ = tc_lpats penv pats pat_tys thing_inside
+ where
+ penv = PE { pe_lazy = False, pe_ctxt = LamPat ctxt, pe_orig = PatOrigin }
+
+tcPat :: HsMatchContext GhcRn
+ -> LPat GhcRn -> ExpSigmaType
+ -> TcM a -- Checker for body
+ -> TcM (LPat GhcTcId, a)
+tcPat ctxt = tcPat_O ctxt PatOrigin
+
+-- | A variant of 'tcPat' that takes a custom origin
+tcPat_O :: HsMatchContext GhcRn
+ -> CtOrigin -- ^ origin to use if the type needs inst'ing
+ -> LPat GhcRn -> ExpSigmaType
+ -> TcM a -- Checker for body
+ -> TcM (LPat GhcTcId, a)
+tcPat_O ctxt orig pat pat_ty thing_inside
+ = tc_lpat pat pat_ty penv thing_inside
+ where
+ penv = PE { pe_lazy = False, pe_ctxt = LamPat ctxt, pe_orig = orig }
+
+
+{-
+************************************************************************
+* *
+ PatEnv, PatCtxt, LetBndrSpec
+* *
+************************************************************************
+-}
+
+data PatEnv
+ = PE { pe_lazy :: Bool -- True <=> lazy context, so no existentials allowed
+ , pe_ctxt :: PatCtxt -- Context in which the whole pattern appears
+ , pe_orig :: CtOrigin -- origin to use if the pat_ty needs inst'ing
+ }
+
+data PatCtxt
+ = LamPat -- Used for lambdas, case etc
+ (HsMatchContext GhcRn)
+
+ | LetPat -- Used only for let(rec) pattern bindings
+ -- See Note [Typing patterns in pattern bindings]
+ { pc_lvl :: TcLevel
+ -- Level of the binding group
+
+ , pc_sig_fn :: Name -> Maybe TcId
+ -- Tells the expected type
+ -- for binders with a signature
+
+ , pc_new :: LetBndrSpec
+ -- How to make a new binder
+ } -- for binders without signatures
+
+data LetBndrSpec
+ = LetLclBndr -- We are going to generalise, and wrap in an AbsBinds
+ -- so clone a fresh binder for the local monomorphic Id
+
+ | LetGblBndr TcPragEnv -- Generalisation plan is NoGen, so there isn't going
+ -- to be an AbsBinds; So we must bind the global version
+ -- of the binder right away.
+ -- And here is the inline-pragma information
+
+instance Outputable LetBndrSpec where
+ ppr LetLclBndr = text "LetLclBndr"
+ ppr (LetGblBndr {}) = text "LetGblBndr"
+
+makeLazy :: PatEnv -> PatEnv
+makeLazy penv = penv { pe_lazy = True }
+
+inPatBind :: PatEnv -> Bool
+inPatBind (PE { pe_ctxt = LetPat {} }) = True
+inPatBind (PE { pe_ctxt = LamPat {} }) = False
+
+{- *********************************************************************
+* *
+ Binders
+* *
+********************************************************************* -}
+
+tcPatBndr :: PatEnv -> Name -> ExpSigmaType -> TcM (HsWrapper, TcId)
+-- (coi, xp) = tcPatBndr penv x pat_ty
+-- Then coi : pat_ty ~ typeof(xp)
+--
+tcPatBndr penv@(PE { pe_ctxt = LetPat { pc_lvl = bind_lvl
+ , pc_sig_fn = sig_fn
+ , pc_new = no_gen } })
+ bndr_name exp_pat_ty
+ -- For the LetPat cases, see
+ -- Note [Typechecking pattern bindings] in GHC.Tc.Gen.Bind
+
+ | Just bndr_id <- sig_fn bndr_name -- There is a signature
+ = do { wrap <- tcSubTypePat penv exp_pat_ty (idType bndr_id)
+ -- See Note [Subsumption check at pattern variables]
+ ; traceTc "tcPatBndr(sig)" (ppr bndr_id $$ ppr (idType bndr_id) $$ ppr exp_pat_ty)
+ ; return (wrap, bndr_id) }
+
+ | otherwise -- No signature
+ = do { (co, bndr_ty) <- case exp_pat_ty of
+ Check pat_ty -> promoteTcType bind_lvl pat_ty
+ Infer infer_res -> ASSERT( bind_lvl == ir_lvl infer_res )
+ -- If we were under a constructor that bumped
+ -- the level, we'd be in checking mode
+ do { bndr_ty <- inferResultToType infer_res
+ ; return (mkTcNomReflCo bndr_ty, bndr_ty) }
+ ; bndr_id <- newLetBndr no_gen bndr_name bndr_ty
+ ; traceTc "tcPatBndr(nosig)" (vcat [ ppr bind_lvl
+ , ppr exp_pat_ty, ppr bndr_ty, ppr co
+ , ppr bndr_id ])
+ ; return (mkWpCastN co, bndr_id) }
+
+tcPatBndr _ bndr_name pat_ty
+ = do { pat_ty <- expTypeToType pat_ty
+ ; traceTc "tcPatBndr(not let)" (ppr bndr_name $$ ppr pat_ty)
+ ; return (idHsWrapper, mkLocalIdOrCoVar bndr_name pat_ty) }
+ -- We should not have "OrCoVar" here, this is a bug (#17545)
+ -- Whether or not there is a sig is irrelevant,
+ -- as this is local
+
+newLetBndr :: LetBndrSpec -> Name -> TcType -> TcM TcId
+-- Make up a suitable Id for the pattern-binder.
+-- See Note [Typechecking pattern bindings], item (4) in GHC.Tc.Gen.Bind
+--
+-- In the polymorphic case when we are going to generalise
+-- (plan InferGen, no_gen = LetLclBndr), generate a "monomorphic version"
+-- of the Id; the original name will be bound to the polymorphic version
+-- by the AbsBinds
+-- In the monomorphic case when we are not going to generalise
+-- (plan NoGen, no_gen = LetGblBndr) there is no AbsBinds,
+-- and we use the original name directly
+newLetBndr LetLclBndr name ty
+ = do { mono_name <- cloneLocalName name
+ ; return (mkLocalId mono_name ty) }
+newLetBndr (LetGblBndr prags) name ty
+ = addInlinePrags (mkLocalId name ty) (lookupPragEnv prags name)
+
+tcSubTypePat :: PatEnv -> ExpSigmaType -> TcSigmaType -> TcM HsWrapper
+-- tcSubTypeET with the UserTypeCtxt specialised to GenSigCtxt
+-- Used when typechecking patterns
+tcSubTypePat penv t1 t2 = tcSubTypeET (pe_orig penv) GenSigCtxt t1 t2
+
+{- Note [Subsumption check at pattern variables]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When we come across a variable with a type signature, we need to do a
+subsumption, not equality, check against the context type. e.g.
+
+ data T = MkT (forall a. a->a)
+ f :: forall b. [b]->[b]
+ MkT f = blah
+
+Since 'blah' returns a value of type T, its payload is a polymorphic
+function of type (forall a. a->a). And that's enough to bind the
+less-polymorphic function 'f', but we need some impedance matching
+to witness the instantiation.
+
+
+************************************************************************
+* *
+ The main worker functions
+* *
+************************************************************************
+
+Note [Nesting]
+~~~~~~~~~~~~~~
+tcPat takes a "thing inside" over which the pattern scopes. This is partly
+so that tcPat can extend the environment for the thing_inside, but also
+so that constraints arising in the thing_inside can be discharged by the
+pattern.
+
+This does not work so well for the ErrCtxt carried by the monad: we don't
+want the error-context for the pattern to scope over the RHS.
+Hence the getErrCtxt/setErrCtxt stuff in tcMultiple
+-}
+
+--------------------
+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 GhcRn
+ -> ExpSigmaType
+ -> PatEnv
+ -> TcM a
+ -> TcM (LPat GhcTcId, 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 GhcRn] -> [ExpSigmaType]
+ -> TcM a
+ -> TcM ([LPat GhcTcId], 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 GhcRn
+ -> ExpSigmaType -- Fully refined result type
+ -> TcM a -- Thing inside
+ -> TcM (Pat GhcTcId, -- Translated pattern
+ a) -- Result of thing inside
+
+tc_pat penv (VarPat x (L l name)) pat_ty thing_inside
+ = do { (wrap, id) <- tcPatBndr penv name pat_ty
+ ; res <- tcExtendIdEnv1 name id thing_inside
+ ; pat_ty <- readExpType pat_ty
+ ; return (mkHsWrapPat wrap (VarPat x (L l id)) pat_ty, res) }
+
+tc_pat penv (ParPat x pat) pat_ty thing_inside
+ = do { (pat', res) <- tc_lpat pat pat_ty penv thing_inside
+ ; return (ParPat x pat', res) }
+
+tc_pat penv (BangPat x pat) pat_ty thing_inside
+ = do { (pat', res) <- tc_lpat pat pat_ty penv thing_inside
+ ; return (BangPat x pat', res) }
+
+tc_pat penv (LazyPat x 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 that the expected pattern type is itself lifted
+ ; pat_ty <- readExpType pat_ty
+ ; _ <- unifyType Nothing (tcTypeKind pat_ty) liftedTypeKind
+
+ ; return (LazyPat x pat', res) }
+
+tc_pat _ (WildPat _) pat_ty thing_inside
+ = do { res <- thing_inside
+ ; pat_ty <- expTypeToType pat_ty
+ ; return (WildPat pat_ty, res) }
+
+tc_pat penv (AsPat x (L nm_loc name) pat) pat_ty thing_inside
+ = do { (wrap, bndr_id) <- setSrcSpan nm_loc (tcPatBndr penv name pat_ty)
+ ; (pat', res) <- tcExtendIdEnv1 name bndr_id $
+ tc_lpat pat (mkCheckExpType $ 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!
+ ; pat_ty <- readExpType pat_ty
+ ; return (mkHsWrapPat wrap (AsPat x (L nm_loc bndr_id) pat') pat_ty,
+ res) }
+
+tc_pat penv (ViewPat _ expr pat) overall_pat_ty thing_inside
+ = do {
+ -- Expr must have type `forall a1...aN. OPT' -> B`
+ -- where overall_pat_ty is an instance of OPT'.
+ ; (expr',expr'_inferred) <- tcInferSigma expr
+
+ -- expression must be a function
+ ; let expr_orig = lexprCtOrigin expr
+ herald = text "A view pattern expression expects"
+ ; (expr_wrap1, [inf_arg_ty], inf_res_ty)
+ <- matchActualFunTys herald expr_orig (Just (unLoc expr)) 1 expr'_inferred
+ -- expr_wrap1 :: expr'_inferred "->" (inf_arg_ty -> inf_res_ty)
+
+ -- check that overall pattern is more polymorphic than arg type
+ ; expr_wrap2 <- tcSubTypePat penv overall_pat_ty inf_arg_ty
+ -- expr_wrap2 :: overall_pat_ty "->" inf_arg_ty
+
+ -- pattern must have inf_res_ty
+ ; (pat', res) <- tc_lpat pat (mkCheckExpType inf_res_ty) penv thing_inside
+
+ ; overall_pat_ty <- readExpType overall_pat_ty
+ ; let expr_wrap2' = mkWpFun expr_wrap2 idHsWrapper
+ overall_pat_ty inf_res_ty doc
+ -- expr_wrap2' :: (inf_arg_ty -> inf_res_ty) "->"
+ -- (overall_pat_ty -> inf_res_ty)
+ expr_wrap = expr_wrap2' <.> expr_wrap1
+ doc = text "When checking the view pattern function:" <+> (ppr expr)
+ ; return (ViewPat overall_pat_ty (mkLHsWrap expr_wrap expr') pat', res)}
+
+-- Type signatures in patterns
+-- See Note [Pattern coercions] below
+tc_pat penv (SigPat _ pat sig_ty) pat_ty thing_inside
+ = do { (inner_ty, tv_binds, wcs, wrap) <- tcPatSig (inPatBind penv)
+ sig_ty pat_ty
+ -- Using tcExtendNameTyVarEnv is appropriate here
+ -- because we're not really bringing fresh tyvars into scope.
+ -- We're *naming* existing tyvars. Note that it is OK for a tyvar
+ -- from an outer scope to mention one of these tyvars in its kind.
+ ; (pat', res) <- tcExtendNameTyVarEnv wcs $
+ tcExtendNameTyVarEnv tv_binds $
+ tc_lpat pat (mkCheckExpType inner_ty) penv thing_inside
+ ; pat_ty <- readExpType pat_ty
+ ; return (mkHsWrapPat wrap (SigPat inner_ty pat' sig_ty) pat_ty, res) }
+
+------------------------
+-- Lists, tuples, arrays
+tc_pat penv (ListPat Nothing pats) pat_ty thing_inside
+ = do { (coi, elt_ty) <- matchExpectedPatTy matchExpectedListTy penv pat_ty
+ ; (pats', res) <- tcMultiple (\p -> tc_lpat p (mkCheckExpType elt_ty))
+ pats penv thing_inside
+ ; pat_ty <- readExpType pat_ty
+ ; return (mkHsWrapPat coi
+ (ListPat (ListPatTc elt_ty Nothing) pats') pat_ty, res)
+}
+
+tc_pat penv (ListPat (Just e) pats) pat_ty thing_inside
+ = do { tau_pat_ty <- expTypeToType pat_ty
+ ; ((pats', res, elt_ty), e')
+ <- tcSyntaxOpGen ListOrigin e [SynType (mkCheckExpType tau_pat_ty)]
+ SynList $
+ \ [elt_ty] ->
+ do { (pats', res) <- tcMultiple (\p -> tc_lpat p (mkCheckExpType elt_ty))
+ pats penv thing_inside
+ ; return (pats', res, elt_ty) }
+ ; return (ListPat (ListPatTc elt_ty (Just (tau_pat_ty,e'))) pats', res)
+}
+
+tc_pat penv (TuplePat _ pats boxity) pat_ty thing_inside
+ = do { let arity = length pats
+ tc = tupleTyCon boxity arity
+ -- NB: tupleTyCon does not flatten 1-tuples
+ -- See Note [Don't flatten tuples from HsSyn] in GHC.Core.Make
+ ; (coi, arg_tys) <- matchExpectedPatTy (matchExpectedTyConApp tc)
+ penv pat_ty
+ -- Unboxed tuples have RuntimeRep vars, which we discard:
+ -- See Note [Unboxed tuple RuntimeRep vars] in GHC.Core.TyCon
+ ; let con_arg_tys = case boxity of Unboxed -> drop arity arg_tys
+ Boxed -> arg_tys
+ ; (pats', res) <- tc_lpats penv pats (map mkCheckExpType con_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
+ unmangled_result = TuplePat con_arg_tys pats' boxity
+ -- pat_ty /= pat_ty iff coi /= IdCo
+ possibly_mangled_result
+ | gopt Opt_IrrefutableTuples dflags &&
+ isBoxed boxity = LazyPat noExtField (noLoc unmangled_result)
+ | otherwise = unmangled_result
+
+ ; pat_ty <- readExpType pat_ty
+ ; ASSERT( con_arg_tys `equalLength` pats ) -- Syntactically enforced
+ return (mkHsWrapPat coi possibly_mangled_result pat_ty, res)
+ }
+
+tc_pat penv (SumPat _ pat alt arity ) pat_ty thing_inside
+ = do { let tc = sumTyCon arity
+ ; (coi, arg_tys) <- matchExpectedPatTy (matchExpectedTyConApp tc)
+ penv pat_ty
+ ; -- Drop levity vars, we don't care about them here
+ let con_arg_tys = drop arity arg_tys
+ ; (pat', res) <- tc_lpat pat (mkCheckExpType (con_arg_tys `getNth` (alt - 1)))
+ penv thing_inside
+ ; pat_ty <- readExpType pat_ty
+ ; return (mkHsWrapPat coi (SumPat con_arg_tys pat' alt arity) 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 penv (LitPat x simple_lit) pat_ty thing_inside
+ = do { let lit_ty = hsLitType simple_lit
+ ; wrap <- tcSubTypePat penv pat_ty lit_ty
+ ; res <- thing_inside
+ ; pat_ty <- readExpType pat_ty
+ ; return ( mkHsWrapPat wrap (LitPat x (convertLit simple_lit)) pat_ty
+ , res) }
+
+------------------------
+-- Overloaded patterns: n, and n+k
+
+-- In the case of a negative literal (the more complicated case),
+-- we get
+--
+-- case v of (-5) -> blah
+--
+-- becoming
+--
+-- if v == (negate (fromInteger 5)) then blah else ...
+--
+-- There are two bits of rebindable syntax:
+-- (==) :: pat_ty -> neg_lit_ty -> Bool
+-- negate :: lit_ty -> neg_lit_ty
+-- where lit_ty is the type of the overloaded literal 5.
+--
+-- When there is no negation, neg_lit_ty and lit_ty are the same
+tc_pat _ (NPat _ (L l over_lit) mb_neg eq) pat_ty thing_inside
+ = do { let orig = LiteralOrigin over_lit
+ ; ((lit', mb_neg'), eq')
+ <- tcSyntaxOp orig eq [SynType pat_ty, SynAny]
+ (mkCheckExpType boolTy) $
+ \ [neg_lit_ty] ->
+ let new_over_lit lit_ty = newOverloadedLit over_lit
+ (mkCheckExpType lit_ty)
+ in case mb_neg of
+ Nothing -> (, Nothing) <$> new_over_lit neg_lit_ty
+ Just neg -> -- Negative literal
+ -- The 'negate' is re-mappable syntax
+ second Just <$>
+ (tcSyntaxOp orig neg [SynRho] (mkCheckExpType neg_lit_ty) $
+ \ [lit_ty] -> new_over_lit lit_ty)
+
+ ; res <- thing_inside
+ ; pat_ty <- readExpType pat_ty
+ ; return (NPat pat_ty (L l lit') mb_neg' eq', res) }
+
+{-
+Note [NPlusK patterns]
+~~~~~~~~~~~~~~~~~~~~~~
+From
+
+ case v of x + 5 -> blah
+
+we get
+
+ if v >= 5 then (\x -> blah) (v - 5) else ...
+
+There are two bits of rebindable syntax:
+ (>=) :: pat_ty -> lit1_ty -> Bool
+ (-) :: pat_ty -> lit2_ty -> var_ty
+
+lit1_ty and lit2_ty could conceivably be different.
+var_ty is the type inferred for x, the variable in the pattern.
+
+If the pushed-down pattern type isn't a tau-type, the two pat_ty's above
+could conceivably be different specializations. But this is very much
+like the situation in Note [Case branches must be taus] in GHC.Tc.Gen.Match.
+So we tauify the pat_ty before proceeding.
+
+Note that we need to type-check the literal twice, because it is used
+twice, and may be used at different types. The second HsOverLit stored in the
+AST is used for the subtraction operation.
+-}
+
+-- See Note [NPlusK patterns]
+tc_pat penv (NPlusKPat _ (L nm_loc name)
+ (L loc lit) _ ge minus) pat_ty
+ thing_inside
+ = do { pat_ty <- expTypeToType pat_ty
+ ; let orig = LiteralOrigin lit
+ ; (lit1', ge')
+ <- tcSyntaxOp orig ge [synKnownType pat_ty, SynRho]
+ (mkCheckExpType boolTy) $
+ \ [lit1_ty] ->
+ newOverloadedLit lit (mkCheckExpType lit1_ty)
+ ; ((lit2', minus_wrap, bndr_id), minus')
+ <- tcSyntaxOpGen orig minus [synKnownType pat_ty, SynRho] SynAny $
+ \ [lit2_ty, var_ty] ->
+ do { lit2' <- newOverloadedLit lit (mkCheckExpType lit2_ty)
+ ; (wrap, bndr_id) <- setSrcSpan nm_loc $
+ tcPatBndr penv name (mkCheckExpType var_ty)
+ -- co :: var_ty ~ idType bndr_id
+
+ -- minus_wrap is applicable to minus'
+ ; return (lit2', wrap, bndr_id) }
+
+ -- The Report says that n+k patterns must be in Integral
+ -- but it's silly to insist on this in the RebindableSyntax case
+ ; unlessM (xoptM LangExt.RebindableSyntax) $
+ do { icls <- tcLookupClass integralClassName
+ ; instStupidTheta orig [mkClassPred icls [pat_ty]] }
+
+ ; res <- tcExtendIdEnv1 name bndr_id thing_inside
+
+ ; let minus'' = case minus' of
+ NoSyntaxExprTc -> pprPanic "tc_pat NoSyntaxExprTc" (ppr minus')
+ -- this should be statically avoidable
+ -- Case (3) from Note [NoSyntaxExpr] in Hs.Expr
+ SyntaxExprTc { syn_expr = minus'_expr
+ , syn_arg_wraps = minus'_arg_wraps
+ , syn_res_wrap = minus'_res_wrap }
+ -> SyntaxExprTc { syn_expr = minus'_expr
+ , syn_arg_wraps = minus'_arg_wraps
+ , syn_res_wrap = minus_wrap <.> minus'_res_wrap }
+ -- Oy. This should really be a record update, but
+ -- we get warnings if we try. #17783
+ pat' = NPlusKPat pat_ty (L nm_loc bndr_id) (L loc lit1') lit2'
+ ge' minus''
+ ; return (pat', res) }
+
+-- HsSpliced is an annotation produced by 'GHC.Rename.Splice.rnSplicePat'.
+-- Here we get rid of it and add the finalizers to the global environment.
+--
+-- See Note [Delaying modFinalizers in untyped splices] in GHC.Rename.Splice.
+tc_pat penv (SplicePat _ (HsSpliced _ mod_finalizers (HsSplicedPat pat)))
+ pat_ty thing_inside
+ = do addModFinalizersWithLclEnv mod_finalizers
+ tc_pat penv pat pat_ty thing_inside
+
+tc_pat _ _other_pat _ _ = panic "tc_pat" -- ConPatOut, SigPatOut
+
+
+{-
+Note [Hopping the LIE in lazy patterns]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In a lazy pattern, we must *not* discharge constraints from the RHS
+from dictionaries bound in the pattern. E.g.
+ f ~(C x) = 3
+We can't discharge the Num constraint from dictionaries bound by
+the pattern C!
+
+So we have to make the constraints from thing_inside "hop around"
+the pattern. Hence the captureConstraints and emitConstraints.
+
+The same thing ensures that equality constraints in a lazy match
+are not made available in the RHS of the match. For example
+ data T a where { T1 :: Int -> T Int; ... }
+ f :: T a -> Int -> a
+ f ~(T1 i) y = y
+It's obviously not sound to refine a to Int in the right
+hand side, because the argument might not match T1 at all!
+
+Finally, a lazy pattern should not bind any existential type variables
+because they won't be in scope when we do the desugaring
+
+
+************************************************************************
+* *
+ Most of the work for constructors is here
+ (the rest is in the ConPatIn case of tc_pat)
+* *
+************************************************************************
+
+[Pattern matching indexed data types]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider the following declarations:
+
+ data family Map k :: * -> *
+ data instance Map (a, b) v = MapPair (Map a (Pair b v))
+
+and a case expression
+
+ case x :: Map (Int, c) w of MapPair m -> ...
+
+As explained by [Wrappers for data instance tycons] in GHC.Types.Id.Make, the
+worker/wrapper types for MapPair are
+
+ $WMapPair :: forall a b v. Map a (Map a b v) -> Map (a, b) v
+ $wMapPair :: forall a b v. Map a (Map a b v) -> :R123Map a b v
+
+So, the type of the scrutinee is Map (Int, c) w, but the tycon of MapPair is
+:R123Map, which means the straight use of boxySplitTyConApp would give a type
+error. Hence, the smart wrapper function boxySplitTyConAppWithFamily calls
+boxySplitTyConApp with the family tycon Map instead, which gives us the family
+type list {(Int, c), w}. To get the correct split for :R123Map, we need to
+unify the family type list {(Int, c), w} with the instance types {(a, b), v}
+(provided by tyConFamInst_maybe together with the family tycon). This
+unification yields the substitution [a -> Int, b -> c, v -> w], which gives us
+the split arguments for the representation tycon :R123Map as {Int, c, w}
+
+In other words, boxySplitTyConAppWithFamily implicitly takes the coercion
+
+ Co123Map a b v :: {Map (a, b) v ~ :R123Map a b v}
+
+moving between representation and family type into account. To produce type
+correct Core, this coercion needs to be used to case the type of the scrutinee
+from the family to the representation type. This is achieved by
+unwrapFamInstScrutinee using a CoPat around the result pattern.
+
+Now it might appear seem as if we could have used the previous GADT type
+refinement infrastructure of refineAlt and friends instead of the explicit
+unification and CoPat generation. However, that would be wrong. Why? The
+whole point of GADT refinement is that the refinement is local to the case
+alternative. In contrast, the substitution generated by the unification of
+the family type list and instance types needs to be propagated to the outside.
+Imagine that in the above example, the type of the scrutinee would have been
+(Map x w), then we would have unified {x, w} with {(a, b), v}, yielding the
+substitution [x -> (a, b), v -> w]. In contrast to GADT matching, the
+instantiation of x with (a, b) must be global; ie, it must be valid in *all*
+alternatives of the case expression, whereas in the GADT case it might vary
+between alternatives.
+
+RIP GADT refinement: refinements have been replaced by the use of explicit
+equality constraints that are used in conjunction with implication constraints
+to express the local scope of GADT refinements.
+-}
+
+-- Running example:
+-- MkT :: forall a b c. (a~[b]) => b -> c -> T a
+-- with scrutinee of type (T ty)
+
+tcConPat :: PatEnv -> Located Name
+ -> ExpSigmaType -- Type of the pattern
+ -> HsConPatDetails GhcRn -> TcM a
+ -> TcM (Pat GhcTcId, a)
+tcConPat penv con_lname@(L _ con_name) pat_ty arg_pats thing_inside
+ = do { con_like <- tcLookupConLike con_name
+ ; case con_like of
+ RealDataCon data_con -> tcDataConPat penv con_lname data_con
+ pat_ty arg_pats thing_inside
+ PatSynCon pat_syn -> tcPatSynPat penv con_lname pat_syn
+ pat_ty arg_pats thing_inside
+ }
+
+tcDataConPat :: PatEnv -> Located Name -> DataCon
+ -> ExpSigmaType -- Type of the pattern
+ -> HsConPatDetails GhcRn -> TcM a
+ -> TcM (Pat GhcTcId, a)
+tcDataConPat penv (L con_span con_name) data_con pat_ty
+ arg_pats thing_inside
+ = do { 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
+ header = L con_span (RealDataCon 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) <- matchExpectedConTy penv tycon pat_ty
+ ; pat_ty <- readExpType pat_ty
+
+ -- Add the stupid theta
+ ; setSrcSpan con_span $ addDataConStupidTheta data_con ctxt_res_tys
+
+ ; let all_arg_tys = eqSpecPreds eq_spec ++ theta ++ arg_tys
+ ; checkExistentials ex_tvs all_arg_tys penv
+
+ ; tenv <- instTyVarsWith PatOrigin univ_tvs ctxt_res_tys
+ -- NB: Do not use zipTvSubst! See #14154
+ -- We want to create a well-kinded substitution, so
+ -- that the instantiated type is well-kinded
+
+ ; (tenv, ex_tvs') <- tcInstSuperSkolTyVarsX tenv 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" (vcat [ ppr con_name
+ , pprTyVars univ_tvs
+ , pprTyVars ex_tvs
+ , ppr eq_spec
+ , ppr theta
+ , pprTyVars ex_tvs'
+ , ppr ctxt_res_tys
+ , ppr arg_tys'
+ , ppr arg_pats ])
+ ; 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 (RealDataCon data_con) arg_tys'
+ arg_pats penv thing_inside
+ ; let res_pat = ConPatOut { pat_con = header,
+ pat_tvs = [], pat_dicts = [],
+ pat_binds = emptyTcEvBinds,
+ pat_args = arg_pats',
+ pat_arg_tys = ctxt_res_tys,
+ pat_wrap = idHsWrapper }
+
+ ; 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 = null eq_spec && not (any isEqPred theta)
+ skol_info = PatSkol (RealDataCon data_con) mc
+ mc = case pe_ctxt penv of
+ LamPat mc -> mc
+ LetPat {} -> PatBindRhs
+
+ ; gadts_on <- xoptM LangExt.GADTs
+ ; families_on <- xoptM LangExt.TypeFamilies
+ ; checkTc (no_equalities || gadts_on || families_on)
+ (text "A pattern match on a GADT requires the" <+>
+ text "GADTs or TypeFamilies language extension")
+ -- #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 (RealDataCon data_con) arg_tys' arg_pats penv thing_inside
+
+ ; let res_pat = ConPatOut { pat_con = header,
+ pat_tvs = ex_tvs',
+ pat_dicts = given,
+ pat_binds = ev_binds,
+ pat_args = arg_pats',
+ pat_arg_tys = ctxt_res_tys,
+ pat_wrap = idHsWrapper }
+ ; return (mkHsWrapPat wrap res_pat pat_ty, res)
+ } }
+
+tcPatSynPat :: PatEnv -> Located Name -> PatSyn
+ -> ExpSigmaType -- Type of the pattern
+ -> HsConPatDetails GhcRn -> TcM a
+ -> TcM (Pat GhcTcId, a)
+tcPatSynPat penv (L con_span _) pat_syn pat_ty arg_pats thing_inside
+ = do { let (univ_tvs, req_theta, ex_tvs, prov_theta, arg_tys, ty) = patSynSig pat_syn
+
+ ; (subst, univ_tvs') <- newMetaTyVars univ_tvs
+
+ ; let all_arg_tys = ty : prov_theta ++ arg_tys
+ ; checkExistentials ex_tvs all_arg_tys penv
+ ; (tenv, ex_tvs') <- tcInstSuperSkolTyVarsX subst ex_tvs
+ ; let ty' = substTy tenv ty
+ arg_tys' = substTys tenv arg_tys
+ prov_theta' = substTheta tenv prov_theta
+ req_theta' = substTheta tenv req_theta
+
+ ; wrap <- tcSubTypePat penv pat_ty ty'
+ ; traceTc "tcPatSynPat" (ppr pat_syn $$
+ ppr pat_ty $$
+ ppr ty' $$
+ ppr ex_tvs' $$
+ ppr prov_theta' $$
+ ppr req_theta' $$
+ ppr arg_tys')
+
+ ; prov_dicts' <- newEvVars prov_theta'
+
+ ; let skol_info = case pe_ctxt penv of
+ LamPat mc -> PatSkol (PatSynCon pat_syn) mc
+ LetPat {} -> UnkSkol -- Doesn't matter
+
+ ; req_wrap <- instCall PatOrigin (mkTyVarTys univ_tvs') req_theta'
+ ; traceTc "instCall" (ppr req_wrap)
+
+ ; traceTc "checkConstraints {" Outputable.empty
+ ; (ev_binds, (arg_pats', res))
+ <- checkConstraints skol_info ex_tvs' prov_dicts' $
+ tcConArgs (PatSynCon pat_syn) arg_tys' arg_pats penv thing_inside
+
+ ; traceTc "checkConstraints }" (ppr ev_binds)
+ ; let res_pat = ConPatOut { pat_con = L con_span $ PatSynCon pat_syn,
+ pat_tvs = ex_tvs',
+ pat_dicts = prov_dicts',
+ pat_binds = ev_binds,
+ pat_args = arg_pats',
+ pat_arg_tys = mkTyVarTys univ_tvs',
+ pat_wrap = req_wrap }
+ ; pat_ty <- readExpType pat_ty
+ ; return (mkHsWrapPat wrap res_pat pat_ty, res) }
+
+----------------------------
+-- | Convenient wrapper for calling a matchExpectedXXX function
+matchExpectedPatTy :: (TcRhoType -> TcM (TcCoercionN, a))
+ -> PatEnv -> ExpSigmaType -> TcM (HsWrapper, a)
+-- See Note [Matching polytyped patterns]
+-- Returns a wrapper : pat_ty ~R inner_ty
+matchExpectedPatTy inner_match (PE { pe_orig = orig }) pat_ty
+ = do { pat_ty <- expTypeToType pat_ty
+ ; (wrap, pat_rho) <- topInstantiate orig pat_ty
+ ; (co, res) <- inner_match pat_rho
+ ; traceTc "matchExpectedPatTy" (ppr pat_ty $$ ppr wrap)
+ ; return (mkWpCastN (mkTcSymCo co) <.> wrap, res) }
+
+----------------------------
+matchExpectedConTy :: PatEnv
+ -> TyCon -- The TyCon that this data
+ -- constructor actually returns
+ -- In the case of a data family this is
+ -- the /representation/ TyCon
+ -> ExpSigmaType -- The type of the pattern; in the case
+ -- of a data family this would mention
+ -- the /family/ TyCon
+ -> TcM (HsWrapper, [TcSigmaType])
+-- See Note [Matching constructor patterns]
+-- Returns a wrapper : pat_ty "->" T ty1 ... tyn
+matchExpectedConTy (PE { pe_orig = orig }) data_tc exp_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 { pat_ty <- expTypeToType exp_pat_ty
+ ; (wrap, pat_rho) <- topInstantiate orig pat_ty
+
+ ; (subst, tvs') <- newMetaTyVars (tyConTyVars data_tc)
+ -- tys = [ty1,ty2]
+
+ ; traceTc "matchExpectedConTy" (vcat [ppr data_tc,
+ ppr (tyConTyVars data_tc),
+ ppr fam_tc, ppr fam_args,
+ ppr exp_pat_ty,
+ ppr pat_ty,
+ ppr pat_rho, ppr wrap])
+ ; co1 <- unifyType Nothing (mkTyConApp fam_tc (substTys subst fam_args)) pat_rho
+ -- co1 : T (ty1,ty2) ~N pat_rho
+ -- could use tcSubType here... but it's the wrong way round
+ -- for actual vs. expected in error messages.
+
+ ; let tys' = mkTyVarTys tvs'
+ co2 = mkTcUnbranchedAxInstCo co_tc tys' []
+ -- co2 : T (ty1,ty2) ~R T7 ty1 ty2
+
+ full_co = mkTcSubCo (mkTcSymCo co1) `mkTcTransCo` co2
+ -- full_co :: pat_rho ~R T7 ty1 ty2
+
+ ; return ( mkWpCastR full_co <.> wrap, tys') }
+
+ | otherwise
+ = do { pat_ty <- expTypeToType exp_pat_ty
+ ; (wrap, pat_rho) <- topInstantiate orig pat_ty
+ ; (coi, tys) <- matchExpectedTyConApp data_tc pat_rho
+ ; return (mkWpCastN (mkTcSymCo coi) <.> wrap, tys) }
+
+{-
+Note [Matching constructor patterns]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose (coi, tys) = matchExpectedConType data_tc pat_ty
+
+ * In the simple case, pat_ty = tc tys
+
+ * If pat_ty is a polytype, we want to instantiate it
+ This is like part of a subsumption check. Eg
+ f :: (forall a. [a]) -> blah
+ f [] = blah
+
+ * In a type family case, suppose we have
+ data family T a
+ data instance T (p,q) = A p | B q
+ Then we'll have internally generated
+ data T7 p q = A p | B q
+ axiom coT7 p q :: T (p,q) ~ T7 p q
+
+ So if pat_ty = T (ty1,ty2), we return (coi, [ty1,ty2]) such that
+ coi = coi2 . coi1 : T7 t ~ pat_ty
+ coi1 : T (ty1,ty2) ~ pat_ty
+ coi2 : T7 ty1 ty2 ~ T (ty1,ty2)
+
+ For families we do all this matching here, not in the unifier,
+ because we never want a whisper of the data_tycon to appear in
+ error messages; it's a purely internal thing
+-}
+
+tcConArgs :: ConLike -> [TcSigmaType]
+ -> Checker (HsConPatDetails GhcRn) (HsConPatDetails GhcTc)
+
+tcConArgs con_like arg_tys (PrefixCon arg_pats) penv thing_inside
+ = do { checkTc (con_arity == no_of_args) -- Check correct arity
+ (arityErr (text "constructor") con_like 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 = conLikeArity con_like
+ no_of_args = length arg_pats
+
+tcConArgs con_like arg_tys (InfixCon p1 p2) penv thing_inside
+ = do { checkTc (con_arity == 2) -- Check correct arity
+ (arityErr (text "constructor") con_like 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 = conLikeArity con_like
+
+tcConArgs con_like 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 (LHsRecField GhcRn (LPat GhcRn))
+ (LHsRecField GhcTcId (LPat GhcTcId))
+ tc_field (L l (HsRecField (L loc (FieldOcc sel (L lr rdr))) pat pun))
+ penv thing_inside
+ = do { sel' <- tcLookupId sel
+ ; pat_ty <- setSrcSpan loc $ find_field_ty sel
+ (occNameFS $ rdrNameOcc rdr)
+ ; (pat', res) <- tcConArg (pat, pat_ty) penv thing_inside
+ ; return (L l (HsRecField (L loc (FieldOcc sel' (L lr rdr))) pat'
+ pun), res) }
+ tc_field (L _ (HsRecField (L _ (XFieldOcc _)) _ _)) _ _
+ = panic "tcConArgs"
+
+
+ find_field_ty :: Name -> FieldLabelString -> TcM TcType
+ find_field_ty sel lbl
+ = case [ty | (fl, ty) <- field_tys, flSelector fl == sel] of
+
+ -- No matching field; chances are this field label comes from some
+ -- other record type (or maybe none). If this happens, just fail,
+ -- otherwise we get crashes later (#8570), and similar:
+ -- 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".
+ [] -> failWith (badFieldCon con_like lbl)
+
+ -- The normal case, when the field comes from the right constructor
+ (pat_ty : extras) -> do
+ traceTc "find_field" (ppr pat_ty <+> ppr extras)
+ ASSERT( null extras ) (return pat_ty)
+
+ field_tys :: [(FieldLabel, TcType)]
+ field_tys = zip (conLikeFieldLabels con_like) 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 GhcRn, TcSigmaType) (LPat GhcTc)
+tcConArg (arg_pat, arg_ty) penv thing_inside
+ = tc_lpat arg_pat (mkCheckExpType 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
+ univ_tvs = dataConUnivTyVars data_con
+ tenv = zipTvSubst univ_tvs (takeList univ_tvs inst_tys)
+ -- NB: inst_tys can be longer than the univ tyvars
+ -- because the constructor might have existentials
+ inst_theta = substTheta tenv stupid_theta
+
+{-
+Note [Arrows and patterns]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+(Oct 07) Arrow notation has the odd property that it involves
+"holes in the scope". For example:
+ expr :: Arrow a => a () Int
+ expr = proc (y,z) -> do
+ x <- term -< y
+ expr' -< x
+
+Here the 'proc (y,z)' binding scopes over the arrow tails but not the
+arrow body (e.g 'term'). As things stand (bogusly) all the
+constraints from the proc body are gathered together, so constraints
+from 'term' will be seen by the tcPat for (y,z). But we must *not*
+bind constraints from 'term' here, because the desugarer will not make
+these bindings scope over 'term'.
+
+The Right Thing is not to confuse these constraints together. But for
+now the Easy Thing is to ensure that we do not have existential or
+GADT constraints in a 'proc', and to short-cut the constraint
+simplification for such vanilla patterns so that it binds no
+constraints. Hence the 'fast path' in tcConPat; but it's also a good
+plan for ordinary vanilla patterns to bypass the constraint
+simplification step.
+
+************************************************************************
+* *
+ Note [Pattern coercions]
+* *
+************************************************************************
+
+In principle, these program would be reasonable:
+
+ f :: (forall a. a->a) -> Int
+ f (x :: Int->Int) = x 3
+
+ g :: (forall a. [a]) -> Bool
+ g [] = True
+
+In both cases, the function type signature restricts what arguments can be passed
+in a call (to polymorphic ones). The pattern type signature then instantiates this
+type. For example, in the first case, (forall a. a->a) <= Int -> Int, and we
+generate the translated term
+ f = \x' :: (forall a. a->a). let x = x' Int in x 3
+
+From a type-system point of view, this is perfectly fine, but it's *very* seldom useful.
+And it requires a significant amount of code to implement, because we need to decorate
+the translated pattern with coercion functions (generated from the subsumption check
+by tcSub).
+
+So for now I'm just insisting on type *equality* in patterns. No subsumption.
+
+Old notes about desugaring, at a time when pattern coercions were handled:
+
+A SigPat is a type coercion and must be handled one at a time. We can't
+combine them unless the type of the pattern inside is identical, and we don't
+bother to check for that. For example:
+
+ data T = T1 Int | T2 Bool
+ f :: (forall a. a -> a) -> T -> t
+ f (g::Int->Int) (T1 i) = T1 (g i)
+ f (g::Bool->Bool) (T2 b) = T2 (g b)
+
+We desugar this as follows:
+
+ f = \ g::(forall a. a->a) t::T ->
+ let gi = g Int
+ in case t of { T1 i -> T1 (gi i)
+ other ->
+ let gb = g Bool
+ in case t of { T2 b -> T2 (gb b)
+ other -> fail }}
+
+Note that we do not treat the first column of patterns as a
+column of variables, because the coerced variables (gi, gb)
+would be of different types. So we get rather grotty code.
+But I don't think this is a common case, and if it was we could
+doubtless improve it.
+
+Meanwhile, the strategy is:
+ * treat each SigPat coercion (always non-identity coercions)
+ as a separate block
+ * deal with the stuff inside, and then wrap a binding round
+ the result to bind the new variable (gi, gb, etc)
+
+
+************************************************************************
+* *
+\subsection{Errors and contexts}
+* *
+************************************************************************
+
+Note [Existential check]
+~~~~~~~~~~~~~~~~~~~~~~~~
+Lazy patterns can't bind existentials. They arise in two ways:
+ * Let bindings let { C a b = e } in b
+ * Twiddle patterns f ~(C a b) = e
+The pe_lazy field of PatEnv says whether we are inside a lazy
+pattern (perhaps deeply)
+
+See also Note [Typechecking pattern bindings] in GHC.Tc.Gen.Bind
+-}
+
+maybeWrapPatCtxt :: Pat GhcRn -> (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 (text "In the pattern:") 2 (ppr pat)
+
+-----------------------------------------------
+checkExistentials :: [TyVar] -- existentials
+ -> [Type] -- argument types
+ -> PatEnv -> TcM ()
+ -- See Note [Existential check]]
+ -- See Note [Arrows and patterns]
+checkExistentials ex_tvs tys _
+ | all (not . (`elemVarSet` tyCoVarsOfTypes tys)) ex_tvs = return ()
+checkExistentials _ _ (PE { pe_ctxt = LetPat {}}) = return ()
+checkExistentials _ _ (PE { pe_ctxt = LamPat ProcExpr }) = failWithTc existentialProcPat
+checkExistentials _ _ (PE { pe_lazy = True }) = failWithTc existentialLazyPat
+checkExistentials _ _ _ = return ()
+
+existentialLazyPat :: SDoc
+existentialLazyPat
+ = hang (text "An existential or GADT data constructor cannot be used")
+ 2 (text "inside a lazy (~) pattern")
+
+existentialProcPat :: SDoc
+existentialProcPat
+ = text "Proc patterns cannot use existential or GADT data constructors"
+
+badFieldCon :: ConLike -> FieldLabelString -> SDoc
+badFieldCon con field
+ = hsep [text "Constructor" <+> quotes (ppr con),
+ text "does not have field", quotes (ppr field)]
+
+polyPatSig :: TcType -> SDoc
+polyPatSig sig_ty
+ = hang (text "Illegal polymorphic type signature in pattern:")
+ 2 (ppr sig_ty)