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