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