TcType.lhs 47.6 KB
Newer Older
1
%
2
% (c) The University of Glasgow 2006
3
4
5
6
% (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
%
\section[TcType]{Types used in the typechecker}

7
8
This module provides the Type interface for front-end parts of the 
compiler.  These parts 
9

10
11
12
	* treat "source types" as opaque: 
		newtypes, and predicates are meaningful. 
	* look through usage types
13

14
The "tc" prefix is for "TypeChecker", because the type checker
15
is the principal client.
16

17
18
\begin{code}
module TcType (
19
  --------------------------------
20
  -- Types 
21
  TcType, TcSigmaType, TcRhoType, TcTauType, TcPredType, TcThetaType, 
22
  TcTyVar, TcTyVarSet, TcKind, 
23

24
25
  BoxyTyVar, BoxySigmaType, BoxyRhoType, BoxyThetaType, BoxyType,

26
  --------------------------------
27
  -- MetaDetails
28
29
30
  UserTypeCtxt(..), pprUserTypeCtxt,
  TcTyVarDetails(..), BoxInfo(..), pprTcTyVarDetails,
  MetaDetails(Flexi, Indirect), SkolemInfo(..), pprSkolTvBinding, pprSkolInfo,
31
32
  isImmutableTyVar, isSkolemTyVar, isMetaTyVar, isBoxyTyVar, 
  isSigTyVar, isExistentialTyVar,  isTyConableTyVar,
33
  metaTvRef, 
34
  isFlexi, isIndirect, isRuntimeUnk, isUnk,
35
36

  --------------------------------
37
  -- Builders
38
  mkPhiTy, mkSigmaTy, 
39

40
41
42
  --------------------------------
  -- Splitters  
  -- These are important because they do not look through newtypes
43
  tcView,
44
  tcSplitForAllTys, tcSplitPhiTy, tcSplitPredFunTy_maybe,
45
  tcSplitFunTy_maybe, tcSplitFunTys, tcFunArgTy, tcFunResultTy, tcSplitFunTysN,
46
  tcSplitTyConApp, tcSplitTyConApp_maybe, tcTyConAppTyCon, tcTyConAppArgs,
47
  tcSplitAppTy_maybe, tcSplitAppTy, tcSplitAppTys, repSplitAppTy_maybe,
48
49
  tcInstHeadTyNotSynonym, tcInstHeadTyAppAllTyVars,
  tcGetTyVar_maybe, tcGetTyVar,
50
  tcSplitSigmaTy, tcMultiSplitSigmaTy, 
51
52
53
54

  ---------------------------------
  -- Predicates. 
  -- Again, newtypes are opaque
55
  tcEqType, tcEqTypes, tcEqPred, tcCmpType, tcCmpTypes, tcCmpPred, tcEqTypeX,
56
  eqKind, 
57
  isSigmaTy, isOverloadedTy, isRigidTy, isBoxyTy,
Ian Lynagh's avatar
Ian Lynagh committed
58
  isDoubleTy, isFloatTy, isIntTy, isWordTy, isStringTy,
59
  isIntegerTy, isBoolTy, isUnitTy, isCharTy,
60
  isTauTy, isTauTyCon, tcIsTyVarTy, tcIsForAllTy, 
61
  isOpenSynTyConApp,
62
63
64

  ---------------------------------
  -- Misc type manipulators
65
  deNoteType,
66
  tyClsNamesOfType, tyClsNamesOfDFunHead, 
67
68
69
70
  getDFunTyKey,

  ---------------------------------
  -- Predicate types  
71
  getClassPredTys_maybe, getClassPredTys, 
72
  isClassPred, isTyVarClassPred, isEqPred, 
73
  mkDictTy, tcSplitPredTy_maybe, 
74
75
  isPredTy, isDictTy, isDictLikeTy,
  tcSplitDFunTy, tcSplitDFunHead, predTyUnique, 
76
  mkClassPred, isInheritablePred, isIPPred, 
77
  isRefineableTy, isRefineablePred,
78

79
80
81
82
83
84
85
86
  ---------------------------------
  -- Foreign import and export
  isFFIArgumentTy,     -- :: DynFlags -> Safety -> Type -> Bool
  isFFIImportResultTy, -- :: DynFlags -> Type -> Bool
  isFFIExportResultTy, -- :: Type -> Bool
  isFFIExternalTy,     -- :: Type -> Bool
  isFFIDynArgumentTy,  -- :: Type -> Bool
  isFFIDynResultTy,    -- :: Type -> Bool
87
88
  isFFIPrimArgumentTy, -- :: DynFlags -> Type -> Bool
  isFFIPrimResultTy,   -- :: DynFlags -> Type -> Bool
89
  isFFILabelTy,        -- :: Type -> Bool
sof's avatar
sof committed
90
91
  isFFIDotnetTy,       -- :: DynFlags -> Type -> Bool
  isFFIDotnetObjTy,    -- :: Type -> Bool
92
  isFFITy,	       -- :: Type -> Bool
93
  isFunPtrTy,          -- :: Type -> Bool
94
  tcSplitIOType_maybe, -- :: Type -> Maybe Type  
sof's avatar
sof committed
95
  toDNType,            -- :: Type -> DNType
96

97
98
  --------------------------------
  -- Rexported from Type
99
  Kind, 	-- Stuff to do with kinds is insensitive to pre/post Tc
100
  unliftedTypeKind, liftedTypeKind, argTypeKind,
Simon Marlow's avatar
Simon Marlow committed
101
  openTypeKind, mkArrowKind, mkArrowKinds, 
102
  isLiftedTypeKind, isUnliftedTypeKind, isSubOpenTypeKind, 
103
  isSubArgTypeKind, isSubKind, splitKindFunTys, defaultKind,
104
  kindVarRef, mkKindVar,  
105

106
  Type, PredType(..), ThetaType, 
107
108
  mkForAllTy, mkForAllTys, 
  mkFunTy, mkFunTys, zipFunTys, 
109
  mkTyConApp, mkAppTy, mkAppTys, applyTy, applyTys,
110
  mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy, mkPredTys, 
111

112
113
  -- Type substitutions
  TvSubst(..), 	-- Representation visible to a few friends
114
  TvSubstEnv, emptyTvSubst, substEqSpec,
115
116
117
  mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst, mkTopTvSubst, notElemTvSubst,
  getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope, lookupTyVar,
  extendTvSubst, extendTvSubstList, isInScope, mkTvSubst, zipTyEnv,
118
  substTy, substTys, substTyWith, substTheta, substTyVar, substTyVars, substTyVarBndr,
119

120
121
  isUnLiftedType,	-- Source types are always lifted
  isUnboxedTupleType,	-- Ditto
122
  isPrimitiveType, 
123

124
  tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
125
  tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars, tidySkolemTyVar,
126
  typeKind, tidyKind,
127

128
  tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
129
130
  tcTyVarsOfType, tcTyVarsOfTypes, tcTyVarsOfPred, exactTyVarsOfType,
  exactTyVarsOfTypes, 
131

132
  pprKind, pprParendKind,
133
  pprType, pprParendType, pprTypeApp, pprTyThingCategory,
134
  pprPred, pprTheta, pprThetaArrow, pprClassPred
135

136
  ) where
137

138
#include "HsVersions.h"
139

140
-- friends:
141
142
143
144
145
import TypeRep
import DataCon
import Class
import Var
import ForeignCall
146
import VarSet
147
import Type
148
import Coercion
149
import TyCon
150
151

-- others:
152
153
import DynFlags
import Name
154
import NameSet
155
156
157
158
159
160
161
162
import VarEnv
import OccName
import PrelNames
import TysWiredIn
import BasicTypes
import Util
import Maybes
import ListSetOps
163
import Outputable
164
import FastString
Simon Marlow's avatar
Simon Marlow committed
165

166
import Data.List
Simon Marlow's avatar
Simon Marlow committed
167
import Data.IORef
168
169
\end{code}

170
171
%************************************************************************
%*									*
172
173
174
175
\subsection{Types}
%*									*
%************************************************************************

176
177
178
The type checker divides the generic Type world into the 
following more structured beasts:

179
sigma ::= forall tyvars. phi
180
181
182
183
184
185
186
187
188
189
	-- A sigma type is a qualified type
	--
	-- Note that even if 'tyvars' is empty, theta
	-- may not be: e.g.   (?x::Int) => Int

	-- Note that 'sigma' is in prenex form:
	-- all the foralls are at the front.
	-- A 'phi' type has no foralls to the right of
	-- an arrow

190
191
192
phi :: theta => rho

rho ::= sigma -> rho
193
194
195
196
197
198
199
200
201
202
203
204
     |  tau

-- A 'tau' type has no quantification anywhere
-- Note that the args of a type constructor must be taus
tau ::= tyvar
     |  tycon tau_1 .. tau_n
     |  tau_1 tau_2
     |  tau_1 -> tau_2

-- In all cases, a (saturated) type synonym application is legal,
-- provided it expands to the required form.

205
\begin{code}
206
207
type TcTyVar = TyVar  	-- Used only during type inference
type TcType = Type 	-- A TcType can have mutable type variables
208
209
210
211
212
	-- Invariant on ForAllTy in TcTypes:
	-- 	forall a. T
	-- a cannot occur inside a MutTyVar in T; that is,
	-- T is "flattened" before quantifying over a

213
-- These types do not have boxy type variables in them
214
215
type TcPredType     = PredType
type TcThetaType    = ThetaType
216
type TcSigmaType    = TcType
217
type TcRhoType      = TcType
218
type TcTauType      = TcType
219
type TcKind         = Kind
220
type TcTyVarSet     = TyVarSet
221

222
223
224
225
226
227
-- These types may have boxy type variables in them
type BoxyTyVar	    = TcTyVar
type BoxyRhoType    = TcType	
type BoxyThetaType  = TcThetaType	
type BoxySigmaType  = TcType		
type BoxyType       = TcType		
228
229
230
231
232
233
\end{code}


%************************************************************************
%*									*
\subsection{TyVarDetails}
234
235
236
%*									*
%************************************************************************

237
238
TyVarDetails gives extra info about type variables, used during type
checking.  It's attached to mutable type variables only.
239
240
It's knot-tied back to Var.lhs.  There is no reason in principle
why Var.lhs shouldn't actually have the definition, but it "belongs" here.
241

242

243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
Note [Signature skolems]
~~~~~~~~~~~~~~~~~~~~~~~~
Consider this

  x :: [a]
  y :: b
  (x,y,z) = ([y,z], z, head x)

Here, x and y have type sigs, which go into the environment.  We used to
instantiate their types with skolem constants, and push those types into
the RHS, so we'd typecheck the RHS with type
	( [a*], b*, c )
where a*, b* are skolem constants, and c is an ordinary meta type varible.

The trouble is that the occurrences of z in the RHS force a* and b* to 
be the *same*, so we can't make them into skolem constants that don't unify
with each other.  Alas.

261
One solution would be insist that in the above defn the programmer uses
262
263
264
the same type variable in both type signatures.  But that takes explanation.

The alternative (currently implemented) is to have a special kind of skolem
265
266
267
268
constant, SigTv, which can unify with other SigTvs.  These are *not* treated
as righd for the purposes of GADTs.  And they are used *only* for pattern 
bindings and mutually recursive function bindings.  See the function
TcBinds.tcInstSig, and its use_skols parameter.
269
270


271
\begin{code}
272
273
-- A TyVarDetails is inside a TyVar
data TcTyVarDetails
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
  = SkolemTv SkolemInfo			-- A skolem constant

  | MetaTv BoxInfo (IORef MetaDetails)

data BoxInfo 
   = BoxTv	-- The contents is a (non-boxy) sigma-type
		-- That is, this MetaTv is a "box"

   | TauTv	-- The contents is a (non-boxy) tau-type
		-- That is, this MetaTv is an ordinary unification variable

   | SigTv SkolemInfo	-- A variant of TauTv, except that it should not be
			-- unified with a type, only with a type variable
			-- SigTvs are only distinguished to improve error messages
			--      see Note [Signature skolems]        
			--      The MetaDetails, if filled in, will 
			--      always be another SigTv or a SkolemTv

-- INVARIANTS:
--  	A TauTv is always filled in with a tau-type, which
--	never contains any BoxTvs, nor any ForAlls 
--
--	However, a BoxTv can contain a type that contains further BoxTvs
--	Notably, when typechecking an explicit list, say [e1,e2], with
--	expected type being a box b1, we fill in b1 with (List b2), where
--	b2 is another (currently empty) box.

data MetaDetails
302
303
  = Flexi	        -- Flexi type variables unify to become 
                   	-- Indirects.  
304

305
306
307
  | Indirect TcType  	-- INVARIANT:
		     	--   For a BoxTv, this type must be non-boxy
                     	--   For a TauTv, this type must be a tau-type
308

309
310
-- Generally speaking, SkolemInfo should not contain location info
-- that is contained in the Name of the tyvar with this SkolemInfo
311
data SkolemInfo
312
313
314
315
316
  = SigSkol UserTypeCtxt	-- A skolem that is created by instantiating
				-- a programmer-supplied type signature
				-- Location of the binding site is on the TyVar

	-- The rest are for non-scoped skolems
317
  | ClsSkol Class	-- Bound at a class decl
318
319
  | InstSkol 		-- Bound at an instance decl
  | FamInstSkol 	-- Bound at a family instance decl
320
  | PatSkol DataCon	-- An existential type variable bound by a pattern for
321
	    		-- a data constructor with an existential type. E.g.
322
323
324
325
			--	data T = forall a. Eq a => MkT a
			-- 	f (MkT x) = ...
			-- The pattern MkT x will allocate an existential type
			-- variable for 'a'.  
326
  | ArrowSkol 		-- An arrow form (see TcArrows)
327

328
  | RuleSkol RuleName	-- The LHS of a RULE
329
330
  | GenSkol [TcTyVar]	-- Bound when doing a subsumption check for 
	    TcType	-- 	(forall tvs. ty)
331

332
333
334
  | RuntimeUnkSkol      -- a type variable used to represent an unknown
                        -- runtime type (used in the GHCi debugger)

335
336
337
338
339
  | UnkSkol		-- Unhelpful info (until I improve it)

-------------------------------------
-- UserTypeCtxt describes the places where a 
-- programmer-written type signature can occur
340
-- Like SkolemInfo, no location info
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
data UserTypeCtxt 
  = FunSigCtxt Name	-- Function type signature
			-- Also used for types in SPECIALISE pragmas
  | ExprSigCtxt		-- Expression type signature
  | ConArgCtxt Name	-- Data constructor argument
  | TySynCtxt Name	-- RHS of a type synonym decl
  | GenPatCtxt		-- Pattern in generic decl
			-- 	f{| a+b |} (Inl x) = ...
  | LamPatSigCtxt		-- Type sig in lambda pattern
			-- 	f (x::t) = ...
  | BindPatSigCtxt	-- Type sig in pattern binding pattern
			--	(x::t, y) = e
  | ResSigCtxt		-- Result type sig
			-- 	f x :: t = ....
  | ForSigCtxt Name	-- Foreign inport or export signature
  | DefaultDeclCtxt	-- Types in a default declaration
  | SpecInstCtxt	-- SPECIALISE instance pragma
358
  | ThBrackCtxt		-- Template Haskell type brackets [t| ... |]
359
360
361
362
363
364
365
366
367
368

-- Notes re TySynCtxt
-- We allow type synonyms that aren't types; e.g.  type List = []
--
-- If the RHS mentions tyvars that aren't in scope, we'll 
-- quantify over them:
--	e.g. 	type T = a->a
-- will become	type T = forall a. a->a
--
-- With gla-exts that's right, but for H98 we should complain. 
369
370
371
372
373
374
375
376
377

---------------------------------
-- Kind variables:

mkKindName :: Unique -> Name
mkKindName unique = mkSystemName unique kind_var_occ

kindVarRef :: KindVar -> IORef MetaDetails
kindVarRef tc = 
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
378
  ASSERT ( isTcTyVar tc )
379
380
  case tcTyVarDetails tc of
    MetaTv TauTv ref -> ref
Ian Lynagh's avatar
Ian Lynagh committed
381
    _                -> pprPanic "kindVarRef" (ppr tc)
382
383
384
385
386
387
388
389
390
391
392
393
394

mkKindVar :: Unique -> IORef MetaDetails -> KindVar
mkKindVar u r 
  = mkTcTyVar (mkKindName u)
              tySuperKind  -- not sure this is right,
                            -- do we need kind vars for
                            -- coercions?
              (MetaTv TauTv r)

kind_var_occ :: OccName	-- Just one for all KindVars
			-- They may be jiggled by tidying
kind_var_occ = mkOccName tvName "k"
\end{code}
395

396
397
398
399
400
%************************************************************************
%*									*
		Pretty-printing
%*									*
%************************************************************************
401

402
403
404
\begin{code}
pprTcTyVarDetails :: TcTyVarDetails -> SDoc
-- For debugging
Ian Lynagh's avatar
Ian Lynagh committed
405
406
407
408
pprTcTyVarDetails (SkolemTv _)         = ptext (sLit "sk")
pprTcTyVarDetails (MetaTv BoxTv _)     = ptext (sLit "box")
pprTcTyVarDetails (MetaTv TauTv _)     = ptext (sLit "tau")
pprTcTyVarDetails (MetaTv (SigTv _) _) = ptext (sLit "sig")
409
410

pprUserTypeCtxt :: UserTypeCtxt -> SDoc
Ian Lynagh's avatar
Ian Lynagh committed
411
412
413
414
415
pprUserTypeCtxt (FunSigCtxt n)  = ptext (sLit "the type signature for") <+> quotes (ppr n)
pprUserTypeCtxt ExprSigCtxt     = ptext (sLit "an expression type signature")
pprUserTypeCtxt (ConArgCtxt c)  = ptext (sLit "the type of the constructor") <+> quotes (ppr c)
pprUserTypeCtxt (TySynCtxt c)   = ptext (sLit "the RHS of the type synonym") <+> quotes (ppr c)
pprUserTypeCtxt GenPatCtxt      = ptext (sLit "the type pattern of a generic definition")
416
pprUserTypeCtxt ThBrackCtxt     = ptext (sLit "a Template Haskell quotation [t|...|]")
Ian Lynagh's avatar
Ian Lynagh committed
417
418
419
420
421
422
pprUserTypeCtxt LamPatSigCtxt   = ptext (sLit "a pattern type signature")
pprUserTypeCtxt BindPatSigCtxt  = ptext (sLit "a pattern type signature")
pprUserTypeCtxt ResSigCtxt      = ptext (sLit "a result type signature")
pprUserTypeCtxt (ForSigCtxt n)  = ptext (sLit "the foreign declaration for") <+> quotes (ppr n)
pprUserTypeCtxt DefaultDeclCtxt = ptext (sLit "a type in a `default' declaration")
pprUserTypeCtxt SpecInstCtxt    = ptext (sLit "a SPECIALISE instance pragma")
423
424
425


--------------------------------
426
427
428
tidySkolemTyVar :: TidyEnv -> TcTyVar -> (TidyEnv, TcTyVar)
-- Tidy the type inside a GenSkol, preparatory to printing it
tidySkolemTyVar env tv
429
  = ASSERT( isTcTyVar tv && (isSkolemTyVar tv || isSigTyVar tv ) )
430
    (env1, mkTcTyVar (tyVarName tv) (tyVarKind tv) info1)
431
  where
432
    (env1, info1) = case tcTyVarDetails tv of
433
434
435
436
437
438
439
440
			SkolemTv info -> (env1, SkolemTv info')
				where
				  (env1, info') = tidy_skol_info env info
			MetaTv (SigTv info) box -> (env1, MetaTv (SigTv info') box)
				where
				  (env1, info') = tidy_skol_info env info
			info -> (env, info)

441
    tidy_skol_info env (GenSkol tvs ty) = (env2, GenSkol tvs1 ty1)
442
443
444
			    where
			      (env1, tvs1) = tidyOpenTyVars env tvs
			      (env2, ty1)  = tidyOpenType env1 ty
445
    tidy_skol_info env info = (env, info)
446
		     
447
448
449
450
pprSkolTvBinding :: TcTyVar -> SDoc
-- Print info about the binding of a skolem tyvar, 
-- or nothing if we don't have anything useful to say
pprSkolTvBinding tv
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
451
  = ASSERT ( isTcTyVar tv )
452
    quotes (ppr tv) <+> ppr_details (tcTyVarDetails tv)
453
  where
Ian Lynagh's avatar
Ian Lynagh committed
454
455
    ppr_details (MetaTv TauTv _)   	= ptext (sLit "is a meta type variable")
    ppr_details (MetaTv BoxTv _)   	= ptext (sLit "is a boxy type variable")
456
457
458
    ppr_details (MetaTv (SigTv info) _) = ppr_skol info
    ppr_details (SkolemTv info)		= ppr_skol info

Ian Lynagh's avatar
Ian Lynagh committed
459
460
461
    ppr_skol UnkSkol	    = ptext (sLit "is an unknown type variable")	-- Unhelpful
    ppr_skol RuntimeUnkSkol = ptext (sLit "is an unknown runtime type")
    ppr_skol info           = sep [ptext (sLit "is a rigid type variable bound by"),
462
				   sep [pprSkolInfo info, 
Ian Lynagh's avatar
Ian Lynagh committed
463
					 nest 2 (ptext (sLit "at") <+> ppr (getSrcLoc tv))]]
464
465
 
pprSkolInfo :: SkolemInfo -> SDoc
466
pprSkolInfo (SigSkol ctxt)   = pprUserTypeCtxt ctxt
Ian Lynagh's avatar
Ian Lynagh committed
467
468
469
470
471
472
473
pprSkolInfo (ClsSkol cls)    = ptext (sLit "the class declaration for") <+> quotes (ppr cls)
pprSkolInfo InstSkol         = ptext (sLit "the instance declaration")
pprSkolInfo FamInstSkol      = ptext (sLit "the family instance declaration")
pprSkolInfo (RuleSkol name)  = ptext (sLit "the RULE") <+> doubleQuotes (ftext name)
pprSkolInfo ArrowSkol        = ptext (sLit "the arrow form")
pprSkolInfo (PatSkol dc)     = sep [ptext (sLit "the constructor") <+> quotes (ppr dc)]
pprSkolInfo (GenSkol tvs ty) = sep [ptext (sLit "the polymorphic type"), 
474
475
476
				    nest 2 (quotes (ppr (mkForAllTys tvs ty)))]

-- UnkSkol
477
478
479
-- For type variables the others are dealt with by pprSkolTvBinding.  
-- For Insts, these cases should not happen
pprSkolInfo UnkSkol = panic "UnkSkol"
480
pprSkolInfo RuntimeUnkSkol = panic "RuntimeUnkSkol"
481
482

instance Outputable MetaDetails where
Ian Lynagh's avatar
Ian Lynagh committed
483
484
  ppr Flexi         = ptext (sLit "Flexi")
  ppr (Indirect ty) = ptext (sLit "Indirect") <+> ppr ty
485
486
\end{code}

487

488
489
490
491
492
493
494
%************************************************************************
%*									*
		Predicates
%*									*
%************************************************************************

\begin{code}
495
496
isImmutableTyVar :: TyVar -> Bool

497
498
499
500
isImmutableTyVar tv
  | isTcTyVar tv = isSkolemTyVar tv
  | otherwise    = True

501
502
503
504
isTyConableTyVar, isSkolemTyVar, isExistentialTyVar, 
  isBoxyTyVar, isMetaTyVar :: TcTyVar -> Bool 

isTyConableTyVar tv	
505
	-- True of a meta-type variable that can be filled in 
506
507
508
509
510
511
512
513
514
	-- with a type constructor application; in particular,
	-- not a SigTv
  = ASSERT( isTcTyVar tv) 
    case tcTyVarDetails tv of
	MetaTv BoxTv      _ -> True
	MetaTv TauTv      _ -> True
	MetaTv (SigTv {}) _ -> False
	SkolemTv {}	    -> False
	
515
isSkolemTyVar tv 
516
  = ASSERT2( isTcTyVar tv, ppr tv )
517
    case tcTyVarDetails tv of
518
519
	SkolemTv _         -> True
 	MetaTv _ _         -> False
520

521
522
523
isExistentialTyVar tv 	-- Existential type variable, bound by a pattern
  = ASSERT( isTcTyVar tv )
    case tcTyVarDetails tv of
524
	SkolemTv (PatSkol {}) -> True
Ian Lynagh's avatar
Ian Lynagh committed
525
	_                     -> False
526

527
isMetaTyVar tv 
528
  = ASSERT2( isTcTyVar tv, ppr tv )
529
    case tcTyVarDetails tv of
530
	MetaTv _ _ -> True
Ian Lynagh's avatar
Ian Lynagh committed
531
	_          -> False
532

533
534
535
536
isBoxyTyVar tv 
  = ASSERT( isTcTyVar tv )
    case tcTyVarDetails tv of
	MetaTv BoxTv _ -> True
Ian Lynagh's avatar
Ian Lynagh committed
537
	_              -> False
538

Ian Lynagh's avatar
Ian Lynagh committed
539
isSigTyVar :: Var -> Bool
540
541
542
543
isSigTyVar tv 
  = ASSERT( isTcTyVar tv )
    case tcTyVarDetails tv of
	MetaTv (SigTv _) _ -> True
Ian Lynagh's avatar
Ian Lynagh committed
544
	_                  -> False
545

546
547
metaTvRef :: TyVar -> IORef MetaDetails
metaTvRef tv 
548
  = ASSERT2( isTcTyVar tv, ppr tv )
549
    case tcTyVarDetails tv of
550
	MetaTv _ ref -> ref
Ian Lynagh's avatar
Ian Lynagh committed
551
	_          -> pprPanic "metaTvRef" (ppr tv)
552
553

isFlexi, isIndirect :: MetaDetails -> Bool
Ian Lynagh's avatar
Ian Lynagh committed
554
555
isFlexi Flexi = True
isFlexi _     = False
556
557

isIndirect (Indirect _) = True
Ian Lynagh's avatar
Ian Lynagh committed
558
isIndirect _            = False
559
560
561
562
563
564
565
566
567
568

isRuntimeUnk :: TyVar -> Bool
isRuntimeUnk x | isTcTyVar x
               , SkolemTv RuntimeUnkSkol <- tcTyVarDetails x = True
               | otherwise = False

isUnk :: TyVar -> Bool
isUnk x | isTcTyVar x
        , SkolemTv UnkSkol <- tcTyVarDetails x = True
        | otherwise = False
569
\end{code}
570

571
572
573
574
575
576
577
578

%************************************************************************
%*									*
\subsection{Tau, sigma and rho}
%*									*
%************************************************************************

\begin{code}
579
mkSigmaTy :: [TyVar] -> [PredType] -> Type -> Type
580
mkSigmaTy tyvars theta tau = mkForAllTys tyvars (mkPhiTy theta tau)
sof's avatar
sof committed
581

582
mkPhiTy :: [PredType] -> Type -> Type
583
mkPhiTy theta ty = foldr (\p r -> mkFunTy (mkPredTy p) r) ty theta
584
585
\end{code}

586
@isTauTy@ tests for nested for-alls.  It should not be called on a boxy type.
sof's avatar
sof committed
587

588
\begin{code}
589
isTauTy :: Type -> Bool
590
isTauTy ty | Just ty' <- tcView ty = isTauTy ty'
591
592
593
594
595
isTauTy (TyVarTy tv)	 = ASSERT( not (isTcTyVar tv && isBoxyTyVar tv) )
			   True
isTauTy (TyConApp tc tys) = all isTauTy tys && isTauTyCon tc
isTauTy (AppTy a b)	  = isTauTy a && isTauTy b
isTauTy (FunTy a b)	  = isTauTy a && isTauTy b
Ian Lynagh's avatar
Ian Lynagh committed
596
597
isTauTy (PredTy _)	  = True		-- Don't look through source types
isTauTy _    		  = False
598
599
600
601


isTauTyCon :: TyCon -> Bool
-- Returns False for type synonyms whose expansion is a polytype
602
isTauTyCon tc 
603
604
  | isClosedSynTyCon tc = isTauTy (snd (synTyConDefn tc))
  | otherwise           = True
605
606
607
608
609
610
611

---------------
isBoxyTy :: TcType -> Bool
isBoxyTy ty = any isBoxyTyVar (varSetElems (tcTyVarsOfType ty))

isRigidTy :: TcType -> Bool
-- A type is rigid if it has no meta type variables in it
612
isRigidTy ty = all isImmutableTyVar (varSetElems (tcTyVarsOfType ty))
613

614
isRefineableTy :: TcType -> (Bool,Bool)
615
616
-- A type should have type refinements applied to it if it has
-- free type variables, and they are all rigid
617
isRefineableTy ty = (null tc_tvs,  all isImmutableTyVar tc_tvs)
618
619
620
		    where
		      tc_tvs = varSetElems (tcTyVarsOfType ty)

621
622
623
624
625
isRefineablePred :: TcPredType -> Bool
isRefineablePred pred = not (null tc_tvs) && all isImmutableTyVar tc_tvs
		      where
		        tc_tvs = varSetElems (tcTyVarsOfPred pred)

626
---------------
627
628
getDFunTyKey :: Type -> OccName	-- Get some string from a type, to be used to 
				-- construct a dictionary function name
629
getDFunTyKey ty | Just ty' <- tcView ty = getDFunTyKey ty'
630
631
632
getDFunTyKey (TyVarTy tv)    = getOccName tv
getDFunTyKey (TyConApp tc _) = getOccName tc
getDFunTyKey (AppTy fun _)   = getDFunTyKey fun
Ian Lynagh's avatar
Ian Lynagh committed
633
getDFunTyKey (FunTy _ _)     = getOccName funTyCon
634
635
636
getDFunTyKey (ForAllTy _ t)  = getDFunTyKey t
getDFunTyKey ty		     = pprPanic "getDFunTyKey" (pprType ty)
-- PredTy shouldn't happen
sof's avatar
sof committed
637
638
639
\end{code}


640
641
%************************************************************************
%*									*
642
\subsection{Expanding and splitting}
643
644
%*									*
%************************************************************************
645

646
647
648
649
650
651
652
653
These tcSplit functions are like their non-Tc analogues, but
	a) they do not look through newtypes
	b) they do not look through PredTys
	c) [future] they ignore usage-type annotations

However, they are non-monadic and do not follow through mutable type
variables.  It's up to you to make sure this doesn't matter.

654
\begin{code}
655
656
657
tcSplitForAllTys :: Type -> ([TyVar], Type)
tcSplitForAllTys ty = split ty ty []
   where
658
     split orig_ty ty tvs | Just ty' <- tcView ty = split orig_ty ty' tvs
Ian Lynagh's avatar
Ian Lynagh committed
659
     split _ (ForAllTy tv ty) tvs 
660
       | not (isCoVar tv) = split ty ty (tv:tvs)
Ian Lynagh's avatar
Ian Lynagh committed
661
     split orig_ty _ tvs = (reverse tvs, orig_ty)
662

Ian Lynagh's avatar
Ian Lynagh committed
663
tcIsForAllTy :: Type -> Bool
664
tcIsForAllTy ty | Just ty' <- tcView ty = tcIsForAllTy ty'
Ian Lynagh's avatar
Ian Lynagh committed
665
666
tcIsForAllTy (ForAllTy tv _) = not (isCoVar tv)
tcIsForAllTy _               = False
667

668
669
670
671
672
673
674
675
676
677
tcSplitPredFunTy_maybe :: Type -> Maybe (PredType, Type)
-- Split off the first predicate argument from a type
tcSplitPredFunTy_maybe ty | Just ty' <- tcView ty = tcSplitPredFunTy_maybe ty'
tcSplitPredFunTy_maybe (ForAllTy tv ty)
  | isCoVar tv = Just (coVarPred tv, ty)
tcSplitPredFunTy_maybe (FunTy arg res)
  | Just p <- tcSplitPredTy_maybe arg = Just (p, res)
tcSplitPredFunTy_maybe _
  = Nothing

678
tcSplitPhiTy :: Type -> (ThetaType, Type)
679
680
681
682
683
684
685
tcSplitPhiTy ty
  = split ty []
  where
    split ty ts 
      = case tcSplitPredFunTy_maybe ty of
	  Just (pred, ty) -> split ty (pred:ts)
	  Nothing         -> (reverse ts, ty)
686

687
tcSplitSigmaTy :: Type -> ([TyVar], ThetaType, Type)
688
tcSplitSigmaTy ty = case tcSplitForAllTys ty of
689
			(tvs, rho) -> case tcSplitPhiTy rho of
690
691
					(theta, tau) -> (tvs, theta, tau)

692
693
694
695
696
697
698
699
700
701
702
703
704
705
-----------------------
tcMultiSplitSigmaTy
	:: TcSigmaType
	-> ( [([TyVar], ThetaType)],	-- forall as.C => forall bs.D
	     TcSigmaType)		-- The rest of the type

-- We need a loop here because we are now prepared to entertain
-- types like
-- 	f:: forall a. Eq a => forall b. Baz b => tau
-- We want to instantiate this to
-- 	f2::tau		{f2 = f1 b (Baz b), f1 = f a (Eq a)}

tcMultiSplitSigmaTy sigma
  = case (tcSplitSigmaTy sigma) of
Ian Lynagh's avatar
Ian Lynagh committed
706
	([], [], _) -> ([], sigma)
707
708
709
710
	(tvs, theta, ty) -> case tcMultiSplitSigmaTy ty of
				(pairs, rest) -> ((tvs,theta):pairs, rest)

-----------------------
711
tcTyConAppTyCon :: Type -> TyCon
712
713
714
tcTyConAppTyCon ty = case tcSplitTyConApp_maybe ty of
			Just (tc, _) -> tc
			Nothing	     -> pprPanic "tcTyConAppTyCon" (pprType ty)
715
716

tcTyConAppArgs :: Type -> [Type]
717
718
719
tcTyConAppArgs ty = case tcSplitTyConApp_maybe ty of
			Just (_, args) -> args
			Nothing	       -> pprPanic "tcTyConAppArgs" (pprType ty)
720
721
722
723
724
725
726

tcSplitTyConApp :: Type -> (TyCon, [Type])
tcSplitTyConApp ty = case tcSplitTyConApp_maybe ty of
			Just stuff -> stuff
			Nothing	   -> pprPanic "tcSplitTyConApp" (pprType ty)

tcSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
727
tcSplitTyConApp_maybe ty | Just ty' <- tcView ty = tcSplitTyConApp_maybe ty'
728
729
tcSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
tcSplitTyConApp_maybe (FunTy arg res)   = Just (funTyCon, [arg,res])
730
	-- Newtypes are opaque, so they may be split
731
732
	-- However, predicates are not treated
	-- as tycon applications by the type checker
Ian Lynagh's avatar
Ian Lynagh committed
733
tcSplitTyConApp_maybe _                 = Nothing
734

735
-----------------------
736
737
738
739
740
741
742
743
tcSplitFunTys :: Type -> ([Type], Type)
tcSplitFunTys ty = case tcSplitFunTy_maybe ty of
			Nothing	       -> ([], ty)
			Just (arg,res) -> (arg:args, res')
				       where
					  (args,res') = tcSplitFunTys res

tcSplitFunTy_maybe :: Type -> Maybe (Type, Type)
744
745
tcSplitFunTy_maybe ty | Just ty' <- tcView ty           = tcSplitFunTy_maybe ty'
tcSplitFunTy_maybe (FunTy arg res) | not (isPredTy arg) = Just (arg, res)
Ian Lynagh's avatar
Ian Lynagh committed
746
tcSplitFunTy_maybe _                                    = Nothing
747
748
749
750
751
752
753
	-- Note the (not (isPredTy arg)) guard
	-- Consider	(?x::Int) => Bool
	-- We don't want to treat this as a function type!
	-- A concrete example is test tc230:
	--	f :: () -> (?p :: ()) => () -> ()
	--
	--	g = f () ()
754

755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
tcSplitFunTysN
	:: TcRhoType 
	-> Arity		-- N: Number of desired args
	-> ([TcSigmaType], 	-- Arg types (N or fewer)
	    TcSigmaType)	-- The rest of the type

tcSplitFunTysN ty n_args
  | n_args == 0
  = ([], ty)
  | Just (arg,res) <- tcSplitFunTy_maybe ty
  = case tcSplitFunTysN res (n_args - 1) of
	(args, res) -> (arg:args, res)
  | otherwise
  = ([], ty)

Ian Lynagh's avatar
Ian Lynagh committed
770
tcSplitFunTy :: Type -> (Type, Type)
771
tcSplitFunTy  ty = expectJust "tcSplitFunTy" (tcSplitFunTy_maybe ty)
Ian Lynagh's avatar
Ian Lynagh committed
772
773

tcFunArgTy :: Type -> Type
774
tcFunArgTy    ty = fst (tcSplitFunTy ty)
Ian Lynagh's avatar
Ian Lynagh committed
775
776

tcFunResultTy :: Type -> Type
777
tcFunResultTy ty = snd (tcSplitFunTy ty)
778

779
-----------------------
780
tcSplitAppTy_maybe :: Type -> Maybe (Type, Type)
781
tcSplitAppTy_maybe ty | Just ty' <- tcView ty = tcSplitAppTy_maybe ty'
782
tcSplitAppTy_maybe ty = repSplitAppTy_maybe ty
783

784
tcSplitAppTy :: Type -> (Type, Type)
785
786
787
788
tcSplitAppTy ty = case tcSplitAppTy_maybe ty of
		    Just stuff -> stuff
		    Nothing    -> pprPanic "tcSplitAppTy" (pprType ty)

789
790
791
792
793
794
795
796
tcSplitAppTys :: Type -> (Type, [Type])
tcSplitAppTys ty
  = go ty []
  where
    go ty args = case tcSplitAppTy_maybe ty of
		   Just (ty', arg) -> go ty' (arg:args)
		   Nothing	   -> (ty,args)

797
-----------------------
798
tcGetTyVar_maybe :: Type -> Maybe TyVar
799
tcGetTyVar_maybe ty | Just ty' <- tcView ty = tcGetTyVar_maybe ty'
Ian Lynagh's avatar
Ian Lynagh committed
800
801
tcGetTyVar_maybe (TyVarTy tv)   = Just tv
tcGetTyVar_maybe _              = Nothing
802
803
804
805
806
807
808

tcGetTyVar :: String -> Type -> TyVar
tcGetTyVar msg ty = expectJust msg (tcGetTyVar_maybe ty)

tcIsTyVarTy :: Type -> Bool
tcIsTyVarTy ty = maybeToBool (tcGetTyVar_maybe ty)

809
-----------------------
810
tcSplitDFunTy :: Type -> ([TyVar], [PredType], Class, [Type])
811
812
-- Split the type of a dictionary function
tcSplitDFunTy ty 
813
814
  = case tcSplitSigmaTy ty   of { (tvs, theta, tau) ->
    case tcSplitDFunHead tau of { (clas, tys) -> 
815
    (tvs, theta, clas, tys) }}
816
817
818
819
820

tcSplitDFunHead :: Type -> (Class, [Type])
tcSplitDFunHead tau  
  = case tcSplitPredTy_maybe tau of 
	Just (ClassP clas tys) -> (clas, tys)
Ian Lynagh's avatar
Ian Lynagh committed
821
	_ -> panic "tcSplitDFunHead"
822

823
tcInstHeadTyNotSynonym :: Type -> Bool
824
825
826
-- Used in Haskell-98 mode, for the argument types of an instance head
-- These must not be type synonyms, but everywhere else type synonyms
-- are transparent, so we need a special function here
827
tcInstHeadTyNotSynonym ty
828
  = case ty of
Ian Lynagh's avatar
Ian Lynagh committed
829
        TyConApp tc _ -> not (isSynTyCon tc)
Ian Lynagh's avatar
Ian Lynagh committed
830
        _ -> True
831
832
833
834
835
836
837

tcInstHeadTyAppAllTyVars :: Type -> Bool
-- Used in Haskell-98 mode, for the argument types of an instance head
-- These must be a constructor applied to type variable arguments
tcInstHeadTyAppAllTyVars ty
  = case ty of
	TyConApp _ tys  -> ok tys
838
	FunTy arg res   -> ok [arg, res]
Ian Lynagh's avatar
Ian Lynagh committed
839
	_               -> False
840
841
842
843
844
845
846
  where
	-- Check that all the types are type variables,
	-- and that each is distinct
    ok tys = equalLength tvs tys && hasNoDups tvs
	   where
	     tvs = mapCatMaybes get_tv tys

simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
847
    get_tv (TyVarTy tv)  = Just tv	-- through synonyms
Ian Lynagh's avatar
Ian Lynagh committed
848
    get_tv _             = Nothing
849
850
\end{code}

851

852
853
854

%************************************************************************
%*									*
855
\subsection{Predicate types}
856
857
%*									*
%************************************************************************
858

859
\begin{code}
860
861
tcSplitPredTy_maybe :: Type -> Maybe PredType
   -- Returns Just for predicates only
862
tcSplitPredTy_maybe ty | Just ty' <- tcView ty = tcSplitPredTy_maybe ty'
863
tcSplitPredTy_maybe (PredTy p)    = Just p
Ian Lynagh's avatar
Ian Lynagh committed
864
865
tcSplitPredTy_maybe _             = Nothing

866
predTyUnique :: PredType -> Unique
Ian Lynagh's avatar
Ian Lynagh committed
867
868
869
predTyUnique (IParam n _)    = getUnique (ipNameName n)
predTyUnique (ClassP clas _) = getUnique clas
predTyUnique (EqPred a b)    = pprPanic "predTyUnique" (ppr (EqPred a b))
870
871
\end{code}

872
873

--------------------- Dictionary types ---------------------------------
874
875

\begin{code}
Ian Lynagh's avatar
Ian Lynagh committed
876
mkClassPred :: Class -> [Type] -> PredType
877
mkClassPred clas tys = ClassP clas tys
878

879
isClassPred :: PredType -> Bool
Ian Lynagh's avatar
Ian Lynagh committed
880
881
isClassPred (ClassP _ _) = True
isClassPred _            = False
882

Ian Lynagh's avatar
Ian Lynagh committed
883
884
885
isTyVarClassPred :: PredType -> Bool
isTyVarClassPred (ClassP _ tys) = all tcIsTyVarTy tys
isTyVarClassPred _              = False
886

887
getClassPredTys_maybe :: PredType -> Maybe (Class, [Type])
888
getClassPredTys_maybe (ClassP clas tys) = Just (clas, tys)
Ian Lynagh's avatar
Ian Lynagh committed
889
getClassPredTys_maybe _                 = Nothing
890
891
892

getClassPredTys :: PredType -> (Class, [Type])
getClassPredTys (ClassP clas tys) = (clas, tys)
Ian Lynagh's avatar
Ian Lynagh committed
893
getClassPredTys _ = panic "getClassPredTys"
894
895

mkDictTy :: Class -> [Type] -> Type
896
mkDictTy clas tys = mkPredTy (ClassP clas tys)
897
898

isDictTy :: Type -> Bool
899
isDictTy ty | Just ty' <- tcView ty = isDictTy ty'
900
isDictTy (PredTy p) = isClassPred p
Ian Lynagh's avatar
Ian Lynagh committed
901
isDictTy _          = False
902
903
904
905
906
907
908
909

isDictLikeTy :: Type -> Bool
-- Note [Dictionary-like types]
isDictLikeTy ty | Just ty' <- tcView ty = isDictTy ty'
isDictLikeTy (PredTy p) = isClassPred p
isDictLikeTy (TyConApp tc tys) 
  | isTupleTyCon tc     = all isDictLikeTy tys
isDictLikeTy _          = False
910
\end{code}
911

912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
Note [Dictionary-like types]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Being "dictionary-like" means either a dictionary type or a tuple thereof.
In GHC 6.10 we build implication constraints which construct such tuples,
and if we land up with a binding
    t :: (C [a], Eq [a])
    t = blah
then we want to treat t as cheap under "-fdicts-cheap" for example.
(Implication constraints are normally inlined, but sadly not if the
occurrence is itself inside an INLINE function!  Until we revise the 
handling of implication constraints, that is.)  This turned out to
be important in getting good arities in DPH code.  Example:

    class C a
    class D a where { foo :: a -> a }
    instance C a => D (Maybe a) where { foo x = x }

    bar :: (C a, C b) => a -> b -> (Maybe a, Maybe b)
    {-# INLINE bar #-}
    bar x y = (foo (Just x), foo (Just y))

Then 'bar' should jolly well have arity 4 (two dicts, two args), but
we ended up with something like
   bar = __inline_me__ (\d1,d2. let t :: (D (Maybe a), D (Maybe b)) = ...
                                in \x,y. <blah>)

This is all a bit ad-hoc; eg it relies on knowing that implication
constraints build tuples.

941
942
943
--------------------- Implicit parameters ---------------------------------

\begin{code}
944
isIPPred :: PredType -> Bool
945
isIPPred (IParam _ _) = True
Ian Lynagh's avatar
Ian Lynagh committed
946
isIPPred _            = False
947

948
isInheritablePred :: PredType -> Bool
949
950
951
952
953
954
955
956
-- Can be inherited by a context.  For example, consider
--	f x = let g y = (?v, y+x)
--	      in (g 3 with ?v = 8, 
--		  g 4 with ?v = 9)
-- The point is that g's type must be quantifed over ?v:
--	g :: (?v :: a) => a -> a
-- but it doesn't need to be quantified over the Num a dictionary
-- which can be free in g's rhs, and shared by both calls to g
957
isInheritablePred (ClassP _ _) = True
958
isInheritablePred (EqPred _ _) = True
Ian Lynagh's avatar
Ian Lynagh committed
959
isInheritablePred _            = False
960
\end{code}
961

962
963
964
965
966
967
968
--------------------- Equality predicates ---------------------------------
\begin{code}
substEqSpec :: TvSubst -> [(TyVar,Type)] -> [(TcType,TcType)]
substEqSpec subst eq_spec = [ (substTyVar subst tv, substTy subst ty)
			    | (tv,ty) <- eq_spec]
\end{code}

969

970
971
972
973
974
%************************************************************************
%*									*
\subsection{Predicates}
%*									*
%************************************************************************
975

976
isSigmaTy returns true of any qualified type.  It doesn't *necessarily* have 
977
978
any foralls.  E.g.
	f :: (?x::Int) => Int -> Int
979

980
\begin{code}
981
isSigmaTy :: Type -> Bool
982
isSigmaTy ty | Just ty' <- tcView ty = isSigmaTy ty'
Ian Lynagh's avatar
Ian Lynagh committed
983
984
985
isSigmaTy (ForAllTy _ _) = True
isSigmaTy (FunTy a _)    = isPredTy a
isSigmaTy _              = False
986
987

isOverloadedTy :: Type -> Bool
988
989
990
-- Yes for a type of a function that might require evidence-passing
-- Used only by bindInstsOfLocalFuns/Pats
-- NB: be sure to check for type with an equality predicate; hence isCoVar
991
isOverloadedTy ty | Just ty' <- tcView ty = isOverloadedTy ty'
992
993
994
isOverloadedTy (ForAllTy tv ty) = isCoVar tv || isOverloadedTy ty
isOverloadedTy (FunTy a _)      = isPredTy a
isOverloadedTy _                = False
995
996
997

isPredTy :: Type -> Bool	-- Belongs in TcType because it does 
				-- not look through newtypes, or predtypes (of course)
998
isPredTy ty | Just ty' <- tcView ty = isPredTy ty'
Ian Lynagh's avatar
Ian Lynagh committed
999
1000
isPredTy (PredTy _) = True
isPredTy _          = False
1001
\end{code}
1002
1003

\begin{code}
Ian Lynagh's avatar
Ian Lynagh committed
1004
1005
isFloatTy, isDoubleTy, isIntegerTy, isIntTy, isWordTy, isBoolTy,
    isUnitTy, isCharTy :: Type -> Bool
1006
1007
1008
1009
isFloatTy      = is_tc floatTyConKey
isDoubleTy     = is_tc doubleTyConKey
isIntegerTy    = is_tc integerTyConKey
isIntTy        = is_tc intTyConKey
Ian Lynagh's avatar
Ian Lynagh committed
1010
isWordTy       = is_tc wordTyConKey
1011
isBoolTy       = is_tc boolTyConKey
1012
isUnitTy       = is_tc unitTyConKey
1013
1014
isCharTy       = is_tc charTyConKey

Ian Lynagh's avatar
Ian Lynagh committed
1015
isStringTy :: Type -> Bool
1016
1017
1018
isStringTy ty
  = case tcSplitTyConApp_maybe ty of
      Just (tc, [arg_ty]) -> tc == listTyCon && isCharTy arg_ty
Ian Lynagh's avatar
Ian Lynagh committed
1019
      _                   -> False
1020
1021
1022
1023
1024
1025
1026

is_tc :: Unique -> Type -> Bool
-- Newtypes are opaque to this
is_tc uniq ty = case tcSplitTyConApp_maybe ty of
			Just (tc, _) -> uniq == getUnique tc
			Nothing	     -> False
\end{code}
1027

1028
1029
1030
1031
1032
\begin{code}
-- NB: Currently used in places where we have already expanded type synonyms;
--     hence no 'coreView'.  This could, however, be changed without breaking
--     any code.
isOpenSynTyConApp :: TcTauType -> Bool
1033
1034
1035
isOpenSynTyConApp (TyConApp tc tys) = isOpenSynTyCon tc && 
                                      length tys == tyConArity tc 
isOpenSynTyConApp _other            = False
1036
1037
\end{code}

1038

1039
1040
%************************************************************************
%*									*
1041
\subsection{Misc}
1042
1043
1044
1045
%*									*
%************************************************************************

\begin{code}
1046
1047
1048
1049
deNoteType :: Type -> Type
-- Remove all *outermost* type synonyms and other notes
deNoteType ty | Just ty' <- tcView ty = deNoteType ty'
deNoteType ty = ty
1050
1051
\end{code}

1052
1053
\begin{code}
tcTyVarsOfType :: Type -> TcTyVarSet
1054
1055
-- Just the *TcTyVars* free in the type
-- (Types.tyVarsOfTypes finds all free TyVars)
1056
1057
tcTyVarsOfType (TyVarTy tv)	    = if isTcTyVar tv then unitVarSet tv
						      else emptyVarSet
Ian Lynagh's avatar
Ian Lynagh committed
1058
tcTyVarsOfType (TyConApp _ tys)     = tcTyVarsOfTypes tys
1059
1060
1061
tcTyVarsOfType (PredTy sty)	    = tcTyVarsOfPred sty
tcTyVarsOfType (FunTy arg res)	    = tcTyVarsOfType arg `unionVarSet` tcTyVarsOfType res
tcTyVarsOfType (AppTy fun arg)	    = tcTyVarsOfType fun `unionVarSet` tcTyVarsOfType arg
1062
1063
tcTyVarsOfType (ForAllTy tyvar ty)  = (tcTyVarsOfType ty `delVarSet` tyvar)
                                      `unionVarSet` tcTyVarsOfTyVar tyvar
1064
1065
	-- We do sometimes quantify over skolem TcTyVars

1066
1067
1068
1069
tcTyVarsOfTyVar :: TcTyVar -> TyVarSet
tcTyVarsOfTyVar tv | isCoVar tv = tcTyVarsOfType (tyVarKind tv)
                   | otherwise  = emptyVarSet

1070
1071
1072
1073
tcTyVarsOfTypes :: [Type] -> TyVarSet
tcTyVarsOfTypes tys = foldr (unionVarSet.tcTyVarsOfType) emptyVarSet tys

tcTyVarsOfPred :: PredType -> TyVarSet
1074
1075
1076
tcTyVarsOfPred (IParam _ ty)  	= tcTyVarsOfType ty
tcTyVarsOfPred (ClassP _ tys) 	= tcTyVarsOfTypes tys
tcTyVarsOfPred (EqPred ty1 ty2) = tcTyVarsOfType ty1 `unionVarSet` tcTyVarsOfType ty2
1077
\end{code}
1078

1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
Note [Silly type synonym]
~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
	type T a = Int
What are the free tyvars of (T x)?  Empty, of course!  
Here's the example that Ralf Laemmel showed me:
	foo :: (forall a. C u a -> C u a) -> u
	mappend :: Monoid u => u -> u -> u

	bar :: Monoid u => u
	bar = foo (\t -> t `mappend` t)
We have to generalise at the arg to f, and we don't
want to capture the constraint (Monad (C u a)) because
it appears to mention a.  Pretty silly, but it was useful to him.

exactTyVarsOfType is used by the type checker to figure out exactly
which type variables are mentioned in a type.  It's also used in the
smart-app checking code --- see TcExpr.tcIdApp
1097

1098
1099
1100
1101
1102
1103
1104
1105
1106
On the other hand, consider a *top-level* definition
	f = (\x -> x) :: T a -> T a
If we don't abstract over 'a' it'll get fixed to GHC.Prim.Any, and then
if we have an application like (f "x") we get a confusing error message 
involving Any.  So the conclusion is this: when generalising
  - at top level use tyVarsOfType
  - in nested bindings use exactTyVarsOfType
See Trac #1813 for example.

1107
\begin{code}
1108
1109
exactTyVarsOfType :: TcType -> TyVarSet
-- Find the free type variables (of any kind)
1110
-- but *expand* type synonyms.  See Note [Silly type synonym] above.
1111
1112
1113
1114
1115
exactTyVarsOfType ty
  = go ty
  where
    go ty | Just ty' <- tcView ty = go ty'	-- This is the key line
    go (TyVarTy tv)         	  = unitVarSet tv
Ian Lynagh's avatar
Ian Lynagh committed
1116
    go (TyConApp _ tys)     	  = exactTyVarsOfTypes tys
1117
1118
1119
1120
    go (PredTy ty)	    	  = go_pred ty
    go (FunTy arg res)	    	  = go arg `unionVarSet` go res
    go (AppTy fun arg)	    	  = go fun `unionVarSet` go arg
    go (ForAllTy tyvar ty)  	  = delVarSet (go ty) tyvar
1121
                                    `unionVarSet` go_tv tyvar
1122

1123
1124
1125
    go_pred (IParam _ ty)    = go ty
    go_pred (ClassP _ tys)   = exactTyVarsOfTypes tys
    go_pred (EqPred ty1 ty2) = go ty1 `unionVarSet` go ty2
1126

1127
1128
1129
    go_tv tyvar | isCoVar tyvar = go (tyVarKind tyvar)
                | otherwise     = emptyVarSet

1130
1131
exactTyVarsOfTypes :: [TcType] -> TyVarSet
exactTyVarsOfTypes tys = foldr (unionVarSet . exactTyVarsOfType) emptyVarSet tys
1132
1133
\end{code}

1134
1135
Find the free tycons and classes of a type.  This is used in the front
end of the compiler.