2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 \section[Unify]{Unifier}
6 The unifier is now squarely in the typechecker monad (because of the
7 updatable substitution).
10 module TcUnify ( unifyTauTy, unifyTauTyList, unifyTauTyLists,
11 unifyFunTy, unifyListTy, unifyTupleTy,
12 unifyKind, unifyKinds, unifyOpenTypeKind
15 #include "HsVersions.h"
19 import TypeRep ( Type(..), PredType(..) ) -- friend
20 import Type ( unliftedTypeKind, liftedTypeKind, openTypeKind,
21 typeCon, openKindCon, hasMoreBoxityInfo,
22 tyVarsOfType, typeKind,
23 mkFunTy, splitFunTy_maybe, splitTyConApp_maybe,
24 splitAppTy_maybe, mkTyConApp,
25 tidyOpenType, tidyOpenTypes, tidyTyVar
27 import TyCon ( TyCon, isTupleTyCon, tupleTyConBoxity, tyConArity )
28 import Var ( tyVarKind, varName, isSigTyVar )
29 import VarSet ( elemVarSet )
30 import TcType ( TcType, TcTauType, TcTyVar, TcKind, newBoxityVar,
31 newTyVarTy, newTyVarTys, tcGetTyVar, tcPutTyVar, zonkTcType
33 import Name ( isSystemName )
36 import BasicTypes ( Arity, Boxity, isBoxed )
37 import TysWiredIn ( listTyCon, mkListTy, mkTupleTy )
42 %************************************************************************
44 \subsection{The Kind variants}
46 %************************************************************************
49 unifyKind :: TcKind -- Expected
53 = tcAddErrCtxtM (unifyCtxt "kind" k1 k2) $
56 unifyKinds :: [TcKind] -> [TcKind] -> TcM ()
57 unifyKinds [] [] = returnTc ()
58 unifyKinds (k1:ks1) (k2:ks2) = unifyKind k1 k2 `thenTc_`
60 unifyKinds _ _ = panic "unifyKinds: length mis-match"
64 unifyOpenTypeKind :: TcKind -> TcM ()
65 -- Ensures that the argument kind is of the form (Type bx)
68 unifyOpenTypeKind ty@(TyVarTy tyvar)
69 = tcGetTyVar tyvar `thenNF_Tc` \ maybe_ty ->
71 Just ty' -> unifyOpenTypeKind ty'
72 other -> unify_open_kind_help ty
75 = case splitTyConApp_maybe ty of
76 Just (tycon, [_]) | tycon == typeCon -> returnTc ()
77 other -> unify_open_kind_help ty
79 unify_open_kind_help ty -- Revert to ordinary unification
80 = newBoxityVar `thenNF_Tc` \ boxity ->
81 unifyKind ty (mkTyConApp typeCon [boxity])
85 %************************************************************************
87 \subsection[Unify-exported]{Exported unification functions}
89 %************************************************************************
91 The exported functions are all defined as versions of some
92 non-exported generic functions.
94 Unify two @TauType@s. Dead straightforward.
97 unifyTauTy :: TcTauType -> TcTauType -> TcM ()
98 unifyTauTy ty1 ty2 -- ty1 expected, ty2 inferred
99 = tcAddErrCtxtM (unifyCtxt "type" ty1 ty2) $
103 @unifyTauTyList@ unifies corresponding elements of two lists of
104 @TauType@s. It uses @uTys@ to do the real work. The lists should be
105 of equal length. We charge down the list explicitly so that we can
106 complain if their lengths differ.
109 unifyTauTyLists :: [TcTauType] -> [TcTauType] -> TcM ()
110 unifyTauTyLists [] [] = returnTc ()
111 unifyTauTyLists (ty1:tys1) (ty2:tys2) = uTys ty1 ty1 ty2 ty2 `thenTc_`
112 unifyTauTyLists tys1 tys2
113 unifyTauTyLists ty1s ty2s = panic "Unify.unifyTauTyLists: mismatched type lists!"
116 @unifyTauTyList@ takes a single list of @TauType@s and unifies them
117 all together. It is used, for example, when typechecking explicit
118 lists, when all the elts should be of the same type.
121 unifyTauTyList :: [TcTauType] -> TcM ()
122 unifyTauTyList [] = returnTc ()
123 unifyTauTyList [ty] = returnTc ()
124 unifyTauTyList (ty1:tys@(ty2:_)) = unifyTauTy ty1 ty2 `thenTc_`
128 %************************************************************************
130 \subsection[Unify-uTys]{@uTys@: getting down to business}
132 %************************************************************************
134 @uTys@ is the heart of the unifier. Each arg happens twice, because
135 we want to report errors in terms of synomyms if poss. The first of
136 the pair is used in error messages only; it is always the same as the
137 second, except that if the first is a synonym then the second may be a
138 de-synonym'd version. This way we get better error messages.
140 We call the first one \tr{ps_ty1}, \tr{ps_ty2} for ``possible synomym''.
143 uTys :: TcTauType -> TcTauType -- Error reporting ty1 and real ty1
144 -- ty1 is the *expected* type
146 -> TcTauType -> TcTauType -- Error reporting ty2 and real ty2
147 -- ty2 is the *actual* type
150 -- Always expand synonyms (see notes at end)
151 -- (this also throws away FTVs)
152 uTys ps_ty1 (NoteTy _ ty1) ps_ty2 ty2 = uTys ps_ty1 ty1 ps_ty2 ty2
153 uTys ps_ty1 ty1 ps_ty2 (NoteTy _ ty2) = uTys ps_ty1 ty1 ps_ty2 ty2
155 -- Ignore usage annotations inside typechecker
156 uTys ps_ty1 (UsageTy _ ty1) ps_ty2 ty2 = uTys ps_ty1 ty1 ps_ty2 ty2
157 uTys ps_ty1 ty1 ps_ty2 (UsageTy _ ty2) = uTys ps_ty1 ty1 ps_ty2 ty2
159 -- Variables; go for uVar
160 uTys ps_ty1 (TyVarTy tyvar1) ps_ty2 ty2 = uVar False tyvar1 ps_ty2 ty2
161 uTys ps_ty1 ty1 ps_ty2 (TyVarTy tyvar2) = uVar True tyvar2 ps_ty1 ty1
162 -- "True" means args swapped
165 uTys _ (PredTy (IParam n1 t1)) _ (PredTy (IParam n2 t2))
166 | n1 == n2 = uTys t1 t1 t2 t2
167 uTys _ (PredTy (ClassP c1 tys1)) _ (PredTy (ClassP c2 tys2))
168 | c1 == c2 = unifyTauTyLists tys1 tys2
170 -- Functions; just check the two parts
171 uTys _ (FunTy fun1 arg1) _ (FunTy fun2 arg2)
172 = uTys fun1 fun1 fun2 fun2 `thenTc_` uTys arg1 arg1 arg2 arg2
174 -- Type constructors must match
175 uTys ps_ty1 (TyConApp con1 tys1) ps_ty2 (TyConApp con2 tys2)
176 | con1 == con2 && length tys1 == length tys2
177 = unifyTauTyLists tys1 tys2
179 | con1 == openKindCon
180 -- When we are doing kind checking, we might match a kind '?'
181 -- against a kind '*' or '#'. Notably, CCallable :: ? -> *, and
182 -- (CCallable Int) and (CCallable Int#) are both OK
183 = unifyOpenTypeKind ps_ty2
185 -- Applications need a bit of care!
186 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
187 -- NB: we've already dealt with type variables and Notes,
188 -- so if one type is an App the other one jolly well better be too
189 uTys ps_ty1 (AppTy s1 t1) ps_ty2 ty2
190 = case splitAppTy_maybe ty2 of
191 Just (s2,t2) -> uTys s1 s1 s2 s2 `thenTc_` uTys t1 t1 t2 t2
192 Nothing -> unifyMisMatch ps_ty1 ps_ty2
194 -- Now the same, but the other way round
195 -- Don't swap the types, because the error messages get worse
196 uTys ps_ty1 ty1 ps_ty2 (AppTy s2 t2)
197 = case splitAppTy_maybe ty1 of
198 Just (s1,t1) -> uTys s1 s1 s2 s2 `thenTc_` uTys t1 t1 t2 t2
199 Nothing -> unifyMisMatch ps_ty1 ps_ty2
201 -- Not expecting for-alls in unification
202 -- ... but the error message from the unifyMisMatch more informative
203 -- than a panic message!
205 -- Anything else fails
206 uTys ps_ty1 ty1 ps_ty2 ty2 = unifyMisMatch ps_ty1 ps_ty2
211 If you are tempted to make a short cut on synonyms, as in this
215 uTys (SynTy con1 args1 ty1) (SynTy con2 args2 ty2)
216 = if (con1 == con2) then
217 -- Good news! Same synonym constructors, so we can shortcut
218 -- by unifying their arguments and ignoring their expansions.
219 unifyTauTypeLists args1 args2
221 -- Never mind. Just expand them and try again
225 then THINK AGAIN. Here is the whole story, as detected and reported
226 by Chris Okasaki \tr{<Chris_Okasaki@loch.mess.cs.cmu.edu>}:
228 Here's a test program that should detect the problem:
232 x = (1 :: Bogus Char) :: Bogus Bool
235 The problem with [the attempted shortcut code] is that
239 is not a sufficient condition to be able to use the shortcut!
240 You also need to know that the type synonym actually USES all
241 its arguments. For example, consider the following type synonym
242 which does not use all its arguments.
247 If you ever tried unifying, say, \tr{Bogus Char} with \tr{Bogus Bool},
248 the unifier would blithely try to unify \tr{Char} with \tr{Bool} and
249 would fail, even though the expanded forms (both \tr{Int}) should
252 Similarly, unifying \tr{Bogus Char} with \tr{Bogus t} would
253 unnecessarily bind \tr{t} to \tr{Char}.
255 ... You could explicitly test for the problem synonyms and mark them
256 somehow as needing expansion, perhaps also issuing a warning to the
261 %************************************************************************
263 \subsection[Unify-uVar]{@uVar@: unifying with a type variable}
265 %************************************************************************
267 @uVar@ is called when at least one of the types being unified is a
268 variable. It does {\em not} assume that the variable is a fixed point
269 of the substitution; rather, notice that @uVar@ (defined below) nips
270 back into @uTys@ if it turns out that the variable is already bound.
273 uVar :: Bool -- False => tyvar is the "expected"
274 -- True => ty is the "expected" thing
276 -> TcTauType -> TcTauType -- printing and real versions
279 uVar swapped tv1 ps_ty2 ty2
280 = tcGetTyVar tv1 `thenNF_Tc` \ maybe_ty1 ->
282 Just ty1 | swapped -> uTys ps_ty2 ty2 ty1 ty1 -- Swap back
283 | otherwise -> uTys ty1 ty1 ps_ty2 ty2 -- Same order
284 other -> uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
286 -- Expand synonyms; ignore FTVs
287 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 (NoteTy _ ty2)
288 = uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
291 -- The both-type-variable case
292 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2@(TyVarTy tv2)
294 -- Same type variable => no-op
298 -- Distinct type variables
299 -- ASSERT maybe_ty1 /= Just
301 = tcGetTyVar tv2 `thenNF_Tc` \ maybe_ty2 ->
303 Just ty2' -> uUnboundVar swapped tv1 maybe_ty1 ty2' ty2'
307 -> WARN( not (k1 `hasMoreBoxityInfo` k2), (ppr tv1 <+> ppr k1) $$ (ppr tv2 <+> ppr k2) )
308 tcPutTyVar tv2 (TyVarTy tv1) `thenNF_Tc_`
312 -> WARN( not (k2 `hasMoreBoxityInfo` k1), (ppr tv2 <+> ppr k2) $$ (ppr tv1 <+> ppr k1) )
313 (tcPutTyVar tv1 ps_ty2 `thenNF_Tc_`
318 update_tv2 = (k2 == openTypeKind) || (k1 /= openTypeKind && nicer_to_update_tv2)
319 -- Try to get rid of open type variables as soon as poss
321 nicer_to_update_tv2 = isSigTyVar tv1
322 -- Don't unify a signature type variable if poss
323 || isSystemName (varName tv2)
324 -- Try to update sys-y type variables in preference to sig-y ones
326 -- Second one isn't a type variable
327 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 non_var_ty2
328 = -- Check that the kinds match
329 checkKinds swapped tv1 non_var_ty2 `thenTc_`
331 -- Check that tv1 isn't a type-signature type variable
332 checkTcM (not (isSigTyVar tv1))
333 (failWithTcM (unifyWithSigErr tv1 ps_ty2)) `thenTc_`
335 -- Check that we aren't losing boxity info (shouldn't happen)
336 warnTc (not (typeKind non_var_ty2 `hasMoreBoxityInfo` tyVarKind tv1))
337 ((ppr tv1 <+> ppr (tyVarKind tv1)) $$
338 (ppr non_var_ty2 <+> ppr (typeKind non_var_ty2))) `thenNF_Tc_`
341 -- Basically we want to update tv1 := ps_ty2
342 -- because ps_ty2 has type-synonym info, which improves later error messages
347 -- f :: (A a -> a -> ()) -> ()
351 -- x = f (\ x p -> p x)
353 -- In the application (p x), we try to match "t" with "A t". If we go
354 -- ahead and bind t to A t (= ps_ty2), we'll lead the type checker into
355 -- an infinite loop later.
356 -- But we should not reject the program, because A t = ().
357 -- Rather, we should bind t to () (= non_var_ty2).
359 -- That's why we have this two-state occurs-check
360 zonkTcType ps_ty2 `thenNF_Tc` \ ps_ty2' ->
361 if not (tv1 `elemVarSet` tyVarsOfType ps_ty2') then
362 tcPutTyVar tv1 ps_ty2' `thenNF_Tc_`
365 zonkTcType non_var_ty2 `thenNF_Tc` \ non_var_ty2' ->
366 if not (tv1 `elemVarSet` tyVarsOfType non_var_ty2') then
367 -- This branch rarely succeeds, except in strange cases
368 -- like that in the example above
369 tcPutTyVar tv1 non_var_ty2' `thenNF_Tc_`
372 failWithTcM (unifyOccurCheck tv1 ps_ty2')
375 checkKinds swapped tv1 ty2
376 -- We're about to unify a type variable tv1 with a non-tyvar-type ty2.
377 -- We need to check that we don't unify a lifted type variable with an
378 -- unlifted type: e.g. (id 3#) is illegal
379 | tk1 == liftedTypeKind && tk2 == unliftedTypeKind
380 = tcAddErrCtxtM (unifyKindCtxt swapped tv1 ty2) $
385 (k1,k2) | swapped = (tk2,tk1)
386 | otherwise = (tk1,tk2)
392 %************************************************************************
394 \subsection[Unify-fun]{@unifyFunTy@}
396 %************************************************************************
398 @unifyFunTy@ is used to avoid the fruitless creation of type variables.
401 unifyFunTy :: TcType -- Fail if ty isn't a function type
402 -> TcM (TcType, TcType) -- otherwise return arg and result types
404 unifyFunTy ty@(TyVarTy tyvar)
405 = tcGetTyVar tyvar `thenNF_Tc` \ maybe_ty ->
407 Just ty' -> unifyFunTy ty'
408 other -> unify_fun_ty_help ty
411 = case splitFunTy_maybe ty of
412 Just arg_and_res -> returnTc arg_and_res
413 Nothing -> unify_fun_ty_help ty
415 unify_fun_ty_help ty -- Special cases failed, so revert to ordinary unification
416 = newTyVarTy openTypeKind `thenNF_Tc` \ arg ->
417 newTyVarTy openTypeKind `thenNF_Tc` \ res ->
418 unifyTauTy ty (mkFunTy arg res) `thenTc_`
423 unifyListTy :: TcType -- expected list type
424 -> TcM TcType -- list element type
426 unifyListTy ty@(TyVarTy tyvar)
427 = tcGetTyVar tyvar `thenNF_Tc` \ maybe_ty ->
429 Just ty' -> unifyListTy ty'
430 other -> unify_list_ty_help ty
433 = case splitTyConApp_maybe ty of
434 Just (tycon, [arg_ty]) | tycon == listTyCon -> returnTc arg_ty
435 other -> unify_list_ty_help ty
437 unify_list_ty_help ty -- Revert to ordinary unification
438 = newTyVarTy liftedTypeKind `thenNF_Tc` \ elt_ty ->
439 unifyTauTy ty (mkListTy elt_ty) `thenTc_`
444 unifyTupleTy :: Boxity -> Arity -> TcType -> TcM [TcType]
445 unifyTupleTy boxity arity ty@(TyVarTy tyvar)
446 = tcGetTyVar tyvar `thenNF_Tc` \ maybe_ty ->
448 Just ty' -> unifyTupleTy boxity arity ty'
449 other -> unify_tuple_ty_help boxity arity ty
451 unifyTupleTy boxity arity ty
452 = case splitTyConApp_maybe ty of
453 Just (tycon, arg_tys)
455 && tyConArity tycon == arity
456 && tupleTyConBoxity tycon == boxity
458 other -> unify_tuple_ty_help boxity arity ty
460 unify_tuple_ty_help boxity arity ty
461 = newTyVarTys arity kind `thenNF_Tc` \ arg_tys ->
462 unifyTauTy ty (mkTupleTy boxity arity arg_tys) `thenTc_`
465 kind | isBoxed boxity = liftedTypeKind
466 | otherwise = openTypeKind
470 %************************************************************************
472 \subsection[Unify-context]{Errors and contexts}
474 %************************************************************************
480 unifyCtxt s ty1 ty2 tidy_env -- ty1 expected, ty2 inferred
481 = zonkTcType ty1 `thenNF_Tc` \ ty1' ->
482 zonkTcType ty2 `thenNF_Tc` \ ty2' ->
483 returnNF_Tc (err ty1' ty2')
488 text "Expected" <+> text s <> colon <+> ppr tidy_ty1,
489 text "Inferred" <+> text s <> colon <+> ppr tidy_ty2
492 (env1, [tidy_ty1,tidy_ty2]) = tidyOpenTypes tidy_env [ty1,ty2]
494 unifyKindCtxt swapped tv1 ty2 tidy_env -- not swapped => tv1 expected, ty2 inferred
495 -- tv1 is zonked already
496 = zonkTcType ty2 `thenNF_Tc` \ ty2' ->
497 returnNF_Tc (err ty2')
499 err ty2 = (env2, ptext SLIT("When matching types") <+>
500 sep [quotes pp_expected, ptext SLIT("and"), quotes pp_actual])
502 (pp_expected, pp_actual) | swapped = (pp2, pp1)
503 | otherwise = (pp1, pp2)
504 (env1, tv1') = tidyTyVar tidy_env tv1
505 (env2, ty2') = tidyOpenType env1 ty2
509 unifyMisMatch ty1 ty2
510 = zonkTcType ty1 `thenNF_Tc` \ ty1' ->
511 zonkTcType ty2 `thenNF_Tc` \ ty2' ->
513 (env, [tidy_ty1, tidy_ty2]) = tidyOpenTypes emptyTidyEnv [ty1',ty2']
514 msg = hang (ptext SLIT("Couldn't match"))
515 4 (sep [quotes (ppr tidy_ty1),
516 ptext SLIT("against"),
517 quotes (ppr tidy_ty2)])
519 failWithTcM (env, msg)
521 unifyWithSigErr tyvar ty
522 = (env2, hang (ptext SLIT("Cannot unify the type-signature variable") <+> quotes (ppr tidy_tyvar))
523 4 (ptext SLIT("with the type") <+> quotes (ppr tidy_ty)))
525 (env1, tidy_tyvar) = tidyTyVar emptyTidyEnv tyvar
526 (env2, tidy_ty) = tidyOpenType env1 ty
528 unifyOccurCheck tyvar ty
529 = (env2, hang (ptext SLIT("Occurs check: cannot construct the infinite type:"))
530 4 (sep [ppr tidy_tyvar, char '=', ppr tidy_ty]))
532 (env1, tidy_tyvar) = tidyTyVar emptyTidyEnv tyvar
533 (env2, tidy_ty) = tidyOpenType env1 ty