ghc/compiler/types/Type.lhs

   1 %
   2 % (c) The GRASP/AQUA Project, Glasgow University, 1998
   3 %
   4 \section[Type]{Type}
   5
   6 \begin{code}
   7 module Type (
   8         Type(..), TyNote(..), UsageAnn(..),             -- Representation visible to friends
   9         Kind, TyVarSubst,
  10
  11         superKind, superBoxity,                         -- :: SuperKind
  12
  13         boxedKind,                                      -- :: Kind :: BX
  14         anyBoxKind,                                     -- :: Kind :: BX
  15         typeCon,                                        -- :: KindCon :: BX -> KX
  16         anyBoxCon,                                      -- :: KindCon :: BX
  17
  18         boxedTypeKind, unboxedTypeKind, openTypeKind,   -- Kind :: superKind
  19
  20         mkArrowKind, mkArrowKinds, hasMoreBoxityInfo,
  21
  22         funTyCon,
  23
  24         mkTyVarTy, mkTyVarTys, getTyVar, getTyVar_maybe, isTyVarTy,
  25
  26         mkAppTy, mkAppTys, splitAppTy, splitAppTys, splitAppTy_maybe,
  27
  28         mkFunTy, mkFunTys, splitFunTy_maybe, splitFunTys, funResultTy,
  29         zipFunTys,
  30
  31         mkTyConApp, mkTyConTy, splitTyConApp_maybe,
  32         splitAlgTyConApp_maybe, splitAlgTyConApp,
  33         mkDictTy, splitDictTy_maybe, isDictTy,
  34
  35         mkSynTy, isSynTy, deNoteType,
  36
  37         mkUsgTy, isUsgTy{- dont use -}, isNotUsgTy, splitUsgTy, unUsgTy, tyUsg,
  38
  39         mkForAllTy, mkForAllTys, splitForAllTy_maybe, splitForAllTys,
  40         applyTy, applyTys, isForAllTy,
  41         mkPiType,
  42
  43         TauType, RhoType, SigmaType, ThetaType,
  44         isTauTy,
  45         mkRhoTy, splitRhoTy,
  46         mkSigmaTy, splitSigmaTy,
  47
  48         -- Lifting and boxity
  49         isUnLiftedType, isUnboxedType, isUnboxedTupleType, isAlgType, isDataType,
  50         typePrimRep,
  51
  52         -- Free variables
  53         tyVarsOfType, tyVarsOfTypes, namesOfType, typeKind,
  54         addFreeTyVars,
  55
  56         -- Substitution
  57         substTy, substTheta, fullSubstTy, substTyVar,
  58         substTopTy, substTopTheta,
  59
  60         -- Tidying up for printing
  61         tidyType,     tidyTypes,
  62         tidyOpenType, tidyOpenTypes,
  63         tidyTyVar,    tidyTyVars,
  64         tidyTopType
  65     ) where
  66
  67 #include "HsVersions.h"
  68
  69 import {-# SOURCE #-}   DataCon( DataCon )
  70 import {-# SOURCE #-}   PprType( pprType )      -- Only called in debug messages
  71
  72 -- friends:
  73 import Var      ( Id, TyVar, IdOrTyVar, UVar,
  74                   tyVarKind, tyVarName, isId, idType, setTyVarName, setVarOcc
  75                 )
  76 import VarEnv
  77 import VarSet
  78
  79 import Name     ( NamedThing(..), Provenance(..), ExportFlag(..),
  80                   mkWiredInTyConName, mkGlobalName, mkLocalName, mkKindOccFS, tcName,
  81                   tidyOccName, TidyOccEnv
  82                 )
  83 import NameSet
  84 import Class    ( classTyCon, Class )
  85 import TyCon    ( TyCon, KindCon,
  86                   mkFunTyCon, mkKindCon, mkSuperKindCon,
  87                   matchesTyCon, isUnboxedTupleTyCon, isUnLiftedTyCon,
  88                   isFunTyCon, isDataTyCon,
  89                   isAlgTyCon, isSynTyCon, tyConArity,
  90                   tyConKind, tyConDataCons, getSynTyConDefn,
  91                   tyConPrimRep, tyConClass_maybe
  92                 )
  93
  94 -- others
  95 import BasicTypes       ( Unused )
  96 import SrcLoc           ( mkBuiltinSrcLoc, noSrcLoc )
  97 import PrelMods         ( pREL_GHC )
  98 import Maybes           ( maybeToBool )
  99 import PrimRep          ( PrimRep(..), isFollowableRep )
 100 import Unique           -- quite a few *Keys
 101 import Util             ( thenCmp, mapAccumL, seqList, ($!) )
 102 import Outputable
 103
 104 \end{code}
 105
 106 %************************************************************************
 107 %*                                                                      *
 108 \subsection{Type Classifications}
 109 %*                                                                      *
 110 %************************************************************************
 111
 112 A type is
 113
 114         *unboxed*       iff its representation is other than a pointer
 115                         Unboxed types cannot instantiate a type variable.
 116                         Unboxed types are always unlifted.
 117
 118         *lifted*        A type is lifted iff it has bottom as an element.
 119                         Closures always have lifted types:  i.e. any
 120                         let-bound identifier in Core must have a lifted
 121                         type.  Operationally, a lifted object is one that
 122                         can be entered.
 123                         (NOTE: previously "pointed").
 124
 125         *algebraic*     A type with one or more constructors, whether declared
 126                         with "data" or "newtype".
 127                         An algebraic type is one that can be deconstructed
 128                         with a case expression.
 129                         *NOT* the same as lifted types,  because we also
 130                         include unboxed tuples in this classification.
 131
 132         *data*          A type declared with "data".  Also boxed tuples.
 133
 134         *primitive*     iff it is a built-in type that can't be expressed
 135                         in Haskell.
 136
 137 Currently, all primitive types are unlifted, but that's not necessarily
 138 the case.  (E.g. Int could be primitive.)
 139
 140 Some primitive types are unboxed, such as Int#, whereas some are boxed
 141 but unlifted (such as ByteArray#).  The only primitive types that we
 142 classify as algebraic are the unboxed tuples.
 143
 144 examples of type classifications:
 145
 146 Type            primitive       boxed           lifted          algebraic
 147 -----------------------------------------------------------------------------
 148 Int#,           Yes             No              No              No
 149 ByteArray#      Yes             Yes             No              No
 150 (# a, b #)      Yes             No              No              Yes
 151 (  a, b  )      No              Yes             Yes             Yes
 152 [a]             No              Yes             Yes             Yes
 153
 154 %************************************************************************
 155 %*                                                                      *
 156 \subsection{The data type}
 157 %*                                                                      *
 158 %************************************************************************
 159
 160
 161 \begin{code}
 162 type SuperKind = Type
 163 type Kind      = Type
 164
 165 type TyVarSubst          = TyVarEnv Type
 166
 167 data Type
 168   = TyVarTy TyVar
 169
 170   | AppTy
 171         Type            -- Function is *not* a TyConApp
 172         Type
 173
 174   | TyConApp                    -- Application of a TyCon
 175         TyCon                   -- *Invariant* saturated appliations of FunTyCon and
 176                                 --      synonyms have their own constructors, below.
 177         [Type]          -- Might not be saturated.
 178
 179   | FunTy                       -- Special case of TyConApp: TyConApp FunTyCon [t1,t2]
 180         Type
 181         Type
 182
 183   | NoteTy                      -- Saturated application of a type synonym
 184         TyNote
 185         Type            -- The expanded version
 186
 187   | ForAllTy
 188         TyVar
 189         Type            -- TypeKind
 190
 191 data TyNote
 192   = SynNote Type        -- The unexpanded version of the type synonym; always a TyConApp
 193   | FTVNote TyVarSet    -- The free type variables of the noted expression
 194   | UsgNote UsageAnn    -- The usage annotation at this node
 195
 196 data UsageAnn
 197   = UsOnce              -- Used at most once
 198   | UsMany              -- Used possibly many times (no info; this annotation can be omitted)
 199   | UsVar UVar          -- Annotation is variable (should only happen inside analysis)
 200 \end{code}
 201
 202
 203 %************************************************************************
 204 %*                                                                      *
 205 \subsection{Kinds}
 206 %*                                                                      *
 207 %************************************************************************
 208
 209 Kinds
 210 ~~~~~
 211 k::K = Type bx
 212      | k -> k
 213      | kv
 214
 215 kv :: KX is a kind variable
 216
 217 Type :: BX -> KX
 218
 219 bx::BX = Boxed
 220       |  Unboxed
 221       |  AnyBox         -- Used *only* for special built-in things
 222                         -- like error :: forall (a::*?). String -> a
 223                         -- Here, the 'a' can be instantiated to a boxed or
 224                         -- unboxed type.
 225       |  bv
 226
 227 bxv :: BX is a boxity variable
 228
 229 sk = KX         -- A kind
 230    | BX         -- A boxity
 231    | sk -> sk   -- In ptic (BX -> KX)
 232
 233 \begin{code}
 234 mk_kind_name key str = mkGlobalName key pREL_GHC (mkKindOccFS tcName str)
 235                                     (LocalDef mkBuiltinSrcLoc NotExported)
 236         -- mk_kind_name is a bit of a hack
 237         -- The LocalDef means that we print the name without
 238         -- a qualifier, which is what we want for these kinds.
 239         -- It's used for both Kinds and Boxities
 240 \end{code}
 241
 242 Define KX, BX.
 243
 244 \begin{code}
 245 superKind :: SuperKind          -- KX, the type of all kinds
 246 superKindName = mk_kind_name kindConKey SLIT("KX")
 247 superKind = TyConApp (mkSuperKindCon superKindName) []
 248
 249 superBoxity :: SuperKind                -- BX, the type of all boxities
 250 superBoxityName = mk_kind_name boxityConKey SLIT("BX")
 251 superBoxity = TyConApp (mkSuperKindCon superBoxityName) []
 252 \end{code}
 253
 254 Define Boxed, Unboxed, AnyBox
 255
 256 \begin{code}
 257 boxedKind, unboxedKind, anyBoxKind :: Kind      -- Of superkind superBoxity
 258
 259 boxedConName = mk_kind_name boxedConKey SLIT("*")
 260 boxedKind    = TyConApp (mkKindCon boxedConName superBoxity) []
 261
 262 unboxedConName = mk_kind_name unboxedConKey SLIT("#")
 263 unboxedKind    = TyConApp (mkKindCon unboxedConName superBoxity) []
 264
 265 anyBoxConName = mk_kind_name anyBoxConKey SLIT("?")
 266 anyBoxCon     = mkKindCon anyBoxConName superBoxity     -- A kind of wild card
 267 anyBoxKind    = TyConApp anyBoxCon []
 268 \end{code}
 269
 270 Define Type
 271
 272 \begin{code}
 273 typeCon :: KindCon
 274 typeConName = mk_kind_name typeConKey SLIT("Type")
 275 typeCon     = mkKindCon typeConName (superBoxity `FunTy` superKind)
 276 \end{code}
 277
 278 Define (Type Boxed), (Type Unboxed), (Type AnyBox)
 279
 280 \begin{code}
 281 boxedTypeKind, unboxedTypeKind, openTypeKind :: Kind
 282 boxedTypeKind   = TyConApp typeCon [boxedKind]
 283 unboxedTypeKind = TyConApp typeCon [unboxedKind]
 284 openTypeKind    = TyConApp typeCon [anyBoxKind]
 285
 286 mkArrowKind :: Kind -> Kind -> Kind
 287 mkArrowKind k1 k2 = k1 `FunTy` k2
 288
 289 mkArrowKinds :: [Kind] -> Kind -> Kind
 290 mkArrowKinds arg_kinds result_kind = foldr mkArrowKind result_kind arg_kinds
 291 \end{code}
 292
 293 \begin{code}
 294 hasMoreBoxityInfo :: Kind -> Kind -> Bool
 295 hasMoreBoxityInfo k1 k2
 296   | k2 == openTypeKind = ASSERT( is_type_kind k1) True
 297   | otherwise          = k1 == k2
 298   where
 299         -- Returns true for things of form (Type x)
 300     is_type_kind k = case splitTyConApp_maybe k of
 301                         Just (tc,[_]) -> tc == typeCon
 302                         Nothing       -> False
 303 \end{code}
 304
 305
 306 %************************************************************************
 307 %*                                                                      *
 308 \subsection{Wired-in type constructors
 309 %*                                                                      *
 310 %************************************************************************
 311
 312 We define a few wired-in type constructors here to avoid module knots
 313
 314 \begin{code}
 315 funTyConName = mkWiredInTyConName funTyConKey pREL_GHC SLIT("(->)") funTyCon
 316 funTyCon = mkFunTyCon funTyConName (mkArrowKinds [boxedTypeKind, boxedTypeKind] boxedTypeKind)
 317 \end{code}
 318
 319
 320
 321 %************************************************************************
 322 %*                                                                      *
 323 \subsection{Constructor-specific functions}
 324 %*                                                                      *
 325 %************************************************************************
 326
 327
 328 ---------------------------------------------------------------------
 329                                 TyVarTy
 330                                 ~~~~~~~
 331 \begin{code}
 332 mkTyVarTy  :: TyVar   -> Type
 333 mkTyVarTy  = TyVarTy
 334
 335 mkTyVarTys :: [TyVar] -> [Type]
 336 mkTyVarTys = map mkTyVarTy -- a common use of mkTyVarTy
 337
 338 getTyVar :: String -> Type -> TyVar
 339 getTyVar msg (TyVarTy tv) = tv
 340 getTyVar msg (NoteTy _ t) = getTyVar msg t
 341 getTyVar msg other        = panic ("getTyVar: " ++ msg)
 342
 343 getTyVar_maybe :: Type -> Maybe TyVar
 344 getTyVar_maybe (TyVarTy tv) = Just tv
 345 getTyVar_maybe (NoteTy _ t) = getTyVar_maybe t
 346 getTyVar_maybe other        = Nothing
 347
 348 isTyVarTy :: Type -> Bool
 349 isTyVarTy (TyVarTy tv)  = True
 350 isTyVarTy (NoteTy _ ty) = isTyVarTy ty
 351 isTyVarTy other         = False
 352 \end{code}
 353
 354
 355 ---------------------------------------------------------------------
 356                                 AppTy
 357                                 ~~~~~
 358 We need to be pretty careful with AppTy to make sure we obey the
 359 invariant that a TyConApp is always visibly so.  mkAppTy maintains the
 360 invariant: use it.
 361
 362 \begin{code}
 363 mkAppTy orig_ty1 orig_ty2 = ASSERT2( isNotUsgTy orig_ty1 && isNotUsgTy orig_ty2, pprType orig_ty1 <+> text "to" <+> pprType orig_ty2 )
 364                             mk_app orig_ty1
 365   where
 366     mk_app (NoteTy _ ty1)    = mk_app ty1
 367     mk_app (TyConApp tc tys) = mkTyConApp tc (tys ++ [orig_ty2])
 368     mk_app ty1               = AppTy orig_ty1 orig_ty2
 369
 370 mkAppTys :: Type -> [Type] -> Type
 371 mkAppTys orig_ty1 []        = orig_ty1
 372         -- This check for an empty list of type arguments
 373         -- avoids the needless of a type synonym constructor.
 374         -- For example: mkAppTys Rational []
 375         --   returns to (Ratio Integer), which has needlessly lost
 376         --   the Rational part.
 377 mkAppTys orig_ty1 orig_tys2 = ASSERT2( isNotUsgTy orig_ty1, pprType orig_ty1 )
 378                               mk_app orig_ty1
 379   where
 380     mk_app (NoteTy _ ty1)    = mk_app ty1
 381     mk_app (TyConApp tc tys) = mkTyConApp tc (tys ++ orig_tys2)
 382     mk_app ty1               = ASSERT2( all isNotUsgTy orig_tys2, pprType orig_ty1 <+> text "to" <+> hsep (map pprType orig_tys2) )
 383                                foldl AppTy orig_ty1 orig_tys2
 384
 385 splitAppTy_maybe :: Type -> Maybe (Type, Type)
 386 splitAppTy_maybe (FunTy ty1 ty2)   = Just (TyConApp funTyCon [ty1], ty2)
 387 splitAppTy_maybe (AppTy ty1 ty2)   = Just (ty1, ty2)
 388 splitAppTy_maybe (NoteTy _ ty)     = splitAppTy_maybe ty
 389 splitAppTy_maybe (TyConApp tc [])  = Nothing
 390 splitAppTy_maybe (TyConApp tc tys) = split tys []
 391                             where
 392                                split [ty2]    acc = Just (TyConApp tc (reverse acc), ty2)
 393                                split (ty:tys) acc = split tys (ty:acc)
 394
 395 splitAppTy_maybe other            = Nothing
 396
 397 splitAppTy :: Type -> (Type, Type)
 398 splitAppTy ty = case splitAppTy_maybe ty of
 399                         Just pr -> pr
 400                         Nothing -> panic "splitAppTy"
 401
 402 splitAppTys :: Type -> (Type, [Type])
 403 splitAppTys ty = split ty ty []
 404   where
 405     split orig_ty (AppTy ty arg)        args = split ty ty (arg:args)
 406     split orig_ty (NoteTy _ ty)         args = split orig_ty ty args
 407     split orig_ty (FunTy ty1 ty2)       args = ASSERT( null args )
 408                                                (TyConApp funTyCon [], [ty1,ty2])
 409     split orig_ty (TyConApp tc tc_args) args = (TyConApp tc [], tc_args ++ args)
 410     split orig_ty ty                    args = (orig_ty, args)
 411 \end{code}
 412
 413
 414 ---------------------------------------------------------------------
 415                                 FunTy
 416                                 ~~~~~
 417
 418 \begin{code}
 419 mkFunTy :: Type -> Type -> Type
 420 mkFunTy arg res = FunTy arg res
 421
 422 mkFunTys :: [Type] -> Type -> Type
 423 mkFunTys tys ty = foldr FunTy ty tys
 424
 425 splitFunTy_maybe :: Type -> Maybe (Type, Type)
 426 splitFunTy_maybe (FunTy arg res) = Just (arg, res)
 427 splitFunTy_maybe (NoteTy _ ty)   = splitFunTy_maybe ty
 428 splitFunTy_maybe other           = Nothing
 429
 430
 431 splitFunTys :: Type -> ([Type], Type)
 432 splitFunTys ty = split [] ty ty
 433   where
 434     split args orig_ty (FunTy arg res) = split (arg:args) res res
 435     split args orig_ty (NoteTy _ ty)   = split args orig_ty ty
 436     split args orig_ty ty              = (reverse args, orig_ty)
 437
 438 zipFunTys :: Outputable a => [a] -> Type -> ([(a,Type)], Type)
 439 zipFunTys orig_xs orig_ty = split [] orig_xs orig_ty orig_ty
 440   where
 441     split acc []     nty ty              = (reverse acc, nty)
 442     split acc (x:xs) nty (FunTy arg res) = split ((x,arg):acc) xs res res
 443     split acc xs     nty (NoteTy _ ty)   = split acc           xs nty ty
 444     split acc (x:xs) nty ty              = pprPanic "zipFunTys" (ppr orig_xs <+> pprType orig_ty)
 445
 446 funResultTy :: Type -> Type
 447 funResultTy (FunTy arg res) = res
 448 funResultTy (NoteTy _ ty)   = funResultTy ty
 449 funResultTy ty              = pprPanic "funResultTy" (pprType ty)
 450 \end{code}
 451
 452
 453 ---------------------------------------------------------------------
 454                                 TyConApp
 455                                 ~~~~~~~~
 456
 457 \begin{code}
 458 mkTyConApp :: TyCon -> [Type] -> Type
 459 mkTyConApp tycon tys
 460   | isFunTyCon tycon && length tys == 2
 461   = case tys of
 462         (ty1:ty2:_) -> FunTy ty1 ty2
 463
 464   | otherwise
 465   = ASSERT(not (isSynTyCon tycon))
 466     TyConApp tycon tys
 467
 468 mkTyConTy :: TyCon -> Type
 469 mkTyConTy tycon = ASSERT( not (isSynTyCon tycon) )
 470                   TyConApp tycon []
 471
 472 -- splitTyConApp "looks through" synonyms, because they don't
 473 -- mean a distinct type, but all other type-constructor applications
 474 -- including functions are returned as Just ..
 475
 476 splitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
 477 splitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
 478 splitTyConApp_maybe (FunTy arg res)   = Just (funTyCon, [arg,res])
 479 splitTyConApp_maybe (NoteTy _ ty)     = splitTyConApp_maybe ty
 480 splitTyConApp_maybe other             = Nothing
 481
 482 -- splitAlgTyConApp_maybe looks for
 483 --      *saturated* applications of *algebraic* data types
 484 -- "Algebraic" => newtype, data type, or dictionary (not function types)
 485 -- We return the constructors too.
 486
 487 splitAlgTyConApp_maybe :: Type -> Maybe (TyCon, [Type], [DataCon])
 488 splitAlgTyConApp_maybe (TyConApp tc tys)
 489   | isAlgTyCon tc &&
 490     tyConArity tc == length tys      = Just (tc, tys, tyConDataCons tc)
 491 splitAlgTyConApp_maybe (NoteTy _ ty) = splitAlgTyConApp_maybe ty
 492 splitAlgTyConApp_maybe other         = Nothing
 493
 494 splitAlgTyConApp :: Type -> (TyCon, [Type], [DataCon])
 495         -- Here the "algebraic" property is an *assertion*
 496 splitAlgTyConApp (TyConApp tc tys) = ASSERT( isAlgTyCon tc && tyConArity tc == length tys )
 497                                      (tc, tys, tyConDataCons tc)
 498 splitAlgTyConApp (NoteTy _ ty)     = splitAlgTyConApp ty
 499 \end{code}
 500
 501 "Dictionary" types are just ordinary data types, but you can
 502 tell from the type constructor whether it's a dictionary or not.
 503
 504 \begin{code}
 505 mkDictTy :: Class -> [Type] -> Type
 506 mkDictTy clas tys = TyConApp (classTyCon clas) tys
 507
 508 splitDictTy_maybe :: Type -> Maybe (Class, [Type])
 509 splitDictTy_maybe (TyConApp tc tys)
 510   |  maybeToBool maybe_class
 511   && tyConArity tc == length tys = Just (clas, tys)
 512   where
 513      maybe_class = tyConClass_maybe tc
 514      Just clas   = maybe_class
 515
 516 splitDictTy_maybe (NoteTy _ ty) = splitDictTy_maybe ty
 517 splitDictTy_maybe other         = Nothing
 518
 519 isDictTy :: Type -> Bool
 520         -- This version is slightly more efficient than (maybeToBool . splitDictTy)
 521 isDictTy (TyConApp tc tys)
 522   |  maybeToBool (tyConClass_maybe tc)
 523   && tyConArity tc == length tys
 524   = True
 525 isDictTy (NoteTy _ ty)  = isDictTy ty
 526 isDictTy other          = False
 527 \end{code}
 528
 529
 530 ---------------------------------------------------------------------
 531                                 SynTy
 532                                 ~~~~~
 533
 534 \begin{code}
 535 mkSynTy syn_tycon tys
 536   = ASSERT( isSynTyCon syn_tycon )
 537     ASSERT( isNotUsgTy body )
 538     NoteTy (SynNote (TyConApp syn_tycon tys))
 539            (substTopTy (zipVarEnv tyvars tys) body)
 540   where
 541     (tyvars, body) = getSynTyConDefn syn_tycon
 542
 543 isSynTy (NoteTy (SynNote _) _) = True
 544 isSynTy other                  = False
 545
 546 deNoteType :: Type -> Type
 547         -- Sorry for the cute name
 548 deNoteType ty@(TyVarTy tyvar)   = ty
 549 deNoteType (TyConApp tycon tys) = TyConApp tycon (map deNoteType tys)
 550 deNoteType (NoteTy _ ty)        = deNoteType ty
 551 deNoteType (AppTy fun arg)      = AppTy (deNoteType fun) (deNoteType arg)
 552 deNoteType (FunTy fun arg)      = FunTy (deNoteType fun) (deNoteType arg)
 553 deNoteType (ForAllTy tv ty)     = ForAllTy tv (deNoteType ty)
 554 \end{code}
 555
 556 Notes on type synonyms
 557 ~~~~~~~~~~~~~~~~~~~~~~
 558 The various "split" functions (splitFunTy, splitRhoTy, splitForAllTy) try
 559 to return type synonyms whereever possible. Thus
 560
 561         type Foo a = a -> a
 562
 563 we want
 564         splitFunTys (a -> Foo a) = ([a], Foo a)
 565 not                                ([a], a -> a)
 566
 567 The reason is that we then get better (shorter) type signatures in
 568 interfaces.  Notably this plays a role in tcTySigs in TcBinds.lhs.
 569
 570
 571
 572
 573 ---------------------------------------------------------------------
 574                                 UsgNote
 575                                 ~~~~~~~
 576
 577 NB: Invariant: if present, usage note is at the very top of the type.
 578 This should be carefully preserved.
 579
 580 In some parts of the compiler, comments use the _Once Upon a
 581 Polymorphic Type_ (POPL'99) usage of "sigma = usage-annotated type;
 582 tau = un-usage-annotated type"; unfortunately this conflicts with the
 583 rho/tau/theta/sigma usage in the rest of the compiler.
 584 (KSW 1999-04)
 585
 586 \begin{code}
 587 mkUsgTy :: UsageAnn -> Type -> Type
 588 #ifndef USMANY
 589 mkUsgTy UsMany ty = ASSERT2( isNotUsgTy ty, pprType ty )
 590                     ty
 591 #endif
 592 mkUsgTy usg    ty = ASSERT2( isNotUsgTy ty, pprType ty )
 593                     NoteTy (UsgNote usg) ty
 594
 595 -- The isUsgTy function is utterly useless if UsManys are omitted.
 596 -- Be warned!  KSW 1999-04.
 597 isUsgTy :: Type -> Bool
 598 #ifndef USMANY
 599 isUsgTy _ = True
 600 #else
 601 isUsgTy (NoteTy (UsgNote _) _) = True
 602 isUsgTy other                  = False
 603 #endif
 604
 605 -- The isNotUsgTy function may return a false True if UsManys are omitted;
 606 -- in other words, A SSERT( isNotUsgTy ty ) may be useful but
 607 -- A SSERT( not (isNotUsg ty) ) is asking for trouble.  KSW 1999-04.
 608 isNotUsgTy :: Type -> Bool
 609 isNotUsgTy (NoteTy (UsgNote _) _) = False
 610 isNotUsgTy other                  = True
 611
 612 -- splitUsgTy_maybe is not exported, since it is meaningless if
 613 -- UsManys are omitted.  It is used in several places in this module,
 614 -- however.  KSW 1999-04.
 615 splitUsgTy_maybe :: Type -> Maybe (UsageAnn,Type)
 616 splitUsgTy_maybe (NoteTy (UsgNote usg) ty2) = ASSERT( isNotUsgTy ty2 )
 617                                               Just (usg,ty2)
 618 splitUsgTy_maybe ty                         = Nothing
 619
 620 splitUsgTy :: Type -> (UsageAnn,Type)
 621 splitUsgTy ty = case splitUsgTy_maybe ty of
 622                   Just ans -> ans
 623                   Nothing  ->
 624 #ifndef USMANY
 625                               (UsMany,ty)
 626 #else
 627                               pprPanic "splitUsgTy: no usage annot:" $ pprType ty
 628 #endif
 629
 630 tyUsg :: Type -> UsageAnn
 631 tyUsg = fst . splitUsgTy
 632
 633 unUsgTy :: Type -> Type
 634 -- strip outer usage annotation if present
 635 unUsgTy ty = case splitUsgTy_maybe ty of
 636                Just (_,ty1) -> ASSERT2( isNotUsgTy ty1, pprType ty )
 637                                ty1
 638                Nothing      -> ty
 639 \end{code}
 640
 641
 642
 643 ---------------------------------------------------------------------
 644                                 ForAllTy
 645                                 ~~~~~~~~
 646
 647 We need to be clever here with usage annotations; they need to be
 648 lifted or lowered through the forall as appropriate.
 649
 650 \begin{code}
 651 mkForAllTy :: TyVar -> Type -> Type
 652 mkForAllTy tyvar ty = case splitUsgTy_maybe ty of
 653                         Just (usg,ty') -> NoteTy (UsgNote usg)
 654                                                  (ForAllTy tyvar ty')
 655                         Nothing        -> ForAllTy tyvar ty
 656
 657 mkForAllTys :: [TyVar] -> Type -> Type
 658 mkForAllTys tyvars ty = case splitUsgTy_maybe ty of
 659                           Just (usg,ty') -> NoteTy (UsgNote usg)
 660                                                    (foldr ForAllTy ty' tyvars)
 661                           Nothing        -> foldr ForAllTy ty tyvars
 662
 663 splitForAllTy_maybe :: Type -> Maybe (TyVar, Type)
 664 splitForAllTy_maybe ty = case splitUsgTy_maybe ty of
 665                            Just (usg,ty') -> do (tyvar,ty'') <- splitFAT_m ty'
 666                                                 return (tyvar, NoteTy (UsgNote usg) ty'')
 667                            Nothing        -> splitFAT_m ty
 668   where
 669     splitFAT_m (NoteTy _ ty)       = splitFAT_m ty
 670     splitFAT_m (ForAllTy tyvar ty) = Just(tyvar, ty)
 671     splitFAT_m _                   = Nothing
 672
 673 isForAllTy :: Type -> Bool
 674 isForAllTy (NoteTy _ ty)       = isForAllTy ty
 675 isForAllTy (ForAllTy tyvar ty) = True
 676 isForAllTy _                 = False
 677
 678 splitForAllTys :: Type -> ([TyVar], Type)
 679 splitForAllTys ty = case splitUsgTy_maybe ty of
 680                       Just (usg,ty') -> let (tvs,ty'') = split ty' ty' []
 681                                         in  (tvs, NoteTy (UsgNote usg) ty'')
 682                       Nothing        -> split ty ty []
 683    where
 684      split orig_ty (ForAllTy tv ty) tvs = split ty ty (tv:tvs)
 685      split orig_ty (NoteTy _ ty)    tvs = split orig_ty ty tvs
 686      split orig_ty t                tvs = (reverse tvs, orig_ty)
 687 \end{code}
 688
 689 @mkPiType@ makes a (->) type or a forall type, depending on whether
 690 it is given a type variable or a term variable.
 691
 692 \begin{code}
 693 mkPiType :: IdOrTyVar -> Type -> Type   -- The more polymorphic version doesn't work...
 694 mkPiType v ty | isId v    = mkFunTy (idType v) ty
 695               | otherwise = mkForAllTy v ty
 696 \end{code}
 697
 698 \begin{code}
 699 applyTy :: Type -> Type -> Type
 700 applyTy (NoteTy note@(UsgNote _) fun) arg = NoteTy note (applyTy fun arg)
 701 applyTy (NoteTy _ fun)                arg = applyTy fun arg
 702 applyTy (ForAllTy tv ty)              arg = ASSERT( isNotUsgTy arg )
 703                                             substTy (mkVarEnv [(tv,arg)]) ty
 704 applyTy other                         arg = panic "applyTy"
 705
 706 applyTys :: Type -> [Type] -> Type
 707 applyTys fun_ty arg_tys
 708  = go [] fun_ty arg_tys
 709  where
 710    go env ty               []         = substTy (mkVarEnv env) ty
 711    go env (NoteTy note@(UsgNote _) fun)
 712                            args       = NoteTy note (go env fun args)
 713    go env (NoteTy _ fun)   args       = go env fun args
 714    go env (ForAllTy tv ty) (arg:args) = ASSERT2( isNotUsgTy arg, vcat ((map pprType arg_tys) ++ [text "in application of" <+> pprType fun_ty]) )
 715                                         go ((tv,arg):env) ty args
 716    go env other            args       = panic "applyTys"
 717 \end{code}
 718
 719 Note that we allow applications to be of usage-annotated- types, as an
 720 extension: we handle them by lifting the annotation outside.  The
 721 argument, however, must still be unannotated.
 722
 723 %************************************************************************
 724 %*                                                                      *
 725 \subsection{Stuff to do with the source-language types}
 726 %*                                                                      *
 727 %************************************************************************
 728
 729 \begin{code}
 730 type RhoType   = Type
 731 type TauType   = Type
 732 type ThetaType = [(Class, [Type])]
 733 type SigmaType = Type
 734 \end{code}
 735
 736 @isTauTy@ tests for nested for-alls.
 737
 738 \begin{code}
 739 isTauTy :: Type -> Bool
 740 isTauTy (TyVarTy v)      = True
 741 isTauTy (TyConApp _ tys) = all isTauTy tys
 742 isTauTy (AppTy a b)      = isTauTy a && isTauTy b
 743 isTauTy (FunTy a b)      = isTauTy a && isTauTy b
 744 isTauTy (NoteTy _ ty)    = isTauTy ty
 745 isTauTy other            = False
 746 \end{code}
 747
 748 \begin{code}
 749 mkRhoTy :: [(Class, [Type])] -> Type -> Type
 750 mkRhoTy theta ty = foldr (\(c,t) r -> FunTy (mkDictTy c t) r) ty theta
 751
 752 splitRhoTy :: Type -> ([(Class, [Type])], Type)
 753 splitRhoTy ty = split ty ty []
 754  where
 755   split orig_ty (FunTy arg res) ts = case splitDictTy_maybe arg of
 756                                         Just pair -> split res res (pair:ts)
 757                                         Nothing   -> (reverse ts, orig_ty)
 758   split orig_ty (NoteTy _ ty) ts   = split orig_ty ty ts
 759   split orig_ty ty ts              = (reverse ts, orig_ty)
 760 \end{code}
 761
 762
 763
 764 \begin{code}
 765 mkSigmaTy tyvars theta tau = mkForAllTys tyvars (mkRhoTy theta tau)
 766
 767 splitSigmaTy :: Type -> ([TyVar], [(Class, [Type])], Type)
 768 splitSigmaTy ty =
 769   (tyvars, theta, tau)
 770  where
 771   (tyvars,rho) = splitForAllTys ty
 772   (theta,tau)  = splitRhoTy rho
 773 \end{code}
 774
 775
 776 %************************************************************************
 777 %*                                                                      *
 778 \subsection{Kinds and free variables}
 779 %*                                                                      *
 780 %************************************************************************
 781
 782 ---------------------------------------------------------------------
 783                 Finding the kind of a type
 784                 ~~~~~~~~~~~~~~~~~~~~~~~~~~
 785 \begin{code}
 786 typeKind :: Type -> Kind
 787
 788 typeKind (TyVarTy tyvar)        = tyVarKind tyvar
 789 typeKind (TyConApp tycon tys)   = foldr (\_ k -> funResultTy k) (tyConKind tycon) tys
 790 typeKind (NoteTy _ ty)          = typeKind ty
 791 typeKind (AppTy fun arg)        = funResultTy (typeKind fun)
 792 typeKind (FunTy fun arg)        = typeKindF arg
 793 typeKind (ForAllTy _ ty)        = typeKindF ty  -- We could make this a new kind polyTypeKind
 794                                                 -- to prevent a forall type unifying with a
 795                                                 -- boxed type variable, but I didn't think it
 796                                                 -- was worth it yet.
 797
 798 -- The complication is that a *function* is boxed even if
 799 -- its *result* type is unboxed.  Seems wierd.
 800
 801 typeKindF :: Type -> Kind
 802 typeKindF (NoteTy _ ty)   = typeKindF ty
 803 typeKindF (FunTy _ ty)    = typeKindF ty
 804 typeKindF (ForAllTy _ ty) = typeKindF ty
 805 typeKindF other           = fix_up (typeKind other)
 806   where
 807     fix_up (TyConApp kc _) | kc == typeCon = boxedTypeKind
 808                 -- Functions at the type level are always boxed
 809     fix_up (NoteTy _ kind) = fix_up kind
 810     fix_up kind            = kind
 811 \end{code}
 812
 813
 814 ---------------------------------------------------------------------
 815                 Free variables of a type
 816                 ~~~~~~~~~~~~~~~~~~~~~~~~
 817 \begin{code}
 818 tyVarsOfType :: Type -> TyVarSet
 819
 820 tyVarsOfType (TyVarTy tv)               = unitVarSet tv
 821 tyVarsOfType (TyConApp tycon tys)       = tyVarsOfTypes tys
 822 tyVarsOfType (NoteTy (FTVNote tvs) ty2) = tvs
 823 tyVarsOfType (NoteTy (SynNote ty1) ty2) = tyVarsOfType ty1
 824 tyVarsOfType (NoteTy (UsgNote _) ty)    = tyVarsOfType ty
 825 tyVarsOfType (FunTy arg res)            = tyVarsOfType arg `unionVarSet` tyVarsOfType res
 826 tyVarsOfType (AppTy fun arg)            = tyVarsOfType fun `unionVarSet` tyVarsOfType arg
 827 tyVarsOfType (ForAllTy tyvar ty)        = tyVarsOfType ty `minusVarSet` unitVarSet tyvar
 828
 829 tyVarsOfTypes :: [Type] -> TyVarSet
 830 tyVarsOfTypes tys = foldr (unionVarSet.tyVarsOfType) emptyVarSet tys
 831
 832 -- Add a Note with the free tyvars to the top of the type
 833 -- (but under a usage if there is one)
 834 addFreeTyVars :: Type -> Type
 835 addFreeTyVars (NoteTy note@(UsgNote _) ty) = NoteTy note (addFreeTyVars ty)
 836 addFreeTyVars ty@(NoteTy (FTVNote _) _)    = ty
 837 addFreeTyVars ty                           = NoteTy (FTVNote (tyVarsOfType ty)) ty
 838
 839 -- Find the free names of a type, including the type constructors and classes it mentions
 840 namesOfType :: Type -> NameSet
 841 namesOfType (TyVarTy tv)                = unitNameSet (getName tv)
 842 namesOfType (TyConApp tycon tys)        = unitNameSet (getName tycon) `unionNameSets`
 843                                           namesOfTypes tys
 844 namesOfType (NoteTy (SynNote ty1) ty2)  = namesOfType ty1
 845 namesOfType (NoteTy other_note    ty2)  = namesOfType ty2
 846 namesOfType (FunTy arg res)             = namesOfType arg `unionNameSets` namesOfType res
 847 namesOfType (AppTy fun arg)             = namesOfType fun `unionNameSets` namesOfType arg
 848 namesOfType (ForAllTy tyvar ty)         = namesOfType ty `minusNameSet` unitNameSet (getName tyvar)
 849
 850 namesOfTypes tys = foldr (unionNameSets . namesOfType) emptyNameSet tys
 851 \end{code}
 852
 853
 854 %************************************************************************
 855 %*                                                                      *
 856 \subsection{Instantiating a type}
 857 %*                                                                      *
 858 %************************************************************************
 859
 860 @substTy@ applies a substitution to a type.  It deals correctly with name capture.
 861
 862 \begin{code}
 863 substTy :: TyVarSubst -> Type -> Type
 864 substTy tenv ty
 865   | isEmptyVarEnv tenv = ty
 866   | otherwise          = subst_ty tenv tset ty
 867   where
 868     tset = foldVarEnv (unionVarSet . tyVarsOfType) emptyVarSet tenv
 869                 -- If ty doesn't have any for-alls, then this thunk
 870                 -- will never be evaluated
 871
 872 substTheta :: TyVarSubst -> ThetaType -> ThetaType
 873 substTheta tenv theta
 874   | isEmptyVarEnv tenv = theta
 875   | otherwise          = [(clas, map (subst_ty tenv tset) tys) | (clas, tys) <- theta]
 876   where
 877     tset = foldVarEnv (unionVarSet . tyVarsOfType) emptyVarSet tenv
 878                 -- If ty doesn't have any for-alls, then this thunk
 879                 -- will never be evaluated
 880
 881 substTopTy :: TyVarSubst -> Type -> Type
 882 substTopTy = substTy    -- Called when doing top-level substitutions.
 883                         -- Here we expect that the free vars of the range of the
 884                         -- substitution will be empty; but during typechecking I'm
 885                         -- a bit dubious about that (mutable tyvars bouund to Int, say)
 886                         -- So I've left it as substTy for the moment.  SLPJ Nov 98
 887 substTopTheta = substTheta
 888 \end{code}
 889
 890 @fullSubstTy@ is like @substTy@ except that it needs to be given a set
 891 of in-scope type variables.  In exchange it's a bit more efficient, at least
 892 if you happen to have that set lying around.
 893
 894 \begin{code}
 895 fullSubstTy :: TyVarSubst               -- Substitution to apply
 896             -> TyVarSet                 -- Superset of the free tyvars of
 897                                         -- the range of the tyvar env
 898             -> Type  -> Type
 899 -- ASSUMPTION: The substitution is idempotent.
 900 -- Equivalently: No tyvar is both in scope, and in the domain of the substitution.
 901 fullSubstTy tenv tset ty | isEmptyVarEnv tenv = ty
 902                          | otherwise          = subst_ty tenv tset ty
 903
 904 -- subst_ty does the business
 905 subst_ty tenv tset ty
 906    = go ty
 907   where
 908     go (TyConApp tc tys)           = let args = map go tys
 909                                      in  args `seqList` TyConApp tc args
 910     go (NoteTy (SynNote ty1) ty2)  = NoteTy (SynNote $! (go ty1)) $! (go ty2)
 911     go (NoteTy (FTVNote _) ty2)    = go ty2             -- Discard the free tyvar note
 912     go (NoteTy (UsgNote usg) ty2)  = (NoteTy $! (UsgNote usg)) $! (go ty2)  -- Keep usage annot
 913     go (FunTy arg res)             = FunTy (go arg) (go res)
 914     go (AppTy fun arg)             = mkAppTy (go fun) (go arg)
 915     go ty@(TyVarTy tv)             = case (lookupVarEnv tenv tv) of
 916                                       Nothing  -> ty
 917                                       Just ty' -> ty'
 918     go (ForAllTy tv ty)            = case substTyVar tenv tset tv of
 919                                         (tenv', tset', tv') -> ForAllTy tv' $! (subst_ty tenv' tset' ty)
 920
 921 substTyVar ::  TyVarSubst -> TyVarSet -> TyVar
 922            -> (TyVarSubst,   TyVarSet,   TyVar)
 923
 924 substTyVar tenv tset tv
 925   | not (tv `elemVarSet` tset)  -- No need to clone
 926                                 -- But must delete from substitution
 927   = (tenv `delVarEnv` tv, tset `extendVarSet` tv, tv)
 928
 929   | otherwise   -- The forall's variable is in scope so
 930                 -- we'd better rename it away from the in-scope variables
 931                 -- Extending the substitution to do this renaming also
 932                 -- has the (correct) effect of discarding any existing
 933                 -- substitution for that variable
 934   = (extendVarEnv tenv tv (TyVarTy tv'), tset `extendVarSet` tv', tv')
 935   where
 936      tv' = uniqAway tset tv
 937 \end{code}
 938
 939
 940 %************************************************************************
 941 %*                                                                      *
 942 \subsection{TidyType}
 943 %*                                                                      *
 944 %************************************************************************
 945
 946 tidyTy tidies up a type for printing in an error message, or in
 947 an interface file.
 948
 949 It doesn't change the uniques at all, just the print names.
 950
 951 \begin{code}
 952 tidyTyVar :: TidyEnv -> TyVar -> (TidyEnv, TyVar)
 953 tidyTyVar env@(tidy_env, subst) tyvar
 954   = case lookupVarEnv subst tyvar of
 955
 956         Just tyvar' ->  -- Already substituted
 957                 (env, tyvar')
 958
 959         Nothing ->      -- Make a new nice name for it
 960
 961                 case tidyOccName tidy_env (getOccName name) of
 962                     (tidy', occ') ->    -- New occname reqd
 963                                 ((tidy', subst'), tyvar')
 964                               where
 965                                 subst' = extendVarEnv subst tyvar tyvar'
 966                                 tyvar' = setTyVarName tyvar name'
 967                                 name'  = mkLocalName (getUnique name) occ' noSrcLoc
 968                                         -- Note: make a *user* tyvar, so it printes nicely
 969                                         -- Could extract src loc, but no need.
 970   where
 971     name = tyVarName tyvar
 972
 973 tidyTyVars env tyvars = mapAccumL tidyTyVar env tyvars
 974
 975 tidyType :: TidyEnv -> Type -> Type
 976 tidyType env@(tidy_env, subst) ty
 977   = go ty
 978   where
 979     go (TyVarTy tv)         = case lookupVarEnv subst tv of
 980                                 Nothing  -> TyVarTy tv
 981                                 Just tv' -> TyVarTy tv'
 982     go (TyConApp tycon tys) = let args = map go tys
 983                               in args `seqList` TyConApp tycon args
 984     go (NoteTy note ty)     = (NoteTy $! (go_note note)) $! (go ty)
 985     go (AppTy fun arg)      = (AppTy $! (go fun)) $! (go arg)
 986     go (FunTy fun arg)      = (FunTy $! (go fun)) $! (go arg)
 987     go (ForAllTy tv ty)     = ForAllTy tv' $! (tidyType env' ty)
 988                             where
 989                               (env', tv') = tidyTyVar env tv
 990
 991     go_note (SynNote ty)        = SynNote $! (go ty)
 992     go_note note@(FTVNote ftvs) = note  -- No need to tidy the free tyvars
 993     go_note note@(UsgNote _)    = note  -- Usage annotation is already tidy
 994
 995 tidyTypes  env tys    = map (tidyType env) tys
 996 \end{code}
 997
 998
 999 @tidyOpenType@ grabs the free type varibles, tidies them
1000 and then uses @tidyType@ to work over the type itself
1001
1002 \begin{code}
1003 tidyOpenType :: TidyEnv -> Type -> (TidyEnv, Type)
1004 tidyOpenType env ty
1005   = (env', tidyType env' ty)
1006   where
1007     env'         = foldl go env (varSetElems (tyVarsOfType ty))
1008     go env tyvar = fst (tidyTyVar env tyvar)
1009
1010 tidyOpenTypes :: TidyEnv -> [Type] -> (TidyEnv, [Type])
1011 tidyOpenTypes env tys = mapAccumL tidyOpenType env tys
1012
1013 tidyTopType :: Type -> Type
1014 tidyTopType ty = tidyType emptyTidyEnv ty
1015 \end{code}
1016
1017
1018 %************************************************************************
1019 %*                                                                      *
1020 \subsection{Boxedness and liftedness}
1021 %*                                                                      *
1022 %************************************************************************
1023
1024 \begin{code}
1025 isUnboxedType :: Type -> Bool
1026 isUnboxedType ty = not (isFollowableRep (typePrimRep ty))
1027
1028 isUnLiftedType :: Type -> Bool
1029 isUnLiftedType ty = case splitTyConApp_maybe ty of
1030                            Just (tc, ty_args) -> isUnLiftedTyCon tc
1031                            other              -> False
1032
1033 isUnboxedTupleType :: Type -> Bool
1034 isUnboxedTupleType ty = case splitTyConApp_maybe ty of
1035                            Just (tc, ty_args) -> isUnboxedTupleTyCon tc
1036                            other              -> False
1037
1038 -- Should only be applied to *types*; hence the assert
1039 isAlgType :: Type -> Bool
1040 isAlgType ty = case splitTyConApp_maybe ty of
1041                         Just (tc, ty_args) -> ASSERT( length ty_args == tyConArity tc )
1042                                               isAlgTyCon tc
1043                         other              -> False
1044
1045 -- Should only be applied to *types*; hence the assert
1046 isDataType :: Type -> Bool
1047 isDataType ty = case splitTyConApp_maybe ty of
1048                         Just (tc, ty_args) -> ASSERT( length ty_args == tyConArity tc )
1049                                               isDataTyCon tc
1050                         other              -> False
1051
1052 typePrimRep :: Type -> PrimRep
1053 typePrimRep ty = case splitTyConApp_maybe ty of
1054                    Just (tc, ty_args) -> tyConPrimRep tc
1055                    other              -> PtrRep
1056 \end{code}
1057
1058 %************************************************************************
1059 %*                                                                      *
1060 \subsection{Equality on types}
1061 %*                                                                      *
1062 %************************************************************************
1063
1064 For the moment at least, type comparisons don't work if
1065 there are embedded for-alls.
1066
1067 \begin{code}
1068 instance Eq Type where
1069   ty1 == ty2 = case ty1 `cmpTy` ty2 of { EQ -> True; other -> False }
1070
1071 instance Ord Type where
1072   compare ty1 ty2 = cmpTy ty1 ty2
1073
1074 cmpTy :: Type -> Type -> Ordering
1075 cmpTy ty1 ty2
1076   = cmp emptyVarEnv ty1 ty2
1077   where
1078   -- The "env" maps type variables in ty1 to type variables in ty2
1079   -- So when comparing for-alls.. (forall tv1 . t1) (forall tv2 . t2)
1080   -- we in effect substitute tv2 for tv1 in t1 before continuing
1081     lookup env tv1 = case lookupVarEnv env tv1 of
1082                           Just tv2 -> tv2
1083                           Nothing  -> tv1
1084
1085     -- Get rid of NoteTy
1086     cmp env (NoteTy _ ty1) ty2 = cmp env ty1 ty2
1087     cmp env ty1 (NoteTy _ ty2) = cmp env ty1 ty2
1088
1089     -- Deal with equal constructors
1090     cmp env (TyVarTy tv1) (TyVarTy tv2) = lookup env tv1 `compare` tv2
1091     cmp env (AppTy f1 a1) (AppTy f2 a2) = cmp env f1 f2 `thenCmp` cmp env a1 a2
1092     cmp env (FunTy f1 a1) (FunTy f2 a2) = cmp env f1 f2 `thenCmp` cmp env a1 a2
1093     cmp env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmps env tys1 tys2)
1094     cmp env (ForAllTy tv1 t1)   (ForAllTy tv2 t2)   = cmp (extendVarEnv env tv1 tv2) t1 t2
1095
1096     -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < ForAllTy
1097     cmp env (AppTy _ _) (TyVarTy _) = GT
1098
1099     cmp env (FunTy _ _) (TyVarTy _) = GT
1100     cmp env (FunTy _ _) (AppTy _ _) = GT
1101
1102     cmp env (TyConApp _ _) (TyVarTy _) = GT
1103     cmp env (TyConApp _ _) (AppTy _ _) = GT
1104     cmp env (TyConApp _ _) (FunTy _ _) = GT
1105
1106     cmp env (ForAllTy _ _) other       = GT
1107
1108     cmp env _ _                        = LT
1109
1110     cmps env []     [] = EQ
1111     cmps env (t:ts) [] = GT
1112     cmps env [] (t:ts) = LT
1113     cmps env (t1:t1s) (t2:t2s) = cmp env t1 t2 `thenCmp` cmps env t1s t2s
1114 \end{code}
1115
1116