X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=ghc%2Fcompiler%2Ftypecheck%2FTcPat.lhs;h=208af13cc0c36c81d054693498bc918dbc9d0d8d;hb=ff818166a0a06e77becad9e28ed116f3b7f5cc8b;hp=e0cb157bac260f263388e73a2a9e2eb0ed1ae819;hpb=77a8c0dbd5c5ad90fe483cb9ddc2b6ef36d3f4d8;p=ghc-hetmet.git diff --git a/ghc/compiler/typecheck/TcPat.lhs b/ghc/compiler/typecheck/TcPat.lhs index e0cb157..208af13 100644 --- a/ghc/compiler/typecheck/TcPat.lhs +++ b/ghc/compiler/typecheck/TcPat.lhs @@ -4,237 +4,460 @@ \section[TcPat]{Typechecking patterns} \begin{code} -module TcPat ( tcPat, tcPatBndr_NoSigs, badFieldCon, polyPatSig ) where +module TcPat ( tcPat, tcPats, PatCtxt(..), badFieldCon, polyPatSig, refineTyVars ) where #include "HsVersions.h" -import HsSyn ( InPat(..), OutPat(..), HsLit(..), HsExpr(..), Sig(..) ) -import RnHsSyn ( RenamedPat ) -import TcHsSyn ( TcPat, TcId ) - -import TcMonad -import Inst ( Inst, OverloadedLit(..), InstOrigin(..), - emptyLIE, plusLIE, LIE, - newMethod, newOverloadedLit, newDicts, newClassDicts - ) -import Name ( Name, getOccName, getSrcLoc ) -import FieldLabel ( fieldLabelName ) -import TcEnv ( tcLookupValue, tcLookupClassByKey, - tcLookupValueByKey, newLocalId, badCon +import HsSyn ( Pat(..), LPat, HsConDetails(..), HsLit(..), HsOverLit(..), + HsExpr(..), LHsBinds, emptyLHsBinds, isEmptyLHsBinds ) +import HsUtils +import TcHsSyn ( TcId, hsLitType ) +import TcRnMonad +import Inst ( InstOrigin(..), + newMethodFromName, newOverloadedLit, newDicts, + instToId, tcInstStupidTheta, tcSyntaxName ) -import TcType ( TcType, TcTyVar, tcInstTyVars, newTyVarTy ) -import TcMonoType ( tcHsSigType ) -import TcUnify ( unifyTauTy, unifyListTy, unifyTupleTy ) - +import Id ( Id, idType, mkLocalId ) +import Var ( tyVarName ) +import Name ( Name ) +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 ( DataCon, dataConSig, dataConFieldLabels, - dataConSourceArity - ) -import Id ( Id, idType, isDataConWrapId_maybe ) -import Type ( Type, isTauTy, mkTyConApp, mkClassPred, boxedTypeKind ) -import Subst ( substTy, substClasses ) -import TysPrim ( charPrimTy, intPrimTy, floatPrimTy, - doublePrimTy, addrPrimTy - ) -import TysWiredIn ( charTy, stringTy, intTy ) -import Unique ( eqClassOpKey, geClassOpKey, minusClassOpKey, - cCallableClassKey - ) +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 Util ( zipEqual ) +import SrcLoc ( Located(..), SrcSpan, noLoc, unLoc ) +import Maybes ( catMaybes ) +import ErrUtils ( Message ) import Outputable +import FastString \end{code} %************************************************************************ %* * -\subsection{Variable patterns} + External interface %* * %************************************************************************ -\begin{code} --- This is the right function to pass to tcPat when there are no signatures -tcPatBndr_NoSigs binder_name pat_ty - = -- Need to make a new, monomorphic, Id - -- The binder_name is already being used for the polymorphic Id - newLocalId (getOccName binder_name) pat_ty loc `thenNF_Tc` \ bndr_id -> - returnTc bndr_id - where - loc = getSrcLoc binder_name -\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 :: (Name -> TcType -> TcM s TcId) -- How to construct a suitable (monomorphic) - -- Id for variables found in the pattern - -- The TcType is the expected type, see note below - -> RenamedPat - - -> TcType -- Expected type derived from the context - -- In the case of a function with a rank-2 signature, - -- this type might be a forall type. - -- INVARIANT: if it is, the foralls will always be visible, - -- not hidden inside a mutable type variable - - -> TcM s (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 (VarPatIn name) pat_ty - = tc_bndr name pat_ty `thenTc` \ bndr_id -> - returnTc (VarPat bndr_id, emptyLIE, 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` \ bndr_id -> - tcPat tc_bndr pat pat_ty `thenTc` \ (pat', lie_req, tvs, ids, lie_avail) -> - tcAddErrCtxt (patCtxt pat_in) $ - returnTc (AsPat bndr_id pat', lie_req, - tvs, (name, bndr_id) `consBag` ids, lie_avail) - -tcPat tc_bndr WildPatIn pat_ty - = returnTc (WildPat pat_ty, emptyLIE, emptyBag, emptyBag, emptyLIE) - -tcPat tc_bndr (NegPatIn pat) pat_ty - = tcPat tc_bndr (negate_lit pat) pat_ty - where - negate_lit (LitPatIn (HsInt i)) = LitPatIn (HsInt (-i)) - negate_lit (LitPatIn (HsIntPrim i)) = LitPatIn (HsIntPrim (-i)) - negate_lit (LitPatIn (HsFrac f)) = LitPatIn (HsFrac (-f)) - negate_lit (LitPatIn (HsFloatPrim f)) = LitPatIn (HsFloatPrim (-f)) - negate_lit (LitPatIn (HsDoublePrim f)) = LitPatIn (HsDoublePrim (-f)) - negate_lit _ = panic "TcPat:negate_pat" - -tcPat tc_bndr (ParPatIn parend_pat) pat_ty - = tcPat tc_bndr parend_pat pat_ty - -tcPat tc_bndr (SigPatIn pat sig) pat_ty - = tcHsSigType sig `thenTc` \ sig_ty -> - - -- Check that the signature isn't a polymorphic one, which - -- we don't permit (at present, anyway) - checkTc (isTauTy sig_ty) (polyPatSig sig_ty) `thenTc_` - - unifyTauTy pat_ty sig_ty `thenTc_` - tcPat tc_bndr pat sig_ty +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 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@(TuplePatIn pats boxity) pat_ty - = tcAddErrCtxt (patCtxt pat_in) $ - - unifyTupleTy boxity arity pat_ty `thenTc` \ arg_tys -> - tcPats tc_bndr pats arg_tys `thenTc` \ (pats', lie_req, tvs, ids, lie_avail) -> - - -- possibly do the "make all tuple-pats irrefutable" test: - let - unmangled_result = TuplePat pats' boxity +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) + +------------------------ +-- 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) } + +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) } + +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. - - 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 + ; 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 + + -- 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 pat_ty `thenTc` \ (data_con, ex_tvs, dicts, lie_avail1, arg_tys) -> - let - field_tys = zipEqual "tcPat" - (map fieldLabelName (dataConFieldLabels data_con)) - arg_tys - in - - -- Check the fields - tc_fields field_tys rpats `thenTc` \ (rpats', lie_req, tvs, ids, lie_avail2) -> - - returnTc (RecPat data_con pat_ty ex_tvs dicts rpats', - lie_req, - 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 (rpat : rpats) thing_inside + = do { (rpat', tvs1, (rpats', tvs2, res)) + <- tc_field rpat (tc_fields rpats thing_inside) + ; return (rpat':rpats', tvs1 ++ tvs2, 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_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) } - (case [ty | (f,ty) <- field_tys, f == field_label] of + 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 @@ -244,202 +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 boxedTypeKind `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 ) - tcLookupValue field_label `thenNF_Tc` \ sel_id -> - returnTc (sel_id, pat_ty) - ) `thenTc` \ (sel_id, pat_ty) -> + do { sel_id <- tcLookupId field_lbl + ; return (sel_id, pat_ty) } - tcPat tc_bndr rhs_pat pat_ty `thenTc` \ (rhs_pat', lie_req2, tvs2, ids2, lie_avail2) -> - - 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{Non-overloaded literals} -%* * -%************************************************************************ - -\begin{code} -tcPat tc_bndr (LitPatIn lit@(HsChar _)) pat_ty = tcSimpleLitPat lit charTy pat_ty -tcPat tc_bndr (LitPatIn lit@(HsIntPrim _)) pat_ty = tcSimpleLitPat lit intPrimTy pat_ty -tcPat tc_bndr (LitPatIn lit@(HsCharPrim _)) pat_ty = tcSimpleLitPat lit charPrimTy pat_ty -tcPat tc_bndr (LitPatIn lit@(HsStringPrim _)) pat_ty = tcSimpleLitPat lit addrPrimTy pat_ty -tcPat tc_bndr (LitPatIn lit@(HsFloatPrim _)) pat_ty = tcSimpleLitPat lit floatPrimTy pat_ty -tcPat tc_bndr (LitPatIn lit@(HsDoublePrim _)) pat_ty = tcSimpleLitPat lit doublePrimTy pat_ty - -tcPat tc_bndr (LitPatIn lit@(HsLitLit s)) pat_ty - -- cf tcExpr on LitLits - = tcLookupClassByKey cCallableClassKey `thenNF_Tc` \ cCallableClass -> - newDicts (LitLitOrigin (_UNPK_ s)) - [mkClassPred cCallableClass [pat_ty]] `thenNF_Tc` \ (dicts, _) -> - returnTc (LitPat lit pat_ty, dicts, emptyBag, emptyBag, emptyLIE) -\end{code} %************************************************************************ %* * -\subsection{Overloaded patterns: int literals and \tr{n+k} patterns} + Type refinement %* * %************************************************************************ \begin{code} -tcPat tc_bndr pat@(LitPatIn lit@(HsString str)) pat_ty - = unifyTauTy pat_ty stringTy `thenTc_` - tcLookupValueByKey eqClassOpKey `thenNF_Tc` \ sel_id -> - newMethod (PatOrigin pat) sel_id [stringTy] `thenNF_Tc` \ (lie, eq_id) -> - let - comp_op = HsApp (HsVar eq_id) (HsLitOut lit stringTy) - in - returnTc (NPat lit stringTy comp_op, lie, emptyBag, emptyBag, emptyLIE) - - -tcPat tc_bndr pat@(LitPatIn lit@(HsInt i)) pat_ty - = tcOverloadedLitPat pat lit (OverloadedIntegral i) pat_ty +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 } } -tcPat tc_bndr pat@(LitPatIn lit@(HsFrac f)) pat_ty - = tcOverloadedLitPat pat lit (OverloadedFractional f) pat_ty - - -tcPat tc_bndr pat@(NPlusKPatIn name lit@(HsInt i)) pat_ty - = tc_bndr name pat_ty `thenTc` \ bndr_id -> - tcLookupValueByKey geClassOpKey `thenNF_Tc` \ ge_sel_id -> - tcLookupValueByKey minusClassOpKey `thenNF_Tc` \ minus_sel_id -> - - newOverloadedLit origin - (OverloadedIntegral i) pat_ty `thenNF_Tc` \ (over_lit_expr, lie1) -> + where + bind_fn tv | isMetaTyVar tv = WildCard -- Wobbly types behave as wild cards + | otherwise = BindMe +\end{code} - newMethod origin ge_sel_id [pat_ty] `thenNF_Tc` \ (lie2, ge_id) -> - newMethod origin minus_sel_id [pat_ty] `thenNF_Tc` \ (lie3, minus_id) -> +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'. - returnTc (NPlusKPat bndr_id lit pat_ty - (SectionR (HsVar ge_id) over_lit_expr) - (SectionR (HsVar minus_id) over_lit_expr), - lie1 `plusLIE` lie2 `plusLIE` lie3, - emptyBag, unitBag (name, bndr_id), emptyLIE) +\begin{code} +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 - -tcPat tc_bndr (NPlusKPatIn pat other) pat_ty - = panic "TcPat:NPlusKPat: not an HsInt literal" + 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 :: (Name -> TcType -> TcM s TcId) -- How to deal with variables - -> [RenamedPat] -> [TcType] -- Excess 'expected types' discarded - -> TcM s ([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} -tcSimpleLitPat lit lit_ty pat_ty - = unifyTauTy pat_ty lit_ty `thenTc_` - returnTc (LitPat lit lit_ty, emptyLIE, emptyBag, emptyBag, emptyLIE) +In both cases, the function type signature restricts what arguments can be passed +in a call (to polymorphic ones). The pattern type signature then instantiates this +type. For example, in the first case, (forall a. a->a) <= Int -> Int, and we +generate the translated term + f = \x' :: (forall a. a->a). let x = x' Int in x 3 +From a type-system point of view, this is perfectly fine, but it's *very* seldom useful. +And it requires a significant amount of code to implement, becuase we need to decorate +the translated pattern with coercion functions (generated from the subsumption check +by tcSub). -tcOverloadedLitPat pat lit over_lit pat_ty - = newOverloadedLit (PatOrigin pat) over_lit pat_ty `thenNF_Tc` \ (over_lit_expr, lie1) -> - tcLookupValueByKey eqClassOpKey `thenNF_Tc` \ eq_sel_id -> - newMethod origin eq_sel_id [pat_ty] `thenNF_Tc` \ (lie2, eq_id) -> +So for now I'm just insisting on type *equality* in patterns. No subsumption. - returnTc (NPat lit pat_ty (HsApp (HsVar eq_id) - over_lit_expr), - lie1 `plusLIE` lie2, - emptyBag, emptyBag, emptyLIE) - where - origin = PatOrigin pat -\end{code} +Old notes about desugaring, at a time when pattern coercions were handled: ------------------------------------------------------- -\begin{code} -tcConstructor pat con_name pat_ty - = -- Check that it's a constructor - tcLookupValue con_name `thenNF_Tc` \ con_id -> - case isDataConWrapId_maybe con_id of { - Nothing -> failWithTc (badCon con_id); - Just data_con -> - - -- Instantiate it - let - (tvs, _, ex_tvs, ex_theta, arg_tys, tycon) = dataConSig data_con - -- Ignore the theta; overloaded constructors only - -- behave differently when called, not when used for - -- matching. - in - tcInstTyVars (ex_tvs ++ tvs) `thenNF_Tc` \ (all_tvs', ty_args', tenv) -> - let - ex_theta' = substClasses tenv ex_theta - arg_tys' = map (substTy tenv) arg_tys - - n_ex_tvs = length ex_tvs - ex_tvs' = take n_ex_tvs all_tvs' - result_ty = mkTyConApp tycon (drop n_ex_tvs ty_args') - in - newClassDicts (PatOrigin pat) ex_theta' `thenNF_Tc` \ (lie_avail, dicts) -> - - -- Check overall type matches - unifyTauTy pat_ty result_ty `thenTc_` - - returnTc (data_con, ex_tvs', dicts, lie_avail, arg_tys') - } -\end{code} - ------------------------------------------------------- -\begin{code} -tcConPat tc_bndr pat con_name arg_pats pat_ty - = tcAddErrCtxt (patCtxt pat) $ - - -- Check the constructor itself - tcConstructor pat con_name pat_ty `thenTc` \ (data_con, ex_tvs', dicts, lie_avail1, arg_tys') -> - - -- 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_req, tvs, ids, lie_avail2) -> - - returnTc (ConPat data_con pat_ty ex_tvs' dicts arg_pats', - lie_req, - listToBag ex_tvs' `unionBags` tvs, - ids, - lie_avail1 `plusLIE` lie_avail2) -\end{code} +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: + + data T = T1 Int | T2 Bool + f :: (forall a. a -> a) -> T -> t + f (g::Int->Int) (T1 i) = T1 (g i) + f (g::Bool->Bool) (T2 b) = T2 (g b) + +We desugar this as follows: + + f = \ g::(forall a. a->a) t::T -> + let gi = g Int + in case t of { T1 i -> T1 (gi i) + other -> + let gb = g Bool + in case t of { T2 b -> T2 (gb b) + other -> fail }} + +Note that we do not treat the first column of patterns as a +column of variables, because the coerced variables (gi, gb) +would be of different types. So we get rather grotty code. +But I don't think this is a common case, and if it was we could +doubtless improve it. + +Meanwhile, the strategy is: + * treat each SigPat coercion (always non-identity coercions) + as a separate block + * deal with the stuff inside, and then wrap a binding round + the result to bind the new variable (gi, gb, etc) %************************************************************************ @@ -449,18 +612,14 @@ tcConPat tc_bndr pat con_name arg_pats pat_ty %************************************************************************ \begin{code} -patCtxt pat = hang (ptext SLIT("In the pattern:")) - 4 (ppr pat) - -recordLabel field_label - = hang (hcat [ptext SLIT("When matching record field"), ppr field_label]) - 4 (hcat [ptext SLIT("with its immediately enclosing constructor")]) - -recordRhs field_label pat - = hang (ptext SLIT("In the record field pattern")) - 4 (sep [ppr field_label, char '=', 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)] @@ -469,5 +628,14 @@ polyPatSig :: TcType -> SDoc polyPatSig sig_ty = hang (ptext SLIT("Illegal polymorphic type signature in pattern:")) 4 (ppr sig_ty) -\end{code} +badTypePat pat = ptext SLIT("Illegal type pattern") <+> ppr pat + +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}