X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=ghc%2Fcompiler%2Ftypecheck%2FTcPat.lhs;h=208af13cc0c36c81d054693498bc918dbc9d0d8d;hb=ff818166a0a06e77becad9e28ed116f3b7f5cc8b;hp=f816b7c181321ea77c9f10105c5af2a01a504bf2;hpb=b085ee40c7f265a5977ea6ec1c415e573be5ff8c;p=ghc-hetmet.git diff --git a/ghc/compiler/typecheck/TcPat.lhs b/ghc/compiler/typecheck/TcPat.lhs index f816b7c..208af13 100644 --- a/ghc/compiler/typecheck/TcPat.lhs +++ b/ghc/compiler/typecheck/TcPat.lhs @@ -4,40 +4,48 @@ \section[TcPat]{Typechecking patterns} \begin{code} -module TcPat ( tcPat, tcMonoPatBndr, tcSubPat, - badFieldCon, polyPatSig - ) where +module TcPat ( tcPat, tcPats, PatCtxt(..), badFieldCon, polyPatSig, refineTyVars ) where #include "HsVersions.h" -import HsSyn ( InPat(..), OutPat(..), HsLit(..), HsOverLit(..), HsExpr(..) ) -import RnHsSyn ( RenamedPat ) -import TcHsSyn ( TcPat, TcId, simpleHsLitTy ) - -import TcMonad +import HsSyn ( Pat(..), LPat, HsConDetails(..), HsLit(..), HsOverLit(..), + HsExpr(..), LHsBinds, emptyLHsBinds, isEmptyLHsBinds ) +import HsUtils +import TcHsSyn ( TcId, hsLitType ) +import TcRnMonad import Inst ( InstOrigin(..), - emptyLIE, plusLIE, LIE, mkLIE, unitLIE, instToId, isEmptyLIE, - newMethod, newMethodFromName, newOverloadedLit, newDicts, tcInstDataCon + newMethodFromName, newOverloadedLit, newDicts, + instToId, tcInstStupidTheta, tcSyntaxName ) -import Id ( mkLocalId, mkSysLocal ) +import Id ( Id, idType, mkLocalId ) +import Var ( tyVarName ) import Name ( Name ) -import FieldLabel ( fieldLabelName ) -import TcEnv ( tcLookupClass, tcLookupDataCon, tcLookupGlobalId, tcLookupId ) -import TcMType ( newTyVarTy, zapToType ) -import TcType ( TcType, TcTyVar, TcSigmaType, - mkClassPred, liftedTypeKind ) -import TcUnify ( tcSubOff, TcHoleType, - unifyTauTy, unifyListTy, unifyPArrTy, unifyTupleTy, - mkCoercion, idCoercion, isIdCoercion, - (<$>), PatCoFn ) -import TcMonoType ( tcHsSigType, UserTypeCtxt(..) ) - -import TysWiredIn ( stringTy ) +import TcSimplify ( tcSimplifyCheck, bindInstsOfLocalFuns ) +import TcEnv ( newLocalName, tcExtendIdEnv1, tcExtendTyVarEnv2, + tcLookupClass, tcLookupDataCon, tcLookupId ) +import TcMType ( newTyFlexiVarTy, arityErr, tcSkolTyVars, readMetaTyVar ) +import TcType ( TcType, TcTyVar, TcSigmaType, TcTauType, zipTopTvSubst, + SkolemInfo(PatSkol), isSkolemTyVar, isMetaTyVar, pprTcTyVar, + TvSubst, mkOpenTvSubst, substTyVar, substTy, MetaDetails(..), + mkTyVarTys, mkClassPred, mkTyConApp, isOverloadedTy ) +import VarEnv ( mkVarEnv ) -- ugly +import Kind ( argTypeKind, liftedTypeKind ) +import TcUnify ( tcSubPat, Expected(..), zapExpectedType, + zapExpectedTo, zapToListTy, zapToTyConApp ) +import TcHsType ( UserTypeCtxt(..), TcSigInfo( sig_tau ), TcSigFun, tcHsPatSigType ) +import TysWiredIn ( stringTy, parrTyCon, tupleTyCon ) +import Unify ( MaybeErr(..), gadtRefineTys, BindFlag(..) ) +import Type ( substTys, substTheta ) import CmdLineOpts ( opt_IrrefutableTuples ) -import DataCon ( dataConFieldLabels, dataConSourceArity ) -import PrelNames ( eqStringName, eqName, geName, cCallableClassName ) +import TyCon ( TyCon ) +import DataCon ( DataCon, dataConTyCon, isVanillaDataCon, dataConInstOrigArgTys, + dataConFieldLabels, dataConSourceArity, dataConSig ) +import PrelNames ( eqStringName, eqName, geName, negateName, minusName, + integralClassName ) import BasicTypes ( isBoxed ) -import Bag +import SrcLoc ( Located(..), SrcSpan, noLoc, unLoc ) +import Maybes ( catMaybes ) +import ErrUtils ( Message ) import Outputable import FastString \end{code} @@ -45,214 +53,411 @@ import FastString %************************************************************************ %* * -\subsection{Variable patterns} + External interface %* * %************************************************************************ -\begin{code} -type BinderChecker = Name -> TcSigmaType -> TcM (PatCoFn, LIE, TcId) - -- How to construct a suitable (monomorphic) - -- Id for variables found in the pattern - -- The TcSigmaType is the expected type - -- from the pattern context - --- The Id may have a sigma type (e.g. f (x::forall a. a->a)) --- so we want to *create* it during pattern type checking. --- We don't want to make Ids first with a type-variable type --- and then unify... becuase we can't unify a sigma type with a type variable. - -tcMonoPatBndr :: BinderChecker - -- This is the right function to pass to tcPat when - -- we're looking at a lambda-bound pattern, - -- so there's no polymorphic guy to worry about - -tcMonoPatBndr binder_name pat_ty - = zapToType pat_ty `thenNF_Tc` \ pat_ty' -> - -- If there are *no constraints* on the pattern type, we - -- revert to good old H-M typechecking, making - -- the type of the binder into an *ordinary* - -- type variable. We find out if there are no constraints - -- by seeing if we are given an "open hole" as our info. - -- What we are trying to avoid here is giving a binder - -- a type that is a 'hole'. The only place holes should - -- appear is as an argument to tcPat and tcExpr/tcMonoExpr. - - returnTc (idCoercion, emptyLIE, mkLocalId binder_name pat_ty') -\end{code} +Note [Nesting] +tcPat takes a "thing inside" over which the patter 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. -%************************************************************************ -%* * -\subsection{Typechecking patterns} -%* * -%************************************************************************ +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 tcPat. \begin{code} -tcPat :: BinderChecker - -> RenamedPat - - -> TcHoleType -- Expected type derived from the context - -- In the case of a function with a rank-2 signature, - -- this type might be a forall type. - - -> TcM (TcPat, - LIE, -- Required by n+k and literal pats - Bag TcTyVar, -- TyVars bound by the pattern - -- These are just the existentially-bound ones. - -- Any tyvars bound by *type signatures* in the - -- patterns are brought into scope before we begin. - Bag (Name, TcId), -- Ids bound by the pattern, along with the Name under - -- which it occurs in the pattern - -- The two aren't the same because we conjure up a new - -- local name for each variable. - LIE) -- Dicts or methods [see below] bound by the pattern - -- from existential constructor patterns +tcPat :: PatCtxt + -> LPat Name -> Expected TcSigmaType + -> TcM a -- Thing inside + -> TcM (LPat TcId, -- Translated pattern + [TcTyVar], -- Existential binders + a) -- Result of thing inside + +tcPat ctxt pat exp_ty thing_inside + = do { err_ctxt <- getErrCtxt + ; maybeAddErrCtxt (patCtxt (unLoc pat)) $ + tc_lpat ctxt pat exp_ty $ + setErrCtxt err_ctxt thing_inside } + -- Restore error context before doing thing_inside + -- See note [Nesting] above + +-------------------- +tcPats :: PatCtxt + -> [LPat Name] + -> [Expected TcSigmaType] -- Excess types discarded + -> TcM a + -> TcM ([LPat TcId], [TcTyVar], a) + +tcPats ctxt [] _ thing_inside + = do { res <- thing_inside + ; return ([], [], res) } + +tcPats ctxt (p:ps) (ty:tys) thing_inside + = do { (p', p_tvs, (ps', ps_tvs, res)) + <- tcPat ctxt p ty $ + tcPats ctxt ps tys thing_inside + ; return (p':ps', p_tvs ++ ps_tvs, res) } + +-------------------- +tcCheckPats :: PatCtxt + -> [LPat Name] -> [TcSigmaType] + -> TcM a + -> TcM ([LPat TcId], [TcTyVar], a) +tcCheckPats ctxt pats tys thing_inside -- A trivial wrapper + = tcPats ctxt pats (map Check tys) thing_inside \end{code} %************************************************************************ %* * -\subsection{Variables, wildcards, lazy pats, as-pats} + Binders %* * %************************************************************************ \begin{code} -tcPat tc_bndr pat@(TypePatIn ty) pat_ty - = failWithTc (badTypePat pat) - -tcPat tc_bndr (VarPatIn name) pat_ty - = tc_bndr name pat_ty `thenTc` \ (co_fn, lie_req, bndr_id) -> - returnTc (co_fn <$> VarPat bndr_id, lie_req, - emptyBag, unitBag (name, bndr_id), emptyLIE) - -tcPat tc_bndr (LazyPatIn pat) pat_ty - = tcPat tc_bndr pat pat_ty `thenTc` \ (pat', lie_req, tvs, ids, lie_avail) -> - returnTc (LazyPat pat', lie_req, tvs, ids, lie_avail) - -tcPat tc_bndr pat_in@(AsPatIn name pat) pat_ty - = tc_bndr name pat_ty `thenTc` \ (co_fn, lie_req1, bndr_id) -> - tcPat tc_bndr pat pat_ty `thenTc` \ (pat', lie_req2, tvs, ids, lie_avail) -> - returnTc (co_fn <$> (AsPat bndr_id pat'), lie_req1 `plusLIE` lie_req2, - tvs, (name, bndr_id) `consBag` ids, lie_avail) - -tcPat tc_bndr WildPatIn pat_ty - = zapToType pat_ty `thenNF_Tc` \ pat_ty' -> - -- We might have an incoming 'hole' type variable; no annotation - -- so zap it to a type. Rather like tcMonoPatBndr. - returnTc (WildPat pat_ty', emptyLIE, emptyBag, emptyBag, emptyLIE) - -tcPat tc_bndr (ParPatIn parend_pat) pat_ty - = tcPat tc_bndr parend_pat pat_ty - -tcPat tc_bndr pat_in@(SigPatIn pat sig) pat_ty - = tcAddErrCtxt (patCtxt pat_in) $ - tcHsSigType PatSigCtxt sig `thenTc` \ sig_ty -> - tcSubPat sig_ty pat_ty `thenTc` \ (co_fn, lie_sig) -> - tcPat tc_bndr pat sig_ty `thenTc` \ (pat', lie_req, tvs, ids, lie_avail) -> - returnTc (co_fn <$> pat', lie_req `plusLIE` lie_sig, tvs, ids, lie_avail) +data PatCtxt = LamPat -- Used for lambda, case, do-notation etc + | LetPat TcSigFun -- Used for let(rec) bindings + +------------------- +tcPatBndr :: PatCtxt -> Name -> Expected TcSigmaType -> TcM TcId +tcPatBndr LamPat bndr_name pat_ty + = do { pat_ty' <- zapExpectedType pat_ty argTypeKind + -- If pat_ty is Expected, this returns the appropriate + -- SigmaType. In Infer mode, we create a fresh type variable. + -- Note the SigmaType: we can get + -- 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 (LetPat lookup_sig) bndr_name pat_ty + | Just sig <- lookup_sig bndr_name + = do { let mono_ty = sig_tau sig + ; mono_name <- newLocalName bndr_name + ; tcSubPat mono_ty pat_ty + ; return (mkLocalId mono_name mono_ty) } + + | otherwise + = do { mono_name <- newLocalName bndr_name + ; pat_ty' <- zapExpectedType pat_ty argTypeKind + ; return (mkLocalId mono_name pat_ty') } + + +------------------- +bindInstsOfPatId :: TcId -> TcM a -> TcM (a, LHsBinds TcId) +bindInstsOfPatId id thing_inside + | not (isOverloadedTy (idType id)) + = do { res <- thing_inside; return (res, emptyLHsBinds) } + | otherwise + = do { (res, lie) <- getLIE thing_inside + ; binds <- bindInstsOfLocalFuns lie [id] + ; return (res, binds) } \end{code} %************************************************************************ %* * -\subsection{Explicit lists, parallel arrays, and tuples} + tc_pat: the main worker function %* * %************************************************************************ \begin{code} -tcPat tc_bndr pat_in@(ListPatIn pats) pat_ty - = tcAddErrCtxt (patCtxt pat_in) $ - unifyListTy pat_ty `thenTc` \ elem_ty -> - tcPats tc_bndr pats (repeat elem_ty) `thenTc` \ (pats', lie_req, tvs, ids, lie_avail) -> - returnTc (ListPat elem_ty pats', lie_req, tvs, ids, lie_avail) - -tcPat tc_bndr pat_in@(PArrPatIn pats) pat_ty - = tcAddErrCtxt (patCtxt pat_in) $ - unifyPArrTy pat_ty `thenTc` \ elem_ty -> - tcPats tc_bndr pats (repeat elem_ty) `thenTc` \ (pats', lie_req, tvs, ids, lie_avail) -> - returnTc (PArrPat elem_ty pats', lie_req, tvs, ids, lie_avail) +tc_lpat :: PatCtxt + -> LPat Name -> Expected TcSigmaType + -> TcM a -- Thing inside + -> TcM (LPat TcId, -- Translated pattern + [TcTyVar], -- Existential binders + a) -- Result of thing inside + +tc_lpat ctxt (L span pat) pat_ty thing_inside + = setSrcSpan span $ + -- It's OK to keep setting the SrcSpan; + -- it just overwrites the previous value + do { (pat', tvs, res) <- tc_pat ctxt pat pat_ty thing_inside + ; return (L span pat', tvs, res) } + +--------------------- +tc_pat ctxt (VarPat name) pat_ty thing_inside + = do { id <- tcPatBndr ctxt name pat_ty + ; (res, binds) <- bindInstsOfPatId id $ + tcExtendIdEnv1 name id $ + (traceTc (text "binding" <+> ppr name <+> ppr (idType id)) + >> thing_inside) + ; let pat' | isEmptyLHsBinds binds = VarPat id + | otherwise = VarPatOut id binds + ; return (pat', [], res) } + +tc_pat ctxt (ParPat pat) pat_ty thing_inside + = do { (pat', tvs, res) <- tc_lpat ctxt pat pat_ty thing_inside + ; return (ParPat pat', tvs, res) } + +-- There's a wrinkle with irrefuatable 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 ctxt lpat@(LazyPat pat) pat_ty thing_inside + = do { reft <- getTypeRefinement + ; (pat', pat_tvs, res) <- tc_lpat ctxt pat pat_ty $ + setTypeRefinement reft thing_inside + ; if (null pat_tvs) then return () + else lazyPatErr lpat pat_tvs + ; return (LazyPat pat', [], res) } + +tc_pat ctxt (WildPat _) pat_ty thing_inside + = do { pat_ty' <- zapExpectedType pat_ty argTypeKind + -- Note argTypeKind, so that + -- f _ = 3 + -- is rejected when f applied to an unboxed tuple + -- However, this means that + -- (case g x of _ -> ...) + -- is rejected g returns an unboxed tuple, which is perhpas + -- annoying. I suppose we could pass the context into tc_pat... + ; res <- thing_inside + ; return (WildPat pat_ty', [], res) } + +tc_pat ctxt (AsPat (L nm_loc name) pat) pat_ty thing_inside + = do { bndr_id <- setSrcSpan nm_loc (tcPatBndr ctxt name pat_ty) + ; (pat', tvs, res) <- tcExtendIdEnv1 name bndr_id $ + tc_lpat ctxt pat (Check (idType bndr_id)) thing_inside + -- NB: if we do inference on: + -- \ (y@(x::forall a. a->a)) = e + -- we'll fail. The as-pattern infers a monotype for 'y', which then + -- fails to unify with the polymorphic type for 'x'. This could + -- perhaps be fixed, but only with a bit more work. + -- + -- If you fix it, don't forget the bindInstsOfPatIds! + ; return (AsPat (L nm_loc bndr_id) pat', tvs, res) } + +tc_pat ctxt (SigPatIn pat sig) pat_ty thing_inside + = do { -- See Note [Pattern coercions] below + (sig_tvs, sig_ty) <- tcHsPatSigType PatSigCtxt sig + ; tcSubPat sig_ty pat_ty + ; subst <- refineTyVars sig_tvs -- See note [Type matching] + ; let tv_binds = [(tyVarName tv, substTyVar subst tv) | tv <- sig_tvs] + sig_ty' = substTy subst sig_ty + ; (pat', tvs, res) + <- tcExtendTyVarEnv2 tv_binds $ + tc_lpat ctxt pat (Check sig_ty') thing_inside + + ; return (SigPatOut pat' sig_ty, tvs, res) } + +tc_pat ctxt pat@(TypePat ty) pat_ty thing_inside + = failWithTc (badTypePat pat) -tcPat tc_bndr pat_in@(TuplePatIn pats boxity) pat_ty - = tcAddErrCtxt (patCtxt pat_in) $ +------------------------ +-- Lists, tuples, arrays +tc_pat ctxt (ListPat pats _) pat_ty thing_inside + = do { elem_ty <- zapToListTy pat_ty + ; (pats', pats_tvs, res) <- tcCheckPats ctxt pats (repeat elem_ty) thing_inside + ; return (ListPat pats' elem_ty, pats_tvs, res) } - unifyTupleTy boxity arity pat_ty `thenTc` \ arg_tys -> - tcPats tc_bndr pats arg_tys `thenTc` \ (pats', lie_req, tvs, ids, lie_avail) -> +tc_pat ctxt (PArrPat pats _) pat_ty thing_inside + = do { [elem_ty] <- zapToTyConApp parrTyCon pat_ty + ; (pats', pats_tvs, res) <- tcCheckPats ctxt pats (repeat elem_ty) thing_inside + ; return (PArrPat pats' elem_ty, pats_tvs, res) } - -- possibly do the "make all tuple-pats irrefutable" test: - let - unmangled_result = TuplePat pats' boxity +tc_pat ctxt (TuplePat pats boxity) pat_ty thing_inside + = do { let arity = length pats + tycon = tupleTyCon boxity arity + ; arg_tys <- zapToTyConApp tycon pat_ty + ; (pats', pats_tvs, res) <- tcCheckPats ctxt 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 + possibly_mangled_result + | opt_IrrefutableTuples && isBoxed boxity = LazyPat (noLoc unmangled_result) + | otherwise = unmangled_result + + ; ASSERT( length arg_tys == arity ) -- Syntactically enforced + return (possibly_mangled_result, pats_tvs, res) } + +------------------------ +-- Data constructors +tc_pat ctxt 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 + ; ty_args <- zapToTyConApp tycon pat_ty + ; (pat', tvs, res) <- tcConPat ctxt con_span data_con tycon ty_args arg_pats thing_inside + ; return (pat', tvs, res) } + + +------------------------ +-- Literal patterns +tc_pat ctxt pat@(LitPat lit@(HsString _)) pat_ty thing_inside + = do { -- Strings are mapped to NPatOuts, which have a guard expression + zapExpectedTo pat_ty stringTy + ; eq_id <- tcLookupId eqStringName + ; res <- thing_inside + ; returnM (NPatOut lit stringTy (nlHsVar eq_id `HsApp` nlHsLit lit), [], res) } + +tc_pat ctxt (LitPat simple_lit) pat_ty thing_inside + = do { -- All other simple lits + zapExpectedTo pat_ty (hsLitType simple_lit) + ; res <- thing_inside + ; returnM (LitPat simple_lit, [], res) } + +------------------------ +-- Overloaded patterns: n, and n+k +tc_pat ctxt pat@(NPatIn over_lit mb_neg) pat_ty thing_inside + = do { pat_ty' <- zapExpectedType pat_ty liftedTypeKind + ; let origin = LiteralOrigin over_lit + ; pos_lit_expr <- newOverloadedLit origin over_lit pat_ty' + ; eq <- newMethodFromName origin pat_ty' eqName + ; lit_expr <- case mb_neg of + Nothing -> returnM pos_lit_expr -- Positive literal + Just neg -> -- Negative literal + -- The 'negate' is re-mappable syntax + do { (_, neg_expr) <- tcSyntaxName origin pat_ty' + (negateName, HsVar neg) + ; returnM (mkHsApp (noLoc neg_expr) pos_lit_expr) } + + ; let -- The literal in an NPatIn is always positive... + -- But in NPatOut, the literal is used to find identical patterns + -- so we must negate the literal when necessary! + lit' = case (over_lit, mb_neg) of + (HsIntegral i _, Nothing) -> HsInteger i pat_ty' + (HsIntegral i _, Just _) -> HsInteger (-i) pat_ty' + (HsFractional f _, Nothing) -> HsRat f pat_ty' + (HsFractional f _, Just _) -> HsRat (-f) pat_ty' + + ; res <- thing_inside + ; returnM (NPatOut lit' pat_ty' (HsApp (nlHsVar eq) lit_expr), [], res) } + +tc_pat ctxt pat@(NPlusKPatIn (L nm_loc name) lit@(HsIntegral i _) minus_name) pat_ty thing_inside + = do { bndr_id <- setSrcSpan nm_loc (tcPatBndr ctxt name pat_ty) + ; let pat_ty' = idType bndr_id + origin = LiteralOrigin lit + ; over_lit_expr <- newOverloadedLit origin lit pat_ty' + ; ge <- newMethodFromName origin pat_ty' geName - possibly_mangled_result - | opt_IrrefutableTuples && isBoxed boxity = LazyPat unmangled_result - | otherwise = unmangled_result - in - returnTc (possibly_mangled_result, lie_req, tvs, ids, lie_avail) - where - arity = length pats -\end{code} - - -%************************************************************************ -%* * -\subsection{Other constructors} -%* * - -%************************************************************************ - -\begin{code} -tcPat tc_bndr pat@(ConPatIn name arg_pats) pat_ty - = tcConPat tc_bndr pat name arg_pats pat_ty - -tcPat tc_bndr pat@(ConOpPatIn pat1 op _ pat2) pat_ty - = tcConPat tc_bndr pat op [pat1, pat2] pat_ty + -- The '-' part is re-mappable syntax + ; (_, minus_expr) <- tcSyntaxName origin pat_ty' (minusName, HsVar minus_name) + + -- 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 origin [mkClassPred icls [pat_ty']] + ; extendLIEs dicts + + ; res <- tcExtendIdEnv1 name bndr_id thing_inside + ; returnM (NPlusKPatOut (L nm_loc bndr_id) i + (SectionR (nlHsVar ge) over_lit_expr) + (SectionR (noLoc minus_expr) over_lit_expr), + [], res) } \end{code} %************************************************************************ %* * -\subsection{Records} + Most of the work for constructors is here + (the rest is in the ConPatIn case of tc_pat) %* * %************************************************************************ \begin{code} -tcPat tc_bndr pat@(RecPatIn name rpats) pat_ty - = tcAddErrCtxt (patCtxt pat) $ - - -- Check the constructor itself - tcConstructor pat name `thenTc` \ (data_con, lie_req1, ex_tvs, ex_dicts, lie_avail1, arg_tys, con_res_ty) -> - - -- Check overall type matches (c.f. tcConPat) - tcSubPat con_res_ty pat_ty `thenTc` \ (co_fn, lie_req2) -> - let - -- 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). - field_tys = zip (map fieldLabelName (dataConFieldLabels data_con)) - arg_tys - in - - -- Check the fields - tc_fields field_tys rpats `thenTc` \ (rpats', lie_req3, tvs, ids, lie_avail2) -> - - returnTc (RecPat data_con pat_ty ex_tvs ex_dicts rpats', - lie_req1 `plusLIE` lie_req2 `plusLIE` lie_req3, - listToBag ex_tvs `unionBags` tvs, - ids, - lie_avail1 `plusLIE` lie_avail2) +tcConPat :: PatCtxt -> SrcSpan -> DataCon -> TyCon -> [TcTauType] + -> HsConDetails Name (LPat Name) -> TcM a + -> TcM (Pat TcId, [TcTyVar], a) +tcConPat ctxt span data_con tycon ty_args arg_pats thing_inside + | isVanillaDataCon data_con + = do { let arg_tys = dataConInstOrigArgTys data_con ty_args + ; tcInstStupidTheta data_con ty_args + ; traceTc (text "tcConPat" <+> vcat [ppr data_con, ppr ty_args, ppr arg_tys]) + ; (arg_pats', tvs, res) <- tcConArgs ctxt data_con arg_pats arg_tys thing_inside + ; return (ConPatOut (L span data_con) [] [] emptyLHsBinds + arg_pats' (mkTyConApp tycon ty_args), + tvs, res) } + + | otherwise -- GADT case + = do { let (tvs, theta, arg_tys, _, res_tys) = dataConSig data_con + ; span <- getSrcSpanM + ; let rigid_info = PatSkol data_con span + ; tvs' <- tcSkolTyVars rigid_info tvs + ; let tv_tys' = mkTyVarTys tvs' + tenv = zipTopTvSubst tvs tv_tys' + theta' = substTheta tenv theta + arg_tys' = substTys tenv arg_tys + res_tys' = substTys tenv res_tys + ; dicts <- newDicts (SigOrigin rigid_info) theta' + + -- Do type refinement! + ; traceTc (text "tcGadtPat" <+> vcat [ppr data_con, ppr tvs', ppr arg_tys', ppr res_tys', + text "ty-args:" <+> ppr ty_args ]) + ; refineAlt ctxt data_con tvs' ty_args res_tys' $ do + + { ((arg_pats', inner_tvs, res), lie_req) <- getLIE $ + do { tcInstStupidTheta data_con tv_tys' + -- The stupid-theta mentions the newly-bound tyvars, so + -- it must live inside the getLIE, so that the + -- tcSimplifyCheck will apply the type refinement to it + ; tcConArgs ctxt data_con arg_pats arg_tys' thing_inside } + + ; dict_binds <- tcSimplifyCheck doc tvs' dicts lie_req + + ; return (ConPatOut (L span data_con) + tvs' (map instToId dicts) dict_binds + arg_pats' (mkTyConApp tycon ty_args), + tvs' ++ inner_tvs, res) } } + where + doc = ptext SLIT("existential context for") <+> quotes (ppr data_con) + +tcConArgs :: PatCtxt -> DataCon + -> HsConDetails Name (LPat Name) -> [TcSigmaType] + -> TcM a + -> TcM (HsConDetails TcId (LPat Id), [TcTyVar], a) + +tcConArgs ctxt data_con (PrefixCon arg_pats) arg_tys thing_inside + = do { checkTc (con_arity == no_of_args) -- Check correct arity + (arityErr "Constructor" data_con con_arity no_of_args) + ; (arg_pats', tvs, res) <- tcCheckPats ctxt arg_pats arg_tys thing_inside + ; return (PrefixCon arg_pats', tvs, res) } + where + con_arity = dataConSourceArity data_con + no_of_args = length arg_pats + +tcConArgs ctxt data_con (InfixCon p1 p2) arg_tys thing_inside + = do { checkTc (con_arity == 2) -- Check correct arity + (arityErr "Constructor" data_con con_arity 2) + ; ([p1',p2'], tvs, res) <- tcCheckPats ctxt [p1,p2] arg_tys thing_inside + ; return (InfixCon p1' p2', tvs, res) } + where + con_arity = dataConSourceArity data_con +tcConArgs ctxt data_con (RecCon rpats) arg_tys thing_inside + = do { (rpats', tvs, res) <- tc_fields rpats thing_inside + ; return (RecCon rpats', tvs, res) } where - tc_fields field_tys [] - = returnTc ([], emptyLIE, emptyBag, emptyBag, emptyLIE) + tc_fields :: [(Located Name, LPat Name)] -> TcM a + -> TcM ([(Located TcId, LPat TcId)], [TcTyVar], a) + tc_fields [] thing_inside + = do { res <- thing_inside + ; return ([], [], res) } - tc_fields field_tys ((field_label, rhs_pat, pun_flag) : rpats) - = tc_fields field_tys rpats `thenTc` \ (rpats', lie_req1, tvs1, ids1, lie_avail1) -> + tc_fields (rpat : rpats) thing_inside + = do { (rpat', tvs1, (rpats', tvs2, res)) + <- tc_field rpat (tc_fields rpats thing_inside) + ; return (rpat':rpats', tvs1 ++ tvs2, res) } - (case [ty | (f,ty) <- field_tys, f == field_label] of + tc_field (field_lbl, pat) thing_inside + = do { (sel_id, pat_ty) <- wrapLocFstM find_field_ty field_lbl + ; (pat', tvs, res) <- tcPat ctxt pat (Check pat_ty) thing_inside + ; return ((sel_id, pat'), tvs, res) } + + find_field_ty field_lbl + = case [ty | (f,ty) <- field_tys, f == field_lbl] of -- No matching field; chances are this field label comes from some -- other record type (or maybe none). As well as reporting an @@ -262,201 +467,142 @@ tcPat tc_bndr pat@(RecPatIn name rpats) pat_ty -- 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". - [] -> addErrTc (badFieldCon name field_label) `thenNF_Tc_` - newTyVarTy liftedTypeKind `thenNF_Tc_` - returnTc (error "Bogus selector Id", pat_ty) + [] -> do { addErrTc (badFieldCon data_con field_lbl) + ; bogus_ty <- newTyFlexiVarTy liftedTypeKind + ; return (error "Bogus selector Id", bogus_ty) } -- The normal case, when the field comes from the right constructor (pat_ty : extras) -> ASSERT( null extras ) - tcLookupGlobalId field_label `thenNF_Tc` \ sel_id -> - returnTc (sel_id, pat_ty) - ) `thenTc` \ (sel_id, pat_ty) -> - - tcPat tc_bndr rhs_pat pat_ty `thenTc` \ (rhs_pat', lie_req2, tvs2, ids2, lie_avail2) -> + do { sel_id <- tcLookupId field_lbl + ; return (sel_id, pat_ty) } - returnTc ((sel_id, rhs_pat', pun_flag) : rpats', - lie_req1 `plusLIE` lie_req2, - tvs1 `unionBags` tvs2, - ids1 `unionBags` ids2, - lie_avail1 `plusLIE` lie_avail2) + field_tys = zip (dataConFieldLabels data_con) arg_tys + -- Don't use zipEqual! If the constructor isn't really a record, then + -- dataConFieldLabels will be empty (and each field in the pattern + -- will generate an error below). \end{code} + %************************************************************************ %* * -\subsection{Literals} + Type refinement %* * %************************************************************************ \begin{code} -tcPat tc_bndr (LitPatIn lit@(HsLitLit s _)) pat_ty - -- cf tcExpr on LitLits - = tcLookupClass cCallableClassName `thenNF_Tc` \ cCallableClass -> - newDicts (LitLitOrigin (unpackFS s)) - [mkClassPred cCallableClass [pat_ty]] `thenNF_Tc` \ dicts -> - returnTc (LitPat (HsLitLit s pat_ty) pat_ty, mkLIE dicts, emptyBag, emptyBag, emptyLIE) - -tcPat tc_bndr pat@(LitPatIn lit@(HsString _)) pat_ty - = unifyTauTy pat_ty stringTy `thenTc_` - tcLookupGlobalId eqStringName `thenNF_Tc` \ eq_id -> - returnTc (NPat lit stringTy (HsVar eq_id `HsApp` HsLit lit), - emptyLIE, emptyBag, emptyBag, emptyLIE) - -tcPat tc_bndr (LitPatIn simple_lit) pat_ty - = unifyTauTy pat_ty (simpleHsLitTy simple_lit) `thenTc_` - returnTc (LitPat simple_lit pat_ty, emptyLIE, emptyBag, emptyBag, emptyLIE) - -tcPat tc_bndr pat@(NPatIn over_lit) pat_ty - = newOverloadedLit origin over_lit pat_ty `thenNF_Tc` \ (over_lit_expr, lie1) -> - newMethodFromName origin pat_ty eqName `thenNF_Tc` \ eq -> - - returnTc (NPat lit' pat_ty (HsApp (HsVar (instToId eq)) over_lit_expr), - lie1 `plusLIE` unitLIE eq, - emptyBag, emptyBag, emptyLIE) +refineAlt :: PatCtxt -> DataCon + -> [TcTyVar] -- Freshly bound type variables + -> [TcType] -- Types from the scrutinee (context) + -> [TcType] -- Types from the pattern + -> TcM a -> TcM a +refineAlt ctxt con ex_tvs ctxt_tys pat_tys thing_inside + = do { old_subst <- getTypeRefinement + ; case gadtRefineTys bind_fn old_subst pat_tys ctxt_tys of + Failed msg -> failWithTc (inaccessibleAlt msg) + Succeeded new_subst -> do { + traceTc (text "refineTypes:match" <+> ppr con <+> ppr new_subst) + ; setTypeRefinement new_subst thing_inside } } + where - origin = PatOrigin pat - lit' = case over_lit of - HsIntegral i _ -> HsInteger i - HsFractional f _ -> HsRat f pat_ty + bind_fn tv | isMetaTyVar tv = WildCard -- Wobbly types behave as wild cards + | otherwise = BindMe \end{code} -%************************************************************************ -%* * -\subsection{n+k patterns} -%* * -%************************************************************************ +Note [Type matching] +~~~~~~~~~~~~~~~~~~~~ +This little function @refineTyVars@ is a little tricky. Suppose we have a pattern type +signature + f = \(x :: Term a) -> body +Then 'a' should be bound to a wobbly type. But if we have + f :: Term b -> some-type + f = \(x :: Term a) -> body +then 'a' should be bound to the rigid type 'b'. So we want to + * instantiate the type sig with fresh meta tyvars (e.g. \alpha) + * unify with the type coming from the context + * read out whatever information has been gleaned + from that unificaiton (e.g. unifying \alpha with 'b') + * and replace \alpha by 'b' in the type, when typechecking the + pattern inside the type sig (x in this case) +It amounts to combining rigid info from the context and from the sig. + +Exactly the same thing happens for 'smart function application'. \begin{code} -tcPat tc_bndr pat@(NPlusKPatIn name lit@(HsIntegral i _) minus_name) pat_ty - = tc_bndr name pat_ty `thenTc` \ (co_fn, lie1, bndr_id) -> - newOverloadedLit origin lit pat_ty `thenNF_Tc` \ (over_lit_expr, lie2) -> - newMethodFromName origin pat_ty geName `thenNF_Tc` \ ge -> - - -- The '-' part is re-mappable syntax - tcLookupId minus_name `thenNF_Tc` \ minus_sel_id -> - newMethod origin minus_sel_id [pat_ty] `thenNF_Tc` \ minus -> - - returnTc (NPlusKPat bndr_id i pat_ty - (SectionR (HsVar (instToId ge)) over_lit_expr) - (SectionR (HsVar (instToId minus)) over_lit_expr), - lie1 `plusLIE` lie2 `plusLIE` mkLIE [ge,minus], - emptyBag, unitBag (name, bndr_id), emptyLIE) +refineTyVars :: [TcTyVar] -- Newly instantiated meta-tyvars of the function + -> TcM TvSubst -- Substitution mapping any of the meta-tyvars that + -- has been unifies to what it was instantiated to +-- Just one level of de-wobblification though. What a hack! +refineTyVars tvs + = do { mb_prs <- mapM mk_pr tvs + ; return (mkOpenTvSubst (mkVarEnv (catMaybes mb_prs))) } where - origin = PatOrigin pat + mk_pr tv = do { details <- readMetaTyVar tv + ; case details of + Indirect ty -> return (Just (tv,ty)) + other -> return Nothing + } \end{code} %************************************************************************ %* * -\subsection{Lists of patterns} + Note [Pattern coercions] %* * %************************************************************************ -Helper functions +In principle, these program would be reasonable: + + f :: (forall a. a->a) -> Int + f (x :: Int->Int) = x 3 -\begin{code} -tcPats :: BinderChecker -- How to deal with variables - -> [RenamedPat] -> [TcType] -- Excess 'expected types' discarded - -> TcM ([TcPat], - LIE, -- Required by n+k and literal pats - Bag TcTyVar, - Bag (Name, TcId), -- Ids bound by the pattern - LIE) -- Dicts bound by the pattern - -tcPats tc_bndr [] tys = returnTc ([], emptyLIE, emptyBag, emptyBag, emptyLIE) - -tcPats tc_bndr (ty:tys) (pat:pats) - = tcPat tc_bndr ty pat `thenTc` \ (pat', lie_req1, tvs1, ids1, lie_avail1) -> - tcPats tc_bndr tys pats `thenTc` \ (pats', lie_req2, tvs2, ids2, lie_avail2) -> - - returnTc (pat':pats', lie_req1 `plusLIE` lie_req2, - tvs1 `unionBags` tvs2, ids1 `unionBags` ids2, - lie_avail1 `plusLIE` lie_avail2) -\end{code} + g :: (forall a. [a]) -> Bool + g [] = True ------------------------------------------------------- -\begin{code} -tcConstructor pat con_name - = -- Check that it's a constructor - tcLookupDataCon con_name `thenNF_Tc` \ data_con -> +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 - -- Instantiate it - tcInstDataCon (PatOrigin pat) data_con `thenNF_Tc` \ (_, ex_dicts, arg_tys, result_ty, lie_req, ex_lie, ex_tvs) -> +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, becuase we need to decorate +the translated pattern with coercion functions (generated from the subsumption check +by tcSub). - returnTc (data_con, lie_req, ex_tvs, ex_dicts, ex_lie, arg_tys, result_ty) -\end{code} +So for now I'm just insisting on type *equality* in patterns. No subsumption. ------------------------------------------------------- -\begin{code} -tcConPat tc_bndr pat con_name arg_pats pat_ty - = tcAddErrCtxt (patCtxt pat) $ - - -- Check the constructor itself - tcConstructor pat con_name `thenTc` \ (data_con, lie_req1, ex_tvs, ex_dicts, lie_avail1, arg_tys, con_res_ty) -> - - -- Check overall type matches. - -- The pat_ty might be a for-all type, in which - -- case we must instantiate to match - tcSubPat con_res_ty pat_ty `thenTc` \ (co_fn, lie_req2) -> - - -- Check correct arity - let - con_arity = dataConSourceArity data_con - no_of_args = length arg_pats - in - checkTc (con_arity == no_of_args) - (arityErr "Constructor" data_con con_arity no_of_args) `thenTc_` - - -- Check arguments - tcPats tc_bndr arg_pats arg_tys `thenTc` \ (arg_pats', lie_req3, tvs, ids, lie_avail2) -> - - returnTc (co_fn <$> ConPat data_con pat_ty ex_tvs ex_dicts arg_pats', - lie_req1 `plusLIE` lie_req2 `plusLIE` lie_req3, - listToBag ex_tvs `unionBags` tvs, - ids, - lie_avail1 `plusLIE` lie_avail2) -\end{code} +Old notes about desugaring, at a time when pattern coercions were handled: +A SigPat is a type coercion and must be handled one at at 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: -%************************************************************************ -%* * -\subsection{Subsumption} -%* * -%************************************************************************ + 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) -Example: - f :: (forall a. a->a) -> Int -> Int - f (g::Int->Int) y = g y -This is ok: the type signature allows fewer callers than -the (more general) signature f :: (Int->Int) -> Int -> Int -I.e. (forall a. a->a) <= Int -> Int -We end up translating this to: - f = \g' :: (forall a. a->a). let g = g' Int in g' y - -tcSubPat does the work - sig_ty is the signature on the pattern itself - (Int->Int in the example) - expected_ty is the type passed inwards from the context - (forall a. a->a in the example) +We desugar this as follows: -\begin{code} -tcSubPat :: TcSigmaType -> TcHoleType -> TcM (PatCoFn, LIE) - -tcSubPat sig_ty exp_ty - = tcSubOff sig_ty exp_ty `thenTc` \ (co_fn, lie) -> - -- co_fn is a coercion on *expressions*, and we - -- need to make a coercion on *patterns* - if isIdCoercion co_fn then - ASSERT( isEmptyLIE lie ) - returnNF_Tc (idCoercion, emptyLIE) - else - tcGetUnique `thenNF_Tc` \ uniq -> - let - arg_id = mkSysLocal FSLIT("sub") uniq exp_ty - the_fn = DictLam [arg_id] (co_fn <$> HsVar arg_id) - pat_co_fn p = SigPat p exp_ty the_fn - in - returnNF_Tc (mkCoercion pat_co_fn, lie) -\end{code} + 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) %************************************************************************ @@ -466,10 +612,14 @@ tcSubPat sig_ty exp_ty %************************************************************************ \begin{code} -patCtxt pat = hang (ptext SLIT("When checking the pattern:")) - 4 (ppr pat) - -badFieldCon :: Name -> Name -> SDoc +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("When checking the pattern:")) + 4 (ppr pat)) + +badFieldCon :: DataCon -> Name -> SDoc badFieldCon con field = hsep [ptext SLIT("Constructor") <+> quotes (ppr con), ptext SLIT("does not have field"), quotes (ppr field)] @@ -480,5 +630,12 @@ polyPatSig sig_ty 4 (ppr sig_ty) badTypePat pat = ptext SLIT("Illegal type pattern") <+> ppr pat -\end{code} +lazyPatErr pat tvs + = failWithTc $ + hang (ptext SLIT("A lazy (~) pattern connot bind existential type variables")) + 2 (vcat (map pprTcTyVar tvs)) + +inaccessibleAlt msg + = hang (ptext SLIT("Inaccessible case alternative:")) 2 msg +\end{code}