X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypes%2FUnify.lhs;h=9f5b405415f5d0e9235a53f60c8bcb9e9d532861;hp=b96f20724e7b54e18b1204539c74fe960a87fc55;hb=c76c69c5b62f1ca4fa52d75b0dfbd37b7eddbb09;hpb=f3c4792fad3bf46e5ee500a909287718324c45d1 diff --git a/compiler/types/Unify.lhs b/compiler/types/Unify.lhs index b96f207..9f5b405 100644 --- a/compiler/types/Unify.lhs +++ b/compiler/types/Unify.lhs @@ -1,16 +1,9 @@ \begin{code} module Unify ( - -- Matching and unification - tcMatchTys, tcMatchTyX, ruleMatchTyX, tcMatchPreds, MatchEnv(..), - - tcUnifyTys, - - gadtRefineTys, BindFlag(..), - - coreRefineTys, dataConCanMatch, TypeRefinement, - - -- Re-export - MaybeErr(..) + -- Matching of types: + -- the "tc" prefix indicates that matching always + -- respects newtypes (rather than looking through them) + tcMatchTys, tcMatchTyX, ruleMatchTyX, tcMatchPreds, MatchEnv(..) ) where #include "HsVersions.h" @@ -18,12 +11,11 @@ module Unify ( import Var ( Var, TyVar, tyVarKind ) import VarEnv import VarSet -import Kind ( isSubKind ) import Type ( typeKind, tyVarsOfType, tyVarsOfTypes, tyVarsOfTheta, mkTyVarTys, TvSubstEnv, emptyTvSubstEnv, TvSubst(..), substTy, tcEqTypeX, - mkOpenTvSubst, tcView ) + mkOpenTvSubst, tcView, isSubKind, eqKind, repSplitAppTy_maybe ) import TypeRep ( Type(..), PredType(..), funTyCon ) -import DataCon ( DataCon, isVanillaDataCon, dataConResTys, dataConInstResTy ) +import DataCon ( DataCon, dataConResTys ) import Util ( snocView ) import ErrUtils ( Message ) import Outputable @@ -196,352 +188,3 @@ match_pred menv subst p1 p2 = Nothing \end{code} -%************************************************************************ -%* * - Unification -%* * -%************************************************************************ - -\begin{code} -tcUnifyTys :: (TyVar -> BindFlag) - -> [Type] -> [Type] - -> Maybe TvSubst -- A regular one-shot substitution --- The two types may have common type variables, and indeed do so in the --- second call to tcUnifyTys in FunDeps.checkClsFD -tcUnifyTys bind_fn tys1 tys2 - = maybeErrToMaybe $ initUM bind_fn $ - do { subst_env <- unify_tys emptyTvSubstEnv tys1 tys2 - - -- Find the fixed point of the resulting non-idempotent substitution - ; let in_scope = mkInScopeSet (tvs1 `unionVarSet` tvs2) - subst = TvSubst in_scope subst_env_fixpt - subst_env_fixpt = mapVarEnv (substTy subst) subst_env - ; return subst } - where - tvs1 = tyVarsOfTypes tys1 - tvs2 = tyVarsOfTypes tys2 - ----------------------------- -dataConCanMatch :: DataCon -> [Type] -> Bool --- Returns True iff the data con can match a scrutinee of type (T tys) --- where T is the type constructor for the data con -dataConCanMatch con tys - | isVanillaDataCon con - = True - | otherwise - = isSuccess $ initUM (\tv -> BindMe) $ - unify_tys emptyTvSubstEnv (dataConResTys con) tys - ----------------------------- -coreRefineTys :: DataCon -> [TyVar] -- Case pattern (con tv1 .. tvn ...) - -> Type -- Type of scrutinee - -> Maybe TypeRefinement - -type TypeRefinement = (TvSubstEnv, Bool) - -- The Bool is True iff all the bindings in the - -- env are for the pattern type variables - -- In this case, there is no type refinement - -- for already-in-scope type variables - --- Used by Core Lint and the simplifier. -coreRefineTys con tvs scrut_ty - = maybeErrToMaybe $ initUM (tryToBind tv_set) $ - do { -- Run the unifier, starting with an empty env - ; subst_env <- unify emptyTvSubstEnv pat_res_ty scrut_ty - - -- Find the fixed point of the resulting non-idempotent substitution - ; let subst = mkOpenTvSubst subst_env_fixpt - subst_env_fixpt = mapVarEnv (substTy subst) subst_env - - ; return (subst_env_fixpt, all_bound_here subst_env) } - where - pat_res_ty = dataConInstResTy con (mkTyVarTys tvs) - - -- 'tvs' are the tyvars bound by the pattern - tv_set = mkVarSet tvs - all_bound_here env = all bound_here (varEnvKeys env) - bound_here uniq = elemVarSetByKey uniq tv_set - --- This version is used by the type checker -gadtRefineTys :: TvSubst - -> DataCon -> [TyVar] - -> [Type] -> [Type] - -> MaybeErr Message (TvSubst, Bool) --- The bool is True <=> the only *new* bindings are for pat_tvs - -gadtRefineTys (TvSubst in_scope env1) con pat_tvs pat_tys ctxt_tys - = initUM (tryToBind tv_set) $ - do { -- Run the unifier, starting with an empty env - ; env2 <- unify_tys env1 pat_tys ctxt_tys - - -- Find the fixed point of the resulting non-idempotent substitution - ; let subst2 = TvSubst in_scope subst_env_fixpt - subst_env_fixpt = mapVarEnv (substTy subst2) env2 - - ; return (subst2, all_bound_here env2) } - where - -- 'tvs' are the tyvars bound by the pattern - tv_set = mkVarSet pat_tvs - all_bound_here env = all bound_here (varEnvKeys env) - bound_here uniq = elemVarEnvByKey uniq env1 || elemVarSetByKey uniq tv_set - -- The bool is True <=> the only *new* bindings are for pat_tvs - ----------------------------- -tryToBind :: TyVarSet -> TyVar -> BindFlag -tryToBind tv_set tv | tv `elemVarSet` tv_set = BindMe - | otherwise = AvoidMe -\end{code} - - -%************************************************************************ -%* * - The workhorse -%* * -%************************************************************************ - -\begin{code} -unify :: TvSubstEnv -- An existing substitution to extend - -> Type -> Type -- Types to be unified - -> UM TvSubstEnv -- Just the extended substitution, - -- Nothing if unification failed --- We do not require the incoming substitution to be idempotent, --- nor guarantee that the outgoing one is. That's fixed up by --- the wrappers. - --- Respects newtypes, PredTypes - -unify subst ty1 ty2 = -- pprTrace "unify" (ppr subst <+> pprParendType ty1 <+> pprParendType ty2) $ - unify_ subst ty1 ty2 - --- in unify_, any NewTcApps/Preds should be taken at face value -unify_ subst (TyVarTy tv1) ty2 = uVar False subst tv1 ty2 -unify_ subst ty1 (TyVarTy tv2) = uVar True subst tv2 ty1 - -unify_ subst ty1 ty2 | Just ty1' <- tcView ty1 = unify subst ty1' ty2 -unify_ subst ty1 ty2 | Just ty2' <- tcView ty2 = unify subst ty1 ty2' - -unify_ subst (PredTy p1) (PredTy p2) = unify_pred subst p1 p2 - -unify_ subst t1@(TyConApp tyc1 tys1) t2@(TyConApp tyc2 tys2) - | tyc1 == tyc2 = unify_tys subst tys1 tys2 - -unify_ subst (FunTy ty1a ty1b) (FunTy ty2a ty2b) - = do { subst' <- unify subst ty1a ty2a - ; unify subst' ty1b ty2b } - - -- Applications need a bit of care! - -- They can match FunTy and TyConApp, so use splitAppTy_maybe - -- NB: we've already dealt with type variables and Notes, - -- so if one type is an App the other one jolly well better be too -unify_ subst (AppTy ty1a ty1b) ty2 - | Just (ty2a, ty2b) <- repSplitAppTy_maybe ty2 - = do { subst' <- unify subst ty1a ty2a - ; unify subst' ty1b ty2b } - -unify_ subst ty1 (AppTy ty2a ty2b) - | Just (ty1a, ty1b) <- repSplitAppTy_maybe ty1 - = do { subst' <- unify subst ty1a ty2a - ; unify subst' ty1b ty2b } - -unify_ subst ty1 ty2 = failWith (misMatch ty1 ty2) - ------------------------------- -unify_pred subst (ClassP c1 tys1) (ClassP c2 tys2) - | c1 == c2 = unify_tys subst tys1 tys2 -unify_pred subst (IParam n1 t1) (IParam n2 t2) - | n1 == n2 = unify subst t1 t2 -unify_pred subst p1 p2 = failWith (misMatch (PredTy p1) (PredTy p2)) - ------------------------------- -unify_tys = unifyList unify - -unifyList :: Outputable a - => (TvSubstEnv -> a -> a -> UM TvSubstEnv) - -> TvSubstEnv -> [a] -> [a] -> UM TvSubstEnv -unifyList unifier subst orig_xs orig_ys - = go subst orig_xs orig_ys - where - go subst [] [] = return subst - go subst (x:xs) (y:ys) = do { subst' <- unifier subst x y - ; go subst' xs ys } - go subst _ _ = failWith (lengthMisMatch orig_xs orig_ys) - ------------------------------- -uVar :: Bool -- Swapped - -> TvSubstEnv -- An existing substitution to extend - -> TyVar -- Type variable to be unified - -> Type -- with this type - -> UM TvSubstEnv - -uVar swap subst tv1 ty - = -- Check to see whether tv1 is refined by the substitution - case (lookupVarEnv subst tv1) of - -- Yes, call back into unify' - Just ty' | swap -> unify subst ty ty' - | otherwise -> unify subst ty' ty - -- No, continue - Nothing -> uUnrefined subst tv1 ty ty - - -uUnrefined :: TvSubstEnv -- An existing substitution to extend - -> TyVar -- Type variable to be unified - -> Type -- with this type - -> Type -- (de-noted version) - -> UM TvSubstEnv - --- We know that tv1 isn't refined - -uUnrefined subst tv1 ty2 ty2' - | Just ty2'' <- tcView ty2' - = uUnrefined subst tv1 ty2 ty2'' -- Unwrap synonyms - -- This is essential, in case we have - -- type Foo a = a - -- and then unify a :=: Foo a - -uUnrefined subst tv1 ty2 (TyVarTy tv2) - | tv1 == tv2 -- Same type variable - = return subst - - -- Check to see whether tv2 is refined - | Just ty' <- lookupVarEnv subst tv2 - = uUnrefined subst tv1 ty' ty' - - -- So both are unrefined; next, see if the kinds force the direction - | k1 == k2 -- Can update either; so check the bind-flags - = do { b1 <- tvBindFlag tv1 - ; b2 <- tvBindFlag tv2 - ; case (b1,b2) of - (BindMe, _) -> bind tv1 ty2 - - (AvoidMe, BindMe) -> bind tv2 ty1 - (AvoidMe, _) -> bind tv1 ty2 - - (WildCard, WildCard) -> return subst - (WildCard, Skolem) -> return subst - (WildCard, _) -> bind tv2 ty1 - - (Skolem, WildCard) -> return subst - (Skolem, Skolem) -> failWith (misMatch ty1 ty2) - (Skolem, _) -> bind tv2 ty1 - } - - | k1 `isSubKind` k2 = bindTv subst tv2 ty1 -- Must update tv2 - | k2 `isSubKind` k1 = bindTv subst tv1 ty2 -- Must update tv1 - - | otherwise = failWith (kindMisMatch tv1 ty2) - where - ty1 = TyVarTy tv1 - k1 = tyVarKind tv1 - k2 = tyVarKind tv2 - bind tv ty = return (extendVarEnv subst tv ty) - -uUnrefined subst tv1 ty2 ty2' -- ty2 is not a type variable - | tv1 `elemVarSet` substTvSet subst (tyVarsOfType ty2') - = failWith (occursCheck tv1 ty2) -- Occurs check - | not (k2 `isSubKind` k1) - = failWith (kindMisMatch tv1 ty2) -- Kind check - | otherwise - = bindTv subst tv1 ty2 -- Bind tyvar to the synonym if poss - where - k1 = tyVarKind tv1 - k2 = typeKind ty2' - -substTvSet :: TvSubstEnv -> TyVarSet -> TyVarSet --- Apply the non-idempotent substitution to a set of type variables, --- remembering that the substitution isn't necessarily idempotent -substTvSet subst tvs - = foldVarSet (unionVarSet . get) emptyVarSet tvs - where - get tv = case lookupVarEnv subst tv of - Nothing -> unitVarSet tv - Just ty -> substTvSet subst (tyVarsOfType ty) - -bindTv subst tv ty -- ty is not a type variable - = do { b <- tvBindFlag tv - ; case b of - Skolem -> failWith (misMatch (TyVarTy tv) ty) - WildCard -> return subst - other -> return (extendVarEnv subst tv ty) - } -\end{code} - -%************************************************************************ -%* * - Unification monad -%* * -%************************************************************************ - -\begin{code} -data BindFlag - = BindMe -- A regular type variable - | AvoidMe -- Like BindMe but, given the choice, avoid binding it - - | Skolem -- This type variable is a skolem constant - -- Don't bind it; it only matches itself - - | WildCard -- This type variable matches anything, - -- and does not affect the substitution - -newtype UM a = UM { unUM :: (TyVar -> BindFlag) - -> MaybeErr Message a } - -instance Monad UM where - return a = UM (\tvs -> Succeeded a) - fail s = UM (\tvs -> Failed (text s)) - m >>= k = UM (\tvs -> case unUM m tvs of - Failed err -> Failed err - Succeeded v -> unUM (k v) tvs) - -initUM :: (TyVar -> BindFlag) -> UM a -> MaybeErr Message a -initUM badtvs um = unUM um badtvs - -tvBindFlag :: TyVar -> UM BindFlag -tvBindFlag tv = UM (\tv_fn -> Succeeded (tv_fn tv)) - -failWith :: Message -> UM a -failWith msg = UM (\tv_fn -> Failed msg) - -maybeErrToMaybe :: MaybeErr fail succ -> Maybe succ -maybeErrToMaybe (Succeeded a) = Just a -maybeErrToMaybe (Failed m) = Nothing - ------------------------------- -repSplitAppTy_maybe :: Type -> Maybe (Type,Type) --- Like Type.splitAppTy_maybe, but any coreView stuff is already done -repSplitAppTy_maybe (FunTy ty1 ty2) = Just (TyConApp funTyCon [ty1], ty2) -repSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2) -repSplitAppTy_maybe (TyConApp tc tys) = case snocView tys of - Just (tys', ty') -> Just (TyConApp tc tys', ty') - Nothing -> Nothing -repSplitAppTy_maybe other = Nothing -\end{code} - - -%************************************************************************ -%* * - Error reporting - We go to a lot more trouble to tidy the types - in TcUnify. Maybe we'll end up having to do that - here too, but I'll leave it for now. -%* * -%************************************************************************ - -\begin{code} -misMatch t1 t2 - = ptext SLIT("Can't match types") <+> quotes (ppr t1) <+> - ptext SLIT("and") <+> quotes (ppr t2) - -lengthMisMatch tys1 tys2 - = sep [ptext SLIT("Can't match unequal length lists"), - nest 2 (ppr tys1), nest 2 (ppr tys2) ] - -kindMisMatch tv1 t2 - = vcat [ptext SLIT("Can't match kinds") <+> quotes (ppr (tyVarKind tv1)) <+> - ptext SLIT("and") <+> quotes (ppr (typeKind t2)), - ptext SLIT("when matching") <+> quotes (ppr tv1) <+> - ptext SLIT("with") <+> quotes (ppr t2)] - -occursCheck tv ty - = hang (ptext SLIT("Can't construct the infinite type")) - 2 (ppr tv <+> equals <+> ppr ty) -\end{code} \ No newline at end of file