X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypes%2FUnify.lhs;h=2f2cfb892734c4c31b990705989bd2916492f72f;hb=da43a382ccc7d3c57068976c312dc583fddc7498;hp=9137150cc3fe84164c905a38fcc2ce320fb288ae;hpb=3d5970436af5ab73957278671059e00d1a52c616;p=ghc-hetmet.git diff --git a/compiler/types/Unify.lhs b/compiler/types/Unify.lhs index 9137150..2f2cfb8 100644 --- a/compiler/types/Unify.lhs +++ b/compiler/types/Unify.lhs @@ -12,11 +12,7 @@ module Unify ( dataConCannotMatch, - -- GADT type refinement - Refinement, emptyRefinement, isEmptyRefinement, - matchRefine, refineType, refinePred, refineResType, - - -- side-effect free unification + -- Side-effect free unification tcUnifyTys, BindFlag(..) ) where @@ -158,23 +154,19 @@ 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 tcEqTypeX (nukeRnEnvL rn_env) ty1' ty2 + -- ty1 has no locally-bound variables, hence nukeRnEnvL + -- Note tcEqType...we are doing source-type matching here + 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 @@ -210,7 +202,7 @@ 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) + | isCoVar tv = do { let (ty1,ty2) = coVarKind tv (ty3,ty4) = coercionKind ty ; subst1 <- match menv subst ty1 ty3 ; match menv subst1 ty2 ty4 } @@ -378,133 +370,6 @@ dataConCannotMatch tys con \end{code} -%************************************************************************ -%* * - 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} - %************************************************************************ %* * @@ -515,7 +380,7 @@ matchRefine co_vars \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 -- @@ -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 } @@ -711,29 +567,33 @@ 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 +631,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}