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, splitAppTys, splitTyConApp_maybe )
21 import TyCon ( TyCon, mkFunTyCon, isTupleTyCon, tyConArity, Arity )
22 import TyVar ( GenTyVar(..), TyVar, tyVarKind, tyVarSetToList,
23 TyVarEnv, lookupTyVarEnv, emptyTyVarEnv, addToTyVarEnv
25 import TcType ( TcType, TcMaybe(..), TcTauType, TcTyVar,
26 newTyVarTy, tcReadTyVar, tcWriteTyVar, zonkTcType
29 import Kind ( Kind, hasMoreBoxityInfo, mkTypeKind, mkBoxedTypeKind )
30 import TysWiredIn ( listTyCon, mkListTy, mkTupleTy )
31 import Maybes ( maybeToBool )
32 import PprType () -- Instances
38 %************************************************************************
40 \subsection[Unify-exported]{Exported unification functions}
42 %************************************************************************
44 The exported functions are all defined as versions of some
45 non-exported generic functions.
47 Unify two @TauType@s. Dead straightforward.
50 unifyTauTy :: TcTauType s -> TcTauType s -> TcM s ()
51 unifyTauTy ty1 ty2 -- ty1 expected, ty2 inferred
52 = tcAddErrCtxtM (unifyCtxt ty1 ty2) $
56 @unifyTauTyList@ unifies corresponding elements of two lists of
57 @TauType@s. It uses @uTys@ to do the real work. The lists should be
58 of equal length. We charge down the list explicitly so that we can
59 complain if their lengths differ.
62 unifyTauTyLists :: [TcTauType s] -> [TcTauType s] -> TcM s ()
63 unifyTauTyLists [] [] = returnTc ()
64 unifyTauTyLists (ty1:tys1) (ty2:tys2) = uTys ty1 ty1 ty2 ty2 `thenTc_`
65 unifyTauTyLists tys1 tys2
66 unifyTauTyLists ty1s ty2s = panic "Unify.unifyTauTyLists: mismatched type lists!"
69 @unifyTauTyList@ takes a single list of @TauType@s and unifies them
70 all together. It is used, for example, when typechecking explicit
71 lists, when all the elts should be of the same type.
74 unifyTauTyList :: [TcTauType s] -> TcM s ()
75 unifyTauTyList [] = returnTc ()
76 unifyTauTyList [ty] = returnTc ()
77 unifyTauTyList (ty1:tys@(ty2:_)) = unifyTauTy ty1 ty2 `thenTc_`
81 %************************************************************************
83 \subsection[Unify-uTys]{@uTys@: getting down to business}
85 %************************************************************************
87 @uTys@ is the heart of the unifier. Each arg happens twice, because
88 we want to report errors in terms of synomyms if poss. The first of
89 the pair is used in error messages only; it is always the same as the
90 second, except that if the first is a synonym then the second may be a
91 de-synonym'd version. This way we get better error messages.
93 We call the first one \tr{ps_ty1}, \tr{ps_ty2} for ``possible synomym''.
96 uTys :: TcTauType s -> TcTauType s -- Error reporting ty1 and real ty1
97 -> TcTauType s -> TcTauType s -- Error reporting ty2 and real ty2
100 -- Always expand synonyms (see notes at end)
101 uTys ps_ty1 (SynTy _ ty1) ps_ty2 ty2 = uTys ps_ty1 ty1 ps_ty2 ty2
102 uTys ps_ty1 ty1 ps_ty2 (SynTy _ ty2) = uTys ps_ty1 ty1 ps_ty2 ty2
104 -- Variables; go for uVar
105 uTys ps_ty1 (TyVarTy tyvar1) ps_ty2 ty2 = uVar tyvar1 ps_ty2 ty2
106 uTys ps_ty1 ty1 ps_ty2 (TyVarTy tyvar2) = uVar tyvar2 ps_ty1 ty1
108 -- Functions; just check the two parts
109 uTys _ (FunTy fun1 arg1) _ (FunTy fun2 arg2)
110 = uTys fun1 fun1 fun2 fun2 `thenTc_` uTys arg1 arg1 arg2 arg2
112 -- Type constructors must match
113 uTys ps_ty1 (TyConApp con1 tys1) ps_ty2 (TyConApp con2 tys2)
114 = checkTc (con1 == con2 && length tys1 == length tys2)
115 (unifyMisMatch ps_ty1 ps_ty2) `thenTc_`
116 unifyTauTyLists tys1 tys2
118 -- Applications need a bit of care!
119 -- They can match FunTy and TyConApp
120 uTys _ (AppTy s1 t1) _ (AppTy s2 t2)
121 = uTys s1 s1 s2 s2 `thenTc_` uTys t1 t1 t2 t2
123 uTys _ (AppTy s1 t1) _ (FunTy fun2 arg2)
124 = uTys s1 s1 s2 s2 `thenTc_` uTys t1 t1 t2 t2
126 -- Converts a -> b to (->) a b
127 s2 = TyConApp mkFunTyCon [fun2]
130 uTys _ (AppTy s1 t1) _ (TyConApp tc tys@(_:_))
131 = case snocView tys of
132 (ts2, t2) -> uTys s1 s1 s2 s2 `thenTc_` uTys t1 t1 t2 t2
134 -- Not efficient, but simple
137 uTys ps1 s1 ps2 s2@(AppTy _ _) = uTys ps2 s2 ps1 s1
138 -- Swap arguments if the App is in the second argument
140 -- Not expecting for-alls in unification
142 uTys ps_ty1 (ForAllTy _ _) ps_ty2 ty2 = panic "Unify.uTys:ForAllTy (1st arg)"
143 uTys ps_ty1 ty1 ps_ty2 (ForAllTy _ _) = panic "Unify.uTys:ForAllTy (2nd arg)"
146 -- Anything else fails
147 uTys ps_ty1 ty1 ps_ty2 ty2 = failWithTc (unifyMisMatch ps_ty1 ps_ty2)
152 If you are tempted to make a short cut on synonyms, as in this
156 uTys (SynTy con1 args1 ty1) (SynTy con2 args2 ty2)
157 = if (con1 == con2) then
158 -- Good news! Same synonym constructors, so we can shortcut
159 -- by unifying their arguments and ignoring their expansions.
160 unifyTauTypeLists args1 args2
162 -- Never mind. Just expand them and try again
166 then THINK AGAIN. Here is the whole story, as detected and reported
167 by Chris Okasaki \tr{<Chris_Okasaki@loch.mess.cs.cmu.edu>}:
169 Here's a test program that should detect the problem:
173 x = (1 :: Bogus Char) :: Bogus Bool
176 The problem with [the attempted shortcut code] is that
180 is not a sufficient condition to be able to use the shortcut!
181 You also need to know that the type synonym actually USES all
182 its arguments. For example, consider the following type synonym
183 which does not use all its arguments.
188 If you ever tried unifying, say, \tr{Bogus Char} with \tr{Bogus Bool},
189 the unifier would blithely try to unify \tr{Char} with \tr{Bool} and
190 would fail, even though the expanded forms (both \tr{Int}) should
193 Similarly, unifying \tr{Bogus Char} with \tr{Bogus t} would
194 unnecessarily bind \tr{t} to \tr{Char}.
196 ... You could explicitly test for the problem synonyms and mark them
197 somehow as needing expansion, perhaps also issuing a warning to the
202 %************************************************************************
204 \subsection[Unify-uVar]{@uVar@: unifying with a type variable}
206 %************************************************************************
208 @uVar@ is called when at least one of the types being unified is a
209 variable. It does {\em not} assume that the variable is a fixed point
210 of the substitution; rather, notice that @bindTo@ (defined below) nips
211 back into @uTys@ if it turns out that the variable is already bound.
213 There is a slight worry that one might try to @bindTo@ a (say) Poly
214 tyvar (as tv1) with an Open tyvar (as ty2) which is already unified to
215 an unboxed type. In fact this can't happen, because the Open ones are
216 always the ones which are unified away.
220 -> TcTauType s -> TcTauType s -- printing and real versions
224 = tcReadTyVar tv1 `thenNF_Tc` \ maybe_ty1 ->
226 BoundTo ty1 -> uTys ty1 ty1 ps_ty2 ty2
227 other -> uUnboundVar tv1 maybe_ty1 ps_ty2 ty2
230 uUnboundVar tv1 maybe_ty1 ps_ty2 (SynTy _ ty2)
231 = uUnboundVar tv1 maybe_ty1 ps_ty2 ty2
234 -- The both-type-variable case
235 uUnboundVar tv1@(TyVar uniq1 kind1 name1 box1)
238 ty2@(TyVarTy tv2@(TyVar uniq2 kind2 name2 box2))
240 -- Same type variable => no-op
244 -- Distinct type variables
245 -- ASSERT maybe_ty1 /= BoundTo
247 = tcReadTyVar tv2 `thenNF_Tc` \ maybe_ty2 ->
249 BoundTo ty2' -> uUnboundVar tv1 maybe_ty1 ty2' ty2'
251 UnBound | (kind1 == kind2 && not (maybeToBool name1)) -- Same kinds and tv1 is anonymous
253 -> tcWriteTyVar tv1 ps_ty2 `thenNF_Tc_` returnTc ()
255 | kind1 `hasMoreBoxityInfo` kind2 -- Update tv2 if possible
256 -> tcWriteTyVar tv2 (TyVarTy tv1) `thenNF_Tc_` returnTc ()
258 | kind2 `hasMoreBoxityInfo` kind1 -- Update tv1 if possible
259 -> tcWriteTyVar tv1 ps_ty2 `thenNF_Tc_` returnTc ()
261 other -> failWithTc (unifyKindErr tv1 ps_ty2)
263 -- Second one isn't a type variable
264 uUnboundVar tv1@(TyVar uniq1 kind1 name1 box1) maybe_ty1 ps_ty2 non_var_ty2
265 | typeKind non_var_ty2 `hasMoreBoxityInfo` kind1
266 = occur_check non_var_ty2 `thenTc_`
267 tcWriteTyVar tv1 ps_ty2 `thenNF_Tc_`
271 = failWithTc (unifyKindErr tv1 ps_ty2)
274 occur_check ty = mapTc occur_check_tv (tyVarSetToList (tyVarsOfType ty)) `thenTc_`
277 occur_check_tv tv2@(TyVar uniq2 _ _ box2)
278 | uniq1 == uniq2 -- Same tyvar; fail
279 = failWithTc (unifyOccurCheck tv1 ps_ty2)
281 | otherwise -- A different tyvar
282 = tcReadTyVar tv2 `thenNF_Tc` \ maybe_ty2 ->
284 BoundTo ty2' -> occur_check ty2'
288 %************************************************************************
290 \subsection[Unify-fun]{@unifyFunTy@}
292 %************************************************************************
294 @unifyFunTy@ is used to avoid the fruitless creation of type variables.
297 unifyFunTy :: TcType s -- Fail if ty isn't a function type
298 -> TcM s (TcType s, TcType s) -- otherwise return arg and result types
300 unifyFunTy ty@(TyVarTy tyvar)
301 = tcReadTyVar tyvar `thenNF_Tc` \ maybe_ty ->
303 BoundTo ty' -> unifyFunTy ty'
304 other -> unify_fun_ty_help ty
307 = case splitFunTy_maybe ty of
308 Just arg_and_res -> returnTc arg_and_res
309 Nothing -> unify_fun_ty_help ty
311 unify_fun_ty_help ty -- Special cases failed, so revert to ordinary unification
312 = newTyVarTy mkTypeKind `thenNF_Tc` \ arg ->
313 newTyVarTy mkTypeKind `thenNF_Tc` \ res ->
314 unifyTauTy (mkFunTy arg res) ty `thenTc_`
319 unifyListTy :: TcType s -- expected list type
320 -> TcM s (TcType s) -- list element type
322 unifyListTy ty@(TyVarTy tyvar)
323 = tcReadTyVar tyvar `thenNF_Tc` \ maybe_ty ->
325 BoundTo ty' -> unifyListTy ty'
326 other -> unify_list_ty_help ty
329 = case splitTyConApp_maybe ty of
330 Just (tycon, [arg_ty]) | tycon == listTyCon -> returnTc arg_ty
331 other -> unify_list_ty_help ty
333 unify_list_ty_help ty -- Revert to ordinary unification
334 = newTyVarTy mkBoxedTypeKind `thenNF_Tc` \ elt_ty ->
335 unifyTauTy (mkListTy elt_ty) ty `thenTc_`
340 unifyTupleTy :: Arity -> TcType s -> TcM s [TcType s]
341 unifyTupleTy arity ty@(TyVarTy tyvar)
342 = tcReadTyVar tyvar `thenNF_Tc` \ maybe_ty ->
344 BoundTo ty' -> unifyTupleTy arity ty'
345 other -> unify_tuple_ty_help arity ty
347 unifyTupleTy arity ty
348 = case splitTyConApp_maybe ty of
349 Just (tycon, arg_tys) | isTupleTyCon tycon
350 && tyConArity tycon == arity
352 other -> unify_tuple_ty_help arity ty
354 unify_tuple_ty_help arity ty
355 = mapNF_Tc (\ _ -> newTyVarTy mkBoxedTypeKind) [1..arity] `thenNF_Tc` \ arg_tys ->
356 unifyTauTy (mkTupleTy arity arg_tys) ty `thenTc_`
360 %************************************************************************
362 \subsection{Unification wih a explicit substitution}
364 %************************************************************************
366 Unify types with an explicit substitution and no monad.
369 type Subst = TyVarEnv Type -- Not necessarily idempotent
371 unifyTysX :: Type -> Type -> Maybe Subst
372 unifyTysX ty1 ty2 = uTysX ty1 ty2 (\s -> Just s) emptyTyVarEnv
374 unifyTyListsX :: [Type] -> [Type] -> Maybe Subst
375 unifyTyListsX tys1 tys2 = uTyListsX tys1 tys2 (\s -> Just s) emptyTyVarEnv
378 uTysX :: Type -> Type
379 -> (Subst -> Maybe Subst)
383 uTysX ty1 (SynTy _ ty2) k subst = uTysX ty1 ty2 k subst
385 -- Variables; go for uVar
386 uTysX (TyVarTy tyvar1) ty2 k subst = uVarX tyvar1 ty2 k subst
387 uTysX ty1 (TyVarTy tyvar2) k subst = uVarX tyvar2 ty1 k subst
389 -- Functions; just check the two parts
390 uTysX (FunTy fun1 arg1) (FunTy fun2 arg2) k subst
391 = uTysX fun1 fun2 (uTysX arg1 arg2 k) subst
393 -- Type constructors must match
394 uTysX (TyConApp con1 tys1) (TyConApp con2 tys2) k subst
395 | (con1 == con2 && length tys1 == length tys2)
396 = uTyListsX tys1 tys2 k subst
398 -- Applications need a bit of care!
399 -- They can match FunTy and TyConApp
400 uTysX (AppTy s1 t1) (AppTy s2 t2) k subst
401 = uTysX s1 s2 (uTysX t1 t2 k) subst
403 uTysX (AppTy s1 t1) (FunTy fun2 arg2) k subst
404 = uTysX s1 s2 (uTysX t1 t2 k) subst
406 -- Converts a -> b to (->) a b
407 s2 = TyConApp mkFunTyCon [fun2]
410 uTysX (AppTy s1 t1) (TyConApp tc tys@(_:_)) k subst
411 = case snocView tys of
412 (ts2, t2) -> uTysX s1 s2 (uTysX t1 t2 k) subst
414 -- Not efficient, but simple
417 uTysX s1 s2@(AppTy _ _) k subst = uTysX s2 s1 k subst
418 -- Swap arguments if the App is in the second argument
420 -- Not expecting for-alls in unification
422 uTysX (ForAllTy _ _) ty2 k subst = panic "Unify.uTysX subst:ForAllTy (1st arg)"
423 uTysX ty1 (ForAllTy _ _) k subst = panic "Unify.uTysX subst:ForAllTy (2nd arg)"
426 -- Anything else fails
427 uTysX ty1 ty2 k subst = Nothing
430 uTyListsX [] [] k subst = k subst
431 uTyListsX (ty1:tys1) (ty2:tys2) k subst = uTysX ty1 ty2 (uTyListsX tys1 tys2 k) subst
432 uTyListsX tys1 tys2 k subst = Nothing -- Fail if the lists are different lengths
436 uVarX tv1 (TyVarTy tv2) k subst | tv1 == tv2 = k subst
437 -- Binding a variable to itself is a no-op
439 uVarX tv1 ty2 k subst
440 = case lookupTyVarEnv subst tv1 of
441 Just ty1 -> -- Already bound
442 uTysX ty1 ty2 k subst
444 Nothing -- Not already bound
445 | typeKind ty2 `hasMoreBoxityInfo` tyVarKind tv1
446 && occur_check_ok ty2
447 -> -- No kind mismatch nor occur check
448 k (addToTyVarEnv subst tv1 ty2)
450 | otherwise -> Nothing -- Fail if kind mis-match or occur check
452 occur_check_ok ty = all occur_check_ok_tv (tyVarSetToList (tyVarsOfType ty))
453 occur_check_ok_tv tv | tv1 == tv = False
454 | otherwise = case lookupTyVarEnv subst tv of
456 Just ty -> occur_check_ok ty
460 %************************************************************************
462 \subsection[Unify-context]{Errors and contexts}
464 %************************************************************************
470 unifyCtxt ty1 ty2 -- ty1 expected, ty2 inferred
471 = zonkTcType ty1 `thenNF_Tc` \ ty1' ->
472 zonkTcType ty2 `thenNF_Tc` \ ty2' ->
473 returnNF_Tc (err ty1' ty2')
475 err ty1' ty2' = vcat [
476 hsep [ptext SLIT("Expected:"), ppr ty1'],
477 hsep [ptext SLIT("Inferred:"), ppr ty2']
480 unifyMisMatch ty1 ty2
481 = hang (ptext SLIT("Couldn't match the type"))
482 4 (sep [quotes (ppr ty1), ptext SLIT("against"), quotes (ppr ty2)])
485 = hang (text "Function type expected, but found the type")
488 unifyKindErr tyvar ty
489 = hang (ptext SLIT("Compiler bug: kind mis-match between"))
490 4 (sep [quotes (hsep [ppr tyvar, ptext SLIT("::"), ppr (tyVarKind tyvar)]),
492 quotes (hsep [ppr ty, ptext SLIT("::"), ppr (typeKind ty)])])
494 unifyOccurCheck tyvar ty
495 = hang (ptext SLIT("Occurs check: cannot construct the infinite type:"))
496 8 (sep [ppr tyvar, char '=', ppr ty])