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