TypeRep.lhs 17.6 KB
Newer Older
1
%
2
% (c) The University of Glasgow 2006
3 4 5 6 7 8
% (c) The GRASP/AQUA Project, Glasgow University, 1998
%
\section[TypeRep]{Type - friends' interface}

\begin{code}
module TypeRep (
9
	TyThing(..), 
10
	Type(..), TyNote(..), 		-- Representation visible 
11
	PredType(..),	 		-- to friends
12
	
13
 	Kind, ThetaType,		-- Synonyms
14

15 16
	funTyCon,

17
	-- Pretty-printing
18 19
	pprType, pprParendType, pprTyThingCategory, 
	pprPred, pprTheta, pprForAll, pprThetaArrow, pprClassPred,
20

21
	-- Kinds
22
	liftedTypeKind, unliftedTypeKind, openTypeKind,
23 24
        argTypeKind, ubxTupleKind,
	isLiftedTypeKindCon, isLiftedTypeKind,
25
	mkArrowKind, mkArrowKinds, isCoercionKind,
26 27 28 29 30 31 32 33 34 35 36 37 38 39 40

        -- Kind constructors...
        liftedTypeKindTyCon, openTypeKindTyCon, unliftedTypeKindTyCon,
        argTypeKindTyCon, ubxTupleKindTyCon,

        -- And their names
        unliftedTypeKindTyConName, openTypeKindTyConName,
        ubxTupleKindTyConName, argTypeKindTyConName,
        liftedTypeKindTyConName,

        -- Super Kinds
	tySuperKind, coSuperKind,
        isTySuperKind, isCoSuperKind,
	tySuperKindTyCon, coSuperKindTyCon,
        
41
	pprKind, pprParendKind
42 43 44 45
    ) where

#include "HsVersions.h"

46
import {-# SOURCE #-} DataCon( DataCon, dataConName )
47

48 49 50 51 52 53 54 55
-- friends:
import Var
import VarSet
import Name
import OccName
import BasicTypes
import TyCon
import Class
56 57

-- others
58
import PrelNames
59
import Outputable
60 61 62 63 64 65 66 67 68 69 70
\end{code}

%************************************************************************
%*									*
\subsection{Type Classifications}
%*									*
%************************************************************************

A type is

	*unboxed*	iff its representation is other than a pointer
71
			Unboxed types are also unlifted.
72 73 74 75 76 77

	*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.
78 79

			Only lifted types may be unified with a type variable.
80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109

	*algebraic*	A type with one or more constructors, whether declared
			with "data" or "newtype".   
			An algebraic type is one that can be deconstructed
			with a case expression.  
			*NOT* the same as lifted types,  because we also 
			include unboxed tuples in this classification.

	*data*		A type declared with "data".  Also boxed tuples.

	*primitive*	iff it is a built-in type that can't be expressed
			in Haskell.

Currently, all primitive types are unlifted, but that's not necessarily
the case.  (E.g. Int could be primitive.)

Some primitive types are unboxed, such as Int#, whereas some are boxed
but unlifted (such as ByteArray#).  The only primitive types that we
classify as algebraic are the unboxed tuples.

examples of type classifications:

Type		primitive	boxed		lifted		algebraic    
-----------------------------------------------------------------------------
Int#,		Yes		No		No		No
ByteArray#	Yes		Yes		No		No
(# a, b #)	Yes		No		No		Yes
(  a, b  )	No		Yes		Yes		Yes
[a]		No		Yes		Yes		Yes

110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130


	----------------------
	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.  

131 132
Solution: 

133
* Newtypes are always represented using TyConApp.
134

135 136 137 138 139
* 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".
140

141 142 143
  Applications of the data constructor P simply vanish:
	P x = x
  
144

145 146 147 148 149
* 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.
150

151 152
The typechecker (TcTyDecls) identifies enough type construtors as 'recursive'
to cut all loops.  The other members of the loop may be marked 'non-recursive'.
153 154


155 156 157 158 159 160 161 162 163
%************************************************************************
%*									*
\subsection{The data type}
%*									*
%************************************************************************


\begin{code}
data Type
164
  = TyVarTy TyVar	
165 166

  | AppTy
167
	Type		-- Function is *not* a TyConApp
168 169
	Type		-- It must be another AppTy, or TyVarTy
			-- (or NoteTy of these)
170

171
  | TyConApp		-- Application of a TyCon, including newtypes *and* synonyms
172
	TyCon		--  *Invariant* saturated appliations of FunTyCon and
173
			-- 	synonyms have their own constructors, below.
174 175
			-- However, *unsaturated* FunTyCons do appear as TyConApps.  
			-- 
176
	[Type]		-- Might not be saturated.
177 178 179
			-- Even type synonyms are not necessarily saturated;
			-- for example unsaturated type synonyms can appear as the 
			-- RHS of a type synonym.
180

181
  | FunTy		-- Special case of TyConApp: TyConApp FunTyCon [t1,t2]
182 183 184
	Type
	Type

185 186 187 188
  | ForAllTy		-- A polymorphic type
	TyVar
	Type	

chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
189
  | PredTy		-- The type of evidence for a type predictate
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
190
	PredType	-- See Note [PredTy], and Note [Equality predicates]
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
191 192 193
	-- NB: A PredTy (EqPred _ _) can appear only as the kind
	--     of a coercion variable; never as the argument or result
	--     of a FunTy (unlike ClassP, IParam)
194 195

  | NoteTy 		-- A type with a note attached
196 197 198
	TyNote
	Type		-- The expanded version

199 200 201 202 203 204 205 206 207
type Kind = Type 	-- Invariant: a kind is always
			--	FunTy k1 k2
			-- or	TyConApp PrimTyCon [...]
			-- or	TyVar kv (during inference only)
			-- or   ForAll ... (for top-level coercions)

type SuperKind = Type   -- Invariant: a super kind is always 
                        --   TyConApp SuperKindTyCon ...

208
data TyNote = FTVNote TyVarSet	-- The free type variables of the noted expression
209 210 211
\end{code}

-------------------------------------
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
212
 		Note [PredTy]
213 214

A type of the form
215 216 217
	PredTy p
represents a value whose type is the Haskell predicate p, 
where a predicate is what occurs before the '=>' in a Haskell type.
218 219 220 221 222
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

223 224 225 226 227 228 229 230 231
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*
Predicates are represented inside GHC by PredType:

\begin{code}
232
data PredType 
233 234
  = ClassP Class [Type]		-- Class predicate
  | IParam (IPName Name) Type	-- Implicit parameter
235
  | EqPred Type Type		-- Equality predicate (ty1 ~ ty2)
236

237
type ThetaType = [PredType]
238 239
\end{code}

240 241 242 243 244 245 246 247 248 249 250 251
(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).

chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
252 253
Note [Equality predicates]
~~~~~~~~~~~~~~~~~~~~~~~~~~
254
	forall a b. (a ~ S b) => a -> b
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
255 256 257 258 259 260 261 262 263 264 265 266 267 268 269
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.

270

271 272 273 274 275 276 277 278 279
%************************************************************************
%*									*
			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.
280 281

\begin{code}
282 283 284 285
data TyThing = AnId     Id
	     | ADataCon DataCon
	     | ATyCon   TyCon
	     | AClass   Class
286 287

instance Outputable TyThing where
288 289 290 291 292 293 294
  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")
295 296 297 298 299 300

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
301
\end{code}
302

303

304 305
%************************************************************************
%*									*
306
		Wired-in type constructors
307 308 309 310 311 312
%*									*
%************************************************************************

We define a few wired-in type constructors here to avoid module knots

\begin{code}
313 314 315
--------------------------
-- First the TyCons...

316 317
funTyCon = mkFunTyCon funTyConName (mkArrowKinds [argTypeKind, openTypeKind] liftedTypeKind)
	-- You might think that (->) should have type (?? -> ? -> *), and you'd be right
318 319
	-- But if we do that we get kind errors when saying
	--	instance Control.Arrow (->)
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
320
	-- becuase the expected kind is (*->*->*).  The trouble is that the
321 322 323
	-- 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.
324

325 326

tySuperKindTyCon     = mkSuperKindTyCon tySuperKindTyConName
327
coSuperKindTyCon     = mkSuperKindTyCon coSuperKindTyConName
328 329 330 331 332 333 334 335

liftedTypeKindTyCon   = mkKindTyCon liftedTypeKindTyConName
openTypeKindTyCon     = mkKindTyCon openTypeKindTyConName
unliftedTypeKindTyCon = mkKindTyCon unliftedTypeKindTyConName
ubxTupleKindTyCon     = mkKindTyCon ubxTupleKindTyConName
argTypeKindTyCon      = mkKindTyCon argTypeKindTyConName

mkKindTyCon :: Name -> TyCon
336
mkKindTyCon name = mkVoidPrimTyCon name tySuperKind 0
337 338 339 340

--------------------------
-- ... and now their names

341 342
tySuperKindTyConName      = mkPrimTyConName FSLIT("BOX") tySuperKindTyConKey tySuperKindTyCon
coSuperKindTyConName      = mkPrimTyConName FSLIT("COERCION") coSuperKindTyConKey coSuperKindTyCon
343 344 345
liftedTypeKindTyConName   = mkPrimTyConName FSLIT("*") liftedTypeKindTyConKey liftedTypeKindTyCon
openTypeKindTyConName     = mkPrimTyConName FSLIT("?") openTypeKindTyConKey openTypeKindTyCon
unliftedTypeKindTyConName = mkPrimTyConName FSLIT("#") unliftedTypeKindTyConKey unliftedTypeKindTyCon
346
ubxTupleKindTyConName     = mkPrimTyConName FSLIT("(#)") ubxTupleKindTyConKey ubxTupleKindTyCon
347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378
argTypeKindTyConName      = mkPrimTyConName FSLIT("??") argTypeKindTyConKey argTypeKindTyCon
funTyConName              = mkPrimTyConName FSLIT("(->)") funTyConKey funTyCon

mkPrimTyConName occ key tycon = mkWiredInName gHC_PRIM (mkOccNameFS tcName 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 []

liftedTypeKind   = kindTyConType liftedTypeKindTyCon
unliftedTypeKind = kindTyConType unliftedTypeKindTyCon
openTypeKind     = kindTyConType openTypeKindTyCon
argTypeKind      = kindTyConType argTypeKindTyCon
ubxTupleKind	 = kindTyConType ubxTupleKindTyCon

mkArrowKind :: Kind -> Kind -> Kind
mkArrowKind k1 k2 = FunTy k1 k2

mkArrowKinds :: [Kind] -> Kind -> Kind
mkArrowKinds arg_kinds result_kind = foldr mkArrowKind result_kind arg_kinds

tySuperKind, coSuperKind :: SuperKind
tySuperKind = kindTyConType tySuperKindTyCon 
coSuperKind = kindTyConType coSuperKindTyCon 

379
isTySuperKind (NoteTy _ ty)    = isTySuperKind ty
380 381 382
isTySuperKind (TyConApp kc []) = kc `hasKey` tySuperKindTyConKey
isTySuperKind other            = False

383
isCoSuperKind :: SuperKind -> Bool
384
isCoSuperKind (NoteTy _ ty)    = isCoSuperKind ty
385 386 387 388
isCoSuperKind (TyConApp kc []) = kc `hasKey` coSuperKindTyConKey
isCoSuperKind other            = False

-------------------
389
-- Lastly we need a few functions on Kinds
390 391 392

isLiftedTypeKindCon tc    = tc `hasKey` liftedTypeKindTyConKey

393
isLiftedTypeKind :: Kind -> Bool
394 395 396
isLiftedTypeKind (TyConApp tc []) = isLiftedTypeKindCon tc
isLiftedTypeKind other            = False

397
isCoercionKind :: Kind -> Bool
398
-- All coercions are of form (ty1 ~ ty2)
399 400 401 402 403
-- This function is here rather than in Coercion, 
-- because it's used in a knot-tied way to enforce invariants in Var
isCoercionKind (NoteTy _ k)         = isCoercionKind k
isCoercionKind (PredTy (EqPred {})) = True
isCoercionKind other		    = False
404 405 406
\end{code}


407

408 409
%************************************************************************
%*									*
410
\subsection{The external interface}
411 412 413
%*									*
%************************************************************************

414 415 416 417 418
@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.

419
\begin{code}
420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438
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
439
pprPred (EqPred ty1 ty2) = sep [ppr ty1, nest 2 (ptext SLIT("~")), ppr ty2]
440 441

pprClassPred :: Class -> [Type] -> SDoc
442 443
pprClassPred clas tys = parenSymOcc (getOccName clas) (ppr clas) 
			<+> sep (map pprParendType tys)
444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465

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 Outputable name => OutputableBndr (IPName name) where
    pprBndr _ n = ppr n	-- Simple for now

------------------
	-- OK, here's the main printer

466 467 468
pprKind = pprType
pprParendKind = pprParendType

469
ppr_type :: Prec -> Type -> SDoc
470
ppr_type p (TyVarTy tv)       = ppr tv
471
ppr_type p (PredTy pred)      = ifPprDebug (ptext SLIT("<pred>")) <> (ppr pred)
472 473
ppr_type p (NoteTy other ty2) = ppr_type p ty2
ppr_type p (TyConApp tc tys)  = ppr_tc_app p tc tys
474 475 476 477

ppr_type p (AppTy t1 t2) = maybeParen p TyConPrec $
			   pprType t1 <+> ppr_type TyConPrec t2

478 479 480
ppr_type p ty@(ForAllTy _ _)       = ppr_forall_type p ty
ppr_type p ty@(FunTy (PredTy _) _) = ppr_forall_type p ty

481 482 483 484 485 486 487 488
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]

489 490
ppr_forall_type :: Prec -> Type -> SDoc
ppr_forall_type p ty
491 492 493 494 495 496
  = maybeParen p FunPrec $
    sep [pprForAll tvs, pprThetaArrow ctxt, pprType tau]
  where
    (tvs,  rho) = split1 [] ty
    (ctxt, tau) = split2 [] rho

497 498 499
    split1 tvs (ForAllTy tv ty) = split1 (tv:tvs) ty
    split1 tvs (NoteTy _ ty)    = split1 tvs ty
    split1 tvs ty		= (reverse tvs, ty)
500
 
501
    split2 ps (NoteTy _ arg 	-- Rather a disgusting case
502
	       `FunTy` res) 	      = split2 ps (arg `FunTy` res)
503
    split2 ps (PredTy p `FunTy` ty)   = split2 (p:ps) ty
504
    split2 ps (NoteTy _ ty) 	      = split2 ps ty
505
    split2 ps ty		      = (reverse ps, ty)
506 507

ppr_tc_app :: Prec -> TyCon -> [Type] -> SDoc
508
ppr_tc_app p tc [] 
509
  = ppr_tc tc
510 511 512
ppr_tc_app p tc [ty] 
  | tc `hasKey` listTyConKey = brackets (pprType ty)
  | tc `hasKey` parrTyConKey = ptext SLIT("[:") <> pprType ty <> ptext SLIT(":]")
513 514 515 516 517 518
  | 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("??")

519 520 521 522 523
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 $
524 525 526
    ppr_tc tc <+> sep (map (ppr_type TyConPrec) tys)

ppr_tc :: TyCon -> SDoc
527 528 529 530 531 532 533
ppr_tc tc = parenSymOcc (getOccName 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

534
-------------------
535
pprForAll []  = empty
536 537 538 539 540 541 542 543
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}