X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcPat.lhs;h=6cb177ed54044994ed4f878637eb83d368a7a582;hp=3c1c3bacdca2949f222cf14f785c6dd8d617adf2;hb=ab22f4e6456820c1b5169d75f5975a94e61f54ce;hpb=af20907ae1c9901b457cbab57e9d533e66e5aa07 diff --git a/compiler/typecheck/TcPat.lhs b/compiler/typecheck/TcPat.lhs index 3c1c3ba..6cb177e 100644 --- a/compiler/typecheck/TcPat.lhs +++ b/compiler/typecheck/TcPat.lhs @@ -1,58 +1,45 @@ % +% (c) The University of Glasgow 2006 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998 % -\section[TcPat]{Typechecking patterns} + +TcPat: Typechecking patterns \begin{code} -module TcPat ( tcPat, tcPats, tcOverloadedLit, - PatCtxt(..), badFieldCon, polyPatSig ) where +module TcPat ( tcLetPat, tcLamPat, tcLamPats, 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 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 TcGadt +import Type +import StaticFlags +import TyCon +import DataCon +import PrelNames +import BasicTypes hiding (SuccessFlag(..)) +import SrcLoc +import ErrUtils +import Util +import Maybes import Outputable import FastString \end{code} @@ -65,12 +52,26 @@ 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_reft = emptyRefinement } + ; (pat', ex_tvs, res) <- tc_lpat pat pat_ty init_state (\ _ -> thing_inside) + + -- Don't know how to deal with pattern-bound existentials yet + ; checkTc (null ex_tvs) (existentialExplode pat) + + ; return (pat', res) } + +----------------- +tcLamPats :: [LPat Name] -- Patterns, + -> [BoxySigmaType] -- and their types + -> BoxyRhoType -- Result type, + -> ((Refinement, BoxyRhoType) -> TcM a) -- and the checker for the body + -> TcM ([LPat TcId], a) -- This is the externally-callable wrapper function -- Typecheck the patterns, extend the environment to bind the variables, @@ -80,36 +81,42 @@ tcPats :: PatCtxt -- 1. Initialise the PatState -- 2. Check the patterns --- 3. Apply the refinement +-- 3. Apply the refinement to the environment and result type -- 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 } +tcLamPats pats tys res_ty thing_inside + = tc_lam_pats (zipEqual "tcLamPats" pats tys) + (emptyRefinement, res_ty) thing_inside - ; (pats', ex_tvs, res) <- tc_lpats init_state pats tys $ \ pstate' -> +tcLamPat :: LPat Name -> BoxySigmaType + -> (Refinement,BoxyRhoType) -- Result type + -> ((Refinement,BoxyRhoType) -> TcM a) -- Checker for body, given its result type + -> TcM (LPat TcId, a) +tcLamPat pat pat_ty res_ty thing_inside + = do { ([pat'],thing) <- tc_lam_pats [(pat, pat_ty)] res_ty thing_inside + ; return (pat', thing) } + +----------------- +tc_lam_pats :: [(LPat Name,BoxySigmaType)] + -> (Refinement,BoxyRhoType) -- Result type + -> ((Refinement,BoxyRhoType) -> TcM a) -- Checker for body, given its result type + -> TcM ([LPat TcId], a) +tc_lam_pats pat_ty_prs (reft, res_ty) thing_inside + = do { let init_state = PS { pat_ctxt = LamPat, pat_reft = reft } + + ; (pats', ex_tvs, res) <- tcMultiple tc_lpat_pr pat_ty_prs init_state $ \ pstate' -> refineEnvironment (pat_reft pstate') $ - thing_inside (refineType (pat_reft pstate') res_ty) + thing_inside (pat_reft pstate', res_ty) - ; tcCheckExistentialPat ctxt pats' ex_tvs tys res_ty + ; let tys = map snd pat_ty_prs + ; tcCheckExistentialPat pats' ex_tvs tys res_ty ; returnM (pats', res) } ----------------- -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) } - - ------------------ -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,20 +128,16 @@ 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 (collectPatsBinders 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_reft :: Refinement -- Binds rigid TcTyVars to their refinements } data PatCtxt @@ -157,7 +160,7 @@ 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 + = 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 +169,18 @@ 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') } + ; return (Id.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) } + ; return (Id.mkLocalId mono_name mono_ty) } | otherwise - = do { pat_ty' <- unBox pat_ty + = do { pat_ty' <- unBoxPatBndrType pat_ty bndr_name ; mono_name <- newLocalName bndr_name - ; return (mkLocalId mono_name pat_ty') } + ; return (Id.mkLocalId mono_name pat_ty') } ------------------- @@ -189,6 +192,31 @@ 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")) + +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} @@ -211,46 +239,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 + do { let (coercion, 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) } + -- We must do this here, so that it correctly ``sees'' all + -- the refinements to the left. Example: + -- Suppose C :: forall a. T a -> a -> Foo + -- Pattern C a p1 True + -- So p1 might refine 'a' to True, and the True + -- pattern had better see it. + ; (pat', tvs, res) <- tc_pat pstate pat pat_ty' thing_inside + ; return (mkCoPat coercion (L span pat') pat_ty, tvs, res) } -------------------- tc_pat :: PatState @@ -271,14 +310,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 @@ -289,23 +328,29 @@ 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 tc_pat pstate lpat@(LazyPat pat) pat_ty thing_inside - = do { (pat', pat_tvs, res) <- tc_lpat pstate pat pat_ty $ \ _ -> + = do { (pat', pat_tvs, res) <- tc_lpat pat pat_ty pstate $ \ _ -> thing_inside pstate -- Ignore refined pstate', -- revert to pstate + -- Check no existentials ; if (null pat_tvs) then return () else lazyPatErr lpat pat_tvs + + -- Check that the pattern has a lifted type + ; pat_tv <- newBoxyTyVar liftedTypeKind + ; boxyUnify pat_ty (mkTyVarTy pat_tv) + ; return (LazyPat pat', [], res) } tc_pat pstate (WildPat _) pat_ty thing_inside - = do { pat_ty' <- 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 @@ -320,7 +365,7 @@ tc_pat pstate (AsPat (L nm_loc name) pat) pat_ty thing_inside 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 @@ -330,20 +375,21 @@ 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 + ; (pats', pats_tvs, res) <- tcMultiple (\p -> tc_lpat p elt_ty) + pats pstate thing_inside ; return (ListPat pats' elt_ty, pats_tvs, res) } tc_pat pstate (PArrPat pats _) pat_ty thing_inside = do { [elt_ty] <- boxySplitTyConApp parrTyCon pat_ty - ; let elt_tys = takeList pats (repeat elt_ty) - ; (pats', pats_tvs, res) <- tc_lpats pstate pats elt_tys thing_inside + ; (pats', pats_tvs, res) <- tcMultiple (\p -> tc_lpat p elt_ty) + pats pstate thing_inside ; ifM (null pats) (zapToMonotype pat_ty) -- c.f. ExplicitPArr in TcExpr ; return (PArrPat pats' elt_ty, pats_tvs, res) } tc_pat pstate (TuplePat pats boxity _) pat_ty thing_inside = do { arg_tys <- boxySplitTyConApp (tupleTyCon boxity (length pats)) pat_ty - ; (pats', pats_tvs, res) <- tc_lpats pstate pats arg_tys thing_inside + ; (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. @@ -399,11 +445,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) } + +tc_pat _ _other_pat _ _ = panic "tc_pat" -- DictPat, ConPatOut, SigPatOut, VarPatOut \end{code} @@ -414,119 +461,186 @@ 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 existing 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. + +In fact, if we have a data instance declaration defining a GADT, eq_spec will +be non-empty and we will get a mixture of global instantiations and local +refinement from a single match. This neatly reflects that, as soon as we +have constrained the type of the scrutinee to the required type index, all +further type refinement is local to the alternative. + \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) -> 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 + = do { span <- getSrcSpanM -- Span for the whole pattern + ; let (univ_tvs, ex_tvs, eq_spec, theta, arg_tys) = dataConFullSig data_con skol_info = PatSkol data_con span - 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 + origin = SigOrigin skol_info + + -- Instantiate the constructor type variables [a->ty] + ; ctxt_res_tys <- boxySplitTyConAppWithFamily tycon pat_ty + ; ex_tvs' <- tcInstSkolTyVars skol_info ex_tvs + ; let tenv = zipTopTvSubst (univ_tvs ++ ex_tvs) + (ctxt_res_tys ++ mkTyVarTys ex_tvs') + eq_spec' = substEqSpec tenv eq_spec + theta' = substTheta tenv theta + arg_tys' = substTys tenv arg_tys + + ; co_vars <- newCoVars eq_spec' -- Make coercion variables + ; pstate' <- refineAlt data_con pstate ex_tvs' co_vars pat_ty ; ((arg_pats', inner_tvs, res), lie_req) <- getLIE $ - 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 <- tcSimplifyCheck doc ex_tvs' dicts lie_req + + ; addDataConStupidTheta data_con ctxt_res_tys + + ; return + (unwrapFamInstScrutinee tycon ctxt_res_tys $ + ConPatOut { pat_con = L con_span data_con, + pat_tvs = ex_tvs' ++ co_vars, + pat_dicts = map instToId dicts, + pat_binds = dict_binds, + pat_args = arg_pats', pat_ty = pat_ty }, + ex_tvs' ++ inner_tvs, res) + } 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 + -- representation 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 <- boxySplitTyConApp fam_tycon pat_ty + ; (_, freshTvs, subst) <- tcInstTyVars (tyConTyVars tycon) + ; boxyUnifyList (substTys subst instTys) scrutinee_arg_tys + ; return freshTvs + } + 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 (WpCo $ 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 (HsConDetails Name (LPat Name)) + (HsConDetails Id (LPat 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_ty1,arg_ty2] (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 + ; ([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 +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 rpats) pstate thing_inside + = do { (rpats', tvs, res) <- tcMultiple tc_field rpats pstate thing_inside ; return (RecCon rpats', 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 + -- doc comments are typechecked to Nothing here + tc_field :: Checker (HsRecField FieldLabel (LPat Name)) (HsRecField TcId (LPat TcId)) + tc_field (HsRecField field_lbl pat _) 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 (mkRecField sel_id pat', 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,13 +659,37 @@ 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). + +tcConArg :: Checker (LPat Name, BoxySigmaType) (LPat Id) +tcConArg (arg_pat, arg_ty) pstate thing_inside + = tc_lpat arg_pat arg_ty pstate thing_inside + -- NB: the tc_lpat will refine pat_ty if necessary + -- based on the current pstate, which may include + -- refinements from peer argument patterns to the left +\end{code} + +\begin{code} +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} @@ -562,69 +700,47 @@ tcConArgs pstate data_con (RecCon rpats) arg_tys thing_inside %************************************************************************ \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 +refineAlt :: DataCon -- For tracing only + -> PatState + -> [TcTyVar] -- Existentials + -> [CoVar] -- Equational constraints + -> BoxySigmaType -- Pattern type + -> TcM PatState + +refineAlt con pstate ex_tvs [] pat_ty + = return pstate -- Common case: no equational constraints + +refineAlt con pstate ex_tvs co_vars pat_ty + | not (isRigidTy pat_ty) + = failWithTc (nonRigidMatch con) + -- We are matching against a GADT constructor with non-trivial + -- constraints, but pattern type is wobbly. For now we fail. + -- We can make sense of this, however: + -- Suppose MkT :: forall a b. (a:=:[b]) => b -> T a + -- (\x -> case x of { MkT v -> v }) + -- We can infer that x must have type T [c], for some wobbly 'c' + -- and translate to + -- (\(x::T [c]) -> case x of + -- MkT b (g::([c]:=:[b])) (v::b) -> v `cast` sym g + -- To implement this, we'd first instantiate the equational + -- constraints with *wobbly* type variables for the existentials; + -- then unify these constraints to make pat_ty the right shape; + -- then proceed exactly as in the rigid case + + | otherwise -- In the rigid case, we perform type refinement + = case gadtRefine (pat_reft pstate) ex_tvs co_vars of { + Failed msg -> failWithTc (inaccessibleAlt msg) ; + Succeeded reft -> do { traceTc trace_msg + ; return (pstate { pat_reft = reft }) } + -- DO NOT refine the envt right away, because we + -- might be inside a lazy pattern. Instead, refine pstate + where + + trace_msg = text "refineAlt:match" <+> + vcat [ ppr con <+> ppr ex_tvs, + ppr [(v, tyVarKind v) | v <- co_vars], + ppr reft] + } \end{code} @@ -767,25 +883,24 @@ 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 "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 bound_ids 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 show_ids = filter is_interesting bound_ids is_interesting id = any (`elemVarSet` idFreeTyVars id) bound_tvs @@ -810,6 +925,10 @@ lazyPatErr pat tvs hang (ptext SLIT("A lazy (~) pattern connot bind existential type variables")) 2 (vcat (map pprSkolTvBinding tvs)) +nonRigidMatch con + = hang (ptext SLIT("GADT pattern match in non-rigid context for") <+> quotes (ppr con)) + 2 (ptext SLIT("Tell GHC HQ if you'd like this to unify the context")) + inaccessibleAlt msg = hang (ptext SLIT("Inaccessible case alternative:")) 2 msg \end{code}