ghc/compiler/typecheck/TcUnify.lhs

   1 %
   2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
   3 %
   4 \section[Unify]{Unifier}
   5
   6 The unifier is now squarely in the typechecker monad (because of the
   7 updatable substitution).
   8
   9 \begin{code}
  10 module TcUnify ( unifyTauTy, unifyTauTyList, unifyTauTyLists,
  11                  unifyFunTy, unifyListTy, unifyTupleTy,
  12                  unifyKind, unifyKinds, unifyOpenTypeKind
  13  ) where
  14
  15 #include "HsVersions.h"
  16
  17 -- friends:
  18 import TcMonad
  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
  26                 )
  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
  32                 )
  33 import Name     ( isSystemName )
  34
  35 -- others:
  36 import BasicTypes ( Arity, Boxity, isBoxed )
  37 import TysWiredIn ( listTyCon, mkListTy, mkTupleTy )
  38 import Outputable
  39 \end{code}
  40
  41
  42 %************************************************************************
  43 %*                                                                      *
  44 \subsection{The Kind variants}
  45 %*                                                                      *
  46 %************************************************************************
  47
  48 \begin{code}
  49 unifyKind :: TcKind                 -- Expected
  50           -> TcKind                 -- Actual
  51           -> TcM ()
  52 unifyKind k1 k2
  53   = tcAddErrCtxtM (unifyCtxt "kind" k1 k2) $
  54     uTys k1 k1 k2 k2
  55
  56 unifyKinds :: [TcKind] -> [TcKind] -> TcM ()
  57 unifyKinds []       []       = returnTc ()
  58 unifyKinds (k1:ks1) (k2:ks2) = unifyKind k1 k2  `thenTc_`
  59                                unifyKinds ks1 ks2
  60 unifyKinds _ _ = panic "unifyKinds: length mis-match"
  61 \end{code}
  62
  63 \begin{code}
  64 unifyOpenTypeKind :: TcKind -> TcM ()
  65 -- Ensures that the argument kind is of the form (Type bx)
  66 -- for some boxity bx
  67
  68 unifyOpenTypeKind ty@(TyVarTy tyvar)
  69   = tcGetTyVar tyvar    `thenNF_Tc` \ maybe_ty ->
  70     case maybe_ty of
  71         Just ty' -> unifyOpenTypeKind ty'
  72         other    -> unify_open_kind_help ty
  73
  74 unifyOpenTypeKind ty
  75   = case splitTyConApp_maybe ty of
  76         Just (tycon, [_]) | tycon == typeCon -> returnTc ()
  77         other                                -> unify_open_kind_help ty
  78
  79 unify_open_kind_help ty -- Revert to ordinary unification
  80   = newBoxityVar        `thenNF_Tc` \ boxity ->
  81     unifyKind ty (mkTyConApp typeCon [boxity])
  82 \end{code}
  83
  84
  85 %************************************************************************
  86 %*                                                                      *
  87 \subsection[Unify-exported]{Exported unification functions}
  88 %*                                                                      *
  89 %************************************************************************
  90
  91 The exported functions are all defined as versions of some
  92 non-exported generic functions.
  93
  94 Unify two @TauType@s.  Dead straightforward.
  95
  96 \begin{code}
  97 unifyTauTy :: TcTauType -> TcTauType -> TcM ()
  98 unifyTauTy ty1 ty2      -- ty1 expected, ty2 inferred
  99   = tcAddErrCtxtM (unifyCtxt "type" ty1 ty2) $
 100     uTys ty1 ty1 ty2 ty2
 101 \end{code}
 102
 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.
 107
 108 \begin{code}
 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!"
 114 \end{code}
 115
 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.
 119
 120 \begin{code}
 121 unifyTauTyList :: [TcTauType] -> TcM ()
 122 unifyTauTyList []                = returnTc ()
 123 unifyTauTyList [ty]              = returnTc ()
 124 unifyTauTyList (ty1:tys@(ty2:_)) = unifyTauTy ty1 ty2   `thenTc_`
 125                                    unifyTauTyList tys
 126 \end{code}
 127
 128 %************************************************************************
 129 %*                                                                      *
 130 \subsection[Unify-uTys]{@uTys@: getting down to business}
 131 %*                                                                      *
 132 %************************************************************************
 133
 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.
 139
 140 We call the first one \tr{ps_ty1}, \tr{ps_ty2} for ``possible synomym''.
 141
 142 \begin{code}
 143 uTys :: TcTauType -> TcTauType  -- Error reporting ty1 and real ty1
 144                                 -- ty1 is the *expected* type
 145
 146      -> TcTauType -> TcTauType  -- Error reporting ty2 and real ty2
 147                                 -- ty2 is the *actual* type
 148      -> TcM ()
 149
 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
 154
 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
 158
 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
 163
 164         -- Predicates
 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
 169
 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
 173
 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
 178
 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
 184
 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
 193
 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
 200
 201         -- Not expecting for-alls in unification
 202         -- ... but the error message from the unifyMisMatch more informative
 203         -- than a panic message!
 204
 205         -- Anything else fails
 206 uTys ps_ty1 ty1 ps_ty2 ty2  = unifyMisMatch ps_ty1 ps_ty2
 207 \end{code}
 208
 209 Notes on synonyms
 210 ~~~~~~~~~~~~~~~~~
 211 If you are tempted to make a short cut on synonyms, as in this
 212 pseudocode...
 213
 214 \begin{verbatim}
 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
 220     else
 221         -- Never mind.  Just expand them and try again
 222         uTys ty1 ty2
 223 \end{verbatim}
 224
 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>}:
 227 \begin{quotation}
 228 Here's a test program that should detect the problem:
 229
 230 \begin{verbatim}
 231         type Bogus a = Int
 232         x = (1 :: Bogus Char) :: Bogus Bool
 233 \end{verbatim}
 234
 235 The problem with [the attempted shortcut code] is that
 236 \begin{verbatim}
 237         con1 == con2
 238 \end{verbatim}
 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.
 243 \begin{verbatim}
 244         type Bogus a = Int
 245 \end{verbatim}
 246
 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
 250 match.
 251
 252 Similarly, unifying \tr{Bogus Char} with \tr{Bogus t} would
 253 unnecessarily bind \tr{t} to \tr{Char}.
 254
 255 ... You could explicitly test for the problem synonyms and mark them
 256 somehow as needing expansion, perhaps also issuing a warning to the
 257 user.
 258 \end{quotation}
 259
 260
 261 %************************************************************************
 262 %*                                                                      *
 263 \subsection[Unify-uVar]{@uVar@: unifying with a type variable}
 264 %*                                                                      *
 265 %************************************************************************
 266
 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.
 271
 272 \begin{code}
 273 uVar :: Bool            -- False => tyvar is the "expected"
 274                         -- True  => ty    is the "expected" thing
 275      -> TcTyVar
 276      -> TcTauType -> TcTauType  -- printing and real versions
 277      -> TcM ()
 278
 279 uVar swapped tv1 ps_ty2 ty2
 280   = tcGetTyVar tv1      `thenNF_Tc` \ maybe_ty1 ->
 281     case maybe_ty1 of
 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
 285
 286         -- Expand synonyms; ignore FTVs
 287 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 (NoteTy _ ty2)
 288   = uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
 289
 290
 291         -- The both-type-variable case
 292 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2@(TyVarTy tv2)
 293
 294         -- Same type variable => no-op
 295   | tv1 == tv2
 296   = returnTc ()
 297
 298         -- Distinct type variables
 299         -- ASSERT maybe_ty1 /= Just
 300   | otherwise
 301   = tcGetTyVar tv2      `thenNF_Tc` \ maybe_ty2 ->
 302     case maybe_ty2 of
 303         Just ty2' -> uUnboundVar swapped tv1 maybe_ty1 ty2' ty2'
 304
 305         Nothing | update_tv2
 306
 307                 -> WARN( not (k1 `hasMoreBoxityInfo` k2), (ppr tv1 <+> ppr k1) $$ (ppr tv2 <+> ppr k2) )
 308                    tcPutTyVar tv2 (TyVarTy tv1)         `thenNF_Tc_`
 309                    returnTc ()
 310                 |  otherwise
 311
 312                 -> WARN( not (k2 `hasMoreBoxityInfo` k1), (ppr tv2 <+> ppr k2) $$ (ppr tv1 <+> ppr k1) )
 313                    (tcPutTyVar tv1 ps_ty2               `thenNF_Tc_`
 314                     returnTc ())
 315   where
 316     k1 = tyVarKind tv1
 317     k2 = tyVarKind tv2
 318     update_tv2 = (k2 == openTypeKind) || (k1 /= openTypeKind && nicer_to_update_tv2)
 319                         -- Try to get rid of open type variables as soon as poss
 320
 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
 325
 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_`
 330
 331         -- Check that tv1 isn't a type-signature type variable
 332     checkTcM (not (isSigTyVar tv1))
 333              (failWithTcM (unifyWithSigErr tv1 ps_ty2)) `thenTc_`
 334
 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_`
 339
 340         -- Occurs check
 341         -- Basically we want to update     tv1 := ps_ty2
 342         -- because ps_ty2 has type-synonym info, which improves later error messages
 343         --
 344         -- But consider
 345         --      type A a = ()
 346         --
 347         --      f :: (A a -> a -> ()) -> ()
 348         --      f = \ _ -> ()
 349         --
 350         --      x :: ()
 351         --      x = f (\ x p -> p x)
 352         --
 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).
 358         --
 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_`
 363         returnTc ()
 364     else
 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_`
 370         returnTc ()
 371     else
 372     failWithTcM (unifyOccurCheck tv1 ps_ty2')
 373
 374
 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)       $
 381     unifyMisMatch k1 k2
 382   | otherwise
 383   = returnTc ()
 384   where
 385     (k1,k2) | swapped   = (tk2,tk1)
 386             | otherwise = (tk1,tk2)
 387     tk1 = tyVarKind tv1
 388     tk2 = typeKind ty2
 389 \end{code}
 390
 391
 392 %************************************************************************
 393 %*                                                                      *
 394 \subsection[Unify-fun]{@unifyFunTy@}
 395 %*                                                                      *
 396 %************************************************************************
 397
 398 @unifyFunTy@ is used to avoid the fruitless creation of type variables.
 399
 400 \begin{code}
 401 unifyFunTy :: TcType                            -- Fail if ty isn't a function type
 402            -> TcM (TcType, TcType)      -- otherwise return arg and result types
 403
 404 unifyFunTy ty@(TyVarTy tyvar)
 405   = tcGetTyVar tyvar    `thenNF_Tc` \ maybe_ty ->
 406     case maybe_ty of
 407         Just ty' -> unifyFunTy ty'
 408         other       -> unify_fun_ty_help ty
 409
 410 unifyFunTy ty
 411   = case splitFunTy_maybe ty of
 412         Just arg_and_res -> returnTc arg_and_res
 413         Nothing          -> unify_fun_ty_help ty
 414
 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_`
 419     returnTc (arg,res)
 420 \end{code}
 421
 422 \begin{code}
 423 unifyListTy :: TcType              -- expected list type
 424             -> TcM TcType      -- list element type
 425
 426 unifyListTy ty@(TyVarTy tyvar)
 427   = tcGetTyVar tyvar    `thenNF_Tc` \ maybe_ty ->
 428     case maybe_ty of
 429         Just ty' -> unifyListTy ty'
 430         other       -> unify_list_ty_help ty
 431
 432 unifyListTy ty
 433   = case splitTyConApp_maybe ty of
 434         Just (tycon, [arg_ty]) | tycon == listTyCon -> returnTc arg_ty
 435         other                                       -> unify_list_ty_help ty
 436
 437 unify_list_ty_help ty   -- Revert to ordinary unification
 438   = newTyVarTy liftedTypeKind           `thenNF_Tc` \ elt_ty ->
 439     unifyTauTy ty (mkListTy elt_ty)     `thenTc_`
 440     returnTc elt_ty
 441 \end{code}
 442
 443 \begin{code}
 444 unifyTupleTy :: Boxity -> Arity -> TcType -> TcM [TcType]
 445 unifyTupleTy boxity arity ty@(TyVarTy tyvar)
 446   = tcGetTyVar tyvar    `thenNF_Tc` \ maybe_ty ->
 447     case maybe_ty of
 448         Just ty' -> unifyTupleTy boxity arity ty'
 449         other    -> unify_tuple_ty_help boxity arity ty
 450
 451 unifyTupleTy boxity arity ty
 452   = case splitTyConApp_maybe ty of
 453         Just (tycon, arg_tys)
 454                 |  isTupleTyCon tycon
 455                 && tyConArity tycon == arity
 456                 && tupleTyConBoxity tycon == boxity
 457                 -> returnTc arg_tys
 458         other -> unify_tuple_ty_help boxity arity ty
 459
 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_`
 463     returnTc arg_tys
 464   where
 465     kind | isBoxed boxity = liftedTypeKind
 466          | otherwise      = openTypeKind
 467 \end{code}
 468
 469
 470 %************************************************************************
 471 %*                                                                      *
 472 \subsection[Unify-context]{Errors and contexts}
 473 %*                                                                      *
 474 %************************************************************************
 475
 476 Errors
 477 ~~~~~~
 478
 479 \begin{code}
 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')
 484   where
 485     err ty1 ty2 = (env1,
 486                    nest 4
 487                         (vcat [
 488                            text "Expected" <+> text s <> colon <+> ppr tidy_ty1,
 489                            text "Inferred" <+> text s <> colon <+> ppr tidy_ty2
 490                         ]))
 491                   where
 492                     (env1, [tidy_ty1,tidy_ty2]) = tidyOpenTypes tidy_env [ty1,ty2]
 493
 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')
 498   where
 499     err ty2 = (env2, ptext SLIT("When matching types") <+>
 500                      sep [quotes pp_expected, ptext SLIT("and"), quotes pp_actual])
 501             where
 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
 506               pp1 = ppr tv1'
 507               pp2 = ppr ty2'
 508
 509 unifyMisMatch ty1 ty2
 510   = zonkTcType ty1      `thenNF_Tc` \ ty1' ->
 511     zonkTcType ty2      `thenNF_Tc` \ ty2' ->
 512     let
 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)])
 518     in
 519     failWithTcM (env, msg)
 520
 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)))
 524   where
 525     (env1, tidy_tyvar) = tidyTyVar emptyTidyEnv tyvar
 526     (env2, tidy_ty)    = tidyOpenType  env1     ty
 527
 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]))
 531   where
 532     (env1, tidy_tyvar) = tidyTyVar emptyTidyEnv tyvar
 533     (env2, tidy_ty)    = tidyOpenType  env1     ty
 534 \end{code}
 535