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,
11 match, matchTy, matchTys
14 #include "HsVersions.h"
16 import TypeRep ( Type(..) ) -- friend
17 import Type ( typeKind, tyVarsOfType, splitAppTy_maybe,
18 splitUTy, isUTy, deNoteType
21 import PprType () -- Instances
22 -- This import isn't strictly necessary, but it makes sure that
23 -- PprType is below Unify in the hierarchy, which in turn makes
24 -- fewer modules boot-import PprType
26 import Var ( tyVarKind )
28 import VarEnv ( TyVarSubstEnv, emptySubstEnv, lookupSubstEnv, extendSubstEnv,
35 %************************************************************************
37 \subsection{Unification with an explicit substitution}
39 %************************************************************************
41 Unify types with an explicit substitution and no monad.
42 Ignore usage annotations.
46 = (TyVarSet, -- Set of template tyvars
47 TyVarSubstEnv) -- Not necessarily idempotent
49 unifyTysX :: TyVarSet -- Template tyvars
52 -> Maybe TyVarSubstEnv
53 unifyTysX tmpl_tyvars ty1 ty2
54 = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
56 unifyTyListsX :: TyVarSet -> [Type] -> [Type]
57 -> Maybe TyVarSubstEnv
58 unifyTyListsX tmpl_tyvars tys1 tys2
59 = uTyListsX tys1 tys2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
64 -> (MySubst -> Maybe result)
68 uTysX (NoteTy _ ty1) ty2 k subst = uTysX ty1 ty2 k subst
69 uTysX ty1 (NoteTy _ ty2) k subst = uTysX ty1 ty2 k subst
71 -- Variables; go for uVar
72 uTysX (TyVarTy tyvar1) (TyVarTy tyvar2) k subst
75 uTysX (TyVarTy tyvar1) ty2 k subst@(tmpls,_)
76 | tyvar1 `elemVarSet` tmpls
77 = uVarX tyvar1 ty2 k subst
78 uTysX ty1 (TyVarTy tyvar2) k subst@(tmpls,_)
79 | tyvar2 `elemVarSet` tmpls
80 = uVarX tyvar2 ty1 k subst
82 -- Functions; just check the two parts
83 uTysX (FunTy fun1 arg1) (FunTy fun2 arg2) k subst
84 = uTysX fun1 fun2 (uTysX arg1 arg2 k) subst
86 -- Type constructors must match
87 uTysX (TyConApp con1 tys1) (TyConApp con2 tys2) k subst
88 | (con1 == con2 && length tys1 == length tys2)
89 = uTyListsX tys1 tys2 k subst
91 -- Applications need a bit of care!
92 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
93 -- NB: we've already dealt with type variables and Notes,
94 -- so if one type is an App the other one jolly well better be too
95 uTysX (AppTy s1 t1) ty2 k subst
96 = case splitAppTy_maybe ty2 of
97 Just (s2, t2) -> uTysX s1 s2 (uTysX t1 t2 k) subst
98 Nothing -> Nothing -- Fail
100 uTysX ty1 (AppTy s2 t2) k subst
101 = case splitAppTy_maybe ty1 of
102 Just (s1, t1) -> uTysX s1 s2 (uTysX t1 t2 k) subst
103 Nothing -> Nothing -- Fail
105 -- Not expecting for-alls in unification
107 uTysX (ForAllTy _ _) ty2 k subst = panic "Unify.uTysX subst:ForAllTy (1st arg)"
108 uTysX ty1 (ForAllTy _ _) k subst = panic "Unify.uTysX subst:ForAllTy (2nd arg)"
112 uTysX (UsageTy _ t1) t2 k subst = uTysX t1 t2 k subst
113 uTysX t1 (UsageTy _ t2) k subst = uTysX t1 t2 k subst
115 -- Anything else fails
116 uTysX ty1 ty2 k subst = Nothing
119 uTyListsX [] [] k subst = k subst
120 uTyListsX (ty1:tys1) (ty2:tys2) k subst = uTysX ty1 ty2 (uTyListsX tys1 tys2 k) subst
121 uTyListsX tys1 tys2 k subst = Nothing -- Fail if the lists are different lengths
125 -- Invariant: tv1 is a unifiable variable
126 uVarX tv1 ty2 k subst@(tmpls, env)
127 = case lookupSubstEnv env tv1 of
128 Just (DoneTy ty1) -> -- Already bound
129 uTysX ty1 ty2 k subst
131 Nothing -- Not already bound
132 | typeKind ty2 == tyVarKind tv1
133 && occur_check_ok ty2
134 -> -- No kind mismatch nor occur check
135 UASSERT( not (isUTy ty2) )
136 k (tmpls, extendSubstEnv env tv1 (DoneTy ty2))
138 | otherwise -> Nothing -- Fail if kind mis-match or occur check
140 occur_check_ok ty = all occur_check_ok_tv (varSetElems (tyVarsOfType ty))
141 occur_check_ok_tv tv | tv1 == tv = False
142 | otherwise = case lookupSubstEnv env tv of
144 Just (DoneTy ty) -> occur_check_ok ty
149 %************************************************************************
151 \subsection{Matching on types}
153 %************************************************************************
155 Matching is a {\em unidirectional} process, matching a type against a
156 template (which is just a type with type variables in it). The
157 matcher assumes that there are no repeated type variables in the
158 template, so that it simply returns a mapping of type variables to
159 types. It also fails on nested foralls.
161 @matchTys@ matches corresponding elements of a list of templates and
162 types. It and @matchTy@ both ignore usage annotations, unlike the
163 main function @match@.
166 matchTy :: TyVarSet -- Template tyvars
168 -> Type -- Proposed instance of template
169 -> Maybe TyVarSubstEnv -- Matching substitution
172 matchTys :: TyVarSet -- Template tyvars
173 -> [Type] -- Templates
174 -> [Type] -- Proposed instance of template
175 -> Maybe (TyVarSubstEnv, -- Matching substitution
176 [Type]) -- Left over instance types
178 matchTy tmpls ty1 ty2 = match False ty1 ty2 tmpls (\ senv -> Just senv) emptySubstEnv
180 matchTys tmpls tys1 tys2 = match_list False tys1 tys2 tmpls
181 (\ (senv,tys) -> Just (senv,tys))
185 @match@ is the main function. It takes a flag indicating whether
186 usage annotations are to be respected.
189 match :: Bool -- Respect usages?
190 -> Type -> Type -- Current match pair
191 -> TyVarSet -- Template vars
192 -> (TyVarSubstEnv -> Maybe result) -- Continuation
193 -> TyVarSubstEnv -- Current subst
196 -- When matching against a type variable, see if the variable
197 -- has already been bound. If so, check that what it's bound to
198 -- is the same as ty; if not, bind it and carry on.
200 match uflag (TyVarTy v) ty tmpls k senv
201 | v `elemVarSet` tmpls
202 = -- v is a template variable
203 case lookupSubstEnv senv v of
204 Nothing -> UASSERT( not (isUTy ty) )
205 k (extendSubstEnv senv v (DoneTy ty))
206 Just (DoneTy ty') | ty' == ty -> k senv -- Succeeds
207 | otherwise -> Nothing -- Fails
210 = -- v is not a template variable; ty had better match
211 -- Can't use (==) because types differ
212 case deNoteType ty of
213 TyVarTy v' | v == v' -> k senv -- Success
214 other -> Nothing -- Failure
215 -- This deNoteType is *required* and cost me much pain. I guess
216 -- the reason the Note-stripping case is *last* rather than first
217 -- is to preserve type synonyms etc., so I'm not moving it to the
218 -- top; but this means that (without the deNotetype) a type
219 -- variable may not match the pattern (TyVarTy v') as one would
220 -- expect, due to an intervening Note. KSW 2000-06.
222 match uflag (FunTy arg1 res1) (FunTy arg2 res2) tmpls k senv
223 = match uflag arg1 arg2 tmpls (match uflag res1 res2 tmpls k) senv
225 match uflag (AppTy fun1 arg1) ty2 tmpls k senv
226 = case splitAppTy_maybe ty2 of
227 Just (fun2,arg2) -> match uflag fun1 fun2 tmpls (match uflag arg1 arg2 tmpls k) senv
228 Nothing -> Nothing -- Fail
230 match uflag (TyConApp tc1 tys1) (TyConApp tc2 tys2) tmpls k senv
232 = match_list uflag tys1 tys2 tmpls k' senv
234 k' (senv', tys2') | null tys2' = k senv' -- Succeed
235 | otherwise = Nothing -- Fail
237 match False (UsageTy _ ty1) ty2 tmpls k senv = match False ty1 ty2 tmpls k senv
238 match False ty1 (UsageTy _ ty2) tmpls k senv = match False ty1 ty2 tmpls k senv
240 match True (UsageTy u1 ty1) (UsageTy u2 ty2) tmpls k senv
241 = match True u1 u2 tmpls (match True ty1 ty2 tmpls k) senv
242 match True ty1@(UsageTy _ _) ty2 tmpls k senv
243 = case splitUTy ty2 of { (u,ty2') -> match True ty1 ty2' tmpls k senv }
244 match True ty1 ty2@(UsageTy _ _) tmpls k senv
245 = case splitUTy ty1 of { (u,ty1') -> match True ty1' ty2 tmpls k senv }
247 -- With type synonyms, we have to be careful for the exact
248 -- same reasons as in the unifier. Please see the
249 -- considerable commentary there before changing anything
251 match uflag (NoteTy _ ty1) ty2 tmpls k senv = match uflag ty1 ty2 tmpls k senv
252 match uflag ty1 (NoteTy _ ty2) tmpls k senv = match uflag ty1 ty2 tmpls k senv
255 match _ _ _ _ _ _ = Nothing
257 match_list uflag [] tys2 tmpls k senv = k (senv, tys2)
258 match_list uflag (ty1:tys1) [] tmpls k senv = Nothing -- Not enough arg tys => failure
259 match_list uflag (ty1:tys1) (ty2:tys2) tmpls k senv
260 = match uflag ty1 ty2 tmpls (match_list uflag tys1 tys2 tmpls k) senv