2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
6 This module contains a unifier and a matcher, both of which
7 use an explicit substitution
10 module Unify ( unifyTysX, unifyTyListsX, unifyExtendTysX,
12 match, matchTy, matchTys,
15 #include "HsVersions.h"
17 import TypeRep ( Type(..) ) -- friend
18 import Type ( typeKind, tyVarsOfType, splitAppTy_maybe, getTyVar_maybe,
19 splitUTy, isUTy, deNoteType
22 import PprType () -- Instances
23 -- This import isn't strictly necessary, but it makes sure that
24 -- PprType is below Unify in the hierarchy, which in turn makes
25 -- fewer modules boot-import PprType
27 import Var ( tyVarKind )
29 import VarEnv ( TyVarSubstEnv, emptySubstEnv, lookupSubstEnv, extendSubstEnv,
36 %************************************************************************
38 \subsection{Unification with an explicit substitution}
40 %************************************************************************
42 (allDistinctTyVars tys tvs) = True
44 all the types tys are type variables,
45 distinct from each other and from tvs.
47 This is useful when checking that unification hasn't unified signature
48 type variables. For example, if the type sig is
49 f :: forall a b. a -> b -> b
50 we want to check that 'a' and 'b' havn't
51 (a) been unified with a non-tyvar type
52 (b) been unified with each other (all distinct)
53 (c) been unified with a variable free in the environment
56 allDistinctTyVars :: [Type] -> TyVarSet -> Bool
58 allDistinctTyVars [] acc
60 allDistinctTyVars (ty:tys) acc
61 = case getTyVar_maybe ty of
62 Nothing -> False -- (a)
63 Just tv | tv `elemVarSet` acc -> False -- (b) or (c)
64 | otherwise -> allDistinctTyVars tys (acc `extendVarSet` tv)
67 %************************************************************************
69 \subsection{Unification with an explicit substitution}
71 %************************************************************************
73 Unify types with an explicit substitution and no monad.
74 Ignore usage annotations.
78 = (TyVarSet, -- Set of template tyvars
79 TyVarSubstEnv) -- Not necessarily idempotent
81 unifyTysX :: TyVarSet -- Template tyvars
84 -> Maybe TyVarSubstEnv
85 unifyTysX tmpl_tyvars ty1 ty2
86 = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
88 unifyExtendTysX :: TyVarSet -- Template tyvars
89 -> TyVarSubstEnv -- Substitution to start with
92 -> Maybe TyVarSubstEnv -- Extended substitution
93 unifyExtendTysX tmpl_tyvars subst ty1 ty2
94 = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, subst)
96 unifyTyListsX :: TyVarSet -> [Type] -> [Type]
97 -> Maybe TyVarSubstEnv
98 unifyTyListsX tmpl_tyvars tys1 tys2
99 = uTyListsX tys1 tys2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
104 -> (MySubst -> Maybe result)
108 uTysX (NoteTy _ ty1) ty2 k subst = uTysX ty1 ty2 k subst
109 uTysX ty1 (NoteTy _ ty2) k subst = uTysX ty1 ty2 k subst
111 -- Variables; go for uVar
112 uTysX (TyVarTy tyvar1) (TyVarTy tyvar2) k subst
115 uTysX (TyVarTy tyvar1) ty2 k subst@(tmpls,_)
116 | tyvar1 `elemVarSet` tmpls
117 = uVarX tyvar1 ty2 k subst
118 uTysX ty1 (TyVarTy tyvar2) k subst@(tmpls,_)
119 | tyvar2 `elemVarSet` tmpls
120 = uVarX tyvar2 ty1 k subst
122 -- Functions; just check the two parts
123 uTysX (FunTy fun1 arg1) (FunTy fun2 arg2) k subst
124 = uTysX fun1 fun2 (uTysX arg1 arg2 k) subst
126 -- Type constructors must match
127 uTysX (TyConApp con1 tys1) (TyConApp con2 tys2) k subst
128 | (con1 == con2 && length tys1 == length tys2)
129 = uTyListsX tys1 tys2 k subst
131 -- Applications need a bit of care!
132 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
133 -- NB: we've already dealt with type variables and Notes,
134 -- so if one type is an App the other one jolly well better be too
135 uTysX (AppTy s1 t1) ty2 k subst
136 = case splitAppTy_maybe ty2 of
137 Just (s2, t2) -> uTysX s1 s2 (uTysX t1 t2 k) subst
138 Nothing -> Nothing -- Fail
140 uTysX ty1 (AppTy s2 t2) k subst
141 = case splitAppTy_maybe ty1 of
142 Just (s1, t1) -> uTysX s1 s2 (uTysX t1 t2 k) subst
143 Nothing -> Nothing -- Fail
145 -- Not expecting for-alls in unification
147 uTysX (ForAllTy _ _) ty2 k subst = panic "Unify.uTysX subst:ForAllTy (1st arg)"
148 uTysX ty1 (ForAllTy _ _) k subst = panic "Unify.uTysX subst:ForAllTy (2nd arg)"
152 uTysX (UsageTy _ t1) t2 k subst = uTysX t1 t2 k subst
153 uTysX t1 (UsageTy _ t2) k subst = uTysX t1 t2 k subst
155 -- Anything else fails
156 uTysX ty1 ty2 k subst = Nothing
159 uTyListsX [] [] k subst = k subst
160 uTyListsX (ty1:tys1) (ty2:tys2) k subst = uTysX ty1 ty2 (uTyListsX tys1 tys2 k) subst
161 uTyListsX tys1 tys2 k subst = Nothing -- Fail if the lists are different lengths
165 -- Invariant: tv1 is a unifiable variable
166 uVarX tv1 ty2 k subst@(tmpls, env)
167 = case lookupSubstEnv env tv1 of
168 Just (DoneTy ty1) -> -- Already bound
169 uTysX ty1 ty2 k subst
171 Nothing -- Not already bound
172 | typeKind ty2 == tyVarKind tv1
173 && occur_check_ok ty2
174 -> -- No kind mismatch nor occur check
175 UASSERT( not (isUTy ty2) )
176 k (tmpls, extendSubstEnv env tv1 (DoneTy ty2))
178 | otherwise -> Nothing -- Fail if kind mis-match or occur check
180 occur_check_ok ty = all occur_check_ok_tv (varSetElems (tyVarsOfType ty))
181 occur_check_ok_tv tv | tv1 == tv = False
182 | otherwise = case lookupSubstEnv env tv of
184 Just (DoneTy ty) -> occur_check_ok ty
189 %************************************************************************
191 \subsection{Matching on types}
193 %************************************************************************
195 Matching is a {\em unidirectional} process, matching a type against a
196 template (which is just a type with type variables in it). The
197 matcher assumes that there are no repeated type variables in the
198 template, so that it simply returns a mapping of type variables to
199 types. It also fails on nested foralls.
201 @matchTys@ matches corresponding elements of a list of templates and
202 types. It and @matchTy@ both ignore usage annotations, unlike the
203 main function @match@.
206 matchTy :: TyVarSet -- Template tyvars
208 -> Type -- Proposed instance of template
209 -> Maybe TyVarSubstEnv -- Matching substitution
212 matchTys :: TyVarSet -- Template tyvars
213 -> [Type] -- Templates
214 -> [Type] -- Proposed instance of template
215 -> Maybe (TyVarSubstEnv, -- Matching substitution
216 [Type]) -- Left over instance types
218 matchTy tmpls ty1 ty2 = match False ty1 ty2 tmpls (\ senv -> Just senv) emptySubstEnv
220 matchTys tmpls tys1 tys2 = match_list False tys1 tys2 tmpls
221 (\ (senv,tys) -> Just (senv,tys))
225 @match@ is the main function. It takes a flag indicating whether
226 usage annotations are to be respected.
229 match :: Bool -- Respect usages?
230 -> Type -> Type -- Current match pair
231 -> TyVarSet -- Template vars
232 -> (TyVarSubstEnv -> Maybe result) -- Continuation
233 -> TyVarSubstEnv -- Current subst
236 -- When matching against a type variable, see if the variable
237 -- has already been bound. If so, check that what it's bound to
238 -- is the same as ty; if not, bind it and carry on.
240 match uflag (TyVarTy v) ty tmpls k senv
241 | v `elemVarSet` tmpls
242 = -- v is a template variable
243 case lookupSubstEnv senv v of
244 Nothing -> UASSERT( not (isUTy ty) )
245 k (extendSubstEnv senv v (DoneTy ty))
246 Just (DoneTy ty') | ty' == ty -> k senv -- Succeeds
247 | otherwise -> Nothing -- Fails
250 = -- v is not a template variable; ty had better match
251 -- Can't use (==) because types differ
252 case deNoteType ty of
253 TyVarTy v' | v == v' -> k senv -- Success
254 other -> Nothing -- Failure
255 -- This deNoteType is *required* and cost me much pain. I guess
256 -- the reason the Note-stripping case is *last* rather than first
257 -- is to preserve type synonyms etc., so I'm not moving it to the
258 -- top; but this means that (without the deNotetype) a type
259 -- variable may not match the pattern (TyVarTy v') as one would
260 -- expect, due to an intervening Note. KSW 2000-06.
262 match uflag (FunTy arg1 res1) (FunTy arg2 res2) tmpls k senv
263 = match uflag arg1 arg2 tmpls (match uflag res1 res2 tmpls k) senv
265 match uflag (AppTy fun1 arg1) ty2 tmpls k senv
266 = case splitAppTy_maybe ty2 of
267 Just (fun2,arg2) -> match uflag fun1 fun2 tmpls (match uflag arg1 arg2 tmpls k) senv
268 Nothing -> Nothing -- Fail
270 match uflag (TyConApp tc1 tys1) (TyConApp tc2 tys2) tmpls k senv
272 = match_list uflag tys1 tys2 tmpls k' senv
274 k' (senv', tys2') | null tys2' = k senv' -- Succeed
275 | otherwise = Nothing -- Fail
277 match False (UsageTy _ ty1) ty2 tmpls k senv = match False ty1 ty2 tmpls k senv
278 match False ty1 (UsageTy _ ty2) tmpls k senv = match False ty1 ty2 tmpls k senv
280 match True (UsageTy u1 ty1) (UsageTy u2 ty2) tmpls k senv
281 = match True u1 u2 tmpls (match True ty1 ty2 tmpls k) senv
282 match True ty1@(UsageTy _ _) ty2 tmpls k senv
283 = case splitUTy ty2 of { (u,ty2') -> match True ty1 ty2' tmpls k senv }
284 match True ty1 ty2@(UsageTy _ _) tmpls k senv
285 = case splitUTy ty1 of { (u,ty1') -> match True ty1' ty2 tmpls k senv }
287 -- With type synonyms, we have to be careful for the exact
288 -- same reasons as in the unifier. Please see the
289 -- considerable commentary there before changing anything
291 match uflag (NoteTy _ ty1) ty2 tmpls k senv = match uflag ty1 ty2 tmpls k senv
292 match uflag ty1 (NoteTy _ ty2) tmpls k senv = match uflag ty1 ty2 tmpls k senv
295 match _ _ _ _ _ _ = Nothing
297 match_list uflag [] tys2 tmpls k senv = k (senv, tys2)
298 match_list uflag (ty1:tys1) [] tmpls k senv = Nothing -- Not enough arg tys => failure
299 match_list uflag (ty1:tys1) (ty2:tys2) tmpls k senv
300 = match uflag ty1 ty2 tmpls (match_list uflag tys1 tys2 tmpls k) senv