X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypes%2FUnify.lhs;h=9c448ce0653af13079713ebe84b28896ced3781d;hp=9137150cc3fe84164c905a38fcc2ce320fb288ae;hb=f537dd87c4a07526e2b1fc1bd1c125d652833641;hpb=3d5970436af5ab73957278671059e00d1a52c616 diff --git a/compiler/types/Unify.lhs b/compiler/types/Unify.lhs index 9137150..9c448ce 100644 --- a/compiler/types/Unify.lhs +++ b/compiler/types/Unify.lhs @@ -8,16 +8,15 @@ module Unify ( -- the "tc" prefix indicates that matching always -- respects newtypes (rather than looking through them) tcMatchTy, tcMatchTys, tcMatchTyX, - ruleMatchTyX, tcMatchPreds, MatchEnv(..), - - dataConCannotMatch, + ruleMatchTyX, tcMatchPreds, - -- GADT type refinement - Refinement, emptyRefinement, isEmptyRefinement, - matchRefine, refineType, refinePred, refineResType, + MatchEnv(..), matchList, - -- side-effect free unification - tcUnifyTys, BindFlag(..) + typesCantMatch, + + -- Side-effect free unification + tcUnifyTys, BindFlag(..), + niFixTvSubst, niSubstTvSet ) where @@ -26,17 +25,17 @@ module Unify ( import Var import VarEnv import VarSet +import Kind import Type -import Coercion import TyCon -import DataCon import TypeRep import Outputable import ErrUtils import Util import Maybes -import UniqFM import FastString + +import Control.Monad (guard) \end{code} @@ -71,9 +70,11 @@ Matching is much tricker than you might think. \begin{code} data MatchEnv - = ME { me_tmpls :: VarSet -- Template tyvars + = ME { me_tmpls :: VarSet -- Template variables , me_env :: RnEnv2 -- Renaming envt for nested foralls - } -- In-scope set includes template tyvars + } -- In-scope set includes template variables + -- Nota Bene: MatchEnv isn't specific to Types. It is used + -- for matching terms and coercions as well as types tcMatchTy :: TyVarSet -- Template tyvars -> Type -- Template @@ -125,7 +126,7 @@ tcMatchPreds -> [PredType] -> [PredType] -> Maybe TvSubstEnv tcMatchPreds tmpls ps1 ps2 - = match_list (match_pred menv) emptyTvSubstEnv ps1 ps2 + = matchList (match_pred menv) emptyTvSubstEnv ps1 ps2 where menv = ME { me_tmpls = mkVarSet tmpls, me_env = mkRnEnv2 in_scope_tyvars } in_scope_tyvars = mkInScopeSet (tyVarsOfTheta ps1 `unionVarSet` tyVarsOfTheta ps2) @@ -158,23 +159,18 @@ match menv subst ty1 ty2 | Just ty1' <- coreView ty1 = match menv subst ty1' ty2 | Just ty2' <- coreView ty2 = match menv subst ty1 ty2' match menv subst (TyVarTy tv1) ty2 + | Just ty1' <- lookupVarEnv subst tv1' -- tv1' is already bound + = if eqTypeX (nukeRnEnvL rn_env) ty1' ty2 + -- ty1 has no locally-bound variables, hence nukeRnEnvL + then Just subst + else Nothing -- ty2 doesn't match + | tv1' `elemVarSet` me_tmpls menv - = case lookupVarEnv subst tv1' of - Nothing -- No existing binding - | any (inRnEnvR rn_env) (varSetElems (tyVarsOfType ty2)) - -> Nothing -- Occurs check - | otherwise - -> do { subst1 <- match_kind menv subst tv1 ty2 - ; return (extendVarEnv subst1 tv1' ty2) } + = if any (inRnEnvR rn_env) (varSetElems (tyVarsOfType ty2)) + then Nothing -- Occurs check + else do { subst1 <- match_kind menv subst tv1 ty2 -- Note [Matching kinds] - - Just ty1' -- There is an existing binding; check whether ty2 matches it - | tcEqTypeX (nukeRnEnvL rn_env) ty1' ty2 - -- ty1 has no locally-bound variables, hence nukeRnEnvL - -- Note tcEqType...we are doing source-type matching here - -> Just subst - | otherwise -> Nothing -- ty2 doesn't match - + ; return (extendVarEnv subst1 tv1' ty2) } | otherwise -- tv1 is not a template tyvar = case ty2 of @@ -209,14 +205,8 @@ match _ _ _ _ match_kind :: MatchEnv -> TvSubstEnv -> TyVar -> Type -> Maybe TvSubstEnv -- Match the kind of the template tyvar with the kind of Type -- Note [Matching kinds] -match_kind menv subst tv ty - | isCoVar tv = do { let (ty1,ty2) = splitCoercionKind (tyVarKind tv) - (ty3,ty4) = coercionKind ty - ; subst1 <- match menv subst ty1 ty3 - ; match menv subst1 ty2 ty4 } - | otherwise = if typeKind ty `isSubKind` tyVarKind tv - then Just subst - else Nothing +match_kind _ subst tv ty + = guard (typeKind ty `isSubKind` tyVarKind tv) >> return subst -- Note [Matching kinds] -- ~~~~~~~~~~~~~~~~~~~~~ @@ -234,15 +224,15 @@ match_kind menv subst tv ty -------------- match_tys :: MatchEnv -> TvSubstEnv -> [Type] -> [Type] -> Maybe TvSubstEnv -match_tys menv subst tys1 tys2 = match_list (match menv) subst tys1 tys2 +match_tys menv subst tys1 tys2 = matchList (match menv) subst tys1 tys2 -------------- -match_list :: (TvSubstEnv -> a -> a -> Maybe TvSubstEnv) - -> TvSubstEnv -> [a] -> [a] -> Maybe TvSubstEnv -match_list _ subst [] [] = Just subst -match_list fn subst (ty1:tys1) (ty2:tys2) = do { subst' <- fn subst ty1 ty2 - ; match_list fn subst' tys1 tys2 } -match_list _ _ _ _ = Nothing +matchList :: (env -> a -> b -> Maybe env) + -> env -> [a] -> [b] -> Maybe env +matchList _ subst [] [] = Just subst +matchList fn subst (a:as) (b:bs) = do { subst' <- fn subst a b + ; matchList fn subst' as bs } +matchList _ _ _ _ = Nothing -------------- match_pred :: MatchEnv -> TvSubstEnv -> PredType -> PredType -> Maybe TvSubstEnv @@ -326,26 +316,9 @@ anything, type functions (incl newtypes) match anything, and only distinct data types fail to match. We can elaborate later. \begin{code} -dataConCannotMatch :: [Type] -> DataCon -> Bool --- Returns True iff the data con *definitely cannot* match a --- scrutinee of type (T tys) --- where T is the type constructor for the data con --- -dataConCannotMatch tys con - | null eq_spec = False -- Common - | all isTyVarTy tys = False -- Also common - | otherwise - = cant_match_s (map (substTyVar subst . fst) eq_spec) - (map snd eq_spec) +typesCantMatch :: [(Type,Type)] -> Bool +typesCantMatch prs = any (\(s,t) -> cant_match s t) prs where - dc_tvs = dataConUnivTyVars con - eq_spec = dataConEqSpec con - subst = zipTopTvSubst dc_tvs tys - - cant_match_s :: [Type] -> [Type] -> Bool - cant_match_s tys1 tys2 = ASSERT( equalLength tys1 tys2 ) - or (zipWith cant_match tys1 tys2) - cant_match :: Type -> Type -> Bool cant_match t1 t2 | Just t1' <- coreView t1 = cant_match t1' t2 @@ -356,7 +329,7 @@ dataConCannotMatch tys con cant_match (TyConApp tc1 tys1) (TyConApp tc2 tys2) | isDataTyCon tc1 && isDataTyCon tc2 - = tc1 /= tc2 || cant_match_s tys1 tys2 + = tc1 /= tc2 || typesCantMatch (zipEqual "typesCantMatch" tys1 tys2) cant_match (FunTy {}) (TyConApp tc _) = isDataTyCon tc cant_match (TyConApp tc _) (FunTy {}) = isDataTyCon tc @@ -380,142 +353,14 @@ dataConCannotMatch tys con %************************************************************************ %* * - What a refinement is -%* * -%************************************************************************ - -\begin{code} -data Refinement = Reft InScopeSet InternalReft - -type InternalReft = TyVarEnv (Coercion, Type) --- INVARIANT: a->(co,ty) then co :: (a:=:ty) --- Not necessarily idemopotent - -instance Outputable Refinement where - ppr (Reft _in_scope env) - = ptext SLIT("Refinement") <+> - braces (ppr env) - -emptyRefinement :: Refinement -emptyRefinement = (Reft emptyInScopeSet emptyVarEnv) - -isEmptyRefinement :: Refinement -> Bool -isEmptyRefinement (Reft _ env) = isEmptyVarEnv env - -refineType :: Refinement -> Type -> Maybe (Coercion, Type) --- Apply the refinement to the type. --- If (refineType r ty) = (co, ty') --- Then co :: ty:=:ty' --- Nothing => the refinement does nothing to this type -refineType (Reft in_scope env) ty - | not (isEmptyVarEnv env), -- Common case - any (`elemVarEnv` env) (varSetElems (tyVarsOfType ty)) - = Just (substTy co_subst ty, substTy tv_subst ty) - | otherwise - = Nothing -- The type doesn't mention any refined type variables - where - tv_subst = mkTvSubst in_scope (mapVarEnv snd env) - co_subst = mkTvSubst in_scope (mapVarEnv fst env) - -refinePred :: Refinement -> PredType -> Maybe (Coercion, PredType) -refinePred (Reft in_scope env) pred - | not (isEmptyVarEnv env), -- Common case - any (`elemVarEnv` env) (varSetElems (tyVarsOfPred pred)) - = Just (mkPredTy (substPred co_subst pred), substPred tv_subst pred) - | otherwise - = Nothing -- The type doesn't mention any refined type variables - where - tv_subst = mkTvSubst in_scope (mapVarEnv snd env) - co_subst = mkTvSubst in_scope (mapVarEnv fst env) - -refineResType :: Refinement -> Type -> Maybe (Coercion, Type) --- Like refineType, but returns the 'sym' coercion --- If (refineResType r ty) = (co, ty') --- Then co :: ty':=:ty -refineResType reft ty - = case refineType reft ty of - Just (co, ty1) -> Just (mkSymCoercion co, ty1) - Nothing -> Nothing -\end{code} - - -%************************************************************************ -%* * - Simple generation of a type refinement -%* * -%************************************************************************ - -\begin{code} -matchRefine :: [CoVar] -> Refinement -\end{code} - -Given a list of coercions, where for each coercion c::(ty1~ty2), the type ty2 -is a specialisation of ty1, produce a type refinement that maps the variables -of ty1 to the corresponding sub-terms of ty2 using appropriate coercions; eg, - - matchRefine (co :: [(a, b)] ~ [(c, Maybe d)]) - = { right (left (right co)) :: a ~ c - , right (right co) :: b ~ Maybe d - } - -Precondition: The rhs types must indeed be a specialisation of the lhs types; - i.e., some free variables of the lhs are replaced with either distinct free - variables or proper type terms to obtain the rhs. (We don't perform full - unification or type matching here!) - -NB: matchRefine does *not* expand the type synonyms. - -\begin{code} -matchRefine co_vars - = Reft in_scope (foldr plusVarEnv emptyVarEnv (map refineOne co_vars)) - where - in_scope = foldr extend emptyInScopeSet co_vars - - -- For each co_var, add it *and* the tyvars it mentions, to in_scope - extend co_var in_scope - = extendInScopeSetSet in_scope $ - extendVarSet (tyVarsOfType (tyVarKind co_var)) co_var - - refineOne co_var = refine (TyVarTy co_var) ty1 ty2 - where - (ty1, ty2) = splitCoercionKind (tyVarKind co_var) - - refine co (TyVarTy tv) ty = unitVarEnv tv (co, ty) - refine co (TyConApp _ tys) (TyConApp _ tys') = refineArgs co tys tys' - refine _ (PredTy _) (PredTy _) = - error "Unify.matchRefine: PredTy" - refine co (FunTy arg res) (FunTy arg' res') = - refine (mkRightCoercion (mkLeftCoercion co)) arg arg' - `plusVarEnv` - refine (mkRightCoercion co) res res' - refine co (AppTy fun arg) (AppTy fun' arg') = - refine (mkLeftCoercion co) fun fun' - `plusVarEnv` - refine (mkRightCoercion co) arg arg' - refine co (ForAllTy tv ty) (ForAllTy _tv ty') = - refine (mkForAllCoercion tv co) ty ty' `delVarEnv` tv - refine _ _ _ = error "RcGadt.matchRefine: mismatch" - - refineArgs :: Coercion -> [Type] -> [Type] -> InternalReft - refineArgs co tys tys' = - fst $ foldr refineArg (emptyVarEnv, id) (zip tys tys') - where - refineArg (ty, ty') (reft, coWrapper) - = (refine (mkRightCoercion (coWrapper co)) ty ty' `plusVarEnv` reft, - mkLeftCoercion . coWrapper) -\end{code} - - -%************************************************************************ -%* * - Unification -%* * + Unification +%* * %************************************************************************ \begin{code} tcUnifyTys :: (TyVar -> BindFlag) -> [Type] -> [Type] - -> Maybe TvSubst -- A regular one-shot substitution + -> Maybe TvSubst -- A regular one-shot (idempotent) substitution -- The two types may have common type variables, and indeed do so in the -- second call to tcUnifyTys in FunDeps.checkClsFD -- @@ -524,28 +369,48 @@ tcUnifyTys bind_fn tys1 tys2 do { subst <- unifyList emptyTvSubstEnv tys1 tys2 -- Find the fixed point of the resulting non-idempotent substitution - ; let in_scope = mkInScopeSet (tvs1 `unionVarSet` tvs2) - tv_env = fixTvSubstEnv in_scope subst + ; return (niFixTvSubst subst) } +\end{code} + + +%************************************************************************ +%* * + Non-idempotent substitution +%* * +%************************************************************************ - ; return (mkTvSubst in_scope tv_env) } +Note [Non-idempotent substitution] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +During unification we use a TvSubstEnv that is + (a) non-idempotent + (b) loop-free; ie repeatedly applying it yields a fixed point + +\begin{code} +niFixTvSubst :: TvSubstEnv -> TvSubst +-- Find the idempotent fixed point of the non-idempotent substitution +-- ToDo: use laziness instead of iteration? +niFixTvSubst env = f env where - tvs1 = tyVarsOfTypes tys1 - tvs2 = tyVarsOfTypes tys2 - ----------------------------- --- XXX Can we do this more nicely, by exploiting laziness? --- Or avoid needing it in the first place? -fixTvSubstEnv :: InScopeSet -> TvSubstEnv -> TvSubstEnv -fixTvSubstEnv in_scope env = f env + f e | not_fixpoint = f (mapVarEnv (substTy subst) e) + | otherwise = subst + where + range_tvs = foldVarEnv (unionVarSet . tyVarsOfType) emptyVarSet e + subst = mkTvSubst (mkInScopeSet range_tvs) e + not_fixpoint = foldVarSet ((||) . in_domain) False range_tvs + in_domain tv = tv `elemVarEnv` e + +niSubstTvSet :: TvSubstEnv -> TyVarSet -> TyVarSet +-- Apply the non-idempotent substitution to a set of type variables, +-- remembering that the substitution isn't necessarily idempotent +-- This is used in the occurs check, before extending the substitution +niSubstTvSet subst tvs + = foldVarSet (unionVarSet . get) emptyVarSet tvs where - f e = let e' = mapUFM (substTy (mkTvSubst in_scope e)) e - in if and $ eltsUFM $ intersectUFM_C tcEqType e e' - then e - else f e' - + get tv = case lookupVarEnv subst tv of + Nothing -> unitVarSet tv + Just ty -> niSubstTvSet subst (tyVarsOfType ty) \end{code} - %************************************************************************ %* * The workhorse @@ -624,8 +489,8 @@ uVar :: TvSubstEnv -- An existing substitution to extend -> UM TvSubstEnv -- PRE-CONDITION: in the call (uVar swap r tv1 ty), we know that --- if swap=False (tv1:=:ty) --- if swap=True (ty:=:tv1) +-- if swap=False (tv1~ty) +-- if swap=True (ty~tv1) uVar subst tv1 ty = -- Check to see whether tv1 is refined by the substitution @@ -647,7 +512,7 @@ uUnrefined subst tv1 ty2 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 + -- and then unify a ~ Foo a uUnrefined subst tv1 ty2 (TyVarTy tv2) | tv1 == tv2 -- Same type variable @@ -663,15 +528,6 @@ uUnrefined subst tv1 ty2 (TyVarTy tv2) ; 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 } @@ -687,7 +543,7 @@ uUnrefined subst tv1 ty2 (TyVarTy 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') + | tv1 `elemVarSet` niSubstTvSet subst (tyVarsOfType ty2') = failWith (occursCheck tv1 ty2) -- Occurs check | not (k2 `isSubKind` k1) = failWith (kindMisMatch tv1 ty2) -- Kind check @@ -697,43 +553,37 @@ uUnrefined subst tv1 ty2 ty2' -- ty2 is not a type variable 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 :: TvSubstEnv -> TyVar -> Type -> UM TvSubstEnv 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 + Skolem -> failWith (misMatch (TyVarTy tv) ty) + BindMe -> return $ extendVarEnv subst tv ty } \end{code} %************************************************************************ %* * - Unification monad + Binding decisions %* * %************************************************************************ \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 +\end{code} - | WildCard -- This type variable matches anything, - -- and does not affect the substitution +%************************************************************************ +%* * + Unification monad +%* * +%************************************************************************ + +\begin{code} newtype UM a = UM { unUM :: (TyVar -> BindFlag) -> MaybeErr Message a } @@ -771,23 +621,23 @@ maybeErrToMaybe (Failed _) = Nothing \begin{code} misMatch :: Type -> Type -> SDoc misMatch t1 t2 - = ptext SLIT("Can't match types") <+> quotes (ppr t1) <+> - ptext SLIT("and") <+> quotes (ppr t2) + = ptext (sLit "Can't match types") <+> quotes (ppr t1) <+> + ptext (sLit "and") <+> quotes (ppr t2) lengthMisMatch :: [Type] -> [Type] -> SDoc lengthMisMatch tys1 tys2 - = sep [ptext SLIT("Can't match unequal length lists"), + = sep [ptext (sLit "Can't match unequal length lists"), nest 2 (ppr tys1), nest 2 (ppr tys2) ] kindMisMatch :: TyVar -> Type -> SDoc 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)] + = 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 :: TyVar -> Type -> SDoc occursCheck tv ty - = hang (ptext SLIT("Can't construct the infinite type")) + = hang (ptext (sLit "Can't construct the infinite type")) 2 (ppr tv <+> equals <+> ppr ty) \end{code}