X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcPat.lhs;h=8304a22ddbe20cdf95fb0fff6824a2543c518ee4;hp=33b76302c9199e6b220feb625bca768522f9cd3d;hb=HEAD;hpb=3e83dfb21b2f2220dce97427fff5c19459ae68d1 diff --git a/compiler/typecheck/TcPat.lhs b/compiler/typecheck/TcPat.lhs index 33b7630..8304a22 100644 --- a/compiler/typecheck/TcPat.lhs +++ b/compiler/typecheck/TcPat.lhs @@ -1,62 +1,45 @@ % +% (c) The University of Glasgow 2006 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998 % -\section[TcPat]{Typechecking patterns} + +TcPat: Typechecking patterns \begin{code} -module TcPat ( tcLetPat, tcLamPat, tcLamPats, tcOverloadedLit, - badFieldCon, polyPatSig ) where +module TcPat ( tcLetPat, TcSigFun, TcSigInfo(..), TcPragFun + , LetBndrSpec(..), addInlinePrags, warnPrags + , tcPat, tcPats, newNoSigLetBndr, newSigLetBndr + , addDataConStupidTheta, badFieldCon, polyPatSig ) where #include "HsVersions.h" -import {-# SOURCE #-} TcExpr( tcSyntaxOp ) -import HsSyn ( Pat(..), LPat, HsConDetails(..), HsLit(..), HsOverLit(..), HsExpr(..), - mkCoPat, idCoercion, - LHsBinds, emptyLHsBinds, isEmptyLHsBinds, - collectPatsBinders, nlHsLit ) -import TcHsSyn ( TcId, hsLitType ) +import {-# SOURCE #-} TcExpr( tcSyntaxOp, tcInferRho) + +import HsSyn +import TcHsSyn import TcRnMonad -import Inst ( InstOrigin(..), shortCutFracLit, shortCutIntLit, - newDicts, instToId, tcInstStupidTheta, isHsVar - ) -import Id ( Id, idType, mkLocalId ) -import CoreFVs ( idFreeTyVars ) -import Name ( Name, mkSystemVarName ) -import TcSimplify ( tcSimplifyCheck, bindInstsOfLocalFuns ) -import TcEnv ( newLocalName, tcExtendIdEnv1, tcExtendTyVarEnv2, - tcLookupClass, tcLookupDataCon, refineEnvironment, - tcLookupField, tcMetaTy ) -import TcMType ( newFlexiTyVarTy, arityErr, tcInstSkolTyVars, -+ newCoVars, zonkTcType ) -import TcType ( TcType, TcTyVar, TcSigmaType, TcRhoType, BoxyType, - SkolemInfo(PatSkol), - BoxySigmaType, BoxyRhoType, argTypeKind, typeKind, - pprSkolTvBinding, isRigidTy, tcTyVarsOfTypes, - zipTopTvSubst, isArgTypeKind, isUnboxedTupleType, - mkTyVarTys, mkClassPred, isOverloadedTy, substEqSpec, - mkFunTy, mkFunTys, tidyOpenType, tidyOpenTypes ) -import VarSet ( elemVarSet ) -import {- Kind parts of -} - Type ( liftedTypeKind ) -import TcUnify ( boxySplitTyConApp, boxySplitListTy, unBox, - zapToMonotype, boxyUnify, checkSigTyVarsWrt, - unifyType ) -import TcHsType ( UserTypeCtxt(..), tcPatSig ) -import TysWiredIn ( boolTy, parrTyCon, tupleTyCon ) -import Type ( substTys, substTheta ) -import StaticFlags ( opt_IrrefutableTuples ) -import TyCon ( TyCon, FieldLabel ) -import DataCon ( DataCon, dataConTyCon, dataConFullSig, dataConName, - dataConFieldLabels, dataConSourceArity ) -import PrelNames ( integralClassName, fromIntegerName, integerTyConName, - fromRationalName, rationalTyConName ) -import BasicTypes ( isBoxed ) -import SrcLoc ( Located(..), SrcSpan, noLoc ) -import ErrUtils ( Message ) -import Util ( zipEqual ) -import Maybes ( MaybeErr(..) ) +import Inst +import Id +import Var +import Name +import TcEnv +import TcMType +import TcType +import TcUnify +import TcHsType +import TysWiredIn +import Coercion +import StaticFlags +import TyCon +import DataCon +import PrelNames +import BasicTypes hiding (SuccessFlag(..)) +import DynFlags +import SrcLoc +import Util import Outputable import FastString +import Control.Monad \end{code} @@ -67,26 +50,22 @@ import FastString %************************************************************************ \begin{code} -tcLetPat :: (Name -> Maybe TcRhoType) - -> LPat Name -> BoxySigmaType - -> TcM a +tcLetPat :: TcSigFun -> LetBndrSpec + -> LPat Name -> TcSigmaType + -> TcM a -> TcM (LPat TcId, a) -tcLetPat sig_fn pat pat_ty thing_inside - = do { let init_state = PS { pat_ctxt = LetPat sig_fn, - pat_reft = emptyRefinement } - ; (pat', ex_tvs, res) <- tc_lpat pat pat_ty init_state (\ _ -> thing_inside) - - -- Don't know how to deal with pattern-bound existentials yet - ; checkTc (null ex_tvs) (existentialExplode pat) - - ; return (pat', res) } +tcLetPat sig_fn no_gen pat pat_ty thing_inside + = tc_lpat pat pat_ty penv thing_inside + where + penv = PE { pe_lazy = True + , pe_ctxt = LetPat sig_fn no_gen } ----------------- -tcLamPats :: [LPat Name] -- Patterns, - -> [BoxySigmaType] -- and their types - -> BoxyRhoType -- Result type, - -> ((Refinement, BoxyRhoType) -> TcM a) -- and the checker for the body - -> TcM ([LPat TcId], a) +tcPats :: HsMatchContext Name + -> [LPat Name] -- Patterns, + -> [TcSigmaType] -- and their types + -> TcM a -- and the checker for the body + -> TcM ([LPat TcId], a) -- This is the externally-callable wrapper function -- Typecheck the patterns, extend the environment to bind the variables, @@ -96,74 +75,114 @@ tcLamPats :: [LPat Name] -- Patterns, -- 1. Initialise the PatState -- 2. Check the patterns --- 3. Apply the refinement to the environment and result type --- 4. Check the body --- 5. Check that no existentials escape - -tcLamPats pats tys res_ty thing_inside - = tc_lam_pats (zipEqual "tcLamPats" pats tys) - (emptyRefinement, res_ty) thing_inside +-- 3. Check the body +-- 4. Check that no existentials escape -tcLamPat :: LPat Name -> BoxySigmaType - -> (Refinement,BoxyRhoType) -- Result type - -> ((Refinement,BoxyRhoType) -> TcM a) -- Checker for body, given its result type - -> TcM (LPat TcId, a) -tcLamPat pat pat_ty res_ty thing_inside - = do { ([pat'],thing) <- tc_lam_pats [(pat, pat_ty)] res_ty thing_inside - ; return (pat', thing) } +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 } + +tcPat :: HsMatchContext Name + -> LPat Name -> TcSigmaType + -> TcM a -- Checker for body, given + -- its result type + -> TcM (LPat TcId, a) +tcPat ctxt pat pat_ty thing_inside + = tc_lpat pat pat_ty penv thing_inside + where + penv = PE { pe_lazy = False, pe_ctxt = LamPat ctxt } + ----------------- -tc_lam_pats :: [(LPat Name,BoxySigmaType)] - -> (Refinement,BoxyRhoType) -- Result type - -> ((Refinement,BoxyRhoType) -> TcM a) -- Checker for body, given its result type - -> TcM ([LPat TcId], a) -tc_lam_pats pat_ty_prs (reft, res_ty) thing_inside - = do { let init_state = PS { pat_ctxt = LamPat, pat_reft = reft } +data PatEnv + = PE { pe_lazy :: Bool -- True <=> lazy context, so no existentials allowed + , pe_ctxt :: PatCtxt -- Context in which the whole pattern appears + } - ; (pats', ex_tvs, res) <- tcMultiple tc_lpat_pr pat_ty_prs init_state $ \ pstate' -> - refineEnvironment (pat_reft pstate') $ - thing_inside (pat_reft pstate', res_ty) +data PatCtxt + = LamPat -- Used for lambdas, case etc + (HsMatchContext Name) - ; let tys = map snd pat_ty_prs - ; tcCheckExistentialPat pats' ex_tvs tys res_ty + | LetPat -- Used only for let(rec) bindings + -- See Note [Let binders] + TcSigFun -- Tells type sig if any + LetBndrSpec -- True <=> no generalisation of this let - ; returnM (pats', res) } +data LetBndrSpec + = LetLclBndr -- The binder is just a local one; + -- an AbsBinds will provide the global version + | LetGblBndr TcPragFun -- There isn't going to be an AbsBinds; + -- here is the inline-pragma information ------------------ -tcCheckExistentialPat :: [LPat TcId] -- Patterns (just for error message) - -> [TcTyVar] -- Existentially quantified tyvars bound by pattern - -> [BoxySigmaType] -- Types of the patterns - -> BoxyRhoType -- Type of the body of the match - -- Tyvars in either of these must not escape - -> TcM () --- NB: we *must* pass "pats_tys" not just "body_ty" to tcCheckExistentialPat --- For example, we must reject this program: --- data C = forall a. C (a -> Int) --- f (C g) x = g x --- Here, result_ty will be simply Int, but expected_ty is (C -> a -> Int). - -tcCheckExistentialPat pats [] pat_tys body_ty - = return () -- Short cut for case when there are no existentials - -tcCheckExistentialPat pats ex_tvs pat_tys body_ty - = addErrCtxtM (sigPatCtxt (collectPatsBinders pats) ex_tvs pat_tys body_ty) $ - checkSigTyVarsWrt (tcTyVarsOfTypes (body_ty:pat_tys)) ex_tvs - -data PatState = PS { - pat_ctxt :: PatCtxt, - pat_reft :: Refinement -- Binds rigid TcTyVars to their refinements - } - -data PatCtxt - = LamPat - | LetPat (Name -> Maybe TcRhoType) -- Used for let(rec) bindings - -patSigCtxt :: PatState -> UserTypeCtxt -patSigCtxt (PS { pat_ctxt = LetPat _ }) = BindPatSigCtxt -patSigCtxt other = LamPatSigCtxt +makeLazy :: PatEnv -> PatEnv +makeLazy penv = penv { pe_lazy = True } + +patSigCtxt :: PatEnv -> UserTypeCtxt +patSigCtxt (PE { pe_ctxt = LetPat {} }) = BindPatSigCtxt +patSigCtxt (PE { pe_ctxt = LamPat {} }) = LamPatSigCtxt + +--------------- +type TcPragFun = Name -> [LSig Name] +type TcSigFun = Name -> Maybe TcSigInfo + +data TcSigInfo + = TcSigInfo { + sig_id :: TcId, -- *Polymorphic* binder for this value... + + sig_scoped :: [Name], -- Scoped type variables + -- 1-1 correspondence with a prefix of sig_tvs + -- However, may be fewer than sig_tvs; + -- see Note [More instantiated than scoped] + sig_tvs :: [TcTyVar], -- Instantiated type variables + -- See Note [Instantiate sig] + + sig_theta :: TcThetaType, -- Instantiated theta + + sig_tau :: TcSigmaType, -- Instantiated tau + -- See Note [sig_tau may be polymorphic] + + sig_loc :: SrcSpan -- The location of the signature + } + +instance Outputable TcSigInfo where + ppr (TcSigInfo { sig_id = id, sig_tvs = tyvars, sig_theta = theta, sig_tau = tau}) + = ppr id <+> ptext (sLit "::") <+> ppr tyvars <+> pprThetaArrowTy theta <+> ppr tau \end{code} +Note [sig_tau may be polymorphic] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Note that "sig_tau" might actually be a polymorphic type, +if the original function had a signature like + forall a. Eq a => forall b. Ord b => .... +But that's ok: tcMatchesFun (called by tcRhs) can deal with that +It happens, too! See Note [Polymorphic methods] in TcClassDcl. + +Note [Let binders] +~~~~~~~~~~~~~~~~~~ +eg x :: Int + y :: Bool + (x,y) = e + +...more notes to add here.. + + +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) + +If we aren't inside a lazy pattern then we can bind existentials, +but we need to be careful about "extra" tyvars. Consider + (\C x -> d) : pat_ty -> res_ty +When looking for existential escape we must check that the existential +bound by C don't unify with the free variables of pat_ty, OR res_ty +(or of course the environment). Hence we need to keep track of the +res_ty free vars. %************************************************************************ @@ -173,67 +192,109 @@ patSigCtxt other = LamPatSigCtxt %************************************************************************ \begin{code} -tcPatBndr :: PatState -> Name -> BoxySigmaType -> TcM TcId -tcPatBndr (PS { pat_ctxt = LamPat }) bndr_name pat_ty - = do { pat_ty' <- unBoxPatBndrType pat_ty bndr_name - -- We have an undecorated binder, so we do rule ABS1, - -- by unboxing the boxy type, forcing any un-filled-in - -- boxes to become monotypes - -- NB that pat_ty' can still be a polytype: - -- data T = MkT (forall a. a->a) - -- f t = case t of { MkT g -> ... } - -- Here, the 'g' must get type (forall a. a->a) from the - -- MkT context - ; return (mkLocalId bndr_name pat_ty') } - -tcPatBndr (PS { pat_ctxt = LetPat lookup_sig }) bndr_name pat_ty - | Just mono_ty <- lookup_sig bndr_name - = do { mono_name <- newLocalName bndr_name - ; boxyUnify mono_ty pat_ty - ; return (mkLocalId mono_name mono_ty) } - +tcPatBndr :: PatEnv -> Name -> TcSigmaType -> TcM (Coercion, TcId) +-- (coi, xp) = tcPatBndr penv x pat_ty +-- Then coi : pat_ty ~ typeof(xp) +-- +tcPatBndr (PE { pe_ctxt = LetPat lookup_sig no_gen}) bndr_name pat_ty + | Just sig <- lookup_sig bndr_name + = do { bndr_id <- newSigLetBndr no_gen bndr_name sig + ; coi <- unifyPatType (idType bndr_id) pat_ty + ; return (coi, bndr_id) } + | otherwise - = do { pat_ty' <- unBoxPatBndrType pat_ty bndr_name - ; mono_name <- newLocalName bndr_name - ; return (mkLocalId mono_name pat_ty') } + = do { bndr_id <- newNoSigLetBndr no_gen bndr_name pat_ty + ; return (mkReflCo pat_ty, bndr_id) } + +tcPatBndr (PE { pe_ctxt = _lam_or_proc }) bndr_name pat_ty + = do { bndr <- mkLocalBinder bndr_name pat_ty + ; return (mkReflCo pat_ty, bndr) } + +------------ +newSigLetBndr :: LetBndrSpec -> Name -> TcSigInfo -> TcM TcId +newSigLetBndr LetLclBndr name sig + = do { mono_name <- newLocalName name + ; mkLocalBinder mono_name (sig_tau sig) } +newSigLetBndr (LetGblBndr prags) name sig + = addInlinePrags (sig_id sig) (prags name) + +------------ +newNoSigLetBndr :: LetBndrSpec -> Name -> TcType -> TcM TcId +-- In the polymorphic case (no_gen = False), generate a "monomorphic version" +-- of the Id; the original name will be bound to the polymorphic version +-- by the AbsBinds +-- In the monomorphic case there is no AbsBinds, and we use the original +-- name directly +newNoSigLetBndr LetLclBndr name ty + =do { mono_name <- newLocalName name + ; mkLocalBinder mono_name ty } +newNoSigLetBndr (LetGblBndr prags) name ty + = do { id <- mkLocalBinder name ty + ; addInlinePrags id (prags name) } + +---------- +addInlinePrags :: TcId -> [LSig Name] -> TcM TcId +addInlinePrags poly_id prags + = tc_inl inl_sigs + where + inl_sigs = filter isInlineLSig prags + tc_inl [] = return poly_id + tc_inl (L loc (InlineSig _ prag) : other_inls) + = do { unless (null other_inls) (setSrcSpan loc warn_dup_inline) + ; return (poly_id `setInlinePragma` prag) } + tc_inl _ = panic "tc_inl" + + warn_dup_inline = warnPrags poly_id inl_sigs $ + ptext (sLit "Duplicate INLINE pragmas for") + +warnPrags :: Id -> [LSig Name] -> SDoc -> TcM () +warnPrags id bad_sigs herald + = addWarnTc (hang (herald <+> quotes (ppr id)) + 2 (ppr_sigs bad_sigs)) + where + ppr_sigs sigs = vcat (map (ppr . getLoc) sigs) +----------------- +mkLocalBinder :: Name -> TcType -> TcM TcId +mkLocalBinder name ty + = do { checkUnboxedTuple ty $ + ptext (sLit "The variable") <+> quotes (ppr name) + ; return (Id.mkLocalId name ty) } + +checkUnboxedTuple :: TcType -> SDoc -> TcM () +-- Check for an unboxed tuple type +-- f = (# True, False #) +-- Zonk first just in case it's hidden inside a meta type variable +-- (This shows up as a (more obscure) kind error +-- in the 'otherwise' case of tcMonoBinds.) +checkUnboxedTuple ty what + = do { zonked_ty <- zonkTcTypeCarefully ty + ; checkTc (not (isUnboxedTupleType zonked_ty)) + (unboxedTupleErr what zonked_ty) } ------------------- -bindInstsOfPatId :: TcId -> TcM a -> TcM (a, LHsBinds TcId) +{- Only needed if we re-add Method constraints +bindInstsOfPatId :: TcId -> TcM a -> TcM (a, TcEvBinds) bindInstsOfPatId id thing_inside | not (isOverloadedTy (idType id)) - = do { res <- thing_inside; return (res, emptyLHsBinds) } + = do { res <- thing_inside; return (res, emptyTcEvBinds) } | otherwise - = do { (res, lie) <- getLIE thing_inside - ; binds <- bindInstsOfLocalFuns lie [id] + = do { (res, lie) <- captureConstraints thing_inside + ; binds <- bindLocalMethods lie [id] ; return (res, binds) } - -------------------- -unBoxPatBndrType ty name = unBoxArgType ty (ptext SLIT("The variable") <+> quotes (ppr name)) -unBoxWildCardType ty = unBoxArgType ty (ptext SLIT("A wild-card pattern")) - -unBoxArgType :: BoxyType -> SDoc -> TcM TcType --- In addition to calling unbox, unBoxArgType ensures that the type is of ArgTypeKind; --- that is, it can't be an unboxed tuple. For example, --- case (f x) of r -> ... --- should fail if 'f' returns an unboxed tuple. -unBoxArgType ty pp_this - = do { ty' <- unBox ty -- Returns a zonked type - - -- Neither conditional is strictly necesssary (the unify alone will do) - -- but they improve error messages, and allocate fewer tyvars - ; if isUnboxedTupleType ty' then - failWithTc msg - else if isArgTypeKind (typeKind ty') then - return ty' - else do -- OpenTypeKind, so constrain it - { ty2 <- newFlexiTyVarTy argTypeKind - ; unifyType ty' ty2 - ; return ty' }} - where - msg = pp_this <+> ptext SLIT("cannot be bound to an unboxed tuple") +-} \end{code} +Note [Polymorphism and pattern bindings] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +When is_mono holds we are not generalising +But the signature can still be polymoprhic! + data T = MkT (forall a. a->a) + x :: forall a. a->a + MkT x = +So the no_gen flag decides whether the pattern-bound variables should +have exactly the type in the type signature (when not generalising) or +the instantiated version (when generalising) %************************************************************************ %* * @@ -243,129 +304,117 @@ unBoxArgType ty pp_this Note [Nesting] ~~~~~~~~~~~~~~ -tcPat takes a "thing inside" over which the patter scopes. This is partly +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 tc_lpats. +Hence the getErrCtxt/setErrCtxt stuff in tcMultiple \begin{code} -------------------- type Checker inp out = forall r. inp - -> PatState - -> (PatState -> TcM r) - -> TcM (out, [TcTyVar], r) + -> PatEnv + -> TcM r + -> TcM (out, r) tcMultiple :: Checker inp out -> Checker [inp] [out] -tcMultiple tc_pat args pstate thing_inside +tcMultiple tc_pat args penv thing_inside = do { err_ctxt <- getErrCtxt - ; let loop pstate [] - = do { res <- thing_inside pstate - ; return ([], [], res) } + ; let loop _ [] + = do { res <- thing_inside + ; return ([], res) } - loop pstate (arg:args) - = do { (p', p_tvs, (ps', ps_tvs, res)) - <- tc_pat arg pstate $ \ pstate' -> + loop penv (arg:args) + = do { (p', (ps', res)) + <- tc_pat arg penv $ setErrCtxt err_ctxt $ - loop pstate' args + loop penv args -- setErrCtxt: restore context before doing the next pattern -- See note [Nesting] above - ; return (p':ps', p_tvs ++ ps_tvs, res) } + ; return (p':ps', res) } - ; loop pstate args } + ; loop penv args } -------------------- -tc_lpat_pr :: (LPat Name, BoxySigmaType) - -> PatState - -> (PatState -> TcM a) - -> TcM (LPat TcId, [TcTyVar], a) -tc_lpat_pr (pat, ty) = tc_lpat pat ty - tc_lpat :: LPat Name - -> BoxySigmaType - -> PatState - -> (PatState -> TcM a) - -> TcM (LPat TcId, [TcTyVar], a) -tc_lpat (L span pat) pat_ty pstate thing_inside - = setSrcSpan span $ - maybeAddErrCtxt (patCtxt pat) $ - do { let (coercion, pat_ty') = refineType (pat_reft pstate) pat_ty - -- Make sure the result type reflects the current refinement - -- We must do this here, so that it correctly ``sees'' all - -- the refinements to the left. Example: - -- Suppose C :: forall a. T a -> a -> Foo - -- Pattern C a p1 True - -- So p1 might refine 'a' to True, and the True - -- pattern had better see it. - - ; (pat', tvs, res) <- tc_pat pstate pat pat_ty' thing_inside - ; return (mkCoPat coercion (L span pat') pat_ty, tvs, res) } + -> TcSigmaType + -> PatEnv + -> TcM a + -> TcM (LPat TcId, a) +tc_lpat (L span pat) pat_ty penv thing_inside + = setSrcSpan span $ + do { (pat', res) <- maybeWrapPatCtxt pat (tc_pat penv pat pat_ty) + thing_inside + ; return (L span pat', res) } + +tc_lpats :: PatEnv + -> [LPat Name] -> [TcSigmaType] + -> TcM a + -> TcM ([LPat TcId], a) +tc_lpats penv pats tys thing_inside + = tcMultiple (\(p,t) -> tc_lpat p t) + (zipEqual "tc_lpats" pats tys) + penv thing_inside -------------------- -tc_pat :: PatState - -> Pat Name -> BoxySigmaType -- Fully refined result type - -> (PatState -> TcM a) -- Thing inside - -> TcM (Pat TcId, -- Translated pattern - [TcTyVar], -- Existential binders - a) -- Result of thing inside - -tc_pat pstate (VarPat name) pat_ty thing_inside - = do { id <- tcPatBndr pstate name pat_ty - ; (res, binds) <- bindInstsOfPatId id $ - tcExtendIdEnv1 name id $ - (traceTc (text "binding" <+> ppr name <+> ppr (idType id)) - >> thing_inside pstate) - ; let pat' | isEmptyLHsBinds binds = VarPat id - | otherwise = VarPatOut id binds - ; return (pat', [], res) } - -tc_pat pstate (ParPat pat) pat_ty thing_inside - = do { (pat', tvs, res) <- tc_lpat pat pat_ty pstate thing_inside - ; return (ParPat pat', tvs, res) } - -tc_pat pstate (BangPat pat) pat_ty thing_inside - = do { (pat', tvs, res) <- tc_lpat pat pat_ty pstate thing_inside - ; return (BangPat pat', tvs, res) } - --- There's a wrinkle with irrefutable patterns, namely that we --- must not propagate type refinement from them. For example --- data T a where { T1 :: Int -> T Int; ... } --- f :: T a -> Int -> a --- f ~(T1 i) y = y --- It's obviously not sound to refine a to Int in the right --- hand side, because the arugment might not match T1 at all! --- --- Nor should a lazy pattern bind any existential type variables --- because they won't be in scope when we do the desugaring -tc_pat pstate lpat@(LazyPat pat) pat_ty thing_inside - = do { (pat', pat_tvs, res) <- tc_lpat pat pat_ty pstate $ \ _ -> - thing_inside pstate - -- Ignore refined pstate', - -- revert to pstate - -- Check no existentials - ; if (null pat_tvs) then return () - else lazyPatErr lpat pat_tvs - - -- Check that the pattern has a lifted type - ; pat_tv <- newBoxyTyVar liftedTypeKind - ; boxyUnify pat_ty (mkTyVarTy pat_tv) - - ; return (LazyPat pat', [], res) } - -tc_pat pstate (WildPat _) pat_ty thing_inside - = do { pat_ty' <- unBoxWildCardType pat_ty -- Make sure it's filled in with monotypes - ; res <- thing_inside pstate - ; return (WildPat pat_ty', [], res) } - -tc_pat pstate (AsPat (L nm_loc name) pat) pat_ty thing_inside - = do { bndr_id <- setSrcSpan nm_loc (tcPatBndr pstate name pat_ty) - ; (pat', tvs, res) <- tcExtendIdEnv1 name bndr_id $ - tc_lpat pat (idType bndr_id) pstate thing_inside +tc_pat :: PatEnv + -> Pat Name + -> TcSigmaType -- Fully refined result type + -> TcM a -- Thing inside + -> TcM (Pat TcId, -- Translated pattern + a) -- Result of thing inside + +tc_pat penv (VarPat name) pat_ty thing_inside + = do { (coi, id) <- tcPatBndr penv name pat_ty + ; res <- tcExtendIdEnv1 name id thing_inside + ; return (mkHsWrapPatCo coi (VarPat id) pat_ty, res) } + +tc_pat penv (ParPat pat) pat_ty thing_inside + = do { (pat', res) <- tc_lpat pat pat_ty penv thing_inside + ; return (ParPat pat', res) } + +tc_pat penv (BangPat pat) pat_ty thing_inside + = do { (pat', res) <- tc_lpat pat pat_ty penv thing_inside + ; return (BangPat pat', res) } + +tc_pat penv lpat@(LazyPat pat) pat_ty thing_inside + = do { (pat', (res, pat_ct)) + <- tc_lpat pat pat_ty (makeLazy penv) $ + captureConstraints thing_inside + -- Ignore refined penv', revert to penv + + ; emitConstraints pat_ct + -- captureConstraints/extendConstraints: + -- see Note [Hopping the LIE in lazy patterns] + + -- Check there are no unlifted types under the lazy pattern + ; when (any (isUnLiftedType . idType) $ collectPatBinders pat') $ + lazyUnliftedPatErr lpat + + -- Check that the expected pattern type is itself lifted + ; pat_ty' <- newFlexiTyVarTy liftedTypeKind + ; _ <- unifyType pat_ty pat_ty' + + ; return (LazyPat pat', res) } + +tc_pat _ p@(QuasiQuotePat _) _ _ + = pprPanic "Should never see QuasiQuotePat in type checker" (ppr p) + +tc_pat _ (WildPat _) pat_ty thing_inside + = do { checkUnboxedTuple pat_ty $ + ptext (sLit "A wild-card pattern") + ; res <- thing_inside + ; return (WildPat pat_ty, res) } + +tc_pat penv (AsPat (L nm_loc name) pat) pat_ty thing_inside + = do { (coi, bndr_id) <- setSrcSpan nm_loc (tcPatBndr penv name pat_ty) + ; (pat', res) <- tcExtendIdEnv1 name bndr_id $ + tc_lpat pat (idType bndr_id) penv thing_inside -- NB: if we do inference on: -- \ (y@(x::forall a. a->a)) = e -- we'll fail. The as-pattern infers a monotype for 'y', which then @@ -373,70 +422,99 @@ tc_pat pstate (AsPat (L nm_loc name) pat) pat_ty thing_inside -- perhaps be fixed, but only with a bit more work. -- -- If you fix it, don't forget the bindInstsOfPatIds! - ; return (AsPat (L nm_loc bndr_id) pat', tvs, res) } + ; return (mkHsWrapPatCo coi (AsPat (L nm_loc bndr_id) pat') pat_ty, res) } + +tc_pat penv vpat@(ViewPat expr pat _) overall_pat_ty thing_inside + = do { checkUnboxedTuple overall_pat_ty $ + ptext (sLit "The view pattern") <+> ppr vpat + + -- Morally, expr must have type `forall a1...aN. OPT' -> B` + -- where overall_pat_ty is an instance of OPT'. + -- Here, we infer a rho type for it, + -- which replaces the leading foralls and constraints + -- with fresh unification variables. + ; (expr',expr'_inferred) <- tcInferRho expr + + -- next, we check that expr is coercible to `overall_pat_ty -> pat_ty` + -- NOTE: this forces pat_ty to be a monotype (because we use a unification + -- variable to find it). this means that in an example like + -- (view -> f) where view :: _ -> forall b. b + -- we will only be able to use view at one instantation in the + -- rest of the view + ; (expr_coi, pat_ty) <- tcInfer $ \ pat_ty -> + unifyPatType expr'_inferred (mkFunTy overall_pat_ty pat_ty) + + -- pattern must have pat_ty + ; (pat', res) <- tc_lpat pat pat_ty penv thing_inside + + ; return (ViewPat (mkLHsWrapCo expr_coi expr') pat' overall_pat_ty, res) } -- Type signatures in patterns -- See Note [Pattern coercions] below -tc_pat pstate (SigPatIn pat sig_ty) pat_ty thing_inside - = do { (inner_ty, tv_binds) <- tcPatSig (patSigCtxt pstate) sig_ty pat_ty - ; (pat', tvs, res) <- tcExtendTyVarEnv2 tv_binds $ - tc_lpat pat inner_ty pstate thing_inside - ; return (SigPatOut pat' inner_ty, tvs, res) } +tc_pat penv (SigPatIn pat sig_ty) pat_ty thing_inside + = do { (inner_ty, tv_binds, wrap) <- tcPatSig (patSigCtxt penv) sig_ty pat_ty + ; (pat', res) <- tcExtendTyVarEnv2 tv_binds $ + tc_lpat pat inner_ty penv thing_inside -tc_pat pstate pat@(TypePat ty) pat_ty thing_inside - = failWithTc (badTypePat pat) + ; return (mkHsWrapPat wrap (SigPatOut pat' inner_ty) pat_ty, res) } ------------------------ -- Lists, tuples, arrays -tc_pat pstate (ListPat pats _) pat_ty thing_inside - = do { elt_ty <- boxySplitListTy pat_ty - ; (pats', pats_tvs, res) <- tcMultiple (\p -> tc_lpat p elt_ty) - pats pstate thing_inside - ; return (ListPat pats' elt_ty, pats_tvs, res) } - -tc_pat pstate (PArrPat pats _) pat_ty thing_inside - = do { [elt_ty] <- boxySplitTyConApp parrTyCon pat_ty - ; (pats', pats_tvs, res) <- tcMultiple (\p -> tc_lpat p elt_ty) - pats pstate thing_inside - ; ifM (null pats) (zapToMonotype pat_ty) -- c.f. ExplicitPArr in TcExpr - ; return (PArrPat pats' elt_ty, pats_tvs, res) } - -tc_pat pstate (TuplePat pats boxity _) pat_ty thing_inside - = do { arg_tys <- boxySplitTyConApp (tupleTyCon boxity (length pats)) pat_ty - ; (pats', pats_tvs, res) <- tcMultiple tc_lpat_pr (pats `zip` arg_tys) - pstate thing_inside +tc_pat penv (ListPat pats _) pat_ty thing_inside + = do { (coi, elt_ty) <- matchExpectedPatTy matchExpectedListTy pat_ty + ; (pats', res) <- tcMultiple (\p -> tc_lpat p elt_ty) + pats penv thing_inside + ; return (mkHsWrapPat coi (ListPat pats' elt_ty) pat_ty, res) + } + +tc_pat penv (PArrPat pats _) pat_ty thing_inside + = do { (coi, elt_ty) <- matchExpectedPatTy matchExpectedPArrTy pat_ty + ; (pats', res) <- tcMultiple (\p -> tc_lpat p elt_ty) + pats penv thing_inside + ; return (mkHsWrapPat coi (PArrPat pats' elt_ty) pat_ty, res) + } + +tc_pat penv (TuplePat pats boxity _) pat_ty thing_inside + = do { let tc = tupleTyCon boxity (length pats) + ; (coi, arg_tys) <- matchExpectedPatTy (matchExpectedTyConApp tc) pat_ty + ; (pats', res) <- tc_lpats penv pats arg_tys thing_inside -- 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 pats' boxity pat_ty + ; let pat_ty' = mkTyConApp tc arg_tys + -- pat_ty /= pat_ty iff coi /= IdCo + unmangled_result = TuplePat pats' boxity pat_ty' possibly_mangled_result - | opt_IrrefutableTuples && isBoxed boxity = LazyPat (noLoc unmangled_result) - | otherwise = unmangled_result + | opt_IrrefutableTuples && + isBoxed boxity = LazyPat (noLoc unmangled_result) + | otherwise = unmangled_result - ; ASSERT( length arg_tys == length pats ) -- Syntactically enforced - return (possibly_mangled_result, pats_tvs, res) } + ; ASSERT( length arg_tys == length pats ) -- Syntactically enforced + return (mkHsWrapPat coi possibly_mangled_result pat_ty, res) + } ------------------------ -- Data constructors -tc_pat pstate pat_in@(ConPatIn (L con_span con_name) arg_pats) pat_ty thing_inside - = do { data_con <- tcLookupDataCon con_name - ; let tycon = dataConTyCon data_con - ; tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside } +tc_pat penv (ConPatIn con arg_pats) pat_ty thing_inside + = tcConPat penv con pat_ty arg_pats thing_inside ------------------------ -- Literal patterns -tc_pat pstate (LitPat simple_lit) pat_ty thing_inside - = do { boxyUnify (hsLitType simple_lit) pat_ty - ; res <- thing_inside pstate - ; returnM (LitPat simple_lit, [], res) } +tc_pat _ (LitPat simple_lit) pat_ty thing_inside + = do { let lit_ty = hsLitType simple_lit + ; coi <- unifyPatType lit_ty pat_ty + -- coi is of kind: pat_ty ~ lit_ty + ; res <- thing_inside + ; return ( mkHsWrapPatCo coi (LitPat simple_lit) pat_ty + , res) } ------------------------ -- Overloaded patterns: n, and n+k -tc_pat pstate pat@(NPat over_lit mb_neg eq _) pat_ty thing_inside +tc_pat _ (NPat over_lit mb_neg eq) pat_ty thing_inside = do { let orig = LiteralOrigin over_lit - ; lit' <- tcOverloadedLit orig over_lit pat_ty + ; lit' <- newOverloadedLit orig over_lit pat_ty ; eq' <- tcSyntaxOp orig eq (mkFunTys [pat_ty, pat_ty] boolTy) ; mb_neg' <- case mb_neg of Nothing -> return Nothing -- Positive literal @@ -444,31 +522,63 @@ tc_pat pstate pat@(NPat over_lit mb_neg eq _) pat_ty thing_inside -- The 'negate' is re-mappable syntax do { neg' <- tcSyntaxOp orig neg (mkFunTy pat_ty pat_ty) ; return (Just neg') } - ; res <- thing_inside pstate - ; returnM (NPat lit' mb_neg' eq' pat_ty, [], res) } + ; res <- thing_inside + ; return (NPat lit' mb_neg' eq', res) } -tc_pat pstate pat@(NPlusKPat (L nm_loc name) lit ge minus) pat_ty thing_inside - = do { bndr_id <- setSrcSpan nm_loc (tcPatBndr pstate name pat_ty) +tc_pat penv (NPlusKPat (L nm_loc name) lit ge minus) pat_ty thing_inside + = do { (coi, bndr_id) <- setSrcSpan nm_loc (tcPatBndr penv name pat_ty) ; let pat_ty' = idType bndr_id orig = LiteralOrigin lit - ; lit' <- tcOverloadedLit orig lit pat_ty' + ; lit' <- newOverloadedLit orig lit pat_ty' -- The '>=' and '-' parts are re-mappable syntax ; ge' <- tcSyntaxOp orig ge (mkFunTys [pat_ty', pat_ty'] boolTy) ; minus' <- tcSyntaxOp orig minus (mkFunTys [pat_ty', pat_ty'] pat_ty') + ; let pat' = NPlusKPat (L nm_loc bndr_id) lit' ge' minus' -- The Report says that n+k patterns must be in Integral -- We may not want this when using re-mappable syntax, though (ToDo?) ; icls <- tcLookupClass integralClassName - ; dicts <- newDicts orig [mkClassPred icls [pat_ty']] - ; extendLIEs dicts + ; instStupidTheta orig [mkClassPred icls [pat_ty']] - ; res <- tcExtendIdEnv1 name bndr_id (thing_inside pstate) - ; returnM (NPlusKPat (L nm_loc bndr_id) lit' ge' minus', [], res) } - -tc_pat _ _other_pat _ _ = panic "tc_pat" -- DictPat, ConPatOut, SigPatOut, VarPatOut + ; res <- tcExtendIdEnv1 name bndr_id thing_inside + ; return (mkHsWrapPatCo coi pat' pat_ty, res) } + +tc_pat _ _other_pat _ _ = panic "tc_pat" -- ConPatOut, SigPatOut + +---------------- +unifyPatType :: TcType -> TcType -> TcM Coercion +-- In patterns we want a coercion from the +-- context type (expected) to the actual pattern type +-- But we don't want to reverse the args to unifyType because +-- that controls the actual/expected stuff in error messages +unifyPatType actual_ty expected_ty + = do { coi <- unifyType actual_ty expected_ty + ; return (mkSymCo coi) } \end{code} +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 arugment 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 + %************************************************************************ %* * @@ -477,81 +587,248 @@ tc_pat _ _other_pat _ _ = panic "tc_pat" -- DictPat, ConPatOut, SigPatOut, VarP %* * %************************************************************************ +[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 MkIds.lhs, 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. + \begin{code} -- Running example: --- MkT :: forall a b c. (a:=:[b]) => b -> c -> T a +-- MkT :: forall a b c. (a~[b]) => b -> c -> T a -- with scrutinee of type (T ty) -tcConPat :: PatState -> SrcSpan -> DataCon -> TyCon - -> BoxySigmaType -- Type of the pattern - -> HsConDetails Name (LPat Name) -> (PatState -> TcM a) - -> TcM (Pat TcId, [TcTyVar], a) -tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside - = do { span <- getSrcSpanM -- Span for the whole pattern - ; let (univ_tvs, ex_tvs, eq_spec, theta, arg_tys) = dataConFullSig data_con - skol_info = PatSkol data_con span +tcConPat :: PatEnv -> Located Name + -> TcRhoType -- Type of the pattern + -> HsConPatDetails Name -> TcM a + -> TcM (Pat TcId, a) +tcConPat penv (L con_span con_name) pat_ty arg_pats thing_inside + = do { data_con <- tcLookupDataCon con_name + ; let tycon = dataConTyCon data_con + -- For data families this is the representation tycon + (univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _) + = dataConFullSig data_con -- Instantiate the constructor type variables [a->ty] - ; ctxt_res_tys <- boxySplitTyConApp tycon pat_ty - ; ex_tvs' <- tcInstSkolTyVars skol_info ex_tvs - ; let tenv = zipTopTvSubst (univ_tvs ++ ex_tvs) - (ctxt_res_tys ++ mkTyVarTys ex_tvs') - eq_spec' = substEqSpec tenv eq_spec - theta' = substTheta tenv theta - arg_tys' = substTys tenv arg_tys - - ; co_vars <- newCoVars eq_spec' -- Make coercion variables - ; pstate' <- refineAlt data_con pstate ex_tvs co_vars pat_ty - - ; ((arg_pats', inner_tvs, res), lie_req) <- getLIE $ - tcConArgs data_con arg_tys' arg_pats pstate' thing_inside - - ; dicts <- newDicts (SigOrigin skol_info) theta' - ; dict_binds <- tcSimplifyCheck doc ex_tvs' dicts lie_req - - ; tcInstStupidTheta data_con ctxt_res_tys - - ; return (ConPatOut { pat_con = L con_span data_con, - pat_tvs = ex_tvs' ++ co_vars, - pat_dicts = map instToId dicts, pat_binds = dict_binds, - pat_args = arg_pats', pat_ty = pat_ty }, - ex_tvs' ++ inner_tvs, res) - } + -- This may involve doing a family-instance coercion, + -- and building a wrapper + ; (wrap, ctxt_res_tys) <- matchExpectedPatTy (matchExpectedConTy tycon) pat_ty + + -- Add the stupid theta + ; setSrcSpan con_span $ addDataConStupidTheta data_con ctxt_res_tys + + ; checkExistentials ex_tvs penv + ; ex_tvs' <- tcInstSuperSkolTyVars 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 + + tenv = zipTopTvSubst (univ_tvs ++ ex_tvs) + (ctxt_res_tys ++ mkTyVarTys ex_tvs') + arg_tys' = substTys tenv arg_tys + + ; if null ex_tvs && null eq_spec && null theta + then do { -- The common case; no class bindings etc + -- (see Note [Arrows and patterns]) + (arg_pats', res) <- tcConArgs data_con arg_tys' + arg_pats penv thing_inside + ; let res_pat = ConPatOut { pat_con = L con_span data_con, + pat_tvs = [], pat_dicts = [], + pat_binds = emptyTcEvBinds, + pat_args = arg_pats', + pat_ty = pat_ty' } + + ; return (mkHsWrapPat wrap res_pat pat_ty, res) } + + else do -- The general case, with existential, + -- and local equality constraints + { let theta' = substTheta tenv (eqSpecPreds eq_spec ++ theta) + -- order is *important* as we generate the list of + -- dictionary binders from theta' + no_equalities = not (any isEqPred theta') + skol_info = case pe_ctxt penv of + LamPat mc -> PatSkol data_con mc + LetPat {} -> UnkSkol -- Doesn't matter + + ; gadts_on <- xoptM Opt_GADTs + ; checkTc (no_equalities || gadts_on) + (ptext (sLit "A pattern match on a GADT requires -XGADTs")) + -- Trac #2905 decided that a *pattern-match* of a GADT + -- should require the GADT language flag + + ; given <- newEvVars theta' + ; (ev_binds, (arg_pats', res)) + <- checkConstraints skol_info ex_tvs' given $ + tcConArgs data_con arg_tys' arg_pats penv thing_inside + + ; let res_pat = ConPatOut { pat_con = L con_span data_con, + pat_tvs = ex_tvs', + pat_dicts = given, + pat_binds = ev_binds, + pat_args = arg_pats', + pat_ty = pat_ty' } + ; return (mkHsWrapPat wrap res_pat pat_ty, res) + } } + +---------------------------- +matchExpectedPatTy :: (TcRhoType -> TcM (Coercion, a)) + -> TcRhoType -> TcM (HsWrapper, a) +-- See Note [Matching polytyped patterns] +-- Returns a wrapper : pat_ty ~ inner_ty +matchExpectedPatTy inner_match pat_ty + | null tvs && null theta + = do { (coi, res) <- inner_match pat_ty + ; return (coToHsWrapper (mkSymCo coi), res) } + -- The Sym is because the inner_match returns a coercion + -- that is the other way round to matchExpectedPatTy + + | otherwise + = do { (_, tys, subst) <- tcInstTyVars tvs + ; wrap1 <- instCall PatOrigin tys (substTheta subst theta) + ; (wrap2, arg_tys) <- matchExpectedPatTy inner_match (TcType.substTy subst tau) + ; return (wrap2 <.> wrap1 , arg_tys) } where - doc = ptext SLIT("existential context for") <+> quotes (ppr data_con) + (tvs, theta, tau) = tcSplitSigmaTy pat_ty + +---------------------------- +matchExpectedConTy :: TyCon -- The TyCon that this data + -- constructor actually returns + -> TcRhoType -- The type of the pattern + -> TcM (Coercion, [TcSigmaType]) +-- See Note [Matching constructor patterns] +-- Returns a coercion : T ty1 ... tyn ~ pat_ty +-- This is the same way round as matchExpectedListTy etc +-- but the other way round to matchExpectedPatTy +matchExpectedConTy data_tc pat_ty + | Just (fam_tc, fam_args, co_tc) <- tyConFamInstSig_maybe data_tc + -- Comments refer to Note [Matching constructor patterns] + -- co_tc :: forall a. T [a] ~ T7 a + = do { (_, tys, subst) <- tcInstTyVars (tyConTyVars data_tc) + -- tys = [ty1,ty2] + + ; coi1 <- unifyType (mkTyConApp fam_tc (substTys subst fam_args)) pat_ty + -- coi1 : T (ty1,ty2) ~ pat_ty + + ; let coi2 = mkAxInstCo co_tc tys + -- coi2 : T (ty1,ty2) ~ T7 ty1 ty2 + + ; return (mkTransCo (mkSymCo coi2) coi1, tys) } + | otherwise + = matchExpectedTyConApp data_tc pat_ty + -- coi : T tys ~ pat_ty +\end{code} + +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 + +\begin{code} tcConArgs :: DataCon -> [TcSigmaType] - -> Checker (HsConDetails Name (LPat Name)) (HsConDetails Id (LPat Id)) + -> Checker (HsConPatDetails Name) (HsConPatDetails Id) -tcConArgs data_con arg_tys (PrefixCon arg_pats) pstate thing_inside +tcConArgs data_con arg_tys (PrefixCon arg_pats) penv thing_inside = do { checkTc (con_arity == no_of_args) -- Check correct arity (arityErr "Constructor" data_con con_arity no_of_args) ; let pats_w_tys = zipEqual "tcConArgs" arg_pats arg_tys - ; (arg_pats', tvs, res) <- tcMultiple tcConArg pats_w_tys - pstate thing_inside - ; return (PrefixCon arg_pats', tvs, res) } + ; (arg_pats', res) <- tcMultiple tcConArg pats_w_tys + penv thing_inside + ; return (PrefixCon arg_pats', res) } where con_arity = dataConSourceArity data_con no_of_args = length arg_pats -tcConArgs data_con [arg_ty1,arg_ty2] (InfixCon p1 p2) pstate thing_inside +tcConArgs data_con arg_tys (InfixCon p1 p2) penv thing_inside = do { checkTc (con_arity == 2) -- Check correct arity (arityErr "Constructor" data_con con_arity 2) - ; ([p1',p2'], tvs, res) <- tcMultiple tcConArg [(p1,arg_ty1),(p2,arg_ty2)] - pstate thing_inside - ; return (InfixCon p1' p2', tvs, res) } + ; let [arg_ty1,arg_ty2] = arg_tys -- This can't fail after the arity check + ; ([p1',p2'], res) <- tcMultiple tcConArg [(p1,arg_ty1),(p2,arg_ty2)] + penv thing_inside + ; return (InfixCon p1' p2', res) } where con_arity = dataConSourceArity data_con -tcConArgs data_con arg_tys (RecCon rpats) pstate thing_inside - = do { (rpats', tvs, res) <- tcMultiple tc_field rpats pstate thing_inside - ; return (RecCon rpats', tvs, res) } +tcConArgs data_con arg_tys (RecCon (HsRecFields rpats dd)) penv thing_inside + = do { (rpats', res) <- tcMultiple tc_field rpats penv thing_inside + ; return (RecCon (HsRecFields rpats' dd), res) } where - tc_field :: Checker (Located Name, LPat Name) (Located TcId, LPat TcId) - tc_field (field_lbl, pat) pstate thing_inside + tc_field :: Checker (HsRecField FieldLabel (LPat Name)) (HsRecField TcId (LPat TcId)) + tc_field (HsRecField field_lbl pat pun) penv thing_inside = do { (sel_id, pat_ty) <- wrapLocFstM find_field_ty field_lbl - ; (pat', tvs, res) <- tcConArg (pat, pat_ty) pstate thing_inside - ; return ((sel_id, pat'), tvs, res) } + ; (pat', res) <- tcConArg (pat, pat_ty) penv thing_inside + ; return (HsRecField sel_id pat' pun, res) } find_field_ty :: FieldLabel -> TcM (Id, TcType) find_field_ty field_lbl @@ -581,124 +858,52 @@ tcConArgs data_con arg_tys (RecCon rpats) pstate thing_inside -- dataConFieldLabels will be empty (and each field in the pattern -- will generate an error below). -tcConArg :: Checker (LPat Name, BoxySigmaType) (LPat Id) -tcConArg (arg_pat, arg_ty) pstate thing_inside - = tc_lpat arg_pat arg_ty pstate thing_inside - -- NB: the tc_lpat will refine pat_ty if necessary - -- based on the current pstate, which may include - -- refinements from peer argument patterns to the left +tcConArg :: Checker (LPat Name, TcSigmaType) (LPat Id) +tcConArg (arg_pat, arg_ty) penv thing_inside + = tc_lpat arg_pat arg_ty penv thing_inside \end{code} - -%************************************************************************ -%* * - Type refinement -%* * -%************************************************************************ - \begin{code} -refineAlt :: DataCon -- For tracing only - -> PatState - -> [TcTyVar] -- Existentials - -> [CoVar] -- Equational constraints - -> BoxySigmaType -- Pattern type - -> TcM PatState - -refineAlt con pstate ex_tvs [] pat_ty - = return pstate -- Common case: no equational constraints - -refineAlt con pstate ex_tvs co_vars pat_ty - | not (isRigidTy pat_ty) - = failWithTc (nonRigidMatch con) - -- We are matching against a GADT constructor with non-trivial - -- constraints, but pattern type is wobbly. For now we fail. - -- We can make sense of this, however: - -- Suppose MkT :: forall a b. (a:=:[b]) => b -> T a - -- (\x -> case x of { MkT v -> v }) - -- We can infer that x must have type T [c], for some wobbly 'c' - -- and translate to - -- (\(x::T [c]) -> case x of - -- MkT b (g::([c]:=:[b])) (v::b) -> v `cast` sym g - -- To implement this, we'd first instantiate the equational - -- constraints with *wobbly* type variables for the existentials; - -- then unify these constraints to make pat_ty the right shape; - -- then proceed exactly as in the rigid case - - | otherwise -- In the rigid case, we perform type refinement - = case gadtRefine (pat_reft pstate) ex_tvs co_vars of { - Failed msg -> failWithTc (inaccessibleAlt msg) ; - Succeeded reft -> do { traceTc trace_msg - ; return (pstate { pat_reft = reft }) } - -- DO NOT refine the envt right away, because we - -- might be inside a lazy pattern. Instead, refine pstate - where - - trace_msg = text "refineAlt:match" <+> ppr con <+> ppr reft - } -\end{code} - - -%************************************************************************ -%* * - Overloaded literals -%* * -%************************************************************************ - -In tcOverloadedLit we convert directly to an Int or Integer if we -know that's what we want. This may save some time, by not -temporarily generating overloaded literals, but it won't catch all -cases (the rest are caught in lookupInst). - -\begin{code} -tcOverloadedLit :: InstOrigin - -> HsOverLit Name - -> BoxyRhoType - -> TcM (HsOverLit TcId) -tcOverloadedLit orig lit@(HsIntegral i fi) res_ty - | not (fi `isHsVar` fromIntegerName) -- Do not generate a LitInst for rebindable syntax. - -- Reason: If we do, tcSimplify will call lookupInst, which - -- will call tcSyntaxName, which does unification, - -- which tcSimplify doesn't like - -- ToDo: noLoc sadness - = do { integer_ty <- tcMetaTy integerTyConName - ; fi' <- tcSyntaxOp orig fi (mkFunTy integer_ty res_ty) - ; return (HsIntegral i (HsApp (noLoc fi') (nlHsLit (HsInteger i integer_ty)))) } - - | Just expr <- shortCutIntLit i res_ty - = return (HsIntegral i expr) - - | otherwise - = do { expr <- newLitInst orig lit res_ty - ; return (HsIntegral i expr) } - -tcOverloadedLit orig lit@(HsFractional r fr) res_ty - | not (fr `isHsVar` fromRationalName) -- c.f. HsIntegral case - = do { rat_ty <- tcMetaTy rationalTyConName - ; fr' <- tcSyntaxOp orig fr (mkFunTy rat_ty res_ty) - -- Overloaded literals must have liftedTypeKind, because - -- we're instantiating an overloaded function here, - -- whereas res_ty might be openTypeKind. This was a bug in 6.2.2 - -- However this'll be picked up by tcSyntaxOp if necessary - ; return (HsFractional r (HsApp (noLoc fr') (nlHsLit (HsRat r rat_ty)))) } - - | Just expr <- shortCutFracLit r res_ty - = return (HsFractional r expr) - - | otherwise - = do { expr <- newLitInst orig lit res_ty - ; return (HsFractional r expr) } - -newLitInst :: InstOrigin -> HsOverLit Name -> BoxyRhoType -> TcM (HsExpr TcId) -newLitInst orig lit res_ty -- Make a LitInst - = do { loc <- getInstLoc orig - ; res_tau <- zapToMonotype res_ty - ; new_uniq <- newUnique - ; let lit_nm = mkSystemVarName new_uniq FSLIT("lit") - lit_inst = LitInst lit_nm lit res_tau loc - ; extendLIE lit_inst - ; return (HsVar (instToId lit_inst)) } +addDataConStupidTheta :: DataCon -> [TcType] -> TcM () +-- Instantiate the "stupid theta" of the data con, and throw +-- the constraints into the constraint set +addDataConStupidTheta data_con inst_tys + | null stupid_theta = return () + | otherwise = instStupidTheta origin inst_theta + where + origin = OccurrenceOf (dataConName data_con) + -- The origin should always report "occurrence of C" + -- even when C occurs in a pattern + stupid_theta = dataConStupidTheta data_con + tenv = mkTopTvSubst (dataConUnivTyVars data_con `zip` inst_tys) + -- NB: inst_tys can be longer than the univ tyvars + -- because the constructor might have existentials + inst_theta = substTheta tenv stupid_theta \end{code} +Note [Arrows and patterns] +~~~~~~~~~~~~~~~~~~~~~~~~~~ +(Oct 07) Arrow noation 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, becuase 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. %************************************************************************ %* * @@ -767,62 +972,88 @@ Meanwhile, the strategy is: %* * %************************************************************************ -\begin{code} -patCtxt :: Pat Name -> Maybe Message -- Not all patterns are worth pushing a context -patCtxt (VarPat _) = Nothing -patCtxt (ParPat _) = Nothing -patCtxt (AsPat _ _) = Nothing -patCtxt pat = Just (hang (ptext SLIT("In the pattern:")) - 4 (ppr pat)) - ------------------------------------------------ - -existentialExplode pat - = hang (vcat [text "My brain just exploded.", - text "I can't handle pattern bindings for existentially-quantified constructors.", - text "In the binding group for"]) - 4 (ppr pat) +{- This was used to improve the error message from + an existential escape. Need to think how to do this. -sigPatCtxt bound_ids bound_tvs pat_tys body_ty tidy_env +sigPatCtxt :: [LPat Var] -> [Var] -> [TcType] -> TcType -> TidyEnv + -> TcM (TidyEnv, SDoc) +sigPatCtxt pats bound_tvs pat_tys body_ty tidy_env = do { pat_tys' <- mapM zonkTcType pat_tys ; body_ty' <- zonkTcType body_ty ; let (env1, tidy_tys) = tidyOpenTypes tidy_env (map idType show_ids) (env2, tidy_pat_tys) = tidyOpenTypes env1 pat_tys' (env3, tidy_body_ty) = tidyOpenType env2 body_ty' ; return (env3, - sep [ptext SLIT("When checking an existential match that binds"), - nest 4 (vcat (zipWith ppr_id show_ids tidy_tys)), - ptext SLIT("The pattern(s) have type(s):") <+> vcat (map ppr tidy_pat_tys), - ptext SLIT("The body has type:") <+> ppr tidy_body_ty + sep [ptext (sLit "When checking an existential match that binds"), + nest 2 (vcat (zipWith ppr_id show_ids tidy_tys)), + ptext (sLit "The pattern(s) have type(s):") <+> vcat (map ppr tidy_pat_tys), + ptext (sLit "The body has type:") <+> ppr tidy_body_ty ]) } where + bound_ids = collectPatsBinders pats show_ids = filter is_interesting bound_ids - is_interesting id = any (`elemVarSet` idFreeTyVars id) bound_tvs + is_interesting id = any (`elemVarSet` varTypeTyVars id) bound_tvs ppr_id id ty = ppr id <+> dcolon <+> ppr ty -- Don't zonk the types so we get the separate, un-unified versions +-} + +\begin{code} +maybeWrapPatCtxt :: Pat Name -> (TcM a -> TcM b) -> TcM a -> TcM b +-- Not all patterns are worth pushing a context +maybeWrapPatCtxt pat tcm thing_inside + | not (worth_wrapping pat) = tcm thing_inside + | otherwise = addErrCtxt msg $ tcm $ popErrCtxt thing_inside + -- Remember to pop before doing thing_inside + where + worth_wrapping (VarPat {}) = False + worth_wrapping (ParPat {}) = False + worth_wrapping (AsPat {}) = False + worth_wrapping _ = True + msg = hang (ptext (sLit "In the pattern:")) 2 (ppr pat) + +----------------------------------------------- +checkExistentials :: [TyVar] -> PatEnv -> TcM () + -- See Note [Arrows and patterns] +checkExistentials [] _ = return () +checkExistentials _ (PE { pe_ctxt = LetPat {}}) = failWithTc existentialLetPat +checkExistentials _ (PE { pe_ctxt = LamPat ProcExpr }) = failWithTc existentialProcPat +checkExistentials _ (PE { pe_lazy = True }) = failWithTc existentialLazyPat +checkExistentials _ _ = return () + +existentialLazyPat :: SDoc +existentialLazyPat + = hang (ptext (sLit "An existential or GADT data constructor cannot be used")) + 2 (ptext (sLit "inside a lazy (~) pattern")) + +existentialProcPat :: SDoc +existentialProcPat + = ptext (sLit "Proc patterns cannot use existential or GADT data constructors") + +existentialLetPat :: SDoc +existentialLetPat + = vcat [text "My brain just exploded", + text "I can't handle pattern bindings for existential or GADT data constructors.", + text "Instead, use a case-expression, or do-notation, to unpack the constructor."] badFieldCon :: DataCon -> Name -> SDoc badFieldCon con field - = hsep [ptext SLIT("Constructor") <+> quotes (ppr con), - ptext SLIT("does not have field"), quotes (ppr field)] + = hsep [ptext (sLit "Constructor") <+> quotes (ppr con), + ptext (sLit "does not have field"), quotes (ppr field)] polyPatSig :: TcType -> SDoc polyPatSig sig_ty - = hang (ptext SLIT("Illegal polymorphic type signature in pattern:")) - 4 (ppr sig_ty) - -badTypePat pat = ptext SLIT("Illegal type pattern") <+> ppr pat + = hang (ptext (sLit "Illegal polymorphic type signature in pattern:")) + 2 (ppr sig_ty) -lazyPatErr pat tvs +lazyUnliftedPatErr :: OutputableBndr name => Pat name -> TcM () +lazyUnliftedPatErr pat = failWithTc $ - hang (ptext SLIT("A lazy (~) pattern connot bind existential type variables")) - 2 (vcat (map pprSkolTvBinding tvs)) - -nonRigidMatch con - = hang (ptext SLIT("GADT pattern match in non-rigid context for") <+> quotes (ppr con)) - 2 (ptext SLIT("Tell GHC HQ if you'd like this to unify the context")) + hang (ptext (sLit "A lazy (~) pattern cannot contain unlifted types:")) + 2 (ppr pat) -inaccessibleAlt msg - = hang (ptext SLIT("Inaccessible case alternative:")) 2 msg +unboxedTupleErr :: SDoc -> Type -> SDoc +unboxedTupleErr what ty + = hang (what <+> ptext (sLit "cannot have an unboxed tuple type:")) + 2 (ppr ty) \end{code}