X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypecheck%2FInst.lhs;h=b5eeff0b6b5ef9b2dc2bfba94ca83eadcdf18626;hp=31a93540dceb1f8834569b9cac157d09eefecddd;hb=66579ff945831c5fc9a17c58c722ff01f2268d76;hpb=0f5e104c36b1dc3d8deeec5fef3d65e7b3a1b5ad diff --git a/compiler/typecheck/Inst.lhs b/compiler/typecheck/Inst.lhs index 31a9354..b5eeff0 100644 --- a/compiler/typecheck/Inst.lhs +++ b/compiler/typecheck/Inst.lhs @@ -7,7 +7,7 @@ The @Inst@ type: dictionaries or method instances \begin{code} module Inst ( - Inst, + Inst, pprInstances, pprDictsTheta, pprDictsInFull, -- User error messages showLIE, pprInst, pprInsts, pprInstInFull, -- Debugging messages @@ -15,6 +15,7 @@ module Inst ( tidyInsts, tidyMoreInsts, newDictBndr, newDictBndrs, newDictBndrsO, + newDictOccs, newDictOcc, instCall, instStupidTheta, cloneDict, mkOverLit, newIPDict, newMethod, newMethodFromName, newMethodWithGivenTy, @@ -39,12 +40,11 @@ module Inst ( InstOrigin(..), InstLoc, pprInstLoc, - mkWantedCo, mkGivenCo, - fromWantedCo, fromGivenCo, - eitherEqInst, mkEqInst, mkEqInsts, mkWantedEqInst, - finalizeEqInst, writeWantedCoercion, - eqInstType, updateEqInstCoercion, - eqInstCoercion, eqInstTys + mkWantedCo, mkGivenCo, isWantedCo, eqInstCoType, mkIdEqInstCo, + mkSymEqInstCo, mkLeftTransEqInstCo, mkRightTransEqInstCo, mkAppEqInstCo, + wantedEqInstIsUnsolved, eitherEqInst, mkEqInst, mkWantedEqInst, + wantedToLocalEqInst, finalizeEqInst, eqInstType, eqInstCoercion, + eqInstTys ) where #include "HsVersions.h" @@ -61,7 +61,7 @@ import InstEnv import FunDeps import TcMType import TcType -import DsUtils +import MkCore import Type import TypeRep import Class @@ -92,6 +92,7 @@ import Control.Monad \end{code} + Selection ~~~~~~~~~ \begin{code} @@ -116,8 +117,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 @@ -278,16 +282,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}) } @@ -334,15 +363,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)) } @@ -350,8 +376,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 @@ -360,15 +386,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} @@ -385,7 +406,7 @@ mkPredName uniq loc pred_ty -- we use the outermost tycon of the lhs, if there is one, to -- improve readability of Core code baseOcc = case splitTyConApp_maybe ty of - Nothing -> mkOccName tcName "$" + Nothing -> mkTcOcc "$" Just (tc, _) -> getOccName tc \end{code} @@ -493,7 +514,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}) @@ -524,7 +545,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] @@ -838,7 +859,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 @@ -935,20 +957,96 @@ syntaxNameCtxt name orig ty tidy_env = do %* * %************************************************************************ +Operations on EqInstCo. + \begin{code} -mkGivenCo :: Coercion -> Either TcTyVar Coercion +mkGivenCo :: Coercion -> EqInstCo mkGivenCo = Right -mkWantedCo :: TcTyVar -> Either TcTyVar Coercion +mkWantedCo :: TcTyVar -> EqInstCo mkWantedCo = Left -fromGivenCo :: Either TcTyVar Coercion -> Coercion -fromGivenCo (Right co) = co -fromGivenCo _ = panic "fromGivenCo: not a wanted coercion" +isWantedCo :: EqInstCo -> Bool +isWantedCo (Left _) = True +isWantedCo _ = False -fromWantedCo :: String -> Either TcTyVar Coercion -> 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 +\end{code} + +Coercion transformations on EqInstCo. These transformations work differently +depending on whether a EqInstCo is for a wanted or local equality: + + Local : apply the inverse of the specified coercion + Wanted: obtain a fresh coercion hole (meta tyvar) and update the old hole + to be the specified coercion applied to the new coercion hole + +\begin{code} +-- Coercion transformation: co = id +-- +mkIdEqInstCo :: EqInstCo -> Type -> TcM () +mkIdEqInstCo (Left cotv) t + = writeMetaTyVar cotv t +mkIdEqInstCo (Right _) _ + = return () + +-- Coercion transformation: co = sym co' +-- +mkSymEqInstCo :: EqInstCo -> (Type, Type) -> TcM EqInstCo +mkSymEqInstCo (Left cotv) (ty1, ty2) + = do { cotv' <- newMetaCoVar ty1 ty2 + ; writeMetaTyVar cotv (mkSymCoercion (TyVarTy cotv')) + ; return $ Left cotv' + } +mkSymEqInstCo (Right co) _ + = return $ Right (mkSymCoercion co) + +-- Coercion transformation: co = co' |> given_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) + ; return $ Left cotv' + } +mkLeftTransEqInstCo (Right co) given_co _ + = return $ Right (co `mkTransCoercion` mkSymCoercion given_co) + +-- Coercion transformation: co = given_co |> 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') + ; return $ Left cotv' + } +mkRightTransEqInstCo (Right co) given_co _ + = return $ Right (mkSymCoercion given_co `mkTransCoercion` co) + +-- Coercion transformation: co = col cor +-- +mkAppEqInstCo :: EqInstCo -> (Type, Type) -> (Type, Type) + -> TcM (EqInstCo, EqInstCo) +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)) + ; return (Left cotv_l, Left cotv_r) + } +mkAppEqInstCo (Right co) _ _ + = return (Right $ 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 @@ -960,20 +1058,23 @@ eitherEqInst (EqInst {tci_co = either_co}) withWanted withGiven Right co -> withGiven co eitherEqInst i _ _ = pprPanic "eitherEqInst" (ppr i) -mkEqInsts :: [PredType] -> [Either TcTyVar Coercion] -> TcM [Inst] -mkEqInsts preds cos = zipWithM mkEqInst preds cos - -mkEqInst :: PredType -> Either TcTyVar Coercion -> TcM Inst +mkEqInst :: PredType -> EqInstCo -> TcM Inst mkEqInst (EqPred ty1 ty2) co = do { uniq <- newUnique ; src_span <- getSrcSpanM ; err_ctxt <- getErrCtxt ; let loc = InstLoc EqOrigin src_span err_ctxt name = mkName uniq src_span - inst = EqInst {tci_left = ty1, tci_right = ty2, tci_co = co, tci_loc = loc, tci_name = name} + inst = EqInst { tci_left = ty1 + , tci_right = ty2 + , tci_co = co + , tci_loc = loc + , tci_name = name + } ; return inst } - where mkName uniq src_span = mkInternalName uniq (mkVarOcc "co") src_span + where + mkName uniq src_span = mkInternalName uniq (mkVarOcc "co") src_span mkEqInst pred _ = pprPanic "mkEqInst" (ppr pred) mkWantedEqInst :: PredType -> TcM Inst @@ -983,40 +1084,42 @@ mkWantedEqInst pred@(EqPred ty1 ty2) } mkWantedEqInst pred = pprPanic "mkWantedEqInst" (ppr pred) --- type inference: --- We want to promote the wanted EqInst to a given EqInst --- in the signature context. --- This means we have to give the coercion a name --- and fill it in as its own name. -finalizeEqInst - :: Inst -- wanted - -> TcM Inst -- given -finalizeEqInst wanted@(EqInst {tci_left = ty1, tci_right = ty2, tci_name = name}) - = do { let var = Var.mkCoVar name (PredTy $ EqPred ty1 ty2) - ; writeWantedCoercion wanted (TyVarTy var) - ; let given = wanted { tci_co = mkGivenCo $ TyVarTy var } - ; return given - } -finalizeEqInst i = pprPanic "finalizeEqInst" (ppr i) +-- 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) +-- +-- * Give it a name and change the coercion around. +-- +finalizeEqInst :: Inst -- wanted + -> TcM Inst -- given +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 + ; writeMetaTyVar cotv (TyVarTy var) + + -- set the new coercion + ; let given = wanted { tci_co = mkGivenCo $ TyVarTy var } + ; return given + } -writeWantedCoercion - :: Inst -- wanted EqInst - -> Coercion -- coercion to fill the hole with - -> TcM () -writeWantedCoercion wanted co - = do { let cotv = fromWantedCo "writeWantedCoercion" $ tci_co wanted - ; writeMetaTyVar cotv co - } +finalizeEqInst i = pprPanic "finalizeEqInst" (ppr i) eqInstType :: Inst -> TcType eqInstType inst = eitherEqInst inst mkTyVarTy id -eqInstCoercion :: Inst -> Either TcTyVar Coercion +eqInstCoercion :: Inst -> EqInstCo eqInstCoercion = tci_co eqInstTys :: Inst -> (TcType, TcType) eqInstTys inst = (tci_left inst, tci_right inst) - -updateEqInstCoercion :: (Either TcTyVar Coercion -> Either TcTyVar Coercion) -> Inst -> Inst -updateEqInstCoercion f inst = inst {tci_co = f $ tci_co inst} \end{code}