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
11 unifyTysX, unifyTyListsX,
15 import Var ( TyVar, tyVarKind )
17 import VarSet ( varSetElems )
18 import Type ( Type(..), funTyCon, typeKind, tyVarsOfType,
21 import Unique ( Uniquable(..) )
22 import Outputable( panic )
23 import Util ( snocView )
26 %************************************************************************
28 \subsection{Unification wih a explicit substitution}
30 %************************************************************************
32 Unify types with an explicit substitution and no monad.
36 = ([TyVar], -- Set of template tyvars
37 TyVarEnv Type) -- Not necessarily idempotent
39 unifyTysX :: [TyVar] -- Template tyvars
42 -> Maybe (TyVarEnv Type)
43 unifyTysX tmpl_tyvars ty1 ty2
44 = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, emptyVarEnv)
46 unifyTyListsX :: [TyVar] -> [Type] -> [Type]
47 -> Maybe (TyVarEnv Type)
48 unifyTyListsX tmpl_tyvars tys1 tys2
49 = uTyListsX tys1 tys2 (\(_,s) -> Just s) (tmpl_tyvars, emptyVarEnv)
54 -> (Subst -> Maybe result)
58 uTysX (NoteTy _ ty1) ty2 k subst = uTysX ty1 ty2 k subst
59 uTysX ty1 (NoteTy _ ty2) k subst = uTysX ty1 ty2 k subst
61 -- Variables; go for uVar
62 uTysX (TyVarTy tyvar1) (TyVarTy tyvar2) k subst
65 uTysX (TyVarTy tyvar1) ty2 k subst@(tmpls,_)
67 = uVarX tyvar1 ty2 k subst
68 uTysX ty1 (TyVarTy tyvar2) k subst@(tmpls,_)
70 = uVarX tyvar2 ty1 k subst
72 -- Functions; just check the two parts
73 uTysX (FunTy fun1 arg1) (FunTy fun2 arg2) k subst
74 = uTysX fun1 fun2 (uTysX arg1 arg2 k) subst
76 -- Type constructors must match
77 uTysX (TyConApp con1 tys1) (TyConApp con2 tys2) k subst
78 | (con1 == con2 && length tys1 == length tys2)
79 = uTyListsX tys1 tys2 k subst
81 -- Applications need a bit of care!
82 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
83 -- NB: we've already dealt with type variables and Notes,
84 -- so if one type is an App the other one jolly well better be too
85 uTysX (AppTy s1 t1) ty2 k subst
86 = case splitAppTy_maybe ty2 of
87 Just (s2, t2) -> uTysX s1 s2 (uTysX t1 t2 k) subst
88 Nothing -> Nothing -- Fail
90 uTysX ty1 (AppTy s2 t2) k subst
91 = case splitAppTy_maybe ty1 of
92 Just (s1, t1) -> uTysX s1 s2 (uTysX t1 t2 k) subst
93 Nothing -> Nothing -- Fail
95 -- Not expecting for-alls in unification
97 uTysX (ForAllTy _ _) ty2 k subst = panic "Unify.uTysX subst:ForAllTy (1st arg)"
98 uTysX ty1 (ForAllTy _ _) k subst = panic "Unify.uTysX subst:ForAllTy (2nd arg)"
101 -- Anything else fails
102 uTysX ty1 ty2 k subst = Nothing
105 uTyListsX [] [] k subst = k subst
106 uTyListsX (ty1:tys1) (ty2:tys2) k subst = uTysX ty1 ty2 (uTyListsX tys1 tys2 k) subst
107 uTyListsX tys1 tys2 k subst = Nothing -- Fail if the lists are different lengths
111 -- Invariant: tv1 is a unifiable variable
112 uVarX tv1 ty2 k subst@(tmpls, env)
113 = case lookupVarEnv env tv1 of
114 Just ty1 -> -- Already bound
115 uTysX ty1 ty2 k subst
117 Nothing -- Not already bound
118 | typeKind ty2 == tyVarKind tv1
119 && occur_check_ok ty2
120 -> -- No kind mismatch nor occur check
121 k (tmpls, extendVarEnv env tv1 ty2)
123 | otherwise -> Nothing -- Fail if kind mis-match or occur check
125 occur_check_ok ty = all occur_check_ok_tv (varSetElems (tyVarsOfType ty))
126 occur_check_ok_tv tv | tv1 == tv = False
127 | otherwise = case lookupVarEnv env tv of
129 Just ty -> occur_check_ok ty
134 %************************************************************************
136 \subsection{Matching on types}
138 %************************************************************************
140 Matching is a {\em unidirectional} process, matching a type against a
141 template (which is just a type with type variables in it). The
142 matcher assumes that there are no repeated type variables in the
143 template, so that it simply returns a mapping of type variables to
144 types. It also fails on nested foralls.
146 @matchTys@ matches corresponding elements of a list of templates and
150 matchTy :: [TyVar] -- Template tyvars
152 -> Type -- Proposed instance of template
153 -> Maybe (TyVarEnv Type) -- Matching substitution
156 matchTys :: [TyVar] -- Template tyvars
157 -> [Type] -- Templates
158 -> [Type] -- Proposed instance of template
159 -> Maybe (TyVarEnv Type, -- Matching substitution
160 [Type]) -- Left over instance types
162 matchTy tmpls ty1 ty2 = match ty1 ty2 (\(_,env) -> Just env)
165 matchTys tmpls tys1 tys2 = match_list tys1 tys2 (\((_,env),tys) -> Just (env,tys))
169 @match@ is the main function.
172 match :: Type -> Type -- Current match pair
173 -> (Subst -> Maybe result) -- Continuation
174 -> Subst -- Current substitution
177 -- When matching against a type variable, see if the variable
178 -- has already been bound. If so, check that what it's bound to
179 -- is the same as ty; if not, bind it and carry on.
181 match (TyVarTy v) ty k = \ s@(tmpls,env) ->
182 if v `elem` tmpls then
183 -- v is a template variable
184 case lookupVarEnv env v of
185 Nothing -> k (tmpls, extendVarEnv env v ty)
186 Just ty' | ty' == ty -> k s -- Succeeds
187 | otherwise -> Nothing -- Fails
189 -- v is not a template variable; ty had better match
190 -- Can't use (==) because types differ
192 TyVarTy v' | getUnique v == getUnique v'
194 other -> Nothing -- Failure
196 match (FunTy arg1 res1) (FunTy arg2 res2) k = match arg1 arg2 (match res1 res2 k)
197 match (AppTy fun1 arg1) ty2 k = case splitAppTy_maybe ty2 of
198 Just (fun2,arg2) -> match fun1 fun2 (match arg1 arg2 k)
199 Nothing -> \ _ -> Nothing -- Fail
200 match (TyConApp tc1 tys1) (TyConApp tc2 tys2) k | tc1 == tc2
201 = match_list tys1 tys2 ( \(s,tys2') ->
208 -- With type synonyms, we have to be careful for the exact
209 -- same reasons as in the unifier. Please see the
210 -- considerable commentary there before changing anything
212 match (NoteTy _ ty1) ty2 k = match ty1 ty2 k
213 match ty1 (NoteTy _ ty2) k = match ty1 ty2 k
216 match _ _ _ = \s -> Nothing
218 match_list [] tys2 k = \s -> k (s, tys2)
219 match_list (ty1:tys1) [] k = \s -> Nothing -- Not enough arg tys => failure
220 match_list (ty1:tys1) (ty2:tys2) k = match ty1 ty2 (match_list tys1 tys2 k)