compiler/types/Type.lhs

   1 %
   2 % (c) The University of Glasgow 2006
   3 % (c) The GRASP/AQUA Project, Glasgow University, 1998
   4 %
   5
   6 Type - public interface
   7
   8 \begin{code}
   9 -- The above warning supression flag is a temporary kludge.
  10 -- While working on this module you are encouraged to remove it and fix
  11 -- any warnings in the module. See
  12 --     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
  13 -- for details
  14
  15 -- | Main functions for manipulating types and type-related things
  16 module Type (
  17         -- Note some of this is just re-exports from TyCon..
  18
  19         -- * Main data types representing Types
  20         -- $type_classification
  21
  22         -- $representation_types
  23         TyThing(..), Type, Pred(..), PredType, ThetaType,
  24         Var, TyVar, isTyVar,
  25
  26         -- ** Constructing and deconstructing types
  27         mkTyVarTy, mkTyVarTys, getTyVar, getTyVar_maybe,
  28
  29         mkAppTy, mkAppTys, splitAppTy, splitAppTys,
  30         splitAppTy_maybe, repSplitAppTy_maybe,
  31
  32         mkFunTy, mkFunTys, splitFunTy, splitFunTy_maybe,
  33         splitFunTys, splitFunTysN,
  34         funResultTy, funArgTy, zipFunTys,
  35
  36         mkTyConApp, mkTyConTy,
  37         tyConAppTyCon, tyConAppArgs,
  38         splitTyConApp_maybe, splitTyConApp,
  39
  40         mkForAllTy, mkForAllTys, splitForAllTy_maybe, splitForAllTys,
  41         applyTy, applyTys, applyTysD, isForAllTy, dropForAlls,
  42
  43         -- (Newtypes)
  44         newTyConInstRhs, carefullySplitNewType_maybe,
  45
  46         -- (Type families)
  47         tyFamInsts, predFamInsts,
  48
  49         -- Pred types
  50         mkPredTy, mkPredTys, mkFamilyTyConApp,
  51         mkDictTy, isDictLikeTy, isClassPred,
  52         isEqPred, allPred, mkEqPred,
  53         mkClassPred, getClassPredTys, getClassPredTys_maybe,
  54         isTyVarClassPred,
  55         mkIPPred, isIPPred,
  56
  57         -- ** Common type constructors
  58         funTyCon,
  59
  60         -- ** Predicates on types
  61         isTyVarTy, isFunTy, isPredTy,
  62         isDictTy, isEqPredTy, isReflPredTy, splitPredTy_maybe, splitEqPredTy_maybe,
  63
  64         -- (Lifting and boxity)
  65         isUnLiftedType, isUnboxedTupleType, isAlgType, isClosedAlgType,
  66         isPrimitiveType, isStrictType, isStrictPred,
  67
  68         -- * Main data types representing Kinds
  69         -- $kind_subtyping
  70         Kind, SimpleKind, KindVar,
  71
  72         -- ** Common Kinds and SuperKinds
  73         liftedTypeKind, unliftedTypeKind, openTypeKind,
  74         argTypeKind, ubxTupleKind,
  75         tySuperKind,
  76
  77         -- ** Common Kind type constructors
  78         liftedTypeKindTyCon, openTypeKindTyCon, unliftedTypeKindTyCon,
  79         argTypeKindTyCon, ubxTupleKindTyCon,
  80
  81         -- * Type free variables
  82         tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
  83         exactTyVarsOfType, exactTyVarsOfTypes, expandTypeSynonyms,
  84         typeSize,
  85
  86         -- * Type comparison
  87         eqType, eqTypeX, eqTypes, cmpType, cmpTypes,
  88         eqPred, eqPredX, cmpPred, eqKind,
  89
  90         -- * Forcing evaluation of types
  91         seqType, seqTypes, seqPred,
  92
  93         -- * Other views onto Types
  94         coreView, tcView,
  95
  96         repType,
  97
  98         -- * Type representation for the code generator
  99         PrimRep(..),
 100
 101         typePrimRep, predTypeRep,
 102
 103         -- * Main type substitution data types
 104         TvSubstEnv,     -- Representation widely visible
 105         TvSubst(..),    -- Representation visible to a few friends
 106
 107         -- ** Manipulating type substitutions
 108         emptyTvSubstEnv, emptyTvSubst,
 109
 110         mkTvSubst, mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst, mkTopTvSubst, notElemTvSubst,
 111         getTvSubstEnv, setTvSubstEnv,
 112         zapTvSubstEnv, getTvInScope,
 113         extendTvInScope, extendTvInScopeList,
 114         extendTvSubst, extendTvSubstList,
 115         isInScope, composeTvSubst, zipTyEnv,
 116         isEmptyTvSubst, unionTvSubst,
 117
 118         -- ** Performing substitution on types
 119         substTy, substTys, substTyWith, substTysWith, substTheta,
 120         substPred, substTyVar, substTyVars, substTyVarBndr,
 121         deShadowTy, lookupTyVar,
 122
 123         -- * Pretty-printing
 124         pprType, pprParendType, pprTypeApp, pprTyThingCategory, pprTyThing, pprForAll,
 125         pprPred, pprPredTy, pprEqPred, pprTheta, pprThetaArrowTy, pprClassPred,
 126         pprKind, pprParendKind,
 127
 128         pprSourceTyCon
 129     ) where
 130
 131 #include "HsVersions.h"
 132
 133 -- We import the representation and primitive functions from TypeRep.
 134 -- Many things are reexported, but not the representation!
 135
 136 import TypeRep
 137
 138 -- friends:
 139 import Var
 140 import VarEnv
 141 import VarSet
 142
 143 import Class
 144 import TyCon
 145 import TysPrim
 146
 147 -- others
 148 import BasicTypes       ( IPName )
 149 import Name             ( Name )
 150 import StaticFlags
 151 import Util
 152 import Outputable
 153 import FastString
 154
 155 import Data.Maybe       ( isJust )
 156
 157 infixr 3 `mkFunTy`      -- Associates to the right
 158 \end{code}
 159
 160 \begin{code}
 161 -- $type_classification
 162 -- #type_classification#
 163 --
 164 -- Types are one of:
 165 --
 166 -- [Unboxed]            Iff its representation is other than a pointer
 167 --                      Unboxed types are also unlifted.
 168 --
 169 -- [Lifted]             Iff it has bottom as an element.
 170 --                      Closures always have lifted types: i.e. any
 171 --                      let-bound identifier in Core must have a lifted
 172 --                      type. Operationally, a lifted object is one that
 173 --                      can be entered.
 174 --                      Only lifted types may be unified with a type variable.
 175 --
 176 -- [Algebraic]          Iff it is a type with one or more constructors, whether
 177 --                      declared with @data@ or @newtype@.
 178 --                      An algebraic type is one that can be deconstructed
 179 --                      with a case expression. This is /not/ the same as
 180 --                      lifted types, because we also include unboxed
 181 --                      tuples in this classification.
 182 --
 183 -- [Data]               Iff it is a type declared with @data@, or a boxed tuple.
 184 --
 185 -- [Primitive]          Iff it is a built-in type that can't be expressed in Haskell.
 186 --
 187 -- Currently, all primitive types are unlifted, but that's not necessarily
 188 -- the case: for example, @Int@ could be primitive.
 189 --
 190 -- Some primitive types are unboxed, such as @Int#@, whereas some are boxed
 191 -- but unlifted (such as @ByteArray#@).  The only primitive types that we
 192 -- classify as algebraic are the unboxed tuples.
 193 --
 194 -- Some examples of type classifications that may make this a bit clearer are:
 195 --
 196 -- @
 197 -- Type         primitive       boxed           lifted          algebraic
 198 -- -----------------------------------------------------------------------------
 199 -- Int#         Yes             No              No              No
 200 -- ByteArray#   Yes             Yes             No              No
 201 -- (\# a, b \#)   Yes             No              No              Yes
 202 -- (  a, b  )   No              Yes             Yes             Yes
 203 -- [a]          No              Yes             Yes             Yes
 204 -- @
 205
 206 -- $representation_types
 207 -- A /source type/ is a type that is a separate type as far as the type checker is
 208 -- concerned, but which has a more low-level representation as far as Core-to-Core
 209 -- passes and the rest of the back end is concerned. Notably, 'PredTy's are removed
 210 -- from the representation type while they do exist in the source types.
 211 --
 212 -- You don't normally have to worry about this, as the utility functions in
 213 -- this module will automatically convert a source into a representation type
 214 -- if they are spotted, to the best of it's abilities. If you don't want this
 215 -- to happen, use the equivalent functions from the "TcType" module.
 216 \end{code}
 217
 218 %************************************************************************
 219 %*                                                                      *
 220                 Type representation
 221 %*                                                                      *
 222 %************************************************************************
 223
 224 \begin{code}
 225 {-# INLINE coreView #-}
 226 coreView :: Type -> Maybe Type
 227 -- ^ In Core, we \"look through\" non-recursive newtypes and 'PredTypes': this
 228 -- function tries to obtain a different view of the supplied type given this
 229 --
 230 -- Strips off the /top layer only/ of a type to give
 231 -- its underlying representation type.
 232 -- Returns Nothing if there is nothing to look through.
 233 --
 234 -- By being non-recursive and inlined, this case analysis gets efficiently
 235 -- joined onto the case analysis that the caller is already doing
 236 coreView (PredTy p)        = Just (predTypeRep p)
 237 coreView (TyConApp tc tys) | Just (tenv, rhs, tys') <- coreExpandTyCon_maybe tc tys
 238                            = Just (mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys')
 239                                 -- Its important to use mkAppTys, rather than (foldl AppTy),
 240                                 -- because the function part might well return a
 241                                 -- partially-applied type constructor; indeed, usually will!
 242 coreView _                 = Nothing
 243
 244
 245 -----------------------------------------------
 246 {-# INLINE tcView #-}
 247 tcView :: Type -> Maybe Type
 248 -- ^ Similar to 'coreView', but for the type checker, which just looks through synonyms
 249 tcView (TyConApp tc tys) | Just (tenv, rhs, tys') <- tcExpandTyCon_maybe tc tys
 250                          = Just (mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys')
 251 tcView _                 = Nothing
 252
 253 -----------------------------------------------
 254 expandTypeSynonyms :: Type -> Type
 255 -- ^ Expand out all type synonyms.  Actually, it'd suffice to expand out
 256 -- just the ones that discard type variables (e.g.  type Funny a = Int)
 257 -- But we don't know which those are currently, so we just expand all.
 258 expandTypeSynonyms ty
 259   = go ty
 260   where
 261     go (TyConApp tc tys)
 262       | Just (tenv, rhs, tys') <- tcExpandTyCon_maybe tc tys
 263       = go (mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys')
 264       | otherwise
 265       = TyConApp tc (map go tys)
 266     go (TyVarTy tv)    = TyVarTy tv
 267     go (AppTy t1 t2)   = AppTy (go t1) (go t2)
 268     go (FunTy t1 t2)   = FunTy (go t1) (go t2)
 269     go (ForAllTy tv t) = ForAllTy tv (go t)
 270     go (PredTy p)      = PredTy (go_pred p)
 271
 272     go_pred (ClassP c ts)  = ClassP c (map go ts)
 273     go_pred (IParam ip t)  = IParam ip (go t)
 274     go_pred (EqPred t1 t2) = EqPred (go t1) (go t2)
 275 \end{code}
 276
 277
 278 %************************************************************************
 279 %*                                                                      *
 280 \subsection{Constructor-specific functions}
 281 %*                                                                      *
 282 %************************************************************************
 283
 284
 285 ---------------------------------------------------------------------
 286                                 TyVarTy
 287                                 ~~~~~~~
 288 \begin{code}
 289 -- | Attempts to obtain the type variable underlying a 'Type', and panics with the
 290 -- given message if this is not a type variable type. See also 'getTyVar_maybe'
 291 getTyVar :: String -> Type -> TyVar
 292 getTyVar msg ty = case getTyVar_maybe ty of
 293                     Just tv -> tv
 294                     Nothing -> panic ("getTyVar: " ++ msg)
 295
 296 isTyVarTy :: Type -> Bool
 297 isTyVarTy ty = isJust (getTyVar_maybe ty)
 298
 299 -- | Attempts to obtain the type variable underlying a 'Type'
 300 getTyVar_maybe :: Type -> Maybe TyVar
 301 getTyVar_maybe ty | Just ty' <- coreView ty = getTyVar_maybe ty'
 302 getTyVar_maybe (TyVarTy tv)                 = Just tv
 303 getTyVar_maybe _                            = Nothing
 304
 305 \end{code}
 306
 307
 308 ---------------------------------------------------------------------
 309                                 AppTy
 310                                 ~~~~~
 311 We need to be pretty careful with AppTy to make sure we obey the
 312 invariant that a TyConApp is always visibly so.  mkAppTy maintains the
 313 invariant: use it.
 314
 315 \begin{code}
 316 -- | Applies a type to another, as in e.g. @k a@
 317 mkAppTy :: Type -> Type -> Type
 318 mkAppTy orig_ty1 orig_ty2
 319   = mk_app orig_ty1
 320   where
 321     mk_app (TyConApp tc tys) = mkTyConApp tc (tys ++ [orig_ty2])
 322     mk_app _                 = AppTy orig_ty1 orig_ty2
 323         -- Note that the TyConApp could be an
 324         -- under-saturated type synonym.  GHC allows that; e.g.
 325         --      type Foo k = k a -> k a
 326         --      type Id x = x
 327         --      foo :: Foo Id -> Foo Id
 328         --
 329         -- Here Id is partially applied in the type sig for Foo,
 330         -- but once the type synonyms are expanded all is well
 331
 332 mkAppTys :: Type -> [Type] -> Type
 333 mkAppTys orig_ty1 []        = orig_ty1
 334         -- This check for an empty list of type arguments
 335         -- avoids the needless loss of a type synonym constructor.
 336         -- For example: mkAppTys Rational []
 337         --   returns to (Ratio Integer), which has needlessly lost
 338         --   the Rational part.
 339 mkAppTys orig_ty1 orig_tys2
 340   = mk_app orig_ty1
 341   where
 342     mk_app (TyConApp tc tys) = mkTyConApp tc (tys ++ orig_tys2)
 343                                 -- mkTyConApp: see notes with mkAppTy
 344     mk_app _                 = foldl AppTy orig_ty1 orig_tys2
 345
 346 -------------
 347 splitAppTy_maybe :: Type -> Maybe (Type, Type)
 348 -- ^ Attempt to take a type application apart, whether it is a
 349 -- function, type constructor, or plain type application. Note
 350 -- that type family applications are NEVER unsaturated by this!
 351 splitAppTy_maybe ty | Just ty' <- coreView ty
 352                     = splitAppTy_maybe ty'
 353 splitAppTy_maybe ty = repSplitAppTy_maybe ty
 354
 355 -------------
 356 repSplitAppTy_maybe :: Type -> Maybe (Type,Type)
 357 -- ^ Does the AppTy split as in 'splitAppTy_maybe', but assumes that
 358 -- any Core view stuff is already done
 359 repSplitAppTy_maybe (FunTy ty1 ty2)   = Just (TyConApp funTyCon [ty1], ty2)
 360 repSplitAppTy_maybe (AppTy ty1 ty2)   = Just (ty1, ty2)
 361 repSplitAppTy_maybe (TyConApp tc tys)
 362   | isDecomposableTyCon tc || tys `lengthExceeds` tyConArity tc
 363   , Just (tys', ty') <- snocView tys
 364   = Just (TyConApp tc tys', ty')    -- Never create unsaturated type family apps!
 365 repSplitAppTy_maybe _other = Nothing
 366 -------------
 367 splitAppTy :: Type -> (Type, Type)
 368 -- ^ Attempts to take a type application apart, as in 'splitAppTy_maybe',
 369 -- and panics if this is not possible
 370 splitAppTy ty = case splitAppTy_maybe ty of
 371                         Just pr -> pr
 372                         Nothing -> panic "splitAppTy"
 373
 374 -------------
 375 splitAppTys :: Type -> (Type, [Type])
 376 -- ^ Recursively splits a type as far as is possible, leaving a residual
 377 -- type being applied to and the type arguments applied to it. Never fails,
 378 -- even if that means returning an empty list of type applications.
 379 splitAppTys ty = split ty ty []
 380   where
 381     split orig_ty ty args | Just ty' <- coreView ty = split orig_ty ty' args
 382     split _       (AppTy ty arg)        args = split ty ty (arg:args)
 383     split _       (TyConApp tc tc_args) args
 384       = let -- keep type families saturated
 385             n | isDecomposableTyCon tc = 0
 386               | otherwise              = tyConArity tc
 387             (tc_args1, tc_args2) = splitAt n tc_args
 388         in
 389         (TyConApp tc tc_args1, tc_args2 ++ args)
 390     split _       (FunTy ty1 ty2)       args = ASSERT( null args )
 391                                                (TyConApp funTyCon [], [ty1,ty2])
 392     split orig_ty _                     args = (orig_ty, args)
 393
 394 \end{code}
 395
 396
 397 ---------------------------------------------------------------------
 398                                 FunTy
 399                                 ~~~~~
 400
 401 \begin{code}
 402 mkFunTy :: Type -> Type -> Type
 403 -- ^ Creates a function type from the given argument and result type
 404 mkFunTy arg res = FunTy arg res
 405
 406 mkFunTys :: [Type] -> Type -> Type
 407 mkFunTys tys ty = foldr mkFunTy ty tys
 408
 409 isFunTy :: Type -> Bool
 410 isFunTy ty = isJust (splitFunTy_maybe ty)
 411
 412 splitFunTy :: Type -> (Type, Type)
 413 -- ^ Attempts to extract the argument and result types from a type, and
 414 -- panics if that is not possible. See also 'splitFunTy_maybe'
 415 splitFunTy ty | Just ty' <- coreView ty = splitFunTy ty'
 416 splitFunTy (FunTy arg res)   = (arg, res)
 417 splitFunTy other             = pprPanic "splitFunTy" (ppr other)
 418
 419 splitFunTy_maybe :: Type -> Maybe (Type, Type)
 420 -- ^ Attempts to extract the argument and result types from a type
 421 splitFunTy_maybe ty | Just ty' <- coreView ty = splitFunTy_maybe ty'
 422 splitFunTy_maybe (FunTy arg res)   = Just (arg, res)
 423 splitFunTy_maybe _                 = Nothing
 424
 425 splitFunTys :: Type -> ([Type], Type)
 426 splitFunTys ty = split [] ty ty
 427   where
 428     split args orig_ty ty | Just ty' <- coreView ty = split args orig_ty ty'
 429     split args _       (FunTy arg res)   = split (arg:args) res res
 430     split args orig_ty _                 = (reverse args, orig_ty)
 431
 432 splitFunTysN :: Int -> Type -> ([Type], Type)
 433 -- ^ Split off exactly the given number argument types, and panics if that is not possible
 434 splitFunTysN 0 ty = ([], ty)
 435 splitFunTysN n ty = ASSERT2( isFunTy ty, int n <+> ppr ty )
 436                     case splitFunTy ty of { (arg, res) ->
 437                     case splitFunTysN (n-1) res of { (args, res) ->
 438                     (arg:args, res) }}
 439
 440 -- | Splits off argument types from the given type and associating
 441 -- them with the things in the input list from left to right. The
 442 -- final result type is returned, along with the resulting pairs of
 443 -- objects and types, albeit with the list of pairs in reverse order.
 444 -- Panics if there are not enough argument types for the input list.
 445 zipFunTys :: Outputable a => [a] -> Type -> ([(a, Type)], Type)
 446 zipFunTys orig_xs orig_ty = split [] orig_xs orig_ty orig_ty
 447   where
 448     split acc []     nty _                 = (reverse acc, nty)
 449     split acc xs     nty ty
 450           | Just ty' <- coreView ty        = split acc xs nty ty'
 451     split acc (x:xs) _   (FunTy arg res)   = split ((x,arg):acc) xs res res
 452     split _   _      _   _                 = pprPanic "zipFunTys" (ppr orig_xs <+> ppr orig_ty)
 453
 454 funResultTy :: Type -> Type
 455 -- ^ Extract the function result type and panic if that is not possible
 456 funResultTy ty | Just ty' <- coreView ty = funResultTy ty'
 457 funResultTy (FunTy _arg res)  = res
 458 funResultTy ty                = pprPanic "funResultTy" (ppr ty)
 459
 460 funArgTy :: Type -> Type
 461 -- ^ Extract the function argument type and panic if that is not possible
 462 funArgTy ty | Just ty' <- coreView ty = funArgTy ty'
 463 funArgTy (FunTy arg _res)  = arg
 464 funArgTy ty                = pprPanic "funArgTy" (ppr ty)
 465 \end{code}
 466
 467 ---------------------------------------------------------------------
 468                                 TyConApp
 469                                 ~~~~~~~~
 470
 471 \begin{code}
 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 -- | The same as @fst . splitTyConApp@
 477 tyConAppTyCon :: Type -> TyCon
 478 tyConAppTyCon ty = fst (splitTyConApp ty)
 479
 480 -- | The same as @snd . splitTyConApp@
 481 tyConAppArgs :: Type -> [Type]
 482 tyConAppArgs ty = snd (splitTyConApp ty)
 483
 484 -- | Attempts to tease a type apart into a type constructor and the application
 485 -- of a number of arguments to that constructor. Panics if that is not possible.
 486 -- See also 'splitTyConApp_maybe'
 487 splitTyConApp :: Type -> (TyCon, [Type])
 488 splitTyConApp ty = case splitTyConApp_maybe ty of
 489                         Just stuff -> stuff
 490                         Nothing    -> pprPanic "splitTyConApp" (ppr ty)
 491
 492 -- | Attempts to tease a type apart into a type constructor and the application
 493 -- of a number of arguments to that constructor
 494 splitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
 495 splitTyConApp_maybe ty | Just ty' <- coreView ty = splitTyConApp_maybe ty'
 496 splitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
 497 splitTyConApp_maybe (FunTy arg res)   = Just (funTyCon, [arg,res])
 498 splitTyConApp_maybe _                 = Nothing
 499
 500 newTyConInstRhs :: TyCon -> [Type] -> Type
 501 -- ^ Unwrap one 'layer' of newtype on a type constructor and its arguments, using an
 502 -- eta-reduced version of the @newtype@ if possible
 503 newTyConInstRhs tycon tys
 504     = ASSERT2( equalLength tvs tys1, ppr tycon $$ ppr tys $$ ppr tvs )
 505       mkAppTys (substTyWith tvs tys1 ty) tys2
 506   where
 507     (tvs, ty)    = newTyConEtadRhs tycon
 508     (tys1, tys2) = splitAtList tvs tys
 509 \end{code}
 510
 511
 512 ---------------------------------------------------------------------
 513                                 SynTy
 514                                 ~~~~~
 515
 516 Notes on type synonyms
 517 ~~~~~~~~~~~~~~~~~~~~~~
 518 The various "split" functions (splitFunTy, splitRhoTy, splitForAllTy) try
 519 to return type synonyms whereever possible. Thus
 520
 521         type Foo a = a -> a
 522
 523 we want
 524         splitFunTys (a -> Foo a) = ([a], Foo a)
 525 not                                ([a], a -> a)
 526
 527 The reason is that we then get better (shorter) type signatures in
 528 interfaces.  Notably this plays a role in tcTySigs in TcBinds.lhs.
 529
 530
 531 Note [Expanding newtypes]
 532 ~~~~~~~~~~~~~~~~~~~~~~~~~
 533 When expanding a type to expose a data-type constructor, we need to be
 534 careful about newtypes, lest we fall into an infinite loop. Here are
 535 the key examples:
 536
 537   newtype Id  x = MkId x
 538   newtype Fix f = MkFix (f (Fix f))
 539   newtype T     = MkT (T -> T)
 540
 541   Type           Expansion
 542  --------------------------
 543   T              T -> T
 544   Fix Maybe      Maybe (Fix Maybe)
 545   Id (Id Int)    Int
 546   Fix Id         NO NO NO
 547
 548 Notice that we can expand T, even though it's recursive.
 549 And we can expand Id (Id Int), even though the Id shows up
 550 twice at the outer level.
 551
 552 So, when expanding, we keep track of when we've seen a recursive
 553 newtype at outermost level; and bale out if we see it again.
 554
 555
 556                 Representation types
 557                 ~~~~~~~~~~~~~~~~~~~~
 558
 559 \begin{code}
 560 -- | Looks through:
 561 --
 562 --      1. For-alls
 563 --      2. Synonyms
 564 --      3. Predicates
 565 --      4. All newtypes, including recursive ones, but not newtype families
 566 --
 567 -- It's useful in the back end of the compiler.
 568 repType :: Type -> Type
 569 -- Only applied to types of kind *; hence tycons are saturated
 570 repType ty
 571   = go [] ty
 572   where
 573     go :: [TyCon] -> Type -> Type
 574     go rec_nts (ForAllTy _ ty)          -- Look through foralls
 575         = go rec_nts ty
 576
 577     go rec_nts (PredTy p)               -- Expand predicates
 578         = go rec_nts (predTypeRep p)
 579
 580     go rec_nts (TyConApp tc tys)        -- Expand newtypes and synonyms
 581       | Just (tenv, rhs, tys') <- coreExpandTyCon_maybe tc tys
 582       = go rec_nts (mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys')
 583
 584       | Just (rec_nts', ty') <- carefullySplitNewType_maybe rec_nts tc tys
 585       = go rec_nts' ty'
 586
 587     go _ ty = ty
 588
 589
 590 carefullySplitNewType_maybe :: [TyCon] -> TyCon -> [Type] -> Maybe ([TyCon],Type)
 591 -- Return the representation of a newtype, unless
 592 -- we've seen it already: see Note [Expanding newtypes]
 593 carefullySplitNewType_maybe rec_nts tc tys
 594   | isNewTyCon tc
 595   , not (tc `elem` rec_nts)  = Just (rec_nts', newTyConInstRhs tc tys)
 596   | otherwise                = Nothing
 597   where
 598     rec_nts' | isRecursiveTyCon tc = tc:rec_nts
 599              | otherwise           = rec_nts
 600
 601
 602 -- ToDo: this could be moved to the code generator, using splitTyConApp instead
 603 -- of inspecting the type directly.
 604
 605 -- | Discovers the primitive representation of a more abstract 'Type'
 606 typePrimRep :: Type -> PrimRep
 607 typePrimRep ty = case repType ty of
 608                    TyConApp tc _ -> tyConPrimRep tc
 609                    FunTy _ _     -> PtrRep
 610                    AppTy _ _     -> PtrRep      -- See note below
 611                    TyVarTy _     -> PtrRep
 612                    _             -> pprPanic "typePrimRep" (ppr ty)
 613         -- Types of the form 'f a' must be of kind *, not *#, so
 614         -- we are guaranteed that they are represented by pointers.
 615         -- The reason is that f must have kind *->*, not *->*#, because
 616         -- (we claim) there is no way to constrain f's kind any other
 617         -- way.
 618 \end{code}
 619
 620
 621 ---------------------------------------------------------------------
 622                                 ForAllTy
 623                                 ~~~~~~~~
 624
 625 \begin{code}
 626 mkForAllTy :: TyVar -> Type -> Type
 627 mkForAllTy tyvar ty
 628   = ForAllTy tyvar ty
 629
 630 -- | Wraps foralls over the type using the provided 'TyVar's from left to right
 631 mkForAllTys :: [TyVar] -> Type -> Type
 632 mkForAllTys tyvars ty = foldr ForAllTy ty tyvars
 633
 634 isForAllTy :: Type -> Bool
 635 isForAllTy (ForAllTy _ _) = True
 636 isForAllTy _              = False
 637
 638 -- | Attempts to take a forall type apart, returning the bound type variable
 639 -- and the remainder of the type
 640 splitForAllTy_maybe :: Type -> Maybe (TyVar, Type)
 641 splitForAllTy_maybe ty = splitFAT_m ty
 642   where
 643     splitFAT_m ty | Just ty' <- coreView ty = splitFAT_m ty'
 644     splitFAT_m (ForAllTy tyvar ty)          = Just(tyvar, ty)
 645     splitFAT_m _                            = Nothing
 646
 647 -- | Attempts to take a forall type apart, returning all the immediate such bound
 648 -- type variables and the remainder of the type. Always suceeds, even if that means
 649 -- returning an empty list of 'TyVar's
 650 splitForAllTys :: Type -> ([TyVar], Type)
 651 splitForAllTys ty = split ty ty []
 652    where
 653      split orig_ty ty tvs | Just ty' <- coreView ty = split orig_ty ty' tvs
 654      split _       (ForAllTy tv ty)  tvs = split ty ty (tv:tvs)
 655      split orig_ty _                 tvs = (reverse tvs, orig_ty)
 656
 657 -- | Equivalent to @snd . splitForAllTys@
 658 dropForAlls :: Type -> Type
 659 dropForAlls ty = snd (splitForAllTys ty)
 660 \end{code}
 661
 662 -- (mkPiType now in CoreUtils)
 663
 664 applyTy, applyTys
 665 ~~~~~~~~~~~~~~~~~
 666
 667 \begin{code}
 668 -- | Instantiate a forall type with one or more type arguments.
 669 -- Used when we have a polymorphic function applied to type args:
 670 --
 671 -- > f t1 t2
 672 --
 673 -- We use @applyTys type-of-f [t1,t2]@ to compute the type of the expression.
 674 -- Panics if no application is possible.
 675 applyTy :: Type -> Type -> Type
 676 applyTy ty arg | Just ty' <- coreView ty = applyTy ty' arg
 677 applyTy (ForAllTy tv ty) arg = substTyWith [tv] [arg] ty
 678 applyTy _                _   = panic "applyTy"
 679
 680 applyTys :: Type -> [Type] -> Type
 681 -- ^ This function is interesting because:
 682 --
 683 --      1. The function may have more for-alls than there are args
 684 --
 685 --      2. Less obviously, it may have fewer for-alls
 686 --
 687 -- For case 2. think of:
 688 --
 689 -- > applyTys (forall a.a) [forall b.b, Int]
 690 --
 691 -- This really can happen, via dressing up polymorphic types with newtype
 692 -- clothing.  Here's an example:
 693 --
 694 -- > newtype R = R (forall a. a->a)
 695 -- > foo = case undefined :: R of
 696 -- >            R f -> f ()
 697
 698 applyTys ty args = applyTysD empty ty args
 699
 700 applyTysD :: SDoc -> Type -> [Type] -> Type     -- Debug version
 701 applyTysD _   orig_fun_ty []      = orig_fun_ty
 702 applyTysD doc orig_fun_ty arg_tys
 703   | n_tvs == n_args     -- The vastly common case
 704   = substTyWith tvs arg_tys rho_ty
 705   | n_tvs > n_args      -- Too many for-alls
 706   = substTyWith (take n_args tvs) arg_tys
 707                 (mkForAllTys (drop n_args tvs) rho_ty)
 708   | otherwise           -- Too many type args
 709   = ASSERT2( n_tvs > 0, doc $$ ppr orig_fun_ty )        -- Zero case gives infnite loop!
 710     applyTysD doc (substTyWith tvs (take n_tvs arg_tys) rho_ty)
 711                   (drop n_tvs arg_tys)
 712   where
 713     (tvs, rho_ty) = splitForAllTys orig_fun_ty
 714     n_tvs = length tvs
 715     n_args = length arg_tys
 716 \end{code}
 717
 718
 719 %************************************************************************
 720 %*                                                                      *
 721                          Pred
 722 %*                                                                      *
 723 %************************************************************************
 724
 725 Polymorphic functions over Pred
 726
 727 \begin{code}
 728 allPred :: (a -> Bool) -> Pred a -> Bool
 729 allPred p (ClassP _ ts)  = all p ts
 730 allPred p (IParam _ t)   = p t
 731 allPred p (EqPred t1 t2) = p t1 && p t2
 732
 733 isClassPred :: Pred a -> Bool
 734 isClassPred (ClassP {}) = True
 735 isClassPred _            = False
 736
 737 isEqPred :: Pred a -> Bool
 738 isEqPred (EqPred {}) = True
 739 isEqPred _           = False
 740
 741 isIPPred :: Pred a -> Bool
 742 isIPPred (IParam {}) = True
 743 isIPPred _           = False
 744 \end{code}
 745
 746 Make PredTypes
 747
 748 \begin{code}
 749 mkPredTy :: PredType -> Type
 750 mkPredTy pred = PredTy pred
 751
 752 mkPredTys :: ThetaType -> [Type]
 753 mkPredTys preds = map PredTy preds
 754
 755 predTypeRep :: PredType -> Type
 756 -- ^ Convert a 'PredType' to its representation type. However, it unwraps
 757 -- only the outermost level; for example, the result might be a newtype application
 758 predTypeRep (IParam _ ty)     = ty
 759 predTypeRep (ClassP clas tys) = mkTyConApp (classTyCon clas) tys
 760 predTypeRep (EqPred ty1 ty2)  = mkTyConApp eqPredPrimTyCon [ty1,ty2]
 761
 762 splitPredTy_maybe :: Type -> Maybe PredType
 763 -- Returns Just for predicates only
 764 splitPredTy_maybe ty | Just ty' <- tcView ty = splitPredTy_maybe ty'
 765 splitPredTy_maybe (PredTy p)    = Just p
 766 splitPredTy_maybe _             = Nothing
 767
 768 isPredTy :: Type -> Bool
 769 isPredTy ty = isJust (splitPredTy_maybe ty)
 770 \end{code}
 771
 772 --------------------- Equality types ---------------------------------
 773 \begin{code}
 774 isReflPredTy :: Type -> Bool
 775 isReflPredTy ty = case splitPredTy_maybe ty of
 776                     Just (EqPred ty1 ty2) -> ty1 `eqType` ty2
 777                     _                     -> False
 778
 779 splitEqPredTy_maybe :: Type -> Maybe (Type,Type)
 780 splitEqPredTy_maybe ty = case splitPredTy_maybe ty of
 781                             Just (EqPred ty1 ty2) -> Just (ty1,ty2)
 782                             _                     -> Nothing
 783
 784 isEqPredTy :: Type -> Bool
 785 isEqPredTy ty = case splitPredTy_maybe ty of
 786                   Just (EqPred {}) -> True
 787                   _                -> False
 788
 789 -- | Creates a type equality predicate
 790 mkEqPred :: (a, a) -> Pred a
 791 mkEqPred (ty1, ty2) = EqPred ty1 ty2
 792 \end{code}
 793
 794 --------------------- Dictionary types ---------------------------------
 795 \begin{code}
 796 mkClassPred :: Class -> [Type] -> PredType
 797 mkClassPred clas tys = ClassP clas tys
 798
 799 isDictTy :: Type -> Bool
 800 isDictTy ty = case splitPredTy_maybe ty of
 801                 Just p  -> isClassPred p
 802                 Nothing -> False
 803
 804 isTyVarClassPred :: PredType -> Bool
 805 isTyVarClassPred (ClassP _ tys) = all isTyVarTy tys
 806 isTyVarClassPred _              = False
 807
 808 getClassPredTys_maybe :: PredType -> Maybe (Class, [Type])
 809 getClassPredTys_maybe (ClassP clas tys) = Just (clas, tys)
 810 getClassPredTys_maybe _                 = Nothing
 811
 812 getClassPredTys :: PredType -> (Class, [Type])
 813 getClassPredTys (ClassP clas tys) = (clas, tys)
 814 getClassPredTys _ = panic "getClassPredTys"
 815
 816 mkDictTy :: Class -> [Type] -> Type
 817 mkDictTy clas tys = mkPredTy (ClassP clas tys)
 818
 819 isDictLikeTy :: Type -> Bool
 820 -- Note [Dictionary-like types]
 821 isDictLikeTy ty | Just ty' <- tcView ty = isDictTy ty'
 822 isDictLikeTy (PredTy p) = isClassPred p
 823 isDictLikeTy (TyConApp tc tys)
 824   | isTupleTyCon tc     = all isDictLikeTy tys
 825 isDictLikeTy _          = False
 826 \end{code}
 827
 828 Note [Dictionary-like types]
 829 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 830 Being "dictionary-like" means either a dictionary type or a tuple thereof.
 831 In GHC 6.10 we build implication constraints which construct such tuples,
 832 and if we land up with a binding
 833     t :: (C [a], Eq [a])
 834     t = blah
 835 then we want to treat t as cheap under "-fdicts-cheap" for example.
 836 (Implication constraints are normally inlined, but sadly not if the
 837 occurrence is itself inside an INLINE function!  Until we revise the
 838 handling of implication constraints, that is.)  This turned out to
 839 be important in getting good arities in DPH code.  Example:
 840
 841     class C a
 842     class D a where { foo :: a -> a }
 843     instance C a => D (Maybe a) where { foo x = x }
 844
 845     bar :: (C a, C b) => a -> b -> (Maybe a, Maybe b)
 846     {-# INLINE bar #-}
 847     bar x y = (foo (Just x), foo (Just y))
 848
 849 Then 'bar' should jolly well have arity 4 (two dicts, two args), but
 850 we ended up with something like
 851    bar = __inline_me__ (\d1,d2. let t :: (D (Maybe a), D (Maybe b)) = ...
 852                                 in \x,y. <blah>)
 853
 854 This is all a bit ad-hoc; eg it relies on knowing that implication
 855 constraints build tuples.
 856
 857 --------------------- Implicit parameters ---------------------------------
 858
 859 \begin{code}
 860 mkIPPred :: IPName Name -> Type -> PredType
 861 mkIPPred ip ty = IParam ip ty
 862 \end{code}
 863
 864 %************************************************************************
 865 %*                                                                      *
 866                    Size
 867 %*                                                                      *
 868 %************************************************************************
 869
 870 \begin{code}
 871 typeSize :: Type -> Int
 872 typeSize (TyVarTy _)     = 1
 873 typeSize (AppTy t1 t2)   = typeSize t1 + typeSize t2
 874 typeSize (FunTy t1 t2)   = typeSize t1 + typeSize t2
 875 typeSize (PredTy p)      = predSize typeSize p
 876 typeSize (ForAllTy _ t)  = 1 + typeSize t
 877 typeSize (TyConApp _ ts) = 1 + sum (map typeSize ts)
 878 \end{code}
 879
 880
 881 %************************************************************************
 882 %*                                                                      *
 883 \subsection{Type families}
 884 %*                                                                      *
 885 %************************************************************************
 886
 887 \begin{code}
 888 -- | Finds type family instances occuring in a type after expanding synonyms.
 889 tyFamInsts :: Type -> [(TyCon, [Type])]
 890 tyFamInsts ty
 891   | Just exp_ty <- tcView ty    = tyFamInsts exp_ty
 892 tyFamInsts (TyVarTy _)          = []
 893 tyFamInsts (TyConApp tc tys)
 894   | isSynFamilyTyCon tc           = [(tc, tys)]
 895   | otherwise                   = concat (map tyFamInsts tys)
 896 tyFamInsts (FunTy ty1 ty2)      = tyFamInsts ty1 ++ tyFamInsts ty2
 897 tyFamInsts (AppTy ty1 ty2)      = tyFamInsts ty1 ++ tyFamInsts ty2
 898 tyFamInsts (ForAllTy _ ty)      = tyFamInsts ty
 899 tyFamInsts (PredTy pty)         = predFamInsts pty
 900
 901 -- | Finds type family instances occuring in a predicate type after expanding
 902 -- synonyms.
 903 predFamInsts :: PredType -> [(TyCon, [Type])]
 904 predFamInsts (ClassP _cla tys) = concat (map tyFamInsts tys)
 905 predFamInsts (IParam _ ty)     = tyFamInsts ty
 906 predFamInsts (EqPred ty1 ty2)  = tyFamInsts ty1 ++ tyFamInsts ty2
 907
 908 mkFamilyTyConApp :: TyCon -> [Type] -> Type
 909 -- ^ Given a family instance TyCon and its arg types, return the
 910 -- corresponding family type.  E.g:
 911 --
 912 -- > data family T a
 913 -- > data instance T (Maybe b) = MkT b
 914 --
 915 -- Where the instance tycon is :RTL, so:
 916 --
 917 -- > mkFamilyTyConApp :RTL Int  =  T (Maybe Int)
 918 mkFamilyTyConApp tc tys
 919   | Just (fam_tc, fam_tys) <- tyConFamInst_maybe tc
 920   , let fam_subst = zipTopTvSubst (tyConTyVars tc) tys
 921   = mkTyConApp fam_tc (substTys fam_subst fam_tys)
 922   | otherwise
 923   = mkTyConApp tc tys
 924
 925 -- | Pretty prints a 'TyCon', using the family instance in case of a
 926 -- representation tycon.  For example:
 927 --
 928 -- > data T [a] = ...
 929 --
 930 -- In that case we want to print @T [a]@, where @T@ is the family 'TyCon'
 931 pprSourceTyCon :: TyCon -> SDoc
 932 pprSourceTyCon tycon
 933   | Just (fam_tc, tys) <- tyConFamInst_maybe tycon
 934   = ppr $ fam_tc `TyConApp` tys        -- can't be FunTyCon
 935   | otherwise
 936   = ppr tycon
 937 \end{code}
 938
 939 %************************************************************************
 940 %*                                                                      *
 941 \subsection{Liftedness}
 942 %*                                                                      *
 943 %************************************************************************
 944
 945 \begin{code}
 946 -- | See "Type#type_classification" for what an unlifted type is
 947 isUnLiftedType :: Type -> Bool
 948         -- isUnLiftedType returns True for forall'd unlifted types:
 949         --      x :: forall a. Int#
 950         -- I found bindings like these were getting floated to the top level.
 951         -- They are pretty bogus types, mind you.  It would be better never to
 952         -- construct them
 953
 954 isUnLiftedType ty | Just ty' <- coreView ty = isUnLiftedType ty'
 955 isUnLiftedType (ForAllTy _ ty)   = isUnLiftedType ty
 956 isUnLiftedType (PredTy p)        = isEqPred p
 957 isUnLiftedType (TyConApp tc _)   = isUnLiftedTyCon tc
 958 isUnLiftedType _                 = False
 959
 960 isUnboxedTupleType :: Type -> Bool
 961 isUnboxedTupleType ty = case splitTyConApp_maybe ty of
 962                            Just (tc, _ty_args) -> isUnboxedTupleTyCon tc
 963                            _                   -> False
 964
 965 -- | See "Type#type_classification" for what an algebraic type is.
 966 -- Should only be applied to /types/, as opposed to e.g. partially
 967 -- saturated type constructors
 968 isAlgType :: Type -> Bool
 969 isAlgType ty
 970   = case splitTyConApp_maybe ty of
 971       Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
 972                             isAlgTyCon tc
 973       _other             -> False
 974
 975 -- | See "Type#type_classification" for what an algebraic type is.
 976 -- Should only be applied to /types/, as opposed to e.g. partially
 977 -- saturated type constructors. Closed type constructors are those
 978 -- with a fixed right hand side, as opposed to e.g. associated types
 979 isClosedAlgType :: Type -> Bool
 980 isClosedAlgType ty
 981   = case splitTyConApp_maybe ty of
 982       Just (tc, ty_args) | isAlgTyCon tc && not (isFamilyTyCon tc)
 983              -> ASSERT2( ty_args `lengthIs` tyConArity tc, ppr ty ) True
 984       _other -> False
 985 \end{code}
 986
 987 \begin{code}
 988 -- | Computes whether an argument (or let right hand side) should
 989 -- be computed strictly or lazily, based only on its type.
 990 -- Works just like 'isUnLiftedType', except that it has a special case
 991 -- for dictionaries (i.e. does not work purely on representation types)
 992
 993 -- Since it takes account of class 'PredType's, you might think
 994 -- this function should be in 'TcType', but 'isStrictType' is used by 'DataCon',
 995 -- which is below 'TcType' in the hierarchy, so it's convenient to put it here.
 996 isStrictType :: Type -> Bool
 997 isStrictType (PredTy pred)     = isStrictPred pred
 998 isStrictType ty | Just ty' <- coreView ty = isStrictType ty'
 999 isStrictType (ForAllTy _ ty)   = isStrictType ty
1000 isStrictType (TyConApp tc _)   = isUnLiftedTyCon tc
1001 isStrictType _                 = False
1002
1003 -- | We may be strict in dictionary types, but only if it
1004 -- has more than one component.
1005 --
1006 -- (Being strict in a single-component dictionary risks
1007 --  poking the dictionary component, which is wrong.)
1008 isStrictPred :: PredType -> Bool
1009 isStrictPred (ClassP clas _) = opt_DictsStrict && not (isNewTyCon (classTyCon clas))
1010 isStrictPred (EqPred {})     = True
1011 isStrictPred (IParam {})     = False
1012 \end{code}
1013
1014 \begin{code}
1015 isPrimitiveType :: Type -> Bool
1016 -- ^ Returns true of types that are opaque to Haskell.
1017 -- Most of these are unlifted, but now that we interact with .NET, we
1018 -- may have primtive (foreign-imported) types that are lifted
1019 isPrimitiveType ty = case splitTyConApp_maybe ty of
1020                         Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
1021                                               isPrimTyCon tc
1022                         _                  -> False
1023 \end{code}
1024
1025
1026 %************************************************************************
1027 %*                                                                      *
1028           The "exact" free variables of a type
1029 %*                                                                      *
1030 %************************************************************************
1031
1032 Note [Silly type synonym]
1033 ~~~~~~~~~~~~~~~~~~~~~~~~~
1034 Consider
1035         type T a = Int
1036 What are the free tyvars of (T x)?  Empty, of course!
1037 Here's the example that Ralf Laemmel showed me:
1038         foo :: (forall a. C u a -> C u a) -> u
1039         mappend :: Monoid u => u -> u -> u
1040
1041         bar :: Monoid u => u
1042         bar = foo (\t -> t `mappend` t)
1043 We have to generalise at the arg to f, and we don't
1044 want to capture the constraint (Monad (C u a)) because
1045 it appears to mention a.  Pretty silly, but it was useful to him.
1046
1047 exactTyVarsOfType is used by the type checker to figure out exactly
1048 which type variables are mentioned in a type.  It's also used in the
1049 smart-app checking code --- see TcExpr.tcIdApp
1050
1051 On the other hand, consider a *top-level* definition
1052         f = (\x -> x) :: T a -> T a
1053 If we don't abstract over 'a' it'll get fixed to GHC.Prim.Any, and then
1054 if we have an application like (f "x") we get a confusing error message
1055 involving Any.  So the conclusion is this: when generalising
1056   - at top level use tyVarsOfType
1057   - in nested bindings use exactTyVarsOfType
1058 See Trac #1813 for example.
1059
1060 \begin{code}
1061 exactTyVarsOfType :: Type -> TyVarSet
1062 -- Find the free type variables (of any kind)
1063 -- but *expand* type synonyms.  See Note [Silly type synonym] above.
1064 exactTyVarsOfType ty
1065   = go ty
1066   where
1067     go ty | Just ty' <- tcView ty = go ty'      -- This is the key line
1068     go (TyVarTy tv)         = unitVarSet tv
1069     go (TyConApp _ tys)     = exactTyVarsOfTypes tys
1070     go (PredTy ty)          = go_pred ty
1071     go (FunTy arg res)      = go arg `unionVarSet` go res
1072     go (AppTy fun arg)      = go fun `unionVarSet` go arg
1073     go (ForAllTy tyvar ty)  = delVarSet (go ty) tyvar
1074
1075     go_pred (IParam _ ty)    = go ty
1076     go_pred (ClassP _ tys)   = exactTyVarsOfTypes tys
1077     go_pred (EqPred ty1 ty2) = go ty1 `unionVarSet` go ty2
1078
1079 exactTyVarsOfTypes :: [Type] -> TyVarSet
1080 exactTyVarsOfTypes tys = foldr (unionVarSet . exactTyVarsOfType) emptyVarSet tys
1081 \end{code}
1082
1083
1084 %************************************************************************
1085 %*                                                                      *
1086 \subsection{Sequencing on types}
1087 %*                                                                      *
1088 %************************************************************************
1089
1090 \begin{code}
1091 seqType :: Type -> ()
1092 seqType (TyVarTy tv)      = tv `seq` ()
1093 seqType (AppTy t1 t2)     = seqType t1 `seq` seqType t2
1094 seqType (FunTy t1 t2)     = seqType t1 `seq` seqType t2
1095 seqType (PredTy p)        = seqPred seqType p
1096 seqType (TyConApp tc tys) = tc `seq` seqTypes tys
1097 seqType (ForAllTy tv ty)  = tv `seq` seqType ty
1098
1099 seqTypes :: [Type] -> ()
1100 seqTypes []       = ()
1101 seqTypes (ty:tys) = seqType ty `seq` seqTypes tys
1102
1103 seqPred :: (a -> ()) -> Pred a -> ()
1104 seqPred seqt (ClassP c tys)   = c `seq` foldr (seq . seqt) () tys
1105 seqPred seqt (IParam n ty)    = n `seq` seqt ty
1106 seqPred seqt (EqPred ty1 ty2) = seqt ty1 `seq` seqt ty2
1107 \end{code}
1108
1109
1110 %************************************************************************
1111 %*                                                                      *
1112                 Comparision for types
1113         (We don't use instances so that we know where it happens)
1114 %*                                                                      *
1115 %************************************************************************
1116
1117 \begin{code}
1118 eqKind :: Kind -> Kind -> Bool
1119 eqKind = eqType
1120
1121 eqType :: Type -> Type -> Bool
1122 -- ^ Type equality on source types. Does not look through @newtypes@ or
1123 -- 'PredType's, but it does look through type synonyms.
1124 eqType t1 t2 = isEqual $ cmpType t1 t2
1125
1126 eqTypeX :: RnEnv2 -> Type -> Type -> Bool
1127 eqTypeX env t1 t2 = isEqual $ cmpTypeX env t1 t2
1128
1129 eqTypes :: [Type] -> [Type] -> Bool
1130 eqTypes tys1 tys2 = isEqual $ cmpTypes tys1 tys2
1131
1132 eqPred :: PredType -> PredType -> Bool
1133 eqPred p1 p2 = isEqual $ cmpPred p1 p2
1134
1135 eqPredX :: RnEnv2 -> PredType -> PredType -> Bool
1136 eqPredX env p1 p2 = isEqual $ cmpPredX env p1 p2
1137 \end{code}
1138
1139 Now here comes the real worker
1140
1141 \begin{code}
1142 cmpType :: Type -> Type -> Ordering
1143 cmpType t1 t2 = cmpTypeX rn_env t1 t2
1144   where
1145     rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfType t1 `unionVarSet` tyVarsOfType t2))
1146
1147 cmpTypes :: [Type] -> [Type] -> Ordering
1148 cmpTypes ts1 ts2 = cmpTypesX rn_env ts1 ts2
1149   where
1150     rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfTypes ts1 `unionVarSet` tyVarsOfTypes ts2))
1151
1152 cmpPred :: PredType -> PredType -> Ordering
1153 cmpPred p1 p2 = cmpPredX rn_env p1 p2
1154   where
1155     rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfPred p1 `unionVarSet` tyVarsOfPred p2))
1156
1157 cmpTypeX :: RnEnv2 -> Type -> Type -> Ordering  -- Main workhorse
1158 cmpTypeX env t1 t2 | Just t1' <- coreView t1 = cmpTypeX env t1' t2
1159                    | Just t2' <- coreView t2 = cmpTypeX env t1 t2'
1160 -- We expand predicate types, because in Core-land we have
1161 -- lots of definitions like
1162 --      fOrdBool :: Ord Bool
1163 --      fOrdBool = D:Ord .. .. ..
1164 -- So the RHS has a data type
1165
1166 cmpTypeX env (TyVarTy tv1)       (TyVarTy tv2)       = rnOccL env tv1 `compare` rnOccR env tv2
1167 cmpTypeX env (ForAllTy tv1 t1)   (ForAllTy tv2 t2)   = cmpTypeX (rnBndr2 env tv1 tv2) t1 t2
1168 cmpTypeX env (AppTy s1 t1)       (AppTy s2 t2)       = cmpTypeX env s1 s2 `thenCmp` cmpTypeX env t1 t2
1169 cmpTypeX env (FunTy s1 t1)       (FunTy s2 t2)       = cmpTypeX env s1 s2 `thenCmp` cmpTypeX env t1 t2
1170 cmpTypeX env (PredTy p1)         (PredTy p2)         = cmpPredX env p1 p2
1171 cmpTypeX env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` cmpTypesX env tys1 tys2
1172
1173     -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < ForAllTy < PredTy
1174 cmpTypeX _ (AppTy _ _)    (TyVarTy _)    = GT
1175
1176 cmpTypeX _ (FunTy _ _)    (TyVarTy _)    = GT
1177 cmpTypeX _ (FunTy _ _)    (AppTy _ _)    = GT
1178
1179 cmpTypeX _ (TyConApp _ _) (TyVarTy _)    = GT
1180 cmpTypeX _ (TyConApp _ _) (AppTy _ _)    = GT
1181 cmpTypeX _ (TyConApp _ _) (FunTy _ _)    = GT
1182
1183 cmpTypeX _ (ForAllTy _ _) (TyVarTy _)    = GT
1184 cmpTypeX _ (ForAllTy _ _) (AppTy _ _)    = GT
1185 cmpTypeX _ (ForAllTy _ _) (FunTy _ _)    = GT
1186 cmpTypeX _ (ForAllTy _ _) (TyConApp _ _) = GT
1187
1188 cmpTypeX _ (PredTy _)     _              = GT
1189
1190 cmpTypeX _ _              _              = LT
1191
1192 -------------
1193 cmpTypesX :: RnEnv2 -> [Type] -> [Type] -> Ordering
1194 cmpTypesX _   []        []        = EQ
1195 cmpTypesX env (t1:tys1) (t2:tys2) = cmpTypeX env t1 t2 `thenCmp` cmpTypesX env tys1 tys2
1196 cmpTypesX _   []        _         = LT
1197 cmpTypesX _   _         []        = GT
1198
1199 -------------
1200 cmpPredX :: RnEnv2 -> PredType -> PredType -> Ordering
1201 cmpPredX env (IParam n1 ty1) (IParam n2 ty2) = (n1 `compare` n2) `thenCmp` cmpTypeX env ty1 ty2
1202         -- Compare names only for implicit parameters
1203         -- This comparison is used exclusively (I believe)
1204         -- for the Avails finite map built in TcSimplify
1205         -- If the types differ we keep them distinct so that we see
1206         -- a distinct pair to run improvement on
1207 cmpPredX env (ClassP c1 tys1) (ClassP c2 tys2) = (c1 `compare` c2) `thenCmp` (cmpTypesX env tys1 tys2)
1208 cmpPredX env (EqPred ty1 ty2) (EqPred ty1' ty2') = (cmpTypeX env ty1 ty1') `thenCmp` (cmpTypeX env ty2 ty2')
1209
1210 -- Constructor order: IParam < ClassP < EqPred
1211 cmpPredX _   (IParam {})     _              = LT
1212 cmpPredX _   (ClassP {})    (IParam {})     = GT
1213 cmpPredX _   (ClassP {})    (EqPred {})     = LT
1214 cmpPredX _   (EqPred {})    _               = GT
1215 \end{code}
1216
1217 PredTypes are used as a FM key in TcSimplify,
1218 so we take the easy path and make them an instance of Ord
1219
1220 \begin{code}
1221 instance Eq  PredType where { (==)    = eqPred }
1222 instance Ord PredType where { compare = cmpPred }
1223 \end{code}
1224
1225
1226 %************************************************************************
1227 %*                                                                      *
1228                 Type substitutions
1229 %*                                                                      *
1230 %************************************************************************
1231
1232 \begin{code}
1233 emptyTvSubstEnv :: TvSubstEnv
1234 emptyTvSubstEnv = emptyVarEnv
1235
1236 composeTvSubst :: InScopeSet -> TvSubstEnv -> TvSubstEnv -> TvSubstEnv
1237 -- ^ @(compose env1 env2)(x)@ is @env1(env2(x))@; i.e. apply @env2@ then @env1@.
1238 -- It assumes that both are idempotent.
1239 -- Typically, @env1@ is the refinement to a base substitution @env2@
1240 composeTvSubst in_scope env1 env2
1241   = env1 `plusVarEnv` mapVarEnv (substTy subst1) env2
1242         -- First apply env1 to the range of env2
1243         -- Then combine the two, making sure that env1 loses if
1244         -- both bind the same variable; that's why env1 is the
1245         --  *left* argument to plusVarEnv, because the right arg wins
1246   where
1247     subst1 = TvSubst in_scope env1
1248
1249 emptyTvSubst :: TvSubst
1250 emptyTvSubst = TvSubst emptyInScopeSet emptyTvSubstEnv
1251
1252 isEmptyTvSubst :: TvSubst -> Bool
1253          -- See Note [Extending the TvSubstEnv]
1254 isEmptyTvSubst (TvSubst _ tenv) = isEmptyVarEnv tenv
1255
1256 mkTvSubst :: InScopeSet -> TvSubstEnv -> TvSubst
1257 mkTvSubst = TvSubst
1258
1259 getTvSubstEnv :: TvSubst -> TvSubstEnv
1260 getTvSubstEnv (TvSubst _ env) = env
1261
1262 getTvInScope :: TvSubst -> InScopeSet
1263 getTvInScope (TvSubst in_scope _) = in_scope
1264
1265 isInScope :: Var -> TvSubst -> Bool
1266 isInScope v (TvSubst in_scope _) = v `elemInScopeSet` in_scope
1267
1268 notElemTvSubst :: TyCoVar -> TvSubst -> Bool
1269 notElemTvSubst v (TvSubst _ tenv) = not (v `elemVarEnv` tenv)
1270
1271 setTvSubstEnv :: TvSubst -> TvSubstEnv -> TvSubst
1272 setTvSubstEnv (TvSubst in_scope _) tenv = TvSubst in_scope tenv
1273
1274 zapTvSubstEnv :: TvSubst -> TvSubst
1275 zapTvSubstEnv (TvSubst in_scope _) = TvSubst in_scope emptyVarEnv
1276
1277 extendTvInScope :: TvSubst -> Var -> TvSubst
1278 extendTvInScope (TvSubst in_scope tenv) var = TvSubst (extendInScopeSet in_scope var) tenv
1279
1280 extendTvInScopeList :: TvSubst -> [Var] -> TvSubst
1281 extendTvInScopeList (TvSubst in_scope tenv) vars = TvSubst (extendInScopeSetList in_scope vars) tenv
1282
1283 extendTvSubst :: TvSubst -> TyVar -> Type -> TvSubst
1284 extendTvSubst (TvSubst in_scope tenv) tv ty = TvSubst in_scope (extendVarEnv tenv tv ty)
1285
1286 extendTvSubstList :: TvSubst -> [TyVar] -> [Type] -> TvSubst
1287 extendTvSubstList (TvSubst in_scope tenv) tvs tys
1288   = TvSubst in_scope (extendVarEnvList tenv (tvs `zip` tys))
1289
1290 unionTvSubst :: TvSubst -> TvSubst -> TvSubst
1291 -- Works when the ranges are disjoint
1292 unionTvSubst (TvSubst in_scope1 tenv1) (TvSubst in_scope2 tenv2)
1293   = ASSERT( not (tenv1 `intersectsVarEnv` tenv2) )
1294     TvSubst (in_scope1 `unionInScope` in_scope2)
1295             (tenv1     `plusVarEnv`   tenv2)
1296
1297 -- mkOpenTvSubst and zipOpenTvSubst generate the in-scope set from
1298 -- the types given; but it's just a thunk so with a bit of luck
1299 -- it'll never be evaluated
1300
1301 -- Note [Generating the in-scope set for a substitution]
1302 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1303 -- If we want to substitute [a -> ty1, b -> ty2] I used to
1304 -- think it was enough to generate an in-scope set that includes
1305 -- fv(ty1,ty2).  But that's not enough; we really should also take the
1306 -- free vars of the type we are substituting into!  Example:
1307 --      (forall b. (a,b,x)) [a -> List b]
1308 -- Then if we use the in-scope set {b}, there is a danger we will rename
1309 -- the forall'd variable to 'x' by mistake, getting this:
1310 --      (forall x. (List b, x, x)
1311 -- Urk!  This means looking at all the calls to mkOpenTvSubst....
1312
1313
1314 -- | Generates the in-scope set for the 'TvSubst' from the types in the incoming
1315 -- environment, hence "open"
1316 mkOpenTvSubst :: TvSubstEnv -> TvSubst
1317 mkOpenTvSubst tenv = TvSubst (mkInScopeSet (tyVarsOfTypes (varEnvElts tenv))) tenv
1318
1319 -- | Generates the in-scope set for the 'TvSubst' from the types in the incoming
1320 -- environment, hence "open"
1321 zipOpenTvSubst :: [TyVar] -> [Type] -> TvSubst
1322 zipOpenTvSubst tyvars tys
1323   | debugIsOn && (length tyvars /= length tys)
1324   = pprTrace "zipOpenTvSubst" (ppr tyvars $$ ppr tys) emptyTvSubst
1325   | otherwise
1326   = TvSubst (mkInScopeSet (tyVarsOfTypes tys)) (zipTyEnv tyvars tys)
1327
1328 -- | Called when doing top-level substitutions. Here we expect that the
1329 -- free vars of the range of the substitution will be empty.
1330 mkTopTvSubst :: [(TyVar, Type)] -> TvSubst
1331 mkTopTvSubst prs = TvSubst emptyInScopeSet (mkVarEnv prs)
1332
1333 zipTopTvSubst :: [TyVar] -> [Type] -> TvSubst
1334 zipTopTvSubst tyvars tys
1335   | debugIsOn && (length tyvars /= length tys)
1336   = pprTrace "zipTopTvSubst" (ppr tyvars $$ ppr tys) emptyTvSubst
1337   | otherwise
1338   = TvSubst emptyInScopeSet (zipTyEnv tyvars tys)
1339
1340 zipTyEnv :: [TyVar] -> [Type] -> TvSubstEnv
1341 zipTyEnv tyvars tys
1342   | debugIsOn && (length tyvars /= length tys)
1343   = pprTrace "zipTyEnv" (ppr tyvars $$ ppr tys) emptyVarEnv
1344   | otherwise
1345   = zip_ty_env tyvars tys emptyVarEnv
1346
1347 -- Later substitutions in the list over-ride earlier ones,
1348 -- but there should be no loops
1349 zip_ty_env :: [TyVar] -> [Type] -> TvSubstEnv -> TvSubstEnv
1350 zip_ty_env []       []       env = env
1351 zip_ty_env (tv:tvs) (ty:tys) env = zip_ty_env tvs tys (extendVarEnv env tv ty)
1352         -- There used to be a special case for when
1353         --      ty == TyVarTy tv
1354         -- (a not-uncommon case) in which case the substitution was dropped.
1355         -- But the type-tidier changes the print-name of a type variable without
1356         -- changing the unique, and that led to a bug.   Why?  Pre-tidying, we had
1357         -- a type {Foo t}, where Foo is a one-method class.  So Foo is really a newtype.
1358         -- And it happened that t was the type variable of the class.  Post-tiding,
1359         -- it got turned into {Foo t2}.  The ext-core printer expanded this using
1360         -- sourceTypeRep, but that said "Oh, t == t2" because they have the same unique,
1361         -- and so generated a rep type mentioning t not t2.
1362         --
1363         -- Simplest fix is to nuke the "optimisation"
1364 zip_ty_env tvs      tys      env   = pprTrace "Var/Type length mismatch: " (ppr tvs $$ ppr tys) env
1365 -- zip_ty_env _ _ env = env
1366
1367 instance Outputable TvSubst where
1368   ppr (TvSubst ins tenv)
1369     = brackets $ sep[ ptext (sLit "TvSubst"),
1370                       nest 2 (ptext (sLit "In scope:") <+> ppr ins),
1371                       nest 2 (ptext (sLit "Type env:") <+> ppr tenv) ]
1372 \end{code}
1373
1374 %************************************************************************
1375 %*                                                                      *
1376                 Performing type substitutions
1377 %*                                                                      *
1378 %************************************************************************
1379
1380 \begin{code}
1381 -- | Type substitution making use of an 'TvSubst' that
1382 -- is assumed to be open, see 'zipOpenTvSubst'
1383 substTyWith :: [TyVar] -> [Type] -> Type -> Type
1384 substTyWith tvs tys = ASSERT( length tvs == length tys )
1385                       substTy (zipOpenTvSubst tvs tys)
1386
1387 -- | Type substitution making use of an 'TvSubst' that
1388 -- is assumed to be open, see 'zipOpenTvSubst'
1389 substTysWith :: [TyVar] -> [Type] -> [Type] -> [Type]
1390 substTysWith tvs tys = ASSERT( length tvs == length tys )
1391                        substTys (zipOpenTvSubst tvs tys)
1392
1393 -- | Substitute within a 'Type'
1394 substTy :: TvSubst -> Type  -> Type
1395 substTy subst ty | isEmptyTvSubst subst = ty
1396                  | otherwise            = subst_ty subst ty
1397
1398 -- | Substitute within several 'Type's
1399 substTys :: TvSubst -> [Type] -> [Type]
1400 substTys subst tys | isEmptyTvSubst subst = tys
1401                    | otherwise            = map (subst_ty subst) tys
1402
1403 -- | Substitute within a 'ThetaType'
1404 substTheta :: TvSubst -> ThetaType -> ThetaType
1405 substTheta subst theta
1406   | isEmptyTvSubst subst = theta
1407   | otherwise            = map (substPred subst) theta
1408
1409 -- | Substitute within a 'PredType'
1410 substPred :: TvSubst -> PredType -> PredType
1411 substPred subst (IParam n ty)     = IParam n (subst_ty subst ty)
1412 substPred subst (ClassP clas tys) = ClassP clas (map (subst_ty subst) tys)
1413 substPred subst (EqPred ty1 ty2)  = EqPred (subst_ty subst ty1) (subst_ty subst ty2)
1414
1415 -- | Remove any nested binders mentioning the 'TyVar's in the 'TyVarSet'
1416 deShadowTy :: TyVarSet -> Type -> Type
1417 deShadowTy tvs ty
1418   = subst_ty (mkTvSubst in_scope emptyTvSubstEnv) ty
1419   where
1420     in_scope = mkInScopeSet tvs
1421
1422 subst_ty :: TvSubst -> Type -> Type
1423 -- subst_ty is the main workhorse for type substitution
1424 --
1425 -- Note that the in_scope set is poked only if we hit a forall
1426 -- so it may often never be fully computed
1427 subst_ty subst ty
1428    = go ty
1429   where
1430     go (TyVarTy tv)      = substTyVar subst tv
1431     go (TyConApp tc tys) = let args = map go tys
1432                            in  args `seqList` TyConApp tc args
1433
1434     go (PredTy p)        = PredTy $! (substPred subst p)
1435
1436     go (FunTy arg res)   = (FunTy $! (go arg)) $! (go res)
1437     go (AppTy fun arg)   = mkAppTy (go fun) $! (go arg)
1438                 -- The mkAppTy smart constructor is important
1439                 -- we might be replacing (a Int), represented with App
1440                 -- by [Int], represented with TyConApp
1441     go (ForAllTy tv ty)  = case substTyVarBndr subst tv of
1442                               (subst', tv') ->
1443                                  ForAllTy tv' $! (subst_ty subst' ty)
1444
1445 substTyVar :: TvSubst -> TyVar  -> Type
1446 substTyVar (TvSubst _ tenv) tv
1447   | Just ty  <- lookupVarEnv tenv tv      = ty  -- See Note [Apply Once]
1448   | otherwise = ASSERT( isTyVar tv ) TyVarTy tv
1449   -- We do not require that the tyvar is in scope
1450   -- Reason: we do quite a bit of (substTyWith [tv] [ty] tau)
1451   -- and it's a nuisance to bring all the free vars of tau into
1452   -- scope --- and then force that thunk at every tyvar
1453   -- Instead we have an ASSERT in substTyVarBndr to check for capture
1454
1455 substTyVars :: TvSubst -> [TyVar] -> [Type]
1456 substTyVars subst tvs = map (substTyVar subst) tvs
1457
1458 lookupTyVar :: TvSubst -> TyVar  -> Maybe Type
1459         -- See Note [Extending the TvSubst]
1460 lookupTyVar (TvSubst _ tenv) tv = lookupVarEnv tenv tv
1461
1462 substTyVarBndr :: TvSubst -> TyVar -> (TvSubst, TyVar)
1463 substTyVarBndr subst@(TvSubst in_scope tenv) old_var
1464   = ASSERT2( _no_capture, ppr old_var $$ ppr subst )
1465     (TvSubst (in_scope `extendInScopeSet` new_var) new_env, new_var)
1466   where
1467     new_env | no_change = delVarEnv tenv old_var
1468             | otherwise = extendVarEnv tenv old_var (TyVarTy new_var)
1469
1470     _no_capture = not (new_var `elemVarSet` tyVarsOfTypes (varEnvElts tenv))
1471     -- Check that we are not capturing something in the substitution
1472
1473     no_change = new_var == old_var
1474         -- no_change means that the new_var is identical in
1475         -- all respects to the old_var (same unique, same kind)
1476         -- See Note [Extending the TvSubst]
1477         --
1478         -- In that case we don't need to extend the substitution
1479         -- to map old to new.  But instead we must zap any
1480         -- current substitution for the variable. For example:
1481         --      (\x.e) with id_subst = [x |-> e']
1482         -- Here we must simply zap the substitution for x
1483
1484     new_var = uniqAway in_scope old_var
1485         -- The uniqAway part makes sure the new variable is not already in scope
1486 \end{code}
1487
1488 ----------------------------------------------------
1489 -- Kind Stuff
1490
1491 Kinds
1492 ~~~~~
1493
1494 \begin{code}
1495 -- $kind_subtyping
1496 -- #kind_subtyping#
1497 -- There's a little subtyping at the kind level:
1498 --
1499 -- @
1500 --               ?
1501 --              \/ &#92;
1502 --             \/   &#92;
1503 --            ??   (\#)
1504 --           \/  &#92;
1505 --          \*    \#
1506 -- .
1507 -- Where:        \*    [LiftedTypeKind]   means boxed type
1508 --              \#    [UnliftedTypeKind] means unboxed type
1509 --              (\#)  [UbxTupleKind]     means unboxed tuple
1510 --              ??   [ArgTypeKind]      is the lub of {\*, \#}
1511 --              ?    [OpenTypeKind]     means any type at all
1512 -- @
1513 --
1514 -- In particular:
1515 --
1516 -- > error :: forall a:?. String -> a
1517 -- > (->)  :: ?? -> ? -> \*
1518 -- > (\\(x::t) -> ...)
1519 --
1520 -- Where in the last example @t :: ??@ (i.e. is not an unboxed tuple)
1521
1522 type KindVar = TyVar  -- invariant: KindVar will always be a
1523                       -- TcTyVar with details MetaTv TauTv ...
1524 -- kind var constructors and functions are in TcType
1525
1526 type SimpleKind = Kind
1527 \end{code}
1528
1529 Kind inference
1530 ~~~~~~~~~~~~~~
1531 During kind inference, a kind variable unifies only with
1532 a "simple kind", sk
1533         sk ::= * | sk1 -> sk2
1534 For example
1535         data T a = MkT a (T Int#)
1536 fails.  We give T the kind (k -> *), and the kind variable k won't unify
1537 with # (the kind of Int#).
1538
1539 Type inference
1540 ~~~~~~~~~~~~~~
1541 When creating a fresh internal type variable, we give it a kind to express
1542 constraints on it.  E.g. in (\x->e) we make up a fresh type variable for x,
1543 with kind ??.
1544
1545 During unification we only bind an internal type variable to a type
1546 whose kind is lower in the sub-kind hierarchy than the kind of the tyvar.
1547
1548 When unifying two internal type variables, we collect their kind constraints by
1549 finding the GLB of the two.  Since the partial order is a tree, they only
1550 have a glb if one is a sub-kind of the other.  In that case, we bind the
1551 less-informative one to the more informative one.  Neat, eh?