From 255418da5d264fb2758bc70925adb2094f34adc3 Mon Sep 17 00:00:00 2001 From: Sylvain Henry Date: Thu, 19 Mar 2020 10:28:01 +0100 Subject: Modules: type-checker (#13009) Update Haddock submodule --- compiler/GHC/Tc/Gen/Pat.hs | 1214 ++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 1214 insertions(+) create mode 100644 compiler/GHC/Tc/Gen/Pat.hs (limited to 'compiler/GHC/Tc/Gen/Pat.hs') 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) -- cgit v1.2.1