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