compiler/typecheck/TcGadt.lhs

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