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, unifyUnboxedTupleTy,
12 unifyKind, unifyKinds, unifyTypeKind
15 #include "HsVersions.h"
19 import Type ( Type(..), tyVarsOfType, funTyCon,
20 mkFunTy, splitFunTy_maybe, splitTyConApp_maybe,
21 Kind, boxedTypeKind, typeCon, anyBoxCon, anyBoxKind,
23 tidyOpenType, tidyOpenTypes, tidyTyVar
25 import TyCon ( TyCon, isTupleTyCon, isUnboxedTupleTyCon,
27 import Name ( isSystemName )
28 import Var ( TyVar, tyVarKind, varName )
30 import VarSet ( varSetElems )
31 import TcType ( TcType, TcTauType, TcTyVar, TcKind,
32 newTyVarTy, newOpenTypeKind, newTyVarTy_OpenKind,
33 tcGetTyVar, tcPutTyVar, zonkTcType, tcTypeKind
36 import BasicTypes ( Arity )
37 import TysWiredIn ( listTyCon, mkListTy, mkTupleTy, mkUnboxedTupleTy )
38 import PprType () -- Instances
44 %************************************************************************
46 \subsection{The Kind variants}
48 %************************************************************************
51 unifyKind :: TcKind -- Expected
55 = tcAddErrCtxtM (unifyCtxt "kind" k1 k2) $
58 unifyKinds :: [TcKind] -> [TcKind] -> TcM s ()
59 unifyKinds [] [] = returnTc ()
60 unifyKinds (k1:ks1) (k2:ks2) = unifyKind k1 k2 `thenTc_`
62 unifyKinds _ _ = panic "unifyKinds: length mis-match"
66 %************************************************************************
68 \subsection[Unify-exported]{Exported unification functions}
70 %************************************************************************
72 The exported functions are all defined as versions of some
73 non-exported generic functions.
75 Unify two @TauType@s. Dead straightforward.
78 unifyTauTy :: TcTauType -> TcTauType -> TcM s ()
79 unifyTauTy ty1 ty2 -- ty1 expected, ty2 inferred
80 = tcAddErrCtxtM (unifyCtxt "type" ty1 ty2) $
84 @unifyTauTyList@ unifies corresponding elements of two lists of
85 @TauType@s. It uses @uTys@ to do the real work. The lists should be
86 of equal length. We charge down the list explicitly so that we can
87 complain if their lengths differ.
90 unifyTauTyLists :: [TcTauType] -> [TcTauType] -> TcM s ()
91 unifyTauTyLists [] [] = returnTc ()
92 unifyTauTyLists (ty1:tys1) (ty2:tys2) = uTys ty1 ty1 ty2 ty2 `thenTc_`
93 unifyTauTyLists tys1 tys2
94 unifyTauTyLists ty1s ty2s = panic "Unify.unifyTauTyLists: mismatched type lists!"
97 @unifyTauTyList@ takes a single list of @TauType@s and unifies them
98 all together. It is used, for example, when typechecking explicit
99 lists, when all the elts should be of the same type.
102 unifyTauTyList :: [TcTauType] -> TcM s ()
103 unifyTauTyList [] = returnTc ()
104 unifyTauTyList [ty] = returnTc ()
105 unifyTauTyList (ty1:tys@(ty2:_)) = unifyTauTy ty1 ty2 `thenTc_`
109 %************************************************************************
111 \subsection[Unify-uTys]{@uTys@: getting down to business}
113 %************************************************************************
115 @uTys@ is the heart of the unifier. Each arg happens twice, because
116 we want to report errors in terms of synomyms if poss. The first of
117 the pair is used in error messages only; it is always the same as the
118 second, except that if the first is a synonym then the second may be a
119 de-synonym'd version. This way we get better error messages.
121 We call the first one \tr{ps_ty1}, \tr{ps_ty2} for ``possible synomym''.
124 uTys :: TcTauType -> TcTauType -- Error reporting ty1 and real ty1
125 -> TcTauType -> TcTauType -- Error reporting ty2 and real ty2
128 -- Always expand synonyms (see notes at end)
129 uTys ps_ty1 (NoteTy _ ty1) ps_ty2 ty2 = uTys ps_ty1 ty1 ps_ty2 ty2
130 uTys ps_ty1 ty1 ps_ty2 (NoteTy _ ty2) = uTys ps_ty1 ty1 ps_ty2 ty2
132 -- Variables; go for uVar
133 uTys ps_ty1 (TyVarTy tyvar1) ps_ty2 ty2 = uVar False tyvar1 ps_ty2 ty2
134 uTys ps_ty1 ty1 ps_ty2 (TyVarTy tyvar2) = uVar True tyvar2 ps_ty1 ty1
135 -- "True" means args swapped
137 -- Functions; just check the two parts
138 uTys _ (FunTy fun1 arg1) _ (FunTy fun2 arg2)
139 = uTys fun1 fun1 fun2 fun2 `thenTc_` uTys arg1 arg1 arg2 arg2
141 -- Type constructors must match
142 uTys ps_ty1 (TyConApp con1 tys1) ps_ty2 (TyConApp con2 tys2)
143 = checkTcM (cons_match && length tys1 == length tys2)
144 (unifyMisMatch ps_ty1 ps_ty2) `thenTc_`
145 unifyTauTyLists tys1 tys2
147 -- The AnyBox wild card matches anything
148 cons_match = con1 == con2
152 -- Applications need a bit of care!
153 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
154 -- NB: we've already dealt with type variables and Notes,
155 -- so if one type is an App the other one jolly well better be too
156 uTys ps_ty1 (AppTy s1 t1) ps_ty2 ty2
157 = case splitAppTy_maybe ty2 of
158 Just (s2,t2) -> uTys s1 s1 s2 s2 `thenTc_` uTys t1 t1 t2 t2
159 Nothing -> unifyMisMatch ps_ty1 ps_ty2
161 -- Now the same, but the other way round
162 -- Don't swap the types, because the error messages get worse
163 uTys ps_ty1 ty1 ps_ty2 (AppTy s2 t2)
164 = case splitAppTy_maybe ty1 of
165 Just (s1,t1) -> uTys s1 s1 s2 s2 `thenTc_` uTys t1 t1 t2 t2
166 Nothing -> unifyMisMatch ps_ty1 ps_ty2
168 -- Not expecting for-alls in unification
169 -- ... but the error message from the unifyMisMatch more informative
170 -- than a panic message!
172 -- Anything else fails
173 uTys ps_ty1 ty1 ps_ty2 ty2 = unifyMisMatch ps_ty1 ps_ty2
178 If you are tempted to make a short cut on synonyms, as in this
182 uTys (SynTy con1 args1 ty1) (SynTy con2 args2 ty2)
183 = if (con1 == con2) then
184 -- Good news! Same synonym constructors, so we can shortcut
185 -- by unifying their arguments and ignoring their expansions.
186 unifyTauTypeLists args1 args2
188 -- Never mind. Just expand them and try again
192 then THINK AGAIN. Here is the whole story, as detected and reported
193 by Chris Okasaki \tr{<Chris_Okasaki@loch.mess.cs.cmu.edu>}:
195 Here's a test program that should detect the problem:
199 x = (1 :: Bogus Char) :: Bogus Bool
202 The problem with [the attempted shortcut code] is that
206 is not a sufficient condition to be able to use the shortcut!
207 You also need to know that the type synonym actually USES all
208 its arguments. For example, consider the following type synonym
209 which does not use all its arguments.
214 If you ever tried unifying, say, \tr{Bogus Char} with \tr{Bogus Bool},
215 the unifier would blithely try to unify \tr{Char} with \tr{Bool} and
216 would fail, even though the expanded forms (both \tr{Int}) should
219 Similarly, unifying \tr{Bogus Char} with \tr{Bogus t} would
220 unnecessarily bind \tr{t} to \tr{Char}.
222 ... You could explicitly test for the problem synonyms and mark them
223 somehow as needing expansion, perhaps also issuing a warning to the
228 %************************************************************************
230 \subsection[Unify-uVar]{@uVar@: unifying with a type variable}
232 %************************************************************************
234 @uVar@ is called when at least one of the types being unified is a
235 variable. It does {\em not} assume that the variable is a fixed point
236 of the substitution; rather, notice that @uVar@ (defined below) nips
237 back into @uTys@ if it turns out that the variable is already bound.
240 uVar :: Bool -- False => tyvar is the "expected"
241 -- True => ty is the "expected" thing
243 -> TcTauType -> TcTauType -- printing and real versions
246 uVar swapped tv1 ps_ty2 ty2
247 = tcGetTyVar tv1 `thenNF_Tc` \ maybe_ty1 ->
249 Just ty1 | swapped -> uTys ps_ty2 ty2 ty1 ty1 -- Swap back
250 | otherwise -> uTys ty1 ty1 ps_ty2 ty2 -- Same order
251 other -> uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
254 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 (NoteTy _ ty2)
255 = uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
258 -- The both-type-variable case
259 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2@(TyVarTy tv2)
261 -- Same type variable => no-op
265 -- Distinct type variables
266 -- ASSERT maybe_ty1 /= Just
268 = tcGetTyVar tv2 `thenNF_Tc` \ maybe_ty2 ->
270 Just ty2' -> uUnboundVar swapped tv1 maybe_ty1 ty2' ty2'
272 Nothing -> checkKinds swapped tv1 ty2 `thenTc_`
274 -- Try to update sys-y type variables in preference to sig-y ones
275 -- (the latter respond False to isSystemName)
276 if isSystemName (varName tv2) then
277 tcPutTyVar tv2 (TyVarTy tv1) `thenNF_Tc_`
280 tcPutTyVar tv1 ps_ty2 `thenNF_Tc_`
283 -- Second one isn't a type variable
284 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 non_var_ty2
285 | non_var_ty2 == anyBoxKind
290 = checkKinds swapped tv1 non_var_ty2 `thenTc_`
291 occur_check non_var_ty2 `thenTc_`
292 tcPutTyVar tv1 ps_ty2 `thenNF_Tc_`
295 occur_check ty = mapTc occur_check_tv (varSetElems (tyVarsOfType ty)) `thenTc_`
299 | tv1 == tv2 -- Same tyvar; fail
300 = zonkTcType ps_ty2 `thenNF_Tc` \ zonked_ty2 ->
301 failWithTcM (unifyOccurCheck tv1 zonked_ty2)
303 | otherwise -- A different tyvar
304 = tcGetTyVar tv2 `thenNF_Tc` \ maybe_ty2 ->
306 Just ty2' -> occur_check ty2'
309 checkKinds swapped tv1 ty2
310 = tcAddErrCtxtM (unifyKindCtxt swapped tv1 ty2) $
312 -- We have to use tcTypeKind not just typeKind to get the
313 -- kind of ty2, because there might be mutable kind variables
314 -- in the way. For example, suppose that ty2 :: (a b), and
315 -- the kind of 'a' is a kind variable 'k' that has (presumably)
316 -- been unified with 'k1 -> k2'.
317 tcTypeKind ty2 `thenNF_Tc` \ k2 ->
320 unifyKind k2 (tyVarKind tv1)
322 unifyKind (tyVarKind tv1) k2
325 %************************************************************************
327 \subsection[Unify-fun]{@unifyFunTy@}
329 %************************************************************************
331 @unifyFunTy@ is used to avoid the fruitless creation of type variables.
334 unifyFunTy :: TcType -- Fail if ty isn't a function type
335 -> TcM s (TcType, TcType) -- otherwise return arg and result types
337 unifyFunTy ty@(TyVarTy tyvar)
338 = tcGetTyVar tyvar `thenNF_Tc` \ maybe_ty ->
340 Just ty' -> unifyFunTy ty'
341 other -> unify_fun_ty_help ty
344 = case splitFunTy_maybe ty of
345 Just arg_and_res -> returnTc arg_and_res
346 Nothing -> unify_fun_ty_help ty
348 unify_fun_ty_help ty -- Special cases failed, so revert to ordinary unification
349 = newTyVarTy_OpenKind `thenNF_Tc` \ arg ->
350 newTyVarTy_OpenKind `thenNF_Tc` \ res ->
351 unifyTauTy ty (mkFunTy arg res) `thenTc_`
356 unifyListTy :: TcType -- expected list type
357 -> TcM s TcType -- list element type
359 unifyListTy ty@(TyVarTy tyvar)
360 = tcGetTyVar tyvar `thenNF_Tc` \ maybe_ty ->
362 Just ty' -> unifyListTy ty'
363 other -> unify_list_ty_help ty
366 = case splitTyConApp_maybe ty of
367 Just (tycon, [arg_ty]) | tycon == listTyCon -> returnTc arg_ty
368 other -> unify_list_ty_help ty
370 unify_list_ty_help ty -- Revert to ordinary unification
371 = newTyVarTy boxedTypeKind `thenNF_Tc` \ elt_ty ->
372 unifyTauTy ty (mkListTy elt_ty) `thenTc_`
377 unifyTupleTy :: Arity -> TcType -> TcM s [TcType]
378 unifyTupleTy arity ty@(TyVarTy tyvar)
379 = tcGetTyVar tyvar `thenNF_Tc` \ maybe_ty ->
381 Just ty' -> unifyTupleTy arity ty'
382 other -> unify_tuple_ty_help arity ty
384 unifyTupleTy arity ty
385 = case splitTyConApp_maybe ty of
386 Just (tycon, arg_tys) | isTupleTyCon tycon
387 && tyConArity tycon == arity
389 other -> unify_tuple_ty_help arity ty
391 unify_tuple_ty_help arity ty
392 = mapNF_Tc (\ _ -> newTyVarTy boxedTypeKind) [1..arity] `thenNF_Tc` \ arg_tys ->
393 unifyTauTy ty (mkTupleTy arity arg_tys) `thenTc_`
398 unifyUnboxedTupleTy :: Arity -> TcType -> TcM s [TcType]
399 unifyUnboxedTupleTy arity ty@(TyVarTy tyvar)
400 = tcGetTyVar tyvar `thenNF_Tc` \ maybe_ty ->
402 Just ty' -> unifyUnboxedTupleTy arity ty'
403 other -> unify_unboxed_tuple_ty_help arity ty
405 unifyUnboxedTupleTy arity ty
406 = case splitTyConApp_maybe ty of
407 Just (tycon, arg_tys) | isUnboxedTupleTyCon tycon
408 && tyConArity tycon == arity
410 other -> unify_tuple_ty_help arity ty
412 unify_unboxed_tuple_ty_help arity ty
413 = mapNF_Tc (\ _ -> newTyVarTy_OpenKind) [1..arity] `thenNF_Tc` \ arg_tys ->
414 unifyTauTy ty (mkUnboxedTupleTy arity arg_tys) `thenTc_`
418 Make sure a kind is of the form (Type b) for some boxity b.
421 unifyTypeKind :: TcKind -> TcM s ()
422 unifyTypeKind kind@(TyVarTy kv)
423 = tcGetTyVar kv `thenNF_Tc` \ maybe_kind ->
425 Just kind' -> unifyTypeKind kind'
426 Nothing -> unify_type_kind_help kind
429 = case splitTyConApp_maybe kind of
430 Just (tycon, [_]) | tycon == typeCon -> returnTc ()
431 other -> unify_type_kind_help kind
433 unify_type_kind_help kind
434 = newOpenTypeKind `thenNF_Tc` \ expected_kind ->
435 unifyKind expected_kind kind
439 %************************************************************************
441 \subsection[Unify-context]{Errors and contexts}
443 %************************************************************************
449 unifyCtxt s ty1 ty2 tidy_env -- ty1 expected, ty2 inferred
450 = zonkTcType ty1 `thenNF_Tc` \ ty1' ->
451 zonkTcType ty2 `thenNF_Tc` \ ty2' ->
452 returnNF_Tc (err ty1' ty2')
457 text "Expected" <+> text s <> colon <+> ppr tidy_ty1,
458 text "Inferred" <+> text s <> colon <+> ppr tidy_ty2
461 (env1, [tidy_ty1,tidy_ty2]) = tidyOpenTypes tidy_env [ty1,ty2]
463 unifyKindCtxt swapped tv1 ty2 tidy_env -- not swapped => tv1 expected, ty2 inferred
464 = returnNF_Tc (env2, ptext SLIT("When matching types") <+>
465 sep [quotes pp_expected, ptext SLIT("and"), quotes pp_actual])
467 (pp_expected, pp_actual) | swapped = (pp2, pp1)
468 | otherwise = (pp1, pp2)
469 (env1, tv1') = tidyTyVar tidy_env tv1
470 (env2, ty2') = tidyOpenType env1 ty2
474 unifyMisMatch ty1 ty2
475 = zonkTcType ty1 `thenNF_Tc` \ ty1' ->
476 zonkTcType ty2 `thenNF_Tc` \ ty2' ->
478 (env, [tidy_ty1, tidy_ty2]) = tidyOpenTypes emptyTidyEnv [ty1',ty2']
479 msg = hang (ptext SLIT("Couldn't match"))
480 4 (sep [quotes (ppr tidy_ty1),
481 ptext SLIT("against"),
482 quotes (ppr tidy_ty2)])
484 failWithTcM (env, msg)
486 unifyOccurCheck tyvar ty
487 = (env2, hang (ptext SLIT("Occurs check: cannot construct the infinite type:"))
488 4 (sep [ppr tidy_tyvar, char '=', ppr tidy_ty]))
490 (env1, tidy_tyvar) = tidyTyVar emptyTidyEnv tyvar
491 (env2, tidy_ty) = tidyOpenType env1 ty