compiler/typecheck/TcGadt.lhs

   1 %
   2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
   3 %
   4
   5 %************************************************************************
   6 %*                                                                      *
   7                 Type refinement for GADTs
   8 %*                                                                      *
   9 %************************************************************************
  10
  11 \begin{code}
  12 module TcGadt (
  13         Refinement, emptyRefinement, gadtRefine,
  14         refineType, refineResType,
  15         dataConCanMatch,
  16         tcUnifyTys, BindFlag(..)
  17   ) where
  18
  19 import HsSyn    ( ExprCoFn(..), idCoercion, isIdCoercion )
  20 import Coercion ( Coercion, mkSymCoercion, mkTransCoercion, mkUnsafeCoercion,
  21                   mkLeftCoercion, mkRightCoercion, mkCoKind, coercionKindPredTy,
  22                   splitCoercionKind, decomposeCo, coercionKind )
  23 import TcType   ( TvSubst(..), TvSubstEnv, substTy, mkTvSubst,
  24                   substTyVar, zipTopTvSubst, typeKind,
  25                   eqKind, isSubKind, repSplitAppTy_maybe,
  26                   tcView, tcGetTyVar_maybe
  27                 )
  28 import Type     ( Type, tyVarsOfType, tyVarsOfTypes, tcEqType, mkTyVarTy )
  29 import TypeRep  ( Type(..), PredType(..) )
  30 import DataCon  ( DataCon, dataConUnivTyVars, dataConEqSpec )
  31 import Var      ( CoVar, TyVar, tyVarKind, varUnique )
  32 import VarEnv
  33 import VarSet
  34 import ErrUtils         ( Message )
  35 import Maybes           ( MaybeErr(..), isJust )
  36 import Control.Monad    ( foldM )
  37 import Outputable
  38 import Unique           ( Unique )
  39 import UniqFM           ( ufmToList )
  40
  41 #include "HsVersions.h"
  42 \end{code}
  43
  44
  45 %************************************************************************
  46 %*                                                                      *
  47                 What a refinement is
  48 %*                                                                      *
  49 %************************************************************************
  50
  51 \begin{code}
  52 data Refinement = Reft InScopeSet InternalReft
  53 -- INVARIANT:   a->(co,ty)   then   co :: (a:=:ty)
  54 -- Not necessarily idemopotent
  55
  56 instance Outputable Refinement where
  57   ppr (Reft in_scope env)
  58     = ptext SLIT("Refinement") <+>
  59         braces (ppr env)
  60
  61 emptyRefinement :: Refinement
  62 emptyRefinement = (Reft emptyInScopeSet emptyVarEnv)
  63
  64
  65 refineType :: Refinement -> Type -> (ExprCoFn, Type)
  66 -- Apply the refinement to the type.
  67 -- If (refineType r ty) = (co, ty')
  68 -- Then co :: ty:=:ty'
  69 refineType (Reft in_scope env) ty
  70   | not (isEmptyVarEnv env),            -- Common case
  71     any (`elemVarEnv` env) (varSetElems (tyVarsOfType ty))
  72   = (ExprCoFn (substTy co_subst ty), substTy tv_subst ty)
  73   | otherwise
  74   = (idCoercion, ty)    -- The type doesn't mention any refined type variables
  75   where
  76     tv_subst = mkTvSubst in_scope (mapVarEnv snd env)
  77     co_subst = mkTvSubst in_scope (mapVarEnv fst env)
  78
  79 refineResType :: Refinement -> Type -> (ExprCoFn, Type)
  80 -- Like refineType, but returns the 'sym' coercion
  81 -- If (refineResType r ty) = (co, ty')
  82 -- Then co :: ty':=:ty
  83 refineResType reft ty
  84   = case refineType reft ty of
  85         (ExprCoFn co, ty1) -> (ExprCoFn (mkSymCoercion co), ty1)
  86         (id_co,       ty1) -> ASSERT( isIdCoercion id_co )
  87                               (idCoercion, ty1)
  88 \end{code}
  89
  90
  91 %************************************************************************
  92 %*                                                                      *
  93                 Generating a type refinement
  94 %*                                                                      *
  95 %************************************************************************
  96
  97 \begin{code}
  98 gadtRefine :: Refinement
  99            -> [TyVar]   -- Bind these by preference
 100            -> [CoVar]
 101            -> MaybeErr Message Refinement
 102 \end{code}
 103
 104 (gadtRefine cvs) takes a list of coercion variables, and returns a
 105 list of coercions, obtained by unifying the types equated by the
 106 incoming coercions.  The returned coercions all have kinds of form
 107 (a:=:ty), where a is a rigid type variable.
 108
 109 Example:
 110   gadtRefine [c :: (a,Int):=:(Bool,b)]
 111   = [ right (left c) :: a:=:Bool,
 112       sym (right c)  :: b:=:Int ]
 113
 114 That is, given evidence 'c' that (a,Int)=(Bool,b), it returns derived
 115 evidence in easy-to-use form.  In particular, given any e::ty, we know
 116 that:
 117         e `cast` ty[right (left c)/a, sym (right c)/b]
 118         :: ty [Bool/a, Int/b]
 119
 120 Two refinements:
 121
 122 - It can fail, if the coercion is unsatisfiable.
 123
 124 - It's biased, by being given a set of type variables to bind
 125   when there is a choice. Example:
 126         MkT :: forall a. a -> T [a]
 127         f :: forall b. T [b] -> b
 128         f x = let v = case x of { MkT y -> y }
 129               in ...
 130   Here we want to bind [a->b], not the other way round, because
 131   in this example the return type is wobbly, and we want the
 132   program to typecheck
 133
 134
 135 -- E.g. (a, Bool, right (left c))
 136 -- INVARIANT: in the triple (tv, ty, co), we have (co :: tv:=:ty)
 137 -- The result is idempotent: the
 138
 139 \begin{code}
 140 gadtRefine (Reft in_scope env1)
 141            ex_tvs co_vars
 142 -- Precondition: fvs( co_vars ) # env1
 143 -- That is, the kinds of the co_vars are a
 144 -- fixed point of the  incoming refinement
 145
 146   = ASSERT2( not $ any (`elemVarEnv` env1) (varSetElems $ tyVarsOfTypes $ map tyVarKind co_vars),
 147              ppr env1 $$ ppr co_vars $$ ppr (map tyVarKind co_vars) )
 148     initUM (tryToBind tv_set) $
 149     do  {       -- Run the unifier, starting with an empty env
 150         ; env2 <- foldM do_one emptyInternalReft co_vars
 151
 152                 -- Find the fixed point of the resulting
 153                 -- non-idempotent substitution
 154         ; let tmp_env = env1 `plusVarEnv` env2
 155               out_env = fixTvCoEnv in_scope' tmp_env
 156         ; WARN( not (null (badReftElts tmp_env)), ppr (badReftElts tmp_env) $$ ppr tmp_env )
 157           WARN( not (null (badReftElts out_env)), ppr (badReftElts out_env) $$ ppr out_env )
 158           return (Reft in_scope' out_env) }
 159   where
 160     tv_set = mkVarSet ex_tvs
 161     in_scope' = foldr extend in_scope co_vars
 162     extend co_var in_scope
 163         = extendInScopeSetSet (extendInScopeSet in_scope co_var)
 164                               (tyVarsOfType (tyVarKind co_var))
 165
 166     do_one reft co_var = unify reft (TyVarTy co_var) ty1 ty2
 167         where
 168            (ty1,ty2) = splitCoercionKind (tyVarKind co_var)
 169 \end{code}
 170
 171 %************************************************************************
 172 %*                                                                      *
 173                 Unification
 174 %*                                                                      *
 175 %************************************************************************
 176
 177 \begin{code}
 178 tcUnifyTys :: (TyVar -> BindFlag)
 179            -> [Type] -> [Type]
 180            -> Maybe TvSubst     -- A regular one-shot substitution
 181 -- The two types may have common type variables, and indeed do so in the
 182 -- second call to tcUnifyTys in FunDeps.checkClsFD
 183 --
 184 -- We implement tcUnifyTys using the evidence-generating 'unify' function
 185 -- in this module, even though we don't need to generate any evidence.
 186 -- This is simply to avoid replicating all all the code for unify
 187 tcUnifyTys bind_fn tys1 tys2
 188   = maybeErrToMaybe $ initUM bind_fn $
 189     do { reft <- unifyList emptyInternalReft cos tys1 tys2
 190
 191         -- Find the fixed point of the resulting non-idempotent substitution
 192         ; let in_scope = mkInScopeSet (tvs1 `unionVarSet` tvs2)
 193               tv_env   = fixTvSubstEnv in_scope (mapVarEnv snd reft)
 194
 195         ; return (mkTvSubst in_scope tv_env) }
 196   where
 197     tvs1 = tyVarsOfTypes tys1
 198     tvs2 = tyVarsOfTypes tys2
 199     cos  = zipWith mkUnsafeCoercion tys1 tys2
 200
 201
 202 ----------------------------
 203 fixTvCoEnv :: InScopeSet -> InternalReft -> InternalReft
 204         -- Find the fixed point of a Refinement
 205         -- (assuming it has no loops!)
 206 fixTvCoEnv in_scope env
 207   = fixpt
 208   where
 209     fixpt         = mapVarEnv step env
 210
 211     step (co, ty) = (co1, ty')
 212       -- Apply fixpt one step:
 213       -- Use refineType to get a substituted type, ty', and a coercion, co_fn,
 214       -- which justifies the substitution.  If the coercion is not the identity
 215       -- then use transitivity with the original coercion
 216       where
 217         (co_fn, ty') = refineType (Reft in_scope fixpt) ty
 218         co1 | ExprCoFn co'' <- co_fn = mkTransCoercion co co''
 219             | otherwise              = ASSERT( isIdCoercion co_fn ) co
 220
 221 -----------------------------
 222 fixTvSubstEnv :: InScopeSet -> TvSubstEnv -> TvSubstEnv
 223 fixTvSubstEnv in_scope env
 224   = fixpt
 225   where
 226     fixpt = mapVarEnv (substTy (mkTvSubst in_scope fixpt)) env
 227
 228 ----------------------------
 229 dataConCanMatch :: DataCon -> [Type] -> Bool
 230 -- Returns True iff the data con can match a scrutinee of type (T tys)
 231 --                  where T is the type constructor for the data con
 232 --
 233 -- Instantiate the equations and try to unify them
 234 dataConCanMatch con tys
 235   = isJust (tcUnifyTys (\tv -> BindMe)
 236                        (map (substTyVar subst . fst) eq_spec)
 237                        (map snd eq_spec))
 238   where
 239     dc_tvs  = dataConUnivTyVars con
 240     eq_spec = dataConEqSpec con
 241     subst   = zipTopTvSubst dc_tvs tys
 242
 243 ----------------------------
 244 tryToBind :: TyVarSet -> TyVar -> BindFlag
 245 tryToBind tv_set tv | tv `elemVarSet` tv_set = BindMe
 246                     | otherwise              = AvoidMe
 247
 248
 249 \end{code}
 250
 251
 252 %************************************************************************
 253 %*                                                                      *
 254                 The workhorse
 255 %*                                                                      *
 256 %************************************************************************
 257
 258 \begin{code}
 259 type InternalReft = TyVarEnv (Coercion, Type)
 260
 261 -- INVARIANT:   a->(co,ty)   then   co :: (a:=:ty)
 262 -- Not necessarily idemopotent
 263
 264 badReftElts :: InternalReft -> [(Unique, (Coercion,Type))]
 265 -- Return the BAD elements of the refinement
 266 -- Should be empty; used in asserions only
 267 badReftElts env
 268   = filter (not . ok) (ufmToList env)
 269   where
 270     ok :: (Unique, (Coercion, Type)) -> Bool
 271     ok (u, (co, ty)) | Just tv <- tcGetTyVar_maybe ty1
 272                      = varUnique tv == u && ty `tcEqType` ty2
 273                      | otherwise = False
 274         where
 275           (ty1,ty2) = coercionKind co
 276
 277 emptyInternalReft :: InternalReft
 278 emptyInternalReft = emptyVarEnv
 279
 280 unify :: InternalReft           -- An existing substitution to extend
 281       -> Coercion       -- Witness of their equality
 282       -> Type -> Type   -- Types to be unified, and witness of their equality
 283       -> UM InternalReft                -- Just the extended substitution,
 284                                 -- Nothing if unification failed
 285 -- We do not require the incoming substitution to be idempotent,
 286 -- nor guarantee that the outgoing one is.  That's fixed up by
 287 -- the wrappers.
 288
 289 -- PRE-CONDITION: in the call (unify r co ty1 ty2), we know that
 290 --                      co :: (ty1:=:ty2)
 291
 292 -- Respects newtypes, PredTypes
 293
 294 unify subst co ty1 ty2 = -- pprTrace "unify" (ppr subst <+> pprParendType ty1 <+> pprParendType ty2) $
 295                          unify_ subst co ty1 ty2
 296
 297 -- in unify_, any NewTcApps/Preds should be taken at face value
 298 unify_ subst co (TyVarTy tv1) ty2  = uVar False subst co tv1 ty2
 299 unify_ subst co ty1 (TyVarTy tv2)  = uVar True  subst co tv2 ty1
 300
 301 unify_ subst co ty1 ty2 | Just ty1' <- tcView ty1 = unify subst co ty1' ty2
 302 unify_ subst co ty1 ty2 | Just ty2' <- tcView ty2 = unify subst co ty1 ty2'
 303
 304 unify_ subst co (PredTy p1) (PredTy p2) = unify_pred subst co p1 p2
 305
 306 unify_ subst co t1@(TyConApp tyc1 tys1) t2@(TyConApp tyc2 tys2)
 307   | tyc1 == tyc2 = unify_tys subst co tys1 tys2
 308
 309 unify_ subst co (FunTy ty1a ty1b) (FunTy ty2a ty2b)
 310   = do  { let [co1,co2] = decomposeCo 2 co
 311         ; subst' <- unify subst co1 ty1a ty2a
 312         ; unify subst' co2 ty1b ty2b }
 313
 314         -- Applications need a bit of care!
 315         -- They can match FunTy and TyConApp, so use splitAppTy_maybe
 316         -- NB: we've already dealt with type variables and Notes,
 317         -- so if one type is an App the other one jolly well better be too
 318 unify_ subst co (AppTy ty1a ty1b) ty2
 319   | Just (ty2a, ty2b) <- repSplitAppTy_maybe ty2
 320   = do  { subst' <- unify subst (mkLeftCoercion co) ty1a ty2a
 321         ; unify subst' (mkRightCoercion co) ty1b ty2b }
 322
 323 unify_ subst co ty1 (AppTy ty2a ty2b)
 324   | Just (ty1a, ty1b) <- repSplitAppTy_maybe ty1
 325   = do  { subst' <- unify subst (mkLeftCoercion co) ty1a ty2a
 326         ; unify subst' (mkRightCoercion co) ty1b ty2b }
 327
 328 unify_ subst co ty1 ty2 = failWith (misMatch ty1 ty2)
 329         -- ForAlls??
 330
 331
 332 ------------------------------
 333 unify_pred subst co (ClassP c1 tys1) (ClassP c2 tys2)
 334   | c1 == c2 = unify_tys subst co tys1 tys2
 335 unify_pred subst co (IParam n1 t1) (IParam n2 t2)
 336   | n1 == n2 = unify subst co t1 t2
 337 unify_pred subst co p1 p2 = failWith (misMatch (PredTy p1) (PredTy p2))
 338
 339 ------------------------------
 340 unify_tys :: InternalReft -> Coercion -> [Type] -> [Type] -> UM InternalReft
 341 unify_tys subst co xs ys
 342   = unifyList subst (decomposeCo (length xs) co) xs ys
 343
 344 unifyList :: InternalReft -> [Coercion] -> [Type] -> [Type] -> UM InternalReft
 345 unifyList subst orig_cos orig_xs orig_ys
 346   = go subst orig_cos orig_xs orig_ys
 347   where
 348     go subst _        []     []     = return subst
 349     go subst (co:cos) (x:xs) (y:ys) = do { subst' <- unify subst co x y
 350                                          ; go subst' cos xs ys }
 351     go subst _ _ _ = failWith (lengthMisMatch orig_xs orig_ys)
 352
 353 ---------------------------------
 354 uVar :: Bool            -- Swapped
 355      -> InternalReft    -- An existing substitution to extend
 356      -> Coercion
 357      -> TyVar           -- Type variable to be unified
 358      -> Type            -- with this type
 359      -> UM InternalReft
 360
 361 -- PRE-CONDITION: in the call (uVar swap r co tv1 ty), we know that
 362 --      if swap=False   co :: (tv1:=:ty)
 363 --      if swap=True    co :: (ty:=:tv1)
 364
 365 uVar swap subst co tv1 ty
 366  = -- Check to see whether tv1 is refined by the substitution
 367    case (lookupVarEnv subst tv1) of
 368
 369      -- Yes, call back into unify'
 370      Just (co',ty')     -- co' :: (tv1:=:ty')
 371         | swap          -- co :: (ty:=:tv1)
 372         -> unify subst (mkTransCoercion co co') ty ty'
 373         | otherwise     -- co :: (tv1:=:ty)
 374         -> unify subst (mkTransCoercion (mkSymCoercion co') co) ty' ty
 375
 376      -- No, continue
 377      Nothing -> uUnrefined subst (if swap then mkSymCoercion co else co)
 378                            tv1 ty ty
 379
 380
 381 uUnrefined :: InternalReft        -- An existing substitution to extend
 382            -> Coercion
 383            -> TyVar               -- Type variable to be unified
 384            -> Type                -- with this type
 385            -> Type                -- (de-noted version)
 386            -> UM InternalReft
 387
 388 -- We know that tv1 isn't refined
 389 -- PRE-CONDITION: in the call (uUnrefined r co tv1 ty2 ty2'), we know that
 390 --      co :: tv1:=:ty2
 391
 392 uUnrefined subst co tv1 ty2 ty2'
 393   | Just ty2'' <- tcView ty2'
 394   = uUnrefined subst co tv1 ty2 ty2''   -- Unwrap synonyms
 395                 -- This is essential, in case we have
 396                 --      type Foo a = a
 397                 -- and then unify a :=: Foo a
 398
 399 uUnrefined subst co tv1 ty2 (TyVarTy tv2)
 400   | tv1 == tv2          -- Same type variable
 401   = return subst
 402
 403     -- Check to see whether tv2 is refined
 404   | Just (co',ty') <- lookupVarEnv subst tv2    -- co' :: tv2:=:ty'
 405   = uUnrefined subst (mkTransCoercion co co') tv1 ty' ty'
 406
 407   -- So both are unrefined; next, see if the kinds force the direction
 408   | eqKind k1 k2        -- Can update either; so check the bind-flags
 409   = do  { b1 <- tvBindFlag tv1
 410         ; b2 <- tvBindFlag tv2
 411         ; case (b1,b2) of
 412             (BindMe, _)          -> bind False tv1 ty2
 413
 414             (AvoidMe, BindMe)    -> bind True tv2 ty1
 415             (AvoidMe, _)         -> bind False tv1 ty2
 416
 417             (WildCard, WildCard) -> return subst
 418             (WildCard, Skolem)   -> return subst
 419             (WildCard, _)        -> bind True tv2 ty1
 420
 421             (Skolem, WildCard)   -> return subst
 422             (Skolem, Skolem)     -> failWith (misMatch ty1 ty2)
 423             (Skolem, _)          -> bind True tv2 ty1
 424         }
 425
 426   | k1 `isSubKind` k2 = bindTv subst (mkSymCoercion co) tv2 ty1 -- Must update tv2
 427   | k2 `isSubKind` k1 = bindTv subst co tv1 ty2 -- Must update tv1
 428
 429   | otherwise = failWith (kindMisMatch tv1 ty2)
 430   where
 431     ty1 = TyVarTy tv1
 432     k1 = tyVarKind tv1
 433     k2 = tyVarKind tv2
 434     bind swap tv ty =
 435         ASSERT2( (coercionKindPredTy co1 `tcEqType` mkCoKind (mkTyVarTy tv) ty)
 436                , (text "Refinement invariant failure: co = " <+> ppr co  <+> ppr (coercionKindPredTy co) $$ text "subst = " <+> ppr tv <+> ppr (mkCoKind (mkTyVarTy tv) ty)))
 437         return (extendVarEnv subst tv (co1,ty))
 438       where
 439         co1 = if swap then mkSymCoercion co else co
 440
 441 uUnrefined subst co tv1 ty2 ty2'        -- ty2 is not a type variable
 442   | tv1 `elemVarSet` substTvSet subst (tyVarsOfType ty2')
 443   = failWith (occursCheck tv1 ty2)      -- Occurs check
 444   | not (k2 `isSubKind` k1)
 445   = failWith (kindMisMatch tv1 ty2)     -- Kind check
 446   | otherwise
 447   = bindTv subst co tv1 ty2             -- Bind tyvar to the synonym if poss
 448   where
 449     k1 = tyVarKind tv1
 450     k2 = typeKind ty2'
 451
 452 substTvSet :: InternalReft -> TyVarSet -> TyVarSet
 453 -- Apply the non-idempotent substitution to a set of type variables,
 454 -- remembering that the substitution isn't necessarily idempotent
 455 substTvSet subst tvs
 456   = foldVarSet (unionVarSet . get) emptyVarSet tvs
 457   where
 458     get tv = case lookupVarEnv subst tv of
 459                 Nothing     -> unitVarSet tv
 460                 Just (_,ty) -> substTvSet subst (tyVarsOfType ty)
 461
 462 bindTv subst co tv ty   -- ty is not a type variable
 463   = ASSERT2( (coercionKindPredTy co `tcEqType` mkCoKind (mkTyVarTy tv) ty),
 464           (text "Refinement invariant failure: co = " <+> ppr co  <+> ppr (coercionKindPredTy co) $$ text "subst = " <+> ppr tv <+> ppr (mkCoKind (mkTyVarTy tv) ty))  )
 465     do  { b <- tvBindFlag tv
 466         ; case b of
 467             Skolem   -> failWith (misMatch (TyVarTy tv) ty)
 468             WildCard -> return subst
 469             other    -> return (extendVarEnv subst tv (co,ty))
 470         }
 471 \end{code}
 472
 473 %************************************************************************
 474 %*                                                                      *
 475                 Unification monad
 476 %*                                                                      *
 477 %************************************************************************
 478
 479 \begin{code}
 480 data BindFlag
 481   = BindMe      -- A regular type variable
 482   | AvoidMe     -- Like BindMe but, given the choice, avoid binding it
 483
 484   | Skolem      -- This type variable is a skolem constant
 485                 -- Don't bind it; it only matches itself
 486
 487   | WildCard    -- This type variable matches anything,
 488                 -- and does not affect the substitution
 489
 490 newtype UM a = UM { unUM :: (TyVar -> BindFlag)
 491                          -> MaybeErr Message a }
 492
 493 instance Monad UM where
 494   return a = UM (\tvs -> Succeeded a)
 495   fail s   = UM (\tvs -> Failed (text s))
 496   m >>= k  = UM (\tvs -> case unUM m tvs of
 497                            Failed err -> Failed err
 498                            Succeeded v  -> unUM (k v) tvs)
 499
 500 initUM :: (TyVar -> BindFlag) -> UM a -> MaybeErr Message a
 501 initUM badtvs um = unUM um badtvs
 502
 503 tvBindFlag :: TyVar -> UM BindFlag
 504 tvBindFlag tv = UM (\tv_fn -> Succeeded (tv_fn tv))
 505
 506 failWith :: Message -> UM a
 507 failWith msg = UM (\tv_fn -> Failed msg)
 508
 509 maybeErrToMaybe :: MaybeErr fail succ -> Maybe succ
 510 maybeErrToMaybe (Succeeded a) = Just a
 511 maybeErrToMaybe (Failed m)    = Nothing
 512 \end{code}
 513
 514
 515 %************************************************************************
 516 %*                                                                      *
 517                 Error reporting
 518         We go to a lot more trouble to tidy the types
 519         in TcUnify.  Maybe we'll end up having to do that
 520         here too, but I'll leave it for now.
 521 %*                                                                      *
 522 %************************************************************************
 523
 524 \begin{code}
 525 misMatch t1 t2
 526   = ptext SLIT("Can't match types") <+> quotes (ppr t1) <+>
 527     ptext SLIT("and") <+> quotes (ppr t2)
 528
 529 lengthMisMatch tys1 tys2
 530   = sep [ptext SLIT("Can't match unequal length lists"),
 531          nest 2 (ppr tys1), nest 2 (ppr tys2) ]
 532
 533 kindMisMatch tv1 t2
 534   = vcat [ptext SLIT("Can't match kinds") <+> quotes (ppr (tyVarKind tv1)) <+>
 535             ptext SLIT("and") <+> quotes (ppr (typeKind t2)),
 536           ptext SLIT("when matching") <+> quotes (ppr tv1) <+>
 537                 ptext SLIT("with") <+> quotes (ppr t2)]
 538
 539 occursCheck tv ty
 540   = hang (ptext SLIT("Can't construct the infinite type"))
 541        2 (ppr tv <+> equals <+> ppr ty)
 542 \end{code}