X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=ghc%2Fcompiler%2Ftypes%2FTypeRep.lhs;h=7447e88fd65af62057ca63622848ee8cd9d7b409;hb=18074d6acde6d642b8fb10b1b49153f717c75446;hp=26e507839403b096c9f9b110e3cdbc91f8c5cba6;hpb=77a8c0dbd5c5ad90fe483cb9ddc2b6ef36d3f4d8;p=ghc-hetmet.git diff --git a/ghc/compiler/types/TypeRep.lhs b/ghc/compiler/types/TypeRep.lhs index 26e5078..7447e88 100644 --- a/ghc/compiler/types/TypeRep.lhs +++ b/ghc/compiler/types/TypeRep.lhs @@ -5,14 +5,17 @@ \begin{code} module TypeRep ( - Type(..), TyNote(..), UsageAnn(..), -- Representation visible to friends - Kind, TyVarSubst, + Type(..), TyNote(..), -- Representation visible + SourceType(..), -- to friends + + Kind, PredType, ThetaType, -- Synonyms + TyVarSubst, superKind, superBoxity, -- KX and BX respectively - boxedBoxity, unboxedBoxity, -- :: BX + liftedBoxity, unliftedBoxity, -- :: BX openKindCon, -- :: KX typeCon, -- :: BX -> KX - boxedTypeKind, unboxedTypeKind, openTypeKind, -- :: KX + liftedTypeKind, unliftedTypeKind, openTypeKind, -- :: KX mkArrowKind, mkArrowKinds, -- :: KX -> KX -> KX funTyCon @@ -21,22 +24,20 @@ module TypeRep ( #include "HsVersions.h" -- friends: -import Var ( TyVar, UVar ) -import VarEnv -import VarSet - -import Name ( Name, Provenance(..), ExportFlag(..), - mkWiredInTyConName, mkGlobalName, mkKindOccFS, tcName, - ) -import TyCon ( TyCon, KindCon, - mkFunTyCon, mkKindCon, mkSuperKindCon, - ) +import Var ( TyVar ) +import VarEnv ( TyVarEnv ) +import VarSet ( TyVarSet ) +import Name ( Name ) +import BasicTypes ( IPName ) +import TyCon ( TyCon, KindCon, mkFunTyCon, mkKindCon, mkSuperKindCon ) +import Class ( Class ) +import Binary -- others -import SrcLoc ( mkBuiltinSrcLoc ) -import PrelNames ( pREL_GHC ) -import Unique -- quite a few *Keys -import Util ( thenCmp ) +import PrelNames ( superKindName, superBoxityName, liftedConName, + unliftedConName, typeConName, openKindConName, + funTyConName + ) \end{code} %************************************************************************ @@ -48,15 +49,15 @@ import Util ( thenCmp ) A type is *unboxed* iff its representation is other than a pointer - Unboxed types cannot instantiate a type variable. - Unboxed types are always unlifted. + Unboxed types are also unlifted. *lifted* A type is lifted iff it has bottom as an element. Closures always have lifted types: i.e. any let-bound identifier in Core must have a lifted type. Operationally, a lifted object is one that can be entered. - (NOTE: previously "pointed"). + + Only lifted types may be unified with a type variable. *algebraic* A type with one or more constructors, whether declared with "data" or "newtype". @@ -87,6 +88,45 @@ ByteArray# Yes Yes No No ( a, b ) No Yes Yes Yes [a] No Yes Yes Yes + + + ---------------------- + A note about newtypes + ---------------------- + +Consider + newtype N = MkN Int + +Then we want N to be represented as an Int, and that's what we arrange. +The front end of the compiler [TcType.lhs] treats N as opaque, +the back end treats it as transparent [Type.lhs]. + +There's a bit of a problem with recursive newtypes + newtype P = MkP P + newtype Q = MkQ (Q->Q) + +Here the 'implicit expansion' we get from treating P and Q as transparent +would give rise to infinite types, which in turn makes eqType diverge. +Similarly splitForAllTys and splitFunTys can get into a loop. + +Solution: for recursive newtypes use a coerce, and treat the newtype +and its representation as distinct right through the compiler. That's +what you get if you use recursive newtypes. (They are rare, so who +cares if they are a tiny bit less efficient.) + +So: non-recursive newtypes are represented using a SourceTy (see below) + recursive newtypes are represented using a TyConApp + +The TyCon still says "I'm a newtype", but we do not represent the +newtype application as a SourceType; instead as a TyConApp. + + +NOTE: currently [March 02] we regard a newtype as 'recursive' if it's in a +mutually recursive group. That's a bit conservative: only if there's a loop +consisting only of newtypes do we need consider it as recursive. But it's +not so easy to discover that, and the situation isn't that common. + + %************************************************************************ %* * \subsection{The data type} @@ -107,36 +147,81 @@ data Type Type -- Function is *not* a TyConApp Type - | TyConApp -- Application of a TyCon - TyCon -- *Invariant* saturated appliations of FunTyCon and - -- synonyms have their own constructors, below. + | TyConApp -- Application of a TyCon + TyCon -- *Invariant* saturated appliations of FunTyCon and + -- synonyms have their own constructors, below. [Type] -- Might not be saturated. - | FunTy -- Special case of TyConApp: TyConApp FunTyCon [t1,t2] + | FunTy -- Special case of TyConApp: TyConApp FunTyCon [t1,t2] Type Type - | NoteTy -- Saturated application of a type synonym + | ForAllTy -- A polymorphic type + TyVar + Type + + | SourceTy -- A high level source type + SourceType -- ...can be expanded to a representation type... + + | NoteTy -- A type with a note attached TyNote Type -- The expanded version - | ForAllTy - TyVar - Type -- TypeKind - data TyNote - = SynNote Type -- The unexpanded version of the type synonym; always a TyConApp - | FTVNote TyVarSet -- The free type variables of the noted expression - | UsgNote UsageAnn -- The usage annotation at this node - | UsgForAll UVar -- Annotation variable binder - | IPNote Name -- It's an implicit parameter - -data UsageAnn - = UsOnce -- Used at most once - | UsMany -- Used possibly many times (no info; this annotation can be omitted) - | UsVar UVar -- Annotation is variable (unbound OK only inside analysis) + = FTVNote TyVarSet -- The free type variables of the noted expression + + | SynNote Type -- Used for type synonyms + -- The Type is always a TyConApp, and is the un-expanded form. + -- The type to which the note is attached is the expanded form. + +\end{code} + +------------------------------------- + Source types + +A type of the form + SourceTy sty +represents a value whose type is the Haskell source type sty. +It can be expanded into its representation, but: + + * The type checker must treat it as opaque + * The rest of the compiler treats it as transparent + +There are two main uses + a) Haskell predicates + b) newtypes + +Consider these examples: + f :: (Eq a) => a -> Int + g :: (?x :: Int -> Int) => a -> Int + h :: (r\l) => {r} => {l::Int | r} + +Here the "Eq a" and "?x :: Int -> Int" and "r\l" are all called *predicates* +Predicates are represented inside GHC by PredType: + +\begin{code} +data SourceType + = ClassP Class [Type] -- Class predicate + | IParam (IPName Name) Type -- Implicit parameter + | NType TyCon [Type] -- A *saturated*, *non-recursive* newtype application + -- [See notes at top about newtypes] + +type PredType = SourceType -- A subtype for predicates +type ThetaType = [PredType] \end{code} +(We don't support TREX records yet, but the setup is designed +to expand to allow them.) + +A Haskell qualified type, such as that for f,g,h above, is +represented using + * a FunTy for the double arrow + * with a PredTy as the function argument + +The predicate really does turn into a real extra argument to the +function. If the argument has type (PredTy p) then the predicate p is +represented by evidence (a dictionary, for example, of type (predRepTy p). + %************************************************************************ %* * @@ -147,61 +232,52 @@ data UsageAnn Kinds ~~~~~ kind :: KX = kind -> kind - | Type boxity -- (Type *) is printed as just * + + | Type liftedness -- (Type *) is printed as just * -- (Type #) is printed as just # - | OpenKind -- Can be boxed or unboxed + | OpenKind -- Can be lifted or unlifted -- Printed '?' | kv -- A kind variable; *only* happens during kind checking -boxity :: BX = * -- Boxed - | # -- Unboxed +boxity :: BX = * -- Lifted + | # -- Unlifted | bv -- A boxity variable; *only* happens during kind checking There's a little subtyping at the kind level: forall b. Type b <: OpenKind -That is, a type of kind (Type b) OK in a context requiring an AnyBox. +That is, a type of kind (Type b) is OK in a context requiring an OpenKind OpenKind, written '?', is used as the kind for certain type variables, in two situations: 1. The universally quantified type variable(s) for special built-in things like error :: forall (a::?). String -> a. - Here, the 'a' can be instantiated to a boxed or unboxed type. + Here, the 'a' can be instantiated to a lifted or unlifted type. 2. Kind '?' is also used when the typechecker needs to create a fresh type variable, one that may very well later be unified with a type. For example, suppose f::a, and we see an application (f x). Then a must be a function type, so we unify a with (b->c). But what kind - are b and c? They can be boxed or unboxed types, so we give them kind '?'. + are b and c? They can be lifted or unlifted types, or indeed type schemes, + so we give them kind '?'. When the type checker generalises over a bunch of type variables, it makes any that still have kind '?' into kind '*'. So kind '?' is never present in an inferred type. -\begin{code} -mk_kind_name key str = mkGlobalName key pREL_GHC (mkKindOccFS tcName str) - (LocalDef mkBuiltinSrcLoc NotExported) - -- mk_kind_name is a bit of a hack - -- The LocalDef means that we print the name without - -- a qualifier, which is what we want for these kinds. - -- It's used for both Kinds and Boxities -\end{code} - ------------------------------------------ Define KX, the type of a kind BX, the type of a boxity \begin{code} superKind :: SuperKind -- KX, the type of all kinds -superKindName = mk_kind_name kindConKey SLIT("KX") superKind = TyConApp (mkSuperKindCon superKindName) [] superBoxity :: SuperKind -- BX, the type of all boxities -superBoxityName = mk_kind_name boxityConKey SLIT("BX") superBoxity = TyConApp (mkSuperKindCon superBoxityName) [] \end{code} @@ -209,29 +285,26 @@ superBoxity = TyConApp (mkSuperKindCon superBoxityName) [] Define boxities: @*@ and @#@ \begin{code} -boxedBoxity, unboxedBoxity :: Kind -- :: BX - -boxedConName = mk_kind_name boxedConKey SLIT("*") -boxedBoxity = TyConApp (mkKindCon boxedConName superBoxity) [] +liftedBoxity, unliftedBoxity :: Kind -- :: BX +liftedBoxity = TyConApp liftedBoxityCon [] +unliftedBoxity = TyConApp unliftedBoxityCon [] -unboxedConName = mk_kind_name unboxedConKey SLIT("#") -unboxedBoxity = TyConApp (mkKindCon unboxedConName superBoxity) [] +liftedBoxityCon = mkKindCon liftedConName superBoxity +unliftedBoxityCon = mkKindCon unliftedConName superBoxity \end{code} ------------------------------------------ -Define kinds: Type, Type *, Type #, and OpenKind +Define kinds: Type, Type *, Type #, OpenKind \begin{code} typeCon :: KindCon -- :: BX -> KX -typeConName = mk_kind_name typeConKey SLIT("Type") typeCon = mkKindCon typeConName (superBoxity `FunTy` superKind) -boxedTypeKind, unboxedTypeKind, openTypeKind :: Kind -- Of superkind superKind +liftedTypeKind, unliftedTypeKind, openTypeKind :: Kind -- Of superkind superKind -boxedTypeKind = TyConApp typeCon [boxedBoxity] -unboxedTypeKind = TyConApp typeCon [unboxedBoxity] +liftedTypeKind = TyConApp typeCon [liftedBoxity] +unliftedTypeKind = TyConApp typeCon [unliftedBoxity] -openKindConName = mk_kind_name anyBoxConKey SLIT("?") openKindCon = mkKindCon openKindConName superKind openTypeKind = TyConApp openKindCon [] \end{code} @@ -247,76 +320,45 @@ mkArrowKinds :: [Kind] -> Kind -> Kind mkArrowKinds arg_kinds result_kind = foldr mkArrowKind result_kind arg_kinds \end{code} - -%************************************************************************ -%* * -\subsection{Wired-in type constructors -%* * -%************************************************************************ - -We define a few wired-in type constructors here to avoid module knots +----------------------------------------------------------------------------- +Binary kinds for interface files \begin{code} -funTyConName = mkWiredInTyConName funTyConKey pREL_GHC SLIT("(->)") funTyCon -funTyCon = mkFunTyCon funTyConName (mkArrowKinds [boxedTypeKind, boxedTypeKind] boxedTypeKind) +instance Binary Kind where + put_ bh k@(TyConApp tc []) + | tc == openKindCon = putByte bh 0 + put_ bh k@(TyConApp tc [TyConApp bc _]) + | tc == typeCon && bc == liftedBoxityCon = putByte bh 2 + | tc == typeCon && bc == unliftedBoxityCon = putByte bh 3 + put_ bh (FunTy f a) = do putByte bh 4; put_ bh f; put_ bh a + put_ bh _ = error "Binary.put(Kind): strange-looking Kind" + + get bh = do + b <- getByte bh + case b of + 0 -> return openTypeKind + 2 -> return liftedTypeKind + 3 -> return unliftedTypeKind + _ -> do f <- get bh; a <- get bh; return (FunTy f a) \end{code} - %************************************************************************ %* * -\subsection{Equality on types} +\subsection{Wired-in type constructors %* * %************************************************************************ -For the moment at least, type comparisons don't work if -there are embedded for-alls. +We define a few wired-in type constructors here to avoid module knots \begin{code} -instance Eq Type where - ty1 == ty2 = case ty1 `cmpTy` ty2 of { EQ -> True; other -> False } - -instance Ord Type where - compare ty1 ty2 = cmpTy ty1 ty2 - -cmpTy :: Type -> Type -> Ordering -cmpTy ty1 ty2 - = cmp emptyVarEnv ty1 ty2 - where - -- The "env" maps type variables in ty1 to type variables in ty2 - -- So when comparing for-alls.. (forall tv1 . t1) (forall tv2 . t2) - -- we in effect substitute tv2 for tv1 in t1 before continuing - lookup env tv1 = case lookupVarEnv env tv1 of - Just tv2 -> tv2 - Nothing -> tv1 - - -- Get rid of NoteTy - cmp env (NoteTy _ ty1) ty2 = cmp env ty1 ty2 - cmp env ty1 (NoteTy _ ty2) = cmp env ty1 ty2 - - -- Deal with equal constructors - cmp env (TyVarTy tv1) (TyVarTy tv2) = lookup env tv1 `compare` tv2 - cmp env (AppTy f1 a1) (AppTy f2 a2) = cmp env f1 f2 `thenCmp` cmp env a1 a2 - cmp env (FunTy f1 a1) (FunTy f2 a2) = cmp env f1 f2 `thenCmp` cmp env a1 a2 - cmp env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmps env tys1 tys2) - cmp env (ForAllTy tv1 t1) (ForAllTy tv2 t2) = cmp (extendVarEnv env tv1 tv2) t1 t2 - - -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < ForAllTy - cmp env (AppTy _ _) (TyVarTy _) = GT - - cmp env (FunTy _ _) (TyVarTy _) = GT - cmp env (FunTy _ _) (AppTy _ _) = GT - - cmp env (TyConApp _ _) (TyVarTy _) = GT - cmp env (TyConApp _ _) (AppTy _ _) = GT - cmp env (TyConApp _ _) (FunTy _ _) = GT - - cmp env (ForAllTy _ _) other = GT - - cmp env _ _ = LT - - cmps env [] [] = EQ - cmps env (t:ts) [] = GT - cmps env [] (t:ts) = LT - cmps env (t1:t1s) (t2:t2s) = cmp env t1 t2 `thenCmp` cmps env t1s t2s +funTyCon = mkFunTyCon funTyConName (mkArrowKinds [liftedTypeKind, liftedTypeKind] liftedTypeKind) + -- You might think that (->) should have type (? -> ? -> *), and you'd be right + -- But if we do that we get kind errors when saying + -- instance Control.Arrow (->) + -- becuase the expected kind is (*->*->*). The trouble is that the + -- expected/actual stuff in the unifier does not go contra-variant, whereas + -- the kind sub-typing does. Sigh. It really only matters if you use (->) in + -- a prefix way, thus: (->) Int# Int#. And this is unusual. \end{code} +