X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypecheck%2FInst.lhs;h=2e081130ad88cdf06bbed36adec5b772acf0ba45;hp=17dce300f00ad2276d200cea6a1faa0cbab1d9dd;hb=296058a1cafa80dec0b3f998348bce7c65f668b0;hpb=c4ec8f2a77894af1c6160c4e8ad5625ab62f0bea diff --git a/compiler/typecheck/Inst.lhs b/compiler/typecheck/Inst.lhs index 17dce30..2e08113 100644 --- a/compiler/typecheck/Inst.lhs +++ b/compiler/typecheck/Inst.lhs @@ -15,15 +15,16 @@ module Inst ( tidyInsts, tidyMoreInsts, newDictBndr, newDictBndrs, newDictBndrsO, + newDictOccs, newDictOcc, instCall, instStupidTheta, cloneDict, mkOverLit, newIPDict, newMethod, newMethodFromName, newMethodWithGivenTy, tcInstClassOp, tcSyntaxName, isHsVar, - tyVarsOfInst, tyVarsOfInsts, tyVarsOfLIE, - ipNamesOfInst, ipNamesOfInsts, fdPredsOfInst, fdPredsOfInsts, - getDictClassTys, dictPred, + tyVarsOfInst, tyVarsOfInsts, tyVarsOfLIE, tcTyVarsOfInst, + tcTyVarsOfInsts, ipNamesOfInst, ipNamesOfInsts, fdPredsOfInst, + fdPredsOfInsts, growInstsTyVars, getDictClassTys, dictPred, lookupSimpleInst, LookupInstResult(..), tcExtendLocalInstEnv, tcGetInstEnvs, getOverlapFlag, @@ -39,13 +40,12 @@ module Inst ( InstOrigin(..), InstLoc, pprInstLoc, - mkWantedCo, mkGivenCo, - isWantedCo, fromWantedCo, fromGivenCo, eqInstCoType, - mkIdEqInstCo, mkSymEqInstCo, mkLeftTransEqInstCo, - mkRightTransEqInstCo, mkAppEqInstCo, - eitherEqInst, mkEqInst, mkEqInsts, mkWantedEqInst, finalizeEqInst, - eqInstType, updateEqInstCoercion, - eqInstCoercion, eqInstTys + mkWantedCo, mkGivenCo, isWantedCo, eqInstCoType, mkIdEqInstCo, + mkSymEqInstCo, mkLeftTransEqInstCo, mkRightTransEqInstCo, mkAppEqInstCo, + mkTyConEqInstCo, mkFunEqInstCo, + wantedEqInstIsUnsolved, eitherEqInst, mkEqInst, mkWantedEqInst, + wantedToLocalEqInst, finalizeEqInst, eqInstType, eqInstCoercion, + eqInstTys ) where #include "HsVersions.h" @@ -63,6 +63,7 @@ import FunDeps import TcMType import TcType import MkCore +import TyCon import Type import TypeRep import Class @@ -118,8 +119,11 @@ instToVar (Dict {tci_name = nm, tci_pred = pred}) instToVar (ImplicInst {tci_name = nm, tci_tyvars = tvs, tci_given = givens, tci_wanted = wanteds}) = mkLocalId nm (mkImplicTy tvs givens wanteds) -instToVar i@(EqInst {}) - = eitherEqInst i id (\(TyVarTy covar) -> covar) +instToVar inst@(EqInst {}) + = eitherEqInst inst id assertCoVar + where + assertCoVar (TyVarTy cotv) = cotv + assertCoVar coty = pprPanic "Inst.instToVar" (ppr coty) instType :: Inst -> Type instType (LitInst {tci_ty = ty}) = ty @@ -150,6 +154,7 @@ getDictClassTys :: Inst -> (Class, [Type]) getDictClassTys (Dict {tci_pred = pred}) = getClassPredTys pred getDictClassTys inst = pprPanic "getDictClassTys" (ppr inst) +-------------------------------- -- fdPredsOfInst is used to get predicates that contain functional -- dependencies *or* might do so. The "might do" part is because -- a constraint (C a b) might have a superclass with FDs @@ -159,14 +164,16 @@ getDictClassTys inst = pprPanic "getDictClassTys" (ppr inst) fdPredsOfInst :: Inst -> [TcPredType] fdPredsOfInst (Dict {tci_pred = pred}) = [pred] fdPredsOfInst (Method {tci_theta = theta}) = theta -fdPredsOfInst (ImplicInst {tci_given = gs, - tci_wanted = ws}) = fdPredsOfInsts (gs ++ ws) +fdPredsOfInst (ImplicInst {tci_wanted = ws}) = fdPredsOfInsts ws + -- The ImplicInst case doesn't look right; + -- what if ws mentions skolem variables? fdPredsOfInst (LitInst {}) = [] fdPredsOfInst (EqInst {}) = [] fdPredsOfInsts :: [Inst] -> [PredType] fdPredsOfInsts insts = concatMap fdPredsOfInst insts +--------------------------------- isInheritableInst :: Inst -> Bool isInheritableInst (Dict {tci_pred = pred}) = isInheritablePred pred isInheritableInst (Method {tci_theta = theta}) = all isInheritablePred theta @@ -186,22 +193,53 @@ ipNamesOfInst (Method {tci_theta = theta}) = [ipNameName n | IParam n _ <- the ipNamesOfInst _ = [] --------------------------------- -tyVarsOfInst :: Inst -> TcTyVarSet + +-- |All free type variables (not including the coercion variables of +-- equalities) +-- +tyVarsOfInst :: Inst -> TyVarSet tyVarsOfInst (LitInst {tci_ty = ty}) = tyVarsOfType ty tyVarsOfInst (Dict {tci_pred = pred}) = tyVarsOfPred pred -tyVarsOfInst (Method {tci_oid = id, tci_tys = tys}) = tyVarsOfTypes tys `unionVarSet` varTypeTyVars id - -- The id might have free type variables; in the case of - -- locally-overloaded class methods, for example -tyVarsOfInst (ImplicInst {tci_tyvars = tvs, tci_given = givens, tci_wanted = wanteds}) +tyVarsOfInst (Method {tci_oid = id, tci_tys = tys}) + = tyVarsOfTypes tys `unionVarSet` varTypeTyVars id + -- The id might have free type variables; in the case of + -- locally-overloaded class methods, for example +tyVarsOfInst (ImplicInst {tci_tyvars = tvs, tci_given = givens, + tci_wanted = wanteds}) = (tyVarsOfInsts givens `unionVarSet` tyVarsOfInsts wanteds) `minusVarSet` mkVarSet tvs `unionVarSet` unionVarSets (map varTypeTyVars tvs) -- Remember the free tyvars of a coercion -tyVarsOfInst (EqInst {tci_left = ty1, tci_right = ty2}) = tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2 +tyVarsOfInst (EqInst {tci_left = ty1, tci_right = ty2}) + = tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2 + +-- |All free meta type variables *including* the coercion variables of +-- equalities +-- +tcTyVarsOfInst :: Inst -> TyVarSet +tcTyVarsOfInst (LitInst {tci_ty = ty}) = tcTyVarsOfType ty +tcTyVarsOfInst (Dict {tci_pred = pred}) = tcTyVarsOfPred pred +tcTyVarsOfInst (Method {tci_oid = id, tci_tys = tys}) + = tcTyVarsOfTypes tys `unionVarSet` varTypeTcTyVars id + -- The id might have free type variables; in the case of + -- locally-overloaded class methods, for example +tcTyVarsOfInst (ImplicInst {tci_tyvars = tvs, tci_given = givens, + tci_wanted = wanteds}) + = (tcTyVarsOfInsts givens `unionVarSet` tcTyVarsOfInsts wanteds) + `minusVarSet` mkVarSet tvs + `unionVarSet` unionVarSets (map varTypeTcTyVars tvs) + -- Remember the free tyvars of a coercion +tcTyVarsOfInst (EqInst {tci_co = co, tci_left = ty1, tci_right = ty2}) + = either unitVarSet tcTyVarsOfType co `unionVarSet` -- include covars + tcTyVarsOfType ty1 `unionVarSet` tcTyVarsOfType ty2 -tyVarsOfInsts :: [Inst] -> VarSet +tyVarsOfInsts :: [Inst] -> TyVarSet tyVarsOfInsts insts = foldr (unionVarSet . tyVarsOfInst) emptyVarSet insts -tyVarsOfLIE :: Bag Inst -> VarSet + +tcTyVarsOfInsts :: [Inst] -> TcTyVarSet +tcTyVarsOfInsts insts = foldr (unionVarSet . tcTyVarsOfInst) emptyVarSet insts + +tyVarsOfLIE :: Bag Inst -> TyVarSet tyVarsOfLIE lie = tyVarsOfInsts (lieToList lie) @@ -214,8 +252,45 @@ addInstToDictBind :: TcDictBinds -> Inst -> LHsExpr TcId -> TcDictBinds addInstToDictBind binds inst rhs = binds `unionBags` instToDictBind inst rhs \end{code} -Predicates -~~~~~~~~~~ +Note [Growing the tau-tvs using constraints] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +(growInstsTyVars insts tvs) is the result of extending the set + of tyvars tvs using all conceivable links from pred + +E.g. tvs = {a}, preds = {H [a] b, K (b,Int) c, Eq e} +Then grow precs tvs = {a,b,c} + +All the type variables from an implicit parameter are added, whether or +not they are mentioned in tvs; see Note [Implicit parameters and ambiguity] +in TcSimplify. + +See also Note [Ambiguity] in TcSimplify + +\begin{code} +growInstsTyVars :: [Inst] -> TyVarSet -> TyVarSet +growInstsTyVars insts tvs + | null insts = tvs + | otherwise = fixVarSet mk_next tvs + where + mk_next tvs = foldr grow_inst_tvs tvs insts + +grow_inst_tvs :: Inst -> TyVarSet -> TyVarSet +grow_inst_tvs (Dict {tci_pred = pred}) tvs = growPredTyVars pred tvs +grow_inst_tvs (Method {tci_theta = theta}) tvs = foldr growPredTyVars tvs theta +grow_inst_tvs (ImplicInst {tci_tyvars = tvs1, tci_wanted = ws}) tvs + = tvs `unionVarSet` (foldr grow_inst_tvs (tvs `delVarSetList` tvs1) ws + `delVarSetList` tvs1) +grow_inst_tvs inst tvs -- EqInst, LitInst + = growTyVars (tyVarsOfInst inst) tvs +\end{code} + + +%************************************************************************ +%* * + Predicates +%* * +%************************************************************************ + \begin{code} isAbstractableInst :: Inst -> Bool @@ -280,16 +355,41 @@ newDictBndrs :: InstLoc -> TcThetaType -> TcM [Inst] newDictBndrs inst_loc theta = mapM (newDictBndr inst_loc) theta newDictBndr :: InstLoc -> TcPredType -> TcM Inst +-- Makes a "given" newDictBndr inst_loc pred@(EqPred ty1 ty2) = do { uniq <- newUnique ; let name = mkPredName uniq inst_loc pred + co = mkGivenCo $ TyVarTy (Var.mkCoVar name (PredTy pred)) ; return (EqInst {tci_name = name, tci_loc = inst_loc, tci_left = ty1, tci_right = ty2, - tci_co = mkGivenCo $ TyVarTy (Var.mkCoVar name (PredTy pred))}) - } -newDictBndr inst_loc pred + tci_co = co }) } + +newDictBndr inst_loc pred = newDict inst_loc pred + +------------------- +newDictOccs :: InstLoc -> TcThetaType -> TcM [Inst] +newDictOccs inst_loc theta = mapM (newDictOcc inst_loc) theta + +newDictOcc :: InstLoc -> TcPredType -> TcM Inst +-- Makes a "wanted" +newDictOcc inst_loc pred@(EqPred ty1 ty2) + = do { uniq <- newUnique + ; cotv <- newMetaCoVar ty1 ty2 + ; let name = mkPredName uniq inst_loc pred + ; return (EqInst {tci_name = name, + tci_loc = inst_loc, + tci_left = ty1, + tci_right = ty2, + tci_co = Left cotv }) } + +newDictOcc inst_loc pred = newDict inst_loc pred + +---------------- +newDict :: InstLoc -> TcPredType -> TcM Inst +-- Always makes a Dict, not an EqInst +newDict inst_loc pred = do { uniq <- newUnique ; let name = mkPredName uniq inst_loc pred ; return (Dict {tci_name = name, tci_pred = pred, tci_loc = inst_loc}) } @@ -336,15 +436,12 @@ instCallDicts _ [] = return idHsWrapper instCallDicts loc (EqPred ty1 ty2 : preds) = do { traceTc (text "instCallDicts" <+> ppr (EqPred ty1 ty2)) ; coi <- boxyUnify ty1 ty2 --- ; coi <- unifyType ty1 ty2 ; let co = fromCoI coi ty1 ; co_fn <- instCallDicts loc preds ; return (co_fn <.> WpTyApp co) } instCallDicts loc (pred : preds) - = do { uniq <- newUnique - ; let name = mkPredName uniq loc pred - dict = Dict {tci_name = name, tci_pred = pred, tci_loc = loc} + = do { dict <- newDict loc pred ; extendLIE dict ; co_fn <- instCallDicts loc preds ; return (co_fn <.> WpApp (instToId dict)) } @@ -352,8 +449,8 @@ instCallDicts loc (pred : preds) ------------- cloneDict :: Inst -> TcM Inst cloneDict dict@(Dict nm _ _) = do { uniq <- newUnique - ; return (dict {tci_name = setNameUnique nm uniq}) } -cloneDict eq@(EqInst {}) = return eq + ; return (dict {tci_name = setNameUnique nm uniq}) } +cloneDict eq@(EqInst {}) = return eq cloneDict other = pprPanic "cloneDict" (ppr other) -- For vanilla implicit parameters, there is only one in scope @@ -362,15 +459,10 @@ cloneDict other = pprPanic "cloneDict" (ppr other) -- scope, so we make up a new namea. newIPDict :: InstOrigin -> IPName Name -> Type -> TcM (IPName Id, Inst) -newIPDict orig ip_name ty = do - inst_loc <- getInstLoc orig - uniq <- newUnique - let - pred = IParam ip_name ty - name = mkPredName uniq inst_loc pred - dict = Dict {tci_name = name, tci_pred = pred, tci_loc = inst_loc} - - return (mapIPName (\_ -> instToId dict) ip_name, dict) +newIPDict orig ip_name ty + = do { inst_loc <- getInstLoc orig + ; dict <- newDict inst_loc (IParam ip_name ty) + ; return (mapIPName (\_ -> instToId dict) ip_name, dict) } \end{code} @@ -495,7 +587,7 @@ Zonking makes sure that the instance types are fully zonked. \begin{code} zonkInst :: Inst -> TcM Inst -zonkInst dict@(Dict { tci_pred = pred}) = do +zonkInst dict@(Dict {tci_pred = pred}) = do new_pred <- zonkTcPredType pred return (dict {tci_pred = new_pred}) @@ -526,7 +618,7 @@ zonkInst eqinst@(EqInst {tci_left = ty1, tci_right = ty2}) (\co -> liftM mkGivenCo $ zonkTcType co) ; ty1' <- zonkTcType ty1 ; ty2' <- zonkTcType ty2 - ; return (eqinst {tci_co = co', tci_left= ty1', tci_right = ty2' }) + ; return (eqinst {tci_co = co', tci_left = ty1', tci_right = ty2' }) } zonkInsts :: [Inst] -> TcRn [Inst] @@ -840,7 +932,8 @@ record_dfun_usage :: Id -> TcRn () record_dfun_usage dfun_id = do { hsc_env <- getTopEnv ; let dfun_name = idName dfun_id - dfun_mod = nameModule dfun_name + dfun_mod = ASSERT( isExternalName dfun_name ) + nameModule dfun_name ; if isInternalName dfun_name || -- Internal name => defined in this module modulePackageId dfun_mod /= thisPackage (hsc_dflags hsc_env) then return () -- internal, or in another package @@ -950,15 +1043,6 @@ isWantedCo :: EqInstCo -> Bool isWantedCo (Left _) = True isWantedCo _ = False -fromGivenCo :: EqInstCo -> Coercion -fromGivenCo (Right co) = co -fromGivenCo _ = panic "fromGivenCo: not a wanted coercion" - -fromWantedCo :: String -> EqInstCo -> TcTyVar -fromWantedCo _ (Left covar) = covar -fromWantedCo msg _ = - panic ("fromWantedCo: not a wanted coercion: " ++ msg) - eqInstCoType :: EqInstCo -> TcType eqInstCoType (Left cotv) = mkTyVarTy cotv eqInstCoType (Right co) = co @@ -976,7 +1060,7 @@ depending on whether a EqInstCo is for a wanted or local equality: -- mkIdEqInstCo :: EqInstCo -> Type -> TcM () mkIdEqInstCo (Left cotv) t - = writeMetaTyVar cotv t + = bindMetaTyVar cotv t mkIdEqInstCo (Right _) _ = return () @@ -985,7 +1069,7 @@ mkIdEqInstCo (Right _) _ mkSymEqInstCo :: EqInstCo -> (Type, Type) -> TcM EqInstCo mkSymEqInstCo (Left cotv) (ty1, ty2) = do { cotv' <- newMetaCoVar ty1 ty2 - ; writeMetaTyVar cotv (mkSymCoercion (TyVarTy cotv')) + ; bindMetaTyVar cotv (mkSymCoercion (TyVarTy cotv')) ; return $ Left cotv' } mkSymEqInstCo (Right co) _ @@ -996,7 +1080,7 @@ mkSymEqInstCo (Right co) _ mkLeftTransEqInstCo :: EqInstCo -> Coercion -> (Type, Type) -> TcM EqInstCo mkLeftTransEqInstCo (Left cotv) given_co (ty1, ty2) = do { cotv' <- newMetaCoVar ty1 ty2 - ; writeMetaTyVar cotv (TyVarTy cotv' `mkTransCoercion` given_co) + ; bindMetaTyVar cotv (TyVarTy cotv' `mkTransCoercion` given_co) ; return $ Left cotv' } mkLeftTransEqInstCo (Right co) given_co _ @@ -1007,7 +1091,7 @@ mkLeftTransEqInstCo (Right co) given_co _ mkRightTransEqInstCo :: EqInstCo -> Coercion -> (Type, Type) -> TcM EqInstCo mkRightTransEqInstCo (Left cotv) given_co (ty1, ty2) = do { cotv' <- newMetaCoVar ty1 ty2 - ; writeMetaTyVar cotv (given_co `mkTransCoercion` TyVarTy cotv') + ; bindMetaTyVar cotv (given_co `mkTransCoercion` TyVarTy cotv') ; return $ Left cotv' } mkRightTransEqInstCo (Right co) given_co _ @@ -1020,16 +1104,53 @@ mkAppEqInstCo :: EqInstCo -> (Type, Type) -> (Type, Type) mkAppEqInstCo (Left cotv) (ty1_l, ty2_l) (ty1_r, ty2_r) = do { cotv_l <- newMetaCoVar ty1_l ty2_l ; cotv_r <- newMetaCoVar ty1_r ty2_r - ; writeMetaTyVar cotv (mkAppCoercion (TyVarTy cotv_l) (TyVarTy cotv_r)) + ; bindMetaTyVar cotv (mkAppCoercion (TyVarTy cotv_l) (TyVarTy cotv_r)) ; return (Left cotv_l, Left cotv_r) } mkAppEqInstCo (Right co) _ _ = return (Right $ mkLeftCoercion co, Right $ mkRightCoercion co) + +-- Coercion transformation: co = con col -> cor +-- +mkTyConEqInstCo :: EqInstCo -> TyCon -> [(Type, Type)] -> TcM ([EqInstCo]) +mkTyConEqInstCo (Left cotv) con ty12s + = do { cotvs <- mapM (uncurry newMetaCoVar) ty12s + ; bindMetaTyVar cotv (mkTyConCoercion con (mkTyVarTys cotvs)) + ; return (map Left cotvs) + } +mkTyConEqInstCo (Right co) _ args + = return $ map (\mkCoes -> Right $ foldl (.) id mkCoes co) mkCoes + -- make cascades of the form + -- mkRightCoercion (mkLeftCoercion .. (mkLeftCoercion co)..) + where + n = length args + mkCoes = [mkRightCoercion : replicate i mkLeftCoercion | i <- [n-1, n-2..0]] + +-- Coercion transformation: co = col -> cor +-- +mkFunEqInstCo :: EqInstCo -> (Type, Type) -> (Type, Type) + -> TcM (EqInstCo, EqInstCo) +mkFunEqInstCo (Left cotv) (ty1_l, ty2_l) (ty1_r, ty2_r) + = do { cotv_l <- newMetaCoVar ty1_l ty2_l + ; cotv_r <- newMetaCoVar ty1_r ty2_r + ; bindMetaTyVar cotv (mkFunCoercion (TyVarTy cotv_l) (TyVarTy cotv_r)) + ; return (Left cotv_l, Left cotv_r) + } +mkFunEqInstCo (Right co) _ _ + = return (Right $ mkRightCoercion (mkLeftCoercion co), + Right $ mkRightCoercion co) \end{code} Operations on entire EqInst. \begin{code} +-- |A wanted equality is unsolved as long as its cotv is unfilled. +-- +wantedEqInstIsUnsolved :: Inst -> TcM Bool +wantedEqInstIsUnsolved (EqInst {tci_co = Left cotv}) + = liftM not $ isFilledMetaTyVar cotv +wantedEqInstIsUnsolved _ = return True + eitherEqInst :: Inst -- given or wanted EqInst -> (TcTyVar -> a) -- result if wanted -> (Coercion -> a) -- result if given @@ -1040,9 +1161,6 @@ eitherEqInst (EqInst {tci_co = either_co}) withWanted withGiven Right co -> withGiven co eitherEqInst i _ _ = pprPanic "eitherEqInst" (ppr i) -mkEqInsts :: [PredType] -> [EqInstCo] -> TcM [Inst] -mkEqInsts preds cos = zipWithM mkEqInst preds cos - mkEqInst :: PredType -> EqInstCo -> TcM Inst mkEqInst (EqPred ty1 ty2) co = do { uniq <- newUnique @@ -1069,6 +1187,15 @@ mkWantedEqInst pred@(EqPred ty1 ty2) } mkWantedEqInst pred = pprPanic "mkWantedEqInst" (ppr pred) +-- Turn a wanted equality into a local that propagates the uninstantiated +-- coercion variable as witness. We need this to propagate wanted irreds into +-- attempts to solve implication constraints. +-- +wantedToLocalEqInst :: Inst -> Inst +wantedToLocalEqInst eq@(EqInst {tci_co = Left cotv}) + = eq {tci_co = Right (mkTyVarTy cotv)} +wantedToLocalEqInst eq = eq + -- Turn a wanted into a local EqInst (needed during type inference for -- signatures) -- @@ -1076,11 +1203,11 @@ mkWantedEqInst pred = pprPanic "mkWantedEqInst" (ppr pred) -- finalizeEqInst :: Inst -- wanted -> TcM Inst -- given -finalizeEqInst wanted@(EqInst{tci_left = ty1, tci_right = ty2, tci_name = name}) +finalizeEqInst wanted@(EqInst{tci_left = ty1, tci_right = ty2, + tci_name = name, tci_co = Left cotv}) = do { let var = Var.mkCoVar name (PredTy $ EqPred ty1 ty2) -- fill the coercion hole - ; let cotv = fromWantedCo "writeWantedCoercion" $ tci_co wanted ; writeMetaTyVar cotv (TyVarTy var) -- set the new coercion @@ -1098,7 +1225,4 @@ eqInstCoercion = tci_co eqInstTys :: Inst -> (TcType, TcType) eqInstTys inst = (tci_left inst, tci_right inst) - -updateEqInstCoercion :: (EqInstCo -> EqInstCo) -> Inst -> Inst -updateEqInstCoercion f inst = inst {tci_co = f $ tci_co inst} \end{code}