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