\begin{code}
module TypeRep (
- Type(..), TyNote(..), PredType(..), -- Representation visible to friends
+ Type(..), TyNote(..), SourceType(..), -- Representation visible to friends
- Kind, ThetaType, RhoType, TauType, SigmaType, -- Synonyms
+ Kind, TauType, 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
import VarEnv
import VarSet
-import Name ( Name, tcName )
+import Name ( Name )
import TyCon ( TyCon, KindCon, mkFunTyCon, mkKindCon, mkSuperKindCon )
import Class ( Class )
-- others
-import PrelNames ( superKindName, superBoxityName, boxedConName,
- unboxedConName, typeConName, openKindConName, funTyConName,
- usageKindConName, usOnceTyConName, usManyTyConName
+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.
+
+
%************************************************************************
%* *
\subsection{The data type}
\begin{code}
type SuperKind = Type
type Kind = Type
+type TauType = Type
type TyVarSubst = TyVarEnv Type
TyVar
Type
- | PredTy -- A Haskell predicate
- PredType
+ | SourceTy -- A high level source type
+ SourceType -- ...can be expanded to a representation type...
| UsageTy -- A usage-annotated type
Type -- - Annotation of kind $ (i.e., usage annotation)
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
+ = FTVNote TyVarSet -- The free type variables of the noted expression
-type ThetaType = [PredType]
-type RhoType = Type
-type TauType = Type
-type SigmaType = Type
+ | 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}
INVARIANT: UsageTys are optional, but may *only* appear immediately
for the purposes of this rule.
-------------------------------------
- Predicates
+ 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
Predicates are represented inside GHC by PredType:
\begin{code}
-data PredType = Class Class [Type]
- | IParam Name Type
+data SourceType = ClassP Class [Type] -- Class predicate
+ | IParam 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
~~~~~
kind :: KX = kind -> kind
- | Type boxity -- (Type *) is printed as just *
+ | Type liftedness -- (Type *) is printed as just *
-- (Type #) is printed as just #
| UsageKind -- Printed '$'; used for usage annotations
- | 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:
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
Define boxities: @*@ and @#@
\begin{code}
-boxedBoxity, unboxedBoxity :: Kind -- :: BX
-boxedBoxity = TyConApp (mkKindCon boxedConName superBoxity) []
+liftedBoxity, unliftedBoxity :: Kind -- :: BX
+liftedBoxity = TyConApp (mkKindCon liftedConName superBoxity) []
-unboxedBoxity = TyConApp (mkKindCon unboxedConName superBoxity) []
+unliftedBoxity = TyConApp (mkKindCon unliftedConName superBoxity) []
\end{code}
------------------------------------------
typeCon :: KindCon -- :: BX -> KX
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]
openKindCon = mkKindCon openKindConName superKind
openTypeKind = TyConApp openKindCon []
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}
------------------------------------------