Hurrah! This major commit adds support for scoped kind variables,
[ghc.git] / compiler / typecheck / TcType.lhs
1 %
2 % (c) The University of Glasgow 2006
3 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 %
5 \section[TcType]{Types used in the typechecker}
6
7 This module provides the Type interface for front-end parts of the 
8 compiler.  These parts 
9
10         * treat "source types" as opaque: 
11                 newtypes, and predicates are meaningful. 
12         * look through usage types
13
14 The "tc" prefix is for "TypeChecker", because the type checker
15 is the principal client.
16
17 \begin{code}
18 {-# OPTIONS -fno-warn-tabs #-}
19 -- The above warning supression flag is a temporary kludge.
20 -- While working on this module you are encouraged to remove it and
21 -- detab the module (please do the detabbing in a separate patch). See
22 --     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#TabsvsSpaces
23 -- for details
24
25 module TcType (
26   --------------------------------
27   -- Types 
28   TcType, TcSigmaType, TcRhoType, TcTauType, TcPredType, TcThetaType, 
29   TcTyVar, TcTyVarSet, TcKind, TcCoVar,
30
31   --------------------------------
32   -- MetaDetails
33   UserTypeCtxt(..), pprUserTypeCtxt,
34   TcTyVarDetails(..), pprTcTyVarDetails, vanillaSkolemTv, superSkolemTv,
35   MetaDetails(Flexi, Indirect), MetaInfo(..), 
36   isImmutableTyVar, isSkolemTyVar, isMetaTyVar,  isMetaTyVarTy, isTyVarTy,
37   isSigTyVar, isOverlappableTyVar,  isTyConableTyVar,
38   isAmbiguousTyVar, metaTvRef, 
39   isFlexi, isIndirect, isRuntimeUnkSkol,
40   isTypeVar, isKindVar,
41
42   --------------------------------
43   -- Builders
44   mkPhiTy, mkSigmaTy, mkTcEqPred,
45
46   --------------------------------
47   -- Splitters  
48   -- These are important because they do not look through newtypes
49   tcView,
50   tcSplitForAllTys, tcSplitPhiTy, tcSplitPredFunTy_maybe,
51   tcSplitFunTy_maybe, tcSplitFunTys, tcFunArgTy, tcFunResultTy, tcSplitFunTysN,
52   tcSplitTyConApp, tcSplitTyConApp_maybe, tcTyConAppTyCon, tcTyConAppArgs,
53   tcSplitAppTy_maybe, tcSplitAppTy, tcSplitAppTys, repSplitAppTy_maybe,
54   tcInstHeadTyNotSynonym, tcInstHeadTyAppAllTyVars,
55   tcGetTyVar_maybe, tcGetTyVar,
56   tcSplitSigmaTy, tcDeepSplitSigmaTy_maybe,  
57
58   ---------------------------------
59   -- Predicates. 
60   -- Again, newtypes are opaque
61   eqType, eqTypes, eqPred, cmpType, cmpTypes, cmpPred, eqTypeX,
62   pickyEqType, eqKind, 
63   isSigmaTy, isOverloadedTy,
64   isDoubleTy, isFloatTy, isIntTy, isWordTy, isStringTy,
65   isIntegerTy, isBoolTy, isUnitTy, isCharTy,
66   isTauTy, isTauTyCon, tcIsTyVarTy, tcIsForAllTy, 
67   isSynFamilyTyConApp,
68   isPredTy, isTyVarClassPred,
69   shallowPredTypePredTree,
70   
71   ---------------------------------
72   -- Misc type manipulators
73   deNoteType,
74   orphNamesOfType, orphNamesOfDFunHead, orphNamesOfCo,
75   getDFunTyKey,
76   evVarPred_maybe, evVarPred,
77
78   ---------------------------------
79   -- Predicate types  
80   mkMinimalBySCs, transSuperClasses, immSuperClasses,
81   
82   -- * Finding type instances
83   tcTyFamInsts,
84
85   -- * Finding "exact" (non-dead) type variables
86   exactTyVarsOfType, exactTyVarsOfTypes,
87
88   -- * Tidying type related things up for printing
89   tidyType,      tidyTypes,
90   tidyOpenType,  tidyOpenTypes,
91   tidyOpenKind,
92   tidyTyVarBndr, tidyTyVarBndrs, tidyFreeTyVars,
93   tidyOpenTyVar, tidyOpenTyVars,
94   tidyTyVarOcc,
95   tidyTopType,
96   tidyKind, 
97   tidyCo, tidyCos,
98
99   ---------------------------------
100   -- Foreign import and export
101   isFFIArgumentTy,     -- :: DynFlags -> Safety -> Type -> Bool
102   isFFIImportResultTy, -- :: DynFlags -> Type -> Bool
103   isFFIExportResultTy, -- :: Type -> Bool
104   isFFIExternalTy,     -- :: Type -> Bool
105   isFFIDynArgumentTy,  -- :: Type -> Bool
106   isFFIDynResultTy,    -- :: Type -> Bool
107   isFFIPrimArgumentTy, -- :: DynFlags -> Type -> Bool
108   isFFIPrimResultTy,   -- :: DynFlags -> Type -> Bool
109   isFFILabelTy,        -- :: Type -> Bool
110   isFFIDotnetTy,       -- :: DynFlags -> Type -> Bool
111   isFFIDotnetObjTy,    -- :: Type -> Bool
112   isFFITy,             -- :: Type -> Bool
113   isFunPtrTy,          -- :: Type -> Bool
114   tcSplitIOType_maybe, -- :: Type -> Maybe Type  
115
116   --------------------------------
117   -- Rexported from Kind
118   Kind, typeKind,
119   unliftedTypeKind, liftedTypeKind, argTypeKind,
120   openTypeKind, constraintKind, mkArrowKind, mkArrowKinds, 
121   isLiftedTypeKind, isUnliftedTypeKind, isSubOpenTypeKind, 
122   isSubArgTypeKind, tcIsSubKind, splitKindFunTys, defaultKind,
123   mkMetaKindVar,
124
125   --------------------------------
126   -- Rexported from Type
127   Type, PredType, ThetaType,
128   mkForAllTy, mkForAllTys, 
129   mkFunTy, mkFunTys, zipFunTys, 
130   mkTyConApp, mkAppTy, mkAppTys, applyTy, applyTys,
131   mkTyVarTy, mkTyVarTys, mkTyConTy,
132
133   isClassPred, isEqPred, isIPPred,
134   mkClassPred, mkIPPred,
135   isDictLikeTy,
136   tcSplitDFunTy, tcSplitDFunHead, 
137   mkEqPred, 
138
139   -- Type substitutions
140   TvSubst(..),  -- Representation visible to a few friends
141   TvSubstEnv, emptyTvSubst, 
142   mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst, 
143   mkTopTvSubst, notElemTvSubst, unionTvSubst,
144   getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope, 
145   Type.lookupTyVar, Type.extendTvSubst, Type.substTyVarBndr,
146   extendTvSubstList, isInScope, mkTvSubst, zipTyEnv,
147   Type.substTy, substTys, substTyWith, substTheta, substTyVar, substTyVars, 
148
149   isUnLiftedType,       -- Source types are always lifted
150   isUnboxedTupleType,   -- Ditto
151   isPrimitiveType, 
152
153   tyVarsOfType, tyVarsOfTypes,
154   tcTyVarsOfType, tcTyVarsOfTypes,
155
156   pprKind, pprParendKind,
157   pprType, pprParendType, pprTypeApp, pprTyThingCategory,
158   pprTheta, pprThetaArrowTy, pprClassPred
159
160   ) where
161
162 #include "HsVersions.h"
163
164 -- friends:
165 import Kind
166 import TypeRep
167 import Class
168 import Var
169 import ForeignCall
170 import VarSet
171 import Coercion
172 import Type
173 import TyCon
174
175 -- others:
176 import DynFlags
177 import Name hiding (varName)
178 import NameSet
179 import VarEnv
180 import PrelNames
181 import TysWiredIn
182 import BasicTypes
183 import Util
184 import Maybes
185 import ListSetOps
186 import Outputable
187 import FastString
188
189 import Data.List( mapAccumL )
190 import Data.IORef
191 \end{code}
192
193 %************************************************************************
194 %*                                                                      *
195 \subsection{Types}
196 %*                                                                      *
197 %************************************************************************
198
199 The type checker divides the generic Type world into the 
200 following more structured beasts:
201
202 sigma ::= forall tyvars. phi
203         -- A sigma type is a qualified type
204         --
205         -- Note that even if 'tyvars' is empty, theta
206         -- may not be: e.g.   (?x::Int) => Int
207
208         -- Note that 'sigma' is in prenex form:
209         -- all the foralls are at the front.
210         -- A 'phi' type has no foralls to the right of
211         -- an arrow
212
213 phi :: theta => rho
214
215 rho ::= sigma -> rho
216      |  tau
217
218 -- A 'tau' type has no quantification anywhere
219 -- Note that the args of a type constructor must be taus
220 tau ::= tyvar
221      |  tycon tau_1 .. tau_n
222      |  tau_1 tau_2
223      |  tau_1 -> tau_2
224
225 -- In all cases, a (saturated) type synonym application is legal,
226 -- provided it expands to the required form.
227
228 \begin{code}
229 type TcTyVar = TyVar    -- Used only during type inference
230 type TcCoVar = CoVar    -- Used only during type inference; mutable
231 type TcType = Type      -- A TcType can have mutable type variables
232         -- Invariant on ForAllTy in TcTypes:
233         --      forall a. T
234         -- a cannot occur inside a MutTyVar in T; that is,
235         -- T is "flattened" before quantifying over a
236
237 -- These types do not have boxy type variables in them
238 type TcPredType     = PredType
239 type TcThetaType    = ThetaType
240 type TcSigmaType    = TcType
241 type TcRhoType      = TcType
242 type TcTauType      = TcType
243 type TcKind         = Kind
244 type TcTyVarSet     = TyVarSet
245 \end{code}
246
247
248 %************************************************************************
249 %*                                                                      *
250 \subsection{TyVarDetails}
251 %*                                                                      *
252 %************************************************************************
253
254 TyVarDetails gives extra info about type variables, used during type
255 checking.  It's attached to mutable type variables only.
256 It's knot-tied back to Var.lhs.  There is no reason in principle
257 why Var.lhs shouldn't actually have the definition, but it "belongs" here.
258
259
260 Note [Signature skolems]
261 ~~~~~~~~~~~~~~~~~~~~~~~~
262 Consider this
263
264   x :: [a]
265   y :: b
266   (x,y,z) = ([y,z], z, head x)
267
268 Here, x and y have type sigs, which go into the environment.  We used to
269 instantiate their types with skolem constants, and push those types into
270 the RHS, so we'd typecheck the RHS with type
271         ( [a*], b*, c )
272 where a*, b* are skolem constants, and c is an ordinary meta type varible.
273
274 The trouble is that the occurrences of z in the RHS force a* and b* to 
275 be the *same*, so we can't make them into skolem constants that don't unify
276 with each other.  Alas.
277
278 One solution would be insist that in the above defn the programmer uses
279 the same type variable in both type signatures.  But that takes explanation.
280
281 The alternative (currently implemented) is to have a special kind of skolem
282 constant, SigTv, which can unify with other SigTvs.  These are *not* treated
283 as rigid for the purposes of GADTs.  And they are used *only* for pattern
284 bindings and mutually recursive function bindings.  See the function
285 TcBinds.tcInstSig, and its use_skols parameter.
286
287
288 \begin{code}
289 -- A TyVarDetails is inside a TyVar
290 data TcTyVarDetails
291   = SkolemTv      -- A skolem
292        Bool       -- True <=> this skolem type variable can be overlapped
293                   --          when looking up instances
294                   -- See Note [Binding when looking up instances] in InstEnv
295
296   | RuntimeUnk    -- Stands for an as-yet-unknown type in the GHCi
297                   -- interactive context
298
299   | FlatSkol TcType
300            -- The "skolem" obtained by flattening during
301            -- constraint simplification
302     
303            -- In comments we will use the notation alpha[flat = ty]
304            -- to represent a flattening skolem variable alpha
305            -- identified with type ty.
306           
307   | MetaTv MetaInfo (IORef MetaDetails)
308
309 vanillaSkolemTv, superSkolemTv :: TcTyVarDetails
310 -- See Note [Binding when looking up instances] in InstEnv
311 vanillaSkolemTv = SkolemTv False  -- Might be instantiated
312 superSkolemTv   = SkolemTv True   -- Treat this as a completely distinct type
313
314 data MetaDetails
315   = Flexi  -- Flexi type variables unify to become Indirects  
316   | Indirect TcType
317
318 instance Outputable MetaDetails where
319   ppr Flexi         = ptext (sLit "Flexi")
320   ppr (Indirect ty) = ptext (sLit "Indirect") <+> ppr ty
321
322 data MetaInfo
323    = TauTv         -- This MetaTv is an ordinary unification variable
324                    -- A TauTv is always filled in with a tau-type, which
325                    -- never contains any ForAlls 
326
327    | SigTv         -- A variant of TauTv, except that it should not be
328                    -- unified with a type, only with a type variable
329                    -- SigTvs are only distinguished to improve error messages
330                    --      see Note [Signature skolems]        
331                    --      The MetaDetails, if filled in, will 
332                    --      always be another SigTv or a SkolemTv
333
334    | TcsTv         -- A MetaTv allocated by the constraint solver
335                    -- Its particular property is that it is always "touchable"
336                    -- Nevertheless, the constraint solver has to try to guess
337                    -- what type to instantiate it to
338
339 -------------------------------------
340 -- UserTypeCtxt describes the origin of the polymorphic type
341 -- in the places where we need to an expression has that type
342
343 data UserTypeCtxt
344   = FunSigCtxt Name     -- Function type signature
345                         -- Also used for types in SPECIALISE pragmas
346   | InfSigCtxt Name     -- Inferred type for function
347   | ExprSigCtxt         -- Expression type signature
348   | ConArgCtxt Name     -- Data constructor argument
349   | TySynCtxt Name      -- RHS of a type synonym decl
350   | LamPatSigCtxt               -- Type sig in lambda pattern
351                         --      f (x::t) = ...
352   | BindPatSigCtxt      -- Type sig in pattern binding pattern
353                         --      (x::t, y) = e
354   | ResSigCtxt          -- Result type sig
355                         --      f x :: t = ....
356   | ForSigCtxt Name     -- Foreign import or export signature
357   | DefaultDeclCtxt     -- Types in a default declaration
358   | InstDeclCtxt        -- An instance declaration
359   | SpecInstCtxt        -- SPECIALISE instance pragma
360   | ThBrackCtxt         -- Template Haskell type brackets [t| ... |]
361   | GenSigCtxt          -- Higher-rank or impredicative situations
362                         -- e.g. (f e) where f has a higher-rank type
363                         -- We might want to elaborate this
364   | GhciCtxt            -- GHCi command :kind <type>
365
366   | ClassSCCtxt Name    -- Superclasses of a class
367   | SigmaCtxt           -- Theta part of a normal for-all type
368                         --      f :: <S> => a -> a
369   | DataTyCtxt Name     -- Theta part of a data decl
370                         --      data <S> => T a = MkT a
371 \end{code}
372
373
374 -- Notes re TySynCtxt
375 -- We allow type synonyms that aren't types; e.g.  type List = []
376 --
377 -- If the RHS mentions tyvars that aren't in scope, we'll 
378 -- quantify over them:
379 --      e.g.    type T = a->a
380 -- will become  type T = forall a. a->a
381 --
382 -- With gla-exts that's right, but for H98 we should complain. 
383
384 ---------------------------------
385 -- Kind variables:
386 \begin{code}
387 mkKindName :: Unique -> Name
388 mkKindName unique = mkSystemName unique kind_var_occ
389
390 mkMetaKindVar :: Unique -> IORef MetaDetails -> MetaKindVar
391 mkMetaKindVar u r
392   = mkTcTyVar (mkKindName u) superKind (MetaTv TauTv r)
393
394 kind_var_occ :: OccName -- Just one for all MetaKindVars
395                         -- They may be jiggled by tidying
396 kind_var_occ = mkOccName tvName "k"
397 \end{code}
398
399 %************************************************************************
400 %*                                                                      *
401                 Pretty-printing
402 %*                                                                      *
403 %************************************************************************
404
405 \begin{code}
406 pprTcTyVarDetails :: TcTyVarDetails -> SDoc
407 -- For debugging
408 pprTcTyVarDetails (SkolemTv True)  = ptext (sLit "ssk")
409 pprTcTyVarDetails (SkolemTv False) = ptext (sLit "sk")
410 pprTcTyVarDetails (RuntimeUnk {})  = ptext (sLit "rt")
411 pprTcTyVarDetails (FlatSkol {})    = ptext (sLit "fsk")
412 pprTcTyVarDetails (MetaTv TauTv _) = ptext (sLit "tau")
413 pprTcTyVarDetails (MetaTv TcsTv _) = ptext (sLit "tcs")
414 pprTcTyVarDetails (MetaTv SigTv _) = ptext (sLit "sig")
415
416 pprUserTypeCtxt :: UserTypeCtxt -> SDoc
417 pprUserTypeCtxt (InfSigCtxt n)    = ptext (sLit "the inferred type for") <+> quotes (ppr n)
418 pprUserTypeCtxt (FunSigCtxt n)    = ptext (sLit "the type signature for") <+> quotes (ppr n)
419 pprUserTypeCtxt ExprSigCtxt       = ptext (sLit "an expression type signature")
420 pprUserTypeCtxt (ConArgCtxt c)    = ptext (sLit "the type of the constructor") <+> quotes (ppr c)
421 pprUserTypeCtxt (TySynCtxt c)     = ptext (sLit "the RHS of the type synonym") <+> quotes (ppr c)
422 pprUserTypeCtxt ThBrackCtxt       = ptext (sLit "a Template Haskell quotation [t|...|]")
423 pprUserTypeCtxt LamPatSigCtxt     = ptext (sLit "a pattern type signature")
424 pprUserTypeCtxt BindPatSigCtxt    = ptext (sLit "a pattern type signature")
425 pprUserTypeCtxt ResSigCtxt        = ptext (sLit "a result type signature")
426 pprUserTypeCtxt (ForSigCtxt n)    = ptext (sLit "the foreign declaration for") <+> quotes (ppr n)
427 pprUserTypeCtxt DefaultDeclCtxt   = ptext (sLit "a type in a `default' declaration")
428 pprUserTypeCtxt InstDeclCtxt      = ptext (sLit "an instance declaration")
429 pprUserTypeCtxt SpecInstCtxt      = ptext (sLit "a SPECIALISE instance pragma")
430 pprUserTypeCtxt GenSigCtxt        = ptext (sLit "a type expected by the context")
431 pprUserTypeCtxt GhciCtxt          = ptext (sLit "a type in a GHCi command")
432 pprUserTypeCtxt (ClassSCCtxt c)   = ptext (sLit "the super-classes of class") <+> quotes (ppr c)
433 pprUserTypeCtxt SigmaCtxt         = ptext (sLit "the context of a polymorphic type")
434 pprUserTypeCtxt (DataTyCtxt tc)   = ptext (sLit "the context of the data type declaration for") <+> quotes (ppr tc)
435 \end{code}
436
437
438 %************************************************************************
439 %*                                                                      *
440 \subsection{TidyType}
441 %*                                                                      *
442 %************************************************************************
443
444 Tidying is here becuase it has a special case for FlatSkol
445
446 \begin{code}
447 -- | This tidies up a type for printing in an error message, or in
448 -- an interface file.
449 -- 
450 -- It doesn't change the uniques at all, just the print names.
451 tidyTyVarBndrs :: TidyEnv -> [TyVar] -> (TidyEnv, [TyVar])
452 tidyTyVarBndrs env tvs = mapAccumL tidyTyVarBndr env tvs
453
454 tidyTyVarBndr :: TidyEnv -> TyVar -> (TidyEnv, TyVar)
455 tidyTyVarBndr tidy_env@(occ_env, subst) tyvar
456   = case tidyOccName occ_env occ1 of
457       (tidy', occ') -> ((tidy', subst'), tyvar')
458         where
459           subst' = extendVarEnv subst tyvar tyvar'
460           tyvar' = setTyVarKind (setTyVarName tyvar name') kind'
461           name'  = tidyNameOcc name occ'
462           kind'  = tidyKind tidy_env (tyVarKind tyvar)
463   where
464     name = tyVarName tyvar
465     occ  = getOccName name
466     -- System Names are for unification variables;
467     -- when we tidy them we give them a trailing "0" (or 1 etc)
468     -- so that they don't take precedence for the un-modified name
469     occ1 | isSystemName name = mkTyVarOcc (occNameString occ ++ "0")
470          | otherwise         = occ
471
472
473 ---------------
474 tidyFreeTyVars :: TidyEnv -> TyVarSet -> TidyEnv
475 -- ^ Add the free 'TyVar's to the env in tidy form,
476 -- so that we can tidy the type they are free in
477 tidyFreeTyVars (full_occ_env, var_env) tyvars 
478   = fst (tidyOpenTyVars (trimmed_occ_env, var_env) tv_list)
479
480   where
481     tv_list = varSetElems tyvars
482     
483     trimmed_occ_env = foldr mk_occ_env emptyOccEnv tv_list
484       -- The idea here is that we restrict the new TidyEnv to the 
485       -- _free_ vars of the type, so that we don't gratuitously rename
486       -- the _bound_ variables of the type
487
488     mk_occ_env :: TyVar -> TidyOccEnv -> TidyOccEnv
489     mk_occ_env tv env 
490        = case lookupOccEnv full_occ_env occ of
491             Just n  -> extendOccEnv env occ n
492             Nothing -> env
493        where
494          occ = getOccName tv
495
496 ---------------
497 tidyOpenTyVars :: TidyEnv -> [TyVar] -> (TidyEnv, [TyVar])
498 tidyOpenTyVars env tyvars = mapAccumL tidyOpenTyVar env tyvars
499
500 ---------------
501 tidyOpenTyVar :: TidyEnv -> TyVar -> (TidyEnv, TyVar)
502 -- ^ Treat a new 'TyVar' as a binder, and give it a fresh tidy name
503 -- using the environment if one has not already been allocated. See
504 -- also 'tidyTyVarBndr'
505 tidyOpenTyVar env@(_, subst) tyvar
506   = case lookupVarEnv subst tyvar of
507         Just tyvar' -> (env, tyvar')            -- Already substituted
508         Nothing     -> tidyTyVarBndr env tyvar  -- Treat it as a binder
509
510 ---------------
511 tidyTyVarOcc :: TidyEnv -> TyVar -> Type
512 tidyTyVarOcc env@(_, subst) tv
513   = case lookupVarEnv subst tv of
514         Nothing  -> expand tv
515         Just tv' -> expand tv'
516   where
517     -- Expand FlatSkols, the skolems introduced by flattening process
518     -- We don't want to show them in type error messages
519     expand tv | isTcTyVar tv
520               , FlatSkol ty <- tcTyVarDetails tv
521               = WARN( True, text "I DON'T THINK THIS SHOULD EVER HAPPEN" <+> ppr tv <+> ppr ty )
522                 tidyType env ty
523               | otherwise
524               = TyVarTy tv
525
526 ---------------
527 tidyTypes :: TidyEnv -> [Type] -> [Type]
528 tidyTypes env tys = map (tidyType env) tys
529
530 ---------------
531 tidyType :: TidyEnv -> Type -> Type
532 tidyType env (TyVarTy tv)         = tidyTyVarOcc env tv
533 tidyType env (TyConApp tycon tys) = let args = tidyTypes env tys
534                                     in args `seqList` TyConApp tycon args
535 tidyType env (AppTy fun arg)      = (AppTy $! (tidyType env fun)) $! (tidyType env arg)
536 tidyType env (FunTy fun arg)      = (FunTy $! (tidyType env fun)) $! (tidyType env arg)
537 tidyType env (ForAllTy tv ty)     = ForAllTy tvp $! (tidyType envp ty)
538                                   where
539                                     (envp, tvp) = tidyTyVarBndr env tv
540
541 ---------------
542 -- | Grabs the free type variables, tidies them
543 -- and then uses 'tidyType' to work over the type itself
544 tidyOpenType :: TidyEnv -> Type -> (TidyEnv, Type)
545 tidyOpenType env ty
546   = (env', tidyType env' ty)
547   where
548     env' = tidyFreeTyVars env (tyVarsOfType ty)
549
550 ---------------
551 tidyOpenTypes :: TidyEnv -> [Type] -> (TidyEnv, [Type])
552 tidyOpenTypes env tys = mapAccumL tidyOpenType env tys
553
554 ---------------
555 -- | Calls 'tidyType' on a top-level type (i.e. with an empty tidying environment)
556 tidyTopType :: Type -> Type
557 tidyTopType ty = tidyType emptyTidyEnv ty
558
559 ---------------
560 tidyOpenKind :: TidyEnv -> Kind -> (TidyEnv, Kind)
561 tidyOpenKind = tidyOpenType
562
563 tidyKind :: TidyEnv -> Kind -> Kind
564 tidyKind = tidyType
565 \end{code}
566
567 %************************************************************************
568 %*                                                                      *
569                             Tidying coercions
570 %*                                                                      *
571 %************************************************************************
572
573 \begin{code}
574 tidyCo :: TidyEnv -> Coercion -> Coercion
575 tidyCo env@(_, subst) co
576   = go co
577   where
578     go (Refl ty)             = Refl (tidyType env ty)
579     go (TyConAppCo tc cos)   = let args = map go cos
580                                in args `seqList` TyConAppCo tc args
581     go (AppCo co1 co2)       = (AppCo $! go co1) $! go co2
582     go (ForAllCo tv co)      = ForAllCo tvp $! (tidyCo envp co)
583                                where
584                                  (envp, tvp) = tidyTyVarBndr env tv
585     go (CoVarCo cv)          = case lookupVarEnv subst cv of
586                                  Nothing  -> CoVarCo cv
587                                  Just cv' -> CoVarCo cv'
588     go (AxiomInstCo con cos) = let args = tidyCos env cos
589                                in  args `seqList` AxiomInstCo con args
590     go (UnsafeCo ty1 ty2)    = (UnsafeCo $! tidyType env ty1) $! tidyType env ty2
591     go (SymCo co)            = SymCo $! go co
592     go (TransCo co1 co2)     = (TransCo $! go co1) $! go co2
593     go (NthCo d co)          = NthCo d $! go co
594     go (InstCo co ty)        = (InstCo $! go co) $! tidyType env ty
595
596 tidyCos :: TidyEnv -> [Coercion] -> [Coercion]
597 tidyCos env = map (tidyCo env)
598 \end{code}
599
600 %************************************************************************
601 %*                  *
602     Finding type family instances
603 %*                  *
604 %************************************************************************
605
606 \begin{code}
607
608 -- | Finds type family instances occuring in a type after expanding synonyms.
609 tcTyFamInsts :: Type -> [(TyCon, [Type])]
610 tcTyFamInsts ty 
611   | Just exp_ty <- tcView ty    = tcTyFamInsts exp_ty
612 tcTyFamInsts (TyVarTy _)          = []
613 tcTyFamInsts (TyConApp tc tys) 
614   | isSynFamilyTyCon tc           = [(tc, tys)]
615   | otherwise                   = concat (map tcTyFamInsts tys)
616 tcTyFamInsts (FunTy ty1 ty2)      = tcTyFamInsts ty1 ++ tcTyFamInsts ty2
617 tcTyFamInsts (AppTy ty1 ty2)      = tcTyFamInsts ty1 ++ tcTyFamInsts ty2
618 tcTyFamInsts (ForAllTy _ ty)      = tcTyFamInsts ty
619 \end{code}
620
621 %************************************************************************
622 %*                  *
623           The "exact" free variables of a type
624 %*                  *
625 %************************************************************************
626
627 Note [Silly type synonym]
628 ~~~~~~~~~~~~~~~~~~~~~~~~~
629 Consider
630   type T a = Int
631 What are the free tyvars of (T x)?  Empty, of course!  
632 Here's the example that Ralf Laemmel showed me:
633   foo :: (forall a. C u a -> C u a) -> u
634   mappend :: Monoid u => u -> u -> u
635
636   bar :: Monoid u => u
637   bar = foo (\t -> t `mappend` t)
638 We have to generalise at the arg to f, and we don't
639 want to capture the constraint (Monad (C u a)) because
640 it appears to mention a.  Pretty silly, but it was useful to him.
641
642 exactTyVarsOfType is used by the type checker to figure out exactly
643 which type variables are mentioned in a type.  It's also used in the
644 smart-app checking code --- see TcExpr.tcIdApp
645
646 On the other hand, consider a *top-level* definition
647   f = (\x -> x) :: T a -> T a
648 If we don't abstract over 'a' it'll get fixed to GHC.Prim.Any, and then
649 if we have an application like (f "x") we get a confusing error message 
650 involving Any.  So the conclusion is this: when generalising
651   - at top level use tyVarsOfType
652   - in nested bindings use exactTyVarsOfType
653 See Trac #1813 for example.
654
655 \begin{code}
656 exactTyVarsOfType :: Type -> TyVarSet
657 -- Find the free type variables (of any kind)
658 -- but *expand* type synonyms.  See Note [Silly type synonym] above.
659 exactTyVarsOfType ty
660   = go ty
661   where
662     go ty | Just ty' <- tcView ty = go ty'  -- This is the key line
663     go (TyVarTy tv)         = unitVarSet tv
664     go (TyConApp _ tys)     = exactTyVarsOfTypes tys
665     go (FunTy arg res)      = go arg `unionVarSet` go res
666     go (AppTy fun arg)      = go fun `unionVarSet` go arg
667     go (ForAllTy tyvar ty)  = delVarSet (go ty) tyvar
668
669 exactTyVarsOfTypes :: [Type] -> TyVarSet
670 exactTyVarsOfTypes tys = foldr (unionVarSet . exactTyVarsOfType) emptyVarSet tys
671 \end{code}
672
673 %************************************************************************
674 %*                                                                      *
675                 Predicates
676 %*                                                                      *
677 %************************************************************************
678
679 \begin{code}
680 isImmutableTyVar :: TyVar -> Bool
681
682 isImmutableTyVar tv
683   | isTcTyVar tv = isSkolemTyVar tv
684   | otherwise    = True
685
686 isTyConableTyVar, isSkolemTyVar, isOverlappableTyVar,
687   isMetaTyVar, isAmbiguousTyVar :: TcTyVar -> Bool 
688
689 isTyConableTyVar tv     
690         -- True of a meta-type variable that can be filled in 
691         -- with a type constructor application; in particular,
692         -- not a SigTv
693   = ASSERT( isTcTyVar tv) 
694     case tcTyVarDetails tv of
695         MetaTv SigTv _ -> False
696         _              -> True
697         
698 isSkolemTyVar tv 
699   = ASSERT2( isTcTyVar tv, ppr tv )
700     case tcTyVarDetails tv of
701         SkolemTv {}   -> True
702         FlatSkol {}   -> True
703         RuntimeUnk {} -> True
704         MetaTv {}     -> False
705
706 isOverlappableTyVar tv
707   = ASSERT( isTcTyVar tv )
708     case tcTyVarDetails tv of
709         SkolemTv overlappable -> overlappable
710         _                     -> False
711
712 isMetaTyVar tv 
713   = ASSERT2( isTcTyVar tv, ppr tv )
714     case tcTyVarDetails tv of
715         MetaTv {} -> True
716         _         -> False
717
718 -- isAmbiguousTyVar is used only when reporting type errors
719 -- It picks out variables that are unbound, namely meta
720 -- type variables and the RuntimUnk variables created by
721 -- RtClosureInspect.zonkRTTIType.  These are "ambiguous" in
722 -- the sense that they stand for an as-yet-unknown type
723 isAmbiguousTyVar tv 
724   = ASSERT2( isTcTyVar tv, ppr tv )
725     case tcTyVarDetails tv of
726         MetaTv {}     -> True
727         RuntimeUnk {} -> True
728         _             -> False
729
730 isMetaTyVarTy :: TcType -> Bool
731 isMetaTyVarTy (TyVarTy tv) = isMetaTyVar tv
732 isMetaTyVarTy _            = False
733
734 isSigTyVar :: Var -> Bool
735 isSigTyVar tv 
736   = ASSERT( isTcTyVar tv )
737     case tcTyVarDetails tv of
738         MetaTv SigTv _ -> True
739         _              -> False
740
741 metaTvRef :: TyVar -> IORef MetaDetails
742 metaTvRef tv 
743   = ASSERT2( isTcTyVar tv, ppr tv )
744     case tcTyVarDetails tv of
745         MetaTv _ ref -> ref
746         _          -> pprPanic "metaTvRef" (ppr tv)
747
748 isFlexi, isIndirect :: MetaDetails -> Bool
749 isFlexi Flexi = True
750 isFlexi _     = False
751
752 isIndirect (Indirect _) = True
753 isIndirect _            = False
754
755 isRuntimeUnkSkol :: TyVar -> Bool
756 -- Called only in TcErrors; see Note [Runtime skolems] there
757 isRuntimeUnkSkol x
758   | isTcTyVar x, RuntimeUnk <- tcTyVarDetails x = True
759   | otherwise                                   = False
760 \end{code}
761
762
763 %************************************************************************
764 %*                                                                      *
765 \subsection{Tau, sigma and rho}
766 %*                                                                      *
767 %************************************************************************
768
769 \begin{code}
770 mkSigmaTy :: [TyVar] -> [PredType] -> Type -> Type
771 mkSigmaTy tyvars theta tau = mkForAllTys tyvars (mkPhiTy theta tau)
772
773 mkPhiTy :: [PredType] -> Type -> Type
774 mkPhiTy theta ty = foldr mkFunTy ty theta
775
776 mkTcEqPred :: TcType -> TcType -> Type
777 -- During type checking we build equalities between 
778 -- type variables with OpenKind or ArgKind.  Ultimately
779 -- they will all settle, but we want the equality predicate
780 -- itself to have kind '*'.  I think.  
781 --
782 -- But this is horribly delicate: what about type variables
783 -- that turn out to be bound to Int#?
784 mkTcEqPred ty1 ty2
785   = mkNakedEqPred (defaultKind (typeKind ty1)) ty1 ty2
786 \end{code}
787
788 @isTauTy@ tests for nested for-alls.  It should not be called on a boxy type.
789
790 \begin{code}
791 isTauTy :: Type -> Bool
792 isTauTy ty | Just ty' <- tcView ty = isTauTy ty'
793 isTauTy (TyVarTy _)       = True
794 isTauTy (TyConApp tc tys) = all isTauTy tys && isTauTyCon tc
795 isTauTy (AppTy a b)       = isTauTy a && isTauTy b
796 isTauTy (FunTy a b)       = isTauTy a && isTauTy b
797 isTauTy _                 = False
798
799 isTauTyCon :: TyCon -> Bool
800 -- Returns False for type synonyms whose expansion is a polytype
801 isTauTyCon tc 
802   | isClosedSynTyCon tc = isTauTy (snd (synTyConDefn tc))
803   | otherwise           = True
804
805 ---------------
806 getDFunTyKey :: Type -> OccName -- Get some string from a type, to be used to
807                                 -- construct a dictionary function name
808 getDFunTyKey ty | Just ty' <- tcView ty = getDFunTyKey ty'
809 getDFunTyKey (TyVarTy tv)    = getOccName tv
810 getDFunTyKey (TyConApp tc _) = getOccName tc
811 getDFunTyKey (AppTy fun _)   = getDFunTyKey fun
812 getDFunTyKey (FunTy _ _)     = getOccName funTyCon
813 getDFunTyKey (ForAllTy _ t)  = getDFunTyKey t
814 \end{code}
815
816
817 %************************************************************************
818 %*                                                                      *
819 \subsection{Expanding and splitting}
820 %*                                                                      *
821 %************************************************************************
822
823 These tcSplit functions are like their non-Tc analogues, but
824         *) they do not look through newtypes
825
826 However, they are non-monadic and do not follow through mutable type
827 variables.  It's up to you to make sure this doesn't matter.
828
829 \begin{code}
830 tcSplitForAllTys :: Type -> ([TyVar], Type)
831 tcSplitForAllTys ty = split ty ty []
832    where
833      split orig_ty ty tvs | Just ty' <- tcView ty = split orig_ty ty' tvs
834      split _ (ForAllTy tv ty) tvs = split ty ty (tv:tvs)
835      split orig_ty _          tvs = (reverse tvs, orig_ty)
836
837 tcIsForAllTy :: Type -> Bool
838 tcIsForAllTy ty | Just ty' <- tcView ty = tcIsForAllTy ty'
839 tcIsForAllTy (ForAllTy {}) = True
840 tcIsForAllTy _             = False
841
842 tcSplitPredFunTy_maybe :: Type -> Maybe (PredType, Type)
843 -- Split off the first predicate argument from a type
844 tcSplitPredFunTy_maybe ty 
845   | Just ty' <- tcView ty = tcSplitPredFunTy_maybe ty'
846 tcSplitPredFunTy_maybe (FunTy arg res)
847   | isPredTy arg = Just (arg, res)
848 tcSplitPredFunTy_maybe _
849   = Nothing
850
851 tcSplitPhiTy :: Type -> (ThetaType, Type)
852 tcSplitPhiTy ty
853   = split ty []
854   where
855     split ty ts 
856       = case tcSplitPredFunTy_maybe ty of
857           Just (pred, ty) -> split ty (pred:ts)
858           Nothing         -> (reverse ts, ty)
859
860 tcSplitSigmaTy :: Type -> ([TyVar], ThetaType, Type)
861 tcSplitSigmaTy ty = case tcSplitForAllTys ty of
862                         (tvs, rho) -> case tcSplitPhiTy rho of
863                                         (theta, tau) -> (tvs, theta, tau)
864
865 -----------------------
866 tcDeepSplitSigmaTy_maybe
867   :: TcSigmaType -> Maybe ([TcType], [TyVar], ThetaType, TcSigmaType)
868 -- Looks for a *non-trivial* quantified type, under zero or more function arrows
869 -- By "non-trivial" we mean either tyvars or constraints are non-empty
870
871 tcDeepSplitSigmaTy_maybe ty
872   | Just (arg_ty, res_ty)           <- tcSplitFunTy_maybe ty
873   , Just (arg_tys, tvs, theta, rho) <- tcDeepSplitSigmaTy_maybe res_ty
874   = Just (arg_ty:arg_tys, tvs, theta, rho)
875
876   | (tvs, theta, rho) <- tcSplitSigmaTy ty
877   , not (null tvs && null theta)
878   = Just ([], tvs, theta, rho)
879
880   | otherwise = Nothing
881
882 -----------------------
883 tcTyConAppTyCon :: Type -> TyCon
884 tcTyConAppTyCon ty = case tcSplitTyConApp_maybe ty of
885                         Just (tc, _) -> tc
886                         Nothing      -> pprPanic "tcTyConAppTyCon" (pprType ty)
887
888 tcTyConAppArgs :: Type -> [Type]
889 tcTyConAppArgs ty = case tcSplitTyConApp_maybe ty of
890                         Just (_, args) -> args
891                         Nothing        -> pprPanic "tcTyConAppArgs" (pprType ty)
892
893 tcSplitTyConApp :: Type -> (TyCon, [Type])
894 tcSplitTyConApp ty = case tcSplitTyConApp_maybe ty of
895                         Just stuff -> stuff
896                         Nothing    -> pprPanic "tcSplitTyConApp" (pprType ty)
897
898 tcSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
899 tcSplitTyConApp_maybe ty | Just ty' <- tcView ty = tcSplitTyConApp_maybe ty'
900 tcSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
901 tcSplitTyConApp_maybe (FunTy arg res)   = Just (funTyCon, [arg,res])
902         -- Newtypes are opaque, so they may be split
903         -- However, predicates are not treated
904         -- as tycon applications by the type checker
905 tcSplitTyConApp_maybe _                 = Nothing
906
907 -----------------------
908 tcSplitFunTys :: Type -> ([Type], Type)
909 tcSplitFunTys ty = case tcSplitFunTy_maybe ty of
910                         Nothing        -> ([], ty)
911                         Just (arg,res) -> (arg:args, res')
912                                        where
913                                           (args,res') = tcSplitFunTys res
914
915 tcSplitFunTy_maybe :: Type -> Maybe (Type, Type)
916 tcSplitFunTy_maybe ty | Just ty' <- tcView ty           = tcSplitFunTy_maybe ty'
917 tcSplitFunTy_maybe (FunTy arg res) | not (isPredTy arg) = Just (arg, res)
918 tcSplitFunTy_maybe _                                    = Nothing
919         -- Note the typeKind guard
920         -- Consider     (?x::Int) => Bool
921         -- We don't want to treat this as a function type!
922         -- A concrete example is test tc230:
923         --      f :: () -> (?p :: ()) => () -> ()
924         --
925         --      g = f () ()
926
927 tcSplitFunTysN
928         :: TcRhoType 
929         -> Arity                -- N: Number of desired args
930         -> ([TcSigmaType],      -- Arg types (N or fewer)
931             TcSigmaType)        -- The rest of the type
932
933 tcSplitFunTysN ty n_args
934   | n_args == 0
935   = ([], ty)
936   | Just (arg,res) <- tcSplitFunTy_maybe ty
937   = case tcSplitFunTysN res (n_args - 1) of
938         (args, res) -> (arg:args, res)
939   | otherwise
940   = ([], ty)
941
942 tcSplitFunTy :: Type -> (Type, Type)
943 tcSplitFunTy  ty = expectJust "tcSplitFunTy" (tcSplitFunTy_maybe ty)
944
945 tcFunArgTy :: Type -> Type
946 tcFunArgTy    ty = fst (tcSplitFunTy ty)
947
948 tcFunResultTy :: Type -> Type
949 tcFunResultTy ty = snd (tcSplitFunTy ty)
950
951 -----------------------
952 tcSplitAppTy_maybe :: Type -> Maybe (Type, Type)
953 tcSplitAppTy_maybe ty | Just ty' <- tcView ty = tcSplitAppTy_maybe ty'
954 tcSplitAppTy_maybe ty = repSplitAppTy_maybe ty
955
956 tcSplitAppTy :: Type -> (Type, Type)
957 tcSplitAppTy ty = case tcSplitAppTy_maybe ty of
958                     Just stuff -> stuff
959                     Nothing    -> pprPanic "tcSplitAppTy" (pprType ty)
960
961 tcSplitAppTys :: Type -> (Type, [Type])
962 tcSplitAppTys ty
963   = go ty []
964   where
965     go ty args = case tcSplitAppTy_maybe ty of
966                    Just (ty', arg) -> go ty' (arg:args)
967                    Nothing         -> (ty,args)
968
969 -----------------------
970 tcGetTyVar_maybe :: Type -> Maybe TyVar
971 tcGetTyVar_maybe ty | Just ty' <- tcView ty = tcGetTyVar_maybe ty'
972 tcGetTyVar_maybe (TyVarTy tv)   = Just tv
973 tcGetTyVar_maybe _              = Nothing
974
975 tcGetTyVar :: String -> Type -> TyVar
976 tcGetTyVar msg ty = expectJust msg (tcGetTyVar_maybe ty)
977
978 tcIsTyVarTy :: Type -> Bool
979 tcIsTyVarTy ty = maybeToBool (tcGetTyVar_maybe ty)
980
981 -----------------------
982 tcSplitDFunTy :: Type -> ([TyVar], Int, Class, [Type])
983 -- Split the type of a dictionary function
984 -- We don't use tcSplitSigmaTy,  because a DFun may (with NDP)
985 -- have non-Pred arguments, such as
986 --     df :: forall m. (forall b. Eq b => Eq (m b)) -> C m
987 tcSplitDFunTy ty 
988   = case tcSplitForAllTys ty   of { (tvs, rho)  ->
989     case split_dfun_args 0 rho of { (n_theta, tau) ->
990     case tcSplitDFunHead tau   of { (clas, tys) ->
991     (tvs, n_theta, clas, tys) }}}
992   where
993     -- Count the context of the dfun.  This can be a mix of
994     -- coercion and class constraints; or (in the general NDP case)
995     -- some other function argument
996     split_dfun_args n ty | Just ty' <- tcView ty = split_dfun_args n ty'
997     split_dfun_args n (FunTy _ ty)     = split_dfun_args (n+1) ty
998     split_dfun_args n ty               = (n, ty)
999
1000 tcSplitDFunHead :: Type -> (Class, [Type])
1001 tcSplitDFunHead = getClassPredTys
1002
1003 tcInstHeadTyNotSynonym :: Type -> Bool
1004 -- Used in Haskell-98 mode, for the argument types of an instance head
1005 -- These must not be type synonyms, but everywhere else type synonyms
1006 -- are transparent, so we need a special function here
1007 tcInstHeadTyNotSynonym ty
1008   = case ty of
1009         TyConApp tc _ -> not (isSynTyCon tc)
1010         _ -> True
1011
1012 tcInstHeadTyAppAllTyVars :: Type -> Bool
1013 -- Used in Haskell-98 mode, for the argument types of an instance head
1014 -- These must be a constructor applied to type variable arguments.
1015 -- But we allow kind instantiations.
1016 tcInstHeadTyAppAllTyVars ty
1017   | Just ty' <- tcView ty       -- Look through synonyms
1018   = tcInstHeadTyAppAllTyVars ty'
1019   | otherwise
1020   = case ty of
1021         TyConApp _ tys  -> ok (filter (not . isKind) tys)  -- avoid kinds
1022         FunTy arg res   -> ok [arg, res]
1023         _               -> False
1024   where
1025         -- Check that all the types are type variables,
1026         -- and that each is distinct
1027     ok tys = equalLength tvs tys && hasNoDups tvs
1028            where
1029              tvs = mapCatMaybes get_tv tys
1030
1031     get_tv (TyVarTy tv)  = Just tv      -- through synonyms
1032     get_tv _             = Nothing
1033 \end{code}
1034
1035 \begin{code}
1036 pickyEqType :: TcType -> TcType -> Bool
1037 -- Check when two types _look_ the same, _including_ synonyms.  
1038 -- So (pickyEqType String [Char]) returns False
1039 pickyEqType ty1 ty2
1040   = go init_env ty1 ty2
1041   where
1042     init_env = mkRnEnv2 (mkInScopeSet (tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2))
1043     go env (TyVarTy tv1)       (TyVarTy tv2)     = rnOccL env tv1 == rnOccR env tv2
1044     go env (ForAllTy tv1 t1)   (ForAllTy tv2 t2) = go (rnBndr2 env tv1 tv2) t1 t2
1045     go env (AppTy s1 t1)       (AppTy s2 t2)     = go env s1 s2 && go env t1 t2
1046     go env (FunTy s1 t1)       (FunTy s2 t2)     = go env s1 s2 && go env t1 t2
1047     go env (TyConApp tc1 ts1) (TyConApp tc2 ts2) = (tc1 == tc2) && gos env ts1 ts2
1048     go _ _ _ = False
1049
1050     gos _   []       []       = True
1051     gos env (t1:ts1) (t2:ts2) = go env t1 t2 && gos env ts1 ts2
1052     gos _ _ _ = False
1053 \end{code}
1054
1055 %************************************************************************
1056 %*                                                                      *
1057 \subsection{Predicate types}
1058 %*                                                                      *
1059 %************************************************************************
1060
1061 Deconstructors and tests on predicate types
1062
1063 \begin{code}
1064 -- | Like 'classifyPredType' but doesn't look through type synonyms.
1065 -- Used to check that programs only use "simple" contexts without any
1066 -- synonyms in them.
1067 shallowPredTypePredTree :: PredType -> PredTree
1068 shallowPredTypePredTree ev_ty
1069   | TyConApp tc tys <- ev_ty
1070   = case () of
1071       () | Just clas <- tyConClass_maybe tc
1072          -> ClassPred clas tys
1073       () | tc `hasKey` eqTyConKey
1074          , let [_, ty1, ty2] = tys
1075          -> EqPred ty1 ty2
1076       () | Just ip <- tyConIP_maybe tc
1077          , let [ty] = tys
1078          -> IPPred ip ty
1079       () | isTupleTyCon tc
1080          -> TuplePred tys
1081       _ -> IrredPred ev_ty
1082   | otherwise
1083   = IrredPred ev_ty
1084
1085 isTyVarClassPred :: PredType -> Bool
1086 isTyVarClassPred ty = case getClassPredTys_maybe ty of
1087     Just (_, tys) -> all isTyVarTy tys
1088     _             -> False
1089
1090 evVarPred_maybe :: EvVar -> Maybe PredType
1091 evVarPred_maybe v = if isPredTy ty then Just ty else Nothing
1092   where ty = varType v
1093
1094 evVarPred :: EvVar -> PredType
1095 evVarPred var
1096  | debugIsOn
1097   = case evVarPred_maybe var of
1098       Just pred -> pred
1099       Nothing   -> pprPanic "tcEvVarPred" (ppr var <+> ppr (varType var))
1100  | otherwise
1101   = varType var
1102 \end{code}
1103
1104 Superclasses
1105
1106 \begin{code}
1107 mkMinimalBySCs :: [PredType] -> [PredType]
1108 -- Remove predicates that can be deduced from others by superclasses
1109 mkMinimalBySCs ptys = [ ploc |  ploc <- ptys
1110                              ,  ploc `not_in_preds` rec_scs ]
1111  where
1112    rec_scs = concatMap trans_super_classes ptys
1113    not_in_preds p ps = null (filter (eqPred p) ps)
1114
1115    trans_super_classes pred   -- Superclasses of pred, excluding pred itself
1116      = case classifyPredType pred of
1117          ClassPred cls tys -> transSuperClasses cls tys
1118          TuplePred ts      -> concatMap trans_super_classes ts
1119          _                 -> []
1120
1121 transSuperClasses :: Class -> [Type] -> [PredType]
1122 transSuperClasses cls tys    -- Superclasses of (cls tys),
1123                              -- excluding (cls tys) itself
1124   = concatMap trans_sc (immSuperClasses cls tys)
1125   where 
1126     trans_sc :: PredType -> [PredType]
1127     -- (trans_sc p) returns (p : p's superclasses)
1128     trans_sc p = case classifyPredType p of
1129                    ClassPred cls tys -> p : transSuperClasses cls tys
1130                    TuplePred ps      -> concatMap trans_sc ps
1131                    _                 -> [p]
1132
1133 immSuperClasses :: Class -> [Type] -> [PredType]
1134 immSuperClasses cls tys
1135   = substTheta (zipTopTvSubst tyvars tys) sc_theta
1136   where 
1137     (tyvars,sc_theta,_,_) = classBigSig cls
1138 \end{code}
1139
1140
1141 %************************************************************************
1142 %*                                                                      *
1143 \subsection{Predicates}
1144 %*                                                                      *
1145 %************************************************************************
1146
1147 isSigmaTy returns true of any qualified type.  It doesn't *necessarily* have 
1148 any foralls.  E.g.
1149         f :: (?x::Int) => Int -> Int
1150
1151 \begin{code}
1152 isSigmaTy :: Type -> Bool
1153 isSigmaTy ty | Just ty' <- tcView ty = isSigmaTy ty'
1154 isSigmaTy (ForAllTy _ _) = True
1155 isSigmaTy (FunTy a _)    = isPredTy a
1156 isSigmaTy _              = False
1157
1158 isOverloadedTy :: Type -> Bool
1159 -- Yes for a type of a function that might require evidence-passing
1160 -- Used only by bindLocalMethods
1161 isOverloadedTy ty | Just ty' <- tcView ty = isOverloadedTy ty'
1162 isOverloadedTy (ForAllTy _ ty) = isOverloadedTy ty
1163 isOverloadedTy (FunTy a _)     = isPredTy a
1164 isOverloadedTy _               = False
1165 \end{code}
1166
1167 \begin{code}
1168 isFloatTy, isDoubleTy, isIntegerTy, isIntTy, isWordTy, isBoolTy,
1169     isUnitTy, isCharTy :: Type -> Bool
1170 isFloatTy      = is_tc floatTyConKey
1171 isDoubleTy     = is_tc doubleTyConKey
1172 isIntegerTy    = is_tc integerTyConKey
1173 isIntTy        = is_tc intTyConKey
1174 isWordTy       = is_tc wordTyConKey
1175 isBoolTy       = is_tc boolTyConKey
1176 isUnitTy       = is_tc unitTyConKey
1177 isCharTy       = is_tc charTyConKey
1178
1179 isStringTy :: Type -> Bool
1180 isStringTy ty
1181   = case tcSplitTyConApp_maybe ty of
1182       Just (tc, [arg_ty]) -> tc == listTyCon && isCharTy arg_ty
1183       _                   -> False
1184
1185 is_tc :: Unique -> Type -> Bool
1186 -- Newtypes are opaque to this
1187 is_tc uniq ty = case tcSplitTyConApp_maybe ty of
1188                         Just (tc, _) -> uniq == getUnique tc
1189                         Nothing      -> False
1190 \end{code}
1191
1192 \begin{code}
1193 -- NB: Currently used in places where we have already expanded type synonyms;
1194 --     hence no 'coreView'.  This could, however, be changed without breaking
1195 --     any code.
1196 isSynFamilyTyConApp :: TcTauType -> Bool
1197 isSynFamilyTyConApp (TyConApp tc tys) = isSynFamilyTyCon tc && 
1198                                       length tys == tyConArity tc 
1199 isSynFamilyTyConApp _other            = False
1200 \end{code}
1201
1202
1203 %************************************************************************
1204 %*                                                                      *
1205 \subsection{Misc}
1206 %*                                                                      *
1207 %************************************************************************
1208
1209 \begin{code}
1210 deNoteType :: Type -> Type
1211 -- Remove all *outermost* type synonyms and other notes
1212 deNoteType ty | Just ty' <- tcView ty = deNoteType ty'
1213 deNoteType ty = ty
1214
1215 tcTyVarsOfType :: Type -> TcTyVarSet
1216 -- Just the *TcTyVars* free in the type
1217 -- (Types.tyVarsOfTypes finds all free TyVars)
1218 tcTyVarsOfType (TyVarTy tv)         = if isTcTyVar tv then unitVarSet tv
1219                                                       else emptyVarSet
1220 tcTyVarsOfType (TyConApp _ tys)     = tcTyVarsOfTypes tys
1221 tcTyVarsOfType (FunTy arg res)      = tcTyVarsOfType arg `unionVarSet` tcTyVarsOfType res
1222 tcTyVarsOfType (AppTy fun arg)      = tcTyVarsOfType fun `unionVarSet` tcTyVarsOfType arg
1223 tcTyVarsOfType (ForAllTy tyvar ty)  = tcTyVarsOfType ty `delVarSet` tyvar
1224         -- We do sometimes quantify over skolem TcTyVars
1225
1226 tcTyVarsOfTypes :: [Type] -> TyVarSet
1227 tcTyVarsOfTypes tys = foldr (unionVarSet.tcTyVarsOfType) emptyVarSet tys
1228 \end{code}
1229
1230 Find the free tycons and classes of a type.  This is used in the front
1231 end of the compiler.
1232
1233 \begin{code}
1234 orphNamesOfTyCon :: TyCon -> NameSet
1235 orphNamesOfTyCon tycon = unitNameSet (getName tycon) `unionNameSets` case tyConClass_maybe tycon of
1236     Nothing  -> emptyNameSet
1237     Just cls -> unitNameSet (getName cls)
1238
1239 orphNamesOfType :: Type -> NameSet
1240 orphNamesOfType ty | Just ty' <- tcView ty = orphNamesOfType ty'
1241                 -- Look through type synonyms (Trac #4912)
1242 orphNamesOfType (TyVarTy _)                = emptyNameSet
1243 orphNamesOfType (TyConApp tycon tys)       = orphNamesOfTyCon tycon
1244                                              `unionNameSets` orphNamesOfTypes tys
1245 orphNamesOfType (FunTy arg res)     = orphNamesOfType arg `unionNameSets` orphNamesOfType res
1246 orphNamesOfType (AppTy fun arg)     = orphNamesOfType fun `unionNameSets` orphNamesOfType arg
1247 orphNamesOfType (ForAllTy _ ty)     = orphNamesOfType ty
1248
1249 orphNamesOfTypes :: [Type] -> NameSet
1250 orphNamesOfTypes tys = foldr (unionNameSets . orphNamesOfType) emptyNameSet tys
1251
1252 orphNamesOfDFunHead :: Type -> NameSet
1253 -- Find the free type constructors and classes 
1254 -- of the head of the dfun instance type
1255 -- The 'dfun_head_type' is because of
1256 --      instance Foo a => Baz T where ...
1257 -- The decl is an orphan if Baz and T are both not locally defined,
1258 --      even if Foo *is* locally defined
1259 orphNamesOfDFunHead dfun_ty 
1260   = case tcSplitSigmaTy dfun_ty of
1261         (_, _, head_ty) -> orphNamesOfType head_ty
1262         
1263 orphNamesOfCo :: Coercion -> NameSet
1264 orphNamesOfCo (Refl ty)             = orphNamesOfType ty
1265 orphNamesOfCo (TyConAppCo tc cos)   = unitNameSet (getName tc) `unionNameSets` orphNamesOfCos cos
1266 orphNamesOfCo (AppCo co1 co2)       = orphNamesOfCo co1 `unionNameSets` orphNamesOfCo co2
1267 orphNamesOfCo (ForAllCo _ co)       = orphNamesOfCo co
1268 orphNamesOfCo (CoVarCo _)           = emptyNameSet
1269 orphNamesOfCo (AxiomInstCo con cos) = orphNamesOfCoCon con `unionNameSets` orphNamesOfCos cos
1270 orphNamesOfCo (UnsafeCo ty1 ty2)    = orphNamesOfType ty1 `unionNameSets` orphNamesOfType ty2
1271 orphNamesOfCo (SymCo co)            = orphNamesOfCo co
1272 orphNamesOfCo (TransCo co1 co2)     = orphNamesOfCo co1 `unionNameSets` orphNamesOfCo co2
1273 orphNamesOfCo (NthCo _ co)          = orphNamesOfCo co
1274 orphNamesOfCo (InstCo co ty)        = orphNamesOfCo co `unionNameSets` orphNamesOfType ty
1275
1276 orphNamesOfCos :: [Coercion] -> NameSet
1277 orphNamesOfCos = foldr (unionNameSets . orphNamesOfCo) emptyNameSet
1278
1279 orphNamesOfCoCon :: CoAxiom -> NameSet
1280 orphNamesOfCoCon (CoAxiom { co_ax_lhs = ty1, co_ax_rhs = ty2 })
1281   = orphNamesOfType ty1 `unionNameSets` orphNamesOfType ty2
1282 \end{code}
1283
1284
1285 %************************************************************************
1286 %*                                                                      *
1287 \subsection[TysWiredIn-ext-type]{External types}
1288 %*                                                                      *
1289 %************************************************************************
1290
1291 The compiler's foreign function interface supports the passing of a
1292 restricted set of types as arguments and results (the restricting factor
1293 being the )
1294
1295 \begin{code}
1296 tcSplitIOType_maybe :: Type -> Maybe (TyCon, Type)
1297 -- (tcSplitIOType_maybe t) returns Just (IO,t',co)
1298 --              if co : t ~ IO t'
1299 --              returns Nothing otherwise
1300 tcSplitIOType_maybe ty
1301   = case tcSplitTyConApp_maybe ty of
1302         Just (io_tycon, [io_res_ty])
1303          | io_tycon `hasKey` ioTyConKey ->
1304             Just (io_tycon, io_res_ty)
1305         _ ->
1306             Nothing
1307
1308 isFFITy :: Type -> Bool
1309 -- True for any TyCon that can possibly be an arg or result of an FFI call
1310 isFFITy ty = checkRepTyCon legalFFITyCon ty
1311
1312 isFFIArgumentTy :: DynFlags -> Safety -> Type -> Bool
1313 -- Checks for valid argument type for a 'foreign import'
1314 isFFIArgumentTy dflags safety ty 
1315    = checkRepTyCon (legalOutgoingTyCon dflags safety) ty
1316
1317 isFFIExternalTy :: Type -> Bool
1318 -- Types that are allowed as arguments of a 'foreign export'
1319 isFFIExternalTy ty = checkRepTyCon legalFEArgTyCon ty
1320
1321 isFFIImportResultTy :: DynFlags -> Type -> Bool
1322 isFFIImportResultTy dflags ty 
1323   = checkRepTyCon (legalFIResultTyCon dflags) ty
1324
1325 isFFIExportResultTy :: Type -> Bool
1326 isFFIExportResultTy ty = checkRepTyCon legalFEResultTyCon ty
1327
1328 isFFIDynArgumentTy :: Type -> Bool
1329 -- The argument type of a foreign import dynamic must be Ptr, FunPtr, Addr,
1330 -- or a newtype of either.
1331 isFFIDynArgumentTy = checkRepTyConKey [ptrTyConKey, funPtrTyConKey]
1332
1333 isFFIDynResultTy :: Type -> Bool
1334 -- The result type of a foreign export dynamic must be Ptr, FunPtr, Addr,
1335 -- or a newtype of either.
1336 isFFIDynResultTy = checkRepTyConKey [ptrTyConKey, funPtrTyConKey]
1337
1338 isFFILabelTy :: Type -> Bool
1339 -- The type of a foreign label must be Ptr, FunPtr, Addr,
1340 -- or a newtype of either.
1341 isFFILabelTy = checkRepTyConKey [ptrTyConKey, funPtrTyConKey]
1342
1343 isFFIPrimArgumentTy :: DynFlags -> Type -> Bool
1344 -- Checks for valid argument type for a 'foreign import prim'
1345 -- Currently they must all be simple unlifted types.
1346 isFFIPrimArgumentTy dflags ty
1347    = checkRepTyCon (legalFIPrimArgTyCon dflags) ty
1348
1349 isFFIPrimResultTy :: DynFlags -> Type -> Bool
1350 -- Checks for valid result type for a 'foreign import prim'
1351 -- Currently it must be an unlifted type, including unboxed tuples.
1352 isFFIPrimResultTy dflags ty
1353    = checkRepTyCon (legalFIPrimResultTyCon dflags) ty
1354
1355 isFFIDotnetTy :: DynFlags -> Type -> Bool
1356 isFFIDotnetTy dflags ty
1357   = checkRepTyCon (\ tc -> (legalFIResultTyCon dflags tc || 
1358                            isFFIDotnetObjTy ty || isStringTy ty)) ty
1359         -- NB: isStringTy used to look through newtypes, but
1360         --     it no longer does so.  May need to adjust isFFIDotNetTy
1361         --     if we do want to look through newtypes.
1362
1363 isFFIDotnetObjTy :: Type -> Bool
1364 isFFIDotnetObjTy ty
1365   = checkRepTyCon check_tc t_ty
1366   where
1367    (_, t_ty) = tcSplitForAllTys ty
1368    check_tc tc = getName tc == objectTyConName
1369
1370 isFunPtrTy :: Type -> Bool
1371 isFunPtrTy = checkRepTyConKey [funPtrTyConKey]
1372
1373 -- normaliseFfiType gets run before checkRepTyCon, so we don't
1374 -- need to worry about looking through newtypes or type functions
1375 -- here; that's already been taken care of.
1376 checkRepTyCon :: (TyCon -> Bool) -> Type -> Bool
1377 checkRepTyCon check_tc ty
1378     | Just (tc, _) <- splitTyConApp_maybe ty
1379     = check_tc tc
1380     | otherwise
1381     = False
1382
1383 checkRepTyConKey :: [Unique] -> Type -> Bool
1384 -- Like checkRepTyCon, but just looks at the TyCon key
1385 checkRepTyConKey keys
1386   = checkRepTyCon (\tc -> tyConUnique tc `elem` keys)
1387 \end{code}
1388
1389 ----------------------------------------------
1390 These chaps do the work; they are not exported
1391 ----------------------------------------------
1392
1393 \begin{code}
1394 legalFEArgTyCon :: TyCon -> Bool
1395 legalFEArgTyCon tc
1396   -- It's illegal to make foreign exports that take unboxed
1397   -- arguments.  The RTS API currently can't invoke such things.  --SDM 7/2000
1398   = boxedMarshalableTyCon tc
1399
1400 legalFIResultTyCon :: DynFlags -> TyCon -> Bool
1401 legalFIResultTyCon dflags tc
1402   | tc == unitTyCon         = True
1403   | otherwise               = marshalableTyCon dflags tc
1404
1405 legalFEResultTyCon :: TyCon -> Bool
1406 legalFEResultTyCon tc
1407   | tc == unitTyCon         = True
1408   | otherwise               = boxedMarshalableTyCon tc
1409
1410 legalOutgoingTyCon :: DynFlags -> Safety -> TyCon -> Bool
1411 -- Checks validity of types going from Haskell -> external world
1412 legalOutgoingTyCon dflags _ tc
1413   = marshalableTyCon dflags tc
1414
1415 legalFFITyCon :: TyCon -> Bool
1416 -- True for any TyCon that can possibly be an arg or result of an FFI call
1417 legalFFITyCon tc
1418   = isUnLiftedTyCon tc || boxedMarshalableTyCon tc || tc == unitTyCon
1419
1420 marshalableTyCon :: DynFlags -> TyCon -> Bool
1421 marshalableTyCon dflags tc
1422   =  (xopt Opt_UnliftedFFITypes dflags 
1423       && isUnLiftedTyCon tc
1424       && not (isUnboxedTupleTyCon tc)
1425       && case tyConPrimRep tc of        -- Note [Marshalling VoidRep]
1426            VoidRep -> False
1427            _       -> True)
1428   || boxedMarshalableTyCon tc
1429
1430 boxedMarshalableTyCon :: TyCon -> Bool
1431 boxedMarshalableTyCon tc
1432    = getUnique tc `elem` [ intTyConKey, int8TyConKey, int16TyConKey
1433                          , int32TyConKey, int64TyConKey
1434                          , wordTyConKey, word8TyConKey, word16TyConKey
1435                          , word32TyConKey, word64TyConKey
1436                          , floatTyConKey, doubleTyConKey
1437                          , ptrTyConKey, funPtrTyConKey
1438                          , charTyConKey
1439                          , stablePtrTyConKey
1440                          , boolTyConKey
1441                          ]
1442
1443 legalFIPrimArgTyCon :: DynFlags -> TyCon -> Bool
1444 -- Check args of 'foreign import prim', only allow simple unlifted types.
1445 -- Strictly speaking it is unnecessary to ban unboxed tuples here since
1446 -- currently they're of the wrong kind to use in function args anyway.
1447 legalFIPrimArgTyCon dflags tc
1448   = xopt Opt_UnliftedFFITypes dflags
1449     && isUnLiftedTyCon tc
1450     && not (isUnboxedTupleTyCon tc)
1451
1452 legalFIPrimResultTyCon :: DynFlags -> TyCon -> Bool
1453 -- Check result type of 'foreign import prim'. Allow simple unlifted
1454 -- types and also unboxed tuple result types '... -> (# , , #)'
1455 legalFIPrimResultTyCon dflags tc
1456   = xopt Opt_UnliftedFFITypes dflags
1457     && isUnLiftedTyCon tc
1458     && (isUnboxedTupleTyCon tc
1459         || case tyConPrimRep tc of      -- Note [Marshalling VoidRep]
1460            VoidRep -> False
1461            _       -> True)
1462 \end{code}
1463
1464 Note [Marshalling VoidRep]
1465 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1466 We don't treat State# (whose PrimRep is VoidRep) as marshalable.
1467 In turn that means you can't write
1468         foreign import foo :: Int -> State# RealWorld
1469
1470 Reason: the back end falls over with panic "primRepHint:VoidRep";
1471         and there is no compelling reason to permit it