\begin{code}
module TypeRep (
- Type(..), TyNote(..), UsageAnn(..), -- Representation visible to friends
- Kind, TyVarSubst,
+ TyThing(..),
+ Type(..), TyNote(..), -- Representation visible
+ PredType(..), -- to friends
+
+ Kind, ThetaType, -- Synonyms
- superKind, superBoxity, -- :: SuperKind
+ funTyCon,
- boxedKind, -- :: Kind :: BX
- anyBoxKind, -- :: Kind :: BX
- typeCon, -- :: KindCon :: BX -> KX
- anyBoxCon, -- :: KindCon :: BX
-
- boxedTypeKind, unboxedTypeKind, openTypeKind, -- Kind :: superKind
+ -- Pretty-printing
+ pprType, pprParendType, pprTyThingCategory,
+ pprPred, pprTheta, pprThetaArrow, pprClassPred,
+ -- Re-export fromKind
+ liftedTypeKind, unliftedTypeKind, openTypeKind,
+ isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind,
mkArrowKind, mkArrowKinds,
-
- funTyCon
+ pprKind, pprParendKind
) where
#include "HsVersions.h"
--- friends:
-import Var ( TyVar, UVar )
-import VarEnv
-import VarSet
+import {-# SOURCE #-} DataCon( DataCon, dataConName )
-import Name ( Name, Provenance(..), ExportFlag(..),
- mkWiredInTyConName, mkGlobalName, mkKindOccFS, tcName,
- )
-import TyCon ( TyCon, KindCon,
- mkFunTyCon, mkKindCon, mkSuperKindCon,
- )
+-- friends:
+import Kind
+import Var ( Var, Id, TyVar, tyVarKind )
+import VarSet ( TyVarSet )
+import Name ( Name, NamedThing(..), BuiltInSyntax(..), mkWiredInName )
+import OccName ( mkOccFS, tcName, parenSymOcc )
+import BasicTypes ( IPName, tupleParens )
+import TyCon ( TyCon, mkFunTyCon, tyConArity, tupleTyConBoxity, isTupleTyCon, isRecursiveTyCon, isNewTyCon )
+import Class ( Class )
-- others
-import SrcLoc ( mkBuiltinSrcLoc )
-import PrelMods ( pREL_GHC )
-import Unique -- quite a few *Keys
-import Util ( thenCmp )
+import PrelNames ( gHC_PRIM, funTyConKey, listTyConKey, parrTyConKey, hasKey )
+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 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}
\begin{code}
-type SuperKind = Type
-type Kind = Type
-
-type TyVarSubst = TyVarEnv Type
-
data Type
- = TyVarTy TyVar
+ = TyVarTy TyVar
| AppTy
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.
+ Type -- It must be another AppTy, or TyVarTy
+ -- (or NoteTy of these)
+
+ | TyConApp -- Application of a TyCon, including newtypes
+ TyCon -- *Invariant* saturated appliations of FunTyCon and
+ -- synonyms have their own constructors, below.
+ -- However, *unsaturated* type synonyms, and FunTyCons
+ -- do appear as TyConApps. (Unsaturated type synonyms
+ -- can appear as the RHS of a type synonym, for exmaple.)
[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
- TyNote
- Type -- The expanded version
-
- | ForAllTy
+ | ForAllTy -- A polymorphic type
TyVar
- Type -- TypeKind
+ Type
-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)
-\end{code}
-
-
-%************************************************************************
-%* *
-\subsection{Kinds}
-%* *
-%************************************************************************
+ | PredTy -- A high level source type
+ PredType -- ...can be expanded to a representation type...
-Kinds
-~~~~~
-k::K = Type bx
- | k -> k
- | kv
+ | NoteTy -- A type with a note attached
+ TyNote
+ Type -- The expanded version
-kv :: KX is a kind variable
+data TyNote
+ = FTVNote TyVarSet -- The free type variables of the noted expression
-Type :: BX -> KX
+ | 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}
-bx::BX = Boxed
- | Unboxed
- | AnyBox -- Used *only* for special built-in things
- -- like error :: forall (a::*?). String -> a
- -- Here, the 'a' can be instantiated to a boxed or
- -- unboxed type.
- | bv
+-------------------------------------
+ Source types
-bxv :: BX is a boxity variable
+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:
-sk = KX -- A kind
- | BX -- A boxity
- | sk -> sk -- In ptic (BX -> KX)
+ * The type checker must treat it as opaque
+ * The rest of the compiler treats it as transparent
-\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}
+Consider these examples:
+ f :: (Eq a) => a -> Int
+ g :: (?x :: Int -> Int) => a -> Int
+ h :: (r\l) => {r} => {l::Int | r}
-Define KX, BX.
+Here the "Eq a" and "?x :: Int -> Int" and "r\l" are all called *predicates*
+Predicates are represented inside GHC by PredType:
\begin{code}
-superKind :: SuperKind -- KX, the type of all kinds
-superKindName = mk_kind_name kindConKey SLIT("KX")
-superKind = TyConApp (mkSuperKindCon superKindName) []
+data PredType
+ = ClassP Class [Type] -- Class predicate
+ | IParam (IPName Name) Type -- Implicit parameter
-superBoxity :: SuperKind -- BX, the type of all boxities
-superBoxityName = mk_kind_name boxityConKey SLIT("BX")
-superBoxity = TyConApp (mkSuperKindCon superBoxityName) []
+type ThetaType = [PredType]
\end{code}
-Define Boxed, Unboxed, AnyBox
-
-\begin{code}
-boxedKind, unboxedKind, anyBoxKind :: Kind -- Of superkind superBoxity
+(We don't support TREX records yet, but the setup is designed
+to expand to allow them.)
-boxedConName = mk_kind_name boxedConKey SLIT("*")
-boxedKind = TyConApp (mkKindCon boxedConName superBoxity) []
+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
-unboxedConName = mk_kind_name unboxedConKey SLIT("#")
-unboxedKind = TyConApp (mkKindCon unboxedConName superBoxity) []
+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).
-anyBoxConName = mk_kind_name anyBoxConKey SLIT("?")
-anyBoxCon = mkKindCon anyBoxConName superBoxity -- A kind of wild card
-anyBoxKind = TyConApp anyBoxCon []
-\end{code}
-Define Type
-
-\begin{code}
-typeCon :: KindCon
-typeConName = mk_kind_name typeConKey SLIT("Type")
-typeCon = mkKindCon typeConName (superBoxity `FunTy` superKind)
-\end{code}
+%************************************************************************
+%* *
+ TyThing
+%* *
+%************************************************************************
-Define (Type Boxed), (Type Unboxed), (Type AnyBox)
+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}
-boxedTypeKind, unboxedTypeKind, openTypeKind :: Kind
-boxedTypeKind = TyConApp typeCon [boxedKind]
-unboxedTypeKind = TyConApp typeCon [unboxedKind]
-openTypeKind = TyConApp typeCon [anyBoxKind]
-
-mkArrowKind :: Kind -> Kind -> Kind
-mkArrowKind k1 k2 = k1 `FunTy` k2
-
-mkArrowKinds :: [Kind] -> Kind -> Kind
-mkArrowKinds arg_kinds result_kind = foldr mkArrowKind result_kind arg_kinds
+data TyThing = AnId Id
+ | ADataCon DataCon
+ | ATyCon TyCon
+ | AClass Class
+
+instance Outputable TyThing where
+ ppr thing = pprTyThingCategory thing <+> quotes (ppr (getName thing))
+
+pprTyThingCategory :: TyThing -> SDoc
+pprTyThingCategory (ATyCon _) = ptext SLIT("Type constructor")
+pprTyThingCategory (AClass _) = ptext SLIT("Class")
+pprTyThingCategory (AnId _) = ptext SLIT("Identifier")
+pprTyThingCategory (ADataCon _) = ptext SLIT("Data constructor")
+
+instance NamedThing TyThing where -- Can't put this with the type
+ getName (AnId id) = getName id -- decl, because the DataCon instance
+ getName (ATyCon tc) = getName tc -- isn't visible there
+ getName (AClass cl) = getName cl
+ getName (ADataCon dc) = dataConName dc
\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 [argTypeKind, openTypeKind] 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
+ BuiltInSyntax
\end{code}
%************************************************************************
%* *
-\subsection{Equality on types}
+\subsection{The external interface}
%* *
%************************************************************************
-For the moment at least, type comparisons don't work if
-there are embedded for-alls.
+@pprType@ is the standard @Type@ printer; the overloaded @ppr@ function is
+defined to use this. @pprParendType@ is the same, except it puts
+parens around the type, except for the atomic cases. @pprParendType@
+works just by setting the initial context precedence very high.
\begin{code}
-instance Eq Type where
- ty1 == ty2 = case ty1 `cmpTy` ty2 of { EQ -> True; other -> False }
+data Prec = TopPrec -- No parens
+ | FunPrec -- Function args; no parens for tycon apps
+ | TyConPrec -- Tycon args; no parens for atomic
+ deriving( Eq, Ord )
+
+maybeParen :: Prec -> Prec -> SDoc -> SDoc
+maybeParen ctxt_prec inner_prec pretty
+ | ctxt_prec < inner_prec = pretty
+ | otherwise = parens pretty
+
+------------------
+pprType, pprParendType :: Type -> SDoc
+pprType ty = ppr_type TopPrec ty
+pprParendType ty = ppr_type TyConPrec ty
+
+------------------
+pprPred :: PredType -> SDoc
+pprPred (ClassP cls tys) = pprClassPred cls tys
+pprPred (IParam ip ty) = ppr ip <> dcolon <> pprType ty
+
+pprClassPred :: Class -> [Type] -> SDoc
+pprClassPred clas tys = parenSymOcc (getOccName clas) (ppr clas)
+ <+> sep (map pprParendType tys)
+
+pprTheta :: ThetaType -> SDoc
+pprTheta theta = parens (sep (punctuate comma (map pprPred theta)))
+
+pprThetaArrow :: ThetaType -> SDoc
+pprThetaArrow theta
+ | null theta = empty
+ | otherwise = parens (sep (punctuate comma (map pprPred theta))) <+> ptext SLIT("=>")
+
+------------------
+instance Outputable Type where
+ ppr ty = pprType ty
+
+instance Outputable PredType where
+ ppr = pprPred
-instance Ord Type where
- compare ty1 ty2 = cmpTy ty1 ty2
+instance Outputable name => OutputableBndr (IPName name) where
+ pprBndr _ n = ppr n -- Simple for now
-cmpTy :: Type -> Type -> Ordering
-cmpTy ty1 ty2
- = cmp emptyVarEnv ty1 ty2
+------------------
+ -- OK, here's the main printer
+
+ppr_type :: Prec -> Type -> SDoc
+ppr_type p (TyVarTy tv) = ppr tv
+ppr_type p (PredTy pred) = braces (ppr pred)
+ppr_type p (NoteTy (SynNote ty1) ty2) = ppr_type p ty1
+ppr_type p (NoteTy other ty2) = ppr_type p ty2
+
+ppr_type p (TyConApp tc tys) = ppr_tc_app p tc tys
+
+ppr_type p (AppTy t1 t2) = maybeParen p TyConPrec $
+ pprType t1 <+> ppr_type TyConPrec t2
+
+ppr_type p ty@(ForAllTy _ _) = ppr_forall_type p ty
+ppr_type p ty@(FunTy (PredTy _) _) = ppr_forall_type p ty
+
+ppr_type p (FunTy ty1 ty2)
+ = -- We don't want to lose synonyms, so we mustn't use splitFunTys here.
+ maybeParen p FunPrec $
+ sep (ppr_type FunPrec ty1 : ppr_fun_tail ty2)
+ where
+ ppr_fun_tail (FunTy ty1 ty2) = (arrow <+> ppr_type FunPrec ty1) : ppr_fun_tail ty2
+ ppr_fun_tail other_ty = [arrow <+> pprType other_ty]
+
+ppr_forall_type :: Prec -> Type -> SDoc
+ppr_forall_type p ty
+ = maybeParen p FunPrec $
+ sep [pprForAll tvs, pprThetaArrow ctxt, pprType tau]
+ where
+ (tvs, rho) = split1 [] ty
+ (ctxt, tau) = split2 [] rho
+
+ split1 tvs (ForAllTy tv ty) = split1 (tv:tvs) ty
+ split1 tvs (NoteTy (FTVNote _) ty) = split1 tvs ty
+ split1 tvs ty = (reverse tvs, ty)
+
+ split2 ps (NoteTy (FTVNote _) arg -- Rather a disgusting case
+ `FunTy` res) = split2 ps (arg `FunTy` res)
+ split2 ps (PredTy p `FunTy` ty) = split2 (p:ps) ty
+ split2 ps (NoteTy (FTVNote _) ty) = split2 ps ty
+ split2 ps ty = (reverse ps, ty)
+
+ppr_tc_app :: Prec -> TyCon -> [Type] -> SDoc
+ppr_tc_app p tc []
+ = ppr_tc tc
+ppr_tc_app p tc [ty]
+ | tc `hasKey` listTyConKey = brackets (pprType ty)
+ | tc `hasKey` parrTyConKey = ptext SLIT("[:") <> pprType ty <> ptext SLIT(":]")
+ppr_tc_app p tc tys
+ | isTupleTyCon tc && tyConArity tc == length tys
+ = tupleParens (tupleTyConBoxity tc) (sep (punctuate comma (map pprType tys)))
+ | otherwise
+ = maybeParen p TyConPrec $
+ ppr_tc tc <+> sep (map (ppr_type TyConPrec) tys)
+
+ppr_tc :: TyCon -> SDoc
+ppr_tc tc = parenSymOcc (getOccName tc) (pp_nt_debug <> ppr tc)
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
+ pp_nt_debug | isNewTyCon tc = ifPprDebug (if isRecursiveTyCon tc
+ then ptext SLIT("<recnt>")
+ else ptext SLIT("<nt>"))
+ | otherwise = empty
+
+-------------------
+pprForAll [] = empty
+pprForAll tvs = ptext SLIT("forall") <+> sep (map pprTvBndr tvs) <> dot
+
+pprTvBndr tv | isLiftedTypeKind kind = ppr tv
+ | otherwise = parens (ppr tv <+> dcolon <+> pprKind kind)
+ where
+ kind = tyVarKind tv
\end{code}