\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
+ usageKindCon, -- :: KX
+ usageTypeKind, -- :: KX
+ usOnceTyCon, usManyTyCon, -- :: $
+ usOnce, usMany, -- :: $
+
funTyCon
) where
#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,
+ usageKindConName, usOnceTyConName, usManyTyConName,
+ funTyConName
+ )
\end{code}
%************************************************************************
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".
( 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}
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).
+
%************************************************************************
%* *
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
+ | UsageKind -- Printed '$'; used for usage annotations
+
+ | 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}
Define boxities: @*@ and @#@
\begin{code}
-boxedBoxity, unboxedBoxity :: Kind -- :: BX
+liftedBoxity, unliftedBoxity :: Kind -- :: BX
+liftedBoxity = TyConApp liftedBoxityCon []
+unliftedBoxity = TyConApp unliftedBoxityCon []
-boxedConName = mk_kind_name boxedConKey SLIT("*")
-boxedBoxity = TyConApp (mkKindCon boxedConName superBoxity) []
-
-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, and UsageKind
\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 []
+
+usageKindCon = mkKindCon usageKindConName superKind
+usageTypeKind = TyConApp usageKindCon []
\end{code}
------------------------------------------
mkArrowKinds arg_kinds result_kind = foldr mkArrowKind result_kind arg_kinds
\end{code}
+-----------------------------------------------------------------------------
+Binary kinds for interface files
+
+\begin{code}
+instance Binary Kind where
+ put_ bh k@(TyConApp tc [])
+ | tc == openKindCon = putByte bh 0
+ | tc == usageKindCon = putByte bh 1
+ 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
+ 1 -> return usageTypeKind
+ 2 -> return liftedTypeKind
+ 3 -> return unliftedTypeKind
+ _ -> do f <- get bh; a <- get bh; return (FunTy f a)
+\end{code}
%************************************************************************
%* *
We define a few wired-in type constructors here to avoid module knots
\begin{code}
-funTyConName = mkWiredInTyConName funTyConKey pREL_GHC SLIT("(->)") funTyCon
-funTyCon = mkFunTyCon funTyConName (mkArrowKinds [boxedTypeKind, boxedTypeKind] boxedTypeKind)
+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}
+------------------------------------------
+Usage tycons @.@ and @!@
-%************************************************************************
-%* *
-\subsection{Equality on types}
-%* *
-%************************************************************************
-
-For the moment at least, type comparisons don't work if
-there are embedded for-alls.
+The usage tycons are of kind usageTypeKind (`$'). The types contain
+no values, and are used purely for usage annotation.
\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
+usOnceTyCon = mkKindCon usOnceTyConName usageTypeKind
+usOnce = TyConApp usOnceTyCon []
+
+usManyTyCon = mkKindCon usManyTyConName usageTypeKind
+usMany = TyConApp usManyTyCon []
\end{code}
projects / ghc-hetmet.git / blobdiff