X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcPat.lhs;h=1759257a04f898b627da20e04e98c68f5ccf6aa6;hb=79011516105291b58324ce71a87f6bb26a131090;hp=3c1c3bacdca2949f222cf14f785c6dd8d617adf2;hpb=af20907ae1c9901b457cbab57e9d533e66e5aa07;p=ghc-hetmet.git diff --git a/compiler/typecheck/TcPat.lhs b/compiler/typecheck/TcPat.lhs index 3c1c3ba..1759257 100644 --- a/compiler/typecheck/TcPat.lhs +++ b/compiler/typecheck/TcPat.lhs @@ -1,60 +1,56 @@ % +% (c) The University of Glasgow 2006 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998 % -\section[TcPat]{Typechecking patterns} + +TcPat: Typechecking patterns \begin{code} -module TcPat ( tcPat, tcPats, tcOverloadedLit, - PatCtxt(..), badFieldCon, polyPatSig ) where +{-# OPTIONS -w #-} +-- The above warning supression flag is a temporary kludge. +-- While working on this module you are encouraged to remove it and fix +-- any warnings in the module. See +-- http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings +-- for details + +module TcPat ( tcLetPat, tcLamPat, tcLamPats, tcProcPat, tcOverloadedLit, + addDataConStupidTheta, badFieldCon, polyPatSig ) where #include "HsVersions.h" -import {-# SOURCE #-} TcExpr( tcSyntaxOp ) -import HsSyn ( Pat(..), LPat, HsConDetails(..), HsLit(..), HsOverLit(..), HsExpr(..), - LHsBinds, emptyLHsBinds, isEmptyLHsBinds, - collectPatsBinders, nlHsLit ) -import TcHsSyn ( TcId, hsLitType ) +import {-# SOURCE #-} TcExpr( tcSyntaxOp, tcInferRho) + +import HsSyn +import TcHsSyn import TcRnMonad -import Inst ( InstOrigin(..), shortCutFracLit, shortCutIntLit, - newDicts, instToId, tcInstStupidTheta, isHsVar - ) -import Id ( Id, idType, mkLocalId ) -import CoreFVs ( idFreeTyVars ) -import Name ( Name, mkSystemVarName ) -import TcSimplify ( tcSimplifyCheck, bindInstsOfLocalFuns ) -import TcEnv ( newLocalName, tcExtendIdEnv1, tcExtendTyVarEnv2, - tcLookupClass, tcLookupDataCon, 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 StaticFlags ( opt_IrrefutableTuples ) -import TyCon ( TyCon ) -import DataCon ( DataCon, dataConTyCon, isVanillaDataCon, - dataConFieldLabels, dataConSourceArity, dataConSig ) -import PrelNames ( integralClassName, fromIntegerName, integerTyConName, - fromRationalName, rationalTyConName ) -import BasicTypes ( isBoxed ) -import SrcLoc ( Located(..), SrcSpan, noLoc ) -import ErrUtils ( Message ) -import Util ( takeList, zipEqual ) +import Inst +import Id +import Var +import CoreFVs +import Name +import TcSimplify +import TcEnv +import TcMType +import TcType +import VarSet +import TcUnify +import TcHsType +import TysWiredIn +import Type +import Coercion +import StaticFlags +import TyCon +import DataCon +import DynFlags +import PrelNames +import BasicTypes hiding (SuccessFlag(..)) +import SrcLoc +import ErrUtils +import Util +import Maybes import Outputable import FastString +import Monad \end{code} @@ -65,12 +61,27 @@ import FastString %************************************************************************ \begin{code} -tcPats :: PatCtxt - -> [LPat Name] -- Patterns, - -> [BoxySigmaType] -- and their types - -> BoxyRhoType -- Result type, - -> (BoxyRhoType -> TcM a) -- and the checker for the body - -> TcM ([LPat TcId], a) +tcLetPat :: (Name -> Maybe TcRhoType) + -> LPat Name -> BoxySigmaType + -> TcM a + -> TcM (LPat TcId, a) +tcLetPat sig_fn pat pat_ty thing_inside + = do { let init_state = PS { pat_ctxt = LetPat sig_fn, + pat_eqs = False } + ; (pat', ex_tvs, res) <- tc_lpat pat pat_ty init_state + (\ _ -> thing_inside) + + -- Don't know how to deal with pattern-bound existentials yet + ; checkTc (null ex_tvs) (existentialExplode pat) + + ; return (pat', res) } + +----------------- +tcLamPats :: [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, @@ -80,36 +91,48 @@ tcPats :: PatCtxt -- 1. Initialise the PatState -- 2. Check the patterns --- 3. Apply the refinement --- 4. Check the body --- 5. Check that no existentials escape +-- 3. Check the body +-- 4. Check that no existentials escape -tcPats ctxt pats tys res_ty thing_inside - = do { let init_state = PS { pat_ctxt = ctxt, pat_reft = emptyTvSubst } +tcLamPats pats tys res_ty thing_inside + = tc_lam_pats LamPat (zipEqual "tcLamPats" pats tys) + res_ty thing_inside - ; (pats', ex_tvs, res) <- tc_lpats init_state pats tys $ \ pstate' -> - refineEnvironment (pat_reft pstate') $ - thing_inside (refineType (pat_reft pstate') res_ty) +tcLamPat :: LPat Name -> BoxySigmaType + -> BoxyRhoType -- Result type + -> (BoxyRhoType -> TcM a) -- Checker for body, given its result type + -> TcM (LPat TcId, a) - ; tcCheckExistentialPat ctxt pats' ex_tvs tys res_ty - - ; returnM (pats', res) } +tcProcPat = tc_lam_pat ProcPat +tcLamPat = tc_lam_pat LamPat +tc_lam_pat ctxt pat pat_ty res_ty thing_inside + = do { ([pat'],thing) <- tc_lam_pats ctxt [(pat, pat_ty)] res_ty thing_inside + ; return (pat', thing) } ----------------- -tcPat :: PatCtxt - -> LPat Name -> BoxySigmaType - -> 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) } +tc_lam_pats :: PatCtxt + -> [(LPat Name,BoxySigmaType)] + -> BoxyRhoType -- Result type + -> (BoxyRhoType -> TcM a) -- Checker for body, given its result type + -> TcM ([LPat TcId], a) +tc_lam_pats ctxt pat_ty_prs res_ty thing_inside + = do { let init_state = PS { pat_ctxt = ctxt, pat_eqs = False } + + ; (pats', ex_tvs, res) <- do { traceTc (text "tc_lam_pats" <+> (ppr pat_ty_prs $$ ppr res_ty)) + ; tcMultiple tc_lpat_pr pat_ty_prs init_state $ \ pstate' -> + if (pat_eqs pstate' && (not $ isRigidTy res_ty)) + then nonRigidResult res_ty + else thing_inside res_ty } + + ; let tys = map snd pat_ty_prs + ; tcCheckExistentialPat pats' ex_tvs tys res_ty + + ; return (pats', res) } ----------------- -tcCheckExistentialPat :: PatCtxt - -> [LPat TcId] -- Patterns (just for error message) +tcCheckExistentialPat :: [LPat TcId] -- Patterns (just for error message) -> [TcTyVar] -- Existentially quantified tyvars bound by pattern -> [BoxySigmaType] -- Types of the patterns -> BoxyRhoType -- Type of the body of the match @@ -121,24 +144,24 @@ tcCheckExistentialPat :: PatCtxt -- 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 +tcCheckExistentialPat 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) $ +tcCheckExistentialPat pats ex_tvs pat_tys body_ty + = addErrCtxtM (sigPatCtxt pats ex_tvs pat_tys body_ty) $ checkSigTyVarsWrt (tcTyVarsOfTypes (body_ty:pat_tys)) ex_tvs data PatState = PS { pat_ctxt :: PatCtxt, - pat_reft :: GadtRefinement -- Binds rigid TcTyVars to their refinements + pat_eqs :: Bool -- <=> there are any equational constraints + -- Used at the end to say whether the result + -- type must be rigid } data PatCtxt = LamPat + | ProcPat -- The pattern in (proc pat -> ...) + -- see Note [Arrows and patterns] | LetPat (Name -> Maybe TcRhoType) -- Used for let(rec) bindings patSigCtxt :: PatState -> UserTypeCtxt @@ -156,8 +179,19 @@ patSigCtxt other = LamPatSigCtxt \begin{code} tcPatBndr :: PatState -> Name -> BoxySigmaType -> TcM TcId -tcPatBndr (PS { pat_ctxt = LamPat }) bndr_name pat_ty - = do { pat_ty' <- unBox 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 (Id.mkLocalId mono_name mono_ty) } + + | otherwise + = do { pat_ty' <- unBoxPatBndrType pat_ty bndr_name + ; mono_name <- newLocalName bndr_name + ; return (Id.mkLocalId mono_name pat_ty') } + +tcPatBndr (PS { pat_ctxt = _lam_or_proc }) bndr_name pat_ty + = do { pat_ty' <- unBoxPatBndrType pat_ty bndr_name -- We have an undecorated binder, so we do rule ABS1, -- by unboxing the boxy type, forcing any un-filled-in -- boxes to become monotypes @@ -166,18 +200,7 @@ tcPatBndr (PS { pat_ctxt = LamPat }) bndr_name pat_ty -- f t = case t of { MkT g -> ... } -- Here, the 'g' must get type (forall a. a->a) from the -- MkT context - ; return (mkLocalId bndr_name pat_ty') } - -tcPatBndr (PS { pat_ctxt = LetPat lookup_sig }) bndr_name pat_ty - | Just mono_ty <- lookup_sig bndr_name - = do { mono_name <- newLocalName bndr_name - ; boxyUnify mono_ty pat_ty - ; return (mkLocalId mono_name mono_ty) } - - | otherwise - = do { pat_ty' <- unBox pat_ty - ; mono_name <- newLocalName bndr_name - ; return (mkLocalId mono_name pat_ty') } + ; return (Id.mkLocalId bndr_name pat_ty') } ------------------- @@ -189,6 +212,32 @@ bindInstsOfPatId id thing_inside = do { (res, lie) <- getLIE thing_inside ; binds <- bindInstsOfLocalFuns lie [id] ; return (res, binds) } + +------------------- +unBoxPatBndrType ty name = unBoxArgType ty (ptext SLIT("The variable") <+> quotes (ppr name)) +unBoxWildCardType ty = unBoxArgType ty (ptext SLIT("A wild-card pattern")) +unBoxViewPatType ty pat = unBoxArgType ty (ptext SLIT("The view pattern") <+> ppr pat) + +unBoxArgType :: BoxyType -> SDoc -> TcM TcType +-- In addition to calling unbox, unBoxArgType ensures that the type is of ArgTypeKind; +-- that is, it can't be an unboxed tuple. For example, +-- case (f x) of r -> ... +-- should fail if 'f' returns an unboxed tuple. +unBoxArgType ty pp_this + = do { ty' <- unBox ty -- Returns a zonked type + + -- Neither conditional is strictly necesssary (the unify alone will do) + -- but they improve error messages, and allocate fewer tyvars + ; if isUnboxedTupleType ty' then + failWithTc msg + else if isSubArgTypeKind (typeKind ty') then + return ty' + else do -- OpenTypeKind, so constrain it + { ty2 <- newFlexiTyVarTy argTypeKind + ; unifyType ty' ty2 + ; return ty' }} + where + msg = pp_this <+> ptext SLIT("cannot be bound to an unboxed tuple") \end{code} @@ -200,7 +249,7 @@ bindInstsOfPatId id thing_inside Note [Nesting] ~~~~~~~~~~~~~~ -tcPat takes a "thing inside" over which the patter scopes. This is partly +tcPat takes a "thing inside" over which the pattern scopes. This is partly so that tcPat can extend the environment for the thing_inside, but also so that constraints arising in the thing_inside can be discharged by the pattern. @@ -211,54 +260,57 @@ Hence the getErrCtxt/setErrCtxt stuff in tc_lpats. \begin{code} -------------------- -tc_lpats :: PatState - -> [LPat Name] - -> [BoxySigmaType] - -> (PatState -> TcM a) - -> TcM ([LPat TcId], [TcTyVar], a) - -tc_lpats pstate pats pat_tys thing_inside +type Checker inp out = forall r. + inp + -> PatState + -> (PatState -> TcM r) + -> TcM (out, [TcTyVar], r) + +tcMultiple :: Checker inp out -> Checker [inp] [out] +tcMultiple tc_pat args pstate thing_inside = do { err_ctxt <- getErrCtxt - ; let loop pstate [] [] + ; let loop pstate [] = do { res <- thing_inside pstate ; return ([], [], res) } - loop pstate (p:ps) (ty:tys) + loop pstate (arg:args) = do { (p', p_tvs, (ps', ps_tvs, res)) - <- tc_lpat pstate p ty $ \ pstate' -> + <- tc_pat arg pstate $ \ pstate' -> setErrCtxt err_ctxt $ - loop pstate' ps tys + loop pstate' args -- setErrCtxt: restore context before doing the next pattern -- See note [Nesting] above ; return (p':ps', p_tvs ++ ps_tvs, res) } - loop _ _ _ = pprPanic "tc_lpats" (ppr pats $$ ppr pat_tys) - - ; loop pstate pats pat_tys } + ; loop pstate args } -------------------- -tc_lpat :: PatState - -> LPat Name - -> BoxySigmaType - -> (PatState -> TcM a) - -> TcM (LPat TcId, [TcTyVar], a) -tc_lpat pstate (L span pat) pat_ty thing_inside +tc_lpat_pr :: (LPat Name, BoxySigmaType) + -> PatState + -> (PatState -> TcM a) + -> TcM (LPat TcId, [TcTyVar], a) +tc_lpat_pr (pat, ty) = tc_lpat pat ty + +tc_lpat :: LPat Name + -> BoxySigmaType + -> PatState + -> (PatState -> TcM a) + -> TcM (LPat TcId, [TcTyVar], a) +tc_lpat (L span pat) pat_ty pstate thing_inside = setSrcSpan span $ maybeAddErrCtxt (patCtxt pat) $ - do { let 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 + do { (pat', tvs, res) <- tc_pat pstate pat pat_ty thing_inside ; return (L span pat', tvs, res) } - -------------------- 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 + -> 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 @@ -271,14 +323,14 @@ tc_pat pstate (VarPat name) pat_ty thing_inside ; return (pat', [], res) } tc_pat pstate (ParPat pat) pat_ty thing_inside - = do { (pat', tvs, res) <- tc_lpat pstate pat pat_ty thing_inside + = do { (pat', tvs, res) <- tc_lpat pat pat_ty pstate thing_inside ; return (ParPat pat', tvs, res) } tc_pat pstate (BangPat pat) pat_ty thing_inside - = do { (pat', tvs, res) <- tc_lpat pstate pat pat_ty thing_inside + = do { (pat', tvs, res) <- tc_lpat pat pat_ty pstate thing_inside ; return (BangPat pat', tvs, res) } --- There's a wrinkle with irrefuatable patterns, namely that we +-- There's a wrinkle with irrefutable patterns, namely that we -- must not propagate type refinement from them. For example -- data T a where { T1 :: Int -> T Int; ... } -- f :: T a -> Int -> a @@ -288,24 +340,48 @@ tc_pat pstate (BangPat 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 +-- +-- Note [Hopping the LIE in lazy patterns] +-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +-- In a lazy pattern, we must *not* discharge constraints from the RHS +-- from dictionaries bound in the pattern. E.g. +-- f ~(C x) = 3 +-- We can't discharge the Num constraint from dictionaries bound by +-- the pattern C! +-- +-- So we have to make the constraints from thing_inside "hop around" +-- the pattern. Hence the getLLE and extendLIEs later. + 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 + = do { (pat', pat_tvs, (res,lie)) + <- tc_lpat pat pat_ty pstate $ \ _ -> + getLIE (thing_inside pstate) + -- Ignore refined pstate', revert to pstate + ; extendLIEs lie + -- getLIE/extendLIEs: see Note [Hopping the LIE in lazy patterns] + + -- Check no existentials ; if (null pat_tvs) then return () else lazyPatErr lpat pat_tvs + + -- Check that the pattern has a lifted type + ; pat_tv <- newBoxyTyVar liftedTypeKind + ; boxyUnify pat_ty (mkTyVarTy pat_tv) + ; return (LazyPat pat', [], res) } +tc_pat _ p@(QuasiQuotePat _) _ _ + = pprPanic "Should never see QuasiQuotePat in type checker" (ppr p) + tc_pat pstate (WildPat _) pat_ty thing_inside - = do { pat_ty' <- unBox pat_ty -- Make sure it's filled in with monotypes + = do { pat_ty' <- unBoxWildCardType pat_ty -- Make sure it's filled in with monotypes ; res <- thing_inside pstate ; return (WildPat pat_ty', [], res) } tc_pat pstate (AsPat (L nm_loc name) pat) pat_ty thing_inside = do { bndr_id <- setSrcSpan nm_loc (tcPatBndr pstate name pat_ty) ; (pat', tvs, res) <- tcExtendIdEnv1 name bndr_id $ - tc_lpat pstate pat (idType bndr_id) thing_inside + tc_lpat pat (idType bndr_id) pstate 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 @@ -315,12 +391,40 @@ tc_pat pstate (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 pstate (orig@(ViewPat expr pat _)) overall_pat_ty thing_inside + = do { -- morally, expr must have type + -- `forall a1...aN. OPT' -> B` + -- where overall_pat_ty is an instance of OPT'. + -- Here, we infer a rho type for it, + -- which replaces the leading foralls and constraints + -- with fresh unification variables. + (expr',expr'_inferred) <- tcInferRho expr + -- next, we check that expr is coercible to `overall_pat_ty -> pat_ty` + ; let expr'_expected = \ pat_ty -> (mkFunTy overall_pat_ty pat_ty) + -- tcSubExp: expected first, offered second + -- returns coercion + -- + -- NOTE: this forces pat_ty to be a monotype (because we use a unification + -- variable to find it). this means that in an example like + -- (view -> f) where view :: _ -> forall b. b + -- we will only be able to use view at one instantation in the + -- rest of the view + ; (expr_coerc, pat_ty) <- tcInfer $ \ pat_ty -> + tcSubExp ViewPatOrigin (expr'_expected pat_ty) expr'_inferred + + -- pattern must have pat_ty + ; (pat', tvs, res) <- tc_lpat pat pat_ty pstate thing_inside + -- this should get zonked later on, but we unBox it here + -- so that we do the same checks as above + ; annotation_ty <- unBoxViewPatType overall_pat_ty orig + ; return (ViewPat (mkLHsWrap expr_coerc expr') pat' annotation_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 + tc_lpat pat inner_ty pstate thing_inside ; return (SigPatOut pat' inner_ty, tvs, res) } tc_pat pstate pat@(TypePat ty) pat_ty thing_inside @@ -329,33 +433,44 @@ tc_pat pstate pat@(TypePat ty) pat_ty thing_inside ------------------------ -- Lists, tuples, arrays 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) } + = do { (elt_ty, coi) <- boxySplitListTy pat_ty + ; let scoi = mkSymCoI coi + ; (pats', pats_tvs, res) <- tcMultiple (\p -> tc_lpat p elt_ty) + pats pstate thing_inside + ; return (mkCoPatCoI scoi (ListPat pats' elt_ty) pat_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) } + = do { (elt_ty, coi) <- boxySplitPArrTy pat_ty + ; let scoi = mkSymCoI coi + ; (pats', pats_tvs, res) <- tcMultiple (\p -> tc_lpat p elt_ty) + pats pstate thing_inside + ; when (null pats) (zapToMonotype pat_ty >> return ()) -- c.f. ExplicitPArr in TcExpr + ; return (mkCoPatCoI scoi (PArrPat pats' elt_ty) pat_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 + = do { let tc = tupleTyCon boxity (length pats) + ; (arg_tys, coi) <- boxySplitTyConApp tc pat_ty + ; let scoi = mkSymCoI coi + ; (pats', pats_tvs, res) <- tcMultiple tc_lpat_pr (pats `zip` arg_tys) + pstate thing_inside -- Under flag control turn a pattern (x,y,z) into ~(x,y,z) -- so that we can experiment with lazy tuple-matching. -- This is a pretty odd place to make the switch, but -- it was easy to do. - ; let unmangled_result = TuplePat pats' boxity pat_ty + ; let pat_ty' = mkTyConApp tc arg_tys + -- pat_ty /= pat_ty iff coi /= IdCo + unmangled_result = TuplePat pats' boxity pat_ty' possibly_mangled_result - | opt_IrrefutableTuples && isBoxed boxity = LazyPat (noLoc unmangled_result) - | otherwise = unmangled_result + | opt_IrrefutableTuples && + isBoxed boxity = LazyPat (noLoc unmangled_result) + | otherwise = unmangled_result - ; ASSERT( length arg_tys == length pats ) -- Syntactically enforced - return (possibly_mangled_result, pats_tvs, res) } + ; ASSERT( length arg_tys == length pats ) -- Syntactically enforced + return (mkCoPatCoI scoi possibly_mangled_result pat_ty, pats_tvs, res) + } ------------------------ -- Data constructors @@ -367,13 +482,20 @@ tc_pat pstate pat_in@(ConPatIn (L con_span con_name) arg_pats) pat_ty thing_insi ------------------------ -- Literal patterns tc_pat pstate (LitPat simple_lit) pat_ty thing_inside - = do { boxyUnify (hsLitType simple_lit) pat_ty + = do { let lit_ty = hsLitType simple_lit + ; coi <- boxyUnify lit_ty pat_ty + -- coi is of kind: lit_ty ~ pat_ty ; res <- thing_inside pstate - ; returnM (LitPat simple_lit, [], res) } + ; span <- getSrcSpanM + -- pattern coercions have to + -- be of kind: pat_ty ~ lit_ty + -- hence, sym coi + ; return (mkCoPatCoI (mkSymCoI coi) (LitPat simple_lit) pat_ty, + [], res) } ------------------------ -- Overloaded patterns: n, and n+k -tc_pat pstate pat@(NPat over_lit mb_neg eq _) pat_ty thing_inside +tc_pat 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) @@ -384,7 +506,7 @@ tc_pat pstate pat@(NPat over_lit mb_neg eq _) pat_ty thing_inside 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) } + ; return (NPat lit' mb_neg' eq', [], res) } tc_pat pstate pat@(NPlusKPat (L nm_loc name) lit ge minus) pat_ty thing_inside = do { bndr_id <- setSrcSpan nm_loc (tcPatBndr pstate name pat_ty) @@ -399,11 +521,12 @@ tc_pat pstate pat@(NPlusKPat (L nm_loc name) lit ge minus) pat_ty thing_inside -- The Report says that n+k patterns must be in Integral -- We may not want this when using re-mappable syntax, though (ToDo?) ; icls <- tcLookupClass integralClassName - ; dicts <- newDicts orig [mkClassPred icls [pat_ty']] - ; extendLIEs dicts + ; instStupidTheta orig [mkClassPred icls [pat_ty']] ; res <- tcExtendIdEnv1 name bndr_id (thing_inside pstate) - ; returnM (NPlusKPat (L nm_loc bndr_id) lit' ge' minus', [], res) } + ; return (NPlusKPat (L nm_loc bndr_id) lit' ge' minus', [], res) } + +tc_pat _ _other_pat _ _ = panic "tc_pat" -- ConPatOut, SigPatOut, VarPatOut \end{code} @@ -414,119 +537,228 @@ tc_pat pstate pat@(NPlusKPat (L nm_loc name) lit ge minus) pat_ty thing_inside %* * %************************************************************************ +[Pattern matching indexed data types] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider the following declarations: + + data family Map k :: * -> * + data instance Map (a, b) v = MapPair (Map a (Pair b v)) + +and a case expression + + case x :: Map (Int, c) w of MapPair m -> ... + +As explained by [Wrappers for data instance tycons] in MkIds.lhs, the +worker/wrapper types for MapPair are + + $WMapPair :: forall a b v. Map a (Map a b v) -> Map (a, b) v + $wMapPair :: forall a b v. Map a (Map a b v) -> :R123Map a b v + +So, the type of the scrutinee is Map (Int, c) w, but the tycon of MapPair is +:R123Map, which means the straight use of boxySplitTyConApp would give a type +error. Hence, the smart wrapper function boxySplitTyConAppWithFamily calls +boxySplitTyConApp with the family tycon Map instead, which gives us the family +type list {(Int, c), w}. To get the correct split for :R123Map, we need to +unify the family type list {(Int, c), w} with the instance types {(a, b), v} +(provided by tyConFamInst_maybe together with the family tycon). This +unification yields the substitution [a -> Int, b -> c, v -> w], which gives us +the split arguments for the representation tycon :R123Map as {Int, c, w} + +In other words, boxySplitTyConAppWithFamily implicitly takes the coercion + + Co123Map a b v :: {Map (a, b) v :=: :R123Map a b v} + +moving between representation and family type into account. To produce type +correct Core, this coercion needs to be used to case the type of the scrutinee +from the family to the representation type. This is achieved by +unwrapFamInstScrutinee using a CoPat around the result pattern. + +Now it might appear seem as if we could have used the previous GADT type +refinement infrastructure of refineAlt and friends instead of the explicit +unification and CoPat generation. However, that would be wrong. Why? The +whole point of GADT refinement is that the refinement is local to the case +alternative. In contrast, the substitution generated by the unification of +the family type list and instance types needs to be propagated to the outside. +Imagine that in the above example, the type of the scrutinee would have been +(Map x w), then we would have unified {x, w} with {(a, b), v}, yielding the +substitution [x -> (a, b), v -> w]. In contrast to GADT matching, the +instantiation of x with (a, b) must be global; ie, it must be valid in *all* +alternatives of the case expression, whereas in the GADT case it might vary +between alternatives. + +RIP GADT refinement: refinements have been replaced by the use of explicit +equality constraints that are used in conjunction with implication constraints +to express the local scope of GADT refinements. + \begin{code} +-- Running example: +-- MkT :: forall a b c. (a:=:[b]) => b -> c -> T a +-- with scrutinee of type (T ty) + tcConPat :: PatState -> SrcSpan -> DataCon -> TyCon -> BoxySigmaType -- Type of the pattern - -> HsConDetails Name (LPat Name) -> (PatState -> TcM a) + -> HsConPatDetails Name -> (PatState -> TcM a) -> TcM (Pat TcId, [TcTyVar], a) tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside - | isVanillaDataCon data_con - = 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 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 { 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 res_tys', - text "ty-args:" <+> ppr ty_args ]) - ; 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 + = do { let (univ_tvs, ex_tvs, eq_spec, eq_theta, dict_theta, arg_tys, _) + = dataConFullSig data_con + skol_info = PatSkol data_con + origin = SigOrigin skol_info + full_theta = eq_theta ++ dict_theta + + -- Instantiate the constructor type variables [a->ty] + -- This may involve doing a family-instance coercion, and building a + -- wrapper + ; (ctxt_res_tys, coi) <- boxySplitTyConAppWithFamily tycon pat_ty + ; let sym_coi = mkSymCoI coi -- boxy split coercion oriented wrongly + pat_ty' = mkTyConApp tycon ctxt_res_tys + -- pat_ty' /= pat_ty iff coi /= IdCo + + wrap_res_pat res_pat = mkCoPatCoI sym_coi uwScrut pat_ty + where + uwScrut = unwrapFamInstScrutinee tycon ctxt_res_tys res_pat + + ; traceTc $ case sym_coi of + IdCo -> text "sym_coi:IdCo" + ACo co -> text "sym_coi: ACoI" <+> ppr co + + -- Add the stupid theta + ; addDataConStupidTheta data_con ctxt_res_tys + + ; ex_tvs' <- tcInstSkolTyVars skol_info ex_tvs + -- Get location from monad, not from ex_tvs + + ; let tenv = zipTopTvSubst (univ_tvs ++ ex_tvs) + (ctxt_res_tys ++ mkTyVarTys ex_tvs') + arg_tys' = substTys tenv arg_tys + + ; if null ex_tvs && null eq_spec && null full_theta + then do { -- The common case; no class bindings etc + -- (see Note [Arrows and patterns]) + (arg_pats', inner_tvs, res) <- tcConArgs data_con arg_tys' + arg_pats pstate thing_inside + ; let res_pat = ConPatOut { pat_con = L con_span data_con, + pat_tvs = [], pat_dicts = [], + pat_binds = emptyLHsBinds, + pat_args = arg_pats', + pat_ty = pat_ty' } + + ; return (wrap_res_pat res_pat, inner_tvs, res) } + + else do -- The general case, with existential, and local equality + -- constraints + { checkTc (case pat_ctxt pstate of { ProcPat -> False; other -> True }) + (existentialProcPat data_con) + + -- Need to test for rigidity if *any* constraints in theta as class + -- constraints may have superclass equality constraints. However, + -- we don't want to check for rigidity if we got here only because + -- ex_tvs was non-null. +-- ; unless (null theta') $ + -- FIXME: AT THE MOMENT WE CHEAT! We only perform the rigidity test + -- if we explicit or implicit (by a GADT def) have equality + -- constraints. + ; let eq_preds = [mkEqPred (mkTyVarTy tv, ty) | (tv, ty) <- eq_spec] + theta' = substTheta tenv (eq_preds ++ full_theta) + -- order is *important* as we generate the list of + -- dictionary binders from theta' + no_equalities = not (any isEqPred theta') + pstate' | no_equalities = pstate + | otherwise = pstate { pat_eqs = True } + + ; unless no_equalities (checkTc (isRigidTy pat_ty) + (nonRigidMatch data_con)) ; ((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 (L con_span data_con) - tvs' (map instToId dicts) dict_binds - arg_pats' (mkTyConApp tycon ty_args), - tvs' ++ inner_tvs, res) + tcConArgs data_con arg_tys' arg_pats pstate' thing_inside + + ; loc <- getInstLoc origin + ; dicts <- newDictBndrs loc theta' + ; dict_binds <- tcSimplifyCheckPat loc ex_tvs' dicts lie_req + + ; let res_pat = ConPatOut { pat_con = L con_span data_con, + pat_tvs = ex_tvs', + pat_dicts = map instToVar dicts, + pat_binds = dict_binds, + pat_args = arg_pats', pat_ty = pat_ty' } + ; return (wrap_res_pat res_pat, ex_tvs' ++ inner_tvs, res) } } where - doc = ptext SLIT("existential context for") <+> quotes (ppr data_con) - -tcConArgs :: PatState -> DataCon - -> HsConDetails Name (LPat Name) -> [TcSigmaType] - -> (PatState -> TcM a) - -> TcM (HsConDetails TcId (LPat Id), [TcTyVar], a) - -tcConArgs pstate data_con (PrefixCon arg_pats) arg_tys thing_inside + -- Split against the family tycon if the pattern constructor + -- belongs to a family instance tycon. + boxySplitTyConAppWithFamily tycon pat_ty = + traceTc traceMsg >> + case tyConFamInst_maybe tycon of + Nothing -> boxySplitTyConApp tycon pat_ty + Just (fam_tycon, instTys) -> + do { (scrutinee_arg_tys, coi) <- boxySplitTyConApp fam_tycon pat_ty + ; (_, freshTvs, subst) <- tcInstTyVars (tyConTyVars tycon) + ; boxyUnifyList (substTys subst instTys) scrutinee_arg_tys + ; return (freshTvs, coi) + } + where + traceMsg = sep [ text "tcConPat:boxySplitTyConAppWithFamily:" <+> + ppr tycon <+> ppr pat_ty + , text " family instance:" <+> + ppr (tyConFamInst_maybe tycon) + ] + + -- Wraps the pattern (which must be a ConPatOut pattern) in a coercion + -- pattern if the tycon is an instance of a family. + -- + unwrapFamInstScrutinee :: TyCon -> [Type] -> Pat Id -> Pat Id + unwrapFamInstScrutinee tycon args pat + | Just co_con <- tyConFamilyCoercion_maybe tycon +-- , not (isNewTyCon tycon) -- newtypes are explicitly unwrapped by + -- the desugarer + -- NB: We can use CoPat directly, rather than mkCoPat, as we know the + -- coercion is not the identity; mkCoPat is inconvenient as it + -- wants a located pattern. + = CoPat (WpCast $ mkTyConApp co_con args) -- co fam ty to repr ty + (pat {pat_ty = mkTyConApp tycon args}) -- representation type + pat_ty -- family inst type + | otherwise + = pat + + +tcConArgs :: DataCon -> [TcSigmaType] + -> Checker (HsConPatDetails Name) (HsConPatDetails Id) + +tcConArgs data_con arg_tys (PrefixCon arg_pats) pstate 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) <- tc_lpats pstate arg_pats arg_tys thing_inside + ; let pats_w_tys = zipEqual "tcConArgs" arg_pats arg_tys + ; (arg_pats', tvs, res) <- tcMultiple tcConArg pats_w_tys + pstate thing_inside ; return (PrefixCon arg_pats', tvs, res) } where con_arity = dataConSourceArity data_con no_of_args = length arg_pats -tcConArgs pstate data_con (InfixCon p1 p2) arg_tys thing_inside +tcConArgs data_con arg_tys (InfixCon p1 p2) pstate thing_inside = do { checkTc (con_arity == 2) -- Check correct arity (arityErr "Constructor" data_con con_arity 2) - ; ([p1',p2'], tvs, res) <- tc_lpats pstate [p1,p2] arg_tys thing_inside + ; let [arg_ty1,arg_ty2] = arg_tys -- This can't fail after the arity check + ; ([p1',p2'], tvs, res) <- tcMultiple tcConArg [(p1,arg_ty1),(p2,arg_ty2)] + pstate thing_inside ; return (InfixCon p1' p2', tvs, res) } where con_arity = dataConSourceArity data_con -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) } +tcConArgs data_con other_args (InfixCon p1 p2) pstate thing_inside + = pprPanic "tcConArgs" (ppr data_con) -- InfixCon always has two arguments + +tcConArgs data_con arg_tys (RecCon (HsRecFields rpats dd)) pstate thing_inside + = do { (rpats', tvs, res) <- tcMultiple tc_field rpats pstate thing_inside + ; return (RecCon (HsRecFields rpats' dd), tvs, res) } where - tc_fields :: PatState -> [(Located Name, LPat Name)] - -> (PatState -> TcM a) - -> TcM ([(Located TcId, LPat TcId)], [TcTyVar], a) - tc_fields pstate [] thing_inside - = do { res <- thing_inside pstate - ; return ([], [], res) } - - tc_fields pstate (rpat : rpats) thing_inside - = do { (rpat', tvs1, (rpats', tvs2, res)) - <- tc_field pstate rpat $ \ pstate' -> - tc_fields pstate' rpats thing_inside - ; return (rpat':rpats', tvs1 ++ tvs2, res) } - - tc_field pstate (field_lbl, pat) thing_inside + tc_field :: Checker (HsRecField FieldLabel (LPat Name)) (HsRecField TcId (LPat TcId)) + tc_field (HsRecField field_lbl pat pun) pstate thing_inside = do { (sel_id, pat_ty) <- wrapLocFstM find_field_ty field_lbl - ; (pat', tvs, res) <- tc_lpat pstate pat pat_ty thing_inside - ; return ((sel_id, pat'), tvs, res) } + ; (pat', tvs, res) <- tcConArg (pat, pat_ty) pstate thing_inside + ; return (HsRecField sel_id pat' pun, tvs, res) } + find_field_ty :: FieldLabel -> TcM (Id, TcType) find_field_ty field_lbl = case [ty | (f,ty) <- field_tys, f == field_lbl] of @@ -545,88 +777,60 @@ tcConArgs pstate data_con (RecCon rpats) arg_tys thing_inside -- The normal case, when the field comes from the right constructor (pat_ty : extras) -> ASSERT( null extras ) - do { sel_id <- tcLookupId field_lbl + do { sel_id <- tcLookupField field_lbl ; return (sel_id, pat_ty) } + field_tys :: [(FieldLabel, TcType)] 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} - -%************************************************************************ -%* * - Type refinement -%* * -%************************************************************************ +tcConArg :: Checker (LPat Name, BoxySigmaType) (LPat Id) +tcConArg (arg_pat, arg_ty) pstate thing_inside + = tc_lpat arg_pat arg_ty pstate thing_inside +\end{code} \begin{code} -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 +addDataConStupidTheta :: DataCon -> [TcType] -> TcM () +-- Instantiate the "stupid theta" of the data con, and throw +-- the constraints into the constraint set +addDataConStupidTheta data_con inst_tys + | null stupid_theta = return () + | otherwise = instStupidTheta origin inst_theta + where + origin = OccurrenceOf (dataConName data_con) + -- The origin should always report "occurrence of C" + -- even when C occurs in a pattern + stupid_theta = dataConStupidTheta data_con + tenv = zipTopTvSubst (dataConUnivTyVars data_con) inst_tys + inst_theta = substTheta tenv stupid_theta \end{code} +Note [Arrows and patterns] +~~~~~~~~~~~~~~~~~~~~~~~~~~ +(Oct 07) Arrow noation has the odd property that it involves "holes in the scope". +For example: + expr :: Arrow a => a () Int + expr = proc (y,z) -> do + x <- term -< y + expr' -< x + +Here the 'proc (y,z)' binding scopes over the arrow tails but not the +arrow body (e.g 'term'). As things stand (bogusly) all the +constraints from the proc body are gathered together, so constraints +from 'term' will be seen by the tcPat for (y,z). But we must *not* +bind constraints from 'term' here, becuase the desugarer will not make +these bindings scope over 'term'. + +The Right Thing is not to confuse these constraints together. But for +now the Easy Thing is to ensure that we do not have existential or +GADT constraints in a 'proc', and to short-cut the constraint +simplification for such vanilla patterns so that it binds no +constraints. Hence the 'fast path' in tcConPat; but it's also a good +plan for ordinary vanilla patterns to bypass the constraint +simplification step. + %************************************************************************ %* * @@ -644,7 +848,7 @@ tcOverloadedLit :: InstOrigin -> HsOverLit Name -> BoxyRhoType -> TcM (HsOverLit TcId) -tcOverloadedLit orig lit@(HsIntegral i fi) res_ty +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, @@ -652,16 +856,16 @@ tcOverloadedLit orig lit@(HsIntegral i fi) res_ty -- 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)))) } + ; return (HsIntegral i (HsApp (noLoc fi') (nlHsLit (HsInteger i integer_ty))) res_ty) } | Just expr <- shortCutIntLit i res_ty - = return (HsIntegral i expr) + = return (HsIntegral i expr res_ty) | otherwise = do { expr <- newLitInst orig lit res_ty - ; return (HsIntegral i expr) } + ; return (HsIntegral i expr res_ty) } -tcOverloadedLit orig lit@(HsFractional r fr) res_ty +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) @@ -669,14 +873,27 @@ tcOverloadedLit orig lit@(HsFractional r fr) res_ty -- 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)))) } + ; return (HsFractional r (HsApp (noLoc fr') (nlHsLit (HsRat r rat_ty))) res_ty) } | Just expr <- shortCutFracLit r res_ty - = return (HsFractional r expr) + = return (HsFractional r expr res_ty) + + | otherwise + = do { expr <- newLitInst orig lit res_ty + ; return (HsFractional r expr res_ty) } + +tcOverloadedLit orig lit@(HsIsString s fr _) res_ty + | not (fr `isHsVar` fromStringName) -- c.f. HsIntegral case + = do { str_ty <- tcMetaTy stringTyConName + ; fr' <- tcSyntaxOp orig fr (mkFunTy str_ty res_ty) + ; return (HsIsString s (HsApp (noLoc fr') (nlHsLit (HsString s))) res_ty) } + + | Just expr <- shortCutStringLit s res_ty + = return (HsIsString s expr res_ty) | otherwise = do { expr <- newLitInst orig lit res_ty - ; return (HsFractional r expr) } + ; return (HsIsString s expr res_ty) } newLitInst :: InstOrigin -> HsOverLit Name -> BoxyRhoType -> TcM (HsExpr TcId) newLitInst orig lit res_ty -- Make a LitInst @@ -684,7 +901,8 @@ newLitInst orig lit res_ty -- Make a LitInst ; 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 + lit_inst = LitInst {tci_name = lit_nm, tci_lit = lit, + tci_ty = res_tau, tci_loc = loc} ; extendLIE lit_inst ; return (HsVar (instToId lit_inst)) } \end{code} @@ -767,28 +985,29 @@ patCtxt pat = Just (hang (ptext SLIT("In the pattern:")) ----------------------------------------------- -existentialExplode pats +existentialExplode pat = hang (vcat [text "My brain just exploded.", text "I can't handle pattern bindings for existentially-quantified constructors.", + text "Instead, use a case-expression, or do-notation, to unpack the constructor.", 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, + 4 (ppr pat) + +sigPatCtxt pats bound_tvs pat_tys body_ty tidy_env + = do { pat_tys' <- mapM zonkTcType pat_tys + ; body_ty' <- zonkTcType body_ty + ; let (env1, tidy_tys) = tidyOpenTypes tidy_env (map idType show_ids) + (env2, tidy_pat_tys) = tidyOpenTypes env1 pat_tys' + (env3, tidy_body_ty) = tidyOpenType env2 body_ty' + ; return (env3, sep [ptext SLIT("When checking an existential match that binds"), nest 4 (vcat (zipWith ppr_id show_ids tidy_tys)), ptext SLIT("The pattern(s) have type(s):") <+> vcat (map ppr tidy_pat_tys), ptext SLIT("The body has type:") <+> ppr tidy_body_ty - ]) + ]) } where + bound_ids = collectPatsBinders pats show_ids = filter is_interesting bound_ids - is_interesting id = any (`elemVarSet` idFreeTyVars id) bound_tvs + is_interesting id = any (`elemVarSet` varTypeTyVars id) bound_tvs ppr_id id ty = ppr id <+> dcolon <+> ppr ty -- Don't zonk the types so we get the separate, un-unified versions @@ -801,15 +1020,32 @@ badFieldCon con field polyPatSig :: TcType -> SDoc polyPatSig sig_ty = hang (ptext SLIT("Illegal polymorphic type signature in pattern:")) - 4 (ppr sig_ty) + 2 (ppr sig_ty) badTypePat pat = ptext SLIT("Illegal type pattern") <+> ppr pat +existentialProcPat :: DataCon -> SDoc +existentialProcPat con + = hang (ptext SLIT("Illegal constructor") <+> quotes (ppr con) <+> ptext SLIT("in a 'proc' pattern")) + 2 (ptext SLIT("Proc patterns cannot use existentials or GADTs")) + lazyPatErr pat tvs = failWithTc $ - hang (ptext SLIT("A lazy (~) pattern connot bind existential type variables")) + hang (ptext SLIT("A lazy (~) pattern cannot bind existential type variables")) 2 (vcat (map pprSkolTvBinding tvs)) +nonRigidMatch con + = hang (ptext SLIT("GADT pattern match in non-rigid context for") <+> quotes (ppr con)) + 2 (ptext SLIT("Solution: add a type signature")) + +nonRigidResult res_ty + = do { env0 <- tcInitTidyEnv + ; let (env1, res_ty') = tidyOpenType env0 res_ty + msg = hang (ptext SLIT("GADT pattern match with non-rigid result type") + <+> quotes (ppr res_ty')) + 2 (ptext SLIT("Solution: add a type signature")) + ; failWithTcM (env1, msg) } + inaccessibleAlt msg = hang (ptext SLIT("Inaccessible case alternative:")) 2 msg \end{code}