-- the "tc" prefix indicates that matching always
-- respects newtypes (rather than looking through them)
tcMatchTy, tcMatchTys, tcMatchTyX,
- ruleMatchTyX, tcMatchPreds, MatchEnv(..),
-
- dataConCannotMatch,
+ ruleMatchTyX, tcMatchPreds,
- -- GADT type refinement
- Refinement, emptyRefinement, isEmptyRefinement,
- matchRefine, refineType, refinePred, refineResType,
+ MatchEnv(..), matchList,
- -- side-effect free unification
- tcUnifyTys, BindFlag(..)
+ typesCantMatch,
+
+ -- Side-effect free unification
+ tcUnifyTys, BindFlag(..),
+ niFixTvSubst, niSubstTvSet
) where
import Var
import VarEnv
import VarSet
+import Kind
import Type
-import Coercion
import TyCon
-import DataCon
import TypeRep
import Outputable
import ErrUtils
import Util
import Maybes
-import UniqFM
import FastString
+
+import Control.Monad (guard)
\end{code}
\begin{code}
data MatchEnv
- = ME { me_tmpls :: VarSet -- Template tyvars
+ = ME { me_tmpls :: VarSet -- Template variables
, me_env :: RnEnv2 -- Renaming envt for nested foralls
- } -- In-scope set includes template tyvars
+ } -- In-scope set includes template variables
+ -- Nota Bene: MatchEnv isn't specific to Types. It is used
+ -- for matching terms and coercions as well as types
tcMatchTy :: TyVarSet -- Template tyvars
-> Type -- Template
-> [PredType] -> [PredType]
-> Maybe TvSubstEnv
tcMatchPreds tmpls ps1 ps2
- = match_list (match_pred menv) emptyTvSubstEnv ps1 ps2
+ = matchList (match_pred menv) emptyTvSubstEnv ps1 ps2
where
menv = ME { me_tmpls = mkVarSet tmpls, me_env = mkRnEnv2 in_scope_tyvars }
in_scope_tyvars = mkInScopeSet (tyVarsOfTheta ps1 `unionVarSet` tyVarsOfTheta ps2)
match menv subst (TyVarTy tv1) ty2
| Just ty1' <- lookupVarEnv subst tv1' -- tv1' is already bound
- = if tcEqTypeX (nukeRnEnvL rn_env) ty1' ty2
+ = if eqTypeX (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
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)
- (ty3,ty4) = coercionKind ty
- ; subst1 <- match menv subst ty1 ty3
- ; match menv subst1 ty2 ty4 }
- | otherwise = if typeKind ty `isSubKind` tyVarKind tv
- then Just subst
- else Nothing
+match_kind _ subst tv ty
+ = guard (typeKind ty `isSubKind` tyVarKind tv) >> return subst
-- Note [Matching kinds]
-- ~~~~~~~~~~~~~~~~~~~~~
--------------
match_tys :: MatchEnv -> TvSubstEnv -> [Type] -> [Type] -> Maybe TvSubstEnv
-match_tys menv subst tys1 tys2 = match_list (match menv) subst tys1 tys2
+match_tys menv subst tys1 tys2 = matchList (match menv) subst tys1 tys2
--------------
-match_list :: (TvSubstEnv -> a -> a -> Maybe TvSubstEnv)
- -> TvSubstEnv -> [a] -> [a] -> Maybe TvSubstEnv
-match_list _ subst [] [] = Just subst
-match_list fn subst (ty1:tys1) (ty2:tys2) = do { subst' <- fn subst ty1 ty2
- ; match_list fn subst' tys1 tys2 }
-match_list _ _ _ _ = Nothing
+matchList :: (env -> a -> b -> Maybe env)
+ -> env -> [a] -> [b] -> Maybe env
+matchList _ subst [] [] = Just subst
+matchList fn subst (a:as) (b:bs) = do { subst' <- fn subst a b
+ ; matchList fn subst' as bs }
+matchList _ _ _ _ = Nothing
--------------
match_pred :: MatchEnv -> TvSubstEnv -> PredType -> PredType -> Maybe TvSubstEnv
distinct data types fail to match. We can elaborate later.
\begin{code}
-dataConCannotMatch :: [Type] -> DataCon -> Bool
--- Returns True iff the data con *definitely cannot* match a
--- scrutinee of type (T tys)
--- where T is the type constructor for the data con
---
-dataConCannotMatch tys con
- | null eq_spec = False -- Common
- | all isTyVarTy tys = False -- Also common
- | otherwise
- = cant_match_s (map (substTyVar subst . fst) eq_spec)
- (map snd eq_spec)
+typesCantMatch :: [(Type,Type)] -> Bool
+typesCantMatch prs = any (\(s,t) -> cant_match s t) prs
where
- dc_tvs = dataConUnivTyVars con
- eq_spec = dataConEqSpec con
- subst = zipTopTvSubst dc_tvs tys
-
- cant_match_s :: [Type] -> [Type] -> Bool
- cant_match_s tys1 tys2 = ASSERT( equalLength tys1 tys2 )
- or (zipWith cant_match tys1 tys2)
-
cant_match :: Type -> Type -> Bool
cant_match t1 t2
| Just t1' <- coreView t1 = cant_match t1' t2
cant_match (TyConApp tc1 tys1) (TyConApp tc2 tys2)
| isDataTyCon tc1 && isDataTyCon tc2
- = tc1 /= tc2 || cant_match_s tys1 tys2
+ = tc1 /= tc2 || typesCantMatch (zipEqual "typesCantMatch" tys1 tys2)
cant_match (FunTy {}) (TyConApp tc _) = isDataTyCon tc
cant_match (TyConApp tc _) (FunTy {}) = isDataTyCon tc
%************************************************************************
%* *
- 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}
-
-
-%************************************************************************
-%* *
- Unification
-%* *
+ Unification
+%* *
%************************************************************************
\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
--
do { subst <- unifyList emptyTvSubstEnv tys1 tys2
-- Find the fixed point of the resulting non-idempotent substitution
- ; let in_scope = mkInScopeSet (tvs1 `unionVarSet` tvs2)
- tv_env = fixTvSubstEnv in_scope subst
+ ; return (niFixTvSubst subst) }
+\end{code}
+
+
+%************************************************************************
+%* *
+ Non-idempotent substitution
+%* *
+%************************************************************************
+
+Note [Non-idempotent substitution]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+During unification we use a TvSubstEnv that is
+ (a) non-idempotent
+ (b) loop-free; ie repeatedly applying it yields a fixed point
- ; return (mkTvSubst in_scope tv_env) }
+\begin{code}
+niFixTvSubst :: TvSubstEnv -> TvSubst
+-- Find the idempotent fixed point of the non-idempotent substitution
+-- ToDo: use laziness instead of iteration?
+niFixTvSubst env = f env
where
- tvs1 = tyVarsOfTypes tys1
- tvs2 = tyVarsOfTypes tys2
-
-----------------------------
--- XXX Can we do this more nicely, by exploiting laziness?
--- Or avoid needing it in the first place?
-fixTvSubstEnv :: InScopeSet -> TvSubstEnv -> TvSubstEnv
-fixTvSubstEnv in_scope env = f env
+ f e | not_fixpoint = f (mapVarEnv (substTy subst) e)
+ | otherwise = subst
+ where
+ range_tvs = foldVarEnv (unionVarSet . tyVarsOfType) emptyVarSet e
+ subst = mkTvSubst (mkInScopeSet range_tvs) e
+ not_fixpoint = foldVarSet ((||) . in_domain) False range_tvs
+ in_domain tv = tv `elemVarEnv` e
+
+niSubstTvSet :: TvSubstEnv -> TyVarSet -> TyVarSet
+-- Apply the non-idempotent substitution to a set of type variables,
+-- remembering that the substitution isn't necessarily idempotent
+-- This is used in the occurs check, before extending the substitution
+niSubstTvSet subst tvs
+ = foldVarSet (unionVarSet . get) emptyVarSet tvs
where
- f e = let e' = mapUFM (substTy (mkTvSubst in_scope e)) e
- in if and $ eltsUFM $ intersectUFM_C tcEqType e e'
- then e
- else f e'
-
+ get tv = case lookupVarEnv subst tv of
+ Nothing -> unitVarSet tv
+ Just ty -> niSubstTvSet subst (tyVarsOfType ty)
\end{code}
-
%************************************************************************
%* *
The workhorse
-> 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
= 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
; 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
}
bind tv ty = return $ extendVarEnv subst tv ty
uUnrefined subst tv1 ty2 ty2' -- ty2 is not a type variable
- | tv1 `elemVarSet` substTvSet subst (tyVarsOfType ty2')
+ | tv1 `elemVarSet` niSubstTvSet subst (tyVarsOfType ty2')
= failWith (occursCheck tv1 ty2) -- Occurs check
| not (k2 `isSubKind` k1)
= failWith (kindMisMatch tv1 ty2) -- Kind check
k1 = tyVarKind tv1
k2 = typeKind ty2'
-substTvSet :: TvSubstEnv -> TyVarSet -> TyVarSet
--- Apply the non-idempotent substitution to a set of type variables,
--- remembering that the substitution isn't necessarily idempotent
-substTvSet subst tvs
- = foldVarSet (unionVarSet . get) emptyVarSet tvs
- where
- get tv = case lookupVarEnv subst tv of
- Nothing -> unitVarSet tv
- Just ty -> substTvSet subst (tyVarsOfType ty)
-
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 }
\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