X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=ghc%2Fcompiler%2Ftypecheck%2FTcPat.lhs;h=ce9e99bedb1be797eede036ab1c24984e59fd610;hb=5d3051c66796dcf884b052f9e4afc3ed19b9f514;hp=2f583bbefe3989501f67950bd5a3b14e78e5cfe1;hpb=da95f4a039f7bc12b625338353df8399dec41c5e;p=ghc-hetmet.git diff --git a/ghc/compiler/typecheck/TcPat.lhs b/ghc/compiler/typecheck/TcPat.lhs index 2f583bb..ce9e99b 100644 --- a/ghc/compiler/typecheck/TcPat.lhs +++ b/ghc/compiler/typecheck/TcPat.lhs @@ -4,44 +4,55 @@ \section[TcPat]{Typechecking patterns} \begin{code} -module TcPat ( tcPat, tcPats, PatCtxt(..), badFieldCon, polyPatSig ) where +module TcPat ( tcPat, tcPats, tcOverloadedLit, + PatCtxt(..), badFieldCon, polyPatSig ) where #include "HsVersions.h" -import HsSyn ( Pat(..), LPat, HsConDetails(..), HsLit(..), HsOverLit(..), - HsExpr(..), LHsBinds, emptyLHsBinds, isEmptyLHsBinds ) -import HsUtils +import {-# SOURCE #-} TcExpr( tcSyntaxOp ) +import HsSyn ( Pat(..), LPat, HsConDetails(..), HsLit(..), HsOverLit(..), HsExpr(..), + LHsBinds, emptyLHsBinds, isEmptyLHsBinds, + collectPatsBinders, nlHsLit ) import TcHsSyn ( TcId, hsLitType ) import TcRnMonad -import Inst ( InstOrigin(..), - newMethodFromName, newOverloadedLit, newDicts, - instToId, tcInstStupidTheta, tcSyntaxName +import Inst ( InstOrigin(..), shortCutFracLit, shortCutIntLit, + newDicts, instToId, tcInstStupidTheta, isHsVar ) import Id ( Id, idType, mkLocalId ) -import Name ( Name ) +import CoreFVs ( idFreeTyVars ) +import Name ( Name, mkSystemVarName ) import TcSimplify ( tcSimplifyCheck, bindInstsOfLocalFuns ) -import TcEnv ( newLocalName, tcExtendIdEnv1, tcExtendTyVarEnv, - tcLookupClass, tcLookupDataCon, tcLookupId ) -import TcMType ( newTyFlexiVarTy, arityErr, tcSkolTyVars ) -import TcType ( TcType, TcTyVar, TcSigmaType, TcTauType, zipTopTvSubst, - SkolemInfo(PatSkol), isSkolemTyVar, pprSkolemTyVar, - mkTyVarTys, mkClassPred, mkTyConApp, isOverloadedTy ) -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(..), tcRefineTys, tcMatchTys ) +import TcEnv ( newLocalName, tcExtendIdEnv1, tcExtendTyVarEnv2, + tcLookupClass, tcLookupDataCon, tcLookupId, refineEnvironment, + tcMetaTy ) +import TcMType ( newFlexiTyVarTy, arityErr, tcInstSkolTyVars, newBoxyTyVar, zonkTcType ) +import TcType ( TcType, TcTyVar, TcSigmaType, TcRhoType, + SkolemInfo(PatSkol), + BoxySigmaType, BoxyRhoType, + pprSkolTvBinding, isRefineableTy, isRigidTy, tcTyVarsOfTypes, mkTyVarTy, lookupTyVar, + emptyTvSubst, substTyVar, substTy, mkTopTvSubst, zipTopTvSubst, zipOpenTvSubst, + mkTyVarTys, mkClassPred, mkTyConApp, isOverloadedTy, + mkFunTy, mkFunTys, exactTyVarsOfTypes, + tidyOpenTypes ) +import VarSet ( elemVarSet, mkVarSet ) +import Kind ( liftedTypeKind, openTypeKind ) +import TcUnify ( boxySplitTyConApp, boxySplitListTy, + unBox, stripBoxyType, zapToMonotype, + boxyMatchTypes, boxyUnify, boxyUnifyList, checkSigTyVarsWrt ) +import TcHsType ( UserTypeCtxt(..), tcPatSig ) +import TysWiredIn ( boolTy, parrTyCon, tupleTyCon ) +import Unify ( MaybeErr(..), gadtRefineTys ) import Type ( substTys, substTheta ) -import CmdLineOpts ( opt_IrrefutableTuples ) +import StaticFlags ( opt_IrrefutableTuples ) import TyCon ( TyCon ) -import DataCon ( DataCon, dataConTyCon, isVanillaDataCon, dataConInstOrigArgTys, +import DataCon ( DataCon, dataConTyCon, isVanillaDataCon, dataConFieldLabels, dataConSourceArity, dataConSig ) -import PrelNames ( eqStringName, eqName, geName, negateName, minusName, - integralClassName ) +import PrelNames ( integralClassName, fromIntegerName, integerTyConName, + fromRationalName, rationalTyConName ) import BasicTypes ( isBoxed ) -import SrcLoc ( Located(..), noLoc, unLoc ) +import SrcLoc ( Located(..), SrcSpan, noLoc ) import ErrUtils ( Message ) +import Util ( takeList, zipEqual ) import Outputable import FastString \end{code} @@ -53,60 +64,90 @@ import FastString %* * %************************************************************************ -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. - -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 :: 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 + -> [LPat Name] -- Patterns, + -> [BoxySigmaType] -- and their types + -> BoxyRhoType -- Result type, + -> (BoxyRhoType -> 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, +-- do the thing inside, use any existentially-bound dictionaries to +-- discharge parts of the returning LIE, and deal with pattern type +-- signatures + +-- 1. Initialise the PatState +-- 2. Check the patterns +-- 3. Apply the refinement +-- 4. Check the body +-- 5. Check that no existentials escape + +tcPats ctxt pats tys res_ty thing_inside + = do { let init_state = PS { pat_ctxt = ctxt, pat_reft = emptyTvSubst } + + ; (pats', ex_tvs, res) <- tc_lpats init_state pats tys $ \ pstate' -> + refineEnvironment (pat_reft pstate') $ + thing_inside (refineType (pat_reft pstate') res_ty) + + ; tcCheckExistentialPat ctxt pats' ex_tvs tys res_ty + + ; returnM (pats', res) } + + +----------------- +tcPat :: PatCtxt + -> LPat Name -> TcType + -> BoxyRhoType -- Result type + -> (BoxyRhoType -> TcM a) -- Checker for body, given its result type + -> TcM (LPat TcId, a) +tcPat ctxt pat pat_ty res_ty thing_inside + = do { ([pat'],thing) <- tcPats ctxt [pat] [pat_ty] res_ty thing_inside + ; return (pat', thing) } + + +----------------- +tcCheckExistentialPat :: PatCtxt + -> [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 ctxt pats [] pat_tys body_ty + = return () -- Short cut for case when there are no existentials + +tcCheckExistentialPat (LetPat _) pats ex_tvs pat_tys body_ty + -- Don't know how to deal with pattern-bound existentials yet + = failWithTc (existentialExplode pats) + +tcCheckExistentialPat ctxt pats ex_tvs pat_tys body_ty + = addErrCtxtM (sigPatCtxt (collectPatsBinders pats) ex_tvs pat_tys) $ + checkSigTyVarsWrt (tcTyVarsOfTypes (body_ty:pat_tys)) ex_tvs + +data PatState = PS { + pat_ctxt :: PatCtxt, + pat_reft :: GadtRefinement -- 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 \end{code} + %************************************************************************ %* * Binders @@ -114,34 +155,28 @@ tcCheckPats ctxt pats tys thing_inside -- A trivial wrapper %************************************************************************ \begin{code} -data PatCtxt = LamPat Bool | LetPat TcSigFun - -- True <=> we are checking the case expression, - -- so can do full-blown refinement - -- False <=> inferring, do no refinement - -------------------- -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 +tcPatBndr :: PatState -> Name -> BoxySigmaType -> TcM TcId +tcPatBndr (PS { pat_ctxt = LamPat }) bndr_name pat_ty + = do { pat_ty' <- unBox pat_ty + -- 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 (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 +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) } | otherwise - = do { mono_name <- newLocalName bndr_name - ; pat_ty' <- zapExpectedType pat_ty argTypeKind + = do { pat_ty' <- unBox pat_ty + ; mono_name <- newLocalName bndr_name ; return (mkLocalId mono_name pat_ty') } @@ -159,40 +194,90 @@ bindInstsOfPatId id thing_inside %************************************************************************ %* * - tc_pat: the main worker function + The main worker functions %* * %************************************************************************ +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. + +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. + \begin{code} -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_lpats :: PatState + -> [LPat Name] + -> [BoxySigmaType] + -> (PatState -> TcM a) + -> TcM ([LPat TcId], [TcTyVar], a) + +tc_lpats pstate pats pat_tys thing_inside + = do { err_ctxt <- getErrCtxt + ; let loop pstate [] [] + = do { res <- thing_inside pstate + ; return ([], [], res) } + + loop pstate (p:ps) (ty:tys) + = do { (p', p_tvs, (ps', ps_tvs, res)) + <- tc_lpat pstate p ty $ \ pstate' -> + setErrCtxt err_ctxt $ + loop pstate' ps tys + -- setErrCtxt: restore context before doing the next pattern + -- See note [Nesting] above + + ; return (p':ps', p_tvs ++ ps_tvs, res) } -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 + loop _ _ _ = pprPanic "tc_lpats" (ppr pats $$ ppr pat_tys) + + ; loop pstate pats pat_tys } + +-------------------- +tc_lpat :: PatState + -> LPat Name + -> BoxySigmaType + -> (PatState -> TcM a) + -> TcM (LPat TcId, [TcTyVar], a) +tc_lpat pstate (L span pat) pat_ty thing_inside + = setSrcSpan span $ + maybeAddErrCtxt (patCtxt pat) $ + do { let pat_ty' = refineType (pat_reft pstate) pat_ty + -- Make sure the result type reflects the current refinement + ; (pat', tvs, res) <- tc_pat pstate 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 + +-------------------- +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) + >> thing_inside pstate) ; 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 +tc_pat pstate (ParPat pat) pat_ty thing_inside + = do { (pat', tvs, res) <- tc_lpat pstate pat pat_ty thing_inside ; return (ParPat pat', tvs, res) } +tc_pat pstate (BangPat pat) pat_ty thing_inside + = do { (pat', tvs, res) <- tc_lpat pstate pat pat_ty thing_inside + ; return (BangPat 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; ... } @@ -203,30 +288,24 @@ tc_pat ctxt (ParPat pat) pat_ty thing_inside -- -- 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 +tc_pat pstate lpat@(LazyPat pat) pat_ty thing_inside + = do { (pat', pat_tvs, res) <- tc_lpat pstate pat pat_ty $ \ _ -> + thing_inside pstate + -- Ignore refined pstate', + -- revert to pstate ; 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 +tc_pat pstate (WildPat _) pat_ty thing_inside + = do { pat_ty' <- unBox pat_ty -- Make sure it's filled in with monotypes + ; res <- thing_inside pstate ; 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) +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 ctxt pat (Check (idType bndr_id)) thing_inside + tc_lpat pstate pat (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 @@ -236,120 +315,95 @@ tc_pat ctxt (AsPat (L nm_loc name) pat) pat_ty thing_inside -- 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 - ; (pat', tvs, res) <- tcExtendTyVarEnv sig_tvs $ - tc_lpat ctxt pat (Check sig_ty) thing_inside - ; return (SigPatOut pat' sig_ty, tvs, 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 pstate pat inner_ty thing_inside + ; return (SigPatOut pat' inner_ty, tvs, res) } -tc_pat ctxt pat@(TypePat ty) pat_ty thing_inside +tc_pat pstate 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 +tc_pat pstate (ListPat pats _) pat_ty thing_inside + = do { elt_ty <- boxySplitListTy pat_ty + ; let elt_tys = takeList pats (repeat elt_ty) + ; (pats', pats_tvs, res) <- tc_lpats pstate pats elt_tys 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 + ; let elt_tys = takeList pats (repeat elt_ty) + ; (pats', pats_tvs, res) <- tc_lpats pstate pats elt_tys 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) <- tc_lpats pstate 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 + ; let unmangled_result = TuplePat pats' boxity pat_ty possibly_mangled_result | opt_IrrefutableTuples && isBoxed boxity = LazyPat (noLoc unmangled_result) | otherwise = unmangled_result - ; ASSERT( length arg_tys == arity ) -- Syntactically enforced + ; ASSERT( length arg_tys == length pats ) -- 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 +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 - ; ty_args <- zapToTyConApp tycon pat_ty - ; (pat', tvs, res) <- tcConPat ctxt data_con tycon ty_args arg_pats thing_inside - ; return (pat', tvs, res) } - + ; tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside } ------------------------ -- 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 +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) } ------------------------ -- 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 +tc_pat pstate pat@(NPat over_lit mb_neg eq _) pat_ty thing_inside + = do { let orig = LiteralOrigin over_lit + ; lit' <- tcOverloadedLit 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 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) + 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) } + +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) ; let pat_ty' = idType bndr_id - origin = LiteralOrigin lit - ; over_lit_expr <- newOverloadedLit origin lit pat_ty' - ; ge <- newMethodFromName origin pat_ty' geName + orig = LiteralOrigin lit + ; lit' <- tcOverloadedLit orig lit pat_ty' - -- The '-' part is re-mappable syntax - ; (_, minus_expr) <- tcSyntaxName origin pat_ty' (minusName, HsVar minus_name) + -- 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') -- 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']] + ; dicts <- newDicts orig [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) } + ; res <- tcExtendIdEnv1 name bndr_id (thing_inside pstate) + ; returnM (NPlusKPat (L nm_loc bndr_id) lit' ge' minus', [], res) } \end{code} @@ -361,89 +415,116 @@ tc_pat ctxt pat@(NPlusKPatIn (L nm_loc name) lit@(HsIntegral i _) minus_name) pa %************************************************************************ \begin{code} -tcConPat :: PatCtxt -> DataCon -> TyCon -> [TcTauType] - -> HsConDetails Name (LPat Name) -> TcM a +tcConPat :: PatState -> SrcSpan -> DataCon -> TyCon + -> BoxySigmaType -- Type of the pattern + -> HsConDetails Name (LPat Name) -> (PatState -> TcM a) -> TcM (Pat TcId, [TcTyVar], a) -tcConPat ctxt data_con tycon ty_args arg_pats thing_inside +tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside | isVanillaDataCon data_con - = do { let arg_tys = dataConInstOrigArgTys data_con ty_args + = do { ty_args <- boxySplitTyConApp tycon pat_ty + ; let (tvs, _, arg_tys, _, _) = dataConSig data_con + arg_tvs = exactTyVarsOfTypes arg_tys + -- See Note [Silly type synonyms in smart-app] in TcExpr + -- for why we must use exactTyVarsOfTypes + inst_prs = zipEqual "tcConPat" tvs ty_args + subst = mkTopTvSubst inst_prs + arg_tys' = substTys subst arg_tys + unconstrained_ty_args = [ty_arg | (tv,ty_arg) <- inst_prs, + not (tv `elemVarSet` arg_tvs)] + ; mapM unBox unconstrained_ty_args -- Zap these to monotypes ; 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 data_con [] [] emptyLHsBinds + ; traceTc (text "tcConPat" <+> vcat [ppr data_con, ppr ty_args, ppr arg_tys']) + ; (arg_pats', tvs, res) <- tcConArgs pstate data_con arg_pats arg_tys' thing_inside + ; return (ConPatOut (L con_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' - ; tcInstStupidTheta data_con tv_tys' + = do { ty_args <- boxySplitTyConApp tycon pat_ty + ; span <- getSrcSpanM -- The whole pattern + + -- Instantiate the constructor type variables and result type + ; let (tvs, theta, arg_tys, _, res_tys) = dataConSig data_con + arg_tvs = exactTyVarsOfTypes arg_tys + -- See Note [Silly type synonyms in smart-app] in TcExpr + -- for why we must use exactTyVarsOfTypes + skol_info = PatSkol data_con span + arg_flags = [ tv `elemVarSet` arg_tvs | tv <- tvs ] + ; tvs' <- tcInstSkolTyVars skol_info tvs + ; let res_tys' = substTys (zipTopTvSubst tvs (mkTyVarTys tvs')) res_tys -- Do type refinement! - ; traceTc (text "tcGadtPat" <+> vcat [ppr data_con, ppr tvs', ppr arg_tys', ppr res_tys', + ; traceTc (text "tcGadtPat" <+> vcat [ppr data_con, ppr tvs', 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 (tcConArgs ctxt data_con arg_pats arg_tys' thing_inside) - + ; refineAlt pstate data_con tvs' arg_flags res_tys' ty_args + $ \ pstate' tv_tys' -> do + + -- ToDo: arg_tys should be boxy, but I don't think theta' should be, + -- or the tv_tys' in the call to tcInstStupidTheta + { let tenv' = zipTopTvSubst tvs tv_tys' + theta' = substTheta tenv' theta + arg_tys' = substTys tenv' arg_tys -- Boxy types + + ; ((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 pstate' data_con arg_pats arg_tys' thing_inside } + + ; dicts <- newDicts (SigOrigin skol_info) theta' ; dict_binds <- tcSimplifyCheck doc tvs' dicts lie_req - ; return (ConPatOut data_con + ; return (ConPatOut (L con_span data_con) tvs' (map instToId dicts) dict_binds arg_pats' (mkTyConApp tycon ty_args), - tvs' ++ inner_tvs, res) } } + tvs' ++ inner_tvs, res) + } } where doc = ptext SLIT("existential context for") <+> quotes (ppr data_con) -tcConArgs :: PatCtxt -> DataCon +tcConArgs :: PatState -> DataCon -> HsConDetails Name (LPat Name) -> [TcSigmaType] - -> TcM a + -> (PatState -> TcM a) -> TcM (HsConDetails TcId (LPat Id), [TcTyVar], a) -tcConArgs ctxt data_con (PrefixCon arg_pats) arg_tys thing_inside +tcConArgs pstate 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 + ; (arg_pats', tvs, res) <- tc_lpats pstate 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 +tcConArgs pstate 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 + ; ([p1',p2'], tvs, res) <- tc_lpats pstate [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 +tcConArgs pstate data_con (RecCon rpats) arg_tys thing_inside + = do { (rpats', tvs, res) <- tc_fields pstate rpats thing_inside ; return (RecCon rpats', tvs, res) } where - tc_fields :: [(Located Name, LPat Name)] -> TcM a + tc_fields :: PatState -> [(Located Name, LPat Name)] + -> (PatState -> TcM a) -> TcM ([(Located TcId, LPat TcId)], [TcTyVar], a) - tc_fields [] thing_inside - = do { res <- thing_inside + tc_fields pstate [] thing_inside + = do { res <- thing_inside pstate ; return ([], [], res) } - tc_fields (rpat : rpats) thing_inside + tc_fields pstate (rpat : rpats) thing_inside = do { (rpat', tvs1, (rpats', tvs2, res)) - <- tc_field rpat (tc_fields rpats thing_inside) + <- tc_field pstate rpat $ \ pstate' -> + tc_fields pstate' rpats thing_inside ; return (rpat':rpats', tvs1 ++ tvs2, res) } - tc_field (field_lbl, pat) thing_inside + tc_field pstate (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 + ; (pat', tvs, res) <- tc_lpat pstate pat pat_ty thing_inside ; return ((sel_id, pat'), tvs, res) } find_field_ty field_lbl @@ -458,7 +539,7 @@ tcConArgs ctxt data_con (RecCon rpats) arg_tys thing_inside -- If foo isn't one of R's fields, we don't want to crash when -- typechecking the "a+b". [] -> do { addErrTc (badFieldCon data_con field_lbl) - ; bogus_ty <- newTyFlexiVarTy liftedTypeKind + ; bogus_ty <- newFlexiTyVarTy liftedTypeKind ; return (error "Bogus selector Id", bogus_ty) } -- The normal case, when the field comes from the right constructor @@ -481,26 +562,135 @@ tcConArgs ctxt data_con (RecCon rpats) arg_tys thing_inside %************************************************************************ \begin{code} -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 - ; let refiner | can_i_refine ctxt = tcRefineTys - | otherwise = tcMatchTys - ; case refiner ex_tvs 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 } } +refineAlt :: PatState + -> DataCon -- For tracing only + -> [TcTyVar] -- Type variables from pattern + -> [Bool] -- Flags indicating which type variables occur + -- in the type of at least one argument + -> [TcType] -- Result types from the pattern + -> [BoxySigmaType] -- Result types from the scrutinee (context) + -> (PatState -> [BoxySigmaType] -> TcM a) + -- Possibly-refined existentials + -> TcM a +refineAlt pstate con pat_tvs arg_flags pat_res_tys ctxt_res_tys thing_inside + | not (all isRigidTy ctxt_res_tys) + -- The context is not a rigid type, so we do no type refinement here. + = do { let arg_tvs = mkVarSet [ tv | (tv, True) <- pat_tvs `zip` arg_flags] + subst = boxyMatchTypes arg_tvs pat_res_tys ctxt_res_tys + + res_tvs = tcTyVarsOfTypes pat_res_tys + -- The tvs are (already) all fresh skolems. We need a + -- fresh skolem for each type variable (to bind in the pattern) + -- even if it's refined away by the type refinement + find_inst tv + | not (tv `elemVarSet` res_tvs) = return (mkTyVarTy tv) + | Just boxy_ty <- lookupTyVar subst tv = return boxy_ty + | otherwise = do { tv <- newBoxyTyVar openTypeKind + ; return (mkTyVarTy tv) } + ; pat_tys' <- mapM find_inst pat_tvs + + -- Do the thing inside + ; res <- thing_inside pstate pat_tys' + + -- Unbox the types that have been filled in by the thing_inside + -- I.e. the ones whose type variables are mentioned in at least one arg + ; let strip ty in_arg_tv | in_arg_tv = stripBoxyType ty + | otherwise = return ty + ; pat_tys'' <- zipWithM strip pat_tys' arg_flags + ; let subst = zipOpenTvSubst pat_tvs pat_tys'' + ; boxyUnifyList (substTys subst pat_res_tys) ctxt_res_tys + + ; return res } -- All boxes now filled + + | otherwise -- The context is rigid, so we can do type refinement + = case gadtRefineTys (pat_reft pstate) con pat_tvs pat_res_tys ctxt_res_tys of + Failed msg -> failWithTc (inaccessibleAlt msg) + Succeeded (new_subst, all_bound_here) + | all_bound_here -- All the new bindings are for pat_tvs, so no need + -- to refine the environment or pstate + -> do { traceTc trace_msg + ; thing_inside pstate pat_tvs' } + | otherwise -- New bindings affect the context, so pass down pstate'. + -- DO NOT refine the envt, because we might be inside a + -- lazy pattern + -> do { traceTc trace_msg + ; thing_inside pstate' pat_tvs' } + where + pat_tvs' = map (substTyVar new_subst) pat_tvs + pstate' = pstate { pat_reft = new_subst } + trace_msg = text "refineTypes:match" <+> ppr con <+> ppr new_subst + +refineType :: GadtRefinement -> BoxyRhoType -> BoxyRhoType +-- Refine the type if it is rigid +refineType reft ty + | isRefineableTy ty = substTy reft ty + | otherwise = ty +\end{code} - where - can_i_refine (LamPat can_refine) = can_refine - can_i_refine other_ctxt = False + +%************************************************************************ +%* * + 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)) } \end{code} + %************************************************************************ %* * Note [Pattern coercions] @@ -573,9 +763,37 @@ patCtxt :: Pat Name -> Maybe Message -- Not all patterns are worth pushing a con patCtxt (VarPat _) = Nothing patCtxt (ParPat _) = Nothing patCtxt (AsPat _ _) = Nothing -patCtxt pat = Just (hang (ptext SLIT("When checking the pattern:")) +patCtxt pat = Just (hang (ptext SLIT("In the pattern:")) 4 (ppr pat)) +----------------------------------------------- + +existentialExplode pats + = 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 (vcat (map ppr pats)) + +sigPatCtxt bound_ids bound_tvs tys tidy_env + = -- tys is (body_ty : pat_tys) + mapM zonkTcType tys `thenM` \ tys' -> + let + (env1, tidy_tys) = tidyOpenTypes tidy_env (map idType show_ids) + (_env2, tidy_body_ty : tidy_pat_tys) = tidyOpenTypes env1 tys' + in + returnM (env1, + 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 + ]) + where + show_ids = filter is_interesting bound_ids + is_interesting id = any (`elemVarSet` idFreeTyVars 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 + badFieldCon :: DataCon -> Name -> SDoc badFieldCon con field = hsep [ptext SLIT("Constructor") <+> quotes (ppr con), @@ -591,9 +809,7 @@ 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 get tvs)) - where - get tv = ASSERT( isSkolemTyVar tv ) pprSkolemTyVar tv + 2 (vcat (map pprSkolTvBinding tvs)) inaccessibleAlt msg = hang (ptext SLIT("Inaccessible case alternative:")) 2 msg