\begin{code}
module TypeRep (
- Type(..), TyNote(..), PredType(..), UsageAnn(..), -- Representation visible to friends
+ Type(..), TyNote(..), PredType(..), -- Representation visible to friends
Kind, ThetaType, RhoType, TauType, SigmaType, -- 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 Var ( TyVar )
import VarEnv
import VarSet
-import Name ( Name, mkGlobalName, mkKindOccFS, tcName )
-import OccName ( tcName )
-import TyCon ( TyCon, KindCon,
- mkFunTyCon, mkKindCon, mkSuperKindCon,
- )
+import Name ( Name )
+import TyCon ( TyCon, KindCon, mkFunTyCon, mkKindCon, mkSuperKindCon )
import Class ( Class )
-- others
-import SrcLoc ( builtinSrcLoc )
-import PrelNames ( pREL_GHC, kindConKey, boxityConKey, boxedConKey,
- unboxedConKey, typeConKey, anyBoxConKey, funTyConName
+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".
| PredTy -- A Haskell predicate
PredType
+ | UsageTy -- A usage-annotated type
+ Type -- - Annotation of kind $ (i.e., usage annotation)
+ Type -- - Annotated type
+
| NoteTy -- A type with a note attached
TyNote
Type -- The expanded version
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
-
-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)
-
type ThetaType = [PredType]
type RhoType = Type
type SigmaType = Type
\end{code}
+INVARIANT: UsageTys are optional, but may *only* appear immediately
+under a FunTy (either argument), or at top-level of a Type permitted
+to be annotated (such as the type of an Id). NoteTys are transparent
+for the purposes of this rule.
-------------------------------------
Predicates
Predicates are represented inside GHC by PredType:
\begin{code}
-data PredType = Class Class [Type]
+data PredType = ClassP Class [Type]
| IParam Name Type
\end{code}
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:
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, 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) builtinSrcLoc
- -- 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
-
-boxedConName = mk_kind_name boxedConKey SLIT("*")
-boxedBoxity = TyConApp (mkKindCon boxedConName superBoxity) []
+liftedBoxity, unliftedBoxity :: Kind -- :: BX
+liftedBoxity = TyConApp (mkKindCon liftedConName superBoxity) []
-unboxedConName = mk_kind_name unboxedConKey SLIT("#")
-unboxedBoxity = TyConApp (mkKindCon unboxedConName superBoxity) []
+unliftedBoxity = TyConApp (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}
------------------------------------------
We define a few wired-in type constructors here to avoid module knots
\begin{code}
-funTyCon = mkFunTyCon funTyConName (mkArrowKinds [boxedTypeKind, boxedTypeKind] boxedTypeKind)
+funTyCon = mkFunTyCon funTyConName (mkArrowKinds [liftedTypeKind, liftedTypeKind] liftedTypeKind)
\end{code}
+------------------------------------------
+Usage tycons @.@ and @!@
+
+The usage tycons are of kind usageTypeKind (`$'). The types contain
+no values, and are used purely for usage annotation.
+
+\begin{code}
+usOnceTyCon = mkKindCon usOnceTyConName usageTypeKind
+usOnce = TyConApp usOnceTyCon []
+
+usManyTyCon = mkKindCon usManyTyConName usageTypeKind
+usMany = TyConApp usManyTyCon []
+\end{code}
projects / ghc-hetmet.git / blobdiff