Implement Partial Type Signatures
[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, applyTysX, 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, pprSigmaTypeExtraCts,
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 appropriate 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( tvs `leLength` tys, ppr tycon $$ ppr tys $$ ppr tvs )
579       applyTysX tvs rhs tys
580   where
581     (tvs, rhs) = newTyConEtadRhs tycon
582 \end{code}
583
584
585 ---------------------------------------------------------------------
586                                 SynTy
587                                 ~~~~~
588
589 Notes on type synonyms
590 ~~~~~~~~~~~~~~~~~~~~~~
591 The various "split" functions (splitFunTy, splitRhoTy, splitForAllTy) try
592 to return type synonyms wherever possible. Thus
593
594         type Foo a = a -> a
595
596 we want
597         splitFunTys (a -> Foo a) = ([a], Foo a)
598 not                                ([a], a -> a)
599
600 The reason is that we then get better (shorter) type signatures in
601 interfaces.  Notably this plays a role in tcTySigs in TcBinds.lhs.
602
603
604                 Representation types
605                 ~~~~~~~~~~~~~~~~~~~~
606
607 Note [Nullary unboxed tuple]
608 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
609 We represent the nullary unboxed tuple as the unary (but void) type
610 Void#.  The reason for this is that the ReprArity is never
611 less than the Arity (as it would otherwise be for a function type like
612 (# #) -> Int).
613
614 As a result, ReprArity is always strictly positive if Arity is. This
615 is important because it allows us to distinguish at runtime between a
616 thunk and a function takes a nullary unboxed tuple as an argument!
617
618 \begin{code}
619 type UnaryType = Type
620
621 data RepType = UbxTupleRep [UnaryType] -- INVARIANT: never an empty list (see Note [Nullary unboxed tuple])
622              | UnaryRep UnaryType
623
624 flattenRepType :: RepType -> [UnaryType]
625 flattenRepType (UbxTupleRep tys) = tys
626 flattenRepType (UnaryRep ty)     = [ty]
627
628 -- | Looks through:
629 --
630 --      1. For-alls
631 --      2. Synonyms
632 --      3. Predicates
633 --      4. All newtypes, including recursive ones, but not newtype families
634 --
635 -- It's useful in the back end of the compiler.
636 repType :: Type -> RepType
637 repType ty
638   = go initRecTc ty
639   where
640     go :: RecTcChecker -> Type -> RepType
641     go rec_nts ty                       -- Expand predicates and synonyms
642       | Just ty' <- coreView ty
643       = go rec_nts ty'
644
645     go rec_nts (ForAllTy _ ty)          -- Drop foralls
646         = go rec_nts ty
647
648     go rec_nts (TyConApp tc tys)        -- Expand newtypes
649       | isNewTyCon tc
650       , tys `lengthAtLeast` tyConArity tc
651       , Just rec_nts' <- checkRecTc rec_nts tc   -- See Note [Expanding newtypes] in TyCon
652       = go rec_nts' (newTyConInstRhs tc tys)
653
654       | isUnboxedTupleTyCon tc
655       = if null tys
656          then UnaryRep voidPrimTy -- See Note [Nullary unboxed tuple]
657          else UbxTupleRep (concatMap (flattenRepType . go rec_nts) tys)
658
659     go _ ty = UnaryRep ty
660
661
662 -- | All type constructors occurring in the type; looking through type
663 --   synonyms, but not newtypes.
664 --  When it finds a Class, it returns the class TyCon.
665 tyConsOfType :: Type -> NameEnv TyCon
666 tyConsOfType ty
667   = go ty
668   where
669      go :: Type -> NameEnv TyCon  -- The NameEnv does duplicate elim
670      go ty | Just ty' <- tcView ty = go ty'
671      go (TyVarTy {})               = emptyNameEnv
672      go (LitTy {})                 = emptyNameEnv
673      go (TyConApp tc tys)          = go_tc tc tys
674      go (AppTy a b)                = go a `plusNameEnv` go b
675      go (FunTy a b)                = go a `plusNameEnv` go b
676      go (ForAllTy _ ty)            = go ty
677
678      go_tc tc tys = extendNameEnv (go_s tys) (tyConName tc) tc
679      go_s tys = foldr (plusNameEnv . go) emptyNameEnv tys
680
681 -- ToDo: this could be moved to the code generator, using splitTyConApp instead
682 -- of inspecting the type directly.
683
684 -- | Discovers the primitive representation of a more abstract 'UnaryType'
685 typePrimRep :: UnaryType -> PrimRep
686 typePrimRep ty
687   = case repType ty of
688       UbxTupleRep _ -> pprPanic "typePrimRep: UbxTupleRep" (ppr ty)
689       UnaryRep rep -> case rep of
690         TyConApp tc _ -> tyConPrimRep tc
691         FunTy _ _     -> PtrRep
692         AppTy _ _     -> PtrRep      -- See Note [AppTy rep]
693         TyVarTy _     -> PtrRep
694         _             -> pprPanic "typePrimRep: UnaryRep" (ppr ty)
695
696 typeRepArity :: Arity -> Type -> RepArity
697 typeRepArity 0 _ = 0
698 typeRepArity n ty = case repType ty of
699   UnaryRep (FunTy ty1 ty2) -> length (flattenRepType (repType ty1)) + typeRepArity (n - 1) ty2
700   _                        -> pprPanic "typeRepArity: arity greater than type can handle" (ppr (n, ty))
701
702 isVoidTy :: Type -> Bool
703 -- True if the type has zero width
704 isVoidTy ty = case repType ty of
705                 UnaryRep (TyConApp tc _) -> isVoidRep (tyConPrimRep tc)
706                 _                        -> False
707 \end{code}
708
709 Note [AppTy rep]
710 ~~~~~~~~~~~~~~~~
711 Types of the form 'f a' must be of kind *, not #, so we are guaranteed
712 that they are represented by pointers.  The reason is that f must have
713 kind (kk -> kk) and kk cannot be unlifted; see Note [The kind invariant]
714 in TypeRep.
715
716 ---------------------------------------------------------------------
717                                 ForAllTy
718                                 ~~~~~~~~
719
720 \begin{code}
721 mkForAllTy :: TyVar -> Type -> Type
722 mkForAllTy tyvar ty
723   = ForAllTy tyvar ty
724
725 -- | Wraps foralls over the type using the provided 'TyVar's from left to right
726 mkForAllTys :: [TyVar] -> Type -> Type
727 mkForAllTys tyvars ty = foldr ForAllTy ty tyvars
728
729 mkPiKinds :: [TyVar] -> Kind -> Kind
730 -- mkPiKinds [k1, k2, (a:k1 -> *)] k2
731 -- returns forall k1 k2. (k1 -> *) -> k2
732 mkPiKinds [] res = res
733 mkPiKinds (tv:tvs) res
734   | isKindVar tv = ForAllTy tv          (mkPiKinds tvs res)
735   | otherwise    = FunTy (tyVarKind tv) (mkPiKinds tvs res)
736
737 mkPiType  :: Var -> Type -> Type
738 -- ^ Makes a @(->)@ type or a forall type, depending
739 -- on whether it is given a type variable or a term variable.
740 mkPiTypes :: [Var] -> Type -> Type
741 -- ^ 'mkPiType' for multiple type or value arguments
742
743 mkPiType v ty
744    | isId v    = mkFunTy (varType v) ty
745    | otherwise = mkForAllTy v ty
746
747 mkPiTypes vs ty = foldr mkPiType ty vs
748
749 isForAllTy :: Type -> Bool
750 isForAllTy (ForAllTy _ _) = True
751 isForAllTy _              = False
752
753 -- | Attempts to take a forall type apart, returning the bound type variable
754 -- and the remainder of the type
755 splitForAllTy_maybe :: Type -> Maybe (TyVar, Type)
756 splitForAllTy_maybe ty = splitFAT_m ty
757   where
758     splitFAT_m ty | Just ty' <- coreView ty = splitFAT_m ty'
759     splitFAT_m (ForAllTy tyvar ty)          = Just(tyvar, ty)
760     splitFAT_m _                            = Nothing
761
762 -- | Attempts to take a forall type apart, returning all the immediate such bound
763 -- type variables and the remainder of the type. Always suceeds, even if that means
764 -- returning an empty list of 'TyVar's
765 splitForAllTys :: Type -> ([TyVar], Type)
766 splitForAllTys ty = split ty ty []
767    where
768      split orig_ty ty tvs | Just ty' <- coreView ty = split orig_ty ty' tvs
769      split _       (ForAllTy tv ty)  tvs = split ty ty (tv:tvs)
770      split orig_ty _                 tvs = (reverse tvs, orig_ty)
771
772 -- | Equivalent to @snd . splitForAllTys@
773 dropForAlls :: Type -> Type
774 dropForAlls ty = snd (splitForAllTys ty)
775 \end{code}
776
777 -- (mkPiType now in CoreUtils)
778
779 applyTy, applyTys
780 ~~~~~~~~~~~~~~~~~
781
782 \begin{code}
783 -- | Instantiate a forall type with one or more type arguments.
784 -- Used when we have a polymorphic function applied to type args:
785 --
786 -- > f t1 t2
787 --
788 -- We use @applyTys type-of-f [t1,t2]@ to compute the type of the expression.
789 -- Panics if no application is possible.
790 applyTy :: Type -> KindOrType -> Type
791 applyTy ty arg | Just ty' <- coreView ty = applyTy ty' arg
792 applyTy (ForAllTy tv ty) arg = substTyWith [tv] [arg] ty
793 applyTy _                _   = panic "applyTy"
794
795 applyTys :: Type -> [KindOrType] -> Type
796 -- ^ This function is interesting because:
797 --
798 --      1. The function may have more for-alls than there are args
799 --
800 --      2. Less obviously, it may have fewer for-alls
801 --
802 -- For case 2. think of:
803 --
804 -- > applyTys (forall a.a) [forall b.b, Int]
805 --
806 -- This really can happen, but only (I think) in situations involving
807 -- undefined.  For example:
808 --       undefined :: forall a. a
809 -- Term: undefined @(forall b. b->b) @Int
810 -- This term should have type (Int -> Int), but notice that
811 -- there are more type args than foralls in 'undefined's type.
812
813 -- If you edit this function, you may need to update the GHC formalism
814 -- See Note [GHC Formalism] in coreSyn/CoreLint.lhs
815 applyTys ty args = applyTysD empty ty args
816
817 applyTysD :: SDoc -> Type -> [Type] -> Type     -- Debug version
818 applyTysD _   orig_fun_ty []      = orig_fun_ty
819 applyTysD doc orig_fun_ty arg_tys
820   | n_tvs == n_args     -- The vastly common case
821   = substTyWith tvs arg_tys rho_ty
822   | n_tvs > n_args      -- Too many for-alls
823   = substTyWith (take n_args tvs) arg_tys
824                 (mkForAllTys (drop n_args tvs) rho_ty)
825   | otherwise           -- Too many type args
826   = ASSERT2( n_tvs > 0, doc $$ ppr orig_fun_ty $$ ppr arg_tys )        -- Zero case gives infinite loop!
827     applyTysD doc (substTyWith tvs (take n_tvs arg_tys) rho_ty)
828                   (drop n_tvs arg_tys)
829   where
830     (tvs, rho_ty) = splitForAllTys orig_fun_ty
831     n_tvs  = length tvs
832     n_args = length arg_tys
833
834 applyTysX :: [TyVar] -> Type -> [Type] -> Type
835 -- applyTyxX beta-reduces (/\tvs. body_ty) arg_tys
836 applyTysX tvs body_ty arg_tys
837   = ASSERT2( length arg_tys >= n_tvs, ppr tvs $$ ppr body_ty $$ ppr arg_tys )
838     mkAppTys (substTyWith tvs (take n_tvs arg_tys) body_ty)
839              (drop n_tvs arg_tys)
840   where
841     n_tvs = length tvs
842 \end{code}
843
844
845 %************************************************************************
846 %*                                                                      *
847                          Pred
848 %*                                                                      *
849 %************************************************************************
850
851 Predicates on PredType
852
853 \begin{code}
854 isPredTy :: Type -> Bool
855   -- NB: isPredTy is used when printing types, which can happen in debug printing
856   --     during type checking of not-fully-zonked types.  So it's not cool to say
857   --     isConstraintKind (typeKind ty) because absent zonking the type might 
858   --     be ill-kinded, and typeKind crashes
859   --     Hence the rather tiresome story here
860 isPredTy ty = go ty []
861   where
862     go :: Type -> [KindOrType] -> Bool
863     go (AppTy ty1 ty2)   args = go ty1 (ty2 : args)
864     go (TyConApp tc tys) args = go_k (tyConKind tc) (tys ++ args)
865     go (TyVarTy tv)      args = go_k (tyVarKind tv) args
866     go _                 _    = False
867
868     go_k :: Kind -> [KindOrType] -> Bool
869     -- True <=> kind is k1 -> .. -> kn -> Constraint
870     go_k k                [] = isConstraintKind k
871     go_k (FunTy _ k1)     (_ :args) = go_k k1 args
872     go_k (ForAllTy kv k1) (k2:args) = go_k (substKiWith [kv] [k2] k1) args
873     go_k _ _ = False                  -- Typeable * Int :: Constraint
874
875 isClassPred, isEqPred, isIPPred :: PredType -> Bool
876 isClassPred ty = case tyConAppTyCon_maybe ty of
877     Just tyCon | isClassTyCon tyCon -> True
878     _                               -> False
879 isEqPred ty = case tyConAppTyCon_maybe ty of
880     Just tyCon -> tyCon `hasKey` eqTyConKey
881     _          -> False
882
883 isIPPred ty = case tyConAppTyCon_maybe ty of
884     Just tc -> isIPTyCon tc
885     _       -> False
886
887 isIPTyCon :: TyCon -> Bool
888 isIPTyCon tc = tc `hasKey` ipClassNameKey
889
890 isIPClass :: Class -> Bool
891 isIPClass cls = cls `hasKey` ipClassNameKey
892   -- Class and it corresponding TyCon have the same Unique
893
894 isIPPred_maybe :: Type -> Maybe (FastString, Type)
895 isIPPred_maybe ty =
896   do (tc,[t1,t2]) <- splitTyConApp_maybe ty
897      guard (isIPTyCon tc)
898      x <- isStrLitTy t1
899      return (x,t2)
900 \end{code}
901
902 Make PredTypes
903
904 --------------------- Equality types ---------------------------------
905 \begin{code}
906 -- | Creates a type equality predicate
907 mkEqPred :: Type -> Type -> PredType
908 mkEqPred ty1 ty2
909   = WARN( not (k `eqKind` typeKind ty2), ppr ty1 $$ ppr ty2 $$ ppr k $$ ppr (typeKind ty2) )
910     TyConApp eqTyCon [k, ty1, ty2]
911   where
912     k = typeKind ty1
913
914 mkCoerciblePred :: Type -> Type -> PredType
915 mkCoerciblePred ty1 ty2
916   = WARN( not (k `eqKind` typeKind ty2), ppr ty1 $$ ppr ty2 $$ ppr k $$ ppr (typeKind ty2) )
917     TyConApp coercibleTyCon [k, ty1, ty2]
918   where
919     k = typeKind ty1
920
921 mkPrimEqPred :: Type -> Type -> Type
922 mkPrimEqPred ty1  ty2
923   = WARN( not (k `eqKind` typeKind ty2), ppr ty1 $$ ppr ty2 )
924     TyConApp eqPrimTyCon [k, ty1, ty2]
925   where
926     k = typeKind ty1
927
928 mkReprPrimEqPred :: Type -> Type -> Type
929 mkReprPrimEqPred ty1  ty2
930   = WARN( not (k `eqKind` typeKind ty2), ppr ty1 $$ ppr ty2 )
931     TyConApp eqReprPrimTyCon [k, ty1, ty2]
932   where
933     k = typeKind ty1
934 \end{code}
935
936 --------------------- Dictionary types ---------------------------------
937 \begin{code}
938 mkClassPred :: Class -> [Type] -> PredType
939 mkClassPred clas tys = TyConApp (classTyCon clas) tys
940
941 isDictTy :: Type -> Bool
942 isDictTy = isClassPred
943
944 isDictLikeTy :: Type -> Bool
945 -- Note [Dictionary-like types]
946 isDictLikeTy ty | Just ty' <- coreView ty = isDictLikeTy ty'
947 isDictLikeTy ty = case splitTyConApp_maybe ty of
948         Just (tc, tys) | isClassTyCon tc -> True
949                        | isTupleTyCon tc -> all isDictLikeTy tys
950         _other                           -> False
951 \end{code}
952
953 Note [Dictionary-like types]
954 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
955 Being "dictionary-like" means either a dictionary type or a tuple thereof.
956 In GHC 6.10 we build implication constraints which construct such tuples,
957 and if we land up with a binding
958     t :: (C [a], Eq [a])
959     t = blah
960 then we want to treat t as cheap under "-fdicts-cheap" for example.
961 (Implication constraints are normally inlined, but sadly not if the
962 occurrence is itself inside an INLINE function!  Until we revise the
963 handling of implication constraints, that is.)  This turned out to
964 be important in getting good arities in DPH code.  Example:
965
966     class C a
967     class D a where { foo :: a -> a }
968     instance C a => D (Maybe a) where { foo x = x }
969
970     bar :: (C a, C b) => a -> b -> (Maybe a, Maybe b)
971     {-# INLINE bar #-}
972     bar x y = (foo (Just x), foo (Just y))
973
974 Then 'bar' should jolly well have arity 4 (two dicts, two args), but
975 we ended up with something like
976    bar = __inline_me__ (\d1,d2. let t :: (D (Maybe a), D (Maybe b)) = ...
977                                 in \x,y. <blah>)
978
979 This is all a bit ad-hoc; eg it relies on knowing that implication
980 constraints build tuples.
981
982
983 Decomposing PredType
984
985 \begin{code}
986 data PredTree = ClassPred Class [Type]
987               | EqPred Type Type
988               | TuplePred [PredType]
989               | IrredPred PredType
990
991 classifyPredType :: PredType -> PredTree
992 classifyPredType ev_ty = case splitTyConApp_maybe ev_ty of
993     Just (tc, tys) | Just clas <- tyConClass_maybe tc
994                    -> ClassPred clas tys
995     Just (tc, tys) | tc `hasKey` eqTyConKey
996                    , let [_, ty1, ty2] = tys
997                    -> EqPred ty1 ty2
998     Just (tc, tys) | isTupleTyCon tc
999                    -> TuplePred tys
1000     _ -> IrredPred ev_ty
1001 \end{code}
1002
1003 \begin{code}
1004 getClassPredTys :: PredType -> (Class, [Type])
1005 getClassPredTys ty = case getClassPredTys_maybe ty of
1006         Just (clas, tys) -> (clas, tys)
1007         Nothing          -> pprPanic "getClassPredTys" (ppr ty)
1008
1009 getClassPredTys_maybe :: PredType -> Maybe (Class, [Type])
1010 getClassPredTys_maybe ty = case splitTyConApp_maybe ty of
1011         Just (tc, tys) | Just clas <- tyConClass_maybe tc -> Just (clas, tys)
1012         _ -> Nothing
1013
1014 getEqPredTys :: PredType -> (Type, Type)
1015 getEqPredTys ty
1016   = case splitTyConApp_maybe ty of
1017       Just (tc, (_ : ty1 : ty2 : tys)) ->
1018         ASSERT( null tys && (tc `hasKey` eqTyConKey || tc `hasKey` coercibleTyConKey) )
1019         (ty1, ty2)
1020       _ -> pprPanic "getEqPredTys" (ppr ty)
1021
1022 getEqPredTys_maybe :: PredType -> Maybe (Role, Type, Type)
1023 getEqPredTys_maybe ty
1024   = case splitTyConApp_maybe ty of
1025       Just (tc, [_, ty1, ty2])
1026         | tc `hasKey` eqTyConKey -> Just (Nominal, ty1, ty2)
1027         | tc `hasKey` coercibleTyConKey -> Just (Representational, ty1, ty2)
1028       _ -> Nothing
1029
1030 getEqPredRole :: PredType -> Role
1031 getEqPredRole ty
1032   = case splitTyConApp_maybe ty of
1033       Just (tc, [_, _, _])
1034         | tc `hasKey` eqTyConKey -> Nominal
1035         | tc `hasKey` coercibleTyConKey -> Representational
1036       _ -> pprPanic "getEqPredRole" (ppr ty)
1037
1038 \end{code}
1039
1040 %************************************************************************
1041 %*                                                                      *
1042                    Size
1043 %*                                                                      *
1044 %************************************************************************
1045
1046 \begin{code}
1047 typeSize :: Type -> Int
1048 typeSize (LitTy {})      = 1
1049 typeSize (TyVarTy {})    = 1
1050 typeSize (AppTy t1 t2)   = typeSize t1 + typeSize t2
1051 typeSize (FunTy t1 t2)   = typeSize t1 + typeSize t2
1052 typeSize (ForAllTy _ t)  = 1 + typeSize t
1053 typeSize (TyConApp _ ts) = 1 + sum (map typeSize ts)
1054 \end{code}
1055
1056
1057 %************************************************************************
1058 %*                                                                      *
1059 \subsection{Type families}
1060 %*                                                                      *
1061 %************************************************************************
1062
1063 \begin{code}
1064 mkFamilyTyConApp :: TyCon -> [Type] -> Type
1065 -- ^ Given a family instance TyCon and its arg types, return the
1066 -- corresponding family type.  E.g:
1067 --
1068 -- > data family T a
1069 -- > data instance T (Maybe b) = MkT b
1070 --
1071 -- Where the instance tycon is :RTL, so:
1072 --
1073 -- > mkFamilyTyConApp :RTL Int  =  T (Maybe Int)
1074 mkFamilyTyConApp tc tys
1075   | Just (fam_tc, fam_tys) <- tyConFamInst_maybe tc
1076   , let tvs = tyConTyVars tc
1077         fam_subst = ASSERT2( length tvs == length tys, ppr tc <+> ppr tys )
1078                     zipTopTvSubst tvs tys
1079   = mkTyConApp fam_tc (substTys fam_subst fam_tys)
1080   | otherwise
1081   = mkTyConApp tc tys
1082
1083 -- | Get the type on the LHS of a coercion induced by a type/data
1084 -- family instance.
1085 coAxNthLHS :: CoAxiom br -> Int -> Type
1086 coAxNthLHS ax ind =
1087   mkTyConApp (coAxiomTyCon ax) (coAxBranchLHS (coAxiomNthBranch ax ind))
1088
1089 -- | Pretty prints a 'TyCon', using the family instance in case of a
1090 -- representation tycon.  For example:
1091 --
1092 -- > data T [a] = ...
1093 --
1094 -- In that case we want to print @T [a]@, where @T@ is the family 'TyCon'
1095 pprSourceTyCon :: TyCon -> SDoc
1096 pprSourceTyCon tycon
1097   | Just (fam_tc, tys) <- tyConFamInst_maybe tycon
1098   = ppr $ fam_tc `TyConApp` tys        -- can't be FunTyCon
1099   | otherwise
1100   = ppr tycon
1101 \end{code}
1102
1103 %************************************************************************
1104 %*                                                                      *
1105 \subsection{Liftedness}
1106 %*                                                                      *
1107 %************************************************************************
1108
1109 \begin{code}
1110 -- | See "Type#type_classification" for what an unlifted type is
1111 isUnLiftedType :: Type -> Bool
1112         -- isUnLiftedType returns True for forall'd unlifted types:
1113         --      x :: forall a. Int#
1114         -- I found bindings like these were getting floated to the top level.
1115         -- They are pretty bogus types, mind you.  It would be better never to
1116         -- construct them
1117
1118 isUnLiftedType ty | Just ty' <- coreView ty = isUnLiftedType ty'
1119 isUnLiftedType (ForAllTy _ ty)      = isUnLiftedType ty
1120 isUnLiftedType (TyConApp tc _)      = isUnLiftedTyCon tc
1121 isUnLiftedType _                    = False
1122
1123 isUnboxedTupleType :: Type -> Bool
1124 isUnboxedTupleType ty = case tyConAppTyCon_maybe ty of
1125                            Just tc -> isUnboxedTupleTyCon tc
1126                            _       -> False
1127
1128 -- | See "Type#type_classification" for what an algebraic type is.
1129 -- Should only be applied to /types/, as opposed to e.g. partially
1130 -- saturated type constructors
1131 isAlgType :: Type -> Bool
1132 isAlgType ty
1133   = case splitTyConApp_maybe ty of
1134       Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
1135                             isAlgTyCon tc
1136       _other             -> False
1137
1138 -- | See "Type#type_classification" for what an algebraic type is.
1139 -- Should only be applied to /types/, as opposed to e.g. partially
1140 -- saturated type constructors. Closed type constructors are those
1141 -- with a fixed right hand side, as opposed to e.g. associated types
1142 isClosedAlgType :: Type -> Bool
1143 isClosedAlgType ty
1144   = case splitTyConApp_maybe ty of
1145       Just (tc, ty_args) | isAlgTyCon tc && not (isFamilyTyCon tc)
1146              -> ASSERT2( ty_args `lengthIs` tyConArity tc, ppr ty ) True
1147       _other -> False
1148 \end{code}
1149
1150 \begin{code}
1151 -- | Computes whether an argument (or let right hand side) should
1152 -- be computed strictly or lazily, based only on its type.
1153 -- Currently, it's just 'isUnLiftedType'.
1154
1155 isStrictType :: Type -> Bool
1156 isStrictType = isUnLiftedType
1157 \end{code}
1158
1159 \begin{code}
1160 isPrimitiveType :: Type -> Bool
1161 -- ^ Returns true of types that are opaque to Haskell.
1162 isPrimitiveType ty = case splitTyConApp_maybe ty of
1163                         Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
1164                                               isPrimTyCon tc
1165                         _                  -> False
1166 \end{code}
1167
1168
1169 %************************************************************************
1170 %*                                                                      *
1171 \subsection{Sequencing on types}
1172 %*                                                                      *
1173 %************************************************************************
1174
1175 \begin{code}
1176 seqType :: Type -> ()
1177 seqType (LitTy n)         = n `seq` ()
1178 seqType (TyVarTy tv)      = tv `seq` ()
1179 seqType (AppTy t1 t2)     = seqType t1 `seq` seqType t2
1180 seqType (FunTy t1 t2)     = seqType t1 `seq` seqType t2
1181 seqType (TyConApp tc tys) = tc `seq` seqTypes tys
1182 seqType (ForAllTy tv ty)  = seqType (tyVarKind tv) `seq` seqType ty
1183
1184 seqTypes :: [Type] -> ()
1185 seqTypes []       = ()
1186 seqTypes (ty:tys) = seqType ty `seq` seqTypes tys
1187 \end{code}
1188
1189
1190 %************************************************************************
1191 %*                                                                      *
1192                 Comparison for types
1193         (We don't use instances so that we know where it happens)
1194 %*                                                                      *
1195 %************************************************************************
1196
1197 \begin{code}
1198 eqKind :: Kind -> Kind -> Bool
1199 -- Watch out for horrible hack: See Note [Comparison with OpenTypeKind]
1200 eqKind = eqType
1201
1202 eqType :: Type -> Type -> Bool
1203 -- ^ Type equality on source types. Does not look through @newtypes@ or
1204 -- 'PredType's, but it does look through type synonyms.
1205 -- Watch out for horrible hack: See Note [Comparison with OpenTypeKind]
1206 eqType t1 t2 = isEqual $ cmpType t1 t2
1207
1208 instance Eq Type where
1209   (==) = eqType
1210
1211 eqTypeX :: RnEnv2 -> Type -> Type -> Bool
1212 eqTypeX env t1 t2 = isEqual $ cmpTypeX env t1 t2
1213
1214 eqTypes :: [Type] -> [Type] -> Bool
1215 eqTypes tys1 tys2 = isEqual $ cmpTypes tys1 tys2
1216
1217 eqPred :: PredType -> PredType -> Bool
1218 eqPred = eqType
1219
1220 eqPredX :: RnEnv2 -> PredType -> PredType -> Bool
1221 eqPredX env p1 p2 = isEqual $ cmpTypeX env p1 p2
1222
1223 eqTyVarBndrs :: RnEnv2 -> [TyVar] -> [TyVar] -> Maybe RnEnv2
1224 -- Check that the tyvar lists are the same length
1225 -- and have matching kinds; if so, extend the RnEnv2
1226 -- Returns Nothing if they don't match
1227 eqTyVarBndrs env [] []
1228  = Just env
1229 eqTyVarBndrs env (tv1:tvs1) (tv2:tvs2)
1230  | eqTypeX env (tyVarKind tv1) (tyVarKind tv2)
1231  = eqTyVarBndrs (rnBndr2 env tv1 tv2) tvs1 tvs2
1232 eqTyVarBndrs _ _ _= Nothing
1233 \end{code}
1234
1235 Now here comes the real worker
1236
1237 \begin{code}
1238 cmpType :: Type -> Type -> Ordering
1239 -- Watch out for horrible hack: See Note [Comparison with OpenTypeKind]
1240 cmpType t1 t2 = cmpTypeX rn_env t1 t2
1241   where
1242     rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfType t1 `unionVarSet` tyVarsOfType t2))
1243
1244 cmpTypes :: [Type] -> [Type] -> Ordering
1245 cmpTypes ts1 ts2 = cmpTypesX rn_env ts1 ts2
1246   where
1247     rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfTypes ts1 `unionVarSet` tyVarsOfTypes ts2))
1248
1249 cmpPred :: PredType -> PredType -> Ordering
1250 cmpPred p1 p2 = cmpTypeX rn_env p1 p2
1251   where
1252     rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfType p1 `unionVarSet` tyVarsOfType p2))
1253
1254 cmpTypeX :: RnEnv2 -> Type -> Type -> Ordering  -- Main workhorse
1255 cmpTypeX env t1 t2 | Just t1' <- coreView t1 = cmpTypeX env t1' t2
1256                    | Just t2' <- coreView t2 = cmpTypeX env t1 t2'
1257 -- We expand predicate types, because in Core-land we have
1258 -- lots of definitions like
1259 --      fOrdBool :: Ord Bool
1260 --      fOrdBool = D:Ord .. .. ..
1261 -- So the RHS has a data type
1262
1263 cmpTypeX env (TyVarTy tv1)       (TyVarTy tv2)       = rnOccL env tv1 `compare` rnOccR env tv2
1264 cmpTypeX env (ForAllTy tv1 t1)   (ForAllTy tv2 t2)   = cmpTypeX env (tyVarKind tv1) (tyVarKind tv2)
1265                                                        `thenCmp` cmpTypeX (rnBndr2 env tv1 tv2) t1 t2
1266 cmpTypeX env (AppTy s1 t1)       (AppTy s2 t2)       = cmpTypeX env s1 s2 `thenCmp` cmpTypeX env t1 t2
1267 cmpTypeX env (FunTy s1 t1)       (FunTy s2 t2)       = cmpTypeX env s1 s2 `thenCmp` cmpTypeX env t1 t2
1268 cmpTypeX env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `cmpTc` tc2) `thenCmp` cmpTypesX env tys1 tys2
1269 cmpTypeX _   (LitTy l1)          (LitTy l2)          = compare l1 l2
1270
1271     -- Deal with the rest: TyVarTy < AppTy < FunTy < LitTy < TyConApp < ForAllTy < PredTy
1272 cmpTypeX _ (AppTy _ _)    (TyVarTy _)    = GT
1273
1274 cmpTypeX _ (FunTy _ _)    (TyVarTy _)    = GT
1275 cmpTypeX _ (FunTy _ _)    (AppTy _ _)    = GT
1276
1277 cmpTypeX _ (LitTy _)      (TyVarTy _)    = GT
1278 cmpTypeX _ (LitTy _)      (AppTy _ _)    = GT
1279 cmpTypeX _ (LitTy _)      (FunTy _ _)    = GT
1280
1281 cmpTypeX _ (TyConApp _ _) (TyVarTy _)    = GT
1282 cmpTypeX _ (TyConApp _ _) (AppTy _ _)    = GT
1283 cmpTypeX _ (TyConApp _ _) (FunTy _ _)    = GT
1284 cmpTypeX _ (TyConApp _ _) (LitTy _)      = GT
1285
1286 cmpTypeX _ (ForAllTy _ _) (TyVarTy _)    = GT
1287 cmpTypeX _ (ForAllTy _ _) (AppTy _ _)    = GT
1288 cmpTypeX _ (ForAllTy _ _) (FunTy _ _)    = GT
1289 cmpTypeX _ (ForAllTy _ _) (LitTy _)      = GT
1290 cmpTypeX _ (ForAllTy _ _) (TyConApp _ _) = GT
1291
1292 cmpTypeX _ _              _              = LT
1293
1294 -------------
1295 cmpTypesX :: RnEnv2 -> [Type] -> [Type] -> Ordering
1296 cmpTypesX _   []        []        = EQ
1297 cmpTypesX env (t1:tys1) (t2:tys2) = cmpTypeX env t1 t2 `thenCmp` cmpTypesX env tys1 tys2
1298 cmpTypesX _   []        _         = LT
1299 cmpTypesX _   _         []        = GT
1300
1301 -------------
1302 cmpTc :: TyCon -> TyCon -> Ordering
1303 -- Here we treat * and Constraint as equal
1304 -- See Note [Kind Constraint and kind *] in Kinds.lhs
1305 --
1306 -- Also we treat OpenTypeKind as equal to either * or #
1307 -- See Note [Comparison with OpenTypeKind]
1308 cmpTc tc1 tc2 
1309   | u1 == openTypeKindTyConKey, isSubOpenTypeKindKey u2 = EQ
1310   | u2 == openTypeKindTyConKey, isSubOpenTypeKindKey u1 = EQ
1311   | otherwise = nu1 `compare` nu2
1312   where
1313     u1  = tyConUnique tc1
1314     nu1 = if u1==constraintKindTyConKey then liftedTypeKindTyConKey else u1
1315     u2  = tyConUnique tc2
1316     nu2 = if u2==constraintKindTyConKey then liftedTypeKindTyConKey else u2
1317 \end{code}
1318
1319 Note [Comparison with OpenTypeKind]
1320 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1321 In PrimOpWrappers we have things like
1322    PrimOpWrappers.mkWeak# = /\ a b c. Prim.mkWeak# a b c
1323 where
1324    Prim.mkWeak# :: forall (a:Open) b c. a -> b -> c 
1325                                      -> State# RealWorld -> (# State# RealWorld, Weak# b #)
1326 Now, eta reduction will turn the definition into
1327      PrimOpWrappers.mkWeak# = Prim.mkWeak#
1328 which is kind-of OK, but now the types aren't really equal.  So HACK HACK
1329 we pretend (in Core) that Open is equal to * or #.  I hate this.
1330
1331 Note [cmpTypeX]
1332 ~~~~~~~~~~~~~~~
1333
1334 When we compare foralls, we should look at the kinds. But if we do so,
1335 we get a corelint error like the following (in
1336 libraries/ghc-prim/GHC/PrimopWrappers.hs):
1337
1338     Binder's type: forall (o_abY :: *).
1339                    o_abY
1340                    -> GHC.Prim.State# GHC.Prim.RealWorld
1341                    -> GHC.Prim.State# GHC.Prim.RealWorld
1342     Rhs type: forall (a_12 :: ?).
1343               a_12
1344               -> GHC.Prim.State# GHC.Prim.RealWorld
1345               -> GHC.Prim.State# GHC.Prim.RealWorld
1346
1347 This is why we don't look at the kind. Maybe we should look if the
1348 kinds are compatible.
1349
1350 -- cmpTypeX env (ForAllTy tv1 t1)   (ForAllTy tv2 t2)
1351 --   = cmpTypeX env (tyVarKind tv1) (tyVarKind tv2) `thenCmp`
1352 --     cmpTypeX (rnBndr2 env tv1 tv2) t1 t2
1353
1354 %************************************************************************
1355 %*                                                                      *
1356                 Type substitutions
1357 %*                                                                      *
1358 %************************************************************************
1359
1360 \begin{code}
1361 emptyTvSubstEnv :: TvSubstEnv
1362 emptyTvSubstEnv = emptyVarEnv
1363
1364 composeTvSubst :: InScopeSet -> TvSubstEnv -> TvSubstEnv -> TvSubstEnv
1365 -- ^ @(compose env1 env2)(x)@ is @env1(env2(x))@; i.e. apply @env2@ then @env1@.
1366 -- It assumes that both are idempotent.
1367 -- Typically, @env1@ is the refinement to a base substitution @env2@
1368 composeTvSubst in_scope env1 env2
1369   = env1 `plusVarEnv` mapVarEnv (substTy subst1) env2
1370         -- First apply env1 to the range of env2
1371         -- Then combine the two, making sure that env1 loses if
1372         -- both bind the same variable; that's why env1 is the
1373         --  *left* argument to plusVarEnv, because the right arg wins
1374   where
1375     subst1 = TvSubst in_scope env1
1376
1377 emptyTvSubst :: TvSubst
1378 emptyTvSubst = TvSubst emptyInScopeSet emptyTvSubstEnv
1379
1380 isEmptyTvSubst :: TvSubst -> Bool
1381          -- See Note [Extending the TvSubstEnv] in TypeRep
1382 isEmptyTvSubst (TvSubst _ tenv) = isEmptyVarEnv tenv
1383
1384 mkTvSubst :: InScopeSet -> TvSubstEnv -> TvSubst
1385 mkTvSubst = TvSubst
1386
1387 getTvSubstEnv :: TvSubst -> TvSubstEnv
1388 getTvSubstEnv (TvSubst _ env) = env
1389
1390 getTvInScope :: TvSubst -> InScopeSet
1391 getTvInScope (TvSubst in_scope _) = in_scope
1392
1393 isInScope :: Var -> TvSubst -> Bool
1394 isInScope v (TvSubst in_scope _) = v `elemInScopeSet` in_scope
1395
1396 notElemTvSubst :: CoVar -> TvSubst -> Bool
1397 notElemTvSubst v (TvSubst _ tenv) = not (v `elemVarEnv` tenv)
1398
1399 setTvSubstEnv :: TvSubst -> TvSubstEnv -> TvSubst
1400 setTvSubstEnv (TvSubst in_scope _) tenv = TvSubst in_scope tenv
1401
1402 zapTvSubstEnv :: TvSubst -> TvSubst
1403 zapTvSubstEnv (TvSubst in_scope _) = TvSubst in_scope emptyVarEnv
1404
1405 extendTvInScope :: TvSubst -> Var -> TvSubst
1406 extendTvInScope (TvSubst in_scope tenv) var = TvSubst (extendInScopeSet in_scope var) tenv
1407
1408 extendTvInScopeList :: TvSubst -> [Var] -> TvSubst
1409 extendTvInScopeList (TvSubst in_scope tenv) vars = TvSubst (extendInScopeSetList in_scope vars) tenv
1410
1411 extendTvSubst :: TvSubst -> TyVar -> Type -> TvSubst
1412 extendTvSubst (TvSubst in_scope tenv) tv ty = TvSubst in_scope (extendVarEnv tenv tv ty)
1413
1414 extendTvSubstList :: TvSubst -> [TyVar] -> [Type] -> TvSubst
1415 extendTvSubstList (TvSubst in_scope tenv) tvs tys
1416   = TvSubst in_scope (extendVarEnvList tenv (tvs `zip` tys))
1417
1418 unionTvSubst :: TvSubst -> TvSubst -> TvSubst
1419 -- Works when the ranges are disjoint
1420 unionTvSubst (TvSubst in_scope1 tenv1) (TvSubst in_scope2 tenv2)
1421   = ASSERT( not (tenv1 `intersectsVarEnv` tenv2) )
1422     TvSubst (in_scope1 `unionInScope` in_scope2)
1423             (tenv1     `plusVarEnv`   tenv2)
1424
1425 -- mkOpenTvSubst and zipOpenTvSubst generate the in-scope set from
1426 -- the types given; but it's just a thunk so with a bit of luck
1427 -- it'll never be evaluated
1428
1429 -- Note [Generating the in-scope set for a substitution]
1430 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1431 -- If we want to substitute [a -> ty1, b -> ty2] I used to
1432 -- think it was enough to generate an in-scope set that includes
1433 -- fv(ty1,ty2).  But that's not enough; we really should also take the
1434 -- free vars of the type we are substituting into!  Example:
1435 --      (forall b. (a,b,x)) [a -> List b]
1436 -- Then if we use the in-scope set {b}, there is a danger we will rename
1437 -- the forall'd variable to 'x' by mistake, getting this:
1438 --      (forall x. (List b, x, x)
1439 -- Urk!  This means looking at all the calls to mkOpenTvSubst....
1440
1441
1442 -- | Generates the in-scope set for the 'TvSubst' from the types in the incoming
1443 -- environment, hence "open"
1444 mkOpenTvSubst :: TvSubstEnv -> TvSubst
1445 mkOpenTvSubst tenv = TvSubst (mkInScopeSet (tyVarsOfTypes (varEnvElts tenv))) tenv
1446
1447 -- | Generates the in-scope set for the 'TvSubst' from the types in the incoming
1448 -- environment, hence "open"
1449 zipOpenTvSubst :: [TyVar] -> [Type] -> TvSubst
1450 zipOpenTvSubst tyvars tys
1451   | debugIsOn && (length tyvars /= length tys)
1452   = pprTrace "zipOpenTvSubst" (ppr tyvars $$ ppr tys) emptyTvSubst
1453   | otherwise
1454   = TvSubst (mkInScopeSet (tyVarsOfTypes tys)) (zipTyEnv tyvars tys)
1455
1456 -- | Called when doing top-level substitutions. Here we expect that the
1457 -- free vars of the range of the substitution will be empty.
1458 mkTopTvSubst :: [(TyVar, Type)] -> TvSubst
1459 mkTopTvSubst prs = TvSubst emptyInScopeSet (mkVarEnv prs)
1460
1461 zipTopTvSubst :: [TyVar] -> [Type] -> TvSubst
1462 zipTopTvSubst tyvars tys
1463   | debugIsOn && (length tyvars /= length tys)
1464   = pprTrace "zipTopTvSubst" (ppr tyvars $$ ppr tys) emptyTvSubst
1465   | otherwise
1466   = TvSubst emptyInScopeSet (zipTyEnv tyvars tys)
1467
1468 zipTyEnv :: [TyVar] -> [Type] -> TvSubstEnv
1469 zipTyEnv tyvars tys
1470   | debugIsOn && (length tyvars /= length tys)
1471   = pprTrace "zipTyEnv" (ppr tyvars $$ ppr tys) emptyVarEnv
1472   | otherwise
1473   = zip_ty_env tyvars tys emptyVarEnv
1474
1475 -- Later substitutions in the list over-ride earlier ones,
1476 -- but there should be no loops
1477 zip_ty_env :: [TyVar] -> [Type] -> TvSubstEnv -> TvSubstEnv
1478 zip_ty_env []       []       env = env
1479 zip_ty_env (tv:tvs) (ty:tys) env = zip_ty_env tvs tys (extendVarEnv env tv ty)
1480         -- There used to be a special case for when
1481         --      ty == TyVarTy tv
1482         -- (a not-uncommon case) in which case the substitution was dropped.
1483         -- But the type-tidier changes the print-name of a type variable without
1484         -- changing the unique, and that led to a bug.   Why?  Pre-tidying, we had
1485         -- a type {Foo t}, where Foo is a one-method class.  So Foo is really a newtype.
1486         -- And it happened that t was the type variable of the class.  Post-tiding,
1487         -- it got turned into {Foo t2}.  The ext-core printer expanded this using
1488         -- sourceTypeRep, but that said "Oh, t == t2" because they have the same unique,
1489         -- and so generated a rep type mentioning t not t2.
1490         --
1491         -- Simplest fix is to nuke the "optimisation"
1492 zip_ty_env tvs      tys      env   = pprTrace "Var/Type length mismatch: " (ppr tvs $$ ppr tys) env
1493 -- zip_ty_env _ _ env = env
1494
1495 instance Outputable TvSubst where
1496   ppr (TvSubst ins tenv)
1497     = brackets $ sep[ ptext (sLit "TvSubst"),
1498                       nest 2 (ptext (sLit "In scope:") <+> ppr ins),
1499                       nest 2 (ptext (sLit "Type env:") <+> ppr tenv) ]
1500 \end{code}
1501
1502 %************************************************************************
1503 %*                                                                      *
1504                 Performing type or kind substitutions
1505 %*                                                                      *
1506 %************************************************************************
1507
1508 \begin{code}
1509 -- | Type substitution making use of an 'TvSubst' that
1510 -- is assumed to be open, see 'zipOpenTvSubst'
1511 substTyWith :: [TyVar] -> [Type] -> Type -> Type
1512 substTyWith tvs tys = ASSERT( length tvs == length tys )
1513                       substTy (zipOpenTvSubst tvs tys)
1514
1515 substKiWith :: [KindVar] -> [Kind] -> Kind -> Kind
1516 substKiWith = substTyWith
1517
1518 -- | Type substitution making use of an 'TvSubst' that
1519 -- is assumed to be open, see 'zipOpenTvSubst'
1520 substTysWith :: [TyVar] -> [Type] -> [Type] -> [Type]
1521 substTysWith tvs tys = ASSERT( length tvs == length tys )
1522                        substTys (zipOpenTvSubst tvs tys)
1523
1524 substKisWith :: [KindVar] -> [Kind] -> [Kind] -> [Kind]
1525 substKisWith = substTysWith
1526
1527 -- | Substitute within a 'Type'
1528 substTy :: TvSubst -> Type  -> Type
1529 substTy subst ty | isEmptyTvSubst subst = ty
1530                  | otherwise            = subst_ty subst ty
1531
1532 -- | Substitute within several 'Type's
1533 substTys :: TvSubst -> [Type] -> [Type]
1534 substTys subst tys | isEmptyTvSubst subst = tys
1535                    | otherwise            = map (subst_ty subst) tys
1536
1537 -- | Substitute within a 'ThetaType'
1538 substTheta :: TvSubst -> ThetaType -> ThetaType
1539 substTheta subst theta
1540   | isEmptyTvSubst subst = theta
1541   | otherwise            = map (substTy subst) theta
1542
1543 -- | Remove any nested binders mentioning the 'TyVar's in the 'TyVarSet'
1544 deShadowTy :: TyVarSet -> Type -> Type
1545 deShadowTy tvs ty
1546   = subst_ty (mkTvSubst in_scope emptyTvSubstEnv) ty
1547   where
1548     in_scope = mkInScopeSet tvs
1549
1550 subst_ty :: TvSubst -> Type -> Type
1551 -- subst_ty is the main workhorse for type substitution
1552 --
1553 -- Note that the in_scope set is poked only if we hit a forall
1554 -- so it may often never be fully computed
1555 subst_ty subst ty
1556    = go ty
1557   where
1558     go (LitTy n)         = n `seq` LitTy n
1559     go (TyVarTy tv)      = substTyVar subst tv
1560     go (TyConApp tc tys) = let args = map go tys
1561                            in  args `seqList` TyConApp tc args
1562
1563     go (FunTy arg res)   = (FunTy $! (go arg)) $! (go res)
1564     go (AppTy fun arg)   = mkAppTy (go fun) $! (go arg)
1565                 -- The mkAppTy smart constructor is important
1566                 -- we might be replacing (a Int), represented with App
1567                 -- by [Int], represented with TyConApp
1568     go (ForAllTy tv ty)  = case substTyVarBndr subst tv of
1569                               (subst', tv') ->
1570                                  ForAllTy tv' $! (subst_ty subst' ty)
1571
1572 substTyVar :: TvSubst -> TyVar  -> Type
1573 substTyVar (TvSubst _ tenv) tv
1574   | Just ty  <- lookupVarEnv tenv tv      = ty  -- See Note [Apply Once]
1575   | otherwise = ASSERT( isTyVar tv ) TyVarTy tv --     in TypeRep
1576   -- We do not require that the tyvar is in scope
1577   -- Reason: we do quite a bit of (substTyWith [tv] [ty] tau)
1578   -- and it's a nuisance to bring all the free vars of tau into
1579   -- scope --- and then force that thunk at every tyvar
1580   -- Instead we have an ASSERT in substTyVarBndr to check for capture
1581
1582 substTyVars :: TvSubst -> [TyVar] -> [Type]
1583 substTyVars subst tvs = map (substTyVar subst) tvs
1584
1585 lookupTyVar :: TvSubst -> TyVar  -> Maybe Type
1586         -- See Note [Extending the TvSubst] in TypeRep
1587 lookupTyVar (TvSubst _ tenv) tv = lookupVarEnv tenv tv
1588
1589 substTyVarBndr :: TvSubst -> TyVar -> (TvSubst, TyVar)
1590 substTyVarBndr subst@(TvSubst in_scope tenv) old_var
1591   = ASSERT2( _no_capture, ppr old_var $$ ppr subst )
1592     (TvSubst (in_scope `extendInScopeSet` new_var) new_env, new_var)
1593   where
1594     new_env | no_change = delVarEnv tenv old_var
1595             | otherwise = extendVarEnv tenv old_var (TyVarTy new_var)
1596
1597     _no_capture = not (new_var `elemVarSet` tyVarsOfTypes (varEnvElts tenv))
1598     -- Assertion check that we are not capturing something in the substitution
1599
1600     old_ki = tyVarKind old_var
1601     no_kind_change = isEmptyVarSet (tyVarsOfType old_ki) -- verify that kind is closed
1602     no_change = no_kind_change && (new_var == old_var)
1603         -- no_change means that the new_var is identical in
1604         -- all respects to the old_var (same unique, same kind)
1605         -- See Note [Extending the TvSubst] in TypeRep
1606         --
1607         -- In that case we don't need to extend the substitution
1608         -- to map old to new.  But instead we must zap any
1609         -- current substitution for the variable. For example:
1610         --      (\x.e) with id_subst = [x |-> e']
1611         -- Here we must simply zap the substitution for x
1612
1613     new_var | no_kind_change = uniqAway in_scope old_var
1614             | otherwise = uniqAway in_scope $ updateTyVarKind (substTy subst) old_var
1615         -- The uniqAway part makes sure the new variable is not already in scope
1616
1617 cloneTyVarBndr :: TvSubst -> TyVar -> Unique -> (TvSubst, TyVar)
1618 cloneTyVarBndr (TvSubst in_scope tv_env) tv uniq
1619   = (TvSubst (extendInScopeSet in_scope tv')
1620              (extendVarEnv tv_env tv (mkTyVarTy tv')), tv')
1621   where
1622     tv' = setVarUnique tv uniq  -- Simply set the unique; the kind
1623                                 -- has no type variables to worry about
1624 \end{code}
1625
1626 ----------------------------------------------------
1627 -- Kind Stuff
1628
1629 Kinds
1630 ~~~~~
1631
1632 For the description of subkinding in GHC, see
1633   http://ghc.haskell.org/trac/ghc/wiki/Commentary/Compiler/TypeType#Kinds
1634
1635 \begin{code}
1636 type MetaKindVar = TyVar  -- invariant: MetaKindVar will always be a
1637                           -- TcTyVar with details MetaTv (TauTv ...) ...
1638 -- meta kind var constructors and functions are in TcType
1639
1640 type SimpleKind = Kind
1641 \end{code}
1642
1643 %************************************************************************
1644 %*                                                                      *
1645         The kind of a type
1646 %*                                                                      *
1647 %************************************************************************
1648
1649 \begin{code}
1650 typeKind :: Type -> Kind
1651 typeKind orig_ty = go orig_ty
1652   where
1653     
1654     go ty@(TyConApp tc tys)
1655       | isPromotedTyCon tc
1656       = ASSERT( tyConArity tc == length tys ) superKind
1657       | otherwise
1658       = kindAppResult (ptext (sLit "typeKind 1") <+> ppr ty $$ ppr orig_ty)
1659                       (tyConKind tc) tys
1660
1661     go ty@(AppTy fun arg)   = kindAppResult (ptext (sLit "typeKind 2") <+> ppr ty $$ ppr orig_ty)
1662                                             (go fun) [arg]
1663     go (LitTy l)            = typeLiteralKind l
1664     go (ForAllTy _ ty)      = go ty
1665     go (TyVarTy tyvar)      = tyVarKind tyvar
1666     go _ty@(FunTy _arg res)
1667         -- Hack alert.  The kind of (Int -> Int#) is liftedTypeKind (*),
1668         --              not unliftedTypeKind (#)
1669         -- The only things that can be after a function arrow are
1670         --   (a) types (of kind openTypeKind or its sub-kinds)
1671         --   (b) kinds (of super-kind TY) (e.g. * -> (* -> *))
1672         | isSuperKind k         = k
1673         | otherwise             = ASSERT2( isSubOpenTypeKind k, ppr _ty $$ ppr k ) liftedTypeKind
1674         where
1675           k = go res
1676
1677 typeLiteralKind :: TyLit -> Kind
1678 typeLiteralKind l =
1679   case l of
1680     NumTyLit _ -> typeNatKind
1681     StrTyLit _ -> typeSymbolKind
1682 \end{code}
1683
1684 Kind inference
1685 ~~~~~~~~~~~~~~
1686 During kind inference, a kind variable unifies only with
1687 a "simple kind", sk
1688         sk ::= * | sk1 -> sk2
1689 For example
1690         data T a = MkT a (T Int#)
1691 fails.  We give T the kind (k -> *), and the kind variable k won't unify
1692 with # (the kind of Int#).
1693
1694 Type inference
1695 ~~~~~~~~~~~~~~
1696 When creating a fresh internal type variable, we give it a kind to express
1697 constraints on it.  E.g. in (\x->e) we make up a fresh type variable for x,
1698 with kind ??.
1699
1700 During unification we only bind an internal type variable to a type
1701 whose kind is lower in the sub-kind hierarchy than the kind of the tyvar.
1702
1703 When unifying two internal type variables, we collect their kind constraints by
1704 finding the GLB of the two.  Since the partial order is a tree, they only
1705 have a glb if one is a sub-kind of the other.  In that case, we bind the
1706 less-informative one to the more informative one.  Neat, eh?