Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
tree: 46809fa916
Fetching contributors…

Cannot retrieve contributors at this time

606 lines (479 sloc) 20.638 kB
%
% (c) The University of Glasgow 2006
% (c) The GRASP/AQUA Project, Glasgow University, 1998
%
\section[TypeRep]{Type - friends' interface}
\begin{code}
-- We expose the relevant stuff from this module via the Type module
{-# OPTIONS_HADDOCK hide #-}
{-# LANGUAGE DeriveDataTypeable #-}
module TypeRep (
TyThing(..),
Type(..),
PredType(..), -- to friends
Kind, ThetaType, -- Synonyms
funTyCon, funTyConName,
-- Pretty-printing
pprType, pprParendType, pprTypeApp,
pprTyThing, pprTyThingCategory,
pprPred, pprEqPred, pprTheta, pprForAll, pprThetaArrow, pprClassPred,
-- Kinds
liftedTypeKind, unliftedTypeKind, openTypeKind,
argTypeKind, ubxTupleKind,
isLiftedTypeKindCon, isLiftedTypeKind,
mkArrowKind, mkArrowKinds, isCoercionKind,
coVarPred,
-- Kind constructors...
liftedTypeKindTyCon, openTypeKindTyCon, unliftedTypeKindTyCon,
argTypeKindTyCon, ubxTupleKindTyCon,
-- And their names
unliftedTypeKindTyConName, openTypeKindTyConName,
ubxTupleKindTyConName, argTypeKindTyConName,
liftedTypeKindTyConName,
-- Super Kinds
tySuperKind, coSuperKind,
isTySuperKind, isCoSuperKind,
tySuperKindTyCon, coSuperKindTyCon,
pprKind, pprParendKind
) where
#include "HsVersions.h"
import {-# SOURCE #-} DataCon( DataCon, dataConName )
-- friends:
import Var
import Name
import BasicTypes
import TyCon
import Class
-- others
import PrelNames
import Outputable
import FastString
-- libraries
import Data.Data hiding ( TyCon )
\end{code}
----------------------
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}
-- | The key representation of types within the compiler
data Type
= TyVarTy TyVar -- ^ Vanilla type variable
| AppTy
Type
Type -- ^ Type application to something other than a 'TyCon'. Parameters:
--
-- 1) Function: must /not/ be a 'TyConApp', must be another 'AppTy', or 'TyVarTy'
--
-- 2) Argument type
| TyConApp
TyCon
[Type] -- ^ Application of a 'TyCon', including newtypes /and/ synonyms.
-- Invariant: saturated appliations of 'FunTyCon' must
-- use 'FunTy' and saturated synonyms must use their own
-- constructors. However, /unsaturated/ 'FunTyCon's do appear as 'TyConApp's.
-- Parameters:
--
-- 1) Type constructor being applied to.
--
-- 2) Type arguments. Might not have enough type arguments here to saturate the constructor.
-- Even type synonyms are not necessarily saturated; for example unsaturated type synonyms
-- can appear as the right hand side of a type synonym.
| FunTy
Type
Type -- ^ Special case of 'TyConApp': @TyConApp FunTyCon [t1, t2]@
| ForAllTy
TyVar
Type -- ^ A polymorphic type
| PredTy
PredType -- ^ The type of evidence for a type predictate.
-- Note that a @PredTy (EqPred _ _)@ can appear only as the kind
-- of a coercion variable; never as the argument or result
-- of a 'FunTy' (unlike the 'PredType' constructors 'ClassP' or 'IParam')
-- See Note [PredTy], and Note [Equality predicates]
deriving (Data, Typeable)
-- | The key type representing kinds in the compiler.
-- Invariant: a kind is always in one of these forms:
--
-- > FunTy k1 k2
-- > TyConApp PrimTyCon [...]
-- > TyVar kv -- (during inference only)
-- > ForAll ... -- (for top-level coercions)
type Kind = Type
-- | "Super kinds", used to help encode 'Kind's as types.
-- Invariant: a super kind is always of this form:
--
-- > TyConApp SuperKindTyCon ...
type SuperKind = Type
\end{code}
-------------------------------------
Note [PredTy]
\begin{code}
-- | 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
-- > 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\"
data PredType
= ClassP Class [Type] -- ^ Class predicate e.g. @Eq a@
| IParam (IPName Name) Type -- ^ Implicit parameter e.g. @?x :: Int@
| EqPred Type Type -- ^ Equality predicate e.g @ty1 ~ ty2@
deriving (Data, Typeable)
-- | A collection of 'PredType's
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).
Note [Equality predicates]
~~~~~~~~~~~~~~~~~~~~~~~~~~
forall a b. (a ~ S b) => a -> b
could be represented by
ForAllTy a (ForAllTy b (FunTy (PredTy (EqPred a (S b))) ...))
OR
ForAllTy a (ForAllTy b (ForAllTy (c::PredTy (EqPred a (S b))) ...))
The latter is what we do. (Unlike for class and implicit parameter
constraints, which do use FunTy.)
Reason:
* FunTy is always a *value* function
* ForAllTy is discarded at runtime
We often need to make a "wildcard" (c::PredTy..). We always use the same
name (wildCoVarName), since it's not mentioned.
%************************************************************************
%* *
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}
-- | A typecheckable-thing, essentially anything that has a name
data TyThing = AnId Id
| ADataCon DataCon
| ATyCon TyCon
| AClass Class
instance Outputable TyThing where
ppr = pprTyThing
pprTyThing :: TyThing -> SDoc
pprTyThing 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}
%************************************************************************
%* *
Wired-in type constructors
%* *
%************************************************************************
We define a few wired-in type constructors here to avoid module knots
\begin{code}
--------------------------
-- First the TyCons...
-- | See "Type#kind_subtyping" for details of the distinction between the 'Kind' 'TyCon's
funTyCon, tySuperKindTyCon, coSuperKindTyCon, liftedTypeKindTyCon,
openTypeKindTyCon, unliftedTypeKindTyCon,
ubxTupleKindTyCon, argTypeKindTyCon
:: TyCon
funTyConName, tySuperKindTyConName, coSuperKindTyConName, liftedTypeKindTyConName,
openTypeKindTyConName, unliftedTypeKindTyConName,
ubxTupleKindTyConName, argTypeKindTyConName
:: Name
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.
tySuperKindTyCon = mkSuperKindTyCon tySuperKindTyConName
coSuperKindTyCon = mkSuperKindTyCon coSuperKindTyConName
liftedTypeKindTyCon = mkKindTyCon liftedTypeKindTyConName tySuperKind
openTypeKindTyCon = mkKindTyCon openTypeKindTyConName tySuperKind
unliftedTypeKindTyCon = mkKindTyCon unliftedTypeKindTyConName tySuperKind
ubxTupleKindTyCon = mkKindTyCon ubxTupleKindTyConName tySuperKind
argTypeKindTyCon = mkKindTyCon argTypeKindTyConName tySuperKind
--------------------------
-- ... and now their names
tySuperKindTyConName = mkPrimTyConName (fsLit "BOX") tySuperKindTyConKey tySuperKindTyCon
coSuperKindTyConName = mkPrimTyConName (fsLit "COERCION") coSuperKindTyConKey coSuperKindTyCon
liftedTypeKindTyConName = mkPrimTyConName (fsLit "*") liftedTypeKindTyConKey liftedTypeKindTyCon
openTypeKindTyConName = mkPrimTyConName (fsLit "?") openTypeKindTyConKey openTypeKindTyCon
unliftedTypeKindTyConName = mkPrimTyConName (fsLit "#") unliftedTypeKindTyConKey unliftedTypeKindTyCon
ubxTupleKindTyConName = mkPrimTyConName (fsLit "(#)") ubxTupleKindTyConKey ubxTupleKindTyCon
argTypeKindTyConName = mkPrimTyConName (fsLit "??") argTypeKindTyConKey argTypeKindTyCon
funTyConName = mkPrimTyConName (fsLit "(->)") funTyConKey funTyCon
mkPrimTyConName :: FastString -> Unique -> TyCon -> Name
mkPrimTyConName occ key tycon = mkWiredInName gHC_PRIM (mkTcOccFS occ)
key
(ATyCon tycon)
BuiltInSyntax
-- All of the super kinds and kinds are defined in Prim and use BuiltInSyntax,
-- because they are never in scope in the source
------------------
-- We also need Kinds and SuperKinds, locally and in TyCon
kindTyConType :: TyCon -> Type
kindTyConType kind = TyConApp kind []
-- | See "Type#kind_subtyping" for details of the distinction between these 'Kind's
liftedTypeKind, unliftedTypeKind, openTypeKind, argTypeKind, ubxTupleKind :: Kind
liftedTypeKind = kindTyConType liftedTypeKindTyCon
unliftedTypeKind = kindTyConType unliftedTypeKindTyCon
openTypeKind = kindTyConType openTypeKindTyCon
argTypeKind = kindTyConType argTypeKindTyCon
ubxTupleKind = kindTyConType ubxTupleKindTyCon
-- | Given two kinds @k1@ and @k2@, creates the 'Kind' @k1 -> k2@
mkArrowKind :: Kind -> Kind -> Kind
mkArrowKind k1 k2 = FunTy k1 k2
-- | Iterated application of 'mkArrowKind'
mkArrowKinds :: [Kind] -> Kind -> Kind
mkArrowKinds arg_kinds result_kind = foldr mkArrowKind result_kind arg_kinds
tySuperKind, coSuperKind :: SuperKind
tySuperKind = kindTyConType tySuperKindTyCon
coSuperKind = kindTyConType coSuperKindTyCon
isTySuperKind :: SuperKind -> Bool
isTySuperKind (TyConApp kc []) = kc `hasKey` tySuperKindTyConKey
isTySuperKind _ = False
isCoSuperKind :: SuperKind -> Bool
isCoSuperKind (TyConApp kc []) = kc `hasKey` coSuperKindTyConKey
isCoSuperKind _ = False
-------------------
-- Lastly we need a few functions on Kinds
isLiftedTypeKindCon :: TyCon -> Bool
isLiftedTypeKindCon tc = tc `hasKey` liftedTypeKindTyConKey
isLiftedTypeKind :: Kind -> Bool
isLiftedTypeKind (TyConApp tc []) = isLiftedTypeKindCon tc
isLiftedTypeKind _ = False
isCoercionKind :: Kind -> Bool
-- All coercions are of form (ty1 ~ ty2)
-- This function is here rather than in Coercion,
-- because it's used in a knot-tied way to enforce invariants in Var
isCoercionKind (PredTy (EqPred {})) = True
isCoercionKind _ = False
coVarPred :: CoVar -> PredType
coVarPred tv
= ASSERT( isCoVar tv )
case tyVarKind tv of
PredTy eq -> eq
other -> pprPanic "coVarPred" (ppr tv $$ ppr other)
\end{code}
%************************************************************************
%* *
\subsection{The external interface}
%* *
%************************************************************************
@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}
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
pprTypeApp :: NamedThing a => a -> [Type] -> SDoc
-- The first arg is the tycon, or sometimes class
-- Print infix if the tycon/class looks like an operator
pprTypeApp tc tys = ppr_type_app TopPrec (getName tc) tys
------------------
pprPred :: PredType -> SDoc
pprPred (ClassP cls tys) = pprClassPred cls tys
pprPred (IParam ip ty) = ppr ip <> dcolon <> pprType ty
pprPred (EqPred ty1 ty2) = pprEqPred (ty1,ty2)
pprEqPred :: (Type,Type) -> SDoc
pprEqPred (ty1,ty2) = sep [ ppr_type FunPrec ty1
, nest 2 (ptext (sLit "~"))
, ppr_type FunPrec ty2]
-- Precedence looks like (->) so that we get
-- Maybe a ~ Bool
-- (a->a) ~ Bool
-- Note parens on the latter!
pprClassPred :: Class -> [Type] -> SDoc
pprClassPred clas tys = ppr_type_app TopPrec (getName clas) tys
pprTheta :: ThetaType -> SDoc
-- pprTheta [pred] = pprPred pred -- I'm in two minds about this
pprTheta theta = parens (sep (punctuate comma (map pprPred theta)))
pprThetaArrow :: ThetaType -> SDoc
pprThetaArrow [] = empty
pprThetaArrow [pred]
| noParenPred pred = pprPred pred <+> darrow
pprThetaArrow preds = parens (sep (punctuate comma (map pprPred preds))) <+> darrow
noParenPred :: PredType -> Bool
-- A predicate that can appear without parens before a "=>"
-- C a => a -> a
-- a~b => a -> b
-- But (?x::Int) => Int -> Int
noParenPred (ClassP {}) = True
noParenPred (EqPred {}) = True
noParenPred (IParam {}) = False
------------------
instance Outputable Type where
ppr ty = pprType ty
instance Outputable PredType where
ppr = pprPred
instance Outputable name => OutputableBndr (IPName name) where
pprBndr _ n = ppr n -- Simple for now
------------------
-- OK, here's the main printer
pprKind, pprParendKind :: Kind -> SDoc
pprKind = pprType
pprParendKind = pprParendType
ppr_type :: Prec -> Type -> SDoc
ppr_type _ (TyVarTy tv) -- Note [Infix type variables]
| isSymOcc (getOccName tv) = parens (ppr tv)
| otherwise = ppr tv
ppr_type p (PredTy pred) = maybeParen p TyConPrec $
ifPprDebug (ptext (sLit "<pred>")) <> (ppr pred)
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)
| not (is_pred ty1) = (arrow <+> ppr_type FunPrec ty1) : ppr_fun_tail ty2
ppr_fun_tail other_ty = [arrow <+> pprType other_ty]
is_pred (PredTy {}) = True
is_pred _ = False
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
-- We need to be extra careful here as equality constraints will occur as
-- type variables with an equality kind. So, while collecting quantified
-- variables, we separate the coercion variables out and turn them into
-- equality predicates.
split1 tvs (ForAllTy tv ty)
| not (isCoVar tv) = split1 (tv:tvs) ty
split1 tvs ty = (reverse tvs, ty)
split2 ps (PredTy p `FunTy` ty) = split2 (p:ps) ty
split2 ps (ForAllTy tv ty)
| isCoVar tv = split2 (coVarPred tv : ps) ty
split2 ps ty = (reverse ps, ty)
ppr_tc_app :: Prec -> TyCon -> [Type] -> SDoc
ppr_tc_app _ tc []
= ppr_tc tc
ppr_tc_app _ tc [ty]
| tc `hasKey` listTyConKey = brackets (pprType ty)
| tc `hasKey` parrTyConKey = ptext (sLit "[:") <> pprType ty <> ptext (sLit ":]")
| tc `hasKey` liftedTypeKindTyConKey = ptext (sLit "*")
| tc `hasKey` unliftedTypeKindTyConKey = ptext (sLit "#")
| tc `hasKey` openTypeKindTyConKey = ptext (sLit "(?)")
| tc `hasKey` ubxTupleKindTyConKey = ptext (sLit "(#)")
| tc `hasKey` argTypeKindTyConKey = ptext (sLit "??")
ppr_tc_app p tc tys
| isTupleTyCon tc && tyConArity tc == length tys
= tupleParens (tupleTyConBoxity tc) (sep (punctuate comma (map pprType tys)))
| otherwise
= ppr_type_app p (getName tc) tys
ppr_type_app :: Prec -> Name -> [Type] -> SDoc
-- Used for classes as well as types; that's why it's separate from ppr_tc_app
ppr_type_app p tc tys
| is_sym_occ -- Print infix if possible
, [ty1,ty2] <- tys -- We know nothing of precedence though
= maybeParen p FunPrec (sep [ppr_type FunPrec ty1,
pprInfixVar True (ppr tc) <+> ppr_type FunPrec ty2])
| otherwise
= maybeParen p TyConPrec (hang (pprPrefixVar is_sym_occ (ppr tc))
2 (sep (map pprParendType tys)))
where
is_sym_occ = isSymOcc (getOccName tc)
ppr_tc :: TyCon -> SDoc -- No brackets for SymOcc
ppr_tc tc
= pp_nt_debug <> ppr tc
where
pp_nt_debug | isNewTyCon tc = ifPprDebug (if isRecursiveTyCon tc
then ptext (sLit "<recnt>")
else ptext (sLit "<nt>"))
| otherwise = empty
-------------------
pprForAll :: [TyVar] -> SDoc
pprForAll [] = empty
pprForAll tvs = ptext (sLit "forall") <+> sep (map pprTvBndr tvs) <> dot
pprTvBndr :: TyVar -> SDoc
pprTvBndr tv | isLiftedTypeKind kind = ppr tv
| otherwise = parens (ppr tv <+> dcolon <+> pprKind kind)
where
kind = tyVarKind tv
\end{code}
Note [Infix type variables]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
With TypeOperators you can say
f :: (a ~> b) -> b
and the (~>) is considered a type variable. However, the type
pretty-printer in this module will just see (a ~> b) as
App (App (TyVarTy "~>") (TyVarTy "a")) (TyVarTy "b")
So it'll print the type in prefix form. To avoid confusion we must
remember to parenthesise the operator, thus
(~>) a b -> b
See Trac #2766.
Jump to Line
Something went wrong with that request. Please try again.