X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypes%2FUnify.lhs;h=9c448ce0653af13079713ebe84b28896ced3781d;hp=d301b7659134d76b8e2e9603f77c9a0f99636d58;hb=914e415702a25a6e52ab1eaaf2aea233d6c6097e;hpb=17b297d97d327620ed6bfab942f8992b2446f1bf diff --git a/compiler/types/Unify.lhs b/compiler/types/Unify.lhs index d301b76..9c448ce 100644 --- a/compiler/types/Unify.lhs +++ b/compiler/types/Unify.lhs @@ -3,21 +3,21 @@ % \begin{code} -{-# OPTIONS_GHC -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/WorkingConventions#Warnings --- for details - module Unify ( -- Matching of types: -- the "tc" prefix indicates that matching always -- respects newtypes (rather than looking through them) tcMatchTy, tcMatchTys, tcMatchTyX, - ruleMatchTyX, tcMatchPreds, MatchEnv(..), - - dataConCannotMatch + ruleMatchTyX, tcMatchPreds, + + MatchEnv(..), matchList, + + typesCantMatch, + + -- Side-effect free unification + tcUnifyTys, BindFlag(..), + niFixTvSubst, niSubstTvSet + ) where #include "HsVersions.h" @@ -25,13 +25,17 @@ module Unify ( import Var import VarEnv import VarSet +import Kind import Type import TyCon -import DataCon import TypeRep import Outputable +import ErrUtils import Util import Maybes +import FastString + +import Control.Monad (guard) \end{code} @@ -66,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 @@ -120,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) @@ -145,35 +151,31 @@ match :: MatchEnv -- For the most part this is pushed downwards -- in-scope set of the RnEnv2 -> Type -> Type -- Template and target respectively -> Maybe TvSubstEnv --- This matcher works on source types; that is, --- it respects NewTypes and PredType +-- This matcher works on core types; that is, it ignores PredTypes +-- Watch out if newtypes become transparent agin! +-- this matcher must respect newtypes -match menv subst ty1 ty2 | Just ty1' <- tcView ty1 = match menv subst ty1' ty2 - | Just ty2' <- tcView ty2 = match menv subst ty1 ty2' +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 - | not (typeKind ty2 `isSubKind` tyVarKind tv1) - -> Nothing -- Kind mis-match - | otherwise - -> Just (extendVarEnv subst tv1' ty2) - - 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 - + = if any (inRnEnvR rn_env) (varSetElems (tyVarsOfType ty2)) + then Nothing -- Occurs check + else do { subst1 <- match_kind menv subst tv1 ty2 + -- Note [Matching kinds] + ; return (extendVarEnv subst1 tv1' ty2) } | otherwise -- tv1 is not a template tyvar = case ty2 of TyVarTy tv2 | tv1' == rnOccR rn_env tv2 -> Just subst - other -> Nothing + _ -> Nothing where rn_env = me_env menv tv1' = rnOccL rn_env tv1 @@ -196,26 +198,49 @@ match menv subst (AppTy ty1a ty1b) ty2 = do { subst' <- match menv subst ty1a ty2a ; match menv subst' ty1b ty2b } -match menv subst ty1 ty2 +match _ _ _ _ = Nothing -------------- -match_tys menv subst tys1 tys2 = match_list (match menv) subst tys1 tys2 +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 _ subst tv ty + = guard (typeKind ty `isSubKind` tyVarKind tv) >> return subst + +-- Note [Matching kinds] +-- ~~~~~~~~~~~~~~~~~~~~~ +-- For ordinary type variables, we don't want (m a) to match (n b) +-- if say (a::*) and (b::*->*). This is just a yes/no issue. +-- +-- For coercion kinds matters are more complicated. If we have a +-- coercion template variable co::a~[b], where a,b are presumably also +-- template type variables, then we must match co's kind against the +-- kind of the actual argument, so as to give bindings to a,b. +-- +-- In fact I have no example in mind that *requires* this kind-matching +-- to instantiate template type variables, but it seems like the right +-- thing to do. C.f. Note [Matching variable types] in Rules.lhs + +-------------- +match_tys :: MatchEnv -> TvSubstEnv -> [Type] -> [Type] -> Maybe TvSubstEnv +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 fn 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 fn subst tys1 tys2 = 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 match_pred menv subst (ClassP c1 tys1) (ClassP c2 tys2) | c1 == c2 = match_tys menv subst tys1 tys2 match_pred menv subst (IParam n1 t1) (IParam n2 t2) | n1 == n2 = match menv subst t1 t2 -match_pred menv subst p1 p2 = Nothing +match_pred _ _ _ _ = Nothing \end{code} @@ -291,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 @@ -321,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 @@ -334,10 +342,302 @@ dataConCannotMatch tys con | Just (f1, a1) <- repSplitAppTy_maybe ty1 = cant_match f1 f2 || cant_match a1 a2 - cant_match ty1 ty2 = False -- Safe! + cant_match _ _ = False -- Safe! -- Things we could add; -- foralls -- look through newtypes -- take account of tyvar bindings (EQ example above) -\end{code} \ No newline at end of file +\end{code} + + +%************************************************************************ +%* * + Unification +%* * +%************************************************************************ + +\begin{code} +tcUnifyTys :: (TyVar -> BindFlag) + -> [Type] -> [Type] + -> 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 +-- +tcUnifyTys bind_fn tys1 tys2 + = maybeErrToMaybe $ initUM bind_fn $ + do { subst <- unifyList emptyTvSubstEnv tys1 tys2 + + -- Find the fixed point of the resulting non-idempotent substitution + ; return (niFixTvSubst subst) } +\end{code} + + +%************************************************************************ +%* * + Non-idempotent substitution +%* * +%************************************************************************ + +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 + 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 + get tv = case lookupVarEnv subst tv of + Nothing -> unitVarSet tv + Just ty -> niSubstTvSet subst (tyVarsOfType ty) +\end{code} + +%************************************************************************ +%* * + The workhorse +%* * +%************************************************************************ + +\begin{code} +unify :: TvSubstEnv -- An existing substitution to extend + -> Type -> Type -- Types to be unified, and witness of their equality + -> 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 + +-- in unify, any NewTcApps/Preds should be taken at face value +unify subst (TyVarTy tv1) ty2 = uVar subst tv1 ty2 +unify subst ty1 (TyVarTy tv2) = uVar 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 (TyConApp tyc1 tys1) (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 _ ty1 ty2 = failWith (misMatch ty1 ty2) + -- ForAlls?? + +------------------------------ +unify_pred :: TvSubstEnv -> PredType -> PredType -> UM TvSubstEnv +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 _ p1 p2 = failWith (misMatch (PredTy p1) (PredTy p2)) + +------------------------------ +unify_tys :: TvSubstEnv -> [Type] -> [Type] -> UM TvSubstEnv +unify_tys subst xs ys = unifyList subst xs ys + +unifyList :: TvSubstEnv -> [Type] -> [Type] -> UM TvSubstEnv +unifyList subst orig_xs orig_ys + = go subst orig_xs orig_ys + where + go subst [] [] = return subst + go subst (x:xs) (y:ys) = do { subst' <- unify subst x y + ; go subst' xs ys } + go _ _ _ = failWith (lengthMisMatch orig_xs orig_ys) + +--------------------------------- +uVar :: TvSubstEnv -- An existing substitution to extend + -> TyVar -- Type variable to be unified + -> Type -- with this type + -> 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) + +uVar subst tv1 ty + = -- Check to see whether tv1 is refined by the substitution + case (lookupVarEnv subst tv1) of + Just ty' -> unify subst ty' ty -- Yes, call back into unify' + Nothing -> uUnrefined subst -- No, continue + tv1 ty ty + +uUnrefined :: TvSubstEnv -- An existing substitution to extend + -> TyVar -- Type variable to be unified + -> Type -- with this type + -> Type -- (version w/ expanded synonyms) + -> 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 + | eqKind 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 + (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` niSubstTvSet 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' + +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) + BindMe -> return $ extendVarEnv subst tv ty + } +\end{code} + +%************************************************************************ +%* * + Binding decisions +%* * +%************************************************************************ + +\begin{code} +data BindFlag + = BindMe -- A regular type variable + + | Skolem -- This type variable is a skolem constant + -- Don't bind it; it only matches itself +\end{code} + + +%************************************************************************ +%* * + Unification monad +%* * +%************************************************************************ + +\begin{code} +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 _) = 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 :: Type -> Type -> SDoc +misMatch t1 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"), + 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)] + +occursCheck :: TyVar -> Type -> SDoc +occursCheck tv ty + = hang (ptext (sLit "Can't construct the infinite type")) + 2 (ppr tv <+> equals <+> ppr ty) +\end{code}