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, 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, tupleTyConBoxity, tyConArity )
29 import Name ( hasBetterProv )
30 import Var ( TyVar, tyVarKind, varName, isSigTyVar )
32 import VarSet ( varSetElems )
33 import TcType ( TcType, TcTauType, TcTyVar, TcKind,
34 newTyVarTy, newOpenTypeKind, newTyVarTy_OpenKind,
35 tcGetTyVar, tcPutTyVar, zonkTcType, tcTypeKind
38 import BasicTypes ( Arity, Boxity, isBoxed )
39 import TysWiredIn ( listTyCon, mkListTy, mkTupleTy )
40 import PprType () -- Instances
46 %************************************************************************
48 \subsection{The Kind variants}
50 %************************************************************************
53 unifyKind :: TcKind -- Expected
57 = tcAddErrCtxtM (unifyCtxt "kind" k1 k2) $
60 unifyKinds :: [TcKind] -> [TcKind] -> TcM s ()
61 unifyKinds [] [] = returnTc ()
62 unifyKinds (k1:ks1) (k2:ks2) = unifyKind k1 k2 `thenTc_`
64 unifyKinds _ _ = panic "unifyKinds: length mis-match"
68 %************************************************************************
70 \subsection[Unify-exported]{Exported unification functions}
72 %************************************************************************
74 The exported functions are all defined as versions of some
75 non-exported generic functions.
77 Unify two @TauType@s. Dead straightforward.
80 unifyTauTy :: TcTauType -> TcTauType -> TcM s ()
81 unifyTauTy ty1 ty2 -- ty1 expected, ty2 inferred
82 = tcAddErrCtxtM (unifyCtxt "type" ty1 ty2) $
86 @unifyTauTyList@ unifies corresponding elements of two lists of
87 @TauType@s. It uses @uTys@ to do the real work. The lists should be
88 of equal length. We charge down the list explicitly so that we can
89 complain if their lengths differ.
92 unifyTauTyLists :: [TcTauType] -> [TcTauType] -> TcM s ()
93 unifyTauTyLists [] [] = returnTc ()
94 unifyTauTyLists (ty1:tys1) (ty2:tys2) = uTys ty1 ty1 ty2 ty2 `thenTc_`
95 unifyTauTyLists tys1 tys2
96 unifyTauTyLists ty1s ty2s = panic "Unify.unifyTauTyLists: mismatched type lists!"
99 @unifyTauTyList@ takes a single list of @TauType@s and unifies them
100 all together. It is used, for example, when typechecking explicit
101 lists, when all the elts should be of the same type.
104 unifyTauTyList :: [TcTauType] -> TcM s ()
105 unifyTauTyList [] = returnTc ()
106 unifyTauTyList [ty] = returnTc ()
107 unifyTauTyList (ty1:tys@(ty2:_)) = unifyTauTy ty1 ty2 `thenTc_`
111 %************************************************************************
113 \subsection[Unify-uTys]{@uTys@: getting down to business}
115 %************************************************************************
117 @uTys@ is the heart of the unifier. Each arg happens twice, because
118 we want to report errors in terms of synomyms if poss. The first of
119 the pair is used in error messages only; it is always the same as the
120 second, except that if the first is a synonym then the second may be a
121 de-synonym'd version. This way we get better error messages.
123 We call the first one \tr{ps_ty1}, \tr{ps_ty2} for ``possible synomym''.
126 uTys :: TcTauType -> TcTauType -- Error reporting ty1 and real ty1
127 -> TcTauType -> TcTauType -- Error reporting ty2 and real ty2
130 -- Always expand synonyms (see notes at end)
131 -- (this also throws away FTVs and usage annots)
132 uTys ps_ty1 (NoteTy _ ty1) ps_ty2 ty2 = uTys ps_ty1 ty1 ps_ty2 ty2
133 uTys ps_ty1 ty1 ps_ty2 (NoteTy _ ty2) = uTys ps_ty1 ty1 ps_ty2 ty2
135 -- Variables; go for uVar
136 uTys ps_ty1 (TyVarTy tyvar1) ps_ty2 ty2 = uVar False tyvar1 ps_ty2 ty2
137 uTys ps_ty1 ty1 ps_ty2 (TyVarTy tyvar2) = uVar True tyvar2 ps_ty1 ty1
138 -- "True" means args swapped
140 -- Functions; just check the two parts
141 uTys _ (FunTy fun1 arg1) _ (FunTy fun2 arg2)
142 = uTys fun1 fun1 fun2 fun2 `thenTc_` uTys arg1 arg1 arg2 arg2
144 -- Type constructors must match
145 uTys ps_ty1 (TyConApp con1 tys1) ps_ty2 (TyConApp con2 tys2)
146 = checkTcM (cons_match && length tys1 == length tys2)
147 (unifyMisMatch ps_ty1 ps_ty2) `thenTc_`
148 unifyTauTyLists tys1 tys2
150 -- The AnyBox wild card matches anything
151 cons_match = con1 == con2
155 -- Applications need a bit of care!
156 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
157 -- NB: we've already dealt with type variables and Notes,
158 -- so if one type is an App the other one jolly well better be too
159 uTys ps_ty1 (AppTy s1 t1) ps_ty2 ty2
160 = case splitAppTy_maybe ty2 of
161 Just (s2,t2) -> uTys s1 s1 s2 s2 `thenTc_` uTys t1 t1 t2 t2
162 Nothing -> unifyMisMatch ps_ty1 ps_ty2
164 -- Now the same, but the other way round
165 -- Don't swap the types, because the error messages get worse
166 uTys ps_ty1 ty1 ps_ty2 (AppTy s2 t2)
167 = case splitAppTy_maybe ty1 of
168 Just (s1,t1) -> uTys s1 s1 s2 s2 `thenTc_` uTys t1 t1 t2 t2
169 Nothing -> unifyMisMatch ps_ty1 ps_ty2
171 -- Not expecting for-alls in unification
172 -- ... but the error message from the unifyMisMatch more informative
173 -- than a panic message!
175 -- Anything else fails
176 uTys ps_ty1 ty1 ps_ty2 ty2 = unifyMisMatch ps_ty1 ps_ty2
181 If you are tempted to make a short cut on synonyms, as in this
185 uTys (SynTy con1 args1 ty1) (SynTy con2 args2 ty2)
186 = if (con1 == con2) then
187 -- Good news! Same synonym constructors, so we can shortcut
188 -- by unifying their arguments and ignoring their expansions.
189 unifyTauTypeLists args1 args2
191 -- Never mind. Just expand them and try again
195 then THINK AGAIN. Here is the whole story, as detected and reported
196 by Chris Okasaki \tr{<Chris_Okasaki@loch.mess.cs.cmu.edu>}:
198 Here's a test program that should detect the problem:
202 x = (1 :: Bogus Char) :: Bogus Bool
205 The problem with [the attempted shortcut code] is that
209 is not a sufficient condition to be able to use the shortcut!
210 You also need to know that the type synonym actually USES all
211 its arguments. For example, consider the following type synonym
212 which does not use all its arguments.
217 If you ever tried unifying, say, \tr{Bogus Char} with \tr{Bogus Bool},
218 the unifier would blithely try to unify \tr{Char} with \tr{Bool} and
219 would fail, even though the expanded forms (both \tr{Int}) should
222 Similarly, unifying \tr{Bogus Char} with \tr{Bogus t} would
223 unnecessarily bind \tr{t} to \tr{Char}.
225 ... You could explicitly test for the problem synonyms and mark them
226 somehow as needing expansion, perhaps also issuing a warning to the
231 %************************************************************************
233 \subsection[Unify-uVar]{@uVar@: unifying with a type variable}
235 %************************************************************************
237 @uVar@ is called when at least one of the types being unified is a
238 variable. It does {\em not} assume that the variable is a fixed point
239 of the substitution; rather, notice that @uVar@ (defined below) nips
240 back into @uTys@ if it turns out that the variable is already bound.
243 uVar :: Bool -- False => tyvar is the "expected"
244 -- True => ty is the "expected" thing
246 -> TcTauType -> TcTauType -- printing and real versions
249 uVar swapped tv1 ps_ty2 ty2
250 = tcGetTyVar tv1 `thenNF_Tc` \ maybe_ty1 ->
252 Just ty1 | swapped -> uTys ps_ty2 ty2 ty1 ty1 -- Swap back
253 | otherwise -> uTys ty1 ty1 ps_ty2 ty2 -- Same order
254 other -> uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
256 -- Expand synonyms; ignore FTVs; ignore usage annots
257 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 (NoteTy _ ty2)
258 = uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
261 -- The both-type-variable case
262 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2@(TyVarTy tv2)
264 -- Same type variable => no-op
268 -- Distinct type variables
269 -- ASSERT maybe_ty1 /= Just
271 = tcGetTyVar tv2 `thenNF_Tc` \ maybe_ty2 ->
273 Just ty2' -> uUnboundVar swapped tv1 maybe_ty1 ty2' ty2'
275 Nothing -> checkKinds swapped tv1 ty2 `thenTc_`
277 if tv1 `dominates` tv2 then
278 tcPutTyVar tv2 (TyVarTy tv1) `thenNF_Tc_`
281 ASSERT( isNotUsgTy ps_ty2 )
282 tcPutTyVar tv1 ps_ty2 `thenNF_Tc_`
285 tv1 `dominates` tv2 = isSigTyVar tv1
286 -- Don't unify a signature type variable if poss
287 || varName tv1 `hasBetterProv` varName tv2
288 -- Try to update sys-y type variables in preference to sig-y ones
290 -- Second one isn't a type variable
291 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 non_var_ty2
292 | non_var_ty2 == anyBoxKind
297 = checkKinds swapped tv1 non_var_ty2 `thenTc_`
298 occur_check non_var_ty2 `thenTc_`
299 ASSERT( isNotUsgTy ps_ty2 )
300 checkTcM (not (isSigTyVar tv1))
301 (failWithTcM (unifyWithSigErr tv1 ps_ty2)) `thenTc_`
303 tcPutTyVar tv1 non_var_ty2 `thenNF_Tc_`
304 -- This used to say "ps_ty2" instead of "non_var_ty2"
306 -- But that led to an infinite loop in the type checker!
310 -- f :: (A a -> a -> ()) -> ()
314 -- x = f (\ x p -> p x)
316 -- Here, we try to match "t" with "A t", and succeed
317 -- because the unifier looks through synonyms. The occurs
318 -- check doesn't kick in because we are "really" binding "t" to "()",
319 -- but we *actually* bind "t" to "A t" if we store ps_ty2.
320 -- That leads the typechecker into an infinite loop later.
324 occur_check ty = mapTc occur_check_tv (varSetElems (tyVarsOfType ty)) `thenTc_`
328 | tv1 == tv2 -- Same tyvar; fail
329 = zonkTcType ps_ty2 `thenNF_Tc` \ zonked_ty2 ->
330 failWithTcM (unifyOccurCheck tv1 zonked_ty2)
332 | otherwise -- A different tyvar
333 = tcGetTyVar tv2 `thenNF_Tc` \ maybe_ty2 ->
335 Just ty2' -> occur_check ty2'
338 checkKinds swapped tv1 ty2
339 = tcAddErrCtxtM (unifyKindCtxt swapped tv1 ty2) $
341 -- We have to use tcTypeKind not just typeKind to get the
342 -- kind of ty2, because there might be mutable kind variables
343 -- in the way. For example, suppose that ty2 :: (a b), and
344 -- the kind of 'a' is a kind variable 'k' that has (presumably)
345 -- been unified with 'k1 -> k2'.
346 tcTypeKind ty2 `thenNF_Tc` \ k2 ->
349 unifyKind k2 (tyVarKind tv1)
351 unifyKind (tyVarKind tv1) k2
354 %************************************************************************
356 \subsection[Unify-fun]{@unifyFunTy@}
358 %************************************************************************
360 @unifyFunTy@ is used to avoid the fruitless creation of type variables.
363 unifyFunTy :: TcType -- Fail if ty isn't a function type
364 -> TcM s (TcType, TcType) -- otherwise return arg and result types
366 unifyFunTy ty@(TyVarTy tyvar)
367 = tcGetTyVar tyvar `thenNF_Tc` \ maybe_ty ->
369 Just ty' -> unifyFunTy ty'
370 other -> unify_fun_ty_help ty
373 = case splitFunTy_maybe ty of
374 Just arg_and_res -> returnTc arg_and_res
375 Nothing -> unify_fun_ty_help ty
377 unify_fun_ty_help ty -- Special cases failed, so revert to ordinary unification
378 = newTyVarTy_OpenKind `thenNF_Tc` \ arg ->
379 newTyVarTy_OpenKind `thenNF_Tc` \ res ->
380 unifyTauTy ty (mkFunTy arg res) `thenTc_`
385 unifyListTy :: TcType -- expected list type
386 -> TcM s TcType -- list element type
388 unifyListTy ty@(TyVarTy tyvar)
389 = tcGetTyVar tyvar `thenNF_Tc` \ maybe_ty ->
391 Just ty' -> unifyListTy ty'
392 other -> unify_list_ty_help ty
395 = case splitTyConApp_maybe ty of
396 Just (tycon, [arg_ty]) | tycon == listTyCon -> returnTc arg_ty
397 other -> unify_list_ty_help ty
399 unify_list_ty_help ty -- Revert to ordinary unification
400 = newTyVarTy boxedTypeKind `thenNF_Tc` \ elt_ty ->
401 unifyTauTy ty (mkListTy elt_ty) `thenTc_`
406 unifyTupleTy :: Boxity -> Arity -> TcType -> TcM s [TcType]
407 unifyTupleTy boxity arity ty@(TyVarTy tyvar)
408 = tcGetTyVar tyvar `thenNF_Tc` \ maybe_ty ->
410 Just ty' -> unifyTupleTy boxity arity ty'
411 other -> unify_tuple_ty_help boxity arity ty
413 unifyTupleTy boxity arity ty
414 = case splitTyConApp_maybe ty of
415 Just (tycon, arg_tys)
417 && tyConArity tycon == arity
418 && tupleTyConBoxity tycon == boxity
420 other -> unify_tuple_ty_help boxity arity ty
422 unify_tuple_ty_help boxity arity ty
423 = mapNF_Tc new_tyvar [1..arity] `thenNF_Tc` \ arg_tys ->
424 unifyTauTy ty (mkTupleTy boxity arity arg_tys) `thenTc_`
427 new_tyvar _ | isBoxed boxity = newTyVarTy boxedTypeKind
428 | otherwise = newTyVarTy_OpenKind
431 Make sure a kind is of the form (Type b) for some boxity b.
434 unifyTypeKind :: TcKind -> TcM s ()
435 unifyTypeKind kind@(TyVarTy kv)
436 = tcGetTyVar kv `thenNF_Tc` \ maybe_kind ->
438 Just kind' -> unifyTypeKind kind'
439 Nothing -> unify_type_kind_help kind
442 = case splitTyConApp_maybe kind of
443 Just (tycon, [_]) | tycon == typeCon -> returnTc ()
444 other -> unify_type_kind_help kind
446 unify_type_kind_help kind
447 = newOpenTypeKind `thenNF_Tc` \ expected_kind ->
448 unifyKind expected_kind kind
452 %************************************************************************
454 \subsection[Unify-context]{Errors and contexts}
456 %************************************************************************
462 unifyCtxt s ty1 ty2 tidy_env -- ty1 expected, ty2 inferred
463 = zonkTcType ty1 `thenNF_Tc` \ ty1' ->
464 zonkTcType ty2 `thenNF_Tc` \ ty2' ->
465 returnNF_Tc (err ty1' ty2')
470 text "Expected" <+> text s <> colon <+> ppr tidy_ty1,
471 text "Inferred" <+> text s <> colon <+> ppr tidy_ty2
474 (env1, [tidy_ty1,tidy_ty2]) = tidyOpenTypes tidy_env [ty1,ty2]
476 unifyKindCtxt swapped tv1 ty2 tidy_env -- not swapped => tv1 expected, ty2 inferred
477 = returnNF_Tc (env2, ptext SLIT("When matching types") <+>
478 sep [quotes pp_expected, ptext SLIT("and"), quotes pp_actual])
480 (pp_expected, pp_actual) | swapped = (pp2, pp1)
481 | otherwise = (pp1, pp2)
482 (env1, tv1') = tidyTyVar tidy_env tv1
483 (env2, ty2') = tidyOpenType env1 ty2
487 unifyMisMatch ty1 ty2
488 = zonkTcType ty1 `thenNF_Tc` \ ty1' ->
489 zonkTcType ty2 `thenNF_Tc` \ ty2' ->
491 (env, [tidy_ty1, tidy_ty2]) = tidyOpenTypes emptyTidyEnv [ty1',ty2']
492 msg = hang (ptext SLIT("Couldn't match"))
493 4 (sep [quotes (ppr tidy_ty1),
494 ptext SLIT("against"),
495 quotes (ppr tidy_ty2)])
497 failWithTcM (env, msg)
499 unifyWithSigErr tyvar ty
500 = (env2, hang (ptext SLIT("Cannot unify the type-signature variable") <+> quotes (ppr tidy_tyvar))
501 4 (ptext SLIT("with the type") <+> quotes (ppr tidy_ty)))
503 (env1, tidy_tyvar) = tidyTyVar emptyTidyEnv tyvar
504 (env2, tidy_ty) = tidyOpenType env1 ty
506 unifyOccurCheck tyvar ty
507 = (env2, hang (ptext SLIT("Occurs check: cannot construct the infinite type:"))
508 4 (sep [ppr tidy_tyvar, char '=', ppr tidy_ty]))
510 (env1, tidy_tyvar) = tidyTyVar emptyTidyEnv tyvar
511 (env2, tidy_ty) = tidyOpenType env1 ty