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