2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1995
4 \section[Unify]{Unifier}
6 The unifier is now squarely in the typechecker monad (because of the
7 updatable substitution).
10 #include "HsVersions.h"
12 module Unify ( unifyTauTy, unifyTauTyList, unifyTauTyLists ) where
14 IMPORT_Trace -- ToDo: rm (debugging only)
21 import CmdLineOpts ( GlobalSwitch(..) )
22 import CoreLift ( isUnboxedButNotState )
23 import Errors ( unifyErr, UnifyErrInfo(..), UnifyErrContext )
24 import Id ( Id, DataCon(..), Inst )
25 import Maybes ( Maybe(..) )
26 import Subst ( extendSubst, SubstResult(..), Subst )
27 #if USE_ATTACK_PRAGMAS
28 import Class ( Class(..), cmpClass ) -- .. for pragmas only
29 import TyCon ( TyCon(..), isBoxedTyCon, isVisibleSynTyCon, cmpTyCon )
30 -- .. on TyCon is for pragmas only
31 import TyVar -- make all visible for pragmas
32 import UniTyFuns ( pprUniType, pprTyCon )
34 import Class ( Class )
35 import TyVar ( TyVar(..), TyVarTemplate )
36 import TyCon ( TyCon, isBoxedTyCon, isVisibleSynTyCon )
38 import UniType ( UniType(..), TauType(..)
39 IF_ATTACK_PRAGMAS(COMMA cmpUniType)
44 %************************************************************************
46 \subsection[Unify-spec]{Specification}
48 %************************************************************************
50 CLAIM: the unifier works correctly even if the types to be unified are not
51 fixed points of the substitution.
53 %************************************************************************
55 \subsection[Unify-exported]{Exported unification functions}
57 %************************************************************************
59 The exported functions are all defined as versions of some
60 non-exported generic functions.
62 Unify two @TauType@s. Dead straightforward.
65 unifyTauTy :: TauType -> TauType -> UnifyErrContext -> TcM ()
67 unifyTauTy ty1 ty2 err_ctxt = uTys ty1 ty1 ty2 ty2 err_ctxt
70 @unifyTauTyLists@ unifies corresponding elements of its two list
71 arguments. The lists should be of equal length.
74 unifyTauTyLists :: [TauType] -> [TauType] -> UnifyErrContext -> TcM ()
76 unifyTauTyLists tys1 tys2 err_ctxt = uList tys1 tys2 err_ctxt
79 @unifyTauTyList@ takes a single list of @TauType@s and unifies them
80 all together. It is used, for example, when typechecking explicit
81 lists, when all the elts should be of the same type.
84 unifyTauTyList :: [TauType] -> UnifyErrContext -> TcM ()
86 unifyTauTyList [] _ = returnTc ()
87 unifyTauTyList [ty] _ = returnTc ()
89 unifyTauTyList (ty1:tys@(ty2:_)) err_ctxt
90 = unifyTauTy ty1 ty2 err_ctxt `thenTc_`
91 unifyTauTyList tys err_ctxt
94 %************************************************************************
96 \subsection[Unify-lists-of-types]{@uList@}
98 %************************************************************************
100 @uList@ unifies corresponding elements of two lists of @TauType@s. It
101 uses @uTys@ to do the real work. We charge down the list explicitly
102 so that we can complain if their lengths differ.
105 uList :: [TauType] -> [TauType]
109 uList [] [] _ = returnTc ()
111 uList (ty1:tys1) (ty2:tys2) err_ctxt
112 = uTys ty1 ty1 ty2 ty2 err_ctxt `thenTc_`
113 uList tys1 tys2 err_ctxt
115 uList ty1s ty2s _ = panic "Unify.uList: mismatched type lists!"
118 %************************************************************************
120 \subsection[Unify-uTys]{@uTys@: getting down to business}
122 %************************************************************************
124 @uTys@ is the heart of the unifier. Each arg happens twice, because
125 we want to report errors in terms of synomyms if poss. The first of
126 the pair is used in error messages only; it is always the same as the
127 second, except that if the first is a synonym then the second may be a
128 de-synonym'd version. This way we get better error messages.
130 We call the first one \tr{ps_ty1}, \tr{ps_ty2} for ``possible synomym''.
133 uTys :: TauType -> TauType -- Error reporting ty1 and real ty1
134 -> TauType -> TauType -- Error reporting ty2 and real ty2
139 %********************************************************
141 Sanity check: should never find a UniTyVarTemplate
143 %********************************************************
148 uTys ps_ty1 ty1@(UniTyVarTemplate tv1) ps_ty2 ty2 err_ctxt
149 = pprPanic "Unify:uTys:unifying w/ UniTyVarTemplate(1):" (ppCat [ppr PprDebug tv1, ppr PprDebug ty2])
151 uTys ps_ty1 ty1 ps_ty2 ty2@(UniTyVarTemplate tv2) err_ctxt
152 = pprPanic "Unify:uTys:unifying w/ UniTyVarTemplate(2):" (ppCat [ppr PprDebug ty1, ppr PprDebug tv2])
157 %********************************************************
161 %********************************************************
164 uTys ps_ty1 (UniTyVar tyvar1) ps_ty2 ty2 err_ctxt = uVar tyvar1 ps_ty2 ty2 err_ctxt
165 uTys ps_ty1 ty1 ps_ty2 (UniTyVar tyvar2) err_ctxt = uVar tyvar2 ps_ty1 ty1 err_ctxt
168 %********************************************************
170 Both function constructors:
172 %********************************************************
175 uTys _ (UniFun fun1 arg1) _ (UniFun fun2 arg2) err_ctxt
176 = uList [fun1, arg1] [fun2, arg2] err_ctxt
179 %********************************************************
181 Both datatype constructors:
183 %********************************************************
186 uTys ps_ty1 ty1@(UniData con1 args1) ps_ty2 ty2@(UniData con2 args2) err_ctxt
187 = if (con1 == con2) then
188 -- Same constructors, just unify the arguments
189 uList args1 args2 err_ctxt
191 -- Different constructors: disaster
192 getSrcLocTc `thenNF_Tc` \ src_loc ->
193 failTc (unifyErr (UnifyMisMatch ps_ty1 ps_ty2) err_ctxt src_loc)
196 %********************************************************
200 %********************************************************
202 If just one or the other is a synonym, just expand it.
205 uTys ps_ty1 (UniSyn con1 args1 ty1) ps_ty2 ty2 err_ctxt
206 | isVisibleSynTyCon con1
207 = uTys ps_ty1 ty1 ps_ty2 ty2 err_ctxt
209 uTys ps_ty1 ty1 ps_ty2 (UniSyn con2 args2 ty2) err_ctxt
210 | isVisibleSynTyCon con2
211 = uTys ps_ty1 ty1 ps_ty2 ty2 err_ctxt
214 If you are tempted to make a short cut on synonyms, as in this
218 uTys (UniSyn con1 args1 ty1) (UniSyn con2 args2 ty2)
219 = if (con1 == con2) then
220 -- Good news! Same synonym constructors, so we can shortcut
221 -- by unifying their arguments and ignoring their expansions.
224 -- Never mind. Just expand them and try again
228 then THINK AGAIN. Here is the whole story, as detected and reported
229 by Chris Okasaki \tr{<Chris_Okasaki@loch.mess.cs.cmu.edu>}:
231 Here's a test program that should detect the problem:
235 x = (1 :: Bogus Char) :: Bogus Bool
238 The problem with [the attempted shortcut code] is that
242 is not a sufficient condition to be able to use the shortcut!
243 You also need to know that the type synonym actually USES all
244 its arguments. For example, consider the following type synonym
245 which does not use all its arguments.
250 If you ever tried unifying, say, \tr{Bogus Char} with \tr{Bogus Bool},
251 the unifier would blithely try to unify \tr{Char} with \tr{Bool} and
252 would fail, even though the expanded forms (both \tr{Int}) should
255 Similarly, unifying \tr{Bogus Char} with \tr{Bogus t} would
256 unnecessarily bind \tr{t} to \tr{Char}.
258 ... You could explicitly test for the problem synonyms and mark them
259 somehow as needing expansion, perhaps also issuing a warning to the
263 Still, if the synonym is abstract, we can only just go ahead and try!
266 uTys ps_ty1 (UniSyn con1 args1 ty1) ps_ty2 (UniSyn con2 args2 ty2) err_ctxt
267 -- Both must be abstract (i.e., non "visible" -- not done yet)
268 = if (con1 == con2) then
269 -- Good news! Same synonym constructors, so we can shortcut
270 -- by unifying their arguments and ignoring their expansions.
271 uList args1 args2 err_ctxt
273 -- Bad news; mis-matched type constructors
274 getSrcLocTc `thenNF_Tc` \ src_loc ->
275 failTc (unifyErr (UnifyMisMatch ps_ty1 ps_ty2) err_ctxt src_loc)
278 %********************************************************
280 Catch-all case---just fails:
282 %********************************************************
284 Anything else fails. For example, matching a @UniFun@ against
287 uTys ps_ty1 ty1 ps_ty2 ty2 err_ctxt
288 = getSrcLocTc `thenNF_Tc` \ src_loc ->
289 failTc (unifyErr (UnifyMisMatch ps_ty1 ps_ty2) err_ctxt src_loc)
292 %************************************************************************
294 \subsection[Unify-uVar]{@uVar@: unifying with a type variable}
296 %************************************************************************
298 @uVar@ is called when at least one of the types being unified is a
299 variable. It does {\em not} assume that the variable is a fixed point
300 of the substitution; rather, notice that @bindTo@ (defined below) nips
301 back into @uTys@ if it turns out that the variable is already bound.
303 There is a slight worry that one might try to @bindTo@ a (say) Poly
304 tyvar (as tv1) with an Open tyvar (as ty2) which is already unified to
305 an unboxed type. In fact this can't happen, because the Open ones are
306 always the ones which are unified away.
310 -> UniType -> UniType -- printing and real versions
314 uVar tv1 ps_ty2 ty2 err_ctxt
318 do _ (UniSyn _ _ ty2) = do tv1 ty2
320 -- Commit any open type variable
321 do (OpenSysTyVar _) ty2 = tv1 `bindTo` ps_ty2
322 do _ ty2@(UniTyVar tv2@(OpenSysTyVar _)) = tv2 `bindTo` ty1
324 -- Eliminate Poly in favour of User
325 do (PolySysTyVar _) ty2@(UniTyVar (UserTyVar _ _)) = tv1 `bindTo` ps_ty2
326 do (PolySysTyVar _) ty2@(UniTyVar (PolySysTyVar _)) = tv1 `bindTo` ps_ty2
327 do (UserTyVar _ _) ty2@(UniTyVar tv2@(PolySysTyVar _)) = tv2 `bindTo` ty1
328 do (UserTyVar _ _) ty2@(UniTyVar (UserTyVar _ _)) = tv1 `bindTo` ps_ty2
330 -- Matching for boxed data types
331 do (PolySysTyVar _) ty2@(UniData con _) | isBoxedTyCon con = tv1 `bindTo` ps_ty2
332 do (UserTyVar _ _) ty2@(UniData con _) | isBoxedTyCon con = tv1 `bindTo` ps_ty2
334 -- Matching for unboxed data types:
335 -- requires specialisation w.r.t. the unboxed type
336 do (PolySysTyVar _) ty2@(UniData con _) = tv1 `bindToUnboxed` ps_ty2
337 do (UserTyVar _ _) ty2@(UniData con _) = tv1 `bindToUnboxed` ps_ty2
339 -- Matching for function types
340 do (PolySysTyVar _) ty2@(UniFun _ _) = tv1 `bindTo` ps_ty2
341 do (UserTyVar _ _) ty2@(UniFun _ _) = tv1 `bindTo` ps_ty2
344 do _ _ = getSrcLocTc `thenNF_Tc` \ src_loc ->
345 failTc (unifyErr (UnifyMisMatch ty1 ps_ty2) err_ctxt src_loc)
347 ----------- END OF CASES ---------------
352 = extendSubstTc tyvar1 ty2 err_ctxt
354 tyvar1 `bindToUnboxed` ty2
355 = getSwitchCheckerTc `thenNF_Tc` \ sw_chkr ->
356 if sw_chkr SpecialiseUnboxed && isUnboxedButNotState ty2 then
357 extendSubstTc tyvar1 ty2 err_ctxt
359 getSrcLocTc `thenNF_Tc` \ src_loc ->
360 failTc (unifyErr (UnifyUnboxedMisMatch ty1 ps_ty2) err_ctxt src_loc)