X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypes%2FUnify.lhs;h=3e35ac6421fcce8dca6c0d2f6bb96e2033efc83c;hb=1ae354e107715a9e3fd4e2d67b61f868c090e4ae;hp=9137150cc3fe84164c905a38fcc2ce320fb288ae;hpb=3d5970436af5ab73957278671059e00d1a52c616;p=ghc-hetmet.git diff --git a/compiler/types/Unify.lhs b/compiler/types/Unify.lhs index 9137150..3e35ac6 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 @@ -393,7 +389,7 @@ type InternalReft = TyVarEnv (Coercion, Type) instance Outputable Refinement where ppr (Reft _in_scope env) - = ptext SLIT("Refinement") <+> + = ptext (sLit "Refinement") <+> braces (ppr env) emptyRefinement :: Refinement @@ -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' @@ -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}