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 TypeRep ( Type(..), funTyCon,
20 Kind, boxedTypeKind, typeCon, anyBoxCon, anyBoxKind,
22 import Type ( tyVarsOfType,
23 mkFunTy, splitFunTy_maybe, splitTyConApp_maybe,
26 tidyOpenType, tidyOpenTypes, tidyTyVar
28 import TyCon ( TyCon, isTupleTyCon, isUnboxedTupleTyCon,
30 import Name ( hasBetterProv )
31 import Var ( TyVar, tyVarKind, varName, isSigTyVar )
33 import VarSet ( varSetElems )
34 import TcType ( TcType, TcTauType, TcTyVar, TcKind,
35 newTyVarTy, newOpenTypeKind, newTyVarTy_OpenKind,
36 tcGetTyVar, tcPutTyVar, zonkTcType, tcTypeKind
39 import BasicTypes ( Arity )
40 import TysWiredIn ( listTyCon, mkListTy, mkTupleTy, mkUnboxedTupleTy )
41 import PprType () -- Instances
47 %************************************************************************
49 \subsection{The Kind variants}
51 %************************************************************************
54 unifyKind :: TcKind -- Expected
58 = tcAddErrCtxtM (unifyCtxt "kind" k1 k2) $
61 unifyKinds :: [TcKind] -> [TcKind] -> TcM s ()
62 unifyKinds [] [] = returnTc ()
63 unifyKinds (k1:ks1) (k2:ks2) = unifyKind k1 k2 `thenTc_`
65 unifyKinds _ _ = panic "unifyKinds: length mis-match"
69 %************************************************************************
71 \subsection[Unify-exported]{Exported unification functions}
73 %************************************************************************
75 The exported functions are all defined as versions of some
76 non-exported generic functions.
78 Unify two @TauType@s. Dead straightforward.
81 unifyTauTy :: TcTauType -> TcTauType -> TcM s ()
82 unifyTauTy ty1 ty2 -- ty1 expected, ty2 inferred
83 = tcAddErrCtxtM (unifyCtxt "type" ty1 ty2) $
87 @unifyTauTyList@ unifies corresponding elements of two lists of
88 @TauType@s. It uses @uTys@ to do the real work. The lists should be
89 of equal length. We charge down the list explicitly so that we can
90 complain if their lengths differ.
93 unifyTauTyLists :: [TcTauType] -> [TcTauType] -> TcM s ()
94 unifyTauTyLists [] [] = returnTc ()
95 unifyTauTyLists (ty1:tys1) (ty2:tys2) = uTys ty1 ty1 ty2 ty2 `thenTc_`
96 unifyTauTyLists tys1 tys2
97 unifyTauTyLists ty1s ty2s = panic "Unify.unifyTauTyLists: mismatched type lists!"
100 @unifyTauTyList@ takes a single list of @TauType@s and unifies them
101 all together. It is used, for example, when typechecking explicit
102 lists, when all the elts should be of the same type.
105 unifyTauTyList :: [TcTauType] -> TcM s ()
106 unifyTauTyList [] = returnTc ()
107 unifyTauTyList [ty] = returnTc ()
108 unifyTauTyList (ty1:tys@(ty2:_)) = unifyTauTy ty1 ty2 `thenTc_`
112 %************************************************************************
114 \subsection[Unify-uTys]{@uTys@: getting down to business}
116 %************************************************************************
118 @uTys@ is the heart of the unifier. Each arg happens twice, because
119 we want to report errors in terms of synomyms if poss. The first of
120 the pair is used in error messages only; it is always the same as the
121 second, except that if the first is a synonym then the second may be a
122 de-synonym'd version. This way we get better error messages.
124 We call the first one \tr{ps_ty1}, \tr{ps_ty2} for ``possible synomym''.
127 uTys :: TcTauType -> TcTauType -- Error reporting ty1 and real ty1
128 -> TcTauType -> TcTauType -- Error reporting ty2 and real ty2
131 -- Always expand synonyms (see notes at end)
132 -- (this also throws away FTVs and usage annots)
133 uTys ps_ty1 (NoteTy _ ty1) ps_ty2 ty2 = uTys ps_ty1 ty1 ps_ty2 ty2
134 uTys ps_ty1 ty1 ps_ty2 (NoteTy _ ty2) = uTys ps_ty1 ty1 ps_ty2 ty2
136 -- Variables; go for uVar
137 uTys ps_ty1 (TyVarTy tyvar1) ps_ty2 ty2 = uVar False tyvar1 ps_ty2 ty2
138 uTys ps_ty1 ty1 ps_ty2 (TyVarTy tyvar2) = uVar True tyvar2 ps_ty1 ty1
139 -- "True" means args swapped
141 -- Functions; just check the two parts
142 uTys _ (FunTy fun1 arg1) _ (FunTy fun2 arg2)
143 = uTys fun1 fun1 fun2 fun2 `thenTc_` uTys arg1 arg1 arg2 arg2
145 -- Type constructors must match
146 uTys ps_ty1 (TyConApp con1 tys1) ps_ty2 (TyConApp con2 tys2)
147 = checkTcM (cons_match && length tys1 == length tys2)
148 (unifyMisMatch ps_ty1 ps_ty2) `thenTc_`
149 unifyTauTyLists tys1 tys2
151 -- The AnyBox wild card matches anything
152 cons_match = con1 == con2
156 -- Applications need a bit of care!
157 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
158 -- NB: we've already dealt with type variables and Notes,
159 -- so if one type is an App the other one jolly well better be too
160 uTys ps_ty1 (AppTy s1 t1) ps_ty2 ty2
161 = case splitAppTy_maybe ty2 of
162 Just (s2,t2) -> uTys s1 s1 s2 s2 `thenTc_` uTys t1 t1 t2 t2
163 Nothing -> unifyMisMatch ps_ty1 ps_ty2
165 -- Now the same, but the other way round
166 -- Don't swap the types, because the error messages get worse
167 uTys ps_ty1 ty1 ps_ty2 (AppTy s2 t2)
168 = case splitAppTy_maybe ty1 of
169 Just (s1,t1) -> uTys s1 s1 s2 s2 `thenTc_` uTys t1 t1 t2 t2
170 Nothing -> unifyMisMatch ps_ty1 ps_ty2
172 -- Not expecting for-alls in unification
173 -- ... but the error message from the unifyMisMatch more informative
174 -- than a panic message!
176 -- Anything else fails
177 uTys ps_ty1 ty1 ps_ty2 ty2 = unifyMisMatch ps_ty1 ps_ty2
182 If you are tempted to make a short cut on synonyms, as in this
186 uTys (SynTy con1 args1 ty1) (SynTy con2 args2 ty2)
187 = if (con1 == con2) then
188 -- Good news! Same synonym constructors, so we can shortcut
189 -- by unifying their arguments and ignoring their expansions.
190 unifyTauTypeLists args1 args2
192 -- Never mind. Just expand them and try again
196 then THINK AGAIN. Here is the whole story, as detected and reported
197 by Chris Okasaki \tr{<Chris_Okasaki@loch.mess.cs.cmu.edu>}:
199 Here's a test program that should detect the problem:
203 x = (1 :: Bogus Char) :: Bogus Bool
206 The problem with [the attempted shortcut code] is that
210 is not a sufficient condition to be able to use the shortcut!
211 You also need to know that the type synonym actually USES all
212 its arguments. For example, consider the following type synonym
213 which does not use all its arguments.
218 If you ever tried unifying, say, \tr{Bogus Char} with \tr{Bogus Bool},
219 the unifier would blithely try to unify \tr{Char} with \tr{Bool} and
220 would fail, even though the expanded forms (both \tr{Int}) should
223 Similarly, unifying \tr{Bogus Char} with \tr{Bogus t} would
224 unnecessarily bind \tr{t} to \tr{Char}.
226 ... You could explicitly test for the problem synonyms and mark them
227 somehow as needing expansion, perhaps also issuing a warning to the
232 %************************************************************************
234 \subsection[Unify-uVar]{@uVar@: unifying with a type variable}
236 %************************************************************************
238 @uVar@ is called when at least one of the types being unified is a
239 variable. It does {\em not} assume that the variable is a fixed point
240 of the substitution; rather, notice that @uVar@ (defined below) nips
241 back into @uTys@ if it turns out that the variable is already bound.
244 uVar :: Bool -- False => tyvar is the "expected"
245 -- True => ty is the "expected" thing
247 -> TcTauType -> TcTauType -- printing and real versions
250 uVar swapped tv1 ps_ty2 ty2
251 = tcGetTyVar tv1 `thenNF_Tc` \ maybe_ty1 ->
253 Just ty1 | swapped -> uTys ps_ty2 ty2 ty1 ty1 -- Swap back
254 | otherwise -> uTys ty1 ty1 ps_ty2 ty2 -- Same order
255 other -> uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
257 -- Expand synonyms; ignore FTVs; ignore usage annots
258 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 (NoteTy _ ty2)
259 = uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
262 -- The both-type-variable case
263 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2@(TyVarTy tv2)
265 -- Same type variable => no-op
269 -- Distinct type variables
270 -- ASSERT maybe_ty1 /= Just
272 = tcGetTyVar tv2 `thenNF_Tc` \ maybe_ty2 ->
274 Just ty2' -> uUnboundVar swapped tv1 maybe_ty1 ty2' ty2'
276 Nothing -> checkKinds swapped tv1 ty2 `thenTc_`
278 if tv1 `dominates` tv2 then
279 tcPutTyVar tv2 (TyVarTy tv1) `thenNF_Tc_`
282 ASSERT( isNotUsgTy ps_ty2 )
283 tcPutTyVar tv1 ps_ty2 `thenNF_Tc_`
286 tv1 `dominates` tv2 = isSigTyVar tv1
287 -- Don't unify a signature type variable if poss
288 || varName tv1 `hasBetterProv` varName tv2
289 -- Try to update sys-y type variables in preference to sig-y ones
291 -- Second one isn't a type variable
292 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 non_var_ty2
293 | non_var_ty2 == anyBoxKind
298 = checkKinds swapped tv1 non_var_ty2 `thenTc_`
299 occur_check non_var_ty2 `thenTc_`
300 ASSERT( isNotUsgTy ps_ty2 )
301 checkTcM (not (isSigTyVar tv1))
302 (failWithTcM (unifyWithSigErr tv1 ps_ty2)) `thenTc_`
304 tcPutTyVar tv1 non_var_ty2 `thenNF_Tc_`
305 -- This used to say "ps_ty2" instead of "non_var_ty2"
307 -- But that led to an infinite loop in the type checker!
311 -- f :: (A a -> a -> ()) -> ()
315 -- x = f (\ x p -> p x)
317 -- Here, we try to match "t" with "A t", and succeed
318 -- because the unifier looks through synonyms. The occurs
319 -- check doesn't kick in because we are "really" binding "t" to "()",
320 -- but we *actually* bind "t" to "A t" if we store ps_ty2.
321 -- That leads the typechecker into an infinite loop later.
325 occur_check ty = mapTc occur_check_tv (varSetElems (tyVarsOfType ty)) `thenTc_`
329 | tv1 == tv2 -- Same tyvar; fail
330 = zonkTcType ps_ty2 `thenNF_Tc` \ zonked_ty2 ->
331 failWithTcM (unifyOccurCheck tv1 zonked_ty2)
333 | otherwise -- A different tyvar
334 = tcGetTyVar tv2 `thenNF_Tc` \ maybe_ty2 ->
336 Just ty2' -> occur_check ty2'
339 checkKinds swapped tv1 ty2
340 = tcAddErrCtxtM (unifyKindCtxt swapped tv1 ty2) $
342 -- We have to use tcTypeKind not just typeKind to get the
343 -- kind of ty2, because there might be mutable kind variables
344 -- in the way. For example, suppose that ty2 :: (a b), and
345 -- the kind of 'a' is a kind variable 'k' that has (presumably)
346 -- been unified with 'k1 -> k2'.
347 tcTypeKind ty2 `thenNF_Tc` \ k2 ->
350 unifyKind k2 (tyVarKind tv1)
352 unifyKind (tyVarKind tv1) k2
355 %************************************************************************
357 \subsection[Unify-fun]{@unifyFunTy@}
359 %************************************************************************
361 @unifyFunTy@ is used to avoid the fruitless creation of type variables.
364 unifyFunTy :: TcType -- Fail if ty isn't a function type
365 -> TcM s (TcType, TcType) -- otherwise return arg and result types
367 unifyFunTy ty@(TyVarTy tyvar)
368 = tcGetTyVar tyvar `thenNF_Tc` \ maybe_ty ->
370 Just ty' -> unifyFunTy ty'
371 other -> unify_fun_ty_help ty
374 = case splitFunTy_maybe ty of
375 Just arg_and_res -> returnTc arg_and_res
376 Nothing -> unify_fun_ty_help ty
378 unify_fun_ty_help ty -- Special cases failed, so revert to ordinary unification
379 = newTyVarTy_OpenKind `thenNF_Tc` \ arg ->
380 newTyVarTy_OpenKind `thenNF_Tc` \ res ->
381 unifyTauTy ty (mkFunTy arg res) `thenTc_`
386 unifyListTy :: TcType -- expected list type
387 -> TcM s TcType -- list element type
389 unifyListTy ty@(TyVarTy tyvar)
390 = tcGetTyVar tyvar `thenNF_Tc` \ maybe_ty ->
392 Just ty' -> unifyListTy ty'
393 other -> unify_list_ty_help ty
396 = case splitTyConApp_maybe ty of
397 Just (tycon, [arg_ty]) | tycon == listTyCon -> returnTc arg_ty
398 other -> unify_list_ty_help ty
400 unify_list_ty_help ty -- Revert to ordinary unification
401 = newTyVarTy boxedTypeKind `thenNF_Tc` \ elt_ty ->
402 unifyTauTy ty (mkListTy elt_ty) `thenTc_`
407 unifyTupleTy :: Arity -> TcType -> TcM s [TcType]
408 unifyTupleTy arity ty@(TyVarTy tyvar)
409 = tcGetTyVar tyvar `thenNF_Tc` \ maybe_ty ->
411 Just ty' -> unifyTupleTy arity ty'
412 other -> unify_tuple_ty_help arity ty
414 unifyTupleTy arity ty
415 = case splitTyConApp_maybe ty of
416 Just (tycon, arg_tys) | isTupleTyCon tycon
417 && tyConArity tycon == arity
419 other -> unify_tuple_ty_help arity ty
421 unify_tuple_ty_help arity ty
422 = mapNF_Tc (\ _ -> newTyVarTy boxedTypeKind) [1..arity] `thenNF_Tc` \ arg_tys ->
423 unifyTauTy ty (mkTupleTy arity arg_tys) `thenTc_`
428 unifyUnboxedTupleTy :: Arity -> TcType -> TcM s [TcType]
429 unifyUnboxedTupleTy arity ty@(TyVarTy tyvar)
430 = tcGetTyVar tyvar `thenNF_Tc` \ maybe_ty ->
432 Just ty' -> unifyUnboxedTupleTy arity ty'
433 other -> unify_unboxed_tuple_ty_help arity ty
435 unifyUnboxedTupleTy arity ty
436 = case splitTyConApp_maybe ty of
437 Just (tycon, arg_tys) | isUnboxedTupleTyCon tycon
438 && tyConArity tycon == arity
440 other -> unify_tuple_ty_help arity ty
442 unify_unboxed_tuple_ty_help arity ty
443 = mapNF_Tc (\ _ -> newTyVarTy_OpenKind) [1..arity] `thenNF_Tc` \ arg_tys ->
444 unifyTauTy ty (mkUnboxedTupleTy arity arg_tys) `thenTc_`
448 Make sure a kind is of the form (Type b) for some boxity b.
451 unifyTypeKind :: TcKind -> TcM s ()
452 unifyTypeKind kind@(TyVarTy kv)
453 = tcGetTyVar kv `thenNF_Tc` \ maybe_kind ->
455 Just kind' -> unifyTypeKind kind'
456 Nothing -> unify_type_kind_help kind
459 = case splitTyConApp_maybe kind of
460 Just (tycon, [_]) | tycon == typeCon -> returnTc ()
461 other -> unify_type_kind_help kind
463 unify_type_kind_help kind
464 = newOpenTypeKind `thenNF_Tc` \ expected_kind ->
465 unifyKind expected_kind kind
469 %************************************************************************
471 \subsection[Unify-context]{Errors and contexts}
473 %************************************************************************
479 unifyCtxt s ty1 ty2 tidy_env -- ty1 expected, ty2 inferred
480 = zonkTcType ty1 `thenNF_Tc` \ ty1' ->
481 zonkTcType ty2 `thenNF_Tc` \ ty2' ->
482 returnNF_Tc (err ty1' ty2')
487 text "Expected" <+> text s <> colon <+> ppr tidy_ty1,
488 text "Inferred" <+> text s <> colon <+> ppr tidy_ty2
491 (env1, [tidy_ty1,tidy_ty2]) = tidyOpenTypes tidy_env [ty1,ty2]
493 unifyKindCtxt swapped tv1 ty2 tidy_env -- not swapped => tv1 expected, ty2 inferred
494 = returnNF_Tc (env2, ptext SLIT("When matching types") <+>
495 sep [quotes pp_expected, ptext SLIT("and"), quotes pp_actual])
497 (pp_expected, pp_actual) | swapped = (pp2, pp1)
498 | otherwise = (pp1, pp2)
499 (env1, tv1') = tidyTyVar tidy_env tv1
500 (env2, ty2') = tidyOpenType env1 ty2
504 unifyMisMatch ty1 ty2
505 = zonkTcType ty1 `thenNF_Tc` \ ty1' ->
506 zonkTcType ty2 `thenNF_Tc` \ ty2' ->
508 (env, [tidy_ty1, tidy_ty2]) = tidyOpenTypes emptyTidyEnv [ty1',ty2']
509 msg = hang (ptext SLIT("Couldn't match"))
510 4 (sep [quotes (ppr tidy_ty1),
511 ptext SLIT("against"),
512 quotes (ppr tidy_ty2)])
514 failWithTcM (env, msg)
516 unifyWithSigErr tyvar ty
517 = (env2, hang (ptext SLIT("Cannot unify the type-signature variable") <+> quotes (ppr tidy_tyvar))
518 4 (ptext SLIT("with the type") <+> quotes (ppr tidy_ty)))
520 (env1, tidy_tyvar) = tidyTyVar emptyTidyEnv tyvar
521 (env2, tidy_ty) = tidyOpenType env1 ty
523 unifyOccurCheck tyvar ty
524 = (env2, hang (ptext SLIT("Occurs check: cannot construct the infinite type:"))
525 4 (sep [ppr tidy_tyvar, char '=', ppr tidy_ty]))
527 (env1, tidy_tyvar) = tidyTyVar emptyTidyEnv tyvar
528 (env2, tidy_ty) = tidyOpenType env1 ty