X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypes%2FUnify.lhs;h=de5ac49c2dae762788fda1596c76415eadaa3748;hb=ced4c13ea3577e01556a2f76c2cc458c0be6c83c;hp=69478bedc6f9b5b381f6b741e3f64e49f72e4065;hpb=35fc429931738f31c60e8a4bb85ef86dd7ce169e;p=ghc-hetmet.git diff --git a/compiler/types/Unify.lhs b/compiler/types/Unify.lhs index 69478be..de5ac49 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 @@ -206,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 } @@ -374,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} - %************************************************************************ %* * @@ -620,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 @@ -643,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 @@ -659,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 } @@ -707,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 } @@ -767,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}