use an explicit substitution
\begin{code}
-module Unify ( unifyTysX, unifyTyListsX,
- match, matchTy, matchTys
+module Unify ( unifyTysX, unifyTyListsX, unifyExtendTysX,
+ allDistinctTyVars,
+ match, matchTy, matchTys,
) where
-import TypeRep ( Type(..), funTyCon
- ) -- friend
-import Type ( typeKind, tyVarsOfType, splitAppTy_maybe
+#include "HsVersions.h"
+
+import TypeRep ( Type(..) ) -- friend
+import Type ( typeKind, tyVarsOfType, splitAppTy_maybe, getTyVar_maybe,
+ splitUTy, isUTy, deNoteType
)
import PprType () -- Instances
-- PprType is below Unify in the hierarchy, which in turn makes
-- fewer modules boot-import PprType
-import Var ( TyVar, tyVarKind )
+import Var ( tyVarKind )
import VarSet
import VarEnv ( TyVarSubstEnv, emptySubstEnv, lookupSubstEnv, extendSubstEnv,
SubstResult(..)
)
-import Outputable( panic )
-import Util ( snocView )
+import Outputable
\end{code}
%************************************************************************
%* *
-\subsection{Unification wih a explicit substitution}
+\subsection{Unification with an explicit substitution}
+%* *
+%************************************************************************
+
+(allDistinctTyVars tys tvs) = True
+ iff
+all the types tys are type variables,
+distinct from each other and from tvs.
+
+This is useful when checking that unification hasn't unified signature
+type variables. For example, if the type sig is
+ f :: forall a b. a -> b -> b
+we want to check that 'a' and 'b' havn't
+ (a) been unified with a non-tyvar type
+ (b) been unified with each other (all distinct)
+ (c) been unified with a variable free in the environment
+
+\begin{code}
+allDistinctTyVars :: [Type] -> TyVarSet -> Bool
+
+allDistinctTyVars [] acc
+ = True
+allDistinctTyVars (ty:tys) acc
+ = case getTyVar_maybe ty of
+ Nothing -> False -- (a)
+ Just tv | tv `elemVarSet` acc -> False -- (b) or (c)
+ | otherwise -> allDistinctTyVars tys (acc `extendVarSet` tv)
+\end{code}
+
+%************************************************************************
+%* *
+\subsection{Unification with an explicit substitution}
%* *
%************************************************************************
Unify types with an explicit substitution and no monad.
+Ignore usage annotations.
\begin{code}
type MySubst
unifyTysX tmpl_tyvars ty1 ty2
= uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
+unifyExtendTysX :: TyVarSet -- Template tyvars
+ -> TyVarSubstEnv -- Substitution to start with
+ -> Type
+ -> Type
+ -> Maybe TyVarSubstEnv -- Extended substitution
+unifyExtendTysX tmpl_tyvars subst ty1 ty2
+ = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, subst)
+
unifyTyListsX :: TyVarSet -> [Type] -> [Type]
-> Maybe TyVarSubstEnv
unifyTyListsX tmpl_tyvars tys1 tys2
uTysX ty1 (ForAllTy _ _) k subst = panic "Unify.uTysX subst:ForAllTy (2nd arg)"
#endif
+ -- Ignore usages
+uTysX (UsageTy _ t1) t2 k subst = uTysX t1 t2 k subst
+uTysX t1 (UsageTy _ t2) k subst = uTysX t1 t2 k subst
+
-- Anything else fails
uTysX ty1 ty2 k subst = Nothing
| typeKind ty2 == tyVarKind tv1
&& occur_check_ok ty2
-> -- No kind mismatch nor occur check
- k (tmpls, extendSubstEnv env tv1 (DoneTy ty2))
+ UASSERT( not (isUTy ty2) )
+ k (tmpls, extendSubstEnv env tv1 (DoneTy ty2))
| otherwise -> Nothing -- Fail if kind mis-match or occur check
where
types. It also fails on nested foralls.
@matchTys@ matches corresponding elements of a list of templates and
-types.
+types. It and @matchTy@ both ignore usage annotations, unlike the
+main function @match@.
\begin{code}
matchTy :: TyVarSet -- Template tyvars
-> Maybe (TyVarSubstEnv, -- Matching substitution
[Type]) -- Left over instance types
-matchTy tmpls ty1 ty2 = match ty1 ty2 tmpls (\ senv -> Just senv) emptySubstEnv
+matchTy tmpls ty1 ty2 = match False ty1 ty2 tmpls (\ senv -> Just senv) emptySubstEnv
-matchTys tmpls tys1 tys2 = match_list tys1 tys2 tmpls
+matchTys tmpls tys1 tys2 = match_list False tys1 tys2 tmpls
(\ (senv,tys) -> Just (senv,tys))
emptySubstEnv
\end{code}
-@match@ is the main function.
+@match@ is the main function. It takes a flag indicating whether
+usage annotations are to be respected.
\begin{code}
-match :: Type -> Type -- Current match pair
+match :: Bool -- Respect usages?
+ -> Type -> Type -- Current match pair
-> TyVarSet -- Template vars
-> (TyVarSubstEnv -> Maybe result) -- Continuation
-> TyVarSubstEnv -- Current subst
-- has already been bound. If so, check that what it's bound to
-- is the same as ty; if not, bind it and carry on.
-match (TyVarTy v) ty tmpls k senv
+match uflag (TyVarTy v) ty tmpls k senv
| v `elemVarSet` tmpls
= -- v is a template variable
case lookupSubstEnv senv v of
- Nothing -> k (extendSubstEnv senv v (DoneTy ty))
+ Nothing -> UASSERT( not (isUTy ty) )
+ k (extendSubstEnv senv v (DoneTy ty))
Just (DoneTy ty') | ty' == ty -> k senv -- Succeeds
| otherwise -> Nothing -- Fails
| otherwise
= -- v is not a template variable; ty had better match
-- Can't use (==) because types differ
- case ty of
+ case deNoteType ty of
TyVarTy v' | v == v' -> k senv -- Success
other -> Nothing -- Failure
+ -- This deNoteType is *required* and cost me much pain. I guess
+ -- the reason the Note-stripping case is *last* rather than first
+ -- is to preserve type synonyms etc., so I'm not moving it to the
+ -- top; but this means that (without the deNotetype) a type
+ -- variable may not match the pattern (TyVarTy v') as one would
+ -- expect, due to an intervening Note. KSW 2000-06.
-match (FunTy arg1 res1) (FunTy arg2 res2) tmpls k senv
- = match arg1 arg2 tmpls (match res1 res2 tmpls k) senv
+match uflag (FunTy arg1 res1) (FunTy arg2 res2) tmpls k senv
+ = match uflag arg1 arg2 tmpls (match uflag res1 res2 tmpls k) senv
-match (AppTy fun1 arg1) ty2 tmpls k senv
+match uflag (AppTy fun1 arg1) ty2 tmpls k senv
= case splitAppTy_maybe ty2 of
- Just (fun2,arg2) -> match fun1 fun2 tmpls (match arg1 arg2 tmpls k) senv
+ Just (fun2,arg2) -> match uflag fun1 fun2 tmpls (match uflag arg1 arg2 tmpls k) senv
Nothing -> Nothing -- Fail
-match (TyConApp tc1 tys1) (TyConApp tc2 tys2) tmpls k senv
+match uflag (TyConApp tc1 tys1) (TyConApp tc2 tys2) tmpls k senv
| tc1 == tc2
- = match_list tys1 tys2 tmpls k' senv
+ = match_list uflag tys1 tys2 tmpls k' senv
where
k' (senv', tys2') | null tys2' = k senv' -- Succeed
| otherwise = Nothing -- Fail
+match False (UsageTy _ ty1) ty2 tmpls k senv = match False ty1 ty2 tmpls k senv
+match False ty1 (UsageTy _ ty2) tmpls k senv = match False ty1 ty2 tmpls k senv
+
+match True (UsageTy u1 ty1) (UsageTy u2 ty2) tmpls k senv
+ = match True u1 u2 tmpls (match True ty1 ty2 tmpls k) senv
+match True ty1@(UsageTy _ _) ty2 tmpls k senv
+ = case splitUTy ty2 of { (u,ty2') -> match True ty1 ty2' tmpls k senv }
+match True ty1 ty2@(UsageTy _ _) tmpls k senv
+ = case splitUTy ty1 of { (u,ty1') -> match True ty1' ty2 tmpls k senv }
+
-- With type synonyms, we have to be careful for the exact
-- same reasons as in the unifier. Please see the
-- considerable commentary there before changing anything
-- here! (WDP 95/05)
-match (NoteTy _ ty1) ty2 tmpls k senv = match ty1 ty2 tmpls k senv
-match ty1 (NoteTy _ ty2) tmpls k senv = match ty1 ty2 tmpls k senv
+match uflag (NoteTy _ ty1) ty2 tmpls k senv = match uflag ty1 ty2 tmpls k senv
+match uflag ty1 (NoteTy _ ty2) tmpls k senv = match uflag ty1 ty2 tmpls k senv
-- Catch-all fails
-match _ _ _ _ _ = Nothing
+match _ _ _ _ _ _ = Nothing
-match_list [] tys2 tmpls k senv = k (senv, tys2)
-match_list (ty1:tys1) [] tmpls k senv = Nothing -- Not enough arg tys => failure
-match_list (ty1:tys1) (ty2:tys2) tmpls k senv = match ty1 ty2 tmpls (match_list tys1 tys2 tmpls k) senv
+match_list uflag [] tys2 tmpls k senv = k (senv, tys2)
+match_list uflag (ty1:tys1) [] tmpls k senv = Nothing -- Not enough arg tys => failure
+match_list uflag (ty1:tys1) (ty2:tys2) tmpls k senv
+ = match uflag ty1 ty2 tmpls (match_list uflag tys1 tys2 tmpls k) senv
\end{code}
+
projects / ghc-hetmet.git / blobdiff