| 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
instance Outputable Refinement where
ppr (Reft _in_scope env)
- = ptext SLIT("Refinement") <+>
+ = ptext (sLit "Refinement") <+>
braces (ppr env)
emptyRefinement :: Refinement
%************************************************************************
\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
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'
; 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
}
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 }
\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}
projects / ghc-hetmet.git / blobdiff