X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcPat.lhs;h=581568893815ea43ed1ef9f24e6926476ab22c68;hp=26bfdd45ea6275afa68303b15ff592b17b55d313;hb=f3399c446c7507d46d6cc550aa2fe7027dbc1b5b;hpb=56a39804b7ba971a170eff8c129882460e1ba24b diff --git a/compiler/typecheck/TcPat.lhs b/compiler/typecheck/TcPat.lhs index 26bfdd4..5815688 100644 --- a/compiler/typecheck/TcPat.lhs +++ b/compiler/typecheck/TcPat.lhs @@ -13,7 +13,7 @@ TcPat: Typechecking patterns -- http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings -- for details -module TcPat ( tcLetPat, tcLamPat, tcLamPats, tcOverloadedLit, +module TcPat ( tcLetPat, tcLamPat, tcLamPats, tcProcPat, tcOverloadedLit, addDataConStupidTheta, badFieldCon, polyPatSig ) where #include "HsVersions.h" @@ -51,6 +51,7 @@ import Util import Maybes import Outputable import FastString +import Monad \end{code} @@ -96,24 +97,29 @@ tcLamPats :: [LPat Name] -- Patterns, -- 5. Check that no existentials escape tcLamPats pats tys res_ty thing_inside - = tc_lam_pats (zipEqual "tcLamPats" pats tys) + = tc_lam_pats LamPat (zipEqual "tcLamPats" pats tys) (emptyRefinement, res_ty) thing_inside 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 + +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) } ----------------- -tc_lam_pats :: [(LPat Name,BoxySigmaType)] +tc_lam_pats :: PatCtxt + -> [(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, pat_eqs = False } +tc_lam_pats ctxt pat_ty_prs (reft, res_ty) thing_inside + = do { let init_state = PS { pat_ctxt = ctxt, pat_reft = reft, pat_eqs = False } ; (pats', ex_tvs, res) <- tcMultiple tc_lpat_pr pat_ty_prs init_state $ \ pstate' -> refineEnvironment (pat_reft pstate') (pat_eqs pstate') $ @@ -156,6 +162,8 @@ data PatState = PS { 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 @@ -173,18 +181,6 @@ patSigCtxt other = LamPatSigCtxt \begin{code} tcPatBndr :: PatState -> Name -> BoxySigmaType -> TcM TcId -tcPatBndr (PS { pat_ctxt = LamPat }) 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 - -- 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 (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 @@ -196,6 +192,18 @@ tcPatBndr (PS { pat_ctxt = LetPat lookup_sig }) bndr_name pat_ty ; 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 + -- 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 (Id.mkLocalId bndr_name pat_ty') } + ------------------- bindInstsOfPatId :: TcId -> TcM a -> TcM (a, LHsBinds TcId) @@ -378,6 +386,9 @@ tc_pat pstate lpat@(LazyPat pat) pat_ty thing_inside ; 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' <- unBoxWildCardType pat_ty -- Make sure it's filled in with monotypes ; res <- thing_inside pstate @@ -414,7 +425,9 @@ tc_pat pstate (orig@(ViewPat expr pat _)) overall_pat_ty thing_inside -- (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 (expr'_expected pat_ty) expr'_inferred) + ; (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 @@ -437,20 +450,25 @@ 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, 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 coi (ListPat pats' elt_ty) pat_ty, pats_tvs, res) } + ; return (mkCoPatCoI scoi (ListPat pats' elt_ty) pat_ty, pats_tvs, res) + } tc_pat pstate (PArrPat pats _) pat_ty thing_inside = 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 ; ifM (null pats) (zapToMonotype pat_ty) -- c.f. ExplicitPArr in TcExpr - ; return (mkCoPatCoI coi (PArrPat pats' elt_ty) pat_ty, pats_tvs, res) } + ; return (mkCoPatCoI scoi (PArrPat pats' elt_ty) pat_ty, pats_tvs, res) + } tc_pat pstate (TuplePat pats boxity _) pat_ty 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 @@ -467,7 +485,7 @@ tc_pat pstate (TuplePat pats boxity _) pat_ty thing_inside | otherwise = unmangled_result ; ASSERT( length arg_tys == length pats ) -- Syntactically enforced - return (mkCoPatCoI coi possibly_mangled_result pat_ty, pats_tvs, res) + return (mkCoPatCoI scoi possibly_mangled_result pat_ty, pats_tvs, res) } ------------------------ @@ -600,56 +618,82 @@ tcConPat :: PatState -> SrcSpan -> DataCon -> TyCon -> HsConPatDetails Name -> (PatState -> TcM a) -> TcM (Pat TcId, [TcTyVar], a) tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside - = do { let (univ_tvs, ex_tvs, eq_spec, eq_theta, dict_theta, arg_tys, _) = dataConFullSig data_con + = 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 + -- This may involve doing a family-instance coercion, and building a + -- wrapper ; (ctxt_res_tys, coi) <- boxySplitTyConAppWithFamily tycon pat_ty - ; let pat_ty' = mkTyConApp tycon ctxt_res_tys - -- pat_ty /= pat_ty iff coi /= IdCo - wrap_res_pat res_pat - = mkCoPatCoI coi (unwrapFamInstScrutinee tycon ctxt_res_tys res_pat) 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 + ; 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]) + 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 + 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' } + 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 - { let eq_spec' = substEqSpec tenv eq_spec - theta' = substTheta tenv full_theta - ; co_vars <- newCoVars eq_spec' -- Make coercion variables - ; traceTc (text "tcConPat: refineAlt") - ; pstate' <- refineAlt data_con pstate ex_tvs' co_vars pat_ty - ; traceTc (text "tcConPat: refineAlt done!") - + else do -- The general case, with existential, and local 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' + ctxt = pat_ctxt pstate + ; checkTc (case ctxt 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. + ; unless (all (not . isEqPred) theta') $ + checkTc (isRigidTy pat_ty) (nonRigidMatch data_con) + ; ((arg_pats', inner_tvs, res), lie_req) <- getLIE $ - tcConArgs data_con arg_tys' arg_pats pstate' thing_inside + tcConArgs data_con arg_tys' arg_pats pstate thing_inside ; loc <- getInstLoc origin ; dicts <- newDictBndrs loc theta' - ; dict_binds <- tcSimplifyCheckPat loc co_vars (pat_reft pstate') + ; dict_binds <- tcSimplifyCheckPat loc [] emptyRefinement ex_tvs' dicts lie_req ; let res_pat = ConPatOut { pat_con = L con_span data_con, - pat_tvs = ex_tvs' ++ co_vars, + pat_tvs = ex_tvs', pat_dicts = map instToVar dicts, pat_binds = dict_binds, pat_args = arg_pats', pat_ty = pat_ty' } @@ -707,9 +751,10 @@ tcConArgs data_con arg_tys (PrefixCon arg_pats) pstate thing_inside con_arity = dataConSourceArity data_con no_of_args = length arg_pats -tcConArgs data_con [arg_ty1,arg_ty2] (InfixCon p1 p2) pstate 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) + ; 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) } @@ -825,11 +870,8 @@ refineAlt con pstate ex_tvs [] pat_ty = return pstate -- Common case: no equational constraints refineAlt con pstate ex_tvs co_vars pat_ty - = do { opt_gadt <- doptM Opt_GADTs -- No type-refinement unless GADTs are on - ; if (not opt_gadt) then return pstate - else do - - { checkTc (isRigidTy pat_ty) (nonRigidMatch con) + = -- See Note [Flags and equational constraints] + do { checkTc (isRigidTy pat_ty) (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: @@ -857,9 +899,20 @@ refineAlt con pstate ex_tvs co_vars pat_ty vcat [ ppr con <+> ppr ex_tvs, ppr [(v, tyVarKind v) | v <- co_vars], ppr reft] - } } } + } } \end{code} +Note [Flags and equational constraints] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +If there are equational constraints, we take account of them +regardless of flag settings; -XGADTs etc applies only to the +*definition* of a data type. + +An alternative would be also to reject a program that *used* +constructors with equational constraints. But want we should avoid at +all costs is simply to *ignore* the constraints, since that gives +incomprehensible errors (Trac #2004). + %************************************************************************ %* * @@ -1049,10 +1102,15 @@ 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 cannot bind existential type variables")) @@ -1060,11 +1118,11 @@ lazyPatErr pat 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")) + 2 (ptext SLIT("Solution: add a type signature")) nonRigidResult res_ty = hang (ptext SLIT("GADT pattern match with non-rigid result type") <+> quotes (ppr res_ty)) - 2 (ptext SLIT("Tell GHC HQ if you'd like this to unify the context")) + 2 (ptext SLIT("Solution: add a type signature")) inaccessibleAlt msg = hang (ptext SLIT("Inaccessible case alternative:")) 2 msg