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     ( funTyCon, Kind, unboxedTypeKind, boxedTypeKind, openTypeKind,
  21                   superBoxity, typeCon, openKindCon, hasMoreBoxityInfo,
  22                   tyVarsOfType, typeKind,
  23                   mkTyVarTy, mkFunTy, splitFunTy_maybe, splitTyConApp_maybe,
  24                   isNotUsgTy, splitAppTy_maybe, mkTyConApp,
  25                   tidyOpenType, tidyOpenTypes, tidyTyVar
  26                 )
  27 import TyCon    ( TyCon, isTupleTyCon, tupleTyConBoxity, tyConArity )
  28 import Name     ( hasBetterProv )
  29 import Var      ( TyVar, tyVarKind, varName, isSigTyVar )
  30 import VarSet   ( varSetElems )
  31 import TcType   ( TcType, TcTauType, TcTyVar, TcKind, newBoxityVar,
  32                   newTyVarTy, newTyVarTys, tcGetTyVar, tcPutTyVar, zonkTcType
  33                 )
  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 and usage annots)
 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         -- Variables; go for uVar
 156 uTys ps_ty1 (TyVarTy tyvar1) ps_ty2 ty2 = uVar False tyvar1 ps_ty2 ty2
 157 uTys ps_ty1 ty1 ps_ty2 (TyVarTy tyvar2) = uVar True  tyvar2 ps_ty1 ty1
 158                                         -- "True" means args swapped
 159
 160         -- Predicates
 161 uTys _ (PredTy (IParam n1 t1)) _ (PredTy (IParam n2 t2))
 162   | n1 == n2 = uTys t1 t1 t2 t2
 163 uTys _ (PredTy (Class c1 tys1)) _ (PredTy (Class c2 tys2))
 164   | c1 == c2 = unifyTauTyLists tys1 tys2
 165
 166         -- Functions; just check the two parts
 167 uTys _ (FunTy fun1 arg1) _ (FunTy fun2 arg2)
 168   = uTys fun1 fun1 fun2 fun2    `thenTc_`    uTys arg1 arg1 arg2 arg2
 169
 170         -- Type constructors must match
 171 uTys ps_ty1 (TyConApp con1 tys1) ps_ty2 (TyConApp con2 tys2)
 172   | con1 == con2 && length tys1 == length tys2
 173   = unifyTauTyLists tys1 tys2
 174
 175   | con1 == openKindCon
 176         -- When we are doing kind checking, we might match a kind '?'
 177         -- against a kind '*' or '#'.  Notably, CCallable :: ? -> *, and
 178         -- (CCallable Int) and (CCallable Int#) are both OK
 179   = unifyOpenTypeKind ps_ty2
 180
 181         -- Applications need a bit of care!
 182         -- They can match FunTy and TyConApp, so use splitAppTy_maybe
 183         -- NB: we've already dealt with type variables and Notes,
 184         -- so if one type is an App the other one jolly well better be too
 185 uTys ps_ty1 (AppTy s1 t1) ps_ty2 ty2
 186   = case splitAppTy_maybe ty2 of
 187         Just (s2,t2) -> uTys s1 s1 s2 s2        `thenTc_`    uTys t1 t1 t2 t2
 188         Nothing      -> unifyMisMatch ps_ty1 ps_ty2
 189
 190         -- Now the same, but the other way round
 191         -- Don't swap the types, because the error messages get worse
 192 uTys ps_ty1 ty1 ps_ty2 (AppTy s2 t2)
 193   = case splitAppTy_maybe ty1 of
 194         Just (s1,t1) -> uTys s1 s1 s2 s2        `thenTc_`    uTys t1 t1 t2 t2
 195         Nothing      -> unifyMisMatch ps_ty1 ps_ty2
 196
 197         -- Not expecting for-alls in unification
 198         -- ... but the error message from the unifyMisMatch more informative
 199         -- than a panic message!
 200
 201         -- Anything else fails
 202 uTys ps_ty1 ty1 ps_ty2 ty2  = unifyMisMatch ps_ty1 ps_ty2
 203 \end{code}
 204
 205 Notes on synonyms
 206 ~~~~~~~~~~~~~~~~~
 207 If you are tempted to make a short cut on synonyms, as in this
 208 pseudocode...
 209
 210 \begin{verbatim}
 211 uTys (SynTy con1 args1 ty1) (SynTy con2 args2 ty2)
 212   = if (con1 == con2) then
 213         -- Good news!  Same synonym constructors, so we can shortcut
 214         -- by unifying their arguments and ignoring their expansions.
 215         unifyTauTypeLists args1 args2
 216     else
 217         -- Never mind.  Just expand them and try again
 218         uTys ty1 ty2
 219 \end{verbatim}
 220
 221 then THINK AGAIN.  Here is the whole story, as detected and reported
 222 by Chris Okasaki \tr{<Chris_Okasaki@loch.mess.cs.cmu.edu>}:
 223 \begin{quotation}
 224 Here's a test program that should detect the problem:
 225
 226 \begin{verbatim}
 227         type Bogus a = Int
 228         x = (1 :: Bogus Char) :: Bogus Bool
 229 \end{verbatim}
 230
 231 The problem with [the attempted shortcut code] is that
 232 \begin{verbatim}
 233         con1 == con2
 234 \end{verbatim}
 235 is not a sufficient condition to be able to use the shortcut!
 236 You also need to know that the type synonym actually USES all
 237 its arguments.  For example, consider the following type synonym
 238 which does not use all its arguments.
 239 \begin{verbatim}
 240         type Bogus a = Int
 241 \end{verbatim}
 242
 243 If you ever tried unifying, say, \tr{Bogus Char} with \tr{Bogus Bool},
 244 the unifier would blithely try to unify \tr{Char} with \tr{Bool} and
 245 would fail, even though the expanded forms (both \tr{Int}) should
 246 match.
 247
 248 Similarly, unifying \tr{Bogus Char} with \tr{Bogus t} would
 249 unnecessarily bind \tr{t} to \tr{Char}.
 250
 251 ... You could explicitly test for the problem synonyms and mark them
 252 somehow as needing expansion, perhaps also issuing a warning to the
 253 user.
 254 \end{quotation}
 255
 256
 257 %************************************************************************
 258 %*                                                                      *
 259 \subsection[Unify-uVar]{@uVar@: unifying with a type variable}
 260 %*                                                                      *
 261 %************************************************************************
 262
 263 @uVar@ is called when at least one of the types being unified is a
 264 variable.  It does {\em not} assume that the variable is a fixed point
 265 of the substitution; rather, notice that @uVar@ (defined below) nips
 266 back into @uTys@ if it turns out that the variable is already bound.
 267
 268 \begin{code}
 269 uVar :: Bool            -- False => tyvar is the "expected"
 270                         -- True  => ty    is the "expected" thing
 271      -> TcTyVar
 272      -> TcTauType -> TcTauType  -- printing and real versions
 273      -> TcM ()
 274
 275 uVar swapped tv1 ps_ty2 ty2
 276   = tcGetTyVar tv1      `thenNF_Tc` \ maybe_ty1 ->
 277     case maybe_ty1 of
 278         Just ty1 | swapped   -> uTys ps_ty2 ty2 ty1 ty1 -- Swap back
 279                  | otherwise -> uTys ty1 ty1 ps_ty2 ty2 -- Same order
 280         other       -> uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
 281
 282         -- Expand synonyms; ignore FTVs; ignore usage annots
 283 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 (NoteTy _ ty2)
 284   = uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
 285
 286
 287         -- The both-type-variable case
 288 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2@(TyVarTy tv2)
 289
 290         -- Same type variable => no-op
 291   | tv1 == tv2
 292   = returnTc ()
 293
 294         -- Distinct type variables
 295         -- ASSERT maybe_ty1 /= Just
 296   | otherwise
 297   = tcGetTyVar tv2      `thenNF_Tc` \ maybe_ty2 ->
 298     case maybe_ty2 of
 299         Just ty2' -> uUnboundVar swapped tv1 maybe_ty1 ty2' ty2'
 300
 301         Nothing | tv1_dominates_tv2
 302
 303                 -> WARN( not (k1 `hasMoreBoxityInfo` k2), (ppr tv1 <+> ppr k1) $$ (ppr tv2 <+> ppr k2) )
 304                    tcPutTyVar tv2 (TyVarTy tv1)         `thenNF_Tc_`
 305                    returnTc ()
 306                 |  otherwise
 307
 308                 -> WARN( not (k2 `hasMoreBoxityInfo` k1), (ppr tv2 <+> ppr k2) $$ (ppr tv1 <+> ppr k1) )
 309                    (ASSERT( isNotUsgTy ps_ty2 )
 310                     tcPutTyVar tv1 ps_ty2               `thenNF_Tc_`
 311                     returnTc ())
 312   where
 313     k1 = tyVarKind tv1
 314     k2 = tyVarKind tv2
 315     tv1_dominates_tv2 =    isSigTyVar tv1
 316                                 -- Don't unify a signature type variable if poss
 317                         || k2 == openTypeKind
 318                                 -- Try to get rid of open type variables as soon as poss
 319                         || varName tv1 `hasBetterProv` varName tv2
 320                                 -- Try to update sys-y type variables in preference to sig-y ones
 321
 322         -- Second one isn't a type variable
 323 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 non_var_ty2
 324   = checkKinds swapped tv1 non_var_ty2                  `thenTc_`
 325     occur_check non_var_ty2                             `thenTc_`
 326     ASSERT( isNotUsgTy ps_ty2 )
 327     checkTcM (not (isSigTyVar tv1))
 328              (failWithTcM (unifyWithSigErr tv1 ps_ty2)) `thenTc_`
 329
 330     warnTc (not (typeKind non_var_ty2 `hasMoreBoxityInfo` tyVarKind tv1))
 331            ((ppr tv1 <+> ppr (tyVarKind tv1)) $$
 332              (ppr non_var_ty2 <+> ppr (typeKind non_var_ty2)))          `thenNF_Tc_`
 333
 334     tcPutTyVar tv1 non_var_ty2                          `thenNF_Tc_`
 335         -- This used to say "ps_ty2" instead of "non_var_ty2"
 336
 337         -- But that led to an infinite loop in the type checker!
 338         -- Consider
 339         --      type A a = ()
 340         --
 341         --      f :: (A a -> a -> ()) -> ()
 342         --      f = \ _ -> ()
 343         --
 344         --      x :: ()
 345         --      x = f (\ x p -> p x)
 346         --
 347         -- Here, we try to match "t" with "A t", and succeed
 348         -- because the unifier looks through synonyms.  The occurs
 349         -- check doesn't kick in because we are "really" binding "t" to "()",
 350         -- but we *actually* bind "t" to "A t" if we store ps_ty2.
 351         -- That leads the typechecker into an infinite loop later.
 352
 353     returnTc ()
 354   where
 355     occur_check ty = mapTc occur_check_tv (varSetElems (tyVarsOfType ty))       `thenTc_`
 356                      returnTc ()
 357
 358     occur_check_tv tv2
 359        | tv1 == tv2             -- Same tyvar; fail
 360        = zonkTcType ps_ty2      `thenNF_Tc` \ zonked_ty2 ->
 361          failWithTcM (unifyOccurCheck tv1 zonked_ty2)
 362
 363        | otherwise              -- A different tyvar
 364        = tcGetTyVar tv2 `thenNF_Tc` \ maybe_ty2 ->
 365          case maybe_ty2 of
 366                 Just ty2' -> occur_check ty2'
 367                 other     -> returnTc ()
 368
 369 checkKinds swapped tv1 ty2
 370 -- We're about to unify a type variable tv1 with a non-tyvar-type ty2.
 371 -- We need to check that we don't unify a boxed type variable with an
 372 -- unboxed type: e.g.  (id 3#) is illegal
 373   | tk1 == boxedTypeKind && tk2 == unboxedTypeKind
 374   = tcAddErrCtxtM (unifyKindCtxt swapped tv1 ty2)       $
 375     unifyMisMatch k1 k2
 376   | otherwise
 377   = returnTc ()
 378   where
 379     (k1,k2) | swapped   = (tk2,tk1)
 380             | otherwise = (tk1,tk2)
 381     tk1 = tyVarKind tv1
 382     tk2 = typeKind ty2
 383 \end{code}
 384
 385
 386 %************************************************************************
 387 %*                                                                      *
 388 \subsection[Unify-fun]{@unifyFunTy@}
 389 %*                                                                      *
 390 %************************************************************************
 391
 392 @unifyFunTy@ is used to avoid the fruitless creation of type variables.
 393
 394 \begin{code}
 395 unifyFunTy :: TcType                            -- Fail if ty isn't a function type
 396            -> TcM (TcType, TcType)      -- otherwise return arg and result types
 397
 398 unifyFunTy ty@(TyVarTy tyvar)
 399   = tcGetTyVar tyvar    `thenNF_Tc` \ maybe_ty ->
 400     case maybe_ty of
 401         Just ty' -> unifyFunTy ty'
 402         other       -> unify_fun_ty_help ty
 403
 404 unifyFunTy ty
 405   = case splitFunTy_maybe ty of
 406         Just arg_and_res -> returnTc arg_and_res
 407         Nothing          -> unify_fun_ty_help ty
 408
 409 unify_fun_ty_help ty    -- Special cases failed, so revert to ordinary unification
 410   = newTyVarTy openTypeKind     `thenNF_Tc` \ arg ->
 411     newTyVarTy openTypeKind     `thenNF_Tc` \ res ->
 412     unifyTauTy ty (mkFunTy arg res)     `thenTc_`
 413     returnTc (arg,res)
 414 \end{code}
 415
 416 \begin{code}
 417 unifyListTy :: TcType              -- expected list type
 418             -> TcM TcType      -- list element type
 419
 420 unifyListTy ty@(TyVarTy tyvar)
 421   = tcGetTyVar tyvar    `thenNF_Tc` \ maybe_ty ->
 422     case maybe_ty of
 423         Just ty' -> unifyListTy ty'
 424         other       -> unify_list_ty_help ty
 425
 426 unifyListTy ty
 427   = case splitTyConApp_maybe ty of
 428         Just (tycon, [arg_ty]) | tycon == listTyCon -> returnTc arg_ty
 429         other                                       -> unify_list_ty_help ty
 430
 431 unify_list_ty_help ty   -- Revert to ordinary unification
 432   = newTyVarTy boxedTypeKind            `thenNF_Tc` \ elt_ty ->
 433     unifyTauTy ty (mkListTy elt_ty)     `thenTc_`
 434     returnTc elt_ty
 435 \end{code}
 436
 437 \begin{code}
 438 unifyTupleTy :: Boxity -> Arity -> TcType -> TcM [TcType]
 439 unifyTupleTy boxity arity ty@(TyVarTy tyvar)
 440   = tcGetTyVar tyvar    `thenNF_Tc` \ maybe_ty ->
 441     case maybe_ty of
 442         Just ty' -> unifyTupleTy boxity arity ty'
 443         other    -> unify_tuple_ty_help boxity arity ty
 444
 445 unifyTupleTy boxity arity ty
 446   = case splitTyConApp_maybe ty of
 447         Just (tycon, arg_tys)
 448                 |  isTupleTyCon tycon
 449                 && tyConArity tycon == arity
 450                 && tupleTyConBoxity tycon == boxity
 451                 -> returnTc arg_tys
 452         other -> unify_tuple_ty_help boxity arity ty
 453
 454 unify_tuple_ty_help boxity arity ty
 455   = newTyVarTys arity kind                              `thenNF_Tc` \ arg_tys ->
 456     unifyTauTy ty (mkTupleTy boxity arity arg_tys)      `thenTc_`
 457     returnTc arg_tys
 458   where
 459     kind | isBoxed boxity = boxedTypeKind
 460          | otherwise      = openTypeKind
 461 \end{code}
 462
 463
 464 %************************************************************************
 465 %*                                                                      *
 466 \subsection[Unify-context]{Errors and contexts}
 467 %*                                                                      *
 468 %************************************************************************
 469
 470 Errors
 471 ~~~~~~
 472
 473 \begin{code}
 474 unifyCtxt s ty1 ty2 tidy_env    -- ty1 expected, ty2 inferred
 475   = zonkTcType ty1      `thenNF_Tc` \ ty1' ->
 476     zonkTcType ty2      `thenNF_Tc` \ ty2' ->
 477     returnNF_Tc (err ty1' ty2')
 478   where
 479     err ty1 ty2 = (env1,
 480                    nest 4
 481                         (vcat [
 482                            text "Expected" <+> text s <> colon <+> ppr tidy_ty1,
 483                            text "Inferred" <+> text s <> colon <+> ppr tidy_ty2
 484                         ]))
 485                   where
 486                     (env1, [tidy_ty1,tidy_ty2]) = tidyOpenTypes tidy_env [ty1,ty2]
 487
 488 unifyKindCtxt swapped tv1 ty2 tidy_env  -- not swapped => tv1 expected, ty2 inferred
 489         -- tv1 is zonked already
 490   = zonkTcType ty2      `thenNF_Tc` \ ty2' ->
 491     returnNF_Tc (err ty2')
 492   where
 493     err ty2 = (env2, ptext SLIT("When matching types") <+>
 494                      sep [quotes pp_expected, ptext SLIT("and"), quotes pp_actual])
 495             where
 496               (pp_expected, pp_actual) | swapped   = (pp2, pp1)
 497                                        | otherwise = (pp1, pp2)
 498               (env1, tv1') = tidyTyVar tidy_env tv1
 499               (env2, ty2') = tidyOpenType  env1 ty2
 500               pp1 = ppr tv1'
 501               pp2 = ppr ty2'
 502
 503 unifyMisMatch ty1 ty2
 504   = zonkTcType ty1      `thenNF_Tc` \ ty1' ->
 505     zonkTcType ty2      `thenNF_Tc` \ ty2' ->
 506     let
 507         (env, [tidy_ty1, tidy_ty2]) = tidyOpenTypes emptyTidyEnv [ty1',ty2']
 508         msg = hang (ptext SLIT("Couldn't match"))
 509                    4 (sep [quotes (ppr tidy_ty1),
 510                            ptext SLIT("against"),
 511                            quotes (ppr tidy_ty2)])
 512     in
 513     failWithTcM (env, msg)
 514
 515 unifyWithSigErr tyvar ty
 516   = (env2, hang (ptext SLIT("Cannot unify the type-signature variable") <+> quotes (ppr tidy_tyvar))
 517               4 (ptext SLIT("with the type") <+> quotes (ppr tidy_ty)))
 518   where
 519     (env1, tidy_tyvar) = tidyTyVar emptyTidyEnv tyvar
 520     (env2, tidy_ty)    = tidyOpenType  env1     ty
 521
 522 unifyOccurCheck tyvar ty
 523   = (env2, hang (ptext SLIT("Occurs check: cannot construct the infinite type:"))
 524               4 (sep [ppr tidy_tyvar, char '=', ppr tidy_ty]))
 525   where
 526     (env1, tidy_tyvar) = tidyTyVar emptyTidyEnv tyvar
 527     (env2, tidy_ty)    = tidyOpenType  env1     ty
 528 \end{code}
 529