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