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