The final batch of changes for the new coercion representation
[ghc.git] / compiler / types / Type.lhs
1 %
2 % (c) The University of Glasgow 2006
3 % (c) The GRASP/AQUA Project, Glasgow University, 1998
4 %
5
6 Type - public interface
7
8 \begin{code}
9 -- The above warning supression flag is a temporary kludge.
10 -- While working on this module you are encouraged to remove it and fix
11 -- any warnings in the module. See
12 --     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
13 -- for details
14
15 -- | Main functions for manipulating types and type-related things
16 module Type (
17         -- Note some of this is just re-exports from TyCon..
18
19         -- * Main data types representing Types
20         -- $type_classification
21         
22         -- $representation_types
23         TyThing(..), Type, Pred(..), PredType, ThetaType,
24         Var, TyVar, isTyVar, 
25
26         -- ** Constructing and deconstructing types
27         mkTyVarTy, mkTyVarTys, getTyVar, getTyVar_maybe,
28
29         mkAppTy, mkAppTys, splitAppTy, splitAppTys, 
30         splitAppTy_maybe, repSplitAppTy_maybe,
31
32         mkFunTy, mkFunTys, splitFunTy, splitFunTy_maybe, 
33         splitFunTys, splitFunTysN,
34         funResultTy, funArgTy, zipFunTys, 
35
36         mkTyConApp, mkTyConTy, 
37         tyConAppTyCon, tyConAppArgs, 
38         splitTyConApp_maybe, splitTyConApp, 
39
40         mkForAllTy, mkForAllTys, splitForAllTy_maybe, splitForAllTys, 
41         applyTy, applyTys, applyTysD, isForAllTy, dropForAlls,
42         
43         -- (Newtypes)
44         newTyConInstRhs, carefullySplitNewType_maybe,
45         
46         -- (Type families)
47         tyFamInsts, predFamInsts,
48
49         -- Pred types
50         mkPredTy, mkPredTys, mkFamilyTyConApp,
51         mkDictTy, isDictLikeTy, isClassPred,
52         isEqPred, allPred, mkEqPred, 
53         mkClassPred, getClassPredTys, getClassPredTys_maybe,
54         isTyVarClassPred, 
55         mkIPPred, isIPPred,
56
57         -- ** Common type constructors
58         funTyCon,
59
60         -- ** Predicates on types
61         isTyVarTy, isFunTy, isPredTy,
62         isDictTy, isEqPredTy, isReflPredTy, splitPredTy_maybe, splitEqPredTy_maybe, 
63
64         -- (Lifting and boxity)
65         isUnLiftedType, isUnboxedTupleType, isAlgType, isClosedAlgType,
66         isPrimitiveType, isStrictType, isStrictPred, 
67
68         -- * Main data types representing Kinds
69         -- $kind_subtyping
70         Kind, SimpleKind, KindVar,
71         
72         -- ** Common Kinds and SuperKinds
73         liftedTypeKind, unliftedTypeKind, openTypeKind,
74         argTypeKind, ubxTupleKind,
75         tySuperKind, 
76
77         -- ** Common Kind type constructors
78         liftedTypeKindTyCon, openTypeKindTyCon, unliftedTypeKindTyCon,
79         argTypeKindTyCon, ubxTupleKindTyCon,
80
81         -- * Type free variables
82         tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
83         exactTyVarsOfType, exactTyVarsOfTypes, expandTypeSynonyms, 
84         typeSize,
85
86         -- * Type comparison
87         eqType, eqTypeX, eqTypes, cmpType, cmpTypes, 
88         eqPred, eqPredX, cmpPred, eqKind,
89
90         -- * Forcing evaluation of types
91         seqType, seqTypes, seqPred,
92
93         -- * Other views onto Types
94         coreView, tcView, 
95
96         repType, 
97
98         -- * Type representation for the code generator
99         PrimRep(..),
100
101         typePrimRep, predTypeRep,
102
103         -- * Main type substitution data types
104         TvSubstEnv,     -- Representation widely visible
105         TvSubst(..),    -- Representation visible to a few friends
106         
107         -- ** Manipulating type substitutions
108         emptyTvSubstEnv, emptyTvSubst,
109         
110         mkTvSubst, mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst, mkTopTvSubst, notElemTvSubst,
111         getTvSubstEnv, setTvSubstEnv,
112         zapTvSubstEnv, getTvInScope,
113         extendTvInScope, extendTvInScopeList,
114         extendTvSubst, extendTvSubstList,
115         isInScope, composeTvSubst, zipTyEnv,
116         isEmptyTvSubst, unionTvSubst,
117
118         -- ** Performing substitution on types
119         substTy, substTys, substTyWith, substTysWith, substTheta, 
120         substPred, substTyVar, substTyVars, substTyVarBndr,
121         deShadowTy, lookupTyVar, 
122
123         -- * Pretty-printing
124         pprType, pprParendType, pprTypeApp, pprTyThingCategory, pprTyThing, pprForAll,
125         pprPred, pprPredTy, pprEqPred, pprTheta, pprThetaArrowTy, pprClassPred, 
126         pprKind, pprParendKind,
127         
128         pprSourceTyCon
129     ) where
130
131 #include "HsVersions.h"
132
133 -- We import the representation and primitive functions from TypeRep.
134 -- Many things are reexported, but not the representation!
135
136 import TypeRep
137
138 -- friends:
139 import Var
140 import VarEnv
141 import VarSet
142
143 import Class
144 import TyCon
145 import TysPrim
146
147 -- others
148 import BasicTypes       ( IPName )
149 import Name             ( Name )
150 import StaticFlags
151 import Util
152 import Outputable
153 import FastString
154
155 import Data.Maybe       ( isJust )
156
157 infixr 3 `mkFunTy`      -- Associates to the right
158 \end{code}
159
160 \begin{code}
161 -- $type_classification
162 -- #type_classification#
163 -- 
164 -- Types are one of:
165 -- 
166 -- [Unboxed]            Iff its representation is other than a pointer
167 --                      Unboxed types are also unlifted.
168 -- 
169 -- [Lifted]             Iff it has bottom as an element.
170 --                      Closures always have lifted types: i.e. any
171 --                      let-bound identifier in Core must have a lifted
172 --                      type. Operationally, a lifted object is one that
173 --                      can be entered.
174 --                      Only lifted types may be unified with a type variable.
175 -- 
176 -- [Algebraic]          Iff it is a type with one or more constructors, whether
177 --                      declared with @data@ or @newtype@.
178 --                      An algebraic type is one that can be deconstructed
179 --                      with a case expression. This is /not/ the same as 
180 --                      lifted types, because we also include unboxed
181 --                      tuples in this classification.
182 -- 
183 -- [Data]               Iff it is a type declared with @data@, or a boxed tuple.
184 -- 
185 -- [Primitive]          Iff it is a built-in type that can't be expressed in Haskell.
186 -- 
187 -- Currently, all primitive types are unlifted, but that's not necessarily
188 -- the case: for example, @Int@ could be primitive.
189 -- 
190 -- Some primitive types are unboxed, such as @Int#@, whereas some are boxed
191 -- but unlifted (such as @ByteArray#@).  The only primitive types that we
192 -- classify as algebraic are the unboxed tuples.
193 -- 
194 -- Some examples of type classifications that may make this a bit clearer are:
195 -- 
196 -- @
197 -- Type         primitive       boxed           lifted          algebraic
198 -- -----------------------------------------------------------------------------
199 -- Int#         Yes             No              No              No
200 -- ByteArray#   Yes             Yes             No              No
201 -- (\# a, b \#)   Yes             No              No              Yes
202 -- (  a, b  )   No              Yes             Yes             Yes
203 -- [a]          No              Yes             Yes             Yes
204 -- @
205
206 -- $representation_types
207 -- A /source type/ is a type that is a separate type as far as the type checker is
208 -- concerned, but which has a more low-level representation as far as Core-to-Core
209 -- passes and the rest of the back end is concerned. Notably, 'PredTy's are removed
210 -- from the representation type while they do exist in the source types.
211 --
212 -- You don't normally have to worry about this, as the utility functions in
213 -- this module will automatically convert a source into a representation type
214 -- if they are spotted, to the best of it's abilities. If you don't want this
215 -- to happen, use the equivalent functions from the "TcType" module.
216 \end{code}
217
218 %************************************************************************
219 %*                                                                      *
220                 Type representation
221 %*                                                                      *
222 %************************************************************************
223
224 \begin{code}
225 {-# INLINE coreView #-}
226 coreView :: Type -> Maybe Type
227 -- ^ In Core, we \"look through\" non-recursive newtypes and 'PredTypes': this
228 -- function tries to obtain a different view of the supplied type given this
229 --
230 -- Strips off the /top layer only/ of a type to give 
231 -- its underlying representation type. 
232 -- Returns Nothing if there is nothing to look through.
233 --
234 -- By being non-recursive and inlined, this case analysis gets efficiently
235 -- joined onto the case analysis that the caller is already doing
236 coreView (PredTy p)        = Just (predTypeRep p)
237 coreView (TyConApp tc tys) | Just (tenv, rhs, tys') <- coreExpandTyCon_maybe tc tys 
238                            = Just (mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys')
239                                 -- Its important to use mkAppTys, rather than (foldl AppTy),
240                                 -- because the function part might well return a 
241                                 -- partially-applied type constructor; indeed, usually will!
242 coreView _                 = Nothing
243
244
245 -----------------------------------------------
246 {-# INLINE tcView #-}
247 tcView :: Type -> Maybe Type
248 -- ^ Similar to 'coreView', but for the type checker, which just looks through synonyms
249 tcView (TyConApp tc tys) | Just (tenv, rhs, tys') <- tcExpandTyCon_maybe tc tys 
250                          = Just (mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys')
251 tcView _                 = Nothing
252
253 -----------------------------------------------
254 expandTypeSynonyms :: Type -> Type
255 -- ^ Expand out all type synonyms.  Actually, it'd suffice to expand out
256 -- just the ones that discard type variables (e.g.  type Funny a = Int)
257 -- But we don't know which those are currently, so we just expand all.
258 expandTypeSynonyms ty 
259   = go ty
260   where
261     go (TyConApp tc tys)
262       | Just (tenv, rhs, tys') <- tcExpandTyCon_maybe tc tys 
263       = go (mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys')
264       | otherwise
265       = TyConApp tc (map go tys)
266     go (TyVarTy tv)    = TyVarTy tv
267     go (AppTy t1 t2)   = AppTy (go t1) (go t2)
268     go (FunTy t1 t2)   = FunTy (go t1) (go t2)
269     go (ForAllTy tv t) = ForAllTy tv (go t)
270     go (PredTy p)      = PredTy (go_pred p)
271
272     go_pred (ClassP c ts)  = ClassP c (map go ts)
273     go_pred (IParam ip t)  = IParam ip (go t)
274     go_pred (EqPred t1 t2) = EqPred (go t1) (go t2)
275 \end{code}
276
277
278 %************************************************************************
279 %*                                                                      *
280 \subsection{Constructor-specific functions}
281 %*                                                                      *
282 %************************************************************************
283
284
285 ---------------------------------------------------------------------
286                                 TyVarTy
287                                 ~~~~~~~
288 \begin{code}
289 -- | Attempts to obtain the type variable underlying a 'Type', and panics with the
290 -- given message if this is not a type variable type. See also 'getTyVar_maybe'
291 getTyVar :: String -> Type -> TyVar
292 getTyVar msg ty = case getTyVar_maybe ty of
293                     Just tv -> tv
294                     Nothing -> panic ("getTyVar: " ++ msg)
295
296 isTyVarTy :: Type -> Bool
297 isTyVarTy ty = isJust (getTyVar_maybe ty)
298
299 -- | Attempts to obtain the type variable underlying a 'Type'
300 getTyVar_maybe :: Type -> Maybe TyVar
301 getTyVar_maybe ty | Just ty' <- coreView ty = getTyVar_maybe ty'
302 getTyVar_maybe (TyVarTy tv)                 = Just tv  
303 getTyVar_maybe _                            = Nothing
304
305 \end{code}
306
307
308 ---------------------------------------------------------------------
309                                 AppTy
310                                 ~~~~~
311 We need to be pretty careful with AppTy to make sure we obey the 
312 invariant that a TyConApp is always visibly so.  mkAppTy maintains the
313 invariant: use it.
314
315 \begin{code}
316 -- | Applies a type to another, as in e.g. @k a@
317 mkAppTy :: Type -> Type -> Type
318 mkAppTy orig_ty1 orig_ty2
319   = mk_app orig_ty1
320   where
321     mk_app (TyConApp tc tys) = mkTyConApp tc (tys ++ [orig_ty2])
322     mk_app _                 = AppTy orig_ty1 orig_ty2
323         -- Note that the TyConApp could be an 
324         -- under-saturated type synonym.  GHC allows that; e.g.
325         --      type Foo k = k a -> k a
326         --      type Id x = x
327         --      foo :: Foo Id -> Foo Id
328         --
329         -- Here Id is partially applied in the type sig for Foo,
330         -- but once the type synonyms are expanded all is well
331
332 mkAppTys :: Type -> [Type] -> Type
333 mkAppTys orig_ty1 []        = orig_ty1
334         -- This check for an empty list of type arguments
335         -- avoids the needless loss of a type synonym constructor.
336         -- For example: mkAppTys Rational []
337         --   returns to (Ratio Integer), which has needlessly lost
338         --   the Rational part.
339 mkAppTys orig_ty1 orig_tys2
340   = mk_app orig_ty1
341   where
342     mk_app (TyConApp tc tys) = mkTyConApp tc (tys ++ orig_tys2)
343                                 -- mkTyConApp: see notes with mkAppTy
344     mk_app _                 = foldl AppTy orig_ty1 orig_tys2
345
346 -------------
347 splitAppTy_maybe :: Type -> Maybe (Type, Type)
348 -- ^ Attempt to take a type application apart, whether it is a
349 -- function, type constructor, or plain type application. Note
350 -- that type family applications are NEVER unsaturated by this!
351 splitAppTy_maybe ty | Just ty' <- coreView ty
352                     = splitAppTy_maybe ty'
353 splitAppTy_maybe ty = repSplitAppTy_maybe ty
354
355 -------------
356 repSplitAppTy_maybe :: Type -> Maybe (Type,Type)
357 -- ^ Does the AppTy split as in 'splitAppTy_maybe', but assumes that 
358 -- any Core view stuff is already done
359 repSplitAppTy_maybe (FunTy ty1 ty2)   = Just (TyConApp funTyCon [ty1], ty2)
360 repSplitAppTy_maybe (AppTy ty1 ty2)   = Just (ty1, ty2)
361 repSplitAppTy_maybe (TyConApp tc tys) 
362   | isDecomposableTyCon tc || tys `lengthExceeds` tyConArity tc 
363   , Just (tys', ty') <- snocView tys
364   = Just (TyConApp tc tys', ty')    -- Never create unsaturated type family apps!
365 repSplitAppTy_maybe _other = Nothing
366 -------------
367 splitAppTy :: Type -> (Type, Type)
368 -- ^ Attempts to take a type application apart, as in 'splitAppTy_maybe',
369 -- and panics if this is not possible
370 splitAppTy ty = case splitAppTy_maybe ty of
371                         Just pr -> pr
372                         Nothing -> panic "splitAppTy"
373
374 -------------
375 splitAppTys :: Type -> (Type, [Type])
376 -- ^ Recursively splits a type as far as is possible, leaving a residual
377 -- type being applied to and the type arguments applied to it. Never fails,
378 -- even if that means returning an empty list of type applications.
379 splitAppTys ty = split ty ty []
380   where
381     split orig_ty ty args | Just ty' <- coreView ty = split orig_ty ty' args
382     split _       (AppTy ty arg)        args = split ty ty (arg:args)
383     split _       (TyConApp tc tc_args) args
384       = let -- keep type families saturated
385             n | isDecomposableTyCon tc = 0
386               | otherwise              = tyConArity tc
387             (tc_args1, tc_args2) = splitAt n tc_args
388         in
389         (TyConApp tc tc_args1, tc_args2 ++ args)
390     split _       (FunTy ty1 ty2)       args = ASSERT( null args )
391                                                (TyConApp funTyCon [], [ty1,ty2])
392     split orig_ty _                     args = (orig_ty, args)
393
394 \end{code}
395
396
397 ---------------------------------------------------------------------
398                                 FunTy
399                                 ~~~~~
400
401 \begin{code}
402 mkFunTy :: Type -> Type -> Type
403 -- ^ Creates a function type from the given argument and result type
404 mkFunTy arg res = FunTy arg res
405
406 mkFunTys :: [Type] -> Type -> Type
407 mkFunTys tys ty = foldr mkFunTy ty tys
408
409 isFunTy :: Type -> Bool 
410 isFunTy ty = isJust (splitFunTy_maybe ty)
411
412 splitFunTy :: Type -> (Type, Type)
413 -- ^ Attempts to extract the argument and result types from a type, and
414 -- panics if that is not possible. See also 'splitFunTy_maybe'
415 splitFunTy ty | Just ty' <- coreView ty = splitFunTy ty'
416 splitFunTy (FunTy arg res)   = (arg, res)
417 splitFunTy other             = pprPanic "splitFunTy" (ppr other)
418
419 splitFunTy_maybe :: Type -> Maybe (Type, Type)
420 -- ^ Attempts to extract the argument and result types from a type
421 splitFunTy_maybe ty | Just ty' <- coreView ty = splitFunTy_maybe ty'
422 splitFunTy_maybe (FunTy arg res)   = Just (arg, res)
423 splitFunTy_maybe _                 = Nothing
424
425 splitFunTys :: Type -> ([Type], Type)
426 splitFunTys ty = split [] ty ty
427   where
428     split args orig_ty ty | Just ty' <- coreView ty = split args orig_ty ty'
429     split args _       (FunTy arg res)   = split (arg:args) res res
430     split args orig_ty _                 = (reverse args, orig_ty)
431
432 splitFunTysN :: Int -> Type -> ([Type], Type)
433 -- ^ Split off exactly the given number argument types, and panics if that is not possible
434 splitFunTysN 0 ty = ([], ty)
435 splitFunTysN n ty = ASSERT2( isFunTy ty, int n <+> ppr ty )
436                     case splitFunTy ty of { (arg, res) ->
437                     case splitFunTysN (n-1) res of { (args, res) ->
438                     (arg:args, res) }}
439
440 -- | Splits off argument types from the given type and associating
441 -- them with the things in the input list from left to right. The
442 -- final result type is returned, along with the resulting pairs of
443 -- objects and types, albeit with the list of pairs in reverse order.
444 -- Panics if there are not enough argument types for the input list.
445 zipFunTys :: Outputable a => [a] -> Type -> ([(a, Type)], Type)
446 zipFunTys orig_xs orig_ty = split [] orig_xs orig_ty orig_ty
447   where
448     split acc []     nty _                 = (reverse acc, nty)
449     split acc xs     nty ty 
450           | Just ty' <- coreView ty        = split acc xs nty ty'
451     split acc (x:xs) _   (FunTy arg res)   = split ((x,arg):acc) xs res res
452     split _   _      _   _                 = pprPanic "zipFunTys" (ppr orig_xs <+> ppr orig_ty)
453     
454 funResultTy :: Type -> Type
455 -- ^ Extract the function result type and panic if that is not possible
456 funResultTy ty | Just ty' <- coreView ty = funResultTy ty'
457 funResultTy (FunTy _arg res)  = res
458 funResultTy ty                = pprPanic "funResultTy" (ppr ty)
459
460 funArgTy :: Type -> Type
461 -- ^ Extract the function argument type and panic if that is not possible
462 funArgTy ty | Just ty' <- coreView ty = funArgTy ty'
463 funArgTy (FunTy arg _res)  = arg
464 funArgTy ty                = pprPanic "funArgTy" (ppr ty)
465 \end{code}
466
467 ---------------------------------------------------------------------
468                                 TyConApp
469                                 ~~~~~~~~
470
471 \begin{code}
472 -- splitTyConApp "looks through" synonyms, because they don't
473 -- mean a distinct type, but all other type-constructor applications
474 -- including functions are returned as Just ..
475
476 -- | The same as @fst . splitTyConApp@
477 tyConAppTyCon :: Type -> TyCon
478 tyConAppTyCon ty = fst (splitTyConApp ty)
479
480 -- | The same as @snd . splitTyConApp@
481 tyConAppArgs :: Type -> [Type]
482 tyConAppArgs ty = snd (splitTyConApp ty)
483
484 -- | Attempts to tease a type apart into a type constructor and the application
485 -- of a number of arguments to that constructor. Panics if that is not possible.
486 -- See also 'splitTyConApp_maybe'
487 splitTyConApp :: Type -> (TyCon, [Type])
488 splitTyConApp ty = case splitTyConApp_maybe ty of
489                         Just stuff -> stuff
490                         Nothing    -> pprPanic "splitTyConApp" (ppr ty)
491
492 -- | Attempts to tease a type apart into a type constructor and the application
493 -- of a number of arguments to that constructor
494 splitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
495 splitTyConApp_maybe ty | Just ty' <- coreView ty = splitTyConApp_maybe ty'
496 splitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
497 splitTyConApp_maybe (FunTy arg res)   = Just (funTyCon, [arg,res])
498 splitTyConApp_maybe _                 = Nothing
499
500 newTyConInstRhs :: TyCon -> [Type] -> Type
501 -- ^ Unwrap one 'layer' of newtype on a type constructor and its arguments, using an 
502 -- eta-reduced version of the @newtype@ if possible
503 newTyConInstRhs tycon tys 
504     = ASSERT2( equalLength tvs tys1, ppr tycon $$ ppr tys $$ ppr tvs )
505       mkAppTys (substTyWith tvs tys1 ty) tys2
506   where
507     (tvs, ty)    = newTyConEtadRhs tycon
508     (tys1, tys2) = splitAtList tvs tys
509 \end{code}
510
511
512 ---------------------------------------------------------------------
513                                 SynTy
514                                 ~~~~~
515
516 Notes on type synonyms
517 ~~~~~~~~~~~~~~~~~~~~~~
518 The various "split" functions (splitFunTy, splitRhoTy, splitForAllTy) try
519 to return type synonyms whereever possible. Thus
520
521         type Foo a = a -> a
522
523 we want 
524         splitFunTys (a -> Foo a) = ([a], Foo a)
525 not                                ([a], a -> a)
526
527 The reason is that we then get better (shorter) type signatures in 
528 interfaces.  Notably this plays a role in tcTySigs in TcBinds.lhs.
529
530
531 Note [Expanding newtypes]
532 ~~~~~~~~~~~~~~~~~~~~~~~~~
533 When expanding a type to expose a data-type constructor, we need to be
534 careful about newtypes, lest we fall into an infinite loop. Here are
535 the key examples:
536
537   newtype Id  x = MkId x
538   newtype Fix f = MkFix (f (Fix f))
539   newtype T     = MkT (T -> T) 
540   
541   Type           Expansion
542  --------------------------
543   T              T -> T
544   Fix Maybe      Maybe (Fix Maybe)
545   Id (Id Int)    Int
546   Fix Id         NO NO NO
547
548 Notice that we can expand T, even though it's recursive.
549 And we can expand Id (Id Int), even though the Id shows up
550 twice at the outer level.  
551
552 So, when expanding, we keep track of when we've seen a recursive
553 newtype at outermost level; and bale out if we see it again.
554
555
556                 Representation types
557                 ~~~~~~~~~~~~~~~~~~~~
558
559 \begin{code}
560 -- | Looks through:
561 --
562 --      1. For-alls
563 --      2. Synonyms
564 --      3. Predicates
565 --      4. All newtypes, including recursive ones, but not newtype families
566 --
567 -- It's useful in the back end of the compiler.
568 repType :: Type -> Type
569 -- Only applied to types of kind *; hence tycons are saturated
570 repType ty
571   = go [] ty
572   where
573     go :: [TyCon] -> Type -> Type
574     go rec_nts (ForAllTy _ ty)          -- Look through foralls
575         = go rec_nts ty
576
577     go rec_nts (PredTy p)               -- Expand predicates
578         = go rec_nts (predTypeRep p)
579
580     go rec_nts (TyConApp tc tys)        -- Expand newtypes and synonyms
581       | Just (tenv, rhs, tys') <- coreExpandTyCon_maybe tc tys 
582       = go rec_nts (mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys')
583
584       | Just (rec_nts', ty') <- carefullySplitNewType_maybe rec_nts tc tys
585       = go rec_nts' ty'
586
587     go _ ty = ty
588
589
590 carefullySplitNewType_maybe :: [TyCon] -> TyCon -> [Type] -> Maybe ([TyCon],Type)
591 -- Return the representation of a newtype, unless 
592 -- we've seen it already: see Note [Expanding newtypes]
593 carefullySplitNewType_maybe rec_nts tc tys
594   | isNewTyCon tc
595   , not (tc `elem` rec_nts)  = Just (rec_nts', newTyConInstRhs tc tys)
596   | otherwise                = Nothing
597   where
598     rec_nts' | isRecursiveTyCon tc = tc:rec_nts
599              | otherwise           = rec_nts
600
601
602 -- ToDo: this could be moved to the code generator, using splitTyConApp instead
603 -- of inspecting the type directly.
604
605 -- | Discovers the primitive representation of a more abstract 'Type'
606 typePrimRep :: Type -> PrimRep
607 typePrimRep ty = case repType ty of
608                    TyConApp tc _ -> tyConPrimRep tc
609                    FunTy _ _     -> PtrRep
610                    AppTy _ _     -> PtrRep      -- See note below
611                    TyVarTy _     -> PtrRep
612                    _             -> pprPanic "typePrimRep" (ppr ty)
613         -- Types of the form 'f a' must be of kind *, not *#, so
614         -- we are guaranteed that they are represented by pointers.
615         -- The reason is that f must have kind *->*, not *->*#, because
616         -- (we claim) there is no way to constrain f's kind any other
617         -- way.
618 \end{code}
619
620
621 ---------------------------------------------------------------------
622                                 ForAllTy
623                                 ~~~~~~~~
624
625 \begin{code}
626 mkForAllTy :: TyVar -> Type -> Type
627 mkForAllTy tyvar ty
628   = ForAllTy tyvar ty
629
630 -- | Wraps foralls over the type using the provided 'TyVar's from left to right
631 mkForAllTys :: [TyVar] -> Type -> Type
632 mkForAllTys tyvars ty = foldr ForAllTy ty tyvars
633
634 isForAllTy :: Type -> Bool
635 isForAllTy (ForAllTy _ _) = True
636 isForAllTy _              = False
637
638 -- | Attempts to take a forall type apart, returning the bound type variable
639 -- and the remainder of the type
640 splitForAllTy_maybe :: Type -> Maybe (TyVar, Type)
641 splitForAllTy_maybe ty = splitFAT_m ty
642   where
643     splitFAT_m ty | Just ty' <- coreView ty = splitFAT_m ty'
644     splitFAT_m (ForAllTy tyvar ty)          = Just(tyvar, ty)
645     splitFAT_m _                            = Nothing
646
647 -- | Attempts to take a forall type apart, returning all the immediate such bound
648 -- type variables and the remainder of the type. Always suceeds, even if that means
649 -- returning an empty list of 'TyVar's
650 splitForAllTys :: Type -> ([TyVar], Type)
651 splitForAllTys ty = split ty ty []
652    where
653      split orig_ty ty tvs | Just ty' <- coreView ty = split orig_ty ty' tvs
654      split _       (ForAllTy tv ty)  tvs = split ty ty (tv:tvs)
655      split orig_ty _                 tvs = (reverse tvs, orig_ty)
656
657 -- | Equivalent to @snd . splitForAllTys@
658 dropForAlls :: Type -> Type
659 dropForAlls ty = snd (splitForAllTys ty)
660 \end{code}
661
662 -- (mkPiType now in CoreUtils)
663
664 applyTy, applyTys
665 ~~~~~~~~~~~~~~~~~
666
667 \begin{code}
668 -- | Instantiate a forall type with one or more type arguments.
669 -- Used when we have a polymorphic function applied to type args:
670 --
671 -- > f t1 t2
672 --
673 -- We use @applyTys type-of-f [t1,t2]@ to compute the type of the expression.
674 -- Panics if no application is possible.
675 applyTy :: Type -> Type -> Type
676 applyTy ty arg | Just ty' <- coreView ty = applyTy ty' arg
677 applyTy (ForAllTy tv ty) arg = substTyWith [tv] [arg] ty
678 applyTy _                _   = panic "applyTy"
679
680 applyTys :: Type -> [Type] -> Type
681 -- ^ This function is interesting because:
682 --
683 --      1. The function may have more for-alls than there are args
684 --
685 --      2. Less obviously, it may have fewer for-alls
686 --
687 -- For case 2. think of:
688 --
689 -- > applyTys (forall a.a) [forall b.b, Int]
690 --
691 -- This really can happen, via dressing up polymorphic types with newtype
692 -- clothing.  Here's an example:
693 --
694 -- > newtype R = R (forall a. a->a)
695 -- > foo = case undefined :: R of
696 -- >            R f -> f ()
697
698 applyTys ty args = applyTysD empty ty args
699
700 applyTysD :: SDoc -> Type -> [Type] -> Type     -- Debug version
701 applyTysD _   orig_fun_ty []      = orig_fun_ty
702 applyTysD doc orig_fun_ty arg_tys 
703   | n_tvs == n_args     -- The vastly common case
704   = substTyWith tvs arg_tys rho_ty
705   | n_tvs > n_args      -- Too many for-alls
706   = substTyWith (take n_args tvs) arg_tys 
707                 (mkForAllTys (drop n_args tvs) rho_ty)
708   | otherwise           -- Too many type args
709   = ASSERT2( n_tvs > 0, doc $$ ppr orig_fun_ty )        -- Zero case gives infnite loop!
710     applyTysD doc (substTyWith tvs (take n_tvs arg_tys) rho_ty)
711                   (drop n_tvs arg_tys)
712   where
713     (tvs, rho_ty) = splitForAllTys orig_fun_ty 
714     n_tvs = length tvs
715     n_args = length arg_tys     
716 \end{code}
717
718
719 %************************************************************************
720 %*                                                                      *
721                          Pred
722 %*                                                                      *
723 %************************************************************************
724
725 Polymorphic functions over Pred
726
727 \begin{code}
728 allPred :: (a -> Bool) -> Pred a -> Bool
729 allPred p (ClassP _ ts)  = all p ts
730 allPred p (IParam _ t)   = p t
731 allPred p (EqPred t1 t2) = p t1 && p t2
732
733 isClassPred :: Pred a -> Bool
734 isClassPred (ClassP {}) = True
735 isClassPred _            = False
736
737 isEqPred :: Pred a -> Bool
738 isEqPred (EqPred {}) = True
739 isEqPred _           = False
740
741 isIPPred :: Pred a -> Bool
742 isIPPred (IParam {}) = True
743 isIPPred _           = False
744 \end{code}
745
746 Make PredTypes
747
748 \begin{code}
749 mkPredTy :: PredType -> Type
750 mkPredTy pred = PredTy pred
751
752 mkPredTys :: ThetaType -> [Type]
753 mkPredTys preds = map PredTy preds
754
755 predTypeRep :: PredType -> Type
756 -- ^ Convert a 'PredType' to its representation type. However, it unwraps 
757 -- only the outermost level; for example, the result might be a newtype application
758 predTypeRep (IParam _ ty)     = ty
759 predTypeRep (ClassP clas tys) = mkTyConApp (classTyCon clas) tys
760 predTypeRep (EqPred ty1 ty2)  = mkTyConApp eqPredPrimTyCon [ty1,ty2]
761
762 splitPredTy_maybe :: Type -> Maybe PredType
763 -- Returns Just for predicates only
764 splitPredTy_maybe ty | Just ty' <- tcView ty = splitPredTy_maybe ty'
765 splitPredTy_maybe (PredTy p)    = Just p
766 splitPredTy_maybe _             = Nothing
767
768 isPredTy :: Type -> Bool
769 isPredTy ty = isJust (splitPredTy_maybe ty)
770 \end{code}
771
772 --------------------- Equality types ---------------------------------
773 \begin{code}
774 isReflPredTy :: Type -> Bool
775 isReflPredTy ty = case splitPredTy_maybe ty of
776                     Just (EqPred ty1 ty2) -> ty1 `eqType` ty2
777                     _                     -> False
778
779 splitEqPredTy_maybe :: Type -> Maybe (Type,Type)
780 splitEqPredTy_maybe ty = case splitPredTy_maybe ty of
781                             Just (EqPred ty1 ty2) -> Just (ty1,ty2)
782                             _                     -> Nothing
783
784 isEqPredTy :: Type -> Bool
785 isEqPredTy ty = case splitPredTy_maybe ty of
786                   Just (EqPred {}) -> True
787                   _                -> False
788
789 -- | Creates a type equality predicate
790 mkEqPred :: (a, a) -> Pred a
791 mkEqPred (ty1, ty2) = EqPred ty1 ty2
792 \end{code}
793
794 --------------------- Dictionary types ---------------------------------
795 \begin{code}
796 mkClassPred :: Class -> [Type] -> PredType
797 mkClassPred clas tys = ClassP clas tys
798
799 isDictTy :: Type -> Bool
800 isDictTy ty = case splitPredTy_maybe ty of
801                 Just p  -> isClassPred p
802                 Nothing -> False
803
804 isTyVarClassPred :: PredType -> Bool
805 isTyVarClassPred (ClassP _ tys) = all isTyVarTy tys
806 isTyVarClassPred _              = False
807
808 getClassPredTys_maybe :: PredType -> Maybe (Class, [Type])
809 getClassPredTys_maybe (ClassP clas tys) = Just (clas, tys)
810 getClassPredTys_maybe _                 = Nothing
811
812 getClassPredTys :: PredType -> (Class, [Type])
813 getClassPredTys (ClassP clas tys) = (clas, tys)
814 getClassPredTys _ = panic "getClassPredTys"
815
816 mkDictTy :: Class -> [Type] -> Type
817 mkDictTy clas tys = mkPredTy (ClassP clas tys)
818
819 isDictLikeTy :: Type -> Bool
820 -- Note [Dictionary-like types]
821 isDictLikeTy ty | Just ty' <- tcView ty = isDictTy ty'
822 isDictLikeTy (PredTy p) = isClassPred p
823 isDictLikeTy (TyConApp tc tys) 
824   | isTupleTyCon tc     = all isDictLikeTy tys
825 isDictLikeTy _          = False
826 \end{code}
827
828 Note [Dictionary-like types]
829 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
830 Being "dictionary-like" means either a dictionary type or a tuple thereof.
831 In GHC 6.10 we build implication constraints which construct such tuples,
832 and if we land up with a binding
833     t :: (C [a], Eq [a])
834     t = blah
835 then we want to treat t as cheap under "-fdicts-cheap" for example.
836 (Implication constraints are normally inlined, but sadly not if the
837 occurrence is itself inside an INLINE function!  Until we revise the 
838 handling of implication constraints, that is.)  This turned out to
839 be important in getting good arities in DPH code.  Example:
840
841     class C a
842     class D a where { foo :: a -> a }
843     instance C a => D (Maybe a) where { foo x = x }
844
845     bar :: (C a, C b) => a -> b -> (Maybe a, Maybe b)
846     {-# INLINE bar #-}
847     bar x y = (foo (Just x), foo (Just y))
848
849 Then 'bar' should jolly well have arity 4 (two dicts, two args), but
850 we ended up with something like
851    bar = __inline_me__ (\d1,d2. let t :: (D (Maybe a), D (Maybe b)) = ...
852                                 in \x,y. <blah>)
853
854 This is all a bit ad-hoc; eg it relies on knowing that implication
855 constraints build tuples.
856
857 --------------------- Implicit parameters ---------------------------------
858
859 \begin{code}
860 mkIPPred :: IPName Name -> Type -> PredType
861 mkIPPred ip ty = IParam ip ty
862 \end{code}
863
864 %************************************************************************
865 %*                                                                      *
866                    Size                                                                 
867 %*                                                                      *
868 %************************************************************************
869
870 \begin{code}
871 typeSize :: Type -> Int
872 typeSize (TyVarTy _)     = 1
873 typeSize (AppTy t1 t2)   = typeSize t1 + typeSize t2
874 typeSize (FunTy t1 t2)   = typeSize t1 + typeSize t2
875 typeSize (PredTy p)      = predSize typeSize p
876 typeSize (ForAllTy _ t)  = 1 + typeSize t
877 typeSize (TyConApp _ ts) = 1 + sum (map typeSize ts)
878 \end{code}
879
880
881 %************************************************************************
882 %*                                                                      *
883 \subsection{Type families}
884 %*                                                                      *
885 %************************************************************************
886
887 \begin{code}
888 -- | Finds type family instances occuring in a type after expanding synonyms.
889 tyFamInsts :: Type -> [(TyCon, [Type])]
890 tyFamInsts ty 
891   | Just exp_ty <- tcView ty    = tyFamInsts exp_ty
892 tyFamInsts (TyVarTy _)          = []
893 tyFamInsts (TyConApp tc tys) 
894   | isSynFamilyTyCon tc           = [(tc, tys)]
895   | otherwise                   = concat (map tyFamInsts tys)
896 tyFamInsts (FunTy ty1 ty2)      = tyFamInsts ty1 ++ tyFamInsts ty2
897 tyFamInsts (AppTy ty1 ty2)      = tyFamInsts ty1 ++ tyFamInsts ty2
898 tyFamInsts (ForAllTy _ ty)      = tyFamInsts ty
899 tyFamInsts (PredTy pty)         = predFamInsts pty
900
901 -- | Finds type family instances occuring in a predicate type after expanding 
902 -- synonyms.
903 predFamInsts :: PredType -> [(TyCon, [Type])]
904 predFamInsts (ClassP _cla tys) = concat (map tyFamInsts tys)
905 predFamInsts (IParam _ ty)     = tyFamInsts ty
906 predFamInsts (EqPred ty1 ty2)  = tyFamInsts ty1 ++ tyFamInsts ty2
907
908 mkFamilyTyConApp :: TyCon -> [Type] -> Type
909 -- ^ Given a family instance TyCon and its arg types, return the
910 -- corresponding family type.  E.g:
911 --
912 -- > data family T a
913 -- > data instance T (Maybe b) = MkT b
914 --
915 -- Where the instance tycon is :RTL, so:
916 --
917 -- > mkFamilyTyConApp :RTL Int  =  T (Maybe Int)
918 mkFamilyTyConApp tc tys
919   | Just (fam_tc, fam_tys) <- tyConFamInst_maybe tc
920   , let fam_subst = zipTopTvSubst (tyConTyVars tc) tys
921   = mkTyConApp fam_tc (substTys fam_subst fam_tys)
922   | otherwise
923   = mkTyConApp tc tys
924
925 -- | Pretty prints a 'TyCon', using the family instance in case of a
926 -- representation tycon.  For example:
927 --
928 -- > data T [a] = ...
929 --
930 -- In that case we want to print @T [a]@, where @T@ is the family 'TyCon'
931 pprSourceTyCon :: TyCon -> SDoc
932 pprSourceTyCon tycon 
933   | Just (fam_tc, tys) <- tyConFamInst_maybe tycon
934   = ppr $ fam_tc `TyConApp` tys        -- can't be FunTyCon
935   | otherwise
936   = ppr tycon
937 \end{code}
938
939 %************************************************************************
940 %*                                                                      *
941 \subsection{Liftedness}
942 %*                                                                      *
943 %************************************************************************
944
945 \begin{code}
946 -- | See "Type#type_classification" for what an unlifted type is
947 isUnLiftedType :: Type -> Bool
948         -- isUnLiftedType returns True for forall'd unlifted types:
949         --      x :: forall a. Int#
950         -- I found bindings like these were getting floated to the top level.
951         -- They are pretty bogus types, mind you.  It would be better never to
952         -- construct them
953
954 isUnLiftedType ty | Just ty' <- coreView ty = isUnLiftedType ty'
955 isUnLiftedType (ForAllTy _ ty)   = isUnLiftedType ty
956 isUnLiftedType (PredTy p)        = isEqPred p
957 isUnLiftedType (TyConApp tc _)   = isUnLiftedTyCon tc
958 isUnLiftedType _                 = False
959
960 isUnboxedTupleType :: Type -> Bool
961 isUnboxedTupleType ty = case splitTyConApp_maybe ty of
962                            Just (tc, _ty_args) -> isUnboxedTupleTyCon tc
963                            _                   -> False
964
965 -- | See "Type#type_classification" for what an algebraic type is.
966 -- Should only be applied to /types/, as opposed to e.g. partially
967 -- saturated type constructors
968 isAlgType :: Type -> Bool
969 isAlgType ty 
970   = case splitTyConApp_maybe ty of
971       Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
972                             isAlgTyCon tc
973       _other             -> False
974
975 -- | See "Type#type_classification" for what an algebraic type is.
976 -- Should only be applied to /types/, as opposed to e.g. partially
977 -- saturated type constructors. Closed type constructors are those
978 -- with a fixed right hand side, as opposed to e.g. associated types
979 isClosedAlgType :: Type -> Bool
980 isClosedAlgType ty
981   = case splitTyConApp_maybe ty of
982       Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
983                             isAlgTyCon tc && not (isFamilyTyCon tc)
984       _other             -> False
985 \end{code}
986
987 \begin{code}
988 -- | Computes whether an argument (or let right hand side) should
989 -- be computed strictly or lazily, based only on its type.
990 -- Works just like 'isUnLiftedType', except that it has a special case 
991 -- for dictionaries (i.e. does not work purely on representation types)
992
993 -- Since it takes account of class 'PredType's, you might think
994 -- this function should be in 'TcType', but 'isStrictType' is used by 'DataCon',
995 -- which is below 'TcType' in the hierarchy, so it's convenient to put it here.
996 isStrictType :: Type -> Bool
997 isStrictType (PredTy pred)     = isStrictPred pred
998 isStrictType ty | Just ty' <- coreView ty = isStrictType ty'
999 isStrictType (ForAllTy _ ty)   = isStrictType ty
1000 isStrictType (TyConApp tc _)   = isUnLiftedTyCon tc
1001 isStrictType _                 = False
1002
1003 -- | We may be strict in dictionary types, but only if it 
1004 -- has more than one component.
1005 --
1006 -- (Being strict in a single-component dictionary risks
1007 --  poking the dictionary component, which is wrong.)
1008 isStrictPred :: PredType -> Bool
1009 isStrictPred (ClassP clas _) = opt_DictsStrict && not (isNewTyCon (classTyCon clas))
1010 isStrictPred (EqPred {})     = True
1011 isStrictPred (IParam {})     = False
1012 \end{code}
1013
1014 \begin{code}
1015 isPrimitiveType :: Type -> Bool
1016 -- ^ Returns true of types that are opaque to Haskell.
1017 -- Most of these are unlifted, but now that we interact with .NET, we
1018 -- may have primtive (foreign-imported) types that are lifted
1019 isPrimitiveType ty = case splitTyConApp_maybe ty of
1020                         Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
1021                                               isPrimTyCon tc
1022                         _                  -> False
1023 \end{code}
1024
1025
1026 %************************************************************************
1027 %*                                                                      *
1028           The "exact" free variables of a type
1029 %*                                                                      *
1030 %************************************************************************
1031
1032 Note [Silly type synonym]
1033 ~~~~~~~~~~~~~~~~~~~~~~~~~
1034 Consider
1035         type T a = Int
1036 What are the free tyvars of (T x)?  Empty, of course!  
1037 Here's the example that Ralf Laemmel showed me:
1038         foo :: (forall a. C u a -> C u a) -> u
1039         mappend :: Monoid u => u -> u -> u
1040
1041         bar :: Monoid u => u
1042         bar = foo (\t -> t `mappend` t)
1043 We have to generalise at the arg to f, and we don't
1044 want to capture the constraint (Monad (C u a)) because
1045 it appears to mention a.  Pretty silly, but it was useful to him.
1046
1047 exactTyVarsOfType is used by the type checker to figure out exactly
1048 which type variables are mentioned in a type.  It's also used in the
1049 smart-app checking code --- see TcExpr.tcIdApp
1050
1051 On the other hand, consider a *top-level* definition
1052         f = (\x -> x) :: T a -> T a
1053 If we don't abstract over 'a' it'll get fixed to GHC.Prim.Any, and then
1054 if we have an application like (f "x") we get a confusing error message 
1055 involving Any.  So the conclusion is this: when generalising
1056   - at top level use tyVarsOfType
1057   - in nested bindings use exactTyVarsOfType
1058 See Trac #1813 for example.
1059
1060 \begin{code}
1061 exactTyVarsOfType :: Type -> TyVarSet
1062 -- Find the free type variables (of any kind)
1063 -- but *expand* type synonyms.  See Note [Silly type synonym] above.
1064 exactTyVarsOfType ty
1065   = go ty
1066   where
1067     go ty | Just ty' <- tcView ty = go ty'      -- This is the key line
1068     go (TyVarTy tv)         = unitVarSet tv
1069     go (TyConApp _ tys)     = exactTyVarsOfTypes tys
1070     go (PredTy ty)          = go_pred ty
1071     go (FunTy arg res)      = go arg `unionVarSet` go res
1072     go (AppTy fun arg)      = go fun `unionVarSet` go arg
1073     go (ForAllTy tyvar ty)  = delVarSet (go ty) tyvar
1074
1075     go_pred (IParam _ ty)    = go ty
1076     go_pred (ClassP _ tys)   = exactTyVarsOfTypes tys
1077     go_pred (EqPred ty1 ty2) = go ty1 `unionVarSet` go ty2
1078
1079 exactTyVarsOfTypes :: [Type] -> TyVarSet
1080 exactTyVarsOfTypes tys = foldr (unionVarSet . exactTyVarsOfType) emptyVarSet tys
1081 \end{code}
1082
1083
1084 %************************************************************************
1085 %*                                                                      *
1086 \subsection{Sequencing on types}
1087 %*                                                                      *
1088 %************************************************************************
1089
1090 \begin{code}
1091 seqType :: Type -> ()
1092 seqType (TyVarTy tv)      = tv `seq` ()
1093 seqType (AppTy t1 t2)     = seqType t1 `seq` seqType t2
1094 seqType (FunTy t1 t2)     = seqType t1 `seq` seqType t2
1095 seqType (PredTy p)        = seqPred seqType p
1096 seqType (TyConApp tc tys) = tc `seq` seqTypes tys
1097 seqType (ForAllTy tv ty)  = tv `seq` seqType ty
1098
1099 seqTypes :: [Type] -> ()
1100 seqTypes []       = ()
1101 seqTypes (ty:tys) = seqType ty `seq` seqTypes tys
1102
1103 seqPred :: (a -> ()) -> Pred a -> ()
1104 seqPred seqt (ClassP c tys)   = c `seq` foldr (seq . seqt) () tys
1105 seqPred seqt (IParam n ty)    = n `seq` seqt ty
1106 seqPred seqt (EqPred ty1 ty2) = seqt ty1 `seq` seqt ty2
1107 \end{code}
1108
1109
1110 %************************************************************************
1111 %*                                                                      *
1112                 Comparision for types 
1113         (We don't use instances so that we know where it happens)
1114 %*                                                                      *
1115 %************************************************************************
1116
1117 \begin{code}
1118 eqKind :: Kind -> Kind -> Bool
1119 eqKind = eqType
1120
1121 eqType :: Type -> Type -> Bool
1122 -- ^ Type equality on source types. Does not look through @newtypes@ or 
1123 -- 'PredType's, but it does look through type synonyms.
1124 eqType t1 t2 = isEqual $ cmpType t1 t2
1125
1126 eqTypeX :: RnEnv2 -> Type -> Type -> Bool
1127 eqTypeX env t1 t2 = isEqual $ cmpTypeX env t1 t2
1128
1129 eqTypes :: [Type] -> [Type] -> Bool
1130 eqTypes tys1 tys2 = isEqual $ cmpTypes tys1 tys2
1131
1132 eqPred :: PredType -> PredType -> Bool
1133 eqPred p1 p2 = isEqual $ cmpPred p1 p2
1134
1135 eqPredX :: RnEnv2 -> PredType -> PredType -> Bool
1136 eqPredX env p1 p2 = isEqual $ cmpPredX env p1 p2
1137 \end{code}
1138
1139 Now here comes the real worker
1140
1141 \begin{code}
1142 cmpType :: Type -> Type -> Ordering
1143 cmpType t1 t2 = cmpTypeX rn_env t1 t2
1144   where
1145     rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfType t1 `unionVarSet` tyVarsOfType t2))
1146
1147 cmpTypes :: [Type] -> [Type] -> Ordering
1148 cmpTypes ts1 ts2 = cmpTypesX rn_env ts1 ts2
1149   where
1150     rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfTypes ts1 `unionVarSet` tyVarsOfTypes ts2))
1151
1152 cmpPred :: PredType -> PredType -> Ordering
1153 cmpPred p1 p2 = cmpPredX rn_env p1 p2
1154   where
1155     rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfPred p1 `unionVarSet` tyVarsOfPred p2))
1156
1157 cmpTypeX :: RnEnv2 -> Type -> Type -> Ordering  -- Main workhorse
1158 cmpTypeX env t1 t2 | Just t1' <- coreView t1 = cmpTypeX env t1' t2
1159                    | Just t2' <- coreView t2 = cmpTypeX env t1 t2'
1160 -- We expand predicate types, because in Core-land we have
1161 -- lots of definitions like
1162 --      fOrdBool :: Ord Bool
1163 --      fOrdBool = D:Ord .. .. ..
1164 -- So the RHS has a data type
1165
1166 cmpTypeX env (TyVarTy tv1)       (TyVarTy tv2)       = rnOccL env tv1 `compare` rnOccR env tv2
1167 cmpTypeX env (ForAllTy tv1 t1)   (ForAllTy tv2 t2)   = cmpTypeX (rnBndr2 env tv1 tv2) t1 t2
1168 cmpTypeX env (AppTy s1 t1)       (AppTy s2 t2)       = cmpTypeX env s1 s2 `thenCmp` cmpTypeX env t1 t2
1169 cmpTypeX env (FunTy s1 t1)       (FunTy s2 t2)       = cmpTypeX env s1 s2 `thenCmp` cmpTypeX env t1 t2
1170 cmpTypeX env (PredTy p1)         (PredTy p2)         = cmpPredX env p1 p2
1171 cmpTypeX env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` cmpTypesX env tys1 tys2
1172
1173     -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < ForAllTy < PredTy
1174 cmpTypeX _ (AppTy _ _)    (TyVarTy _)    = GT
1175
1176 cmpTypeX _ (FunTy _ _)    (TyVarTy _)    = GT
1177 cmpTypeX _ (FunTy _ _)    (AppTy _ _)    = GT
1178
1179 cmpTypeX _ (TyConApp _ _) (TyVarTy _)    = GT
1180 cmpTypeX _ (TyConApp _ _) (AppTy _ _)    = GT
1181 cmpTypeX _ (TyConApp _ _) (FunTy _ _)    = GT
1182
1183 cmpTypeX _ (ForAllTy _ _) (TyVarTy _)    = GT
1184 cmpTypeX _ (ForAllTy _ _) (AppTy _ _)    = GT
1185 cmpTypeX _ (ForAllTy _ _) (FunTy _ _)    = GT
1186 cmpTypeX _ (ForAllTy _ _) (TyConApp _ _) = GT
1187
1188 cmpTypeX _ (PredTy _)     _              = GT
1189
1190 cmpTypeX _ _              _              = LT
1191
1192 -------------
1193 cmpTypesX :: RnEnv2 -> [Type] -> [Type] -> Ordering
1194 cmpTypesX _   []        []        = EQ
1195 cmpTypesX env (t1:tys1) (t2:tys2) = cmpTypeX env t1 t2 `thenCmp` cmpTypesX env tys1 tys2
1196 cmpTypesX _   []        _         = LT
1197 cmpTypesX _   _         []        = GT
1198
1199 -------------
1200 cmpPredX :: RnEnv2 -> PredType -> PredType -> Ordering
1201 cmpPredX env (IParam n1 ty1) (IParam n2 ty2) = (n1 `compare` n2) `thenCmp` cmpTypeX env ty1 ty2
1202         -- Compare names only for implicit parameters
1203         -- This comparison is used exclusively (I believe) 
1204         -- for the Avails finite map built in TcSimplify
1205         -- If the types differ we keep them distinct so that we see 
1206         -- a distinct pair to run improvement on 
1207 cmpPredX env (ClassP c1 tys1) (ClassP c2 tys2) = (c1 `compare` c2) `thenCmp` (cmpTypesX env tys1 tys2)
1208 cmpPredX env (EqPred ty1 ty2) (EqPred ty1' ty2') = (cmpTypeX env ty1 ty1') `thenCmp` (cmpTypeX env ty2 ty2')
1209
1210 -- Constructor order: IParam < ClassP < EqPred
1211 cmpPredX _   (IParam {})     _              = LT
1212 cmpPredX _   (ClassP {})    (IParam {})     = GT
1213 cmpPredX _   (ClassP {})    (EqPred {})     = LT
1214 cmpPredX _   (EqPred {})    _               = GT
1215 \end{code}
1216
1217 PredTypes are used as a FM key in TcSimplify, 
1218 so we take the easy path and make them an instance of Ord
1219
1220 \begin{code}
1221 instance Eq  PredType where { (==)    = eqPred }
1222 instance Ord PredType where { compare = cmpPred }
1223 \end{code}
1224
1225
1226 %************************************************************************
1227 %*                                                                      *
1228                 Type substitutions
1229 %*                                                                      *
1230 %************************************************************************
1231
1232 \begin{code}
1233 emptyTvSubstEnv :: TvSubstEnv
1234 emptyTvSubstEnv = emptyVarEnv
1235
1236 composeTvSubst :: InScopeSet -> TvSubstEnv -> TvSubstEnv -> TvSubstEnv
1237 -- ^ @(compose env1 env2)(x)@ is @env1(env2(x))@; i.e. apply @env2@ then @env1@.
1238 -- It assumes that both are idempotent.
1239 -- Typically, @env1@ is the refinement to a base substitution @env2@
1240 composeTvSubst in_scope env1 env2
1241   = env1 `plusVarEnv` mapVarEnv (substTy subst1) env2
1242         -- First apply env1 to the range of env2
1243         -- Then combine the two, making sure that env1 loses if
1244         -- both bind the same variable; that's why env1 is the
1245         --  *left* argument to plusVarEnv, because the right arg wins
1246   where
1247     subst1 = TvSubst in_scope env1
1248
1249 emptyTvSubst :: TvSubst
1250 emptyTvSubst = TvSubst emptyInScopeSet emptyTvSubstEnv
1251
1252 isEmptyTvSubst :: TvSubst -> Bool
1253          -- See Note [Extending the TvSubstEnv]
1254 isEmptyTvSubst (TvSubst _ tenv) = isEmptyVarEnv tenv
1255
1256 mkTvSubst :: InScopeSet -> TvSubstEnv -> TvSubst
1257 mkTvSubst = TvSubst
1258
1259 getTvSubstEnv :: TvSubst -> TvSubstEnv
1260 getTvSubstEnv (TvSubst _ env) = env
1261
1262 getTvInScope :: TvSubst -> InScopeSet
1263 getTvInScope (TvSubst in_scope _) = in_scope
1264
1265 isInScope :: Var -> TvSubst -> Bool
1266 isInScope v (TvSubst in_scope _) = v `elemInScopeSet` in_scope
1267
1268 notElemTvSubst :: TyCoVar -> TvSubst -> Bool
1269 notElemTvSubst v (TvSubst _ tenv) = not (v `elemVarEnv` tenv)
1270
1271 setTvSubstEnv :: TvSubst -> TvSubstEnv -> TvSubst
1272 setTvSubstEnv (TvSubst in_scope _) tenv = TvSubst in_scope tenv
1273
1274 zapTvSubstEnv :: TvSubst -> TvSubst
1275 zapTvSubstEnv (TvSubst in_scope _) = TvSubst in_scope emptyVarEnv
1276
1277 extendTvInScope :: TvSubst -> Var -> TvSubst
1278 extendTvInScope (TvSubst in_scope tenv) var = TvSubst (extendInScopeSet in_scope var) tenv
1279
1280 extendTvInScopeList :: TvSubst -> [Var] -> TvSubst
1281 extendTvInScopeList (TvSubst in_scope tenv) vars = TvSubst (extendInScopeSetList in_scope vars) tenv
1282
1283 extendTvSubst :: TvSubst -> TyVar -> Type -> TvSubst
1284 extendTvSubst (TvSubst in_scope tenv) tv ty = TvSubst in_scope (extendVarEnv tenv tv ty)
1285
1286 extendTvSubstList :: TvSubst -> [TyVar] -> [Type] -> TvSubst
1287 extendTvSubstList (TvSubst in_scope tenv) tvs tys 
1288   = TvSubst in_scope (extendVarEnvList tenv (tvs `zip` tys))
1289
1290 unionTvSubst :: TvSubst -> TvSubst -> TvSubst
1291 -- Works when the ranges are disjoint
1292 unionTvSubst (TvSubst in_scope1 tenv1) (TvSubst in_scope2 tenv2)
1293   = ASSERT( not (tenv1 `intersectsVarEnv` tenv2) )
1294     TvSubst (in_scope1 `unionInScope` in_scope2)
1295             (tenv1     `plusVarEnv`   tenv2)
1296
1297 -- mkOpenTvSubst and zipOpenTvSubst generate the in-scope set from
1298 -- the types given; but it's just a thunk so with a bit of luck
1299 -- it'll never be evaluated
1300
1301 -- Note [Generating the in-scope set for a substitution]
1302 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1303 -- If we want to substitute [a -> ty1, b -> ty2] I used to 
1304 -- think it was enough to generate an in-scope set that includes
1305 -- fv(ty1,ty2).  But that's not enough; we really should also take the
1306 -- free vars of the type we are substituting into!  Example:
1307 --      (forall b. (a,b,x)) [a -> List b]
1308 -- Then if we use the in-scope set {b}, there is a danger we will rename
1309 -- the forall'd variable to 'x' by mistake, getting this:
1310 --      (forall x. (List b, x, x)
1311 -- Urk!  This means looking at all the calls to mkOpenTvSubst....
1312
1313
1314 -- | Generates the in-scope set for the 'TvSubst' from the types in the incoming
1315 -- environment, hence "open"
1316 mkOpenTvSubst :: TvSubstEnv -> TvSubst
1317 mkOpenTvSubst tenv = TvSubst (mkInScopeSet (tyVarsOfTypes (varEnvElts tenv))) tenv
1318
1319 -- | Generates the in-scope set for the 'TvSubst' from the types in the incoming
1320 -- environment, hence "open"
1321 zipOpenTvSubst :: [TyVar] -> [Type] -> TvSubst
1322 zipOpenTvSubst tyvars tys 
1323   | debugIsOn && (length tyvars /= length tys)
1324   = pprTrace "zipOpenTvSubst" (ppr tyvars $$ ppr tys) emptyTvSubst
1325   | otherwise
1326   = TvSubst (mkInScopeSet (tyVarsOfTypes tys)) (zipTyEnv tyvars tys)
1327
1328 -- | Called when doing top-level substitutions. Here we expect that the 
1329 -- free vars of the range of the substitution will be empty.
1330 mkTopTvSubst :: [(TyVar, Type)] -> TvSubst
1331 mkTopTvSubst prs = TvSubst emptyInScopeSet (mkVarEnv prs)
1332
1333 zipTopTvSubst :: [TyVar] -> [Type] -> TvSubst
1334 zipTopTvSubst tyvars tys 
1335   | debugIsOn && (length tyvars /= length tys)
1336   = pprTrace "zipTopTvSubst" (ppr tyvars $$ ppr tys) emptyTvSubst
1337   | otherwise
1338   = TvSubst emptyInScopeSet (zipTyEnv tyvars tys)
1339
1340 zipTyEnv :: [TyVar] -> [Type] -> TvSubstEnv
1341 zipTyEnv tyvars tys
1342   | debugIsOn && (length tyvars /= length tys)
1343   = pprTrace "zipTyEnv" (ppr tyvars $$ ppr tys) emptyVarEnv
1344   | otherwise
1345   = zip_ty_env tyvars tys emptyVarEnv
1346
1347 -- Later substitutions in the list over-ride earlier ones, 
1348 -- but there should be no loops
1349 zip_ty_env :: [TyVar] -> [Type] -> TvSubstEnv -> TvSubstEnv
1350 zip_ty_env []       []       env = env
1351 zip_ty_env (tv:tvs) (ty:tys) env = zip_ty_env tvs tys (extendVarEnv env tv ty)
1352         -- There used to be a special case for when 
1353         --      ty == TyVarTy tv
1354         -- (a not-uncommon case) in which case the substitution was dropped.
1355         -- But the type-tidier changes the print-name of a type variable without
1356         -- changing the unique, and that led to a bug.   Why?  Pre-tidying, we had 
1357         -- a type {Foo t}, where Foo is a one-method class.  So Foo is really a newtype.
1358         -- And it happened that t was the type variable of the class.  Post-tiding, 
1359         -- it got turned into {Foo t2}.  The ext-core printer expanded this using
1360         -- sourceTypeRep, but that said "Oh, t == t2" because they have the same unique,
1361         -- and so generated a rep type mentioning t not t2.  
1362         --
1363         -- Simplest fix is to nuke the "optimisation"
1364 zip_ty_env tvs      tys      env   = pprTrace "Var/Type length mismatch: " (ppr tvs $$ ppr tys) env
1365 -- zip_ty_env _ _ env = env
1366
1367 instance Outputable TvSubst where
1368   ppr (TvSubst ins tenv)
1369     = brackets $ sep[ ptext (sLit "TvSubst"),
1370                       nest 2 (ptext (sLit "In scope:") <+> ppr ins), 
1371                       nest 2 (ptext (sLit "Type env:") <+> ppr tenv) ]
1372 \end{code}
1373
1374 %************************************************************************
1375 %*                                                                      *
1376                 Performing type substitutions
1377 %*                                                                      *
1378 %************************************************************************
1379
1380 \begin{code}
1381 -- | Type substitution making use of an 'TvSubst' that
1382 -- is assumed to be open, see 'zipOpenTvSubst'
1383 substTyWith :: [TyVar] -> [Type] -> Type -> Type
1384 substTyWith tvs tys = ASSERT( length tvs == length tys )
1385                       substTy (zipOpenTvSubst tvs tys)
1386
1387 -- | Type substitution making use of an 'TvSubst' that
1388 -- is assumed to be open, see 'zipOpenTvSubst'
1389 substTysWith :: [TyVar] -> [Type] -> [Type] -> [Type]
1390 substTysWith tvs tys = ASSERT( length tvs == length tys )
1391                        substTys (zipOpenTvSubst tvs tys)
1392
1393 -- | Substitute within a 'Type'
1394 substTy :: TvSubst -> Type  -> Type
1395 substTy subst ty | isEmptyTvSubst subst = ty
1396                  | otherwise            = subst_ty subst ty
1397
1398 -- | Substitute within several 'Type's
1399 substTys :: TvSubst -> [Type] -> [Type]
1400 substTys subst tys | isEmptyTvSubst subst = tys
1401                    | otherwise            = map (subst_ty subst) tys
1402
1403 -- | Substitute within a 'ThetaType'
1404 substTheta :: TvSubst -> ThetaType -> ThetaType
1405 substTheta subst theta
1406   | isEmptyTvSubst subst = theta
1407   | otherwise            = map (substPred subst) theta
1408
1409 -- | Substitute within a 'PredType'
1410 substPred :: TvSubst -> PredType -> PredType
1411 substPred subst (IParam n ty)     = IParam n (subst_ty subst ty)
1412 substPred subst (ClassP clas tys) = ClassP clas (map (subst_ty subst) tys)
1413 substPred subst (EqPred ty1 ty2)  = EqPred (subst_ty subst ty1) (subst_ty subst ty2)
1414
1415 -- | Remove any nested binders mentioning the 'TyVar's in the 'TyVarSet'
1416 deShadowTy :: TyVarSet -> Type -> Type
1417 deShadowTy tvs ty 
1418   = subst_ty (mkTvSubst in_scope emptyTvSubstEnv) ty
1419   where
1420     in_scope = mkInScopeSet tvs
1421
1422 subst_ty :: TvSubst -> Type -> Type
1423 -- subst_ty is the main workhorse for type substitution
1424 --
1425 -- Note that the in_scope set is poked only if we hit a forall
1426 -- so it may often never be fully computed 
1427 subst_ty subst ty
1428    = go ty
1429   where
1430     go (TyVarTy tv)      = substTyVar subst tv
1431     go (TyConApp tc tys) = let args = map go tys
1432                            in  args `seqList` TyConApp tc args
1433
1434     go (PredTy p)        = PredTy $! (substPred subst p)
1435
1436     go (FunTy arg res)   = (FunTy $! (go arg)) $! (go res)
1437     go (AppTy fun arg)   = mkAppTy (go fun) $! (go arg)
1438                 -- The mkAppTy smart constructor is important
1439                 -- we might be replacing (a Int), represented with App
1440                 -- by [Int], represented with TyConApp
1441     go (ForAllTy tv ty)  = case substTyVarBndr subst tv of
1442                               (subst', tv') ->
1443                                  ForAllTy tv' $! (subst_ty subst' ty)
1444
1445 substTyVar :: TvSubst -> TyVar  -> Type
1446 substTyVar (TvSubst _ tenv) tv
1447   | Just ty  <- lookupVarEnv tenv tv      = ty  -- See Note [Apply Once]
1448   | otherwise = ASSERT( isTyVar tv ) TyVarTy tv
1449   -- We do not require that the tyvar is in scope
1450   -- Reason: we do quite a bit of (substTyWith [tv] [ty] tau)
1451   -- and it's a nuisance to bring all the free vars of tau into
1452   -- scope --- and then force that thunk at every tyvar
1453   -- Instead we have an ASSERT in substTyVarBndr to check for capture
1454
1455 substTyVars :: TvSubst -> [TyVar] -> [Type]
1456 substTyVars subst tvs = map (substTyVar subst) tvs
1457
1458 lookupTyVar :: TvSubst -> TyVar  -> Maybe Type
1459         -- See Note [Extending the TvSubst]
1460 lookupTyVar (TvSubst _ tenv) tv = lookupVarEnv tenv tv
1461
1462 substTyVarBndr :: TvSubst -> TyVar -> (TvSubst, TyVar)
1463 substTyVarBndr subst@(TvSubst in_scope tenv) old_var
1464   = ASSERT2( _no_capture, ppr old_var $$ ppr subst ) 
1465     (TvSubst (in_scope `extendInScopeSet` new_var) new_env, new_var)
1466   where
1467     new_env | no_change = delVarEnv tenv old_var
1468             | otherwise = extendVarEnv tenv old_var (TyVarTy new_var)
1469
1470     _no_capture = not (new_var `elemVarSet` tyVarsOfTypes (varEnvElts tenv))
1471     -- Check that we are not capturing something in the substitution
1472
1473     no_change = new_var == old_var
1474         -- no_change means that the new_var is identical in
1475         -- all respects to the old_var (same unique, same kind)
1476         -- See Note [Extending the TvSubst]
1477         --
1478         -- In that case we don't need to extend the substitution
1479         -- to map old to new.  But instead we must zap any 
1480         -- current substitution for the variable. For example:
1481         --      (\x.e) with id_subst = [x |-> e']
1482         -- Here we must simply zap the substitution for x
1483
1484     new_var = uniqAway in_scope old_var
1485         -- The uniqAway part makes sure the new variable is not already in scope
1486 \end{code}
1487
1488 ----------------------------------------------------
1489 -- Kind Stuff
1490
1491 Kinds
1492 ~~~~~
1493
1494 \begin{code}
1495 -- $kind_subtyping
1496 -- #kind_subtyping#
1497 -- There's a little subtyping at the kind level:
1498 --
1499 -- @
1500 --               ?
1501 --              \/ &#92;
1502 --             \/   &#92;
1503 --            ??   (\#)
1504 --           \/  &#92;
1505 --          \*    \#
1506 -- .
1507 -- Where:        \*    [LiftedTypeKind]   means boxed type
1508 --              \#    [UnliftedTypeKind] means unboxed type
1509 --              (\#)  [UbxTupleKind]     means unboxed tuple
1510 --              ??   [ArgTypeKind]      is the lub of {\*, \#}
1511 --              ?    [OpenTypeKind]     means any type at all
1512 -- @
1513 --
1514 -- In particular:
1515 --
1516 -- > error :: forall a:?. String -> a
1517 -- > (->)  :: ?? -> ? -> \*
1518 -- > (\\(x::t) -> ...)
1519 --
1520 -- Where in the last example @t :: ??@ (i.e. is not an unboxed tuple)
1521
1522 type KindVar = TyVar  -- invariant: KindVar will always be a 
1523                       -- TcTyVar with details MetaTv TauTv ...
1524 -- kind var constructors and functions are in TcType
1525
1526 type SimpleKind = Kind
1527 \end{code}
1528
1529 Kind inference
1530 ~~~~~~~~~~~~~~
1531 During kind inference, a kind variable unifies only with 
1532 a "simple kind", sk
1533         sk ::= * | sk1 -> sk2
1534 For example 
1535         data T a = MkT a (T Int#)
1536 fails.  We give T the kind (k -> *), and the kind variable k won't unify
1537 with # (the kind of Int#).
1538
1539 Type inference
1540 ~~~~~~~~~~~~~~
1541 When creating a fresh internal type variable, we give it a kind to express 
1542 constraints on it.  E.g. in (\x->e) we make up a fresh type variable for x, 
1543 with kind ??.  
1544
1545 During unification we only bind an internal type variable to a type
1546 whose kind is lower in the sub-kind hierarchy than the kind of the tyvar.
1547
1548 When unifying two internal type variables, we collect their kind constraints by
1549 finding the GLB of the two.  Since the partial order is a tree, they only
1550 have a glb if one is a sub-kind of the other.  In that case, we bind the
1551 less-informative one to the more informative one.  Neat, eh?