X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcSimplify.lhs;h=5f357d0a726abe60623836f1d6d8e98cb4f3833f;hp=43412296670dc4a98a4b6c4d25e0c6172d9b8bfa;hb=4ba96c06f2b69ea1fe2b27718013713e94c1520c;hpb=5822cb8d13aa3c05d2b46b4510c13d94b902eb21 diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs index 4341229..5f357d0 100644 --- a/compiler/typecheck/TcSimplify.lhs +++ b/compiler/typecheck/TcSimplify.lhs @@ -6,6 +6,13 @@ TcSimplify \begin{code} +{-# 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 TcSimplify ( tcSimplifyInfer, tcSimplifyInferCheck, tcSimplifyCheck, tcSimplifyRestricted, @@ -982,17 +989,15 @@ makeImplicationBind loc all_tvs reft | otherwise -- Otherwise we must generate a binding = do { uniq <- newUnique ; span <- getSrcSpanM - ; let (eq_givens,dict_givens) = partitionGivenEqInsts givens + ; let (eq_givens, dict_givens) = partition isEqInst givens eq_tyvar_cos = map TyVarTy $ uniqSetToList $ tyVarsOfTypes $ map eqInstType eq_givens ; let name = mkInternalName uniq (mkVarOcc "ic") span implic_inst = ImplicInst { tci_name = name, tci_reft = reft, tci_tyvars = all_tvs, tci_given = (eq_givens ++ dict_givens), tci_wanted = irreds, tci_loc = loc } - ; let - -- only create binder for dict_irreds - -- we - (eq_irreds,dict_irreds) = partitionWantedEqInsts irreds + ; let -- only create binder for dict_irreds + (eq_irreds, dict_irreds) = partition isEqInst irreds n_dict_irreds = length dict_irreds dict_irred_ids = map instToId dict_irreds tup_ty = mkTupleTy Boxed n_dict_irreds (map idType dict_irred_ids) @@ -1646,12 +1651,25 @@ data WantSCs = NoSCs | AddSCs -- Tells whether we should add the superclasses -- Note [SUPER-CLASS LOOP 1] \end{code} + %************************************************************************ %* * \subsection[reduce]{@reduce@} %* * %************************************************************************ +Note [Ancestor Equalities] +~~~~~~~~~~~~~~~~~~~~~~~~~~ +During context reduction, we add to the wanted equalities also those +equalities that (transitively) occur in superclass contexts of wanted +class constraints. Consider the following code + + class a ~ Int => C a + instance C Int + +If (C a) is wanted, we want to add (a ~ Int), which will be discharged by +substituting Int for a. Hence, we ultimately want (C Int), which we +discharge with the explicit instance. \begin{code} reduceContext :: RedEnv @@ -1670,31 +1688,32 @@ reduceContext env wanteds text "----------------------" ])) + ; let givens = red_givens env + (given_eqs0, given_dicts0) = partition isEqInst givens + (wanted_eqs0, wanted_dicts) = partition isEqInst wanteds - ; let givens = red_givens env - (given_eqs0,given_dicts0) = partitionGivenEqInsts givens - (wanted_eqs,wanted_dicts) = partitionWantedEqInsts wanteds + -- We want to add as wanted equalities those that (transitively) + -- occur in superclass contexts of wanted class constraints. + -- See Note [Ancestor Equalities] + ; ancestor_eqs <- ancestorEqualities wanted_dicts + ; let wanted_eqs = wanted_eqs0 ++ ancestor_eqs + ; traceTc $ text "reduceContext: ancestor eqs" <+> ppr ancestor_eqs - ; -- 1. Normalise the *given* *equality* constraints - (given_eqs,eliminate_skolems) <- normaliseGivens given_eqs0 + -- 1. Normalise the *given* *equality* constraints + ; (given_eqs, eliminate_skolems) <- normaliseGivens given_eqs0 - ; -- 2. Normalise the *given* *dictionary* constraints + -- 2. Normalise the *given* *dictionary* constraints -- wrt. the toplevel and given equations - (given_dicts,given_binds) <- normaliseGivenDicts given_eqs given_dicts0 + ; (given_dicts, given_binds) <- normaliseGivenDicts given_eqs + given_dicts0 - ; -- 3. Solve the *wanted* *equation* constraints - eq_irreds0 <- solveWanteds given_eqs wanted_eqs + -- 3. Solve the *wanted* *equation* constraints + ; eq_irreds0 <- solveWanteds given_eqs wanted_eqs - -- 4. Normalise the *wanted* equality constraints with respect to each other + -- 4. Normalise the *wanted* equality constraints with respect to + -- each other ; eq_irreds <- normaliseWanteds eq_irreds0 --- -- Do the real work --- -- Process non-implication constraints first, so that they are --- -- available to help solving the implication constraints --- -- ToDo: seems a bit inefficient and ad-hoc --- ; let (implics, rest) = partition isImplicInst wanteds --- ; avails <- reduceList env (rest ++ implics) init_state - -- 5. Build the Avail mapping from "given_dicts" ; init_state <- foldlM addGiven emptyAvails given_dicts @@ -1703,18 +1722,18 @@ reduceContext env wanteds ; wanted_dicts' <- zonkInsts wanted_dicts ; avails <- reduceList env wanted_dicts' init_state ; (binds, irreds0, needed_givens) <- extractResults avails wanted_dicts' - ; traceTc (text "reduceContext extractresults" <+> vcat - [ppr avails,ppr wanted_dicts',ppr binds,ppr needed_givens]) + ; traceTc $ text "reduceContext extractresults" <+> vcat + [ppr avails,ppr wanted_dicts',ppr binds,ppr needed_givens] - ; -- 7. Normalise the *wanted* *dictionary* constraints + -- 7. Normalise the *wanted* *dictionary* constraints -- wrt. the toplevel and given equations - (irreds1,normalise_binds1) <- normaliseWantedDicts given_eqs irreds0 + ; (irreds1,normalise_binds1) <- normaliseWantedDicts given_eqs irreds0 - ; -- 8. Substitute the wanted *equations* in the wanted *dictionaries* - (irreds,normalise_binds2) <- substEqInDictInsts eq_irreds irreds1 + -- 8. Substitute the wanted *equations* in the wanted *dictionaries* + ; (irreds,normalise_binds2) <- substEqInDictInsts eq_irreds irreds1 - ; -- 9. eliminate the artificial skolem constants introduced in 1. - eliminate_skolems + -- 9. eliminate the artificial skolem constants introduced in 1. + ; eliminate_skolems -- If there was some FD improvement, -- or new wanted equations have been exposed, @@ -1722,7 +1741,7 @@ reduceContext env wanteds ; let improved = availsImproved avails || (not $ isEmptyBag normalise_binds1) || (not $ isEmptyBag normalise_binds2) - || (not $ null $ fst $ partitionGivenEqInsts irreds) + || (any isEqInst irreds) ; traceTc (text "reduceContext end" <+> (vcat [ text "----------------------", @@ -1738,7 +1757,13 @@ reduceContext env wanteds text "----------------------" ])) - ; return (improved, given_binds `unionBags` normalise_binds1 `unionBags` normalise_binds2 `unionBags` binds, irreds ++ eq_irreds, needed_givens) } + ; return (improved, + given_binds `unionBags` normalise_binds1 + `unionBags` normalise_binds2 + `unionBags` binds, + irreds ++ eq_irreds, + needed_givens) + } tcImproveOne :: Avails -> Inst -> TcM ImprovementDone tcImproveOne avails inst @@ -2075,7 +2100,7 @@ reduceImplication env orig_avails reft tvs extra_givens wanteds inst_loc -- when inferring types. ; let dict_wanteds = filter (not . isEqInst) wanteds - (extra_eq_givens,extra_dict_givens) = partitionGivenEqInsts extra_givens + (extra_eq_givens, extra_dict_givens) = partition isEqInst extra_givens dict_ids = map instToId extra_dict_givens -- TOMDO: given equational constraints bug! -- we need a different evidence for given @@ -2368,21 +2393,6 @@ addRefinedGiven reft (refined_givens, avails) given -- and hopefully the optimiser will spot the duplicated work | otherwise = return (refined_givens, avails) - -addRefinedGiven' :: Refinement -> [Inst] -> Inst -> TcM [Inst] -addRefinedGiven' reft refined_givens given - | isDict given -- We sometimes have 'given' methods, but they - -- are always optional, so we can drop them - , let pred = dictPred given - , isRefineablePred pred -- See Note [ImplicInst rigidity] - , Just (co, pred) <- refinePred reft pred - = do { new_given <- newDictBndr (instLoc given) pred - ; return (new_given:refined_givens) } - -- ToDo: the superclasses of the original given all exist in Avails - -- so we could really just cast them, but it's more awkward to do, - -- and hopefully the optimiser will spot the duplicated work - | otherwise - = return refined_givens \end{code} Note [ImplicInst rigidity] @@ -2421,7 +2431,7 @@ addAvailAndSCs want_scs avails inst avail where is_loop pred = any (`tcEqType` mkPredTy pred) dep_tys -- Note: this compares by *type*, not by Unique - deps = findAllDeps (unitVarSet (instToId inst)) avail + deps = findAllDeps (unitVarSet (instToVar inst)) avail dep_tys = map idType (varSetElems deps) findAllDeps :: IdSet -> AvailHow -> IdSet @@ -2463,14 +2473,41 @@ addSCs is_loop avails dict ; addSCs is_loop avails' sc_dict } where sc_sel_rhs = L (instSpan dict) (HsWrap co_fn (HsVar sc_sel)) - co_fn = WpApp (instToId dict) <.> mkWpTyApps tys + co_fn = WpApp (instToVar dict) <.> mkWpTyApps tys is_given :: Inst -> Bool is_given sc_dict = case findAvail avails sc_dict of Just (Given _) -> True -- Given is cheaper than superclass selection other -> False + +-- From the a set of insts obtain all equalities that (transitively) occur in +-- superclass contexts of class constraints (aka the ancestor equalities). +-- +ancestorEqualities :: [Inst] -> TcM [Inst] +ancestorEqualities + = mapM mkWantedEqInst -- turn only equality predicates.. + . filter isEqPred -- ..into wanted equality insts + . bagToList + . addAEsToBag emptyBag -- collect the superclass constraints.. + . map dictPred -- ..of all predicates in a bag + . filter isClassDict + where + addAEsToBag :: Bag PredType -> [PredType] -> Bag PredType + addAEsToBag bag [] = bag + addAEsToBag bag (pred:preds) + | pred `elemBag` bag = addAEsToBag bag preds + | isEqPred pred = addAEsToBag bagWithPred preds + | isClassPred pred = addAEsToBag bagWithPred predsWithSCs + | otherwise = addAEsToBag bag preds + where + bagWithPred = bag `snocBag` pred + predsWithSCs = preds ++ substTheta (zipTopTvSubst tyvars tys) sc_theta + -- + (tyvars, sc_theta, _, _) = classBigSig clas + (clas, tys) = getClassPredTys pred \end{code} + %************************************************************************ %* * \section{tcSimplifyTop: defaulting} @@ -2733,7 +2770,6 @@ tcSimplifyDeriv :: InstOrigin -> TcM ThetaType -- Needed -- Given instance (wanted) => C inst_ty -- Simplify 'wanted' as much as possible --- The inst_ty is needed only for the termination check tcSimplifyDeriv orig tyvars theta = do { (tvs, _, tenv) <- tcInstTyVars tyvars @@ -2743,8 +2779,9 @@ tcSimplifyDeriv orig tyvars theta ; wanteds <- newDictBndrsO orig (substTheta tenv theta) ; (irreds, _) <- tryHardCheckLoop doc wanteds - ; let (tv_dicts, others) = partition isTyVarDict irreds + ; let (tv_dicts, others) = partition ok irreds ; addNoInstanceErrs others + -- See Note [Exotic derived instance contexts] in TcMType ; let rev_env = zipTopTvSubst tvs (mkTyVarTys tyvars) simpl_theta = substTheta rev_env (map dictPred tv_dicts) @@ -2754,49 +2791,10 @@ tcSimplifyDeriv orig tyvars theta ; return simpl_theta } where doc = ptext SLIT("deriving classes for a data type") -\end{code} - -Note [Exotic derived instance contexts] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Consider - data T a b c = MkT (Foo a b c) deriving( Eq ) - instance (C Int a, Eq b, Eq c) => Eq (Foo a b c) - -Notice that this instance (just) satisfies the Paterson termination -conditions. Then we *could* derive an instance decl like this: - - instance (C Int a, Eq b, Eq c) => Eq (T a b c) - -even though there is no instance for (C Int a), because there just -*might* be an instance for, say, (C Int Bool) at a site where we -need the equality instance for T's. -However, this seems pretty exotic, and it's quite tricky to allow -this, and yet give sensible error messages in the (much more common) -case where we really want that instance decl for C. - -So for now we simply require that the derived instance context -should have only type-variable constraints. - -Here is another example: - data Fix f = In (f (Fix f)) deriving( Eq ) -Here, if we are prepared to allow -fallow-undecidable-instances we -could derive the instance - instance Eq (f (Fix f)) => Eq (Fix f) -but this is so delicate that I don't think it should happen inside -'deriving'. If you want this, write it yourself! - -NB: if you want to lift this condition, make sure you still meet the -termination conditions! If not, the deriving mechanism generates -larger and larger constraints. Example: - data Succ a = S a - data Seq a = Cons a (Seq (Succ a)) | Nil deriving Show - -Note the lack of a Show instance for Succ. First we'll generate - instance (Show (Succ a), Show a) => Show (Seq a) -and then - instance (Show (Succ (Succ a)), Show (Succ a), Show a) => Show (Seq a) -and so on. Instead we want to complain of no instance for (Show (Succ a)). + ok dict | isDict dict = validDerivPred (dictPred dict) + | otherwise = False +\end{code} @tcSimplifyDefault@ just checks class-type constraints, essentially; @@ -3088,51 +3086,28 @@ misMatchMsg :: TcType -> TcType -> TcM (TidyEnv, SDoc) -- The argument order is: actual type, expected type misMatchMsg ty_act ty_exp = do { env0 <- tcInitTidyEnv - ; (env1, pp_exp, extra_exp) <- ppr_ty env0 ty_exp ty_act - ; (env2, pp_act, extra_act) <- ppr_ty env1 ty_act ty_exp + ; ty_exp <- zonkTcType ty_exp + ; ty_act <- zonkTcType ty_act + ; (env1, pp_exp, extra_exp) <- ppr_ty env0 ty_exp + ; (env2, pp_act, extra_act) <- ppr_ty env1 ty_act ; return (env2, sep [sep [ptext SLIT("Couldn't match expected type") <+> pp_exp, nest 7 $ ptext SLIT("against inferred type") <+> pp_act], nest 2 (extra_exp $$ extra_act)]) } -ppr_ty :: TidyEnv -> TcType -> TcType -> TcM (TidyEnv, SDoc, SDoc) -ppr_ty env ty other_ty - = do { ty' <- zonkTcType ty - ; let (env1, tidy_ty) = tidyOpenType env ty' - ; (env2, extra) <- ppr_extra env1 tidy_ty other_ty +ppr_ty :: TidyEnv -> TcType -> TcM (TidyEnv, SDoc, SDoc) +ppr_ty env ty + = do { let (env1, tidy_ty) = tidyOpenType env ty + ; (env2, extra) <- ppr_extra env1 tidy_ty ; return (env2, quotes (ppr tidy_ty), extra) } --- (ppr_extra env ty other_ty) shows extra info about 'ty' -ppr_extra env (TyVarTy tv) other_ty +-- (ppr_extra env ty) shows extra info about 'ty' +ppr_extra env (TyVarTy tv) | isSkolemTyVar tv || isSigTyVar tv = return (env1, pprSkolTvBinding tv1) where (env1, tv1) = tidySkolemTyVar env tv -ppr_extra env (TyConApp tc1 _) (TyConApp tc2 _) - | getOccName tc1 == getOccName tc2 - = -- This case helps with messages that would otherwise say - -- Could not match 'T' does not match 'M.T' - -- which is not helpful - do { this_mod <- getModule - ; return (env, quotes (ppr tc1) <+> ptext SLIT("is defined") <+> mk_mod this_mod) } - where - tc_mod = nameModule (getName tc1) - tc_pkg = modulePackageId tc_mod - tc2_pkg = modulePackageId (nameModule (getName tc2)) - mk_mod this_mod - | tc_mod == this_mod = ptext SLIT("in this module") - - | not home_pkg && tc2_pkg /= tc_pkg = pp_pkg - -- Suppress the module name if (a) it's from another package - -- (b) other_ty isn't from that same package - - | otherwise = ptext SLIT("in module") <+> quotes (ppr tc_mod) <+> pp_pkg - where - home_pkg = tc_pkg == modulePackageId this_mod - pp_pkg | home_pkg = empty - | otherwise = ptext SLIT("in package") <+> quotes (ppr tc_pkg) - -ppr_extra env ty other_ty = return (env, empty) -- Normal case +ppr_extra env ty = return (env, empty) -- Normal case \end{code}