2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1996
4 \section[Unify]{Unifier}
6 The unifier is now squarely in the typechecker monad (because of the
7 updatable substitution).
10 module Unify ( unifyTauTy, unifyTauTyList, unifyTauTyLists,
11 unifyFunTy, unifyListTy, unifyTupleTy,
12 Subst, unifyTysX, unifyTyListsX
15 #include "HsVersions.h"
19 import Type ( GenType(..), Type, tyVarsOfType,
20 typeKind, mkFunTy, splitFunTy_maybe, splitTyConApp_maybe )
21 import TyCon ( TyCon, mkFunTyCon, isTupleTyCon, tyConArity, Arity )
22 import TyVar ( TyVar, GenTyVar(..), tyVarKind, tyVarFlexi,
23 TyVarEnv, lookupTyVarEnv, emptyTyVarEnv, addToTyVarEnv,
26 import TcType ( TcType, TcMaybe(..), TcTauType, TcTyVar,
27 newTyVarTy, tcReadTyVar, tcWriteTyVar, zonkTcType
30 import Kind ( Kind, hasMoreBoxityInfo, mkTypeKind, mkBoxedTypeKind )
31 import TysWiredIn ( listTyCon, mkListTy, mkTupleTy )
32 import Maybes ( maybeToBool )
33 import PprType () -- Instances
39 %************************************************************************
41 \subsection[Unify-exported]{Exported unification functions}
43 %************************************************************************
45 The exported functions are all defined as versions of some
46 non-exported generic functions.
48 Unify two @TauType@s. Dead straightforward.
51 unifyTauTy :: TcTauType s -> TcTauType s -> TcM s ()
52 unifyTauTy ty1 ty2 -- ty1 expected, ty2 inferred
53 = tcAddErrCtxtM (unifyCtxt ty1 ty2) $
57 @unifyTauTyList@ unifies corresponding elements of two lists of
58 @TauType@s. It uses @uTys@ to do the real work. The lists should be
59 of equal length. We charge down the list explicitly so that we can
60 complain if their lengths differ.
63 unifyTauTyLists :: [TcTauType s] -> [TcTauType s] -> TcM s ()
64 unifyTauTyLists [] [] = returnTc ()
65 unifyTauTyLists (ty1:tys1) (ty2:tys2) = uTys ty1 ty1 ty2 ty2 `thenTc_`
66 unifyTauTyLists tys1 tys2
67 unifyTauTyLists ty1s ty2s = panic "Unify.unifyTauTyLists: mismatched type lists!"
70 @unifyTauTyList@ takes a single list of @TauType@s and unifies them
71 all together. It is used, for example, when typechecking explicit
72 lists, when all the elts should be of the same type.
75 unifyTauTyList :: [TcTauType s] -> TcM s ()
76 unifyTauTyList [] = returnTc ()
77 unifyTauTyList [ty] = returnTc ()
78 unifyTauTyList (ty1:tys@(ty2:_)) = unifyTauTy ty1 ty2 `thenTc_`
82 %************************************************************************
84 \subsection[Unify-uTys]{@uTys@: getting down to business}
86 %************************************************************************
88 @uTys@ is the heart of the unifier. Each arg happens twice, because
89 we want to report errors in terms of synomyms if poss. The first of
90 the pair is used in error messages only; it is always the same as the
91 second, except that if the first is a synonym then the second may be a
92 de-synonym'd version. This way we get better error messages.
94 We call the first one \tr{ps_ty1}, \tr{ps_ty2} for ``possible synomym''.
97 uTys :: TcTauType s -> TcTauType s -- Error reporting ty1 and real ty1
98 -> TcTauType s -> TcTauType s -- Error reporting ty2 and real ty2
101 -- Always expand synonyms (see notes at end)
102 uTys ps_ty1 (SynTy _ ty1) ps_ty2 ty2 = uTys ps_ty1 ty1 ps_ty2 ty2
103 uTys ps_ty1 ty1 ps_ty2 (SynTy _ ty2) = uTys ps_ty1 ty1 ps_ty2 ty2
105 -- Variables; go for uVar
106 uTys ps_ty1 (TyVarTy tyvar1) ps_ty2 ty2 = uVar tyvar1 ps_ty2 ty2
107 uTys ps_ty1 ty1 ps_ty2 (TyVarTy tyvar2) = uVar tyvar2 ps_ty1 ty1
109 -- Functions; just check the two parts
110 uTys _ (FunTy fun1 arg1) _ (FunTy fun2 arg2)
111 = uTys fun1 fun1 fun2 fun2 `thenTc_` uTys arg1 arg1 arg2 arg2
113 -- Type constructors must match
114 uTys ps_ty1 (TyConApp con1 tys1) ps_ty2 (TyConApp con2 tys2)
115 = checkTc (con1 == con2 && length tys1 == length tys2)
116 (unifyMisMatch ps_ty1 ps_ty2) `thenTc_`
117 unifyTauTyLists tys1 tys2
119 -- Applications need a bit of care!
120 -- They can match FunTy and TyConApp
121 uTys _ (AppTy s1 t1) _ (AppTy s2 t2)
122 = uTys s1 s1 s2 s2 `thenTc_` uTys t1 t1 t2 t2
124 uTys _ (AppTy s1 t1) _ (FunTy fun2 arg2)
125 = uTys s1 s1 s2 s2 `thenTc_` uTys t1 t1 t2 t2
127 -- Converts a -> b to (->) a b
128 s2 = TyConApp mkFunTyCon [fun2]
131 uTys _ (AppTy s1 t1) _ (TyConApp tc tys@(_:_))
132 = case snocView tys of
133 (ts2, t2) -> uTys s1 s1 s2 s2 `thenTc_` uTys t1 t1 t2 t2
135 -- Not efficient, but simple
138 uTys ps1 s1 ps2 s2@(AppTy _ _) = uTys ps2 s2 ps1 s1
139 -- Swap arguments if the App is in the second argument
141 -- Not expecting for-alls in unification
143 uTys ps_ty1 (ForAllTy _ _) ps_ty2 ty2 = panic "Unify.uTys:ForAllTy (1st arg)"
144 uTys ps_ty1 ty1 ps_ty2 (ForAllTy _ _) = panic "Unify.uTys:ForAllTy (2nd arg)"
147 -- Anything else fails
148 uTys ps_ty1 ty1 ps_ty2 ty2 = failWithTc (unifyMisMatch ps_ty1 ps_ty2)
153 If you are tempted to make a short cut on synonyms, as in this
157 uTys (SynTy con1 args1 ty1) (SynTy con2 args2 ty2)
158 = if (con1 == con2) then
159 -- Good news! Same synonym constructors, so we can shortcut
160 -- by unifying their arguments and ignoring their expansions.
161 unifyTauTypeLists args1 args2
163 -- Never mind. Just expand them and try again
167 then THINK AGAIN. Here is the whole story, as detected and reported
168 by Chris Okasaki \tr{<Chris_Okasaki@loch.mess.cs.cmu.edu>}:
170 Here's a test program that should detect the problem:
174 x = (1 :: Bogus Char) :: Bogus Bool
177 The problem with [the attempted shortcut code] is that
181 is not a sufficient condition to be able to use the shortcut!
182 You also need to know that the type synonym actually USES all
183 its arguments. For example, consider the following type synonym
184 which does not use all its arguments.
189 If you ever tried unifying, say, \tr{Bogus Char} with \tr{Bogus Bool},
190 the unifier would blithely try to unify \tr{Char} with \tr{Bool} and
191 would fail, even though the expanded forms (both \tr{Int}) should
194 Similarly, unifying \tr{Bogus Char} with \tr{Bogus t} would
195 unnecessarily bind \tr{t} to \tr{Char}.
197 ... You could explicitly test for the problem synonyms and mark them
198 somehow as needing expansion, perhaps also issuing a warning to the
203 %************************************************************************
205 \subsection[Unify-uVar]{@uVar@: unifying with a type variable}
207 %************************************************************************
209 @uVar@ is called when at least one of the types being unified is a
210 variable. It does {\em not} assume that the variable is a fixed point
211 of the substitution; rather, notice that @bindTo@ (defined below) nips
212 back into @uTys@ if it turns out that the variable is already bound.
214 There is a slight worry that one might try to @bindTo@ a (say) Poly
215 tyvar (as tv1) with an Open tyvar (as ty2) which is already unified to
216 an unboxed type. In fact this can't happen, because the Open ones are
217 always the ones which are unified away.
221 -> TcTauType s -> TcTauType s -- printing and real versions
225 = tcReadTyVar tv1 `thenNF_Tc` \ maybe_ty1 ->
227 BoundTo ty1 -> uTys ty1 ty1 ps_ty2 ty2
228 other -> uUnboundVar tv1 maybe_ty1 ps_ty2 ty2
231 uUnboundVar tv1 maybe_ty1 ps_ty2 (SynTy _ ty2)
232 = uUnboundVar tv1 maybe_ty1 ps_ty2 ty2
235 -- The both-type-variable case
236 uUnboundVar tv1@(TyVar uniq1 kind1 name1 box1)
239 ty2@(TyVarTy tv2@(TyVar uniq2 kind2 name2 box2))
241 -- Same type variable => no-op
245 -- Distinct type variables
246 -- ASSERT maybe_ty1 /= BoundTo
248 = tcReadTyVar tv2 `thenNF_Tc` \ maybe_ty2 ->
250 BoundTo ty2' -> uUnboundVar tv1 maybe_ty1 ty2' ty2'
252 UnBound | (kind1 == kind2 && not (maybeToBool name1)) -- Same kinds and tv1 is anonymous
254 -> tcWriteTyVar tv1 ps_ty2 `thenNF_Tc_` returnTc ()
256 | kind1 `hasMoreBoxityInfo` kind2 -- Update tv2 if possible
257 -> tcWriteTyVar tv2 (TyVarTy tv1) `thenNF_Tc_` returnTc ()
259 | kind2 `hasMoreBoxityInfo` kind1 -- Update tv1 if possible
260 -> tcWriteTyVar tv1 ps_ty2 `thenNF_Tc_` returnTc ()
262 other -> failWithTc (unifyKindErr tv1 ps_ty2)
264 -- Second one isn't a type variable
265 uUnboundVar tv1@(TyVar uniq1 kind1 name1 box1) maybe_ty1 ps_ty2 non_var_ty2
266 | typeKind non_var_ty2 `hasMoreBoxityInfo` kind1
267 = occur_check non_var_ty2 `thenTc_`
268 tcWriteTyVar tv1 ps_ty2 `thenNF_Tc_`
272 = failWithTc (unifyKindErr tv1 ps_ty2)
275 occur_check ty = mapTc occur_check_tv (tyVarSetToList (tyVarsOfType ty)) `thenTc_`
278 occur_check_tv tv2@(TyVar uniq2 _ _ box2)
279 | uniq1 == uniq2 -- Same tyvar; fail
280 = failWithTc (unifyOccurCheck tv1 ps_ty2)
282 | otherwise -- A different tyvar
283 = tcReadTyVar tv2 `thenNF_Tc` \ maybe_ty2 ->
285 BoundTo ty2' -> occur_check ty2'
289 %************************************************************************
291 \subsection[Unify-fun]{@unifyFunTy@}
293 %************************************************************************
295 @unifyFunTy@ is used to avoid the fruitless creation of type variables.
298 unifyFunTy :: TcType s -- Fail if ty isn't a function type
299 -> TcM s (TcType s, TcType s) -- otherwise return arg and result types
301 unifyFunTy ty@(TyVarTy tyvar)
302 = tcReadTyVar tyvar `thenNF_Tc` \ maybe_ty ->
304 BoundTo ty' -> unifyFunTy ty'
305 other -> unify_fun_ty_help ty
308 = case splitFunTy_maybe ty of
309 Just arg_and_res -> returnTc arg_and_res
310 Nothing -> unify_fun_ty_help ty
312 unify_fun_ty_help ty -- Special cases failed, so revert to ordinary unification
313 = newTyVarTy mkTypeKind `thenNF_Tc` \ arg ->
314 newTyVarTy mkTypeKind `thenNF_Tc` \ res ->
315 unifyTauTy ty (mkFunTy arg res) `thenTc_`
320 unifyListTy :: TcType s -- expected list type
321 -> TcM s (TcType s) -- list element type
323 unifyListTy ty@(TyVarTy tyvar)
324 = tcReadTyVar tyvar `thenNF_Tc` \ maybe_ty ->
326 BoundTo ty' -> unifyListTy ty'
327 other -> unify_list_ty_help ty
330 = case splitTyConApp_maybe ty of
331 Just (tycon, [arg_ty]) | tycon == listTyCon -> returnTc arg_ty
332 other -> unify_list_ty_help ty
334 unify_list_ty_help ty -- Revert to ordinary unification
335 = newTyVarTy mkBoxedTypeKind `thenNF_Tc` \ elt_ty ->
336 unifyTauTy ty (mkListTy elt_ty) `thenTc_`
341 unifyTupleTy :: Arity -> TcType s -> TcM s [TcType s]
342 unifyTupleTy arity ty@(TyVarTy tyvar)
343 = tcReadTyVar tyvar `thenNF_Tc` \ maybe_ty ->
345 BoundTo ty' -> unifyTupleTy arity ty'
346 other -> unify_tuple_ty_help arity ty
348 unifyTupleTy arity ty
349 = case splitTyConApp_maybe ty of
350 Just (tycon, arg_tys) | isTupleTyCon tycon
351 && tyConArity tycon == arity
353 other -> unify_tuple_ty_help arity ty
355 unify_tuple_ty_help arity ty
356 = mapNF_Tc (\ _ -> newTyVarTy mkBoxedTypeKind) [1..arity] `thenNF_Tc` \ arg_tys ->
357 unifyTauTy ty (mkTupleTy arity arg_tys) `thenTc_`
361 %************************************************************************
363 \subsection{Unification wih a explicit substitution}
365 %************************************************************************
367 Unify types with an explicit substitution and no monad.
370 type Subst = TyVarEnv (GenType Bool) -- Not necessarily idempotent
372 unifyTysX :: GenType Bool
375 unifyTysX ty1 ty2 = uTysX ty1 ty2 (\s -> Just s) emptyTyVarEnv
377 unifyTyListsX :: [GenType Bool] -> [GenType Bool] -> Maybe Subst
378 unifyTyListsX tys1 tys2 = uTyListsX tys1 tys2 (\s -> Just s) emptyTyVarEnv
381 uTysX :: GenType Bool
383 -> (Subst -> Maybe Subst)
387 uTysX (SynTy _ ty1) ty2 k subst = uTysX ty1 ty2 k subst
388 uTysX ty1 (SynTy _ ty2) k subst = uTysX ty1 ty2 k subst
390 -- Variables; go for uVar
391 uTysX (TyVarTy tyvar1) (TyVarTy tyvar2) k subst
394 uTysX (TyVarTy tyvar1) ty2 k subst
396 = uVarX tyvar1 ty2 k subst
397 uTysX ty1 (TyVarTy tyvar2) k subst
399 = uVarX tyvar2 ty1 k subst
401 -- Functions; just check the two parts
402 uTysX (FunTy fun1 arg1) (FunTy fun2 arg2) k subst
403 = uTysX fun1 fun2 (uTysX arg1 arg2 k) subst
405 -- Type constructors must match
406 uTysX (TyConApp con1 tys1) (TyConApp con2 tys2) k subst
407 | (con1 == con2 && length tys1 == length tys2)
408 = uTyListsX tys1 tys2 k subst
410 -- Applications need a bit of care!
411 -- They can match FunTy and TyConApp
412 uTysX (AppTy s1 t1) (AppTy s2 t2) k subst
413 = uTysX s1 s2 (uTysX t1 t2 k) subst
415 uTysX (AppTy s1 t1) (FunTy fun2 arg2) k subst
416 = uTysX s1 s2 (uTysX t1 t2 k) subst
418 -- Converts a -> b to (->) a b
419 s2 = TyConApp mkFunTyCon [fun2]
422 uTysX (AppTy s1 t1) (TyConApp tc tys@(_:_)) k subst
423 = case snocView tys of
424 (ts2, t2) -> uTysX s1 s2 (uTysX t1 t2 k) subst
426 -- Not efficient, but simple
429 uTysX s1 s2@(AppTy _ _) k subst = uTysX s2 s1 k subst
430 -- Swap arguments if the App is in the second argument
432 -- Not expecting for-alls in unification
434 uTysX (ForAllTy _ _) ty2 k subst = panic "Unify.uTysX subst:ForAllTy (1st arg)"
435 uTysX ty1 (ForAllTy _ _) k subst = panic "Unify.uTysX subst:ForAllTy (2nd arg)"
438 -- Anything else fails
439 uTysX ty1 ty2 k subst = Nothing
442 uTyListsX [] [] k subst = k subst
443 uTyListsX (ty1:tys1) (ty2:tys2) k subst = uTysX ty1 ty2 (uTyListsX tys1 tys2 k) subst
444 uTyListsX tys1 tys2 k subst = Nothing -- Fail if the lists are different lengths
448 -- Invariant: tv1 is a unifiable variable
449 uVarX tv1 ty2 k subst
450 = case lookupTyVarEnv subst tv1 of
451 Just ty1 -> -- Already bound
452 uTysX ty1 ty2 k subst
454 Nothing -- Not already bound
455 | typeKind ty2 `hasMoreBoxityInfo` tyVarKind tv1
456 && occur_check_ok ty2
457 -> -- No kind mismatch nor occur check
458 k (addToTyVarEnv subst tv1 ty2)
460 | otherwise -> Nothing -- Fail if kind mis-match or occur check
462 occur_check_ok ty = all occur_check_ok_tv (tyVarSetToList (tyVarsOfType ty))
463 occur_check_ok_tv tv | tv1 == tv = False
464 | otherwise = case lookupTyVarEnv subst tv of
466 Just ty -> occur_check_ok ty
470 %************************************************************************
472 \subsection[Unify-context]{Errors and contexts}
474 %************************************************************************
480 unifyCtxt ty1 ty2 -- ty1 expected, ty2 inferred
481 = zonkTcType ty1 `thenNF_Tc` \ ty1' ->
482 zonkTcType ty2 `thenNF_Tc` \ ty2' ->
483 returnNF_Tc (err ty1' ty2')
485 err ty1' ty2' = vcat [
486 hsep [ptext SLIT("Expected:"), ppr ty1'],
487 hsep [ptext SLIT("Inferred:"), ppr ty2']
490 unifyMisMatch ty1 ty2
491 = hang (ptext SLIT("Couldn't match the type"))
492 4 (sep [quotes (ppr ty1), ptext SLIT("against"), quotes (ppr ty2)])
494 unifyKindErr tyvar ty
495 = hang (ptext SLIT("Kind mis-match between"))
496 4 (sep [quotes (hsep [ppr tyvar, ptext SLIT("::"), ppr (tyVarKind tyvar)]),
498 quotes (hsep [ppr ty, ptext SLIT("::"), ppr (typeKind ty)])])
500 unifyOccurCheck tyvar ty
501 = hang (ptext SLIT("Occurs check: cannot construct the infinite type:"))
502 8 (sep [ppr tyvar, char '=', ppr ty])