X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypes%2FUnify.lhs;h=7195e5b2f54a425e3b54ae6db71d29309af66cd2;hb=0e73a9fbdc8555ffb948cfd72401a700b122c395;hp=9137150cc3fe84164c905a38fcc2ce320fb288ae;hpb=3d5970436af5ab73957278671059e00d1a52c616;p=ghc-hetmet.git diff --git a/compiler/types/Unify.lhs b/compiler/types/Unify.lhs index 9137150..7195e5b 100644 --- a/compiler/types/Unify.lhs +++ b/compiler/types/Unify.lhs @@ -158,23 +158,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 +206,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 } @@ -388,12 +384,12 @@ dataConCannotMatch tys con data Refinement = Reft InScopeSet InternalReft type InternalReft = TyVarEnv (Coercion, Type) --- INVARIANT: a->(co,ty) then co :: (a:=:ty) +-- INVARIANT: a->(co,ty) then co :: (a~ty) -- Not necessarily idemopotent instance Outputable Refinement where ppr (Reft _in_scope env) - = ptext SLIT("Refinement") <+> + = ptext (sLit "Refinement") <+> braces (ppr env) emptyRefinement :: Refinement @@ -405,7 +401,7 @@ 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' +-- Then co :: ty~ty' -- Nothing => the refinement does nothing to this type refineType (Reft in_scope env) ty | not (isEmptyVarEnv env), -- Common case @@ -431,7 +427,7 @@ refinePred (Reft in_scope env) pred refineResType :: Refinement -> Type -> Maybe (Coercion, Type) -- Like refineType, but returns the 'sym' coercion -- If (refineResType r ty) = (co, ty') --- Then co :: ty':=:ty +-- Then co :: ty'~ty refineResType reft ty = case refineType reft ty of Just (co, ty1) -> Just (mkSymCoercion co, ty1) @@ -446,7 +442,7 @@ refineResType reft ty %************************************************************************ \begin{code} -matchRefine :: [CoVar] -> Refinement +matchRefine :: [TyVar] -> [Coercion] -> Refinement \end{code} Given a list of coercions, where for each coercion c::(ty1~ty2), the type ty2 @@ -466,19 +462,16 @@ Precondition: The rhs types must indeed be a specialisation of the lhs types; NB: matchRefine does *not* expand the type synonyms. \begin{code} -matchRefine co_vars - = Reft in_scope (foldr plusVarEnv emptyVarEnv (map refineOne co_vars)) +matchRefine in_scope_tvs cos + = Reft in_scope (foldr plusVarEnv emptyVarEnv (map refineOne cos)) where - in_scope = foldr extend emptyInScopeSet co_vars + in_scope = mkInScopeSet (mkVarSet in_scope_tvs) + -- NB: in_scope_tvs include both coercion variables + -- *and* the tyvars in their kinds - -- 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 + refineOne co = refine co ty1 ty2 where - (ty1, ty2) = splitCoercionKind (tyVarKind co_var) + (ty1, ty2) = coercionKind co refine co (TyVarTy tv) ty = unitVarEnv tv (co, ty) refine co (TyConApp _ tys) (TyConApp _ tys') = refineArgs co tys tys' @@ -624,8 +617,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 +640,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 +656,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 +695,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 +759,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}