ghc/compiler/types/TypeRep.lhs

   1 %
   2 % (c) The GRASP/AQUA Project, Glasgow University, 1998
   3 %
   4 \section[TypeRep]{Type - friends' interface}
   5
   6 \begin{code}
   7 module TypeRep (
   8         Type(..), TyNote(..), UsageAnn(..),             -- Representation visible to friends
   9         Kind, TyVarSubst,
  10
  11         superKind, superBoxity,                         -- KX and BX respectively
  12         boxedBoxity, unboxedBoxity,                     -- :: BX
  13         openKindCon,                                    -- :: KX
  14         typeCon,                                        -- :: BX -> KX
  15         boxedTypeKind, unboxedTypeKind, openTypeKind,   -- :: KX
  16         mkArrowKind, mkArrowKinds,                      -- :: KX -> KX -> KX
  17
  18         funTyCon
  19     ) where
  20
  21 #include "HsVersions.h"
  22
  23 -- friends:
  24 import Var      ( TyVar, UVar )
  25 import VarEnv
  26 import VarSet
  27
  28 import Name     ( Name, Provenance(..), ExportFlag(..),
  29                   mkWiredInTyConName, mkGlobalName, mkKindOccFS, tcName,
  30                 )
  31 import TyCon    ( TyCon, KindCon,
  32                   mkFunTyCon, mkKindCon, mkSuperKindCon,
  33                 )
  34
  35 -- others
  36 import SrcLoc           ( mkBuiltinSrcLoc )
  37 import PrelNames        ( pREL_GHC )
  38 import Unique           -- quite a few *Keys
  39 import Util             ( thenCmp )
  40 \end{code}
  41
  42 %************************************************************************
  43 %*                                                                      *
  44 \subsection{Type Classifications}
  45 %*                                                                      *
  46 %************************************************************************
  47
  48 A type is
  49
  50         *unboxed*       iff its representation is other than a pointer
  51                         Unboxed types cannot instantiate a type variable.
  52                         Unboxed types are always unlifted.
  53
  54         *lifted*        A type is lifted iff it has bottom as an element.
  55                         Closures always have lifted types:  i.e. any
  56                         let-bound identifier in Core must have a lifted
  57                         type.  Operationally, a lifted object is one that
  58                         can be entered.
  59                         (NOTE: previously "pointed").
  60
  61         *algebraic*     A type with one or more constructors, whether declared
  62                         with "data" or "newtype".
  63                         An algebraic type is one that can be deconstructed
  64                         with a case expression.
  65                         *NOT* the same as lifted types,  because we also
  66                         include unboxed tuples in this classification.
  67
  68         *data*          A type declared with "data".  Also boxed tuples.
  69
  70         *primitive*     iff it is a built-in type that can't be expressed
  71                         in Haskell.
  72
  73 Currently, all primitive types are unlifted, but that's not necessarily
  74 the case.  (E.g. Int could be primitive.)
  75
  76 Some primitive types are unboxed, such as Int#, whereas some are boxed
  77 but unlifted (such as ByteArray#).  The only primitive types that we
  78 classify as algebraic are the unboxed tuples.
  79
  80 examples of type classifications:
  81
  82 Type            primitive       boxed           lifted          algebraic
  83 -----------------------------------------------------------------------------
  84 Int#,           Yes             No              No              No
  85 ByteArray#      Yes             Yes             No              No
  86 (# a, b #)      Yes             No              No              Yes
  87 (  a, b  )      No              Yes             Yes             Yes
  88 [a]             No              Yes             Yes             Yes
  89
  90 %************************************************************************
  91 %*                                                                      *
  92 \subsection{The data type}
  93 %*                                                                      *
  94 %************************************************************************
  95
  96
  97 \begin{code}
  98 type SuperKind = Type
  99 type Kind      = Type
 100
 101 type TyVarSubst = TyVarEnv Type
 102
 103 data Type
 104   = TyVarTy TyVar
 105
 106   | AppTy
 107         Type            -- Function is *not* a TyConApp
 108         Type
 109
 110   | TyConApp                    -- Application of a TyCon
 111         TyCon                   -- *Invariant* saturated appliations of FunTyCon and
 112                                 --      synonyms have their own constructors, below.
 113         [Type]          -- Might not be saturated.
 114
 115   | FunTy                       -- Special case of TyConApp: TyConApp FunTyCon [t1,t2]
 116         Type
 117         Type
 118
 119   | NoteTy                      -- Saturated application of a type synonym
 120         TyNote
 121         Type            -- The expanded version
 122
 123   | ForAllTy
 124         TyVar
 125         Type            -- TypeKind
 126
 127 data TyNote
 128   = SynNote Type        -- The unexpanded version of the type synonym; always a TyConApp
 129   | FTVNote TyVarSet    -- The free type variables of the noted expression
 130   | UsgNote UsageAnn    -- The usage annotation at this node
 131   | UsgForAll UVar      -- Annotation variable binder
 132   | IPNote Name         -- It's an implicit parameter
 133
 134 data UsageAnn
 135   = UsOnce              -- Used at most once
 136   | UsMany              -- Used possibly many times (no info; this annotation can be omitted)
 137   | UsVar    UVar       -- Annotation is variable (unbound OK only inside analysis)
 138 \end{code}
 139
 140
 141 %************************************************************************
 142 %*                                                                      *
 143 \subsection{Kinds}
 144 %*                                                                      *
 145 %************************************************************************
 146
 147 Kinds
 148 ~~~~~
 149 kind :: KX = kind -> kind
 150            | Type boxity        -- (Type *) is printed as just *
 151                                 -- (Type #) is printed as just #
 152
 153            | OpenKind           -- Can be boxed or unboxed
 154                                 -- Printed '?'
 155
 156            | kv                 -- A kind variable; *only* happens during kind checking
 157
 158 boxity :: BX = *        -- Boxed
 159              | #        -- Unboxed
 160              | bv       -- A boxity variable; *only* happens during kind checking
 161
 162 There's a little subtyping at the kind level:
 163         forall b. Type b <: OpenKind
 164
 165 That is, a type of kind (Type b) OK in a context requiring an AnyBox.
 166
 167 OpenKind, written '?', is used as the kind for certain type variables,
 168 in two situations:
 169
 170 1.  The universally quantified type variable(s) for special built-in
 171     things like error :: forall (a::?). String -> a.
 172     Here, the 'a' can be instantiated to a boxed or unboxed type.
 173
 174 2.  Kind '?' is also used when the typechecker needs to create a fresh
 175     type variable, one that may very well later be unified with a type.
 176     For example, suppose f::a, and we see an application (f x).  Then a
 177     must be a function type, so we unify a with (b->c).  But what kind
 178     are b and c?  They can be boxed or unboxed types, so we give them kind '?'.
 179
 180     When the type checker generalises over a bunch of type variables, it
 181     makes any that still have kind '?' into kind '*'.  So kind '?' is never
 182     present in an inferred type.
 183
 184
 185 \begin{code}
 186 mk_kind_name key str = mkGlobalName key pREL_GHC (mkKindOccFS tcName str)
 187                                     (LocalDef mkBuiltinSrcLoc NotExported)
 188         -- mk_kind_name is a bit of a hack
 189         -- The LocalDef means that we print the name without
 190         -- a qualifier, which is what we want for these kinds.
 191         -- It's used for both Kinds and Boxities
 192 \end{code}
 193
 194 ------------------------------------------
 195 Define  KX, the type of a kind
 196         BX, the type of a boxity
 197
 198 \begin{code}
 199 superKind :: SuperKind          -- KX, the type of all kinds
 200 superKindName = mk_kind_name kindConKey SLIT("KX")
 201 superKind = TyConApp (mkSuperKindCon superKindName) []
 202
 203 superBoxity :: SuperKind                -- BX, the type of all boxities
 204 superBoxityName = mk_kind_name boxityConKey SLIT("BX")
 205 superBoxity = TyConApp (mkSuperKindCon superBoxityName) []
 206 \end{code}
 207
 208 ------------------------------------------
 209 Define boxities: @*@ and @#@
 210
 211 \begin{code}
 212 boxedBoxity, unboxedBoxity :: Kind              -- :: BX
 213
 214 boxedConName = mk_kind_name boxedConKey SLIT("*")
 215 boxedBoxity  = TyConApp (mkKindCon boxedConName superBoxity) []
 216
 217 unboxedConName = mk_kind_name unboxedConKey SLIT("#")
 218 unboxedBoxity  = TyConApp (mkKindCon unboxedConName superBoxity) []
 219 \end{code}
 220
 221 ------------------------------------------
 222 Define kinds: Type, Type *, Type #, and OpenKind
 223
 224 \begin{code}
 225 typeCon :: KindCon      -- :: BX -> KX
 226 typeConName = mk_kind_name typeConKey SLIT("Type")
 227 typeCon     = mkKindCon typeConName (superBoxity `FunTy` superKind)
 228
 229 boxedTypeKind, unboxedTypeKind, openTypeKind :: Kind    -- Of superkind superKind
 230
 231 boxedTypeKind   = TyConApp typeCon [boxedBoxity]
 232 unboxedTypeKind = TyConApp typeCon [unboxedBoxity]
 233
 234 openKindConName = mk_kind_name anyBoxConKey SLIT("?")
 235 openKindCon     = mkKindCon openKindConName superKind
 236 openTypeKind    = TyConApp openKindCon []
 237 \end{code}
 238
 239 ------------------------------------------
 240 Define arrow kinds
 241
 242 \begin{code}
 243 mkArrowKind :: Kind -> Kind -> Kind
 244 mkArrowKind k1 k2 = k1 `FunTy` k2
 245
 246 mkArrowKinds :: [Kind] -> Kind -> Kind
 247 mkArrowKinds arg_kinds result_kind = foldr mkArrowKind result_kind arg_kinds
 248 \end{code}
 249
 250
 251 %************************************************************************
 252 %*                                                                      *
 253 \subsection{Wired-in type constructors
 254 %*                                                                      *
 255 %************************************************************************
 256
 257 We define a few wired-in type constructors here to avoid module knots
 258
 259 \begin{code}
 260 funTyConName = mkWiredInTyConName funTyConKey pREL_GHC SLIT("(->)") funTyCon
 261 funTyCon = mkFunTyCon funTyConName (mkArrowKinds [boxedTypeKind, boxedTypeKind] boxedTypeKind)
 262 \end{code}
 263
 264
 265 %************************************************************************
 266 %*                                                                      *
 267 \subsection{Equality on types}
 268 %*                                                                      *
 269 %************************************************************************
 270
 271 For the moment at least, type comparisons don't work if
 272 there are embedded for-alls.
 273
 274 \begin{code}
 275 instance Eq Type where
 276   ty1 == ty2 = case ty1 `cmpTy` ty2 of { EQ -> True; other -> False }
 277
 278 instance Ord Type where
 279   compare ty1 ty2 = cmpTy ty1 ty2
 280
 281 cmpTy :: Type -> Type -> Ordering
 282 cmpTy ty1 ty2
 283   = cmp emptyVarEnv ty1 ty2
 284   where
 285   -- The "env" maps type variables in ty1 to type variables in ty2
 286   -- So when comparing for-alls.. (forall tv1 . t1) (forall tv2 . t2)
 287   -- we in effect substitute tv2 for tv1 in t1 before continuing
 288     lookup env tv1 = case lookupVarEnv env tv1 of
 289                           Just tv2 -> tv2
 290                           Nothing  -> tv1
 291
 292     -- Get rid of NoteTy
 293     cmp env (NoteTy _ ty1) ty2 = cmp env ty1 ty2
 294     cmp env ty1 (NoteTy _ ty2) = cmp env ty1 ty2
 295
 296     -- Deal with equal constructors
 297     cmp env (TyVarTy tv1) (TyVarTy tv2) = lookup env tv1 `compare` tv2
 298     cmp env (AppTy f1 a1) (AppTy f2 a2) = cmp env f1 f2 `thenCmp` cmp env a1 a2
 299     cmp env (FunTy f1 a1) (FunTy f2 a2) = cmp env f1 f2 `thenCmp` cmp env a1 a2
 300     cmp env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmps env tys1 tys2)
 301     cmp env (ForAllTy tv1 t1)   (ForAllTy tv2 t2)   = cmp (extendVarEnv env tv1 tv2) t1 t2
 302
 303     -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < ForAllTy
 304     cmp env (AppTy _ _) (TyVarTy _) = GT
 305
 306     cmp env (FunTy _ _) (TyVarTy _) = GT
 307     cmp env (FunTy _ _) (AppTy _ _) = GT
 308
 309     cmp env (TyConApp _ _) (TyVarTy _) = GT
 310     cmp env (TyConApp _ _) (AppTy _ _) = GT
 311     cmp env (TyConApp _ _) (FunTy _ _) = GT
 312
 313     cmp env (ForAllTy _ _) other       = GT
 314
 315     cmp env _ _                        = LT
 316
 317     cmps env []     [] = EQ
 318     cmps env (t:ts) [] = GT
 319     cmps env [] (t:ts) = LT
 320     cmps env (t1:t1s) (t2:t2s) = cmp env t1 t2 `thenCmp` cmps env t1s t2s
 321 \end{code}
 322