Two small refactorings
[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, FlexibleContexts #-}
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, ArgFlag(..), KindOrType, PredType, ThetaType,
18 Var, TyVar, isTyVar, TyCoVar, TyBinder, TyVarBinder,
19
20 -- ** Constructing and deconstructing types
21 mkTyVarTy, mkTyVarTys, getTyVar, getTyVar_maybe, repGetTyVar_maybe,
22 getCastedTyVar_maybe, tyVarKind,
23
24 mkAppTy, mkAppTys, splitAppTy, splitAppTys, repSplitAppTys,
25 splitAppTy_maybe, repSplitAppTy_maybe, tcRepSplitAppTy_maybe,
26
27 mkFunTy, mkFunTys, splitFunTy, splitFunTy_maybe,
28 splitFunTys, funResultTy, funArgTy,
29
30 mkTyConApp, mkTyConTy,
31 tyConAppTyCon_maybe, tyConAppTyConPicky_maybe,
32 tyConAppArgs_maybe, tyConAppTyCon, tyConAppArgs,
33 splitTyConApp_maybe, splitTyConApp, tyConAppArgN, nextRole,
34 tcRepSplitTyConApp_maybe, tcSplitTyConApp_maybe,
35 splitListTyConApp_maybe,
36 repSplitTyConApp_maybe,
37
38 mkForAllTy, mkForAllTys, mkInvForAllTys, mkSpecForAllTys,
39 mkVisForAllTys, mkInvForAllTy,
40 splitForAllTys, splitForAllTyVarBndrs,
41 splitForAllTy_maybe, splitForAllTy,
42 splitPiTy_maybe, splitPiTy, splitPiTys,
43 mkPiTy, mkPiTys, mkTyConBindersPreferAnon,
44 mkLamType, mkLamTypes,
45 piResultTy, piResultTys,
46 applyTysX, dropForAlls,
47
48 mkNumLitTy, isNumLitTy,
49 mkStrLitTy, isStrLitTy,
50
51 getRuntimeRep_maybe, getRuntimeRepFromKind_maybe,
52
53 mkCastTy, mkCoercionTy, splitCastTy_maybe,
54
55 userTypeError_maybe, pprUserTypeErrorTy,
56
57 coAxNthLHS,
58 stripCoercionTy, splitCoercionType_maybe,
59
60 splitPiTysInvisible, filterOutInvisibleTypes,
61 partitionInvisibles,
62 synTyConResKind,
63
64 modifyJoinResTy, setJoinResTy,
65
66 -- Analyzing types
67 TyCoMapper(..), mapType, mapCoercion,
68
69 -- (Newtypes)
70 newTyConInstRhs,
71
72 -- Pred types
73 mkFamilyTyConApp,
74 isDictLikeTy,
75 mkPrimEqPred, mkReprPrimEqPred, mkPrimEqPredRole,
76 equalityTyCon,
77 mkHeteroPrimEqPred, mkHeteroReprPrimEqPred,
78 mkClassPred,
79 isClassPred, isEqPred, isNomEqPred,
80 isIPPred, isIPPred_maybe, isIPTyCon, isIPClass,
81 isCTupleClass,
82
83 -- Deconstructing predicate types
84 PredTree(..), EqRel(..), eqRelRole, classifyPredType,
85 getClassPredTys, getClassPredTys_maybe,
86 getEqPredTys, getEqPredTys_maybe, getEqPredRole,
87 predTypeEqRel,
88
89 -- ** Binders
90 sameVis,
91 mkTyVarBinder, mkTyVarBinders,
92 mkAnonBinder,
93 isAnonTyBinder, isNamedTyBinder,
94 binderVar, binderVars, binderKind, binderArgFlag,
95 tyBinderType, tyBinderVar_maybe,
96 binderRelevantType_maybe, caseBinder,
97 isVisibleArgFlag, isInvisibleArgFlag, isVisibleBinder, isInvisibleBinder,
98 tyConBindersTyBinders,
99
100 -- ** Common type constructors
101 funTyCon,
102
103 -- ** Predicates on types
104 isTyVarTy, isFunTy, isDictTy, isPredTy, isCoercionTy,
105 isCoercionTy_maybe, isCoercionType, isForAllTy,
106 isPiTy, isTauTy, isFamFreeTy,
107
108 isValidJoinPointType,
109
110 -- (Lifting and boxity)
111 isLiftedType_maybe, isUnliftedType, isUnboxedTupleType, isUnboxedSumType,
112 isAlgType, isDataFamilyAppType,
113 isPrimitiveType, isStrictType,
114 isRuntimeRepTy, isRuntimeRepVar, isRuntimeRepKindedTy,
115 dropRuntimeRepArgs,
116 getRuntimeRep, getRuntimeRepFromKind,
117
118 -- * Main data types representing Kinds
119 Kind,
120
121 -- ** Finding the kind of a type
122 typeKind, isTypeLevPoly, resultIsLevPoly,
123
124 -- ** Common Kind
125 liftedTypeKind,
126
127 -- * Type free variables
128 tyCoFVsOfType, tyCoFVsBndr,
129 tyCoVarsOfType, tyCoVarsOfTypes,
130 tyCoVarsOfTypeDSet,
131 coVarsOfType,
132 coVarsOfTypes, closeOverKinds, closeOverKindsList,
133 noFreeVarsOfType,
134 splitVisVarsOfType, splitVisVarsOfTypes,
135 expandTypeSynonyms,
136 typeSize, occCheckExpand,
137
138 -- * Well-scoped lists of variables
139 dVarSetElemsWellScoped, toposortTyVars, tyCoVarsOfTypeWellScoped,
140 tyCoVarsOfTypesWellScoped,
141
142 -- * Type comparison
143 eqType, eqTypeX, eqTypes, nonDetCmpType, nonDetCmpTypes, nonDetCmpTypeX,
144 nonDetCmpTypesX, nonDetCmpTc,
145 eqVarBndrs,
146
147 -- * Forcing evaluation of types
148 seqType, seqTypes,
149
150 -- * Other views onto Types
151 coreView, tcView,
152
153 tyConsOfType,
154
155 -- * Main type substitution data types
156 TvSubstEnv, -- Representation widely visible
157 TCvSubst(..), -- Representation visible to a few friends
158
159 -- ** Manipulating type substitutions
160 emptyTvSubstEnv, emptyTCvSubst, mkEmptyTCvSubst,
161
162 mkTCvSubst, zipTvSubst, mkTvSubstPrs,
163 notElemTCvSubst,
164 getTvSubstEnv, setTvSubstEnv,
165 zapTCvSubst, getTCvInScope, getTCvSubstRangeFVs,
166 extendTCvInScope, extendTCvInScopeList, extendTCvInScopeSet,
167 extendTCvSubst, extendCvSubst,
168 extendTvSubst, extendTvSubstBinderAndInScope,
169 extendTvSubstList, extendTvSubstAndInScope,
170 extendTvSubstWithClone,
171 isInScope, composeTCvSubstEnv, composeTCvSubst, zipTyEnv, zipCoEnv,
172 isEmptyTCvSubst, unionTCvSubst,
173
174 -- ** Performing substitution on types and kinds
175 substTy, substTys, substTyWith, substTysWith, substTheta,
176 substTyAddInScope,
177 substTyUnchecked, substTysUnchecked, substThetaUnchecked,
178 substTyWithUnchecked,
179 substCoUnchecked, substCoWithUnchecked,
180 substTyVarBndr, substTyVarBndrs, substTyVar, substTyVars,
181 cloneTyVarBndr, cloneTyVarBndrs, lookupTyVar,
182
183 -- * Pretty-printing
184 pprType, pprParendType, pprPrecType,
185 pprTypeApp, pprTyThingCategory, pprShortTyThing,
186 pprTvBndr, pprTvBndrs, pprForAll, pprUserForAll,
187 pprSigmaType, ppSuggestExplicitKinds,
188 pprTheta, pprThetaArrowTy, pprClassPred,
189 pprKind, pprParendKind, pprSourceTyCon,
190 PprPrec(..), topPrec, sigPrec, opPrec, funPrec, appPrec, maybeParen,
191 pprTyVar, pprTyVars,
192 pprWithTYPE,
193
194 -- * Tidying type related things up for printing
195 tidyType, tidyTypes,
196 tidyOpenType, tidyOpenTypes,
197 tidyOpenKind,
198 tidyTyCoVarBndr, tidyTyCoVarBndrs, tidyFreeTyCoVars,
199 tidyOpenTyCoVar, tidyOpenTyCoVars,
200 tidyTyVarOcc,
201 tidyTopType,
202 tidyKind,
203 tidyTyVarBinder, tidyTyVarBinders
204 ) where
205
206 #include "HsVersions.h"
207
208 import GhcPrelude
209
210 import BasicTypes
211
212 -- We import the representation and primitive functions from TyCoRep.
213 -- Many things are reexported, but not the representation!
214
215 import Kind
216 import TyCoRep
217
218 -- friends:
219 import Var
220 import VarEnv
221 import VarSet
222 import UniqSet
223
224 import Class
225 import TyCon
226 import TysPrim
227 import {-# SOURCE #-} TysWiredIn ( listTyCon, typeNatKind
228 , typeSymbolKind, liftedTypeKind )
229 import PrelNames
230 import CoAxiom
231 import {-# SOURCE #-} Coercion
232
233 -- others
234 import Util
235 import Outputable
236 import FastString
237 import Pair
238 import DynFlags ( gopt_set, GeneralFlag(Opt_PrintExplicitRuntimeReps) )
239 import ListSetOps
240 import Digraph
241 import Unique ( nonDetCmpUnique )
242
243 import Maybes ( orElse )
244 import Data.Maybe ( isJust, mapMaybe )
245 import Control.Monad ( guard )
246 import Control.Arrow ( first, second )
247
248 -- $type_classification
249 -- #type_classification#
250 --
251 -- Types are one of:
252 --
253 -- [Unboxed] Iff its representation is other than a pointer
254 -- Unboxed types are also unlifted.
255 --
256 -- [Lifted] Iff it has bottom as an element.
257 -- Closures always have lifted types: i.e. any
258 -- let-bound identifier in Core must have a lifted
259 -- type. Operationally, a lifted object is one that
260 -- can be entered.
261 -- Only lifted types may be unified with a type variable.
262 --
263 -- [Algebraic] Iff it is a type with one or more constructors, whether
264 -- declared with @data@ or @newtype@.
265 -- An algebraic type is one that can be deconstructed
266 -- with a case expression. This is /not/ the same as
267 -- lifted types, because we also include unboxed
268 -- tuples in this classification.
269 --
270 -- [Data] Iff it is a type declared with @data@, or a boxed tuple.
271 --
272 -- [Primitive] Iff it is a built-in type that can't be expressed in Haskell.
273 --
274 -- Currently, all primitive types are unlifted, but that's not necessarily
275 -- the case: for example, @Int@ could be primitive.
276 --
277 -- Some primitive types are unboxed, such as @Int#@, whereas some are boxed
278 -- but unlifted (such as @ByteArray#@). The only primitive types that we
279 -- classify as algebraic are the unboxed tuples.
280 --
281 -- Some examples of type classifications that may make this a bit clearer are:
282 --
283 -- @
284 -- Type primitive boxed lifted algebraic
285 -- -----------------------------------------------------------------------------
286 -- Int# Yes No No No
287 -- ByteArray# Yes Yes No No
288 -- (\# a, b \#) Yes No No Yes
289 -- (\# a | b \#) Yes No No Yes
290 -- ( a, b ) No Yes Yes Yes
291 -- [a] No Yes Yes Yes
292 -- @
293
294 -- $representation_types
295 -- A /source type/ is a type that is a separate type as far as the type checker is
296 -- concerned, but which has a more low-level representation as far as Core-to-Core
297 -- passes and the rest of the back end is concerned.
298 --
299 -- You don't normally have to worry about this, as the utility functions in
300 -- this module will automatically convert a source into a representation type
301 -- if they are spotted, to the best of it's abilities. If you don't want this
302 -- to happen, use the equivalent functions from the "TcType" module.
303
304 {-
305 ************************************************************************
306 * *
307 Type representation
308 * *
309 ************************************************************************
310
311 Note [coreView vs tcView]
312 ~~~~~~~~~~~~~~~~~~~~~~~~~
313 So far as the typechecker is concerned, 'Constraint' and 'TYPE LiftedRep' are distinct kinds.
314
315 But in Core these two are treated as identical.
316
317 We implement this by making 'coreView' convert 'Constraint' to 'TYPE LiftedRep' on the fly.
318 The function tcView (used in the type checker) does not do this.
319
320 See also Trac #11715, which tracks removing this inconsistency.
321
322 -}
323
324 {-# INLINE coreView #-}
325 coreView :: Type -> Maybe Type
326 -- ^ This function Strips off the /top layer only/ of a type synonym
327 -- application (if any) its underlying representation type.
328 -- Returns Nothing if there is nothing to look through.
329 -- This function considers 'Constraint' to be a synonym of @TYPE LiftedRep@.
330 --
331 -- By being non-recursive and inlined, this case analysis gets efficiently
332 -- joined onto the case analysis that the caller is already doing
333 coreView (TyConApp tc tys) | Just (tenv, rhs, tys') <- expandSynTyCon_maybe tc tys
334 = Just (mkAppTys (substTy (mkTvSubstPrs tenv) rhs) tys')
335 -- The free vars of 'rhs' should all be bound by 'tenv', so it's
336 -- ok to use 'substTy' here.
337 -- See also Note [The substitution invariant] in TyCoRep.
338 -- Its important to use mkAppTys, rather than (foldl AppTy),
339 -- because the function part might well return a
340 -- partially-applied type constructor; indeed, usually will!
341
342 coreView (TyConApp tc []) -- At the Core level, Constraint = Type
343 | isConstraintKindCon tc
344 = Just liftedTypeKind
345
346 coreView _ = Nothing
347
348 -- | Gives the typechecker view of a type. This unwraps synonyms but
349 -- leaves 'Constraint' alone. c.f. coreView, which turns Constraint into
350 -- TYPE LiftedRep. Returns Nothing if no unwrapping happens.
351 -- See also Note [coreView vs tcView] in Type.
352 {-# INLINE tcView #-}
353 tcView :: Type -> Maybe Type
354 tcView (TyConApp tc tys) | Just (tenv, rhs, tys') <- expandSynTyCon_maybe tc tys
355 = Just (mkAppTys (substTy (mkTvSubstPrs tenv) rhs) tys')
356 -- The free vars of 'rhs' should all be bound by 'tenv', so it's
357 -- ok to use 'substTy' here.
358 -- See also Note [The substitution invariant] in TyCoRep.
359 -- Its important to use mkAppTys, rather than (foldl AppTy),
360 -- because the function part might well return a
361 -- partially-applied type constructor; indeed, usually will!
362 tcView _ = Nothing
363
364 -----------------------------------------------
365 expandTypeSynonyms :: Type -> Type
366 -- ^ Expand out all type synonyms. Actually, it'd suffice to expand out
367 -- just the ones that discard type variables (e.g. type Funny a = Int)
368 -- But we don't know which those are currently, so we just expand all.
369 --
370 -- 'expandTypeSynonyms' only expands out type synonyms mentioned in the type,
371 -- not in the kinds of any TyCon or TyVar mentioned in the type.
372 --
373 -- Keep this synchronized with 'synonymTyConsOfType'
374 expandTypeSynonyms ty
375 = go (mkEmptyTCvSubst in_scope) ty
376 where
377 in_scope = mkInScopeSet (tyCoVarsOfType ty)
378
379 go subst (TyConApp tc tys)
380 | Just (tenv, rhs, tys') <- expandSynTyCon_maybe tc expanded_tys
381 = let subst' = mkTvSubst in_scope (mkVarEnv tenv)
382 -- Make a fresh substitution; rhs has nothing to
383 -- do with anything that has happened so far
384 -- NB: if you make changes here, be sure to build an
385 -- /idempotent/ substitution, even in the nested case
386 -- type T a b = a -> b
387 -- type S x y = T y x
388 -- (Trac #11665)
389 in mkAppTys (go subst' rhs) tys'
390 | otherwise
391 = TyConApp tc expanded_tys
392 where
393 expanded_tys = (map (go subst) tys)
394
395 go _ (LitTy l) = LitTy l
396 go subst (TyVarTy tv) = substTyVar subst tv
397 go subst (AppTy t1 t2) = mkAppTy (go subst t1) (go subst t2)
398 go subst (FunTy arg res)
399 = mkFunTy (go subst arg) (go subst res)
400 go subst (ForAllTy (TvBndr tv vis) t)
401 = let (subst', tv') = substTyVarBndrUsing go subst tv in
402 ForAllTy (TvBndr tv' vis) (go subst' t)
403 go subst (CastTy ty co) = mkCastTy (go subst ty) (go_co subst co)
404 go subst (CoercionTy co) = mkCoercionTy (go_co subst co)
405
406 go_co subst (Refl r ty)
407 = mkReflCo r (go subst ty)
408 -- NB: coercions are always expanded upon creation
409 go_co subst (TyConAppCo r tc args)
410 = mkTyConAppCo r tc (map (go_co subst) args)
411 go_co subst (AppCo co arg)
412 = mkAppCo (go_co subst co) (go_co subst arg)
413 go_co subst (ForAllCo tv kind_co co)
414 = let (subst', tv', kind_co') = go_cobndr subst tv kind_co in
415 mkForAllCo tv' kind_co' (go_co subst' co)
416 go_co subst (FunCo r co1 co2)
417 = mkFunCo r (go_co subst co1) (go_co subst co2)
418 go_co subst (CoVarCo cv)
419 = substCoVar subst cv
420 go_co subst (AxiomInstCo ax ind args)
421 = mkAxiomInstCo ax ind (map (go_co subst) args)
422 go_co subst (UnivCo p r t1 t2)
423 = mkUnivCo (go_prov subst p) r (go subst t1) (go subst t2)
424 go_co subst (SymCo co)
425 = mkSymCo (go_co subst co)
426 go_co subst (TransCo co1 co2)
427 = mkTransCo (go_co subst co1) (go_co subst co2)
428 go_co subst (NthCo r n co)
429 = mkNthCo r n (go_co subst co)
430 go_co subst (LRCo lr co)
431 = mkLRCo lr (go_co subst co)
432 go_co subst (InstCo co arg)
433 = mkInstCo (go_co subst co) (go_co subst arg)
434 go_co subst (CoherenceCo co1 co2)
435 = mkCoherenceCo (go_co subst co1) (go_co subst co2)
436 go_co subst (KindCo co)
437 = mkKindCo (go_co subst co)
438 go_co subst (SubCo co)
439 = mkSubCo (go_co subst co)
440 go_co subst (AxiomRuleCo ax cs)
441 = AxiomRuleCo ax (map (go_co subst) cs)
442 go_co _ (HoleCo h)
443 = pprPanic "expandTypeSynonyms hit a hole" (ppr h)
444
445 go_prov _ UnsafeCoerceProv = UnsafeCoerceProv
446 go_prov subst (PhantomProv co) = PhantomProv (go_co subst co)
447 go_prov subst (ProofIrrelProv co) = ProofIrrelProv (go_co subst co)
448 go_prov _ p@(PluginProv _) = p
449
450 -- the "False" and "const" are to accommodate the type of
451 -- substForAllCoBndrUsing, which is general enough to
452 -- handle coercion optimization (which sometimes swaps the
453 -- order of a coercion)
454 go_cobndr subst = substForAllCoBndrUsing False (go_co subst) subst
455
456 {-
457 ************************************************************************
458 * *
459 Analyzing types
460 * *
461 ************************************************************************
462
463 These functions do a map-like operation over types, performing some operation
464 on all variables and binding sites. Primarily used for zonking.
465
466 Note [Efficiency for mapCoercion ForAllCo case]
467 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
468 As noted in Note [Forall coercions] in TyCoRep, a ForAllCo is a bit redundant.
469 It stores a TyVar and a Coercion, where the kind of the TyVar always matches
470 the left-hand kind of the coercion. This is convenient lots of the time, but
471 not when mapping a function over a coercion.
472
473 The problem is that tcm_tybinder will affect the TyVar's kind and
474 mapCoercion will affect the Coercion, and we hope that the results will be
475 the same. Even if they are the same (which should generally happen with
476 correct algorithms), then there is an efficiency issue. In particular,
477 this problem seems to make what should be a linear algorithm into a potentially
478 exponential one. But it's only going to be bad in the case where there's
479 lots of foralls in the kinds of other foralls. Like this:
480
481 forall a : (forall b : (forall c : ...). ...). ...
482
483 This construction seems unlikely. So we'll do the inefficient, easy way
484 for now.
485
486 Note [Specialising mappers]
487 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
488 These INLINABLE pragmas are indispensable. mapType/mapCoercion are used
489 to implement zonking, and it's vital that they get specialised to the TcM
490 monad. This specialisation happens automatically (that is, without a
491 SPECIALISE pragma) as long as the definitions are INLINABLE. For example,
492 this one change made a 20% allocation difference in perf/compiler/T5030.
493
494 -}
495
496 -- | This describes how a "map" operation over a type/coercion should behave
497 data TyCoMapper env m
498 = TyCoMapper
499 { tcm_smart :: Bool -- ^ Should the new type be created with smart
500 -- constructors?
501 , tcm_tyvar :: env -> TyVar -> m Type
502 , tcm_covar :: env -> CoVar -> m Coercion
503 , tcm_hole :: env -> CoercionHole -> m Coercion
504 -- ^ What to do with coercion holes.
505 -- See Note [Coercion holes] in TyCoRep.
506
507 , tcm_tybinder :: env -> TyVar -> ArgFlag -> m (env, TyVar)
508 -- ^ The returned env is used in the extended scope
509 }
510
511 {-# INLINABLE mapType #-} -- See Note [Specialising mappers]
512 mapType :: Monad m => TyCoMapper env m -> env -> Type -> m Type
513 mapType mapper@(TyCoMapper { tcm_smart = smart, tcm_tyvar = tyvar
514 , tcm_tybinder = tybinder })
515 env ty
516 = go ty
517 where
518 go (TyVarTy tv) = tyvar env tv
519 go (AppTy t1 t2) = mkappty <$> go t1 <*> go t2
520 go t@(TyConApp _ []) = return t -- avoid allocation in this exceedingly
521 -- common case (mostly, for *)
522 go (TyConApp tc tys) = mktyconapp tc <$> mapM go tys
523 go (FunTy arg res) = FunTy <$> go arg <*> go res
524 go (ForAllTy (TvBndr tv vis) inner)
525 = do { (env', tv') <- tybinder env tv vis
526 ; inner' <- mapType mapper env' inner
527 ; return $ ForAllTy (TvBndr tv' vis) inner' }
528 go ty@(LitTy {}) = return ty
529 go (CastTy ty co) = mkcastty <$> go ty <*> mapCoercion mapper env co
530 go (CoercionTy co) = CoercionTy <$> mapCoercion mapper env co
531
532 (mktyconapp, mkappty, mkcastty)
533 | smart = (mkTyConApp, mkAppTy, mkCastTy)
534 | otherwise = (TyConApp, AppTy, CastTy)
535
536 {-# INLINABLE mapCoercion #-} -- See Note [Specialising mappers]
537 mapCoercion :: Monad m
538 => TyCoMapper env m -> env -> Coercion -> m Coercion
539 mapCoercion mapper@(TyCoMapper { tcm_smart = smart, tcm_covar = covar
540 , tcm_hole = cohole, tcm_tybinder = tybinder })
541 env co
542 = go co
543 where
544 go (Refl r ty) = Refl r <$> mapType mapper env ty
545 go (TyConAppCo r tc args)
546 = mktyconappco r tc <$> mapM go args
547 go (AppCo c1 c2) = mkappco <$> go c1 <*> go c2
548 go (ForAllCo tv kind_co co)
549 = do { kind_co' <- go kind_co
550 ; (env', tv') <- tybinder env tv Inferred
551 ; co' <- mapCoercion mapper env' co
552 ; return $ mkforallco tv' kind_co' co' }
553 -- See Note [Efficiency for mapCoercion ForAllCo case]
554 go (FunCo r c1 c2) = mkFunCo r <$> go c1 <*> go c2
555 go (CoVarCo cv) = covar env cv
556 go (AxiomInstCo ax i args)
557 = mkaxiominstco ax i <$> mapM go args
558 go (HoleCo hole) = cohole env hole
559 go (UnivCo p r t1 t2)
560 = mkunivco <$> go_prov p <*> pure r
561 <*> mapType mapper env t1 <*> mapType mapper env t2
562 go (SymCo co) = mksymco <$> go co
563 go (TransCo c1 c2) = mktransco <$> go c1 <*> go c2
564 go (AxiomRuleCo r cos) = AxiomRuleCo r <$> mapM go cos
565 go (NthCo r i co) = mknthco r i <$> go co
566 go (LRCo lr co) = mklrco lr <$> go co
567 go (InstCo co arg) = mkinstco <$> go co <*> go arg
568 go (CoherenceCo c1 c2) = mkcoherenceco <$> go c1 <*> go c2
569 go (KindCo co) = mkkindco <$> go co
570 go (SubCo co) = mksubco <$> go co
571
572 go_prov UnsafeCoerceProv = return UnsafeCoerceProv
573 go_prov (PhantomProv co) = PhantomProv <$> go co
574 go_prov (ProofIrrelProv co) = ProofIrrelProv <$> go co
575 go_prov p@(PluginProv _) = return p
576
577 ( mktyconappco, mkappco, mkaxiominstco, mkunivco
578 , mksymco, mktransco, mknthco, mklrco, mkinstco, mkcoherenceco
579 , mkkindco, mksubco, mkforallco)
580 | smart
581 = ( mkTyConAppCo, mkAppCo, mkAxiomInstCo, mkUnivCo
582 , mkSymCo, mkTransCo, mkNthCo, mkLRCo, mkInstCo, mkCoherenceCo
583 , mkKindCo, mkSubCo, mkForAllCo )
584 | otherwise
585 = ( TyConAppCo, AppCo, AxiomInstCo, UnivCo
586 , SymCo, TransCo, NthCo, LRCo, InstCo, CoherenceCo
587 , KindCo, SubCo, ForAllCo )
588
589 {-
590 ************************************************************************
591 * *
592 \subsection{Constructor-specific functions}
593 * *
594 ************************************************************************
595
596
597 ---------------------------------------------------------------------
598 TyVarTy
599 ~~~~~~~
600 -}
601
602 -- | Attempts to obtain the type variable underlying a 'Type', and panics with the
603 -- given message if this is not a type variable type. See also 'getTyVar_maybe'
604 getTyVar :: String -> Type -> TyVar
605 getTyVar msg ty = case getTyVar_maybe ty of
606 Just tv -> tv
607 Nothing -> panic ("getTyVar: " ++ msg)
608
609 isTyVarTy :: Type -> Bool
610 isTyVarTy ty = isJust (getTyVar_maybe ty)
611
612 -- | Attempts to obtain the type variable underlying a 'Type'
613 getTyVar_maybe :: Type -> Maybe TyVar
614 getTyVar_maybe ty | Just ty' <- coreView ty = getTyVar_maybe ty'
615 | otherwise = repGetTyVar_maybe ty
616
617 -- | If the type is a tyvar, possibly under a cast, returns it, along
618 -- with the coercion. Thus, the co is :: kind tv ~N kind type
619 getCastedTyVar_maybe :: Type -> Maybe (TyVar, CoercionN)
620 getCastedTyVar_maybe ty | Just ty' <- coreView ty = getCastedTyVar_maybe ty'
621 getCastedTyVar_maybe (CastTy (TyVarTy tv) co) = Just (tv, co)
622 getCastedTyVar_maybe (TyVarTy tv)
623 = Just (tv, mkReflCo Nominal (tyVarKind tv))
624 getCastedTyVar_maybe _ = Nothing
625
626 -- | Attempts to obtain the type variable underlying a 'Type', without
627 -- any expansion
628 repGetTyVar_maybe :: Type -> Maybe TyVar
629 repGetTyVar_maybe (TyVarTy tv) = Just tv
630 repGetTyVar_maybe _ = Nothing
631
632 {-
633 ---------------------------------------------------------------------
634 AppTy
635 ~~~~~
636 We need to be pretty careful with AppTy to make sure we obey the
637 invariant that a TyConApp is always visibly so. mkAppTy maintains the
638 invariant: use it.
639
640 Note [Decomposing fat arrow c=>t]
641 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
642 Can we unify (a b) with (Eq a => ty)? If we do so, we end up with
643 a partial application like ((=>) Eq a) which doesn't make sense in
644 source Haskell. In contrast, we *can* unify (a b) with (t1 -> t2).
645 Here's an example (Trac #9858) of how you might do it:
646 i :: (Typeable a, Typeable b) => Proxy (a b) -> TypeRep
647 i p = typeRep p
648
649 j = i (Proxy :: Proxy (Eq Int => Int))
650 The type (Proxy (Eq Int => Int)) is only accepted with -XImpredicativeTypes,
651 but suppose we want that. But then in the call to 'i', we end
652 up decomposing (Eq Int => Int), and we definitely don't want that.
653
654 This really only applies to the type checker; in Core, '=>' and '->'
655 are the same, as are 'Constraint' and '*'. But for now I've put
656 the test in repSplitAppTy_maybe, which applies throughout, because
657 the other calls to splitAppTy are in Unify, which is also used by
658 the type checker (e.g. when matching type-function equations).
659
660 -}
661
662 -- | Applies a type to another, as in e.g. @k a@
663 mkAppTy :: Type -> Type -> Type
664 -- See Note [Respecting definitional equality], invariant (EQ1).
665 mkAppTy (CastTy fun_ty co) arg_ty
666 | ([arg_co], res_co) <- decomposePiCos (typeKind fun_ty) [arg_ty] co
667 = (fun_ty `mkAppTy` (arg_ty `mkCastTy` arg_co)) `mkCastTy` res_co
668
669 mkAppTy (TyConApp tc tys) ty2 = mkTyConApp tc (tys ++ [ty2])
670 mkAppTy ty1 ty2 = AppTy ty1 ty2
671 -- Note that the TyConApp could be an
672 -- under-saturated type synonym. GHC allows that; e.g.
673 -- type Foo k = k a -> k a
674 -- type Id x = x
675 -- foo :: Foo Id -> Foo Id
676 --
677 -- Here Id is partially applied in the type sig for Foo,
678 -- but once the type synonyms are expanded all is well
679
680 mkAppTys :: Type -> [Type] -> Type
681 mkAppTys ty1 [] = ty1
682 mkAppTys (CastTy fun_ty co) arg_tys -- much more efficient then nested mkAppTy
683 -- Why do this? See (EQ1) of
684 -- Note [Respecting definitional equality]
685 -- in TyCoRep
686 = foldl AppTy ((mkAppTys fun_ty casted_arg_tys) `mkCastTy` res_co) leftovers
687 where
688 (arg_cos, res_co) = decomposePiCos (typeKind fun_ty) arg_tys co
689 (args_to_cast, leftovers) = splitAtList arg_cos arg_tys
690 casted_arg_tys = zipWith mkCastTy args_to_cast arg_cos
691 mkAppTys (TyConApp tc tys1) tys2 = mkTyConApp tc (tys1 ++ tys2)
692 mkAppTys ty1 tys2 = foldl AppTy ty1 tys2
693
694 -------------
695 splitAppTy_maybe :: Type -> Maybe (Type, Type)
696 -- ^ Attempt to take a type application apart, whether it is a
697 -- function, type constructor, or plain type application. Note
698 -- that type family applications are NEVER unsaturated by this!
699 splitAppTy_maybe ty | Just ty' <- coreView ty
700 = splitAppTy_maybe ty'
701 splitAppTy_maybe ty = repSplitAppTy_maybe ty
702
703 -------------
704 repSplitAppTy_maybe :: HasDebugCallStack => Type -> Maybe (Type,Type)
705 -- ^ Does the AppTy split as in 'splitAppTy_maybe', but assumes that
706 -- any Core view stuff is already done
707 repSplitAppTy_maybe (FunTy ty1 ty2)
708 = Just (TyConApp funTyCon [rep1, rep2, ty1], ty2)
709 where
710 rep1 = getRuntimeRep ty1
711 rep2 = getRuntimeRep ty2
712
713 repSplitAppTy_maybe (AppTy ty1 ty2)
714 = Just (ty1, ty2)
715
716 repSplitAppTy_maybe (TyConApp tc tys)
717 | mightBeUnsaturatedTyCon tc || tys `lengthExceeds` tyConArity tc
718 , Just (tys', ty') <- snocView tys
719 = Just (TyConApp tc tys', ty') -- Never create unsaturated type family apps!
720
721 repSplitAppTy_maybe _other = Nothing
722
723 -- this one doesn't braek apart (c => t).
724 -- See Note [Decomposing fat arrow c=>t]
725 -- Defined here to avoid module loops between Unify and TcType.
726 tcRepSplitAppTy_maybe :: Type -> Maybe (Type,Type)
727 -- ^ Does the AppTy split as in 'tcSplitAppTy_maybe', but assumes that
728 -- any coreView stuff is already done. Refuses to look through (c => t)
729 tcRepSplitAppTy_maybe (FunTy ty1 ty2)
730 | isConstraintKind (typeKind ty1)
731 = Nothing -- See Note [Decomposing fat arrow c=>t]
732
733 | otherwise
734 = Just (TyConApp funTyCon [rep1, rep2, ty1], ty2)
735 where
736 rep1 = getRuntimeRep ty1
737 rep2 = getRuntimeRep ty2
738
739 tcRepSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2)
740 tcRepSplitAppTy_maybe (TyConApp tc tys)
741 | mightBeUnsaturatedTyCon tc || tys `lengthExceeds` tyConArity tc
742 , Just (tys', ty') <- snocView tys
743 = Just (TyConApp tc tys', ty') -- Never create unsaturated type family apps!
744 tcRepSplitAppTy_maybe _other = Nothing
745
746 -- | Split a type constructor application into its type constructor and
747 -- applied types. Note that this may fail in the case of a 'FunTy' with an
748 -- argument of unknown kind 'FunTy' (e.g. @FunTy (a :: k) Int@. since the kind
749 -- of @a@ isn't of the form @TYPE rep@). Consequently, you may need to zonk your
750 -- type before using this function.
751 --
752 -- If you only need the 'TyCon', consider using 'tcTyConAppTyCon_maybe'.
753 tcSplitTyConApp_maybe :: HasCallStack => Type -> Maybe (TyCon, [Type])
754 -- Defined here to avoid module loops between Unify and TcType.
755 tcSplitTyConApp_maybe ty | Just ty' <- tcView ty = tcSplitTyConApp_maybe ty'
756 tcSplitTyConApp_maybe ty = tcRepSplitTyConApp_maybe ty
757
758 -- | Like 'tcSplitTyConApp_maybe' but doesn't look through type synonyms.
759 tcRepSplitTyConApp_maybe :: HasCallStack => Type -> Maybe (TyCon, [Type])
760 -- Defined here to avoid module loops between Unify and TcType.
761 tcRepSplitTyConApp_maybe (TyConApp tc tys)
762 = Just (tc, tys)
763
764 tcRepSplitTyConApp_maybe (FunTy arg res)
765 = Just (funTyCon, [arg_rep, res_rep, arg, res])
766 where
767 arg_rep = getRuntimeRep arg
768 res_rep = getRuntimeRep res
769
770 tcRepSplitTyConApp_maybe _
771 = Nothing
772
773 -------------
774 splitAppTy :: Type -> (Type, Type)
775 -- ^ Attempts to take a type application apart, as in 'splitAppTy_maybe',
776 -- and panics if this is not possible
777 splitAppTy ty = case splitAppTy_maybe ty of
778 Just pr -> pr
779 Nothing -> panic "splitAppTy"
780
781 -------------
782 splitAppTys :: Type -> (Type, [Type])
783 -- ^ Recursively splits a type as far as is possible, leaving a residual
784 -- type being applied to and the type arguments applied to it. Never fails,
785 -- even if that means returning an empty list of type applications.
786 splitAppTys ty = split ty ty []
787 where
788 split orig_ty ty args | Just ty' <- coreView ty = split orig_ty ty' args
789 split _ (AppTy ty arg) args = split ty ty (arg:args)
790 split _ (TyConApp tc tc_args) args
791 = let -- keep type families saturated
792 n | mightBeUnsaturatedTyCon tc = 0
793 | otherwise = tyConArity tc
794 (tc_args1, tc_args2) = splitAt n tc_args
795 in
796 (TyConApp tc tc_args1, tc_args2 ++ args)
797 split _ (FunTy ty1 ty2) args
798 = ASSERT( null args )
799 (TyConApp funTyCon [], [rep1, rep2, ty1, ty2])
800 where
801 rep1 = getRuntimeRep ty1
802 rep2 = getRuntimeRep ty2
803
804 split orig_ty _ args = (orig_ty, args)
805
806 -- | Like 'splitAppTys', but doesn't look through type synonyms
807 repSplitAppTys :: HasDebugCallStack => Type -> (Type, [Type])
808 repSplitAppTys ty = split ty []
809 where
810 split (AppTy ty arg) args = split ty (arg:args)
811 split (TyConApp tc tc_args) args
812 = let n | mightBeUnsaturatedTyCon tc = 0
813 | otherwise = tyConArity tc
814 (tc_args1, tc_args2) = splitAt n tc_args
815 in
816 (TyConApp tc tc_args1, tc_args2 ++ args)
817 split (FunTy ty1 ty2) args
818 = ASSERT( null args )
819 (TyConApp funTyCon [], [rep1, rep2, ty1, ty2])
820 where
821 rep1 = getRuntimeRep ty1
822 rep2 = getRuntimeRep ty2
823
824 split ty args = (ty, args)
825
826 {-
827 LitTy
828 ~~~~~
829 -}
830
831 mkNumLitTy :: Integer -> Type
832 mkNumLitTy n = LitTy (NumTyLit n)
833
834 -- | Is this a numeric literal. We also look through type synonyms.
835 isNumLitTy :: Type -> Maybe Integer
836 isNumLitTy ty | Just ty1 <- coreView ty = isNumLitTy ty1
837 isNumLitTy (LitTy (NumTyLit n)) = Just n
838 isNumLitTy _ = Nothing
839
840 mkStrLitTy :: FastString -> Type
841 mkStrLitTy s = LitTy (StrTyLit s)
842
843 -- | Is this a symbol literal. We also look through type synonyms.
844 isStrLitTy :: Type -> Maybe FastString
845 isStrLitTy ty | Just ty1 <- coreView ty = isStrLitTy ty1
846 isStrLitTy (LitTy (StrTyLit s)) = Just s
847 isStrLitTy _ = Nothing
848
849
850 -- | Is this type a custom user error?
851 -- If so, give us the kind and the error message.
852 userTypeError_maybe :: Type -> Maybe Type
853 userTypeError_maybe t
854 = do { (tc, _kind : msg : _) <- splitTyConApp_maybe t
855 -- There may be more than 2 arguments, if the type error is
856 -- used as a type constructor (e.g. at kind `Type -> Type`).
857
858 ; guard (tyConName tc == errorMessageTypeErrorFamName)
859 ; return msg }
860
861 -- | Render a type corresponding to a user type error into a SDoc.
862 pprUserTypeErrorTy :: Type -> SDoc
863 pprUserTypeErrorTy ty =
864 case splitTyConApp_maybe ty of
865
866 -- Text "Something"
867 Just (tc,[txt])
868 | tyConName tc == typeErrorTextDataConName
869 , Just str <- isStrLitTy txt -> ftext str
870
871 -- ShowType t
872 Just (tc,[_k,t])
873 | tyConName tc == typeErrorShowTypeDataConName -> ppr t
874
875 -- t1 :<>: t2
876 Just (tc,[t1,t2])
877 | tyConName tc == typeErrorAppendDataConName ->
878 pprUserTypeErrorTy t1 <> pprUserTypeErrorTy t2
879
880 -- t1 :$$: t2
881 Just (tc,[t1,t2])
882 | tyConName tc == typeErrorVAppendDataConName ->
883 pprUserTypeErrorTy t1 $$ pprUserTypeErrorTy t2
884
885 -- An unevaluated type function
886 _ -> ppr ty
887
888
889
890
891 {-
892 ---------------------------------------------------------------------
893 FunTy
894 ~~~~~
895
896 Note [Representation of function types]
897 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
898
899 Functions (e.g. Int -> Char) are can be thought of as being applications
900 of funTyCon (known in Haskell surface syntax as (->)),
901
902 (->) :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
903 (a :: TYPE r1) (b :: TYPE r2).
904 a -> b -> Type
905
906 However, for efficiency's sake we represent saturated applications of (->)
907 with FunTy. For instance, the type,
908
909 (->) r1 r2 a b
910
911 is equivalent to,
912
913 FunTy (Anon a) b
914
915 Note how the RuntimeReps are implied in the FunTy representation. For this
916 reason we must be careful when recontructing the TyConApp representation (see,
917 for instance, splitTyConApp_maybe).
918
919 In the compiler we maintain the invariant that all saturated applications of
920 (->) are represented with FunTy.
921
922 See #11714.
923 -}
924
925 isFunTy :: Type -> Bool
926 isFunTy ty = isJust (splitFunTy_maybe ty)
927
928 splitFunTy :: Type -> (Type, Type)
929 -- ^ Attempts to extract the argument and result types from a type, and
930 -- panics if that is not possible. See also 'splitFunTy_maybe'
931 splitFunTy ty | Just ty' <- coreView ty = splitFunTy ty'
932 splitFunTy (FunTy arg res) = (arg, res)
933 splitFunTy other = pprPanic "splitFunTy" (ppr other)
934
935 splitFunTy_maybe :: Type -> Maybe (Type, Type)
936 -- ^ Attempts to extract the argument and result types from a type
937 splitFunTy_maybe ty | Just ty' <- coreView ty = splitFunTy_maybe ty'
938 splitFunTy_maybe (FunTy arg res) = Just (arg, res)
939 splitFunTy_maybe _ = Nothing
940
941 splitFunTys :: Type -> ([Type], Type)
942 splitFunTys ty = split [] ty ty
943 where
944 split args orig_ty ty | Just ty' <- coreView ty = split args orig_ty ty'
945 split args _ (FunTy arg res) = split (arg:args) res res
946 split args orig_ty _ = (reverse args, orig_ty)
947
948 funResultTy :: Type -> Type
949 -- ^ Extract the function result type and panic if that is not possible
950 funResultTy ty | Just ty' <- coreView ty = funResultTy ty'
951 funResultTy (FunTy _ res) = res
952 funResultTy ty = pprPanic "funResultTy" (ppr ty)
953
954 funArgTy :: Type -> Type
955 -- ^ Extract the function argument type and panic if that is not possible
956 funArgTy ty | Just ty' <- coreView ty = funArgTy ty'
957 funArgTy (FunTy arg _res) = arg
958 funArgTy ty = pprPanic "funArgTy" (ppr ty)
959
960 piResultTy :: HasDebugCallStack => Type -> Type -> Type
961 piResultTy ty arg = case piResultTy_maybe ty arg of
962 Just res -> res
963 Nothing -> pprPanic "piResultTy" (ppr ty $$ ppr arg)
964
965 piResultTy_maybe :: Type -> Type -> Maybe Type
966
967 -- ^ Just like 'piResultTys' but for a single argument
968 -- Try not to iterate 'piResultTy', because it's inefficient to substitute
969 -- one variable at a time; instead use 'piResultTys"
970 piResultTy_maybe ty arg
971 | Just ty' <- coreView ty = piResultTy_maybe ty' arg
972
973 | FunTy _ res <- ty
974 = Just res
975
976 | ForAllTy (TvBndr tv _) res <- ty
977 = let empty_subst = mkEmptyTCvSubst $ mkInScopeSet $
978 tyCoVarsOfTypes [arg,res]
979 in Just (substTy (extendTvSubst empty_subst tv arg) res)
980
981 | otherwise
982 = Nothing
983
984 -- | (piResultTys f_ty [ty1, .., tyn]) gives the type of (f ty1 .. tyn)
985 -- where f :: f_ty
986 -- 'piResultTys' is interesting because:
987 -- 1. 'f_ty' may have more for-alls than there are args
988 -- 2. Less obviously, it may have fewer for-alls
989 -- For case 2. think of:
990 -- piResultTys (forall a.a) [forall b.b, Int]
991 -- This really can happen, but only (I think) in situations involving
992 -- undefined. For example:
993 -- undefined :: forall a. a
994 -- Term: undefined @(forall b. b->b) @Int
995 -- This term should have type (Int -> Int), but notice that
996 -- there are more type args than foralls in 'undefined's type.
997
998 -- If you edit this function, you may need to update the GHC formalism
999 -- See Note [GHC Formalism] in coreSyn/CoreLint.hs
1000
1001 -- This is a heavily used function (e.g. from typeKind),
1002 -- so we pay attention to efficiency, especially in the special case
1003 -- where there are no for-alls so we are just dropping arrows from
1004 -- a function type/kind.
1005 piResultTys :: HasDebugCallStack => Type -> [Type] -> Type
1006 piResultTys ty [] = ty
1007 piResultTys ty orig_args@(arg:args)
1008 | Just ty' <- coreView ty
1009 = piResultTys ty' orig_args
1010
1011 | FunTy _ res <- ty
1012 = piResultTys res args
1013
1014 | ForAllTy (TvBndr tv _) res <- ty
1015 = go (extendVarEnv emptyTvSubstEnv tv arg) res args
1016
1017 | otherwise
1018 = pprPanic "piResultTys1" (ppr ty $$ ppr orig_args)
1019 where
1020 in_scope = mkInScopeSet (tyCoVarsOfTypes (ty:orig_args))
1021
1022 go :: TvSubstEnv -> Type -> [Type] -> Type
1023 go tv_env ty [] = substTy (mkTvSubst in_scope tv_env) ty
1024
1025 go tv_env ty all_args@(arg:args)
1026 | Just ty' <- coreView ty
1027 = go tv_env ty' all_args
1028
1029 | FunTy _ res <- ty
1030 = go tv_env res args
1031
1032 | ForAllTy (TvBndr tv _) res <- ty
1033 = go (extendVarEnv tv_env tv arg) res args
1034
1035 | TyVarTy tv <- ty
1036 , Just ty' <- lookupVarEnv tv_env tv
1037 -- Deals with piResultTys (forall a. a) [forall b.b, Int]
1038 = piResultTys ty' all_args
1039
1040 | otherwise
1041 = pprPanic "piResultTys2" (ppr ty $$ ppr orig_args $$ ppr all_args)
1042
1043 applyTysX :: [TyVar] -> Type -> [Type] -> Type
1044 -- applyTyxX beta-reduces (/\tvs. body_ty) arg_tys
1045 -- Assumes that (/\tvs. body_ty) is closed
1046 applyTysX tvs body_ty arg_tys
1047 = ASSERT2( arg_tys `lengthAtLeast` n_tvs, pp_stuff )
1048 ASSERT2( tyCoVarsOfType body_ty `subVarSet` mkVarSet tvs, pp_stuff )
1049 mkAppTys (substTyWith tvs (take n_tvs arg_tys) body_ty)
1050 (drop n_tvs arg_tys)
1051 where
1052 pp_stuff = vcat [ppr tvs, ppr body_ty, ppr arg_tys]
1053 n_tvs = length tvs
1054
1055 {-
1056 ---------------------------------------------------------------------
1057 TyConApp
1058 ~~~~~~~~
1059 -}
1060
1061 -- | A key function: builds a 'TyConApp' or 'FunTy' as appropriate to
1062 -- its arguments. Applies its arguments to the constructor from left to right.
1063 mkTyConApp :: TyCon -> [Type] -> Type
1064 mkTyConApp tycon tys
1065 | isFunTyCon tycon
1066 , [_rep1,_rep2,ty1,ty2] <- tys
1067 = FunTy ty1 ty2
1068
1069 | otherwise
1070 = TyConApp tycon tys
1071
1072 -- splitTyConApp "looks through" synonyms, because they don't
1073 -- mean a distinct type, but all other type-constructor applications
1074 -- including functions are returned as Just ..
1075
1076 -- | Retrieve the tycon heading this type, if there is one. Does /not/
1077 -- look through synonyms.
1078 tyConAppTyConPicky_maybe :: Type -> Maybe TyCon
1079 tyConAppTyConPicky_maybe (TyConApp tc _) = Just tc
1080 tyConAppTyConPicky_maybe (FunTy {}) = Just funTyCon
1081 tyConAppTyConPicky_maybe _ = Nothing
1082
1083
1084 -- | The same as @fst . splitTyConApp@
1085 tyConAppTyCon_maybe :: Type -> Maybe TyCon
1086 tyConAppTyCon_maybe ty | Just ty' <- coreView ty = tyConAppTyCon_maybe ty'
1087 tyConAppTyCon_maybe (TyConApp tc _) = Just tc
1088 tyConAppTyCon_maybe (FunTy {}) = Just funTyCon
1089 tyConAppTyCon_maybe _ = Nothing
1090
1091 tyConAppTyCon :: Type -> TyCon
1092 tyConAppTyCon ty = tyConAppTyCon_maybe ty `orElse` pprPanic "tyConAppTyCon" (ppr ty)
1093
1094 -- | The same as @snd . splitTyConApp@
1095 tyConAppArgs_maybe :: Type -> Maybe [Type]
1096 tyConAppArgs_maybe ty | Just ty' <- coreView ty = tyConAppArgs_maybe ty'
1097 tyConAppArgs_maybe (TyConApp _ tys) = Just tys
1098 tyConAppArgs_maybe (FunTy arg res)
1099 | Just rep1 <- getRuntimeRep_maybe arg
1100 , Just rep2 <- getRuntimeRep_maybe res
1101 = Just [rep1, rep2, arg, res]
1102 tyConAppArgs_maybe _ = Nothing
1103
1104 tyConAppArgs :: Type -> [Type]
1105 tyConAppArgs ty = tyConAppArgs_maybe ty `orElse` pprPanic "tyConAppArgs" (ppr ty)
1106
1107 tyConAppArgN :: Int -> Type -> Type
1108 -- Executing Nth
1109 tyConAppArgN n ty
1110 = case tyConAppArgs_maybe ty of
1111 Just tys -> ASSERT2( tys `lengthExceeds` n, ppr n <+> ppr tys ) tys `getNth` n
1112 Nothing -> pprPanic "tyConAppArgN" (ppr n <+> ppr ty)
1113
1114 -- | Attempts to tease a type apart into a type constructor and the application
1115 -- of a number of arguments to that constructor. Panics if that is not possible.
1116 -- See also 'splitTyConApp_maybe'
1117 splitTyConApp :: Type -> (TyCon, [Type])
1118 splitTyConApp ty = case splitTyConApp_maybe ty of
1119 Just stuff -> stuff
1120 Nothing -> pprPanic "splitTyConApp" (ppr ty)
1121
1122 -- | Attempts to tease a type apart into a type constructor and the application
1123 -- of a number of arguments to that constructor
1124 splitTyConApp_maybe :: HasDebugCallStack => Type -> Maybe (TyCon, [Type])
1125 splitTyConApp_maybe ty | Just ty' <- coreView ty = splitTyConApp_maybe ty'
1126 splitTyConApp_maybe ty = repSplitTyConApp_maybe ty
1127
1128 -- | Like 'splitTyConApp_maybe', but doesn't look through synonyms. This
1129 -- assumes the synonyms have already been dealt with.
1130 repSplitTyConApp_maybe :: HasDebugCallStack => Type -> Maybe (TyCon, [Type])
1131 repSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
1132 repSplitTyConApp_maybe (FunTy arg res)
1133 | Just arg_rep <- getRuntimeRep_maybe arg
1134 , Just res_rep <- getRuntimeRep_maybe res
1135 = Just (funTyCon, [arg_rep, res_rep, arg, res])
1136 repSplitTyConApp_maybe _ = Nothing
1137
1138 -- | Attempts to tease a list type apart and gives the type of the elements if
1139 -- successful (looks through type synonyms)
1140 splitListTyConApp_maybe :: Type -> Maybe Type
1141 splitListTyConApp_maybe ty = case splitTyConApp_maybe ty of
1142 Just (tc,[e]) | tc == listTyCon -> Just e
1143 _other -> Nothing
1144
1145 nextRole :: Type -> Role
1146 nextRole ty
1147 | Just (tc, tys) <- splitTyConApp_maybe ty
1148 , let num_tys = length tys
1149 , num_tys < tyConArity tc
1150 = tyConRoles tc `getNth` num_tys
1151
1152 | otherwise
1153 = Nominal
1154
1155 newTyConInstRhs :: TyCon -> [Type] -> Type
1156 -- ^ Unwrap one 'layer' of newtype on a type constructor and its
1157 -- arguments, using an eta-reduced version of the @newtype@ if possible.
1158 -- This requires tys to have at least @newTyConInstArity tycon@ elements.
1159 newTyConInstRhs tycon tys
1160 = ASSERT2( tvs `leLength` tys, ppr tycon $$ ppr tys $$ ppr tvs )
1161 applyTysX tvs rhs tys
1162 where
1163 (tvs, rhs) = newTyConEtadRhs tycon
1164
1165 {-
1166 ---------------------------------------------------------------------
1167 CastTy
1168 ~~~~~~
1169 A casted type has its *kind* casted into something new.
1170
1171 -}
1172
1173 splitCastTy_maybe :: Type -> Maybe (Type, Coercion)
1174 splitCastTy_maybe ty | Just ty' <- coreView ty = splitCastTy_maybe ty'
1175 splitCastTy_maybe (CastTy ty co) = Just (ty, co)
1176 splitCastTy_maybe _ = Nothing
1177
1178 -- | Make a 'CastTy'. The Coercion must be nominal. Checks the
1179 -- Coercion for reflexivity, dropping it if it's reflexive.
1180 -- See Note [Respecting definitional equality] in TyCoRep
1181 mkCastTy :: Type -> Coercion -> Type
1182 mkCastTy ty co | isReflexiveCo co = ty -- (EQ2) from the Note
1183 -- NB: Do the slow check here. This is important to keep the splitXXX
1184 -- functions working properly. Otherwise, we may end up with something
1185 -- like (((->) |> something_reflexive_but_not_obviously_so) biz baz)
1186 -- fails under splitFunTy_maybe. This happened with the cheaper check
1187 -- in test dependent/should_compile/dynamic-paper.
1188
1189 mkCastTy (CastTy ty co1) co2 = mkCastTy ty (co1 `mkTransCo` co2) -- (EQ3) from the Note
1190 -- call mkCastTy again for the reflexivity check
1191 mkCastTy ty co = CastTy ty co
1192
1193 tyConBindersTyBinders :: [TyConBinder] -> [TyBinder]
1194 -- Return the tyConBinders in TyBinder form
1195 tyConBindersTyBinders = map to_tyb
1196 where
1197 to_tyb (TvBndr tv (NamedTCB vis)) = Named (TvBndr tv vis)
1198 to_tyb (TvBndr tv AnonTCB) = Anon (tyVarKind tv)
1199
1200 {-
1201 --------------------------------------------------------------------
1202 CoercionTy
1203 ~~~~~~~~~~
1204 CoercionTy allows us to inject coercions into types. A CoercionTy
1205 should appear only in the right-hand side of an application.
1206 -}
1207
1208 mkCoercionTy :: Coercion -> Type
1209 mkCoercionTy = CoercionTy
1210
1211 isCoercionTy :: Type -> Bool
1212 isCoercionTy (CoercionTy _) = True
1213 isCoercionTy _ = False
1214
1215 isCoercionTy_maybe :: Type -> Maybe Coercion
1216 isCoercionTy_maybe (CoercionTy co) = Just co
1217 isCoercionTy_maybe _ = Nothing
1218
1219 stripCoercionTy :: Type -> Coercion
1220 stripCoercionTy (CoercionTy co) = co
1221 stripCoercionTy ty = pprPanic "stripCoercionTy" (ppr ty)
1222
1223 {-
1224 ---------------------------------------------------------------------
1225 SynTy
1226 ~~~~~
1227
1228 Notes on type synonyms
1229 ~~~~~~~~~~~~~~~~~~~~~~
1230 The various "split" functions (splitFunTy, splitRhoTy, splitForAllTy) try
1231 to return type synonyms wherever possible. Thus
1232
1233 type Foo a = a -> a
1234
1235 we want
1236 splitFunTys (a -> Foo a) = ([a], Foo a)
1237 not ([a], a -> a)
1238
1239 The reason is that we then get better (shorter) type signatures in
1240 interfaces. Notably this plays a role in tcTySigs in TcBinds.hs.
1241
1242
1243 ---------------------------------------------------------------------
1244 ForAllTy
1245 ~~~~~~~~
1246 -}
1247
1248 -- | Make a dependent forall over an Inferred (as opposed to Specified)
1249 -- variable
1250 mkInvForAllTy :: TyVar -> Type -> Type
1251 mkInvForAllTy tv ty = ASSERT( isTyVar tv )
1252 ForAllTy (TvBndr tv Inferred) ty
1253
1254 -- | Like mkForAllTys, but assumes all variables are dependent and Inferred,
1255 -- a common case
1256 mkInvForAllTys :: [TyVar] -> Type -> Type
1257 mkInvForAllTys tvs ty = ASSERT( all isTyVar tvs )
1258 foldr mkInvForAllTy ty tvs
1259
1260 -- | Like mkForAllTys, but assumes all variables are dependent and specified,
1261 -- a common case
1262 mkSpecForAllTys :: [TyVar] -> Type -> Type
1263 mkSpecForAllTys tvs = ASSERT( all isTyVar tvs )
1264 mkForAllTys [ TvBndr tv Specified | tv <- tvs ]
1265
1266 -- | Like mkForAllTys, but assumes all variables are dependent and visible
1267 mkVisForAllTys :: [TyVar] -> Type -> Type
1268 mkVisForAllTys tvs = ASSERT( all isTyVar tvs )
1269 mkForAllTys [ TvBndr tv Required | tv <- tvs ]
1270
1271 mkLamType :: Var -> Type -> Type
1272 -- ^ Makes a @(->)@ type or an implicit forall type, depending
1273 -- on whether it is given a type variable or a term variable.
1274 -- This is used, for example, when producing the type of a lambda.
1275 -- Always uses Inferred binders.
1276 mkLamTypes :: [Var] -> Type -> Type
1277 -- ^ 'mkLamType' for multiple type or value arguments
1278
1279 mkLamType v ty
1280 | isTyVar v = ForAllTy (TvBndr v Inferred) ty
1281 | otherwise = FunTy (varType v) ty
1282
1283 mkLamTypes vs ty = foldr mkLamType ty vs
1284
1285 -- | Given a list of type-level vars and a result kind,
1286 -- makes TyBinders, preferring anonymous binders
1287 -- if the variable is, in fact, not dependent.
1288 -- e.g. mkTyConBindersPreferAnon [(k:*),(b:k),(c:k)] (k->k)
1289 -- We want (k:*) Named, (a;k) Anon, (c:k) Anon
1290 --
1291 -- All binders are /visible/.
1292 mkTyConBindersPreferAnon :: [TyVar] -> Type -> [TyConBinder]
1293 mkTyConBindersPreferAnon vars inner_ty = fst (go vars)
1294 where
1295 go :: [TyVar] -> ([TyConBinder], VarSet) -- also returns the free vars
1296 go [] = ([], tyCoVarsOfType inner_ty)
1297 go (v:vs) | v `elemVarSet` fvs
1298 = ( TvBndr v (NamedTCB Required) : binders
1299 , fvs `delVarSet` v `unionVarSet` kind_vars )
1300 | otherwise
1301 = ( TvBndr v AnonTCB : binders
1302 , fvs `unionVarSet` kind_vars )
1303 where
1304 (binders, fvs) = go vs
1305 kind_vars = tyCoVarsOfType $ tyVarKind v
1306
1307 -- | Take a ForAllTy apart, returning the list of tyvars and the result type.
1308 -- This always succeeds, even if it returns only an empty list. Note that the
1309 -- result type returned may have free variables that were bound by a forall.
1310 splitForAllTys :: Type -> ([TyVar], Type)
1311 splitForAllTys ty = split ty ty []
1312 where
1313 split orig_ty ty tvs | Just ty' <- coreView ty = split orig_ty ty' tvs
1314 split _ (ForAllTy (TvBndr tv _) ty) tvs = split ty ty (tv:tvs)
1315 split orig_ty _ tvs = (reverse tvs, orig_ty)
1316
1317 -- | Like 'splitPiTys' but split off only /named/ binders.
1318 splitForAllTyVarBndrs :: Type -> ([TyVarBinder], Type)
1319 splitForAllTyVarBndrs ty = split ty ty []
1320 where
1321 split orig_ty ty bs | Just ty' <- coreView ty = split orig_ty ty' bs
1322 split _ (ForAllTy b res) bs = split res res (b:bs)
1323 split orig_ty _ bs = (reverse bs, orig_ty)
1324 {-# INLINE splitForAllTyVarBndrs #-}
1325
1326 -- | Checks whether this is a proper forall (with a named binder)
1327 isForAllTy :: Type -> Bool
1328 isForAllTy ty | Just ty' <- coreView ty = isForAllTy ty'
1329 isForAllTy (ForAllTy {}) = True
1330 isForAllTy _ = False
1331
1332 -- | Is this a function or forall?
1333 isPiTy :: Type -> Bool
1334 isPiTy ty | Just ty' <- coreView ty = isForAllTy ty'
1335 isPiTy (ForAllTy {}) = True
1336 isPiTy (FunTy {}) = True
1337 isPiTy _ = False
1338
1339 -- | Take a forall type apart, or panics if that is not possible.
1340 splitForAllTy :: Type -> (TyVar, Type)
1341 splitForAllTy ty
1342 | Just answer <- splitForAllTy_maybe ty = answer
1343 | otherwise = pprPanic "splitForAllTy" (ppr ty)
1344
1345 -- | Drops all ForAllTys
1346 dropForAlls :: Type -> Type
1347 dropForAlls ty = go ty
1348 where
1349 go ty | Just ty' <- coreView ty = go ty'
1350 go (ForAllTy _ res) = go res
1351 go res = res
1352
1353 -- | Attempts to take a forall type apart, but only if it's a proper forall,
1354 -- with a named binder
1355 splitForAllTy_maybe :: Type -> Maybe (TyVar, Type)
1356 splitForAllTy_maybe ty = go ty
1357 where
1358 go ty | Just ty' <- coreView ty = go ty'
1359 go (ForAllTy (TvBndr tv _) ty) = Just (tv, ty)
1360 go _ = Nothing
1361
1362 -- | Attempts to take a forall type apart; works with proper foralls and
1363 -- functions
1364 splitPiTy_maybe :: Type -> Maybe (TyBinder, Type)
1365 splitPiTy_maybe ty = go ty
1366 where
1367 go ty | Just ty' <- coreView ty = go ty'
1368 go (ForAllTy bndr ty) = Just (Named bndr, ty)
1369 go (FunTy arg res) = Just (Anon arg, res)
1370 go _ = Nothing
1371
1372 -- | Takes a forall type apart, or panics
1373 splitPiTy :: Type -> (TyBinder, Type)
1374 splitPiTy ty
1375 | Just answer <- splitPiTy_maybe ty = answer
1376 | otherwise = pprPanic "splitPiTy" (ppr ty)
1377
1378 -- | Split off all TyBinders to a type, splitting both proper foralls
1379 -- and functions
1380 splitPiTys :: Type -> ([TyBinder], Type)
1381 splitPiTys ty = split ty ty
1382 where
1383 split orig_ty ty | Just ty' <- coreView ty = split orig_ty ty'
1384 split _ (ForAllTy b res) = let (bs, ty) = split res res
1385 in (Named b : bs, ty)
1386 split _ (FunTy arg res) = let (bs, ty) = split res res
1387 in (Anon arg : bs, ty)
1388 split orig_ty _ = ([], orig_ty)
1389
1390 -- Like splitPiTys, but returns only *invisible* binders, including constraints
1391 -- Stops at the first visible binder
1392 splitPiTysInvisible :: Type -> ([TyBinder], Type)
1393 splitPiTysInvisible ty = split ty ty []
1394 where
1395 split orig_ty ty bs | Just ty' <- coreView ty = split orig_ty ty' bs
1396 split _ (ForAllTy b@(TvBndr _ vis) res) bs
1397 | isInvisibleArgFlag vis = split res res (Named b : bs)
1398 split _ (FunTy arg res) bs
1399 | isPredTy arg = split res res (Anon arg : bs)
1400 split orig_ty _ bs = (reverse bs, orig_ty)
1401
1402 -- | Given a tycon and its arguments, filters out any invisible arguments
1403 filterOutInvisibleTypes :: TyCon -> [Type] -> [Type]
1404 filterOutInvisibleTypes tc tys = snd $ partitionInvisibles tc id tys
1405
1406 -- | Given a tycon and a list of things (which correspond to arguments),
1407 -- partitions the things into
1408 -- Inferred or Specified ones and
1409 -- Required ones
1410 -- The callback function is necessary for this scenario:
1411 --
1412 -- > T :: forall k. k -> k
1413 -- > partitionInvisibles T [forall m. m -> m -> m, S, R, Q]
1414 --
1415 -- After substituting, we get
1416 --
1417 -- > T (forall m. m -> m -> m) :: (forall m. m -> m -> m) -> forall n. n -> n -> n
1418 --
1419 -- Thus, the first argument is invisible, @S@ is visible, @R@ is invisible again,
1420 -- and @Q@ is visible.
1421 --
1422 -- If you're absolutely sure that your tycon's kind doesn't end in a variable,
1423 -- it's OK if the callback function panics, as that's the only time it's
1424 -- consulted.
1425 partitionInvisibles :: TyCon -> (a -> Type) -> [a] -> ([a], [a])
1426 partitionInvisibles tc get_ty = go emptyTCvSubst (tyConKind tc)
1427 where
1428 go _ _ [] = ([], [])
1429 go subst (ForAllTy (TvBndr tv vis) res_ki) (x:xs)
1430 | isVisibleArgFlag vis = second (x :) (go subst' res_ki xs)
1431 | otherwise = first (x :) (go subst' res_ki xs)
1432 where
1433 subst' = extendTvSubst subst tv (get_ty x)
1434 go subst (TyVarTy tv) xs
1435 | Just ki <- lookupTyVar subst tv = go subst ki xs
1436 go _ _ xs = ([], xs) -- something is ill-kinded. But this can happen
1437 -- when printing errors. Assume everything is visible.
1438
1439 -- @isTauTy@ tests if a type has no foralls
1440 isTauTy :: Type -> Bool
1441 isTauTy ty | Just ty' <- coreView ty = isTauTy ty'
1442 isTauTy (TyVarTy _) = True
1443 isTauTy (LitTy {}) = True
1444 isTauTy (TyConApp tc tys) = all isTauTy tys && isTauTyCon tc
1445 isTauTy (AppTy a b) = isTauTy a && isTauTy b
1446 isTauTy (FunTy a b) = isTauTy a && isTauTy b
1447 isTauTy (ForAllTy {}) = False
1448 isTauTy (CastTy ty _) = isTauTy ty
1449 isTauTy (CoercionTy _) = False -- Not sure about this
1450
1451 {-
1452 %************************************************************************
1453 %* *
1454 TyBinders
1455 %* *
1456 %************************************************************************
1457 -}
1458
1459 -- | Make an anonymous binder
1460 mkAnonBinder :: Type -> TyBinder
1461 mkAnonBinder = Anon
1462
1463 -- | Does this binder bind a variable that is /not/ erased? Returns
1464 -- 'True' for anonymous binders.
1465 isAnonTyBinder :: TyBinder -> Bool
1466 isAnonTyBinder (Named {}) = False
1467 isAnonTyBinder (Anon {}) = True
1468
1469 isNamedTyBinder :: TyBinder -> Bool
1470 isNamedTyBinder (Named {}) = True
1471 isNamedTyBinder (Anon {}) = False
1472
1473 tyBinderVar_maybe :: TyBinder -> Maybe TyVar
1474 tyBinderVar_maybe (Named tv) = Just $ binderVar tv
1475 tyBinderVar_maybe _ = Nothing
1476
1477 tyBinderType :: TyBinder -> Type
1478 -- Barely used
1479 tyBinderType (Named tvb) = binderKind tvb
1480 tyBinderType (Anon ty) = ty
1481
1482 -- | Extract a relevant type, if there is one.
1483 binderRelevantType_maybe :: TyBinder -> Maybe Type
1484 binderRelevantType_maybe (Named {}) = Nothing
1485 binderRelevantType_maybe (Anon ty) = Just ty
1486
1487 -- | Like 'maybe', but for binders.
1488 caseBinder :: TyBinder -- ^ binder to scrutinize
1489 -> (TyVarBinder -> a) -- ^ named case
1490 -> (Type -> a) -- ^ anonymous case
1491 -> a
1492 caseBinder (Named v) f _ = f v
1493 caseBinder (Anon t) _ d = d t
1494
1495
1496 {-
1497 %************************************************************************
1498 %* *
1499 Pred
1500 * *
1501 ************************************************************************
1502
1503 Predicates on PredType
1504
1505 Note [isPredTy complications]
1506 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1507 You would think that we could define
1508 isPredTy ty = isConstraintKind (typeKind ty)
1509 But there are a number of complications:
1510
1511 * isPredTy is used when printing types, which can happen in debug
1512 printing during type checking of not-fully-zonked types. So it's
1513 not cool to say isConstraintKind (typeKind ty) because, absent
1514 zonking, the type might be ill-kinded, and typeKind crashes. Hence the
1515 rather tiresome story here
1516
1517 * isPredTy must return "True" to *unlifted* coercions, such as (t1 ~# t2)
1518 and (t1 ~R# t2), which are not of kind Constraint! Currently they are
1519 of kind #.
1520
1521 * If we do form the type '(C a => C [a]) => blah', then we'd like to
1522 print it as such. But that means that isPredTy must return True for
1523 (C a => C [a]). Admittedly that type is illegal in Haskell, but we
1524 want to print it nicely in error messages.
1525 -}
1526
1527 -- | Is the type suitable to classify a given/wanted in the typechecker?
1528 isPredTy :: Type -> Bool
1529 -- See Note [isPredTy complications]
1530 isPredTy ty = go ty []
1531 where
1532 go :: Type -> [KindOrType] -> Bool
1533 go (AppTy ty1 ty2) args = go ty1 (ty2 : args)
1534 go (TyVarTy tv) args = go_k (tyVarKind tv) args
1535 go (TyConApp tc tys) args = ASSERT( null args ) -- TyConApp invariant
1536 go_tc tc tys
1537 go (FunTy arg res) []
1538 | isPredTy arg = isPredTy res -- (Eq a => C a)
1539 | otherwise = False -- (Int -> Bool)
1540 go (ForAllTy _ ty) [] = go ty []
1541 go (CastTy _ co) args = go_k (pSnd (coercionKind co)) args
1542 go _ _ = False
1543
1544 go_tc :: TyCon -> [KindOrType] -> Bool
1545 go_tc tc args
1546 | tc `hasKey` eqPrimTyConKey || tc `hasKey` eqReprPrimTyConKey
1547 = args `lengthIs` 4 -- ~# and ~R# sadly have result kind #
1548 -- not Constraint; but we still want
1549 -- isPredTy to reply True.
1550 | otherwise = go_k (tyConKind tc) args
1551
1552 go_k :: Kind -> [KindOrType] -> Bool
1553 -- True <=> ('k' applied to 'kts') = Constraint
1554 go_k k [] = isConstraintKind k
1555 go_k k (arg:args) = case piResultTy_maybe k arg of
1556 Just k' -> go_k k' args
1557 Nothing -> WARN( True, text "isPredTy" <+> ppr ty )
1558 False
1559 -- This last case shouldn't happen under most circumstances. It can
1560 -- occur if we call isPredTy during kind checking, especially if one
1561 -- of the following happens:
1562 --
1563 -- 1. There is actually a kind error. Example in which this showed up:
1564 -- polykinds/T11399
1565 --
1566 -- 2. A type constructor application appears to be oversaturated. An
1567 -- example of this occurred in GHC Trac #13187:
1568 --
1569 -- {-# LANGUAGE PolyKinds #-}
1570 -- type Const a b = b
1571 -- f :: Const Int (,) Bool Char -> Char
1572 --
1573 -- We call isPredTy (Const k1 k2 Int (,) Bool Char
1574 -- where k1,k2 are unification variables that have been
1575 -- unified to *, and (*->*->*) resp, /but not zonked/.
1576 -- This shows that isPredTy can report a false negative
1577 -- if a constraint is similarly oversaturated, but
1578 -- it's hard to do better than isPredTy currently does without
1579 -- zonking, so we punt on such cases for now. This only happens
1580 -- during debug-printing, so it doesn't matter.
1581
1582 isClassPred, isEqPred, isNomEqPred, isIPPred :: PredType -> Bool
1583 isClassPred ty = case tyConAppTyCon_maybe ty of
1584 Just tyCon | isClassTyCon tyCon -> True
1585 _ -> False
1586 isEqPred ty = case tyConAppTyCon_maybe ty of
1587 Just tyCon -> tyCon `hasKey` eqPrimTyConKey
1588 || tyCon `hasKey` eqReprPrimTyConKey
1589 _ -> False
1590
1591 isNomEqPred ty = case tyConAppTyCon_maybe ty of
1592 Just tyCon -> tyCon `hasKey` eqPrimTyConKey
1593 _ -> False
1594
1595 isIPPred ty = case tyConAppTyCon_maybe ty of
1596 Just tc -> isIPTyCon tc
1597 _ -> False
1598
1599 isIPTyCon :: TyCon -> Bool
1600 isIPTyCon tc = tc `hasKey` ipClassKey
1601 -- Class and its corresponding TyCon have the same Unique
1602
1603 isIPClass :: Class -> Bool
1604 isIPClass cls = cls `hasKey` ipClassKey
1605
1606 isCTupleClass :: Class -> Bool
1607 isCTupleClass cls = isTupleTyCon (classTyCon cls)
1608
1609 isIPPred_maybe :: Type -> Maybe (FastString, Type)
1610 isIPPred_maybe ty =
1611 do (tc,[t1,t2]) <- splitTyConApp_maybe ty
1612 guard (isIPTyCon tc)
1613 x <- isStrLitTy t1
1614 return (x,t2)
1615
1616 {-
1617 Make PredTypes
1618
1619 --------------------- Equality types ---------------------------------
1620 -}
1621
1622 -- | Makes a lifted equality predicate at the given role
1623 mkPrimEqPredRole :: Role -> Type -> Type -> PredType
1624 mkPrimEqPredRole Nominal = mkPrimEqPred
1625 mkPrimEqPredRole Representational = mkReprPrimEqPred
1626 mkPrimEqPredRole Phantom = panic "mkPrimEqPredRole phantom"
1627
1628 -- | Creates a primitive type equality predicate.
1629 -- Invariant: the types are not Coercions
1630 mkPrimEqPred :: Type -> Type -> Type
1631 mkPrimEqPred ty1 ty2
1632 = TyConApp eqPrimTyCon [k1, k2, ty1, ty2]
1633 where
1634 k1 = typeKind ty1
1635 k2 = typeKind ty2
1636
1637 -- | Creates a primite type equality predicate with explicit kinds
1638 mkHeteroPrimEqPred :: Kind -> Kind -> Type -> Type -> Type
1639 mkHeteroPrimEqPred k1 k2 ty1 ty2 = TyConApp eqPrimTyCon [k1, k2, ty1, ty2]
1640
1641 -- | Creates a primitive representational type equality predicate
1642 -- with explicit kinds
1643 mkHeteroReprPrimEqPred :: Kind -> Kind -> Type -> Type -> Type
1644 mkHeteroReprPrimEqPred k1 k2 ty1 ty2
1645 = TyConApp eqReprPrimTyCon [k1, k2, ty1, ty2]
1646
1647 -- | Try to split up a coercion type into the types that it coerces
1648 splitCoercionType_maybe :: Type -> Maybe (Type, Type)
1649 splitCoercionType_maybe ty
1650 = do { (tc, [_, _, ty1, ty2]) <- splitTyConApp_maybe ty
1651 ; guard $ tc `hasKey` eqPrimTyConKey || tc `hasKey` eqReprPrimTyConKey
1652 ; return (ty1, ty2) }
1653
1654 mkReprPrimEqPred :: Type -> Type -> Type
1655 mkReprPrimEqPred ty1 ty2
1656 = TyConApp eqReprPrimTyCon [k1, k2, ty1, ty2]
1657 where
1658 k1 = typeKind ty1
1659 k2 = typeKind ty2
1660
1661 equalityTyCon :: Role -> TyCon
1662 equalityTyCon Nominal = eqPrimTyCon
1663 equalityTyCon Representational = eqReprPrimTyCon
1664 equalityTyCon Phantom = eqPhantPrimTyCon
1665
1666 -- --------------------- Dictionary types ---------------------------------
1667
1668 mkClassPred :: Class -> [Type] -> PredType
1669 mkClassPred clas tys = TyConApp (classTyCon clas) tys
1670
1671 isDictTy :: Type -> Bool
1672 isDictTy = isClassPred
1673
1674 isDictLikeTy :: Type -> Bool
1675 -- Note [Dictionary-like types]
1676 isDictLikeTy ty | Just ty' <- coreView ty = isDictLikeTy ty'
1677 isDictLikeTy ty = case splitTyConApp_maybe ty of
1678 Just (tc, tys) | isClassTyCon tc -> True
1679 | isTupleTyCon tc -> all isDictLikeTy tys
1680 _other -> False
1681
1682 {-
1683 Note [Dictionary-like types]
1684 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1685 Being "dictionary-like" means either a dictionary type or a tuple thereof.
1686 In GHC 6.10 we build implication constraints which construct such tuples,
1687 and if we land up with a binding
1688 t :: (C [a], Eq [a])
1689 t = blah
1690 then we want to treat t as cheap under "-fdicts-cheap" for example.
1691 (Implication constraints are normally inlined, but sadly not if the
1692 occurrence is itself inside an INLINE function! Until we revise the
1693 handling of implication constraints, that is.) This turned out to
1694 be important in getting good arities in DPH code. Example:
1695
1696 class C a
1697 class D a where { foo :: a -> a }
1698 instance C a => D (Maybe a) where { foo x = x }
1699
1700 bar :: (C a, C b) => a -> b -> (Maybe a, Maybe b)
1701 {-# INLINE bar #-}
1702 bar x y = (foo (Just x), foo (Just y))
1703
1704 Then 'bar' should jolly well have arity 4 (two dicts, two args), but
1705 we ended up with something like
1706 bar = __inline_me__ (\d1,d2. let t :: (D (Maybe a), D (Maybe b)) = ...
1707 in \x,y. <blah>)
1708
1709 This is all a bit ad-hoc; eg it relies on knowing that implication
1710 constraints build tuples.
1711
1712
1713 Decomposing PredType
1714 -}
1715
1716 -- | A choice of equality relation. This is separate from the type 'Role'
1717 -- because 'Phantom' does not define a (non-trivial) equality relation.
1718 data EqRel = NomEq | ReprEq
1719 deriving (Eq, Ord)
1720
1721 instance Outputable EqRel where
1722 ppr NomEq = text "nominal equality"
1723 ppr ReprEq = text "representational equality"
1724
1725 eqRelRole :: EqRel -> Role
1726 eqRelRole NomEq = Nominal
1727 eqRelRole ReprEq = Representational
1728
1729 data PredTree
1730 = ClassPred Class [Type]
1731 | EqPred EqRel Type Type
1732 | IrredPred PredType
1733 | ForAllPred [TyVarBinder] [PredType] PredType
1734 -- ForAllPred: see Note [Quantified constraints] in TcCanonical
1735 -- NB: There is no TuplePred case
1736 -- Tuple predicates like (Eq a, Ord b) are just treated
1737 -- as ClassPred, as if we had a tuple class with two superclasses
1738 -- class (c1, c2) => (%,%) c1 c2
1739
1740 classifyPredType :: PredType -> PredTree
1741 classifyPredType ev_ty = case splitTyConApp_maybe ev_ty of
1742 Just (tc, [_, _, ty1, ty2])
1743 | tc `hasKey` eqReprPrimTyConKey -> EqPred ReprEq ty1 ty2
1744 | tc `hasKey` eqPrimTyConKey -> EqPred NomEq ty1 ty2
1745
1746 Just (tc, tys)
1747 | Just clas <- tyConClass_maybe tc
1748 -> ClassPred clas tys
1749
1750 _ | (tvs, rho) <- splitForAllTyVarBndrs ev_ty
1751 , (theta, pred) <- splitFunTys rho
1752 , not (null tvs && null theta)
1753 -> ForAllPred tvs theta pred
1754
1755 | otherwise
1756 -> IrredPred ev_ty
1757
1758 getClassPredTys :: HasDebugCallStack => PredType -> (Class, [Type])
1759 getClassPredTys ty = case getClassPredTys_maybe ty of
1760 Just (clas, tys) -> (clas, tys)
1761 Nothing -> pprPanic "getClassPredTys" (ppr ty)
1762
1763 getClassPredTys_maybe :: PredType -> Maybe (Class, [Type])
1764 getClassPredTys_maybe ty = case splitTyConApp_maybe ty of
1765 Just (tc, tys) | Just clas <- tyConClass_maybe tc -> Just (clas, tys)
1766 _ -> Nothing
1767
1768 getEqPredTys :: PredType -> (Type, Type)
1769 getEqPredTys ty
1770 = case splitTyConApp_maybe ty of
1771 Just (tc, [_, _, ty1, ty2])
1772 | tc `hasKey` eqPrimTyConKey
1773 || tc `hasKey` eqReprPrimTyConKey
1774 -> (ty1, ty2)
1775 _ -> pprPanic "getEqPredTys" (ppr ty)
1776
1777 getEqPredTys_maybe :: PredType -> Maybe (Role, Type, Type)
1778 getEqPredTys_maybe ty
1779 = case splitTyConApp_maybe ty of
1780 Just (tc, [_, _, ty1, ty2])
1781 | tc `hasKey` eqPrimTyConKey -> Just (Nominal, ty1, ty2)
1782 | tc `hasKey` eqReprPrimTyConKey -> Just (Representational, ty1, ty2)
1783 _ -> Nothing
1784
1785 getEqPredRole :: PredType -> Role
1786 getEqPredRole ty = eqRelRole (predTypeEqRel ty)
1787
1788 -- | Get the equality relation relevant for a pred type.
1789 predTypeEqRel :: PredType -> EqRel
1790 predTypeEqRel ty
1791 | Just (tc, _) <- splitTyConApp_maybe ty
1792 , tc `hasKey` eqReprPrimTyConKey
1793 = ReprEq
1794 | otherwise
1795 = NomEq
1796
1797 {-
1798 %************************************************************************
1799 %* *
1800 Well-scoped tyvars
1801 * *
1802 ************************************************************************
1803 -}
1804
1805 -- | Do a topological sort on a list of tyvars,
1806 -- so that binders occur before occurrences
1807 -- E.g. given [ a::k, k::*, b::k ]
1808 -- it'll return a well-scoped list [ k::*, a::k, b::k ]
1809 --
1810 -- This is a deterministic sorting operation
1811 -- (that is, doesn't depend on Uniques).
1812 toposortTyVars :: [TyCoVar] -> [TyCoVar]
1813 toposortTyVars tvs = reverse $
1814 [ node_payload node | node <- topologicalSortG $
1815 graphFromEdgedVerticesOrd nodes ]
1816 where
1817 var_ids :: VarEnv Int
1818 var_ids = mkVarEnv (zip tvs [1..])
1819
1820 nodes :: [ Node Int TyVar ]
1821 nodes = [ DigraphNode
1822 tv
1823 (lookupVarEnv_NF var_ids tv)
1824 (mapMaybe (lookupVarEnv var_ids)
1825 (tyCoVarsOfTypeList (tyVarKind tv)))
1826 | tv <- tvs ]
1827
1828 -- | Extract a well-scoped list of variables from a deterministic set of
1829 -- variables. The result is deterministic.
1830 -- NB: There used to exist varSetElemsWellScoped :: VarSet -> [Var] which
1831 -- took a non-deterministic set and produced a non-deterministic
1832 -- well-scoped list. If you care about the list being well-scoped you also
1833 -- most likely care about it being in deterministic order.
1834 dVarSetElemsWellScoped :: DVarSet -> [Var]
1835 dVarSetElemsWellScoped = toposortTyVars . dVarSetElems
1836
1837 -- | Get the free vars of a type in scoped order
1838 tyCoVarsOfTypeWellScoped :: Type -> [TyVar]
1839 tyCoVarsOfTypeWellScoped = toposortTyVars . tyCoVarsOfTypeList
1840
1841 -- | Get the free vars of types in scoped order
1842 tyCoVarsOfTypesWellScoped :: [Type] -> [TyVar]
1843 tyCoVarsOfTypesWellScoped = toposortTyVars . tyCoVarsOfTypesList
1844
1845 {-
1846 ************************************************************************
1847 * *
1848 \subsection{Type families}
1849 * *
1850 ************************************************************************
1851 -}
1852
1853 mkFamilyTyConApp :: TyCon -> [Type] -> Type
1854 -- ^ Given a family instance TyCon and its arg types, return the
1855 -- corresponding family type. E.g:
1856 --
1857 -- > data family T a
1858 -- > data instance T (Maybe b) = MkT b
1859 --
1860 -- Where the instance tycon is :RTL, so:
1861 --
1862 -- > mkFamilyTyConApp :RTL Int = T (Maybe Int)
1863 mkFamilyTyConApp tc tys
1864 | Just (fam_tc, fam_tys) <- tyConFamInst_maybe tc
1865 , let tvs = tyConTyVars tc
1866 fam_subst = ASSERT2( tvs `equalLength` tys, ppr tc <+> ppr tys )
1867 zipTvSubst tvs tys
1868 = mkTyConApp fam_tc (substTys fam_subst fam_tys)
1869 | otherwise
1870 = mkTyConApp tc tys
1871
1872 -- | Get the type on the LHS of a coercion induced by a type/data
1873 -- family instance.
1874 coAxNthLHS :: CoAxiom br -> Int -> Type
1875 coAxNthLHS ax ind =
1876 mkTyConApp (coAxiomTyCon ax) (coAxBranchLHS (coAxiomNthBranch ax ind))
1877
1878 -- | Pretty prints a 'TyCon', using the family instance in case of a
1879 -- representation tycon. For example:
1880 --
1881 -- > data T [a] = ...
1882 --
1883 -- In that case we want to print @T [a]@, where @T@ is the family 'TyCon'
1884 pprSourceTyCon :: TyCon -> SDoc
1885 pprSourceTyCon tycon
1886 | Just (fam_tc, tys) <- tyConFamInst_maybe tycon
1887 = ppr $ fam_tc `TyConApp` tys -- can't be FunTyCon
1888 | otherwise
1889 = ppr tycon
1890
1891 -- @isTauTy@ tests if a type has no foralls
1892 isFamFreeTy :: Type -> Bool
1893 isFamFreeTy ty | Just ty' <- coreView ty = isFamFreeTy ty'
1894 isFamFreeTy (TyVarTy _) = True
1895 isFamFreeTy (LitTy {}) = True
1896 isFamFreeTy (TyConApp tc tys) = all isFamFreeTy tys && isFamFreeTyCon tc
1897 isFamFreeTy (AppTy a b) = isFamFreeTy a && isFamFreeTy b
1898 isFamFreeTy (FunTy a b) = isFamFreeTy a && isFamFreeTy b
1899 isFamFreeTy (ForAllTy _ ty) = isFamFreeTy ty
1900 isFamFreeTy (CastTy ty _) = isFamFreeTy ty
1901 isFamFreeTy (CoercionTy _) = False -- Not sure about this
1902
1903 {-
1904 ************************************************************************
1905 * *
1906 \subsection{Liftedness}
1907 * *
1908 ************************************************************************
1909 -}
1910
1911 -- | Returns Just True if this type is surely lifted, Just False
1912 -- if it is surely unlifted, Nothing if we can't be sure (i.e., it is
1913 -- levity polymorphic), and panics if the kind does not have the shape
1914 -- TYPE r.
1915 isLiftedType_maybe :: HasDebugCallStack => Type -> Maybe Bool
1916 isLiftedType_maybe ty = go (getRuntimeRep ty)
1917 where
1918 go rr | Just rr' <- coreView rr = go rr'
1919 go (TyConApp lifted_rep [])
1920 | lifted_rep `hasKey` liftedRepDataConKey = Just True
1921 go (TyConApp {}) = Just False -- everything else is unlifted
1922 go _ = Nothing -- levity polymorphic
1923
1924 -- | See "Type#type_classification" for what an unlifted type is.
1925 -- Panics on levity polymorphic types.
1926 isUnliftedType :: HasDebugCallStack => Type -> Bool
1927 -- isUnliftedType returns True for forall'd unlifted types:
1928 -- x :: forall a. Int#
1929 -- I found bindings like these were getting floated to the top level.
1930 -- They are pretty bogus types, mind you. It would be better never to
1931 -- construct them
1932 isUnliftedType ty
1933 = not (isLiftedType_maybe ty `orElse`
1934 pprPanic "isUnliftedType" (ppr ty <+> dcolon <+> ppr (typeKind ty)))
1935
1936 -- | Is this a type of kind RuntimeRep? (e.g. LiftedRep)
1937 isRuntimeRepKindedTy :: Type -> Bool
1938 isRuntimeRepKindedTy = isRuntimeRepTy . typeKind
1939
1940 -- | Drops prefix of RuntimeRep constructors in 'TyConApp's. Useful for e.g.
1941 -- dropping 'LiftedRep arguments of unboxed tuple TyCon applications:
1942 --
1943 -- dropRuntimeRepArgs [ 'LiftedRep, 'IntRep
1944 -- , String, Int# ] == [String, Int#]
1945 --
1946 dropRuntimeRepArgs :: [Type] -> [Type]
1947 dropRuntimeRepArgs = dropWhile isRuntimeRepKindedTy
1948
1949 -- | Extract the RuntimeRep classifier of a type. For instance,
1950 -- @getRuntimeRep_maybe Int = LiftedRep@. Returns 'Nothing' if this is not
1951 -- possible.
1952 getRuntimeRep_maybe :: HasDebugCallStack
1953 => Type -> Maybe Type
1954 getRuntimeRep_maybe = getRuntimeRepFromKind_maybe . typeKind
1955
1956 -- | Extract the RuntimeRep classifier of a type. For instance,
1957 -- @getRuntimeRep_maybe Int = LiftedRep@. Panics if this is not possible.
1958 getRuntimeRep :: HasDebugCallStack => Type -> Type
1959 getRuntimeRep ty
1960 = case getRuntimeRep_maybe ty of
1961 Just r -> r
1962 Nothing -> pprPanic "getRuntimeRep" (ppr ty <+> dcolon <+> ppr (typeKind ty))
1963
1964 -- | Extract the RuntimeRep classifier of a type from its kind. For example,
1965 -- @getRuntimeRepFromKind * = LiftedRep@; Panics if this is not possible.
1966 getRuntimeRepFromKind :: HasDebugCallStack
1967 => Type -> Type
1968 getRuntimeRepFromKind k =
1969 case getRuntimeRepFromKind_maybe k of
1970 Just r -> r
1971 Nothing -> pprPanic "getRuntimeRepFromKind"
1972 (ppr k <+> dcolon <+> ppr (typeKind k))
1973
1974 -- | Extract the RuntimeRep classifier of a type from its kind. For example,
1975 -- @getRuntimeRepFromKind * = LiftedRep@; Returns 'Nothing' if this is not
1976 -- possible.
1977 getRuntimeRepFromKind_maybe :: HasDebugCallStack
1978 => Type -> Maybe Type
1979 getRuntimeRepFromKind_maybe = go
1980 where
1981 go k | Just k' <- coreView k = go k'
1982 go k
1983 | Just (_tc, [arg]) <- splitTyConApp_maybe k
1984 = ASSERT2( _tc `hasKey` tYPETyConKey, ppr k )
1985 Just arg
1986 go _ = Nothing
1987
1988 isUnboxedTupleType :: Type -> Bool
1989 isUnboxedTupleType ty
1990 = tyConAppTyCon (getRuntimeRep ty) `hasKey` tupleRepDataConKey
1991 -- NB: Do not use typePrimRep, as that can't tell the difference between
1992 -- unboxed tuples and unboxed sums
1993
1994
1995 isUnboxedSumType :: Type -> Bool
1996 isUnboxedSumType ty
1997 = tyConAppTyCon (getRuntimeRep ty) `hasKey` sumRepDataConKey
1998
1999 -- | See "Type#type_classification" for what an algebraic type is.
2000 -- Should only be applied to /types/, as opposed to e.g. partially
2001 -- saturated type constructors
2002 isAlgType :: Type -> Bool
2003 isAlgType ty
2004 = case splitTyConApp_maybe ty of
2005 Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
2006 isAlgTyCon tc
2007 _other -> False
2008
2009 -- | Check whether a type is a data family type
2010 isDataFamilyAppType :: Type -> Bool
2011 isDataFamilyAppType ty = case tyConAppTyCon_maybe ty of
2012 Just tc -> isDataFamilyTyCon tc
2013 _ -> False
2014
2015 -- | Computes whether an argument (or let right hand side) should
2016 -- be computed strictly or lazily, based only on its type.
2017 -- Currently, it's just 'isUnliftedType'. Panics on levity-polymorphic types.
2018 isStrictType :: HasDebugCallStack => Type -> Bool
2019 isStrictType = isUnliftedType
2020
2021 isPrimitiveType :: Type -> Bool
2022 -- ^ Returns true of types that are opaque to Haskell.
2023 isPrimitiveType ty = case splitTyConApp_maybe ty of
2024 Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
2025 isPrimTyCon tc
2026 _ -> False
2027
2028 {-
2029 ************************************************************************
2030 * *
2031 \subsection{Join points}
2032 * *
2033 ************************************************************************
2034 -}
2035
2036 -- | Determine whether a type could be the type of a join point of given total
2037 -- arity, according to the polymorphism rule. A join point cannot be polymorphic
2038 -- in its return type, since given
2039 -- join j @a @b x y z = e1 in e2,
2040 -- the types of e1 and e2 must be the same, and a and b are not in scope for e2.
2041 -- (See Note [The polymorphism rule of join points] in CoreSyn.) Returns False
2042 -- also if the type simply doesn't have enough arguments.
2043 --
2044 -- Note that we need to know how many arguments (type *and* value) the putative
2045 -- join point takes; for instance, if
2046 -- j :: forall a. a -> Int
2047 -- then j could be a binary join point returning an Int, but it could *not* be a
2048 -- unary join point returning a -> Int.
2049 --
2050 -- TODO: See Note [Excess polymorphism and join points]
2051 isValidJoinPointType :: JoinArity -> Type -> Bool
2052 isValidJoinPointType arity ty
2053 = valid_under emptyVarSet arity ty
2054 where
2055 valid_under tvs arity ty
2056 | arity == 0
2057 = isEmptyVarSet (tvs `intersectVarSet` tyCoVarsOfType ty)
2058 | Just (t, ty') <- splitForAllTy_maybe ty
2059 = valid_under (tvs `extendVarSet` t) (arity-1) ty'
2060 | Just (_, res_ty) <- splitFunTy_maybe ty
2061 = valid_under tvs (arity-1) res_ty
2062 | otherwise
2063 = False
2064
2065 {- Note [Excess polymorphism and join points]
2066 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2067 In principle, if a function would be a join point except that it fails
2068 the polymorphism rule (see Note [The polymorphism rule of join points] in
2069 CoreSyn), it can still be made a join point with some effort. This is because
2070 all tail calls must return the same type (they return to the same context!), and
2071 thus if the return type depends on an argument, that argument must always be the
2072 same.
2073
2074 For instance, consider:
2075
2076 let f :: forall a. a -> Char -> [a]
2077 f @a x c = ... f @a y 'a' ...
2078 in ... f @Int 1 'b' ... f @Int 2 'c' ...
2079
2080 (where the calls are tail calls). `f` fails the polymorphism rule because its
2081 return type is [a], where [a] is bound. But since the type argument is always
2082 'Int', we can rewrite it as:
2083
2084 let f' :: Int -> Char -> [Int]
2085 f' x c = ... f' y 'a' ...
2086 in ... f' 1 'b' ... f 2 'c' ...
2087
2088 and now we can make f' a join point:
2089
2090 join f' :: Int -> Char -> [Int]
2091 f' x c = ... jump f' y 'a' ...
2092 in ... jump f' 1 'b' ... jump f' 2 'c' ...
2093
2094 It's not clear that this comes up often, however. TODO: Measure how often and
2095 add this analysis if necessary. See Trac #14620.
2096
2097
2098 ************************************************************************
2099 * *
2100 \subsection{Sequencing on types}
2101 * *
2102 ************************************************************************
2103 -}
2104
2105 seqType :: Type -> ()
2106 seqType (LitTy n) = n `seq` ()
2107 seqType (TyVarTy tv) = tv `seq` ()
2108 seqType (AppTy t1 t2) = seqType t1 `seq` seqType t2
2109 seqType (FunTy t1 t2) = seqType t1 `seq` seqType t2
2110 seqType (TyConApp tc tys) = tc `seq` seqTypes tys
2111 seqType (ForAllTy (TvBndr tv _) ty) = seqType (tyVarKind tv) `seq` seqType ty
2112 seqType (CastTy ty co) = seqType ty `seq` seqCo co
2113 seqType (CoercionTy co) = seqCo co
2114
2115 seqTypes :: [Type] -> ()
2116 seqTypes [] = ()
2117 seqTypes (ty:tys) = seqType ty `seq` seqTypes tys
2118
2119 {-
2120 ************************************************************************
2121 * *
2122 Comparison for types
2123 (We don't use instances so that we know where it happens)
2124 * *
2125 ************************************************************************
2126
2127 Note [Equality on AppTys]
2128 ~~~~~~~~~~~~~~~~~~~~~~~~~
2129 In our cast-ignoring equality, we want to say that the following two
2130 are equal:
2131
2132 (Maybe |> co) (Int |> co') ~? Maybe Int
2133
2134 But the left is an AppTy while the right is a TyConApp. The solution is
2135 to use repSplitAppTy_maybe to break up the TyConApp into its pieces and
2136 then continue. Easy to do, but also easy to forget to do.
2137
2138 -}
2139
2140 eqType :: Type -> Type -> Bool
2141 -- ^ Type equality on source types. Does not look through @newtypes@ or
2142 -- 'PredType's, but it does look through type synonyms.
2143 -- This first checks that the kinds of the types are equal and then
2144 -- checks whether the types are equal, ignoring casts and coercions.
2145 -- (The kind check is a recursive call, but since all kinds have type
2146 -- @Type@, there is no need to check the types of kinds.)
2147 -- See also Note [Non-trivial definitional equality] in TyCoRep.
2148 eqType t1 t2 = isEqual $ nonDetCmpType t1 t2
2149 -- It's OK to use nonDetCmpType here and eqType is deterministic,
2150 -- nonDetCmpType does equality deterministically
2151
2152 -- | Compare types with respect to a (presumably) non-empty 'RnEnv2'.
2153 eqTypeX :: RnEnv2 -> Type -> Type -> Bool
2154 eqTypeX env t1 t2 = isEqual $ nonDetCmpTypeX env t1 t2
2155 -- It's OK to use nonDetCmpType here and eqTypeX is deterministic,
2156 -- nonDetCmpTypeX does equality deterministically
2157
2158 -- | Type equality on lists of types, looking through type synonyms
2159 -- but not newtypes.
2160 eqTypes :: [Type] -> [Type] -> Bool
2161 eqTypes tys1 tys2 = isEqual $ nonDetCmpTypes tys1 tys2
2162 -- It's OK to use nonDetCmpType here and eqTypes is deterministic,
2163 -- nonDetCmpTypes does equality deterministically
2164
2165 eqVarBndrs :: RnEnv2 -> [Var] -> [Var] -> Maybe RnEnv2
2166 -- Check that the var lists are the same length
2167 -- and have matching kinds; if so, extend the RnEnv2
2168 -- Returns Nothing if they don't match
2169 eqVarBndrs env [] []
2170 = Just env
2171 eqVarBndrs env (tv1:tvs1) (tv2:tvs2)
2172 | eqTypeX env (tyVarKind tv1) (tyVarKind tv2)
2173 = eqVarBndrs (rnBndr2 env tv1 tv2) tvs1 tvs2
2174 eqVarBndrs _ _ _= Nothing
2175
2176 -- Now here comes the real worker
2177
2178 {-
2179 Note [nonDetCmpType nondeterminism]
2180 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2181 nonDetCmpType is implemented in terms of nonDetCmpTypeX. nonDetCmpTypeX
2182 uses nonDetCmpTc which compares TyCons by their Unique value. Using Uniques for
2183 ordering leads to nondeterminism. We hit the same problem in the TyVarTy case,
2184 comparing type variables is nondeterministic, note the call to nonDetCmpVar in
2185 nonDetCmpTypeX.
2186 See Note [Unique Determinism] for more details.
2187 -}
2188
2189 nonDetCmpType :: Type -> Type -> Ordering
2190 nonDetCmpType t1 t2
2191 -- we know k1 and k2 have the same kind, because they both have kind *.
2192 = nonDetCmpTypeX rn_env t1 t2
2193 where
2194 rn_env = mkRnEnv2 (mkInScopeSet (tyCoVarsOfTypes [t1, t2]))
2195
2196 nonDetCmpTypes :: [Type] -> [Type] -> Ordering
2197 nonDetCmpTypes ts1 ts2 = nonDetCmpTypesX rn_env ts1 ts2
2198 where
2199 rn_env = mkRnEnv2 (mkInScopeSet (tyCoVarsOfTypes (ts1 ++ ts2)))
2200
2201 -- | An ordering relation between two 'Type's (known below as @t1 :: k1@
2202 -- and @t2 :: k2@)
2203 data TypeOrdering = TLT -- ^ @t1 < t2@
2204 | TEQ -- ^ @t1 ~ t2@ and there are no casts in either,
2205 -- therefore we can conclude @k1 ~ k2@
2206 | TEQX -- ^ @t1 ~ t2@ yet one of the types contains a cast so
2207 -- they may differ in kind.
2208 | TGT -- ^ @t1 > t2@
2209 deriving (Eq, Ord, Enum, Bounded)
2210
2211 nonDetCmpTypeX :: RnEnv2 -> Type -> Type -> Ordering -- Main workhorse
2212 -- See Note [Non-trivial definitional equality] in TyCoRep
2213 nonDetCmpTypeX env orig_t1 orig_t2 =
2214 case go env orig_t1 orig_t2 of
2215 -- If there are casts then we also need to do a comparison of the kinds of
2216 -- the types being compared
2217 TEQX -> toOrdering $ go env k1 k2
2218 ty_ordering -> toOrdering ty_ordering
2219 where
2220 k1 = typeKind orig_t1
2221 k2 = typeKind orig_t2
2222
2223 toOrdering :: TypeOrdering -> Ordering
2224 toOrdering TLT = LT
2225 toOrdering TEQ = EQ
2226 toOrdering TEQX = EQ
2227 toOrdering TGT = GT
2228
2229 liftOrdering :: Ordering -> TypeOrdering
2230 liftOrdering LT = TLT
2231 liftOrdering EQ = TEQ
2232 liftOrdering GT = TGT
2233
2234 thenCmpTy :: TypeOrdering -> TypeOrdering -> TypeOrdering
2235 thenCmpTy TEQ rel = rel
2236 thenCmpTy TEQX rel = hasCast rel
2237 thenCmpTy rel _ = rel
2238
2239 hasCast :: TypeOrdering -> TypeOrdering
2240 hasCast TEQ = TEQX
2241 hasCast rel = rel
2242
2243 -- Returns both the resulting ordering relation between the two types
2244 -- and whether either contains a cast.
2245 go :: RnEnv2 -> Type -> Type -> TypeOrdering
2246 go env t1 t2
2247 | Just t1' <- coreView t1 = go env t1' t2
2248 | Just t2' <- coreView t2 = go env t1 t2'
2249
2250 go env (TyVarTy tv1) (TyVarTy tv2)
2251 = liftOrdering $ rnOccL env tv1 `nonDetCmpVar` rnOccR env tv2
2252 go env (ForAllTy (TvBndr tv1 _) t1) (ForAllTy (TvBndr tv2 _) t2)
2253 = go env (tyVarKind tv1) (tyVarKind tv2)
2254 `thenCmpTy` go (rnBndr2 env tv1 tv2) t1 t2
2255 -- See Note [Equality on AppTys]
2256 go env (AppTy s1 t1) ty2
2257 | Just (s2, t2) <- repSplitAppTy_maybe ty2
2258 = go env s1 s2 `thenCmpTy` go env t1 t2
2259 go env ty1 (AppTy s2 t2)
2260 | Just (s1, t1) <- repSplitAppTy_maybe ty1
2261 = go env s1 s2 `thenCmpTy` go env t1 t2
2262 go env (FunTy s1 t1) (FunTy s2 t2)
2263 = go env s1 s2 `thenCmpTy` go env t1 t2
2264 go env (TyConApp tc1 tys1) (TyConApp tc2 tys2)
2265 = liftOrdering (tc1 `nonDetCmpTc` tc2) `thenCmpTy` gos env tys1 tys2
2266 go _ (LitTy l1) (LitTy l2) = liftOrdering (compare l1 l2)
2267 go env (CastTy t1 _) t2 = hasCast $ go env t1 t2
2268 go env t1 (CastTy t2 _) = hasCast $ go env t1 t2
2269
2270 go _ (CoercionTy {}) (CoercionTy {}) = TEQ
2271
2272 -- Deal with the rest: TyVarTy < CoercionTy < AppTy < LitTy < TyConApp < ForAllTy
2273 go _ ty1 ty2
2274 = liftOrdering $ (get_rank ty1) `compare` (get_rank ty2)
2275 where get_rank :: Type -> Int
2276 get_rank (CastTy {})
2277 = pprPanic "nonDetCmpTypeX.get_rank" (ppr [ty1,ty2])
2278 get_rank (TyVarTy {}) = 0
2279 get_rank (CoercionTy {}) = 1
2280 get_rank (AppTy {}) = 3
2281 get_rank (LitTy {}) = 4
2282 get_rank (TyConApp {}) = 5
2283 get_rank (FunTy {}) = 6
2284 get_rank (ForAllTy {}) = 7
2285
2286 gos :: RnEnv2 -> [Type] -> [Type] -> TypeOrdering
2287 gos _ [] [] = TEQ
2288 gos _ [] _ = TLT
2289 gos _ _ [] = TGT
2290 gos env (ty1:tys1) (ty2:tys2) = go env ty1 ty2 `thenCmpTy` gos env tys1 tys2
2291
2292 -------------
2293 nonDetCmpTypesX :: RnEnv2 -> [Type] -> [Type] -> Ordering
2294 nonDetCmpTypesX _ [] [] = EQ
2295 nonDetCmpTypesX env (t1:tys1) (t2:tys2) = nonDetCmpTypeX env t1 t2
2296 `thenCmp` nonDetCmpTypesX env tys1 tys2
2297 nonDetCmpTypesX _ [] _ = LT
2298 nonDetCmpTypesX _ _ [] = GT
2299
2300 -------------
2301 -- | Compare two 'TyCon's. NB: This should /never/ see 'Constraint' (as
2302 -- recognized by Kind.isConstraintKindCon) which is considered a synonym for
2303 -- 'Type' in Core.
2304 -- See Note [Kind Constraint and kind Type] in Kind.
2305 -- See Note [nonDetCmpType nondeterminism]
2306 nonDetCmpTc :: TyCon -> TyCon -> Ordering
2307 nonDetCmpTc tc1 tc2
2308 = ASSERT( not (isConstraintKindCon tc1) && not (isConstraintKindCon tc2) )
2309 u1 `nonDetCmpUnique` u2
2310 where
2311 u1 = tyConUnique tc1
2312 u2 = tyConUnique tc2
2313
2314 {-
2315 ************************************************************************
2316 * *
2317 The kind of a type
2318 * *
2319 ************************************************************************
2320 -}
2321
2322 typeKind :: HasDebugCallStack => Type -> Kind
2323 typeKind (TyConApp tc tys) = piResultTys (tyConKind tc) tys
2324 typeKind (AppTy fun arg) = typeKind_apps fun [arg]
2325 typeKind (LitTy l) = typeLiteralKind l
2326 typeKind (FunTy {}) = liftedTypeKind
2327 typeKind (TyVarTy tyvar) = tyVarKind tyvar
2328 typeKind (CastTy _ty co) = pSnd $ coercionKind co
2329 typeKind (CoercionTy co) = coercionType co
2330 typeKind ty@(ForAllTy {}) = case occCheckExpand tvs k of
2331 Just k' -> k'
2332 Nothing -> pprPanic "typeKind"
2333 (ppr ty $$ ppr k $$ ppr tvs $$ ppr body)
2334 where
2335 (tvs, body) = splitForAllTys ty
2336 k = typeKind body
2337
2338 typeKind_apps :: HasDebugCallStack => Type -> [Type] -> Kind
2339 -- The sole purpose of the function is to accumulate
2340 -- the type arugments, so we can call piResultTys, rather than
2341 -- a succession of calls to piResultTy (which is asymptotically
2342 -- less efficient as the number of arguments increases)
2343 typeKind_apps (AppTy fun arg) args = typeKind_apps fun (arg:args)
2344 typeKind_apps fun args = piResultTys (typeKind fun) args
2345
2346 --------------------------
2347 typeLiteralKind :: TyLit -> Kind
2348 typeLiteralKind l =
2349 case l of
2350 NumTyLit _ -> typeNatKind
2351 StrTyLit _ -> typeSymbolKind
2352
2353 -- | Returns True if a type is levity polymorphic. Should be the same
2354 -- as (isKindLevPoly . typeKind) but much faster.
2355 -- Precondition: The type has kind (TYPE blah)
2356 isTypeLevPoly :: Type -> Bool
2357 isTypeLevPoly = go
2358 where
2359 go ty@(TyVarTy {}) = check_kind ty
2360 go ty@(AppTy {}) = check_kind ty
2361 go ty@(TyConApp tc _) | not (isTcLevPoly tc) = False
2362 | otherwise = check_kind ty
2363 go (ForAllTy _ ty) = go ty
2364 go (FunTy {}) = False
2365 go (LitTy {}) = False
2366 go ty@(CastTy {}) = check_kind ty
2367 go ty@(CoercionTy {}) = pprPanic "isTypeLevPoly co" (ppr ty)
2368
2369 check_kind = isKindLevPoly . typeKind
2370
2371 -- | Looking past all pi-types, is the end result potentially levity polymorphic?
2372 -- Example: True for (forall r (a :: TYPE r). String -> a)
2373 -- Example: False for (forall r1 r2 (a :: TYPE r1) (b :: TYPE r2). a -> b -> Type)
2374 resultIsLevPoly :: Type -> Bool
2375 resultIsLevPoly = isTypeLevPoly . snd . splitPiTys
2376
2377
2378 {- **********************************************************************
2379 * *
2380 Occurs check expansion
2381 %* *
2382 %********************************************************************* -}
2383
2384 {- Note [Occurs check expansion]
2385 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2386 (occurCheckExpand tv xi) expands synonyms in xi just enough to get rid
2387 of occurrences of tv outside type function arguments, if that is
2388 possible; otherwise, it returns Nothing.
2389
2390 For example, suppose we have
2391 type F a b = [a]
2392 Then
2393 occCheckExpand b (F Int b) = Just [Int]
2394 but
2395 occCheckExpand a (F a Int) = Nothing
2396
2397 We don't promise to do the absolute minimum amount of expanding
2398 necessary, but we try not to do expansions we don't need to. We
2399 prefer doing inner expansions first. For example,
2400 type F a b = (a, Int, a, [a])
2401 type G b = Char
2402 We have
2403 occCheckExpand b (F (G b)) = Just (F Char)
2404 even though we could also expand F to get rid of b.
2405 -}
2406
2407 occCheckExpand :: [Var] -> Type -> Maybe Type
2408 -- See Note [Occurs check expansion]
2409 -- We may have needed to do some type synonym unfolding in order to
2410 -- get rid of the variable (or forall), so we also return the unfolded
2411 -- version of the type, which is guaranteed to be syntactically free
2412 -- of the given type variable. If the type is already syntactically
2413 -- free of the variable, then the same type is returned.
2414 occCheckExpand vs_to_avoid ty
2415 = go (mkVarSet vs_to_avoid, emptyVarEnv) ty
2416 where
2417 go :: (VarSet, VarEnv TyVar) -> Type -> Maybe Type
2418 -- The VarSet is the set of variables we are trying to avoid
2419 -- The VarEnv carries mappings necessary
2420 -- because of kind expansion
2421 go cxt@(as, env) (TyVarTy tv')
2422 | tv' `elemVarSet` as = Nothing
2423 | Just tv'' <- lookupVarEnv env tv' = return (mkTyVarTy tv'')
2424 | otherwise = do { tv'' <- go_var cxt tv'
2425 ; return (mkTyVarTy tv'') }
2426
2427 go _ ty@(LitTy {}) = return ty
2428 go cxt (AppTy ty1 ty2) = do { ty1' <- go cxt ty1
2429 ; ty2' <- go cxt ty2
2430 ; return (mkAppTy ty1' ty2') }
2431 go cxt (FunTy ty1 ty2) = do { ty1' <- go cxt ty1
2432 ; ty2' <- go cxt ty2
2433 ; return (mkFunTy ty1' ty2') }
2434 go cxt@(as, env) (ForAllTy (TvBndr tv vis) body_ty)
2435 = do { ki' <- go cxt (tyVarKind tv)
2436 ; let tv' = setTyVarKind tv ki'
2437 env' = extendVarEnv env tv tv'
2438 as' = as `delVarSet` tv
2439 ; body' <- go (as', env') body_ty
2440 ; return (ForAllTy (TvBndr tv' vis) body') }
2441
2442 -- For a type constructor application, first try expanding away the
2443 -- offending variable from the arguments. If that doesn't work, next
2444 -- see if the type constructor is a type synonym, and if so, expand
2445 -- it and try again.
2446 go cxt ty@(TyConApp tc tys)
2447 = case mapM (go cxt) tys of
2448 Just tys' -> return (mkTyConApp tc tys')
2449 Nothing | Just ty' <- tcView ty -> go cxt ty'
2450 | otherwise -> Nothing
2451 -- Failing that, try to expand a synonym
2452
2453 go cxt (CastTy ty co) = do { ty' <- go cxt ty
2454 ; co' <- go_co cxt co
2455 ; return (mkCastTy ty' co') }
2456 go cxt (CoercionTy co) = do { co' <- go_co cxt co
2457 ; return (mkCoercionTy co') }
2458
2459 ------------------
2460 go_var cxt v = do { k' <- go cxt (varType v)
2461 ; return (setVarType v k') }
2462 -- Works for TyVar and CoVar
2463 -- See Note [Occurrence checking: look inside kinds]
2464
2465 ------------------
2466 go_co cxt (Refl r ty) = do { ty' <- go cxt ty
2467 ; return (mkReflCo r ty') }
2468 -- Note: Coercions do not contain type synonyms
2469 go_co cxt (TyConAppCo r tc args) = do { args' <- mapM (go_co cxt) args
2470 ; return (mkTyConAppCo r tc args') }
2471 go_co cxt (AppCo co arg) = do { co' <- go_co cxt co
2472 ; arg' <- go_co cxt arg
2473 ; return (mkAppCo co' arg') }
2474 go_co cxt@(as, env) (ForAllCo tv kind_co body_co)
2475 = do { kind_co' <- go_co cxt kind_co
2476 ; let tv' = setTyVarKind tv $
2477 pFst (coercionKind kind_co')
2478 env' = extendVarEnv env tv tv'
2479 as' = as `delVarSet` tv
2480 ; body' <- go_co (as', env') body_co
2481 ; return (ForAllCo tv' kind_co' body') }
2482 go_co cxt (FunCo r co1 co2) = do { co1' <- go_co cxt co1
2483 ; co2' <- go_co cxt co2
2484 ; return (mkFunCo r co1' co2') }
2485 go_co cxt (CoVarCo c) = do { c' <- go_var cxt c
2486 ; return (mkCoVarCo c') }
2487 go_co cxt (HoleCo h) = do { c' <- go_var cxt (ch_co_var h)
2488 ; return (HoleCo (h { ch_co_var = c' })) }
2489 go_co cxt (AxiomInstCo ax ind args) = do { args' <- mapM (go_co cxt) args
2490 ; return (mkAxiomInstCo ax ind args') }
2491 go_co cxt (UnivCo p r ty1 ty2) = do { p' <- go_prov cxt p
2492 ; ty1' <- go cxt ty1
2493 ; ty2' <- go cxt ty2
2494 ; return (mkUnivCo p' r ty1' ty2') }
2495 go_co cxt (SymCo co) = do { co' <- go_co cxt co
2496 ; return (mkSymCo co') }
2497 go_co cxt (TransCo co1 co2) = do { co1' <- go_co cxt co1
2498 ; co2' <- go_co cxt co2
2499 ; return (mkTransCo co1' co2') }
2500 go_co cxt (NthCo r n co) = do { co' <- go_co cxt co
2501 ; return (mkNthCo r n co') }
2502 go_co cxt (LRCo lr co) = do { co' <- go_co cxt co
2503 ; return (mkLRCo lr co') }
2504 go_co cxt (InstCo co arg) = do { co' <- go_co cxt co
2505 ; arg' <- go_co cxt arg
2506 ; return (mkInstCo co' arg') }
2507 go_co cxt (CoherenceCo co1 co2) = do { co1' <- go_co cxt co1
2508 ; co2' <- go_co cxt co2
2509 ; return (mkCoherenceCo co1' co2') }
2510 go_co cxt (KindCo co) = do { co' <- go_co cxt co
2511 ; return (mkKindCo co') }
2512 go_co cxt (SubCo co) = do { co' <- go_co cxt co
2513 ; return (mkSubCo co') }
2514 go_co cxt (AxiomRuleCo ax cs) = do { cs' <- mapM (go_co cxt) cs
2515 ; return (mkAxiomRuleCo ax cs') }
2516
2517 ------------------
2518 go_prov _ UnsafeCoerceProv = return UnsafeCoerceProv
2519 go_prov cxt (PhantomProv co) = PhantomProv <$> go_co cxt co
2520 go_prov cxt (ProofIrrelProv co) = ProofIrrelProv <$> go_co cxt co
2521 go_prov _ p@(PluginProv _) = return p
2522
2523
2524 {-
2525 %************************************************************************
2526 %* *
2527 Miscellaneous functions
2528 %* *
2529 %************************************************************************
2530
2531 -}
2532 -- | All type constructors occurring in the type; looking through type
2533 -- synonyms, but not newtypes.
2534 -- When it finds a Class, it returns the class TyCon.
2535 tyConsOfType :: Type -> UniqSet TyCon
2536 tyConsOfType ty
2537 = go ty
2538 where
2539 go :: Type -> UniqSet TyCon -- The UniqSet does duplicate elim
2540 go ty | Just ty' <- coreView ty = go ty'
2541 go (TyVarTy {}) = emptyUniqSet
2542 go (LitTy {}) = emptyUniqSet
2543 go (TyConApp tc tys) = go_tc tc `unionUniqSets` go_s tys
2544 go (AppTy a b) = go a `unionUniqSets` go b
2545 go (FunTy a b) = go a `unionUniqSets` go b `unionUniqSets` go_tc funTyCon
2546 go (ForAllTy (TvBndr tv _) ty) = go ty `unionUniqSets` go (tyVarKind tv)
2547 go (CastTy ty co) = go ty `unionUniqSets` go_co co
2548 go (CoercionTy co) = go_co co
2549
2550 go_co (Refl _ ty) = go ty
2551 go_co (TyConAppCo _ tc args) = go_tc tc `unionUniqSets` go_cos args
2552 go_co (AppCo co arg) = go_co co `unionUniqSets` go_co arg
2553 go_co (ForAllCo _ kind_co co) = go_co kind_co `unionUniqSets` go_co co
2554 go_co (FunCo _ co1 co2) = go_co co1 `unionUniqSets` go_co co2
2555 go_co (AxiomInstCo ax _ args) = go_ax ax `unionUniqSets` go_cos args
2556 go_co (UnivCo p _ t1 t2) = go_prov p `unionUniqSets` go t1 `unionUniqSets` go t2
2557 go_co (CoVarCo {}) = emptyUniqSet
2558 go_co (HoleCo {}) = emptyUniqSet
2559 go_co (SymCo co) = go_co co
2560 go_co (TransCo co1 co2) = go_co co1 `unionUniqSets` go_co co2
2561 go_co (NthCo _ _ co) = go_co co
2562 go_co (LRCo _ co) = go_co co
2563 go_co (InstCo co arg) = go_co co `unionUniqSets` go_co arg
2564 go_co (CoherenceCo co1 co2) = go_co co1 `unionUniqSets` go_co co2
2565 go_co (KindCo co) = go_co co
2566 go_co (SubCo co) = go_co co
2567 go_co (AxiomRuleCo _ cs) = go_cos cs
2568
2569 go_prov UnsafeCoerceProv = emptyUniqSet
2570 go_prov (PhantomProv co) = go_co co
2571 go_prov (ProofIrrelProv co) = go_co co
2572 go_prov (PluginProv _) = emptyUniqSet
2573 -- this last case can happen from the tyConsOfType used from
2574 -- checkTauTvUpdate
2575
2576 go_s tys = foldr (unionUniqSets . go) emptyUniqSet tys
2577 go_cos cos = foldr (unionUniqSets . go_co) emptyUniqSet cos
2578
2579 go_tc tc = unitUniqSet tc
2580 go_ax ax = go_tc $ coAxiomTyCon ax
2581
2582 -- | Find the result 'Kind' of a type synonym,
2583 -- after applying it to its 'arity' number of type variables
2584 -- Actually this function works fine on data types too,
2585 -- but they'd always return '*', so we never need to ask
2586 synTyConResKind :: TyCon -> Kind
2587 synTyConResKind tycon = piResultTys (tyConKind tycon) (mkTyVarTys (tyConTyVars tycon))
2588
2589 -- | Retrieve the free variables in this type, splitting them based
2590 -- on whether they are used visibly or invisibly. Invisible ones come
2591 -- first.
2592 splitVisVarsOfType :: Type -> Pair TyCoVarSet
2593 splitVisVarsOfType orig_ty = Pair invis_vars vis_vars
2594 where
2595 Pair invis_vars1 vis_vars = go orig_ty
2596 invis_vars = invis_vars1 `minusVarSet` vis_vars
2597
2598 go (TyVarTy tv) = Pair (tyCoVarsOfType $ tyVarKind tv) (unitVarSet tv)
2599 go (AppTy t1 t2) = go t1 `mappend` go t2
2600 go (TyConApp tc tys) = go_tc tc tys
2601 go (FunTy t1 t2) = go t1 `mappend` go t2
2602 go (ForAllTy (TvBndr tv _) ty)
2603 = ((`delVarSet` tv) <$> go ty) `mappend`
2604 (invisible (tyCoVarsOfType $ tyVarKind tv))
2605 go (LitTy {}) = mempty
2606 go (CastTy ty co) = go ty `mappend` invisible (tyCoVarsOfCo co)
2607 go (CoercionTy co) = invisible $ tyCoVarsOfCo co
2608
2609 invisible vs = Pair vs emptyVarSet
2610
2611 go_tc tc tys = let (invis, vis) = partitionInvisibles tc id tys in
2612 invisible (tyCoVarsOfTypes invis) `mappend` foldMap go vis
2613
2614 splitVisVarsOfTypes :: [Type] -> Pair TyCoVarSet
2615 splitVisVarsOfTypes = foldMap splitVisVarsOfType
2616
2617 modifyJoinResTy :: Int -- Number of binders to skip
2618 -> (Type -> Type) -- Function to apply to result type
2619 -> Type -- Type of join point
2620 -> Type -- New type
2621 -- INVARIANT: If any of the first n binders are foralls, those tyvars cannot
2622 -- appear in the original result type. See isValidJoinPointType.
2623 modifyJoinResTy orig_ar f orig_ty
2624 = go orig_ar orig_ty
2625 where
2626 go 0 ty = f ty
2627 go n ty | Just (arg_bndr, res_ty) <- splitPiTy_maybe ty
2628 = mkPiTy arg_bndr (go (n-1) res_ty)
2629 | otherwise
2630 = pprPanic "modifyJoinResTy" (ppr orig_ar <+> ppr orig_ty)
2631
2632 setJoinResTy :: Int -- Number of binders to skip
2633 -> Type -- New result type
2634 -> Type -- Type of join point
2635 -> Type -- New type
2636 -- INVARIANT: Same as for modifyJoinResTy
2637 setJoinResTy ar new_res_ty ty
2638 = modifyJoinResTy ar (const new_res_ty) ty
2639
2640 {-
2641 %************************************************************************
2642 %* *
2643 Pretty-printing
2644 %* *
2645 %************************************************************************
2646
2647 Most pretty-printing is either in TyCoRep or IfaceType.
2648
2649 -}
2650
2651 -- | This variant preserves any use of TYPE in a type, effectively
2652 -- locally setting -fprint-explicit-runtime-reps.
2653 pprWithTYPE :: Type -> SDoc
2654 pprWithTYPE ty = updSDocDynFlags (flip gopt_set Opt_PrintExplicitRuntimeReps) $
2655 ppr ty