\begin{code}
module TypeRep (
- Type(..), TyNote(..), PredType(..), UsageAnn(..), -- Representation visible to friends
+ TyThing(..),
+ Type(..), TyNote(..), -- Representation visible
+ PredType(..), -- to friends
- Kind, ThetaType, RhoType, TauType, SigmaType, -- Synonyms
+ Kind, 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
+ funTyCon,
+
+ crudePprType -- Prints type representations for debugging
) where
#include "HsVersions.h"
+import {-# SOURCE #-} DataCon( DataCon )
+
-- 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 Class ( Class )
+import Var ( Id, TyVar, tyVarKind )
+import VarEnv ( TyVarEnv )
+import VarSet ( TyVarSet )
+import Name ( Name, mkWiredInName, mkInternalName )
+import OccName ( mkOccFS, mkKindOccFS, tcName )
+import BasicTypes ( IPName )
+import TyCon ( TyCon, KindCon, mkFunTyCon, mkKindCon, mkSuperKindCon, isNewTyCon )
+import Class ( Class )
-- others
-import SrcLoc ( mkBuiltinSrcLoc )
-import PrelNames ( pREL_GHC, kindConKey, boxityConKey, boxedConKey, unboxedConKey,
- typeConKey, anyBoxConKey, funTyConKey
+import PrelNames ( gHC_PRIM, kindConKey, boxityConKey, liftedConKey,
+ unliftedConKey, typeConKey, anyBoxConKey,
+ funTyConKey
)
+import SrcLoc ( noSrcLoc )
+import Outputable
\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:
+
+* Newtypes are always represented using NewTcApp, never as TyConApp.
+
+* For non-recursive newtypes, P, treat P just like a type synonym after
+ type-checking is done; i.e. it's opaque during type checking (functions
+ from TcType) but transparent afterwards (functions from Type).
+ "Treat P as a type synonym" means "all functions expand NewTcApps
+ on the fly".
+
+ Applications of the data constructor P simply vanish:
+ P x = x
+
+
+* For recursive newtypes Q, treat the Q and its representation as
+ distinct right through the compiler. Applications of the data consructor
+ use a coerce:
+ Q = \(x::Q->Q). coerce Q x
+ They are rare, so who cares if they are a tiny bit less efficient.
+
+The typechecker (TcTyDecls) identifies enough type construtors as 'recursive'
+to cut all loops. The other members of the loop may be marked 'non-recursive'.
+
+
%************************************************************************
%* *
\subsection{The data type}
-- synonyms have their own constructors, below.
[Type] -- Might not be saturated.
+ | NewTcApp -- Application of a NewType TyCon. All newtype applications
+ TyCon -- show up like this until they are fed through newTypeRep,
+ -- which returns
+ -- * an ordinary TyConApp for non-saturated,
+ -- or recursive newtypes
+ --
+ -- * the representation type of the newtype for satuarted,
+ -- non-recursive ones
+ -- [But the result of a call to newTypeRep is always consumed
+ -- immediately; it never lives on in another type. So in any
+ -- type, newtypes are always represented with NewTcApp.]
+ [Type] -- Might not be saturated.
+
| FunTy -- Special case of TyConApp: TyConApp FunTyCon [t1,t2]
Type
Type
TyVar
Type
- | PredTy -- A Haskell predicate
- PredType
+ | PredTy -- A high level source type
+ PredType -- ...can be expanded to a representation 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
+ = FTVNote TyVarSet -- The free type variables of the noted expression
-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 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}
-
-------------------------------------
- Predicates
+ Source types
+
+A type of the form
+ PredTy p
+represents a value whose type is the Haskell predicate p,
+where a predicate is what occurs before the '=>' in a Haskell type.
+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
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 PredType
+ = ClassP Class [Type] -- Class predicate
+ | IParam (IPName Name) Type -- Implicit parameter
+
+type ThetaType = [PredType]
\end{code}
(We don't support TREX records yet, but the setup is designed
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:
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}
+superKindName = kindQual FSLIT("KX") kindConKey
+superBoxityName = kindQual FSLIT("BX") boxityConKey
+liftedConName = kindQual FSLIT("*") liftedConKey
+unliftedConName = kindQual FSLIT("#") unliftedConKey
+openKindConName = kindQual FSLIT("?") anyBoxConKey
+typeConName = kindQual FSLIT("Type") typeConKey
+
+kindQual str uq = mkInternalName uq (mkKindOccFS tcName str) noSrcLoc
+ -- Kinds are not z-encoded in interface file, hence mkKindOccFS
+ -- And they don't come from any particular module; indeed we always
+ -- want to print them unqualified. Hence the InternalName.
+\end{code}
+
+\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
\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}
%************************************************************************
%* *
+ TyThing
+%* *
+%************************************************************************
+
+Despite the fact that DataCon has to be imported via a hi-boot route,
+this module seems the right place for TyThing, because it's needed for
+funTyCon and all the types in TysPrim.
+
+\begin{code}
+data TyThing = AnId Id
+ | ADataCon DataCon
+ | ATyCon TyCon
+ | AClass Class
+\end{code}
+
+
+%************************************************************************
+%* *
\subsection{Wired-in type constructors
%* *
%************************************************************************
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.
+
+funTyConName = mkWiredInName gHC_PRIM
+ (mkOccFS tcName FSLIT("(->)"))
+ funTyConKey
+ Nothing -- No parent object
+ (ATyCon funTyCon) -- Relevant TyCon
\end{code}
+
+%************************************************************************
+%* *
+ Crude printing
+ For debug purposes, we may want to print a type directly
+%* *
+%************************************************************************
+
+\begin{code}
+crudePprType :: Type -> SDoc
+crudePprType (TyVarTy tv) = ppr tv
+crudePprType (AppTy t1 t2) = crudePprType t1 <+> (parens (crudePprType t2))
+crudePprType (FunTy t1 t2) = crudePprType t1 <+> (parens (crudePprType t2))
+crudePprType (TyConApp tc tys) = ppr_tc_app (ppr tc <> pp_nt tc) tys
+crudePprType (NewTcApp tc tys) = ptext SLIT("<nt>") <+> ppr_tc_app (ppr tc <> pp_nt tc) tys
+crudePprType (ForAllTy tv ty) = sep [ptext SLIT("forall") <+>
+ parens (ppr tv <+> crudePprType (tyVarKind tv)) <> dot,
+ crudePprType ty]
+crudePprType (PredTy st) = braces (crudePprPredTy st)
+crudePprType (NoteTy (SynNote ty1) ty2) = crudePprType ty1
+crudePprType (NoteTy other ty) = crudePprType ty
+
+crudePprPredTy (ClassP cls tys) = ppr_tc_app (ppr cls) tys
+crudePprPredTy (IParam ip ty) = ppr ip <> dcolon <> crudePprType ty
+
+ppr_tc_app :: SDoc -> [Type] -> SDoc
+ppr_tc_app tc tys = tc <+> sep (map (parens . crudePprType) tys)
+
+pp_nt tc | isNewTyCon tc = ptext SLIT("(nt)")
+ | otherwise = empty
+\end{code}
\ No newline at end of file
projects / ghc-hetmet.git / blobdiff