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