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,
22 Kind, boxedTypeKind, typeCon, anyBoxCon, anyBoxKind,
24 tidyOpenType, tidyOpenTypes, tidyTyVar
26 import TyCon ( TyCon, isTupleTyCon, isUnboxedTupleTyCon,
28 import Name ( hasBetterProv )
29 import Var ( TyVar, tyVarKind, varName, isSigTyVar )
31 import VarSet ( varSetElems )
32 import TcType ( TcType, TcTauType, TcTyVar, TcKind,
33 newTyVarTy, newOpenTypeKind, newTyVarTy_OpenKind,
34 tcGetTyVar, tcPutTyVar, zonkTcType, tcTypeKind
37 import BasicTypes ( Arity )
38 import TysWiredIn ( listTyCon, mkListTy, mkTupleTy, mkUnboxedTupleTy )
39 import PprType () -- Instances
45 %************************************************************************
47 \subsection{The Kind variants}
49 %************************************************************************
52 unifyKind :: TcKind -- Expected
56 = tcAddErrCtxtM (unifyCtxt "kind" k1 k2) $
59 unifyKinds :: [TcKind] -> [TcKind] -> TcM s ()
60 unifyKinds [] [] = returnTc ()
61 unifyKinds (k1:ks1) (k2:ks2) = unifyKind k1 k2 `thenTc_`
63 unifyKinds _ _ = panic "unifyKinds: length mis-match"
67 %************************************************************************
69 \subsection[Unify-exported]{Exported unification functions}
71 %************************************************************************
73 The exported functions are all defined as versions of some
74 non-exported generic functions.
76 Unify two @TauType@s. Dead straightforward.
79 unifyTauTy :: TcTauType -> TcTauType -> TcM s ()
80 unifyTauTy ty1 ty2 -- ty1 expected, ty2 inferred
81 = tcAddErrCtxtM (unifyCtxt "type" ty1 ty2) $
85 @unifyTauTyList@ unifies corresponding elements of two lists of
86 @TauType@s. It uses @uTys@ to do the real work. The lists should be
87 of equal length. We charge down the list explicitly so that we can
88 complain if their lengths differ.
91 unifyTauTyLists :: [TcTauType] -> [TcTauType] -> TcM s ()
92 unifyTauTyLists [] [] = returnTc ()
93 unifyTauTyLists (ty1:tys1) (ty2:tys2) = uTys ty1 ty1 ty2 ty2 `thenTc_`
94 unifyTauTyLists tys1 tys2
95 unifyTauTyLists ty1s ty2s = panic "Unify.unifyTauTyLists: mismatched type lists!"
98 @unifyTauTyList@ takes a single list of @TauType@s and unifies them
99 all together. It is used, for example, when typechecking explicit
100 lists, when all the elts should be of the same type.
103 unifyTauTyList :: [TcTauType] -> TcM s ()
104 unifyTauTyList [] = returnTc ()
105 unifyTauTyList [ty] = returnTc ()
106 unifyTauTyList (ty1:tys@(ty2:_)) = unifyTauTy ty1 ty2 `thenTc_`
110 %************************************************************************
112 \subsection[Unify-uTys]{@uTys@: getting down to business}
114 %************************************************************************
116 @uTys@ is the heart of the unifier. Each arg happens twice, because
117 we want to report errors in terms of synomyms if poss. The first of
118 the pair is used in error messages only; it is always the same as the
119 second, except that if the first is a synonym then the second may be a
120 de-synonym'd version. This way we get better error messages.
122 We call the first one \tr{ps_ty1}, \tr{ps_ty2} for ``possible synomym''.
125 uTys :: TcTauType -> TcTauType -- Error reporting ty1 and real ty1
126 -> TcTauType -> TcTauType -- Error reporting ty2 and real ty2
129 -- Always expand synonyms (see notes at end)
130 -- (this also throws away FTVs and usage annots)
131 uTys ps_ty1 (NoteTy _ ty1) ps_ty2 ty2 = uTys ps_ty1 ty1 ps_ty2 ty2
132 uTys ps_ty1 ty1 ps_ty2 (NoteTy _ ty2) = uTys ps_ty1 ty1 ps_ty2 ty2
134 -- Variables; go for uVar
135 uTys ps_ty1 (TyVarTy tyvar1) ps_ty2 ty2 = uVar False tyvar1 ps_ty2 ty2
136 uTys ps_ty1 ty1 ps_ty2 (TyVarTy tyvar2) = uVar True tyvar2 ps_ty1 ty1
137 -- "True" means args swapped
139 -- Functions; just check the two parts
140 uTys _ (FunTy fun1 arg1) _ (FunTy fun2 arg2)
141 = uTys fun1 fun1 fun2 fun2 `thenTc_` uTys arg1 arg1 arg2 arg2
143 -- Type constructors must match
144 uTys ps_ty1 (TyConApp con1 tys1) ps_ty2 (TyConApp con2 tys2)
145 = checkTcM (cons_match && length tys1 == length tys2)
146 (unifyMisMatch ps_ty1 ps_ty2) `thenTc_`
147 unifyTauTyLists tys1 tys2
149 -- The AnyBox wild card matches anything
150 cons_match = con1 == con2
154 -- Applications need a bit of care!
155 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
156 -- NB: we've already dealt with type variables and Notes,
157 -- so if one type is an App the other one jolly well better be too
158 uTys ps_ty1 (AppTy s1 t1) ps_ty2 ty2
159 = case splitAppTy_maybe ty2 of
160 Just (s2,t2) -> uTys s1 s1 s2 s2 `thenTc_` uTys t1 t1 t2 t2
161 Nothing -> unifyMisMatch ps_ty1 ps_ty2
163 -- Now the same, but the other way round
164 -- Don't swap the types, because the error messages get worse
165 uTys ps_ty1 ty1 ps_ty2 (AppTy s2 t2)
166 = case splitAppTy_maybe ty1 of
167 Just (s1,t1) -> uTys s1 s1 s2 s2 `thenTc_` uTys t1 t1 t2 t2
168 Nothing -> unifyMisMatch ps_ty1 ps_ty2
170 -- Not expecting for-alls in unification
171 -- ... but the error message from the unifyMisMatch more informative
172 -- than a panic message!
174 -- Anything else fails
175 uTys ps_ty1 ty1 ps_ty2 ty2 = unifyMisMatch ps_ty1 ps_ty2
180 If you are tempted to make a short cut on synonyms, as in this
184 uTys (SynTy con1 args1 ty1) (SynTy con2 args2 ty2)
185 = if (con1 == con2) then
186 -- Good news! Same synonym constructors, so we can shortcut
187 -- by unifying their arguments and ignoring their expansions.
188 unifyTauTypeLists args1 args2
190 -- Never mind. Just expand them and try again
194 then THINK AGAIN. Here is the whole story, as detected and reported
195 by Chris Okasaki \tr{<Chris_Okasaki@loch.mess.cs.cmu.edu>}:
197 Here's a test program that should detect the problem:
201 x = (1 :: Bogus Char) :: Bogus Bool
204 The problem with [the attempted shortcut code] is that
208 is not a sufficient condition to be able to use the shortcut!
209 You also need to know that the type synonym actually USES all
210 its arguments. For example, consider the following type synonym
211 which does not use all its arguments.
216 If you ever tried unifying, say, \tr{Bogus Char} with \tr{Bogus Bool},
217 the unifier would blithely try to unify \tr{Char} with \tr{Bool} and
218 would fail, even though the expanded forms (both \tr{Int}) should
221 Similarly, unifying \tr{Bogus Char} with \tr{Bogus t} would
222 unnecessarily bind \tr{t} to \tr{Char}.
224 ... You could explicitly test for the problem synonyms and mark them
225 somehow as needing expansion, perhaps also issuing a warning to the
230 %************************************************************************
232 \subsection[Unify-uVar]{@uVar@: unifying with a type variable}
234 %************************************************************************
236 @uVar@ is called when at least one of the types being unified is a
237 variable. It does {\em not} assume that the variable is a fixed point
238 of the substitution; rather, notice that @uVar@ (defined below) nips
239 back into @uTys@ if it turns out that the variable is already bound.
242 uVar :: Bool -- False => tyvar is the "expected"
243 -- True => ty is the "expected" thing
245 -> TcTauType -> TcTauType -- printing and real versions
248 uVar swapped tv1 ps_ty2 ty2
249 = tcGetTyVar tv1 `thenNF_Tc` \ maybe_ty1 ->
251 Just ty1 | swapped -> uTys ps_ty2 ty2 ty1 ty1 -- Swap back
252 | otherwise -> uTys ty1 ty1 ps_ty2 ty2 -- Same order
253 other -> uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
255 -- Expand synonyms; ignore FTVs; ignore usage annots
256 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 (NoteTy _ ty2)
257 = uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
260 -- The both-type-variable case
261 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2@(TyVarTy tv2)
263 -- Same type variable => no-op
267 -- Distinct type variables
268 -- ASSERT maybe_ty1 /= Just
270 = tcGetTyVar tv2 `thenNF_Tc` \ maybe_ty2 ->
272 Just ty2' -> uUnboundVar swapped tv1 maybe_ty1 ty2' ty2'
274 Nothing -> checkKinds swapped tv1 ty2 `thenTc_`
276 if tv1 `dominates` tv2 then
277 tcPutTyVar tv2 (TyVarTy tv1) `thenNF_Tc_`
280 ASSERT( isNotUsgTy ps_ty2 )
281 tcPutTyVar tv1 ps_ty2 `thenNF_Tc_`
284 tv1 `dominates` tv2 = isSigTyVar tv1
285 -- Don't unify a signature type variable if poss
286 || varName tv1 `hasBetterProv` varName tv2
287 -- Try to update sys-y type variables in preference to sig-y ones
289 -- Second one isn't a type variable
290 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 non_var_ty2
291 | non_var_ty2 == anyBoxKind
296 = checkKinds swapped tv1 non_var_ty2 `thenTc_`
297 occur_check non_var_ty2 `thenTc_`
298 ASSERT( isNotUsgTy ps_ty2 )
299 checkTcM (not (isSigTyVar tv1))
300 (failWithTcM (unifyWithSigErr tv1 ps_ty2)) `thenTc_`
301 tcPutTyVar tv1 ps_ty2 `thenNF_Tc_`
304 occur_check ty = mapTc occur_check_tv (varSetElems (tyVarsOfType ty)) `thenTc_`
308 | tv1 == tv2 -- Same tyvar; fail
309 = zonkTcType ps_ty2 `thenNF_Tc` \ zonked_ty2 ->
310 failWithTcM (unifyOccurCheck tv1 zonked_ty2)
312 | otherwise -- A different tyvar
313 = tcGetTyVar tv2 `thenNF_Tc` \ maybe_ty2 ->
315 Just ty2' -> occur_check ty2'
318 checkKinds swapped tv1 ty2
319 = tcAddErrCtxtM (unifyKindCtxt swapped tv1 ty2) $
321 -- We have to use tcTypeKind not just typeKind to get the
322 -- kind of ty2, because there might be mutable kind variables
323 -- in the way. For example, suppose that ty2 :: (a b), and
324 -- the kind of 'a' is a kind variable 'k' that has (presumably)
325 -- been unified with 'k1 -> k2'.
326 tcTypeKind ty2 `thenNF_Tc` \ k2 ->
329 unifyKind k2 (tyVarKind tv1)
331 unifyKind (tyVarKind tv1) k2
334 %************************************************************************
336 \subsection[Unify-fun]{@unifyFunTy@}
338 %************************************************************************
340 @unifyFunTy@ is used to avoid the fruitless creation of type variables.
343 unifyFunTy :: TcType -- Fail if ty isn't a function type
344 -> TcM s (TcType, TcType) -- otherwise return arg and result types
346 unifyFunTy ty@(TyVarTy tyvar)
347 = tcGetTyVar tyvar `thenNF_Tc` \ maybe_ty ->
349 Just ty' -> unifyFunTy ty'
350 other -> unify_fun_ty_help ty
353 = case splitFunTy_maybe ty of
354 Just arg_and_res -> returnTc arg_and_res
355 Nothing -> unify_fun_ty_help ty
357 unify_fun_ty_help ty -- Special cases failed, so revert to ordinary unification
358 = newTyVarTy_OpenKind `thenNF_Tc` \ arg ->
359 newTyVarTy_OpenKind `thenNF_Tc` \ res ->
360 unifyTauTy ty (mkFunTy arg res) `thenTc_`
365 unifyListTy :: TcType -- expected list type
366 -> TcM s TcType -- list element type
368 unifyListTy ty@(TyVarTy tyvar)
369 = tcGetTyVar tyvar `thenNF_Tc` \ maybe_ty ->
371 Just ty' -> unifyListTy ty'
372 other -> unify_list_ty_help ty
375 = case splitTyConApp_maybe ty of
376 Just (tycon, [arg_ty]) | tycon == listTyCon -> returnTc arg_ty
377 other -> unify_list_ty_help ty
379 unify_list_ty_help ty -- Revert to ordinary unification
380 = newTyVarTy boxedTypeKind `thenNF_Tc` \ elt_ty ->
381 unifyTauTy ty (mkListTy elt_ty) `thenTc_`
386 unifyTupleTy :: Arity -> TcType -> TcM s [TcType]
387 unifyTupleTy arity ty@(TyVarTy tyvar)
388 = tcGetTyVar tyvar `thenNF_Tc` \ maybe_ty ->
390 Just ty' -> unifyTupleTy arity ty'
391 other -> unify_tuple_ty_help arity ty
393 unifyTupleTy arity ty
394 = case splitTyConApp_maybe ty of
395 Just (tycon, arg_tys) | isTupleTyCon tycon
396 && tyConArity tycon == arity
398 other -> unify_tuple_ty_help arity ty
400 unify_tuple_ty_help arity ty
401 = mapNF_Tc (\ _ -> newTyVarTy boxedTypeKind) [1..arity] `thenNF_Tc` \ arg_tys ->
402 unifyTauTy ty (mkTupleTy arity arg_tys) `thenTc_`
407 unifyUnboxedTupleTy :: Arity -> TcType -> TcM s [TcType]
408 unifyUnboxedTupleTy arity ty@(TyVarTy tyvar)
409 = tcGetTyVar tyvar `thenNF_Tc` \ maybe_ty ->
411 Just ty' -> unifyUnboxedTupleTy arity ty'
412 other -> unify_unboxed_tuple_ty_help arity ty
414 unifyUnboxedTupleTy arity ty
415 = case splitTyConApp_maybe ty of
416 Just (tycon, arg_tys) | isUnboxedTupleTyCon tycon
417 && tyConArity tycon == arity
419 other -> unify_tuple_ty_help arity ty
421 unify_unboxed_tuple_ty_help arity ty
422 = mapNF_Tc (\ _ -> newTyVarTy_OpenKind) [1..arity] `thenNF_Tc` \ arg_tys ->
423 unifyTauTy ty (mkUnboxedTupleTy arity arg_tys) `thenTc_`
427 Make sure a kind is of the form (Type b) for some boxity b.
430 unifyTypeKind :: TcKind -> TcM s ()
431 unifyTypeKind kind@(TyVarTy kv)
432 = tcGetTyVar kv `thenNF_Tc` \ maybe_kind ->
434 Just kind' -> unifyTypeKind kind'
435 Nothing -> unify_type_kind_help kind
438 = case splitTyConApp_maybe kind of
439 Just (tycon, [_]) | tycon == typeCon -> returnTc ()
440 other -> unify_type_kind_help kind
442 unify_type_kind_help kind
443 = newOpenTypeKind `thenNF_Tc` \ expected_kind ->
444 unifyKind expected_kind kind
448 %************************************************************************
450 \subsection[Unify-context]{Errors and contexts}
452 %************************************************************************
458 unifyCtxt s ty1 ty2 tidy_env -- ty1 expected, ty2 inferred
459 = zonkTcType ty1 `thenNF_Tc` \ ty1' ->
460 zonkTcType ty2 `thenNF_Tc` \ ty2' ->
461 returnNF_Tc (err ty1' ty2')
466 text "Expected" <+> text s <> colon <+> ppr tidy_ty1,
467 text "Inferred" <+> text s <> colon <+> ppr tidy_ty2
470 (env1, [tidy_ty1,tidy_ty2]) = tidyOpenTypes tidy_env [ty1,ty2]
472 unifyKindCtxt swapped tv1 ty2 tidy_env -- not swapped => tv1 expected, ty2 inferred
473 = returnNF_Tc (env2, ptext SLIT("When matching types") <+>
474 sep [quotes pp_expected, ptext SLIT("and"), quotes pp_actual])
476 (pp_expected, pp_actual) | swapped = (pp2, pp1)
477 | otherwise = (pp1, pp2)
478 (env1, tv1') = tidyTyVar tidy_env tv1
479 (env2, ty2') = tidyOpenType env1 ty2
483 unifyMisMatch ty1 ty2
484 = zonkTcType ty1 `thenNF_Tc` \ ty1' ->
485 zonkTcType ty2 `thenNF_Tc` \ ty2' ->
487 (env, [tidy_ty1, tidy_ty2]) = tidyOpenTypes emptyTidyEnv [ty1',ty2']
488 msg = hang (ptext SLIT("Couldn't match"))
489 4 (sep [quotes (ppr tidy_ty1),
490 ptext SLIT("against"),
491 quotes (ppr tidy_ty2)])
493 failWithTcM (env, msg)
495 unifyWithSigErr tyvar ty
496 = (env2, hang (ptext SLIT("Cannot unify the type-signature variable") <+> quotes (ppr tidy_tyvar))
497 4 (ptext SLIT("with the type") <+> quotes (ppr tidy_ty)))
499 (env1, tidy_tyvar) = tidyTyVar emptyTidyEnv tyvar
500 (env2, tidy_ty) = tidyOpenType env1 ty
502 unifyOccurCheck tyvar ty
503 = (env2, hang (ptext SLIT("Occurs check: cannot construct the infinite type:"))
504 4 (sep [ppr tidy_tyvar, char '=', ppr tidy_ty]))
506 (env1, tidy_tyvar) = tidyTyVar emptyTidyEnv tyvar
507 (env2, tidy_ty) = tidyOpenType env1 ty