Fix #15954 by rejigging check_type's order
[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, tcRepSplitTyConApp, 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 -- | Like 'tcSplitTyConApp' but doesn't look through type synonyms.
802 tcRepSplitTyConApp :: HasCallStack => Type -> (TyCon, [Type])
803 -- Defined here to avoid module loops between Unify and TcType.
804 tcRepSplitTyConApp ty =
805 case tcRepSplitTyConApp_maybe ty of
806 Just stuff -> stuff
807 Nothing -> pprPanic "tcRepSplitTyConApp" (ppr ty)
808
809 -------------
810 splitAppTy :: Type -> (Type, Type)
811 -- ^ Attempts to take a type application apart, as in 'splitAppTy_maybe',
812 -- and panics if this is not possible
813 splitAppTy ty = case splitAppTy_maybe ty of
814 Just pr -> pr
815 Nothing -> panic "splitAppTy"
816
817 -------------
818 splitAppTys :: Type -> (Type, [Type])
819 -- ^ Recursively splits a type as far as is possible, leaving a residual
820 -- type being applied to and the type arguments applied to it. Never fails,
821 -- even if that means returning an empty list of type applications.
822 splitAppTys ty = split ty ty []
823 where
824 split orig_ty ty args | Just ty' <- coreView ty = split orig_ty ty' args
825 split _ (AppTy ty arg) args = split ty ty (arg:args)
826 split _ (TyConApp tc tc_args) args
827 = let -- keep type families saturated
828 n | mightBeUnsaturatedTyCon tc = 0
829 | otherwise = tyConArity tc
830 (tc_args1, tc_args2) = splitAt n tc_args
831 in
832 (TyConApp tc tc_args1, tc_args2 ++ args)
833 split _ (FunTy ty1 ty2) args
834 = ASSERT( null args )
835 (TyConApp funTyCon [], [rep1, rep2, ty1, ty2])
836 where
837 rep1 = getRuntimeRep ty1
838 rep2 = getRuntimeRep ty2
839
840 split orig_ty _ args = (orig_ty, args)
841
842 -- | Like 'splitAppTys', but doesn't look through type synonyms
843 repSplitAppTys :: HasDebugCallStack => Type -> (Type, [Type])
844 repSplitAppTys ty = split ty []
845 where
846 split (AppTy ty arg) args = split ty (arg:args)
847 split (TyConApp tc tc_args) args
848 = let n | mightBeUnsaturatedTyCon tc = 0
849 | otherwise = tyConArity tc
850 (tc_args1, tc_args2) = splitAt n tc_args
851 in
852 (TyConApp tc tc_args1, tc_args2 ++ args)
853 split (FunTy ty1 ty2) args
854 = ASSERT( null args )
855 (TyConApp funTyCon [], [rep1, rep2, ty1, ty2])
856 where
857 rep1 = getRuntimeRep ty1
858 rep2 = getRuntimeRep ty2
859
860 split ty args = (ty, args)
861
862 {-
863 LitTy
864 ~~~~~
865 -}
866
867 mkNumLitTy :: Integer -> Type
868 mkNumLitTy n = LitTy (NumTyLit n)
869
870 -- | Is this a numeric literal. We also look through type synonyms.
871 isNumLitTy :: Type -> Maybe Integer
872 isNumLitTy ty | Just ty1 <- coreView ty = isNumLitTy ty1
873 isNumLitTy (LitTy (NumTyLit n)) = Just n
874 isNumLitTy _ = Nothing
875
876 mkStrLitTy :: FastString -> Type
877 mkStrLitTy s = LitTy (StrTyLit s)
878
879 -- | Is this a symbol literal. We also look through type synonyms.
880 isStrLitTy :: Type -> Maybe FastString
881 isStrLitTy ty | Just ty1 <- coreView ty = isStrLitTy ty1
882 isStrLitTy (LitTy (StrTyLit s)) = Just s
883 isStrLitTy _ = Nothing
884
885 -- | Is this a type literal (symbol or numeric).
886 isLitTy :: Type -> Maybe TyLit
887 isLitTy ty | Just ty1 <- coreView ty = isLitTy ty1
888 isLitTy (LitTy l) = Just l
889 isLitTy _ = Nothing
890
891 -- | Is this type a custom user error?
892 -- If so, give us the kind and the error message.
893 userTypeError_maybe :: Type -> Maybe Type
894 userTypeError_maybe t
895 = do { (tc, _kind : msg : _) <- splitTyConApp_maybe t
896 -- There may be more than 2 arguments, if the type error is
897 -- used as a type constructor (e.g. at kind `Type -> Type`).
898
899 ; guard (tyConName tc == errorMessageTypeErrorFamName)
900 ; return msg }
901
902 -- | Render a type corresponding to a user type error into a SDoc.
903 pprUserTypeErrorTy :: Type -> SDoc
904 pprUserTypeErrorTy ty =
905 case splitTyConApp_maybe ty of
906
907 -- Text "Something"
908 Just (tc,[txt])
909 | tyConName tc == typeErrorTextDataConName
910 , Just str <- isStrLitTy txt -> ftext str
911
912 -- ShowType t
913 Just (tc,[_k,t])
914 | tyConName tc == typeErrorShowTypeDataConName -> ppr t
915
916 -- t1 :<>: t2
917 Just (tc,[t1,t2])
918 | tyConName tc == typeErrorAppendDataConName ->
919 pprUserTypeErrorTy t1 <> pprUserTypeErrorTy t2
920
921 -- t1 :$$: t2
922 Just (tc,[t1,t2])
923 | tyConName tc == typeErrorVAppendDataConName ->
924 pprUserTypeErrorTy t1 $$ pprUserTypeErrorTy t2
925
926 -- An unevaluated type function
927 _ -> ppr ty
928
929
930
931
932 {-
933 ---------------------------------------------------------------------
934 FunTy
935 ~~~~~
936
937 Note [Representation of function types]
938 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
939
940 Functions (e.g. Int -> Char) can be thought of as being applications
941 of funTyCon (known in Haskell surface syntax as (->)),
942
943 (->) :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
944 (a :: TYPE r1) (b :: TYPE r2).
945 a -> b -> Type
946
947 However, for efficiency's sake we represent saturated applications of (->)
948 with FunTy. For instance, the type,
949
950 (->) r1 r2 a b
951
952 is equivalent to,
953
954 FunTy (Anon a) b
955
956 Note how the RuntimeReps are implied in the FunTy representation. For this
957 reason we must be careful when recontructing the TyConApp representation (see,
958 for instance, splitTyConApp_maybe).
959
960 In the compiler we maintain the invariant that all saturated applications of
961 (->) are represented with FunTy.
962
963 See #11714.
964 -}
965
966 isFunTy :: Type -> Bool
967 isFunTy ty = isJust (splitFunTy_maybe ty)
968
969 splitFunTy :: Type -> (Type, Type)
970 -- ^ Attempts to extract the argument and result types from a type, and
971 -- panics if that is not possible. See also 'splitFunTy_maybe'
972 splitFunTy ty | Just ty' <- coreView ty = splitFunTy ty'
973 splitFunTy (FunTy arg res) = (arg, res)
974 splitFunTy other = pprPanic "splitFunTy" (ppr other)
975
976 splitFunTy_maybe :: Type -> Maybe (Type, Type)
977 -- ^ Attempts to extract the argument and result types from a type
978 splitFunTy_maybe ty | Just ty' <- coreView ty = splitFunTy_maybe ty'
979 splitFunTy_maybe (FunTy arg res) = Just (arg, res)
980 splitFunTy_maybe _ = Nothing
981
982 splitFunTys :: Type -> ([Type], Type)
983 splitFunTys ty = split [] ty ty
984 where
985 split args orig_ty ty | Just ty' <- coreView ty = split args orig_ty ty'
986 split args _ (FunTy arg res) = split (arg:args) res res
987 split args orig_ty _ = (reverse args, orig_ty)
988
989 funResultTy :: Type -> Type
990 -- ^ Extract the function result type and panic if that is not possible
991 funResultTy ty | Just ty' <- coreView ty = funResultTy ty'
992 funResultTy (FunTy _ res) = res
993 funResultTy ty = pprPanic "funResultTy" (ppr ty)
994
995 funArgTy :: Type -> Type
996 -- ^ Extract the function argument type and panic if that is not possible
997 funArgTy ty | Just ty' <- coreView ty = funArgTy ty'
998 funArgTy (FunTy arg _res) = arg
999 funArgTy ty = pprPanic "funArgTy" (ppr ty)
1000
1001 -- ^ Just like 'piResultTys' but for a single argument
1002 -- Try not to iterate 'piResultTy', because it's inefficient to substitute
1003 -- one variable at a time; instead use 'piResultTys"
1004 piResultTy :: HasDebugCallStack => Type -> Type -> Type
1005 piResultTy ty arg = case piResultTy_maybe ty arg of
1006 Just res -> res
1007 Nothing -> pprPanic "piResultTy" (ppr ty $$ ppr arg)
1008
1009 piResultTy_maybe :: Type -> Type -> Maybe Type
1010 piResultTy_maybe ty arg
1011 | Just ty' <- coreView ty = piResultTy_maybe ty' arg
1012
1013 | FunTy _ res <- ty
1014 = Just res
1015
1016 | ForAllTy (Bndr tv _) res <- ty
1017 = let empty_subst = mkEmptyTCvSubst $ mkInScopeSet $
1018 tyCoVarsOfTypes [arg,res]
1019 in Just (substTy (extendTCvSubst empty_subst tv arg) res)
1020
1021 | otherwise
1022 = Nothing
1023
1024 -- | (piResultTys f_ty [ty1, .., tyn]) gives the type of (f ty1 .. tyn)
1025 -- where f :: f_ty
1026 -- 'piResultTys' is interesting because:
1027 -- 1. 'f_ty' may have more for-alls than there are args
1028 -- 2. Less obviously, it may have fewer for-alls
1029 -- For case 2. think of:
1030 -- piResultTys (forall a.a) [forall b.b, Int]
1031 -- This really can happen, but only (I think) in situations involving
1032 -- undefined. For example:
1033 -- undefined :: forall a. a
1034 -- Term: undefined @(forall b. b->b) @Int
1035 -- This term should have type (Int -> Int), but notice that
1036 -- there are more type args than foralls in 'undefined's type.
1037
1038 -- If you edit this function, you may need to update the GHC formalism
1039 -- See Note [GHC Formalism] in coreSyn/CoreLint.hs
1040
1041 -- This is a heavily used function (e.g. from typeKind),
1042 -- so we pay attention to efficiency, especially in the special case
1043 -- where there are no for-alls so we are just dropping arrows from
1044 -- a function type/kind.
1045 piResultTys :: HasDebugCallStack => Type -> [Type] -> Type
1046 piResultTys ty [] = ty
1047 piResultTys ty orig_args@(arg:args)
1048 | Just ty' <- coreView ty
1049 = piResultTys ty' orig_args
1050
1051 | FunTy _ res <- ty
1052 = piResultTys res args
1053
1054 | ForAllTy (Bndr tv _) res <- ty
1055 = go (extendTCvSubst init_subst tv arg) res args
1056
1057 | otherwise
1058 = pprPanic "piResultTys1" (ppr ty $$ ppr orig_args)
1059 where
1060 init_subst = mkEmptyTCvSubst $ mkInScopeSet (tyCoVarsOfTypes (ty:orig_args))
1061
1062 go :: TCvSubst -> Type -> [Type] -> Type
1063 go subst ty [] = substTy subst ty
1064
1065 go subst ty all_args@(arg:args)
1066 | Just ty' <- coreView ty
1067 = go subst ty' all_args
1068
1069 | FunTy _ res <- ty
1070 = go subst res args
1071
1072 | ForAllTy (Bndr tv _) res <- ty
1073 = go (extendTCvSubst subst tv arg) res args
1074
1075 | not (isEmptyTCvSubst subst) -- See Note [Care with kind instantiation]
1076 = go init_subst
1077 (substTy subst ty)
1078 all_args
1079
1080 | otherwise
1081 = -- We have not run out of arguments, but the function doesn't
1082 -- have the right kind to apply to them; so panic.
1083 -- Without the explicit isEmptyVarEnv test, an ill-kinded type
1084 -- would give an infniite loop, which is very unhelpful
1085 -- c.f. Trac #15473
1086 pprPanic "piResultTys2" (ppr ty $$ ppr orig_args $$ ppr all_args)
1087
1088 applyTysX :: [TyVar] -> Type -> [Type] -> Type
1089 -- applyTyxX beta-reduces (/\tvs. body_ty) arg_tys
1090 -- Assumes that (/\tvs. body_ty) is closed
1091 applyTysX tvs body_ty arg_tys
1092 = ASSERT2( arg_tys `lengthAtLeast` n_tvs, pp_stuff )
1093 ASSERT2( tyCoVarsOfType body_ty `subVarSet` mkVarSet tvs, pp_stuff )
1094 mkAppTys (substTyWith tvs (take n_tvs arg_tys) body_ty)
1095 (drop n_tvs arg_tys)
1096 where
1097 pp_stuff = vcat [ppr tvs, ppr body_ty, ppr arg_tys]
1098 n_tvs = length tvs
1099
1100
1101
1102 {- Note [Care with kind instantiation]
1103 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1104 Suppose we have
1105 T :: forall k. k
1106 and we are finding the kind of
1107 T (forall b. b -> b) * Int
1108 Then
1109 T (forall b. b->b) :: k[ k :-> forall b. b->b]
1110 :: forall b. b -> b
1111 So
1112 T (forall b. b->b) * :: (b -> b)[ b :-> *]
1113 :: * -> *
1114
1115 In other words we must intantiate the forall!
1116
1117 Similarly (Trac #15428)
1118 S :: forall k f. k -> f k
1119 and we are finding the kind of
1120 S * (* ->) Int Bool
1121 We have
1122 S * (* ->) :: (k -> f k)[ k :-> *, f :-> (* ->)]
1123 :: * -> * -> *
1124 So again we must instantiate.
1125
1126 The same thing happens in ToIface.toIfaceAppArgsX.
1127
1128
1129 ---------------------------------------------------------------------
1130 TyConApp
1131 ~~~~~~~~
1132 -}
1133
1134 -- | A key function: builds a 'TyConApp' or 'FunTy' as appropriate to
1135 -- its arguments. Applies its arguments to the constructor from left to right.
1136 mkTyConApp :: TyCon -> [Type] -> Type
1137 mkTyConApp tycon tys
1138 | isFunTyCon tycon
1139 , [_rep1,_rep2,ty1,ty2] <- tys
1140 = FunTy ty1 ty2
1141
1142 | otherwise
1143 = TyConApp tycon tys
1144
1145 -- splitTyConApp "looks through" synonyms, because they don't
1146 -- mean a distinct type, but all other type-constructor applications
1147 -- including functions are returned as Just ..
1148
1149 -- | Retrieve the tycon heading this type, if there is one. Does /not/
1150 -- look through synonyms.
1151 tyConAppTyConPicky_maybe :: Type -> Maybe TyCon
1152 tyConAppTyConPicky_maybe (TyConApp tc _) = Just tc
1153 tyConAppTyConPicky_maybe (FunTy {}) = Just funTyCon
1154 tyConAppTyConPicky_maybe _ = Nothing
1155
1156
1157 -- | The same as @fst . splitTyConApp@
1158 tyConAppTyCon_maybe :: Type -> Maybe TyCon
1159 tyConAppTyCon_maybe ty | Just ty' <- coreView ty = tyConAppTyCon_maybe ty'
1160 tyConAppTyCon_maybe (TyConApp tc _) = Just tc
1161 tyConAppTyCon_maybe (FunTy {}) = Just funTyCon
1162 tyConAppTyCon_maybe _ = Nothing
1163
1164 tyConAppTyCon :: Type -> TyCon
1165 tyConAppTyCon ty = tyConAppTyCon_maybe ty `orElse` pprPanic "tyConAppTyCon" (ppr ty)
1166
1167 -- | The same as @snd . splitTyConApp@
1168 tyConAppArgs_maybe :: Type -> Maybe [Type]
1169 tyConAppArgs_maybe ty | Just ty' <- coreView ty = tyConAppArgs_maybe ty'
1170 tyConAppArgs_maybe (TyConApp _ tys) = Just tys
1171 tyConAppArgs_maybe (FunTy arg res)
1172 | Just rep1 <- getRuntimeRep_maybe arg
1173 , Just rep2 <- getRuntimeRep_maybe res
1174 = Just [rep1, rep2, arg, res]
1175 tyConAppArgs_maybe _ = Nothing
1176
1177 tyConAppArgs :: Type -> [Type]
1178 tyConAppArgs ty = tyConAppArgs_maybe ty `orElse` pprPanic "tyConAppArgs" (ppr ty)
1179
1180 tyConAppArgN :: Int -> Type -> Type
1181 -- Executing Nth
1182 tyConAppArgN n ty
1183 = case tyConAppArgs_maybe ty of
1184 Just tys -> ASSERT2( tys `lengthExceeds` n, ppr n <+> ppr tys ) tys `getNth` n
1185 Nothing -> pprPanic "tyConAppArgN" (ppr n <+> 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. Panics if that is not possible.
1189 -- See also 'splitTyConApp_maybe'
1190 splitTyConApp :: Type -> (TyCon, [Type])
1191 splitTyConApp ty = case splitTyConApp_maybe ty of
1192 Just stuff -> stuff
1193 Nothing -> pprPanic "splitTyConApp" (ppr ty)
1194
1195 -- | Attempts to tease a type apart into a type constructor and the application
1196 -- of a number of arguments to that constructor
1197 splitTyConApp_maybe :: HasDebugCallStack => Type -> Maybe (TyCon, [Type])
1198 splitTyConApp_maybe ty | Just ty' <- coreView ty = splitTyConApp_maybe ty'
1199 splitTyConApp_maybe ty = repSplitTyConApp_maybe ty
1200
1201 -- | Like 'splitTyConApp_maybe', but doesn't look through synonyms. This
1202 -- assumes the synonyms have already been dealt with.
1203 repSplitTyConApp_maybe :: HasDebugCallStack => Type -> Maybe (TyCon, [Type])
1204 repSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
1205 repSplitTyConApp_maybe (FunTy arg res)
1206 | Just arg_rep <- getRuntimeRep_maybe arg
1207 , Just res_rep <- getRuntimeRep_maybe res
1208 = Just (funTyCon, [arg_rep, res_rep, arg, res])
1209 repSplitTyConApp_maybe _ = Nothing
1210
1211 -- | Attempts to tease a list type apart and gives the type of the elements if
1212 -- successful (looks through type synonyms)
1213 splitListTyConApp_maybe :: Type -> Maybe Type
1214 splitListTyConApp_maybe ty = case splitTyConApp_maybe ty of
1215 Just (tc,[e]) | tc == listTyCon -> Just e
1216 _other -> Nothing
1217
1218 nextRole :: Type -> Role
1219 nextRole ty
1220 | Just (tc, tys) <- splitTyConApp_maybe ty
1221 , let num_tys = length tys
1222 , num_tys < tyConArity tc
1223 = tyConRoles tc `getNth` num_tys
1224
1225 | otherwise
1226 = Nominal
1227
1228 newTyConInstRhs :: TyCon -> [Type] -> Type
1229 -- ^ Unwrap one 'layer' of newtype on a type constructor and its
1230 -- arguments, using an eta-reduced version of the @newtype@ if possible.
1231 -- This requires tys to have at least @newTyConInstArity tycon@ elements.
1232 newTyConInstRhs tycon tys
1233 = ASSERT2( tvs `leLength` tys, ppr tycon $$ ppr tys $$ ppr tvs )
1234 applyTysX tvs rhs tys
1235 where
1236 (tvs, rhs) = newTyConEtadRhs tycon
1237
1238 {-
1239 ---------------------------------------------------------------------
1240 CastTy
1241 ~~~~~~
1242 A casted type has its *kind* casted into something new.
1243
1244 Note [Weird typing rule for ForAllTy]
1245 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1246 Here is the (truncated) typing rule for the dependent ForAllTy:
1247
1248 inner : kind
1249 ------------------------------------
1250 ForAllTy (Bndr tyvar vis) inner : kind
1251
1252 inner : TYPE r
1253 ------------------------------------
1254 ForAllTy (Bndr covar vis) inner : TYPE
1255
1256 Note that when inside the binder is a tyvar, neither the inner type nor for
1257 ForAllTy itself have to have kind *! But, it means that we should push any kind
1258 casts through the ForAllTy. The only trouble is avoiding capture.
1259 -}
1260
1261 splitCastTy_maybe :: Type -> Maybe (Type, Coercion)
1262 splitCastTy_maybe ty | Just ty' <- coreView ty = splitCastTy_maybe ty'
1263 splitCastTy_maybe (CastTy ty co) = Just (ty, co)
1264 splitCastTy_maybe _ = Nothing
1265
1266 -- | Make a 'CastTy'. The Coercion must be nominal. Checks the
1267 -- Coercion for reflexivity, dropping it if it's reflexive.
1268 -- See Note [Respecting definitional equality] in TyCoRep
1269 mkCastTy :: Type -> Coercion -> Type
1270 mkCastTy ty co | isReflexiveCo co = ty -- (EQ2) from the Note
1271 -- NB: Do the slow check here. This is important to keep the splitXXX
1272 -- functions working properly. Otherwise, we may end up with something
1273 -- like (((->) |> something_reflexive_but_not_obviously_so) biz baz)
1274 -- fails under splitFunTy_maybe. This happened with the cheaper check
1275 -- in test dependent/should_compile/dynamic-paper.
1276
1277 mkCastTy (CastTy ty co1) co2
1278 -- (EQ3) from the Note
1279 = mkCastTy ty (co1 `mkTransCo` co2)
1280 -- call mkCastTy again for the reflexivity check
1281
1282 mkCastTy (ForAllTy (Bndr tv vis) inner_ty) co
1283 -- (EQ4) from the Note
1284 | isTyVar tv
1285 , let fvs = tyCoVarsOfCo co
1286 = -- have to make sure that pushing the co in doesn't capture the bound var!
1287 if tv `elemVarSet` fvs
1288 then let empty_subst = mkEmptyTCvSubst (mkInScopeSet fvs)
1289 (subst, tv') = substVarBndr empty_subst tv
1290 in ForAllTy (Bndr tv' vis) (substTy subst inner_ty `mkCastTy` co)
1291 else ForAllTy (Bndr tv vis) (inner_ty `mkCastTy` co)
1292
1293 mkCastTy ty co = CastTy ty co
1294
1295 tyConBindersTyCoBinders :: [TyConBinder] -> [TyCoBinder]
1296 -- Return the tyConBinders in TyCoBinder form
1297 tyConBindersTyCoBinders = map to_tyb
1298 where
1299 to_tyb (Bndr tv (NamedTCB vis)) = Named (Bndr tv vis)
1300 to_tyb (Bndr tv AnonTCB) = Anon (varType tv)
1301
1302 {-
1303 --------------------------------------------------------------------
1304 CoercionTy
1305 ~~~~~~~~~~
1306 CoercionTy allows us to inject coercions into types. A CoercionTy
1307 should appear only in the right-hand side of an application.
1308 -}
1309
1310 mkCoercionTy :: Coercion -> Type
1311 mkCoercionTy = CoercionTy
1312
1313 isCoercionTy :: Type -> Bool
1314 isCoercionTy (CoercionTy _) = True
1315 isCoercionTy _ = False
1316
1317 isCoercionTy_maybe :: Type -> Maybe Coercion
1318 isCoercionTy_maybe (CoercionTy co) = Just co
1319 isCoercionTy_maybe _ = Nothing
1320
1321 stripCoercionTy :: Type -> Coercion
1322 stripCoercionTy (CoercionTy co) = co
1323 stripCoercionTy ty = pprPanic "stripCoercionTy" (ppr ty)
1324
1325 {-
1326 ---------------------------------------------------------------------
1327 SynTy
1328 ~~~~~
1329
1330 Notes on type synonyms
1331 ~~~~~~~~~~~~~~~~~~~~~~
1332 The various "split" functions (splitFunTy, splitRhoTy, splitForAllTy) try
1333 to return type synonyms wherever possible. Thus
1334
1335 type Foo a = a -> a
1336
1337 we want
1338 splitFunTys (a -> Foo a) = ([a], Foo a)
1339 not ([a], a -> a)
1340
1341 The reason is that we then get better (shorter) type signatures in
1342 interfaces. Notably this plays a role in tcTySigs in TcBinds.hs.
1343
1344
1345 ---------------------------------------------------------------------
1346 ForAllTy
1347 ~~~~~~~~
1348 -}
1349
1350 -- | Make a dependent forall over an Inferred variablem
1351 mkTyCoInvForAllTy :: TyCoVar -> Type -> Type
1352 mkTyCoInvForAllTy tv ty
1353 | isCoVar tv
1354 , not (tv `elemVarSet` tyCoVarsOfType ty)
1355 = mkFunTy (varType tv) ty
1356 | otherwise
1357 = ForAllTy (Bndr tv Inferred) ty
1358
1359 -- | Like mkTyCoInvForAllTy, but tv should be a tyvar
1360 mkInvForAllTy :: TyVar -> Type -> Type
1361 mkInvForAllTy tv ty = ASSERT( isTyVar tv )
1362 ForAllTy (Bndr tv Inferred) ty
1363
1364 -- | Like mkForAllTys, but assumes all variables are dependent and Inferred,
1365 -- a common case
1366 mkTyCoInvForAllTys :: [TyCoVar] -> Type -> Type
1367 mkTyCoInvForAllTys tvs ty = foldr mkTyCoInvForAllTy ty tvs
1368
1369 -- | Like 'mkTyCoInvForAllTys', but tvs should be a list of tyvar
1370 mkInvForAllTys :: [TyVar] -> Type -> Type
1371 mkInvForAllTys tvs ty = foldr mkInvForAllTy ty tvs
1372
1373 -- | Like mkForAllTys, but assumes all variables are dependent and Specified,
1374 -- a common case
1375 mkSpecForAllTys :: [TyVar] -> Type -> Type
1376 mkSpecForAllTys tvs = ASSERT( all isTyVar tvs )
1377 -- covar is always Inferred, so all inputs should be tyvar
1378 mkForAllTys [ Bndr tv Specified | tv <- tvs ]
1379
1380 -- | Like mkForAllTys, but assumes all variables are dependent and visible
1381 mkVisForAllTys :: [TyVar] -> Type -> Type
1382 mkVisForAllTys tvs = ASSERT( all isTyVar tvs )
1383 -- covar is always Inferred, so all inputs should be tyvar
1384 mkForAllTys [ Bndr tv Required | tv <- tvs ]
1385
1386 mkLamType :: Var -> Type -> Type
1387 -- ^ Makes a @(->)@ type or an implicit forall type, depending
1388 -- on whether it is given a type variable or a term variable.
1389 -- This is used, for example, when producing the type of a lambda.
1390 -- Always uses Inferred binders.
1391 mkLamTypes :: [Var] -> Type -> Type
1392 -- ^ 'mkLamType' for multiple type or value arguments
1393
1394 mkLamType v ty
1395 | isCoVar v
1396 , v `elemVarSet` tyCoVarsOfType ty
1397 = ForAllTy (Bndr v Inferred) ty
1398 | isTyVar v
1399 = ForAllTy (Bndr v Inferred) ty
1400 | otherwise
1401 = FunTy (varType v) ty
1402
1403 mkLamTypes vs ty = foldr mkLamType ty vs
1404
1405 -- | Given a list of type-level vars and a result kind,
1406 -- makes TyCoBinders, preferring anonymous binders
1407 -- if the variable is, in fact, not dependent.
1408 -- e.g. mkTyConBindersPreferAnon [(k:*),(b:k),(c:k)] (k->k)
1409 -- We want (k:*) Named, (b:k) Anon, (c:k) Anon
1410 --
1411 -- All non-coercion binders are /visible/.
1412 mkTyConBindersPreferAnon :: [TyVar] -> TyCoVarSet -> [TyConBinder]
1413 mkTyConBindersPreferAnon vars inner_tkvs = ASSERT( all isTyVar vars)
1414 fst (go vars)
1415 where
1416 go :: [TyVar] -> ([TyConBinder], VarSet) -- also returns the free vars
1417 go [] = ([], inner_tkvs)
1418 go (v:vs) | v `elemVarSet` fvs
1419 = ( Bndr v (NamedTCB Required) : binders
1420 , fvs `delVarSet` v `unionVarSet` kind_vars )
1421 | otherwise
1422 = ( Bndr v AnonTCB : binders
1423 , fvs `unionVarSet` kind_vars )
1424 where
1425 (binders, fvs) = go vs
1426 kind_vars = tyCoVarsOfType $ tyVarKind v
1427
1428 -- | Take a ForAllTy apart, returning the list of tycovars and the result type.
1429 -- This always succeeds, even if it returns only an empty list. Note that the
1430 -- result type returned may have free variables that were bound by a forall.
1431 splitForAllTys :: Type -> ([TyCoVar], Type)
1432 splitForAllTys ty = split ty ty []
1433 where
1434 split orig_ty ty tvs | Just ty' <- coreView ty = split orig_ty ty' tvs
1435 split _ (ForAllTy (Bndr tv _) ty) tvs = split ty ty (tv:tvs)
1436 split orig_ty _ tvs = (reverse tvs, orig_ty)
1437
1438 -- | Like splitForAllTys, but split only for tyvars.
1439 -- This always succeeds, even if it returns only an empty list. Note that the
1440 -- result type returned may have free variables that were bound by a forall.
1441 splitTyVarForAllTys :: Type -> ([TyVar], Type)
1442 splitTyVarForAllTys ty = split ty ty []
1443 where
1444 split orig_ty ty tvs | Just ty' <- coreView ty = split orig_ty ty' tvs
1445 split _ (ForAllTy (Bndr tv _) ty) tvs | isTyVar tv = split ty ty (tv:tvs)
1446 split orig_ty _ tvs = (reverse tvs, orig_ty)
1447
1448 -- | Checks whether this is a proper forall (with a named binder)
1449 isForAllTy :: Type -> Bool
1450 isForAllTy ty | Just ty' <- coreView ty = isForAllTy ty'
1451 isForAllTy (ForAllTy {}) = True
1452 isForAllTy _ = False
1453
1454 -- | Like `isForAllTy`, but returns True only if it is a tyvar binder
1455 isForAllTy_ty :: Type -> Bool
1456 isForAllTy_ty ty | Just ty' <- coreView ty = isForAllTy_ty ty'
1457 isForAllTy_ty (ForAllTy (Bndr tv _) _) | isTyVar tv = True
1458 isForAllTy_ty _ = False
1459
1460 -- | Like `isForAllTy`, but returns True only if it is a covar binder
1461 isForAllTy_co :: Type -> Bool
1462 isForAllTy_co ty | Just ty' <- coreView ty = isForAllTy_co ty'
1463 isForAllTy_co (ForAllTy (Bndr tv _) _) | isCoVar tv = True
1464 isForAllTy_co _ = False
1465
1466 -- | Is this a function or forall?
1467 isPiTy :: Type -> Bool
1468 isPiTy ty | Just ty' <- coreView ty = isForAllTy ty'
1469 isPiTy (ForAllTy {}) = True
1470 isPiTy (FunTy {}) = True
1471 isPiTy _ = False
1472
1473 -- | Take a forall type apart, or panics if that is not possible.
1474 splitForAllTy :: Type -> (TyCoVar, Type)
1475 splitForAllTy ty
1476 | Just answer <- splitForAllTy_maybe ty = answer
1477 | otherwise = pprPanic "splitForAllTy" (ppr ty)
1478
1479 -- | Drops all ForAllTys
1480 dropForAlls :: Type -> Type
1481 dropForAlls ty = go ty
1482 where
1483 go ty | Just ty' <- coreView ty = go ty'
1484 go (ForAllTy _ res) = go res
1485 go res = res
1486
1487 -- | Attempts to take a forall type apart, but only if it's a proper forall,
1488 -- with a named binder
1489 splitForAllTy_maybe :: Type -> Maybe (TyCoVar, Type)
1490 splitForAllTy_maybe ty = go ty
1491 where
1492 go ty | Just ty' <- coreView ty = go ty'
1493 go (ForAllTy (Bndr tv _) ty) = Just (tv, ty)
1494 go _ = Nothing
1495
1496 -- | Like splitForAllTy_maybe, but only returns Just if it is a tyvar binder.
1497 splitForAllTy_ty_maybe :: Type -> Maybe (TyCoVar, Type)
1498 splitForAllTy_ty_maybe ty = go ty
1499 where
1500 go ty | Just ty' <- coreView ty = go ty'
1501 go (ForAllTy (Bndr tv _) ty) | isTyVar tv = Just (tv, ty)
1502 go _ = Nothing
1503
1504 -- | Like splitForAllTy_maybe, but only returns Just if it is a covar binder.
1505 splitForAllTy_co_maybe :: Type -> Maybe (TyCoVar, Type)
1506 splitForAllTy_co_maybe ty = go ty
1507 where
1508 go ty | Just ty' <- coreView ty = go ty'
1509 go (ForAllTy (Bndr tv _) ty) | isCoVar tv = Just (tv, ty)
1510 go _ = Nothing
1511
1512 -- | Attempts to take a forall type apart; works with proper foralls and
1513 -- functions
1514 splitPiTy_maybe :: Type -> Maybe (TyCoBinder, Type)
1515 splitPiTy_maybe ty = go ty
1516 where
1517 go ty | Just ty' <- coreView ty = go ty'
1518 go (ForAllTy bndr ty) = Just (Named bndr, ty)
1519 go (FunTy arg res) = Just (Anon arg, res)
1520 go _ = Nothing
1521
1522 -- | Takes a forall type apart, or panics
1523 splitPiTy :: Type -> (TyCoBinder, Type)
1524 splitPiTy ty
1525 | Just answer <- splitPiTy_maybe ty = answer
1526 | otherwise = pprPanic "splitPiTy" (ppr ty)
1527
1528 -- | Split off all TyCoBinders to a type, splitting both proper foralls
1529 -- and functions
1530 splitPiTys :: Type -> ([TyCoBinder], Type)
1531 splitPiTys ty = split ty ty []
1532 where
1533 split orig_ty ty bs | Just ty' <- coreView ty = split orig_ty ty' bs
1534 split _ (ForAllTy b res) bs = split res res (Named b : bs)
1535 split _ (FunTy arg res) bs = split res res (Anon arg : bs)
1536 split orig_ty _ bs = (reverse bs, orig_ty)
1537
1538 -- | Like 'splitPiTys' but split off only /named/ binders
1539 -- and returns TyCoVarBinders rather than TyCoBinders
1540 splitForAllVarBndrs :: Type -> ([TyCoVarBinder], Type)
1541 splitForAllVarBndrs ty = split ty ty []
1542 where
1543 split orig_ty ty bs | Just ty' <- coreView ty = split orig_ty ty' bs
1544 split _ (ForAllTy b res) bs = split res res (b:bs)
1545 split orig_ty _ bs = (reverse bs, orig_ty)
1546 {-# INLINE splitForAllVarBndrs #-}
1547
1548 invisibleTyBndrCount :: Type -> Int
1549 -- Returns the number of leading invisible forall'd binders in the type
1550 -- Includes invisible predicate arguments; e.g. for
1551 -- e.g. forall {k}. (k ~ *) => k -> k
1552 -- returns 2 not 1
1553 invisibleTyBndrCount ty = length (fst (splitPiTysInvisible ty))
1554
1555 -- Like splitPiTys, but returns only *invisible* binders, including constraints
1556 -- Stops at the first visible binder
1557 splitPiTysInvisible :: Type -> ([TyCoBinder], Type)
1558 splitPiTysInvisible ty = split ty ty []
1559 where
1560 split orig_ty ty bs
1561 | Just ty' <- coreView ty = split orig_ty ty' bs
1562 split _ (ForAllTy b res) bs
1563 | Bndr _ vis <- b
1564 , isInvisibleArgFlag vis = split res res (Named b : bs)
1565 split _ (FunTy arg res) bs
1566 | isPredTy arg = split res res (Anon arg : bs)
1567 split orig_ty _ bs = (reverse bs, orig_ty)
1568
1569 splitPiTysInvisibleN :: Int -> Type -> ([TyCoBinder], Type)
1570 -- Same as splitPiTysInvisible, but stop when
1571 -- - you have found 'n' TyCoBinders,
1572 -- - or you run out of invisible binders
1573 splitPiTysInvisibleN n ty = split n ty ty []
1574 where
1575 split n orig_ty ty bs
1576 | n == 0 = (reverse bs, orig_ty)
1577 | Just ty' <- coreView ty = split n orig_ty ty' bs
1578 | ForAllTy b res <- ty
1579 , Bndr _ vis <- b
1580 , isInvisibleArgFlag vis = split (n-1) res res (Named b : bs)
1581 | FunTy arg res <- ty
1582 , isPredTy arg = split (n-1) res res (Anon arg : bs)
1583 | otherwise = (reverse bs, orig_ty)
1584
1585 -- | Given a 'TyCon' and a list of argument types, filter out any invisible
1586 -- (i.e., 'Inferred' or 'Specified') arguments.
1587 filterOutInvisibleTypes :: TyCon -> [Type] -> [Type]
1588 filterOutInvisibleTypes tc tys = snd $ partitionInvisibleTypes tc tys
1589
1590 -- | Given a 'TyCon' and a list of argument types, filter out any 'Inferred'
1591 -- arguments.
1592 filterOutInferredTypes :: TyCon -> [Type] -> [Type]
1593 filterOutInferredTypes tc tys =
1594 filterByList (map (/= Inferred) $ tyConArgFlags tc tys) tys
1595
1596 -- | Given a 'TyCon' and a list of argument types, partition the arguments
1597 -- into:
1598 --
1599 -- 1. 'Inferred' or 'Specified' (i.e., invisible) arguments and
1600 --
1601 -- 2. 'Required' (i.e., visible) arguments
1602 partitionInvisibleTypes :: TyCon -> [Type] -> ([Type], [Type])
1603 partitionInvisibleTypes tc tys =
1604 partitionByList (map isInvisibleArgFlag $ tyConArgFlags tc tys) tys
1605
1606 -- | Given a list of things paired with their visibilities, partition the
1607 -- things into (invisible things, visible things).
1608 partitionInvisibles :: [(a, ArgFlag)] -> ([a], [a])
1609 partitionInvisibles = partitionWith pick_invis
1610 where
1611 pick_invis :: (a, ArgFlag) -> Either a a
1612 pick_invis (thing, vis) | isInvisibleArgFlag vis = Left thing
1613 | otherwise = Right thing
1614
1615 -- | Given a 'TyCon' and a list of argument types to which the 'TyCon' is
1616 -- applied, determine each argument's visibility
1617 -- ('Inferred', 'Specified', or 'Required').
1618 --
1619 -- Wrinkle: consider the following scenario:
1620 --
1621 -- > T :: forall k. k -> k
1622 -- > tyConArgFlags T [forall m. m -> m -> m, S, R, Q]
1623 --
1624 -- After substituting, we get
1625 --
1626 -- > T (forall m. m -> m -> m) :: (forall m. m -> m -> m) -> forall n. n -> n -> n
1627 --
1628 -- Thus, the first argument is invisible, @S@ is visible, @R@ is invisible again,
1629 -- and @Q@ is visible.
1630 tyConArgFlags :: TyCon -> [Type] -> [ArgFlag]
1631 tyConArgFlags tc = fun_kind_arg_flags (tyConKind tc)
1632
1633 -- | Given a 'Type' and a list of argument types to which the 'Type' is
1634 -- applied, determine each argument's visibility
1635 -- ('Inferred', 'Specified', or 'Required').
1636 --
1637 -- Most of the time, the arguments will be 'Required', but not always. Consider
1638 -- @f :: forall a. a -> Type@. In @f Type Bool@, the first argument (@Type@) is
1639 -- 'Specified' and the second argument (@Bool@) is 'Required'. It is precisely
1640 -- this sort of higher-rank situation in which 'appTyArgFlags' comes in handy,
1641 -- since @f Type Bool@ would be represented in Core using 'AppTy's.
1642 -- (See also Trac #15792).
1643 appTyArgFlags :: Type -> [Type] -> [ArgFlag]
1644 appTyArgFlags ty = fun_kind_arg_flags (typeKind ty)
1645
1646 -- | Given a function kind and a list of argument types (where each argument's
1647 -- kind aligns with the corresponding position in the argument kind), determine
1648 -- each argument's visibility ('Inferred', 'Specified', or 'Required').
1649 fun_kind_arg_flags :: Kind -> [Type] -> [ArgFlag]
1650 fun_kind_arg_flags = go emptyTCvSubst
1651 where
1652 go subst ki arg_tys
1653 | Just ki' <- coreView ki = go subst ki' arg_tys
1654 go _ _ [] = []
1655 go subst (ForAllTy (Bndr tv argf) res_ki) (arg_ty:arg_tys)
1656 = argf : go subst' res_ki arg_tys
1657 where
1658 subst' = extendTvSubst subst tv arg_ty
1659 go subst (TyVarTy tv) arg_tys
1660 | Just ki <- lookupTyVar subst tv = go subst ki arg_tys
1661 go _ _ arg_tys = map (const Required) arg_tys
1662 -- something is ill-kinded. But this can happen
1663 -- when printing errors. Assume everything is Required.
1664
1665 -- @isTauTy@ tests if a type has no foralls
1666 isTauTy :: Type -> Bool
1667 isTauTy ty | Just ty' <- coreView ty = isTauTy ty'
1668 isTauTy (TyVarTy _) = True
1669 isTauTy (LitTy {}) = True
1670 isTauTy (TyConApp tc tys) = all isTauTy tys && isTauTyCon tc
1671 isTauTy (AppTy a b) = isTauTy a && isTauTy b
1672 isTauTy (FunTy a b) = isTauTy a && isTauTy b
1673 isTauTy (ForAllTy {}) = False
1674 isTauTy (CastTy ty _) = isTauTy ty
1675 isTauTy (CoercionTy _) = False -- Not sure about this
1676
1677 {-
1678 %************************************************************************
1679 %* *
1680 TyCoBinders
1681 %* *
1682 %************************************************************************
1683 -}
1684
1685 -- | Make an anonymous binder
1686 mkAnonBinder :: Type -> TyCoBinder
1687 mkAnonBinder = Anon
1688
1689 -- | Does this binder bind a variable that is /not/ erased? Returns
1690 -- 'True' for anonymous binders.
1691 isAnonTyCoBinder :: TyCoBinder -> Bool
1692 isAnonTyCoBinder (Named {}) = False
1693 isAnonTyCoBinder (Anon {}) = True
1694
1695 isNamedTyCoBinder :: TyCoBinder -> Bool
1696 isNamedTyCoBinder (Named {}) = True
1697 isNamedTyCoBinder (Anon {}) = False
1698
1699 tyCoBinderVar_maybe :: TyCoBinder -> Maybe TyCoVar
1700 tyCoBinderVar_maybe (Named tv) = Just $ binderVar tv
1701 tyCoBinderVar_maybe _ = Nothing
1702
1703 tyCoBinderType :: TyCoBinder -> Type
1704 -- Barely used
1705 tyCoBinderType (Named tvb) = binderType tvb
1706 tyCoBinderType (Anon ty) = ty
1707
1708 tyBinderType :: TyBinder -> Type
1709 tyBinderType (Named (Bndr tv _))
1710 = ASSERT( isTyVar tv )
1711 tyVarKind tv
1712 tyBinderType (Anon ty) = ty
1713
1714 -- | Extract a relevant type, if there is one.
1715 binderRelevantType_maybe :: TyCoBinder -> Maybe Type
1716 binderRelevantType_maybe (Named {}) = Nothing
1717 binderRelevantType_maybe (Anon ty) = Just ty
1718
1719 -- | Like 'maybe', but for binders.
1720 caseBinder :: TyCoBinder -- ^ binder to scrutinize
1721 -> (TyCoVarBinder -> a) -- ^ named case
1722 -> (Type -> a) -- ^ anonymous case
1723 -> a
1724 caseBinder (Named v) f _ = f v
1725 caseBinder (Anon t) _ d = d t
1726
1727
1728 {-
1729 %************************************************************************
1730 %* *
1731 Pred
1732 * *
1733 ************************************************************************
1734
1735 Predicates on PredType
1736
1737 Note [Types for coercions, predicates, and evidence]
1738 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1739 We treat differently:
1740
1741 (a) Predicate types
1742 Test: isPredTy
1743 Binders: DictIds
1744 Kind: Constraint
1745 Examples: (Eq a), and (a ~ b)
1746
1747 (b) Coercion types are primitive, unboxed equalities
1748 Test: isCoVarTy
1749 Binders: CoVars (can appear in coercions)
1750 Kind: TYPE (TupleRep [])
1751 Examples: (t1 ~# t2) or (t1 ~R# t2)
1752
1753 (c) Evidence types is the type of evidence manipulated by
1754 the type constraint solver.
1755 Test: isEvVarType
1756 Binders: EvVars
1757 Kind: Constraint or TYPE (TupleRep [])
1758 Examples: all coercion types and predicate types
1759
1760 Coercion types and predicate types are mutually exclusive,
1761 but evidence types are a superset of both.
1762
1763 When treated as a user type, predicates are invisible and are
1764 implicitly instantiated; but coercion types, and non-pred evidence
1765 types, are just regular old types.
1766
1767 Note [isPredTy complications]
1768 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1769 You would think that we could define
1770 isPredTy ty = isConstraintKind (typeKind ty)
1771 But there are a number of complications:
1772
1773 * isPredTy is used when printing types, which can happen in debug
1774 printing during type checking of not-fully-zonked types. So it's
1775 not cool to say isConstraintKind (typeKind ty) because, absent
1776 zonking, the type might be ill-kinded, and typeKind crashes. Hence the
1777 rather tiresome story here
1778
1779 * isPredTy must return "True" to *unlifted* coercions, such as (t1 ~# t2)
1780 and (t1 ~R# t2), which are not of kind Constraint! Currently they are
1781 of kind #.
1782
1783 * If we do form the type '(C a => C [a]) => blah', then we'd like to
1784 print it as such. But that means that isPredTy must return True for
1785 (C a => C [a]). Admittedly that type is illegal in Haskell, but we
1786 want to print it nicely in error messages.
1787
1788 Note [Evidence for quantified constraints]
1789 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1790 The superclass mechanism in TcCanonical.makeSuperClasses risks
1791 taking a quantified constraint like
1792 (forall a. C a => a ~ b)
1793 and generate superclass evidence
1794 (forall a. C a => a ~# b)
1795
1796 This is a funny thing: neither isPredTy nor isCoVarType are true
1797 of it. So we are careful not to generate it in the first place:
1798 see Note [Equality superclasses in quantified constraints]
1799 in TcCanonical.
1800 -}
1801
1802 -- | Split a type constructor application into its type constructor and
1803 -- applied types. Note that this may fail in the case of a 'FunTy' with an
1804 -- argument of unknown kind 'FunTy' (e.g. @FunTy (a :: k) Int@. since the kind
1805 -- of @a@ isn't of the form @TYPE rep@). Consequently, you may need to zonk your
1806 -- type before using this function.
1807 --
1808 -- If you only need the 'TyCon', consider using 'tcTyConAppTyCon_maybe'.
1809 tcSplitTyConApp_maybe :: HasCallStack => Type -> Maybe (TyCon, [Type])
1810 -- Defined here to avoid module loops between Unify and TcType.
1811 tcSplitTyConApp_maybe ty | Just ty' <- tcView ty = tcSplitTyConApp_maybe ty'
1812 tcSplitTyConApp_maybe ty = tcRepSplitTyConApp_maybe ty
1813
1814 -- tcIsConstraintKind stuf only makes sense in the typechecker
1815 -- After that Constraint = Type
1816 -- See Note [coreView vs tcView]
1817 -- Defined here because it is used in isPredTy and tcRepSplitAppTy_maybe (sigh)
1818 tcIsConstraintKind :: Kind -> Bool
1819 tcIsConstraintKind ty
1820 | Just (tc, args) <- tcSplitTyConApp_maybe ty -- Note: tcSplit here
1821 , isConstraintKindCon tc
1822 = ASSERT2( null args, ppr ty ) True
1823
1824 | otherwise
1825 = False
1826
1827 -- | Is this kind equivalent to @*@?
1828 --
1829 -- This considers 'Constraint' to be distinct from @*@. For a version that
1830 -- treats them as the same type, see 'isLiftedTypeKind'.
1831 tcIsLiftedTypeKind :: Kind -> Bool
1832 tcIsLiftedTypeKind ty
1833 | Just (type_tc, [arg]) <- tcSplitTyConApp_maybe ty
1834 , type_tc `hasKey` tYPETyConKey
1835 , Just (lifted_rep_tc, args) <- tcSplitTyConApp_maybe arg
1836 , lifted_rep_tc `hasKey` liftedRepDataConKey
1837 = ASSERT2( null args, ppr ty ) True
1838 | otherwise
1839 = False
1840
1841 tcReturnsConstraintKind :: Kind -> Bool
1842 -- True <=> the Kind ultimately returns a Constraint
1843 -- E.g. * -> Constraint
1844 -- forall k. k -> Constraint
1845 tcReturnsConstraintKind kind
1846 | Just kind' <- tcView kind = tcReturnsConstraintKind kind'
1847 tcReturnsConstraintKind (ForAllTy _ ty) = tcReturnsConstraintKind ty
1848 tcReturnsConstraintKind (FunTy _ ty) = tcReturnsConstraintKind ty
1849 tcReturnsConstraintKind (TyConApp tc _) = isConstraintKindCon tc
1850 tcReturnsConstraintKind _ = False
1851
1852 isEvVarType :: Type -> Bool
1853 -- True of (a) predicates, of kind Constraint, such as (Eq a), and (a ~ b)
1854 -- (b) coercion types, such as (t1 ~# t2) or (t1 ~R# t2)
1855 -- See Note [Types for coercions, predicates, and evidence]
1856 -- See Note [Evidence for quantified constraints]
1857 isEvVarType ty = isCoVarType ty || isPredTy ty
1858
1859 -- | Does this type classify a core (unlifted) Coercion?
1860 -- At either role nominal or representational
1861 -- (t1 ~# t2) or (t1 ~R# t2)
1862 -- See Note [Types for coercions, predicates, and evidence]
1863 isCoVarType :: Type -> Bool
1864 isCoVarType ty
1865 | Just (tc,tys) <- splitTyConApp_maybe ty
1866 , (tc `hasKey` eqPrimTyConKey) || (tc `hasKey` eqReprPrimTyConKey)
1867 , tys `lengthIs` 4
1868 = True
1869 isCoVarType _ = False
1870
1871 -- | Is the type suitable to classify a given/wanted in the typechecker?
1872 isPredTy :: Type -> Bool
1873 -- See Note [isPredTy complications]
1874 -- NB: /not/ true of (t1 ~# t2) or (t1 ~R# t2)
1875 -- See Note [Types for coercions, predicates, and evidence]
1876 isPredTy ty = go ty []
1877 where
1878 go :: Type -> [KindOrType] -> Bool
1879 -- Since we are looking at the kind,
1880 -- no need to look through type synonyms
1881 go (AppTy ty1 ty2) args = go ty1 (ty2 : args)
1882 go (TyVarTy tv) args = go_k (tyVarKind tv) args
1883 go (TyConApp tc tys) args = ASSERT( null args ) -- TyConApp invariant
1884 go_k (tyConKind tc) tys
1885 go (FunTy arg res) []
1886 | isPredTy arg = isPredTy res -- (Eq a => C a)
1887 | otherwise = False -- (Int -> Bool)
1888 go (ForAllTy _ ty) [] = go ty []
1889 go (CastTy _ co) args = go_k (pSnd (coercionKind co)) args
1890 go _ _ = False
1891
1892 go_k :: Kind -> [KindOrType] -> Bool
1893 -- True <=> ('k' applied to 'kts') = Constraint
1894 go_k k [] = tcIsConstraintKind k
1895 go_k k (arg:args) = case piResultTy_maybe k arg of
1896 Just k' -> go_k k' args
1897 Nothing -> WARN( True, text "isPredTy" <+> ppr ty )
1898 False
1899 -- This last case shouldn't happen under most circumstances. It can
1900 -- occur if we call isPredTy during kind checking, especially if one
1901 -- of the following happens:
1902 --
1903 -- 1. There is actually a kind error. Example in which this showed up:
1904 -- polykinds/T11399
1905 --
1906 -- 2. A type constructor application appears to be oversaturated. An
1907 -- example of this occurred in GHC Trac #13187:
1908 --
1909 -- {-# LANGUAGE PolyKinds #-}
1910 -- type Const a b = b
1911 -- f :: Const Int (,) Bool Char -> Char
1912 --
1913 -- We call isPredTy (Const k1 k2 Int (,) Bool Char
1914 -- where k1,k2 are unification variables that have been
1915 -- unified to *, and (*->*->*) resp, /but not zonked/.
1916 -- This shows that isPredTy can report a false negative
1917 -- if a constraint is similarly oversaturated, but
1918 -- it's hard to do better than isPredTy currently does without
1919 -- zonking, so we punt on such cases for now. This only happens
1920 -- during debug-printing, so it doesn't matter.
1921
1922 isClassPred, isEqPred, isNomEqPred, isIPPred :: PredType -> Bool
1923 isClassPred ty = case tyConAppTyCon_maybe ty of
1924 Just tyCon | isClassTyCon tyCon -> True
1925 _ -> False
1926 isEqPred ty = case tyConAppTyCon_maybe ty of
1927 Just tyCon -> tyCon `hasKey` eqPrimTyConKey
1928 || tyCon `hasKey` eqReprPrimTyConKey
1929 _ -> False
1930
1931 isNomEqPred ty = case tyConAppTyCon_maybe ty of
1932 Just tyCon -> tyCon `hasKey` eqPrimTyConKey
1933 _ -> False
1934
1935 isIPPred ty = case tyConAppTyCon_maybe ty of
1936 Just tc -> isIPTyCon tc
1937 _ -> False
1938
1939 isIPTyCon :: TyCon -> Bool
1940 isIPTyCon tc = tc `hasKey` ipClassKey
1941 -- Class and its corresponding TyCon have the same Unique
1942
1943 isIPClass :: Class -> Bool
1944 isIPClass cls = cls `hasKey` ipClassKey
1945
1946 isCTupleClass :: Class -> Bool
1947 isCTupleClass cls = isTupleTyCon (classTyCon cls)
1948
1949 isIPPred_maybe :: Type -> Maybe (FastString, Type)
1950 isIPPred_maybe ty =
1951 do (tc,[t1,t2]) <- splitTyConApp_maybe ty
1952 guard (isIPTyCon tc)
1953 x <- isStrLitTy t1
1954 return (x,t2)
1955
1956 {-
1957 Make PredTypes
1958
1959 --------------------- Equality types ---------------------------------
1960 -}
1961
1962 -- | Makes a lifted equality predicate at the given role
1963 mkPrimEqPredRole :: Role -> Type -> Type -> PredType
1964 mkPrimEqPredRole Nominal = mkPrimEqPred
1965 mkPrimEqPredRole Representational = mkReprPrimEqPred
1966 mkPrimEqPredRole Phantom = panic "mkPrimEqPredRole phantom"
1967
1968 -- | Creates a primitive type equality predicate.
1969 -- Invariant: the types are not Coercions
1970 mkPrimEqPred :: Type -> Type -> Type
1971 mkPrimEqPred ty1 ty2
1972 = TyConApp eqPrimTyCon [k1, k2, ty1, ty2]
1973 where
1974 k1 = typeKind ty1
1975 k2 = typeKind ty2
1976
1977 -- | Creates a primite type equality predicate with explicit kinds
1978 mkHeteroPrimEqPred :: Kind -> Kind -> Type -> Type -> Type
1979 mkHeteroPrimEqPred k1 k2 ty1 ty2 = TyConApp eqPrimTyCon [k1, k2, ty1, ty2]
1980
1981 -- | Creates a primitive representational type equality predicate
1982 -- with explicit kinds
1983 mkHeteroReprPrimEqPred :: Kind -> Kind -> Type -> Type -> Type
1984 mkHeteroReprPrimEqPred k1 k2 ty1 ty2
1985 = TyConApp eqReprPrimTyCon [k1, k2, ty1, ty2]
1986
1987 -- | Try to split up a coercion type into the types that it coerces
1988 splitCoercionType_maybe :: Type -> Maybe (Type, Type)
1989 splitCoercionType_maybe ty
1990 = do { (tc, [_, _, ty1, ty2]) <- splitTyConApp_maybe ty
1991 ; guard $ tc `hasKey` eqPrimTyConKey || tc `hasKey` eqReprPrimTyConKey
1992 ; return (ty1, ty2) }
1993
1994 mkReprPrimEqPred :: Type -> Type -> Type
1995 mkReprPrimEqPred ty1 ty2
1996 = TyConApp eqReprPrimTyCon [k1, k2, ty1, ty2]
1997 where
1998 k1 = typeKind ty1
1999 k2 = typeKind ty2
2000
2001 equalityTyCon :: Role -> TyCon
2002 equalityTyCon Nominal = eqPrimTyCon
2003 equalityTyCon Representational = eqReprPrimTyCon
2004 equalityTyCon Phantom = eqPhantPrimTyCon
2005
2006 -- --------------------- Dictionary types ---------------------------------
2007
2008 mkClassPred :: Class -> [Type] -> PredType
2009 mkClassPred clas tys = TyConApp (classTyCon clas) tys
2010
2011 isDictTy :: Type -> Bool
2012 isDictTy = isClassPred
2013
2014 isDictLikeTy :: Type -> Bool
2015 -- Note [Dictionary-like types]
2016 isDictLikeTy ty | Just ty' <- coreView ty = isDictLikeTy ty'
2017 isDictLikeTy ty = case splitTyConApp_maybe ty of
2018 Just (tc, tys) | isClassTyCon tc -> True
2019 | isTupleTyCon tc -> all isDictLikeTy tys
2020 _other -> False
2021
2022 {-
2023 Note [Dictionary-like types]
2024 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2025 Being "dictionary-like" means either a dictionary type or a tuple thereof.
2026 In GHC 6.10 we build implication constraints which construct such tuples,
2027 and if we land up with a binding
2028 t :: (C [a], Eq [a])
2029 t = blah
2030 then we want to treat t as cheap under "-fdicts-cheap" for example.
2031 (Implication constraints are normally inlined, but sadly not if the
2032 occurrence is itself inside an INLINE function! Until we revise the
2033 handling of implication constraints, that is.) This turned out to
2034 be important in getting good arities in DPH code. Example:
2035
2036 class C a
2037 class D a where { foo :: a -> a }
2038 instance C a => D (Maybe a) where { foo x = x }
2039
2040 bar :: (C a, C b) => a -> b -> (Maybe a, Maybe b)
2041 {-# INLINE bar #-}
2042 bar x y = (foo (Just x), foo (Just y))
2043
2044 Then 'bar' should jolly well have arity 4 (two dicts, two args), but
2045 we ended up with something like
2046 bar = __inline_me__ (\d1,d2. let t :: (D (Maybe a), D (Maybe b)) = ...
2047 in \x,y. <blah>)
2048
2049 This is all a bit ad-hoc; eg it relies on knowing that implication
2050 constraints build tuples.
2051
2052
2053 Decomposing PredType
2054 -}
2055
2056 -- | A choice of equality relation. This is separate from the type 'Role'
2057 -- because 'Phantom' does not define a (non-trivial) equality relation.
2058 data EqRel = NomEq | ReprEq
2059 deriving (Eq, Ord)
2060
2061 instance Outputable EqRel where
2062 ppr NomEq = text "nominal equality"
2063 ppr ReprEq = text "representational equality"
2064
2065 eqRelRole :: EqRel -> Role
2066 eqRelRole NomEq = Nominal
2067 eqRelRole ReprEq = Representational
2068
2069 data PredTree
2070 = ClassPred Class [Type]
2071 | EqPred EqRel Type Type
2072 | IrredPred PredType
2073 | ForAllPred [TyCoVarBinder] [PredType] PredType
2074 -- ForAllPred: see Note [Quantified constraints] in TcCanonical
2075 -- NB: There is no TuplePred case
2076 -- Tuple predicates like (Eq a, Ord b) are just treated
2077 -- as ClassPred, as if we had a tuple class with two superclasses
2078 -- class (c1, c2) => (%,%) c1 c2
2079
2080 classifyPredType :: PredType -> PredTree
2081 classifyPredType ev_ty = case splitTyConApp_maybe ev_ty of
2082 Just (tc, [_, _, ty1, ty2])
2083 | tc `hasKey` eqReprPrimTyConKey -> EqPred ReprEq ty1 ty2
2084 | tc `hasKey` eqPrimTyConKey -> EqPred NomEq ty1 ty2
2085
2086 Just (tc, tys)
2087 | Just clas <- tyConClass_maybe tc
2088 -> ClassPred clas tys
2089
2090 _ | (tvs, rho) <- splitForAllVarBndrs ev_ty
2091 , (theta, pred) <- splitFunTys rho
2092 , not (null tvs && null theta)
2093 -> ForAllPred tvs theta pred
2094
2095 | otherwise
2096 -> IrredPred ev_ty
2097
2098 getClassPredTys :: HasDebugCallStack => PredType -> (Class, [Type])
2099 getClassPredTys ty = case getClassPredTys_maybe ty of
2100 Just (clas, tys) -> (clas, tys)
2101 Nothing -> pprPanic "getClassPredTys" (ppr ty)
2102
2103 getClassPredTys_maybe :: PredType -> Maybe (Class, [Type])
2104 getClassPredTys_maybe ty = case splitTyConApp_maybe ty of
2105 Just (tc, tys) | Just clas <- tyConClass_maybe tc -> Just (clas, tys)
2106 _ -> Nothing
2107
2108 getEqPredTys :: PredType -> (Type, Type)
2109 getEqPredTys ty
2110 = case splitTyConApp_maybe ty of
2111 Just (tc, [_, _, ty1, ty2])
2112 | tc `hasKey` eqPrimTyConKey
2113 || tc `hasKey` eqReprPrimTyConKey
2114 -> (ty1, ty2)
2115 _ -> pprPanic "getEqPredTys" (ppr ty)
2116
2117 getEqPredTys_maybe :: PredType -> Maybe (Role, Type, Type)
2118 getEqPredTys_maybe ty
2119 = case splitTyConApp_maybe ty of
2120 Just (tc, [_, _, ty1, ty2])
2121 | tc `hasKey` eqPrimTyConKey -> Just (Nominal, ty1, ty2)
2122 | tc `hasKey` eqReprPrimTyConKey -> Just (Representational, ty1, ty2)
2123 _ -> Nothing
2124
2125 getEqPredRole :: PredType -> Role
2126 getEqPredRole ty = eqRelRole (predTypeEqRel ty)
2127
2128 -- | Get the equality relation relevant for a pred type.
2129 predTypeEqRel :: PredType -> EqRel
2130 predTypeEqRel ty
2131 | Just (tc, _) <- splitTyConApp_maybe ty
2132 , tc `hasKey` eqReprPrimTyConKey
2133 = ReprEq
2134 | otherwise
2135 = NomEq
2136
2137 {-
2138 %************************************************************************
2139 %* *
2140 Well-scoped tyvars
2141 * *
2142 ************************************************************************
2143
2144 Note [ScopedSort]
2145 ~~~~~~~~~~~~~~~~~
2146 Consider
2147
2148 foo :: Proxy a -> Proxy (b :: k) -> Proxy (a :: k2) -> ()
2149
2150 This function type is implicitly generalised over [a, b, k, k2]. These
2151 variables will be Specified; that is, they will be available for visible
2152 type application. This is because they are written in the type signature
2153 by the user.
2154
2155 However, we must ask: what order will they appear in? In cases without
2156 dependency, this is easy: we just use the lexical left-to-right ordering
2157 of first occurrence. With dependency, we cannot get off the hook so
2158 easily.
2159
2160 We thus state:
2161
2162 * These variables appear in the order as given by ScopedSort, where
2163 the input to ScopedSort is the left-to-right order of first occurrence.
2164
2165 Note that this applies only to *implicit* quantification, without a
2166 `forall`. If the user writes a `forall`, then we just use the order given.
2167
2168 ScopedSort is defined thusly (as proposed in #15743):
2169 * Work left-to-right through the input list, with a cursor.
2170 * If variable v at the cursor is depended on by any earlier variable w,
2171 move v immediately before the leftmost such w.
2172
2173 INVARIANT: The prefix of variables before the cursor form a valid telescope.
2174
2175 Note that ScopedSort makes sense only after type inference is done and all
2176 types/kinds are fully settled and zonked.
2177
2178 -}
2179
2180 -- | Do a topological sort on a list of tyvars,
2181 -- so that binders occur before occurrences
2182 -- E.g. given [ a::k, k::*, b::k ]
2183 -- it'll return a well-scoped list [ k::*, a::k, b::k ]
2184 --
2185 -- This is a deterministic sorting operation
2186 -- (that is, doesn't depend on Uniques).
2187 --
2188 -- It is also meant to be stable: that is, variables should not
2189 -- be reordered unnecessarily. This is specified in Note [ScopedSort]
2190 -- See also Note [Ordering of implicit variables] in RnTypes
2191
2192 scopedSort :: [TyCoVar] -> [TyCoVar]
2193 scopedSort = go [] []
2194 where
2195 go :: [TyCoVar] -- already sorted, in reverse order
2196 -> [TyCoVarSet] -- each set contains all the variables which must be placed
2197 -- before the tv corresponding to the set; they are accumulations
2198 -- of the fvs in the sorted tvs' kinds
2199
2200 -- This list is in 1-to-1 correspondence with the sorted tyvars
2201 -- INVARIANT:
2202 -- all (\tl -> all (`subVarSet` head tl) (tail tl)) (tails fv_list)
2203 -- That is, each set in the list is a superset of all later sets.
2204
2205 -> [TyCoVar] -- yet to be sorted
2206 -> [TyCoVar]
2207 go acc _fv_list [] = reverse acc
2208 go acc fv_list (tv:tvs)
2209 = go acc' fv_list' tvs
2210 where
2211 (acc', fv_list') = insert tv acc fv_list
2212
2213 insert :: TyCoVar -- var to insert
2214 -> [TyCoVar] -- sorted list, in reverse order
2215 -> [TyCoVarSet] -- list of fvs, as above
2216 -> ([TyCoVar], [TyCoVarSet]) -- augmented lists
2217 insert tv [] [] = ([tv], [tyCoVarsOfType (tyVarKind tv)])
2218 insert tv (a:as) (fvs:fvss)
2219 | tv `elemVarSet` fvs
2220 , (as', fvss') <- insert tv as fvss
2221 = (a:as', fvs `unionVarSet` fv_tv : fvss')
2222
2223 | otherwise
2224 = (tv:a:as, fvs `unionVarSet` fv_tv : fvs : fvss)
2225 where
2226 fv_tv = tyCoVarsOfType (tyVarKind tv)
2227
2228 -- lists not in correspondence
2229 insert _ _ _ = panic "scopedSort"
2230
2231 -- | Extract a well-scoped list of variables from a deterministic set of
2232 -- variables. The result is deterministic.
2233 -- NB: There used to exist varSetElemsWellScoped :: VarSet -> [Var] which
2234 -- took a non-deterministic set and produced a non-deterministic
2235 -- well-scoped list. If you care about the list being well-scoped you also
2236 -- most likely care about it being in deterministic order.
2237 dVarSetElemsWellScoped :: DVarSet -> [Var]
2238 dVarSetElemsWellScoped = scopedSort . dVarSetElems
2239
2240 -- | Get the free vars of a type in scoped order
2241 tyCoVarsOfTypeWellScoped :: Type -> [TyVar]
2242 tyCoVarsOfTypeWellScoped = scopedSort . tyCoVarsOfTypeList
2243
2244 -- | Get the free vars of types in scoped order
2245 tyCoVarsOfTypesWellScoped :: [Type] -> [TyVar]
2246 tyCoVarsOfTypesWellScoped = scopedSort . tyCoVarsOfTypesList
2247
2248 -- | Given the suffix of a telescope, returns the prefix.
2249 -- Ex: given [(k :: j), (a :: Proxy k)], returns [(j :: *)].
2250 tyCoVarsOfBindersWellScoped :: [TyVar] -> [TyVar]
2251 tyCoVarsOfBindersWellScoped tvs
2252 = tyCoVarsOfTypeWellScoped (mkInvForAllTys tvs unitTy)
2253
2254 ------------- Closing over kinds -----------------
2255
2256 -- | Add the kind variables free in the kinds of the tyvars in the given set.
2257 -- Returns a non-deterministic set.
2258 closeOverKinds :: TyVarSet -> TyVarSet
2259 closeOverKinds = fvVarSet . closeOverKindsFV . nonDetEltsUniqSet
2260 -- It's OK to use nonDetEltsUniqSet here because we immediately forget
2261 -- about the ordering by returning a set.
2262
2263 -- | Given a list of tyvars returns a deterministic FV computation that
2264 -- returns the given tyvars with the kind variables free in the kinds of the
2265 -- given tyvars.
2266 closeOverKindsFV :: [TyVar] -> FV
2267 closeOverKindsFV tvs =
2268 mapUnionFV (tyCoFVsOfType . tyVarKind) tvs `unionFV` mkFVs tvs
2269
2270 -- | Add the kind variables free in the kinds of the tyvars in the given set.
2271 -- Returns a deterministically ordered list.
2272 closeOverKindsList :: [TyVar] -> [TyVar]
2273 closeOverKindsList tvs = fvVarList $ closeOverKindsFV tvs
2274
2275 -- | Add the kind variables free in the kinds of the tyvars in the given set.
2276 -- Returns a deterministic set.
2277 closeOverKindsDSet :: DTyVarSet -> DTyVarSet
2278 closeOverKindsDSet = fvDVarSet . closeOverKindsFV . dVarSetElems
2279
2280 {-
2281 ************************************************************************
2282 * *
2283 \subsection{Type families}
2284 * *
2285 ************************************************************************
2286 -}
2287
2288 mkFamilyTyConApp :: TyCon -> [Type] -> Type
2289 -- ^ Given a family instance TyCon and its arg types, return the
2290 -- corresponding family type. E.g:
2291 --
2292 -- > data family T a
2293 -- > data instance T (Maybe b) = MkT b
2294 --
2295 -- Where the instance tycon is :RTL, so:
2296 --
2297 -- > mkFamilyTyConApp :RTL Int = T (Maybe Int)
2298 mkFamilyTyConApp tc tys
2299 | Just (fam_tc, fam_tys) <- tyConFamInst_maybe tc
2300 , let tvs = tyConTyVars tc
2301 fam_subst = ASSERT2( tvs `equalLength` tys, ppr tc <+> ppr tys )
2302 zipTvSubst tvs tys
2303 = mkTyConApp fam_tc (substTys fam_subst fam_tys)
2304 | otherwise
2305 = mkTyConApp tc tys
2306
2307 -- | Get the type on the LHS of a coercion induced by a type/data
2308 -- family instance.
2309 coAxNthLHS :: CoAxiom br -> Int -> Type
2310 coAxNthLHS ax ind =
2311 mkTyConApp (coAxiomTyCon ax) (coAxBranchLHS (coAxiomNthBranch ax ind))
2312
2313 -- | Pretty prints a 'TyCon', using the family instance in case of a
2314 -- representation tycon. For example:
2315 --
2316 -- > data T [a] = ...
2317 --
2318 -- In that case we want to print @T [a]@, where @T@ is the family 'TyCon'
2319 pprSourceTyCon :: TyCon -> SDoc
2320 pprSourceTyCon tycon
2321 | Just (fam_tc, tys) <- tyConFamInst_maybe tycon
2322 = ppr $ fam_tc `TyConApp` tys -- can't be FunTyCon
2323 | otherwise
2324 = ppr tycon
2325
2326 isFamFreeTy :: Type -> Bool
2327 isFamFreeTy ty | Just ty' <- coreView ty = isFamFreeTy ty'
2328 isFamFreeTy (TyVarTy _) = True
2329 isFamFreeTy (LitTy {}) = True
2330 isFamFreeTy (TyConApp tc tys) = all isFamFreeTy tys && isFamFreeTyCon tc
2331 isFamFreeTy (AppTy a b) = isFamFreeTy a && isFamFreeTy b
2332 isFamFreeTy (FunTy a b) = isFamFreeTy a && isFamFreeTy b
2333 isFamFreeTy (ForAllTy _ ty) = isFamFreeTy ty
2334 isFamFreeTy (CastTy ty _) = isFamFreeTy ty
2335 isFamFreeTy (CoercionTy _) = False -- Not sure about this
2336
2337 {-
2338 ************************************************************************
2339 * *
2340 \subsection{Liftedness}
2341 * *
2342 ************************************************************************
2343 -}
2344
2345 -- | Returns Just True if this type is surely lifted, Just False
2346 -- if it is surely unlifted, Nothing if we can't be sure (i.e., it is
2347 -- levity polymorphic), and panics if the kind does not have the shape
2348 -- TYPE r.
2349 isLiftedType_maybe :: HasDebugCallStack => Type -> Maybe Bool
2350 isLiftedType_maybe ty = go (getRuntimeRep ty)
2351 where
2352 go rr | Just rr' <- coreView rr = go rr'
2353 go (TyConApp lifted_rep [])
2354 | lifted_rep `hasKey` liftedRepDataConKey = Just True
2355 go (TyConApp {}) = Just False -- everything else is unlifted
2356 go _ = Nothing -- levity polymorphic
2357
2358 -- | See "Type#type_classification" for what an unlifted type is.
2359 -- Panics on levity polymorphic types.
2360 isUnliftedType :: HasDebugCallStack => Type -> Bool
2361 -- isUnliftedType returns True for forall'd unlifted types:
2362 -- x :: forall a. Int#
2363 -- I found bindings like these were getting floated to the top level.
2364 -- They are pretty bogus types, mind you. It would be better never to
2365 -- construct them
2366 isUnliftedType ty
2367 = not (isLiftedType_maybe ty `orElse`
2368 pprPanic "isUnliftedType" (ppr ty <+> dcolon <+> ppr (typeKind ty)))
2369
2370 -- | Is this a type of kind RuntimeRep? (e.g. LiftedRep)
2371 isRuntimeRepKindedTy :: Type -> Bool
2372 isRuntimeRepKindedTy = isRuntimeRepTy . typeKind
2373
2374 -- | Drops prefix of RuntimeRep constructors in 'TyConApp's. Useful for e.g.
2375 -- dropping 'LiftedRep arguments of unboxed tuple TyCon applications:
2376 --
2377 -- dropRuntimeRepArgs [ 'LiftedRep, 'IntRep
2378 -- , String, Int# ] == [String, Int#]
2379 --
2380 dropRuntimeRepArgs :: [Type] -> [Type]
2381 dropRuntimeRepArgs = dropWhile isRuntimeRepKindedTy
2382
2383 -- | Extract the RuntimeRep classifier of a type. For instance,
2384 -- @getRuntimeRep_maybe Int = LiftedRep@. Returns 'Nothing' if this is not
2385 -- possible.
2386 getRuntimeRep_maybe :: HasDebugCallStack
2387 => Type -> Maybe Type
2388 getRuntimeRep_maybe = getRuntimeRepFromKind_maybe . typeKind
2389
2390 -- | Extract the RuntimeRep classifier of a type. For instance,
2391 -- @getRuntimeRep_maybe Int = LiftedRep@. Panics if this is not possible.
2392 getRuntimeRep :: HasDebugCallStack => Type -> Type
2393 getRuntimeRep ty
2394 = case getRuntimeRep_maybe ty of
2395 Just r -> r
2396 Nothing -> pprPanic "getRuntimeRep" (ppr ty <+> dcolon <+> ppr (typeKind ty))
2397
2398 -- | Extract the RuntimeRep classifier of a type from its kind. For example,
2399 -- @getRuntimeRepFromKind * = LiftedRep@; Panics if this is not possible.
2400 getRuntimeRepFromKind :: HasDebugCallStack
2401 => Type -> Type
2402 getRuntimeRepFromKind k =
2403 case getRuntimeRepFromKind_maybe k of
2404 Just r -> r
2405 Nothing -> pprPanic "getRuntimeRepFromKind"
2406 (ppr k <+> dcolon <+> ppr (typeKind k))
2407
2408 -- | Extract the RuntimeRep classifier of a type from its kind. For example,
2409 -- @getRuntimeRepFromKind * = LiftedRep@; Returns 'Nothing' if this is not
2410 -- possible.
2411 getRuntimeRepFromKind_maybe :: HasDebugCallStack
2412 => Type -> Maybe Type
2413 getRuntimeRepFromKind_maybe = go
2414 where
2415 go k | Just k' <- coreView k = go k'
2416 go k
2417 | Just (_tc, [arg]) <- splitTyConApp_maybe k
2418 = ASSERT2( _tc `hasKey` tYPETyConKey, ppr k )
2419 Just arg
2420 go _ = Nothing
2421
2422 isUnboxedTupleType :: Type -> Bool
2423 isUnboxedTupleType ty
2424 = tyConAppTyCon (getRuntimeRep ty) `hasKey` tupleRepDataConKey
2425 -- NB: Do not use typePrimRep, as that can't tell the difference between
2426 -- unboxed tuples and unboxed sums
2427
2428
2429 isUnboxedSumType :: Type -> Bool
2430 isUnboxedSumType ty
2431 = tyConAppTyCon (getRuntimeRep ty) `hasKey` sumRepDataConKey
2432
2433 -- | See "Type#type_classification" for what an algebraic type is.
2434 -- Should only be applied to /types/, as opposed to e.g. partially
2435 -- saturated type constructors
2436 isAlgType :: Type -> Bool
2437 isAlgType ty
2438 = case splitTyConApp_maybe ty of
2439 Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
2440 isAlgTyCon tc
2441 _other -> False
2442
2443 -- | Check whether a type is a data family type
2444 isDataFamilyAppType :: Type -> Bool
2445 isDataFamilyAppType ty = case tyConAppTyCon_maybe ty of
2446 Just tc -> isDataFamilyTyCon tc
2447 _ -> False
2448
2449 -- | Computes whether an argument (or let right hand side) should
2450 -- be computed strictly or lazily, based only on its type.
2451 -- Currently, it's just 'isUnliftedType'. Panics on levity-polymorphic types.
2452 isStrictType :: HasDebugCallStack => Type -> Bool
2453 isStrictType = isUnliftedType
2454
2455 isPrimitiveType :: Type -> Bool
2456 -- ^ Returns true of types that are opaque to Haskell.
2457 isPrimitiveType ty = case splitTyConApp_maybe ty of
2458 Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
2459 isPrimTyCon tc
2460 _ -> False
2461
2462 {-
2463 ************************************************************************
2464 * *
2465 \subsection{Join points}
2466 * *
2467 ************************************************************************
2468 -}
2469
2470 -- | Determine whether a type could be the type of a join point of given total
2471 -- arity, according to the polymorphism rule. A join point cannot be polymorphic
2472 -- in its return type, since given
2473 -- join j @a @b x y z = e1 in e2,
2474 -- the types of e1 and e2 must be the same, and a and b are not in scope for e2.
2475 -- (See Note [The polymorphism rule of join points] in CoreSyn.) Returns False
2476 -- also if the type simply doesn't have enough arguments.
2477 --
2478 -- Note that we need to know how many arguments (type *and* value) the putative
2479 -- join point takes; for instance, if
2480 -- j :: forall a. a -> Int
2481 -- then j could be a binary join point returning an Int, but it could *not* be a
2482 -- unary join point returning a -> Int.
2483 --
2484 -- TODO: See Note [Excess polymorphism and join points]
2485 isValidJoinPointType :: JoinArity -> Type -> Bool
2486 isValidJoinPointType arity ty
2487 = valid_under emptyVarSet arity ty
2488 where
2489 valid_under tvs arity ty
2490 | arity == 0
2491 = isEmptyVarSet (tvs `intersectVarSet` tyCoVarsOfType ty)
2492 | Just (t, ty') <- splitForAllTy_maybe ty
2493 = valid_under (tvs `extendVarSet` t) (arity-1) ty'
2494 | Just (_, res_ty) <- splitFunTy_maybe ty
2495 = valid_under tvs (arity-1) res_ty
2496 | otherwise
2497 = False
2498
2499 {- Note [Excess polymorphism and join points]
2500 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2501 In principle, if a function would be a join point except that it fails
2502 the polymorphism rule (see Note [The polymorphism rule of join points] in
2503 CoreSyn), it can still be made a join point with some effort. This is because
2504 all tail calls must return the same type (they return to the same context!), and
2505 thus if the return type depends on an argument, that argument must always be the
2506 same.
2507
2508 For instance, consider:
2509
2510 let f :: forall a. a -> Char -> [a]
2511 f @a x c = ... f @a y 'a' ...
2512 in ... f @Int 1 'b' ... f @Int 2 'c' ...
2513
2514 (where the calls are tail calls). `f` fails the polymorphism rule because its
2515 return type is [a], where [a] is bound. But since the type argument is always
2516 'Int', we can rewrite it as:
2517
2518 let f' :: Int -> Char -> [Int]
2519 f' x c = ... f' y 'a' ...
2520 in ... f' 1 'b' ... f 2 'c' ...
2521
2522 and now we can make f' a join point:
2523
2524 join f' :: Int -> Char -> [Int]
2525 f' x c = ... jump f' y 'a' ...
2526 in ... jump f' 1 'b' ... jump f' 2 'c' ...
2527
2528 It's not clear that this comes up often, however. TODO: Measure how often and
2529 add this analysis if necessary. See Trac #14620.
2530
2531
2532 ************************************************************************
2533 * *
2534 \subsection{Sequencing on types}
2535 * *
2536 ************************************************************************
2537 -}
2538
2539 seqType :: Type -> ()
2540 seqType (LitTy n) = n `seq` ()
2541 seqType (TyVarTy tv) = tv `seq` ()
2542 seqType (AppTy t1 t2) = seqType t1 `seq` seqType t2
2543 seqType (FunTy t1 t2) = seqType t1 `seq` seqType t2
2544 seqType (TyConApp tc tys) = tc `seq` seqTypes tys
2545 seqType (ForAllTy (Bndr tv _) ty) = seqType (varType tv) `seq` seqType ty
2546 seqType (CastTy ty co) = seqType ty `seq` seqCo co
2547 seqType (CoercionTy co) = seqCo co
2548
2549 seqTypes :: [Type] -> ()
2550 seqTypes [] = ()
2551 seqTypes (ty:tys) = seqType ty `seq` seqTypes tys
2552
2553 {-
2554 ************************************************************************
2555 * *
2556 Comparison for types
2557 (We don't use instances so that we know where it happens)
2558 * *
2559 ************************************************************************
2560
2561 Note [Equality on AppTys]
2562 ~~~~~~~~~~~~~~~~~~~~~~~~~
2563 In our cast-ignoring equality, we want to say that the following two
2564 are equal:
2565
2566 (Maybe |> co) (Int |> co') ~? Maybe Int
2567
2568 But the left is an AppTy while the right is a TyConApp. The solution is
2569 to use repSplitAppTy_maybe to break up the TyConApp into its pieces and
2570 then continue. Easy to do, but also easy to forget to do.
2571
2572 -}
2573
2574 eqType :: Type -> Type -> Bool
2575 -- ^ Type equality on source types. Does not look through @newtypes@ or
2576 -- 'PredType's, but it does look through type synonyms.
2577 -- This first checks that the kinds of the types are equal and then
2578 -- checks whether the types are equal, ignoring casts and coercions.
2579 -- (The kind check is a recursive call, but since all kinds have type
2580 -- @Type@, there is no need to check the types of kinds.)
2581 -- See also Note [Non-trivial definitional equality] in TyCoRep.
2582 eqType t1 t2 = isEqual $ nonDetCmpType t1 t2
2583 -- It's OK to use nonDetCmpType here and eqType is deterministic,
2584 -- nonDetCmpType does equality deterministically
2585
2586 -- | Compare types with respect to a (presumably) non-empty 'RnEnv2'.
2587 eqTypeX :: RnEnv2 -> Type -> Type -> Bool
2588 eqTypeX env t1 t2 = isEqual $ nonDetCmpTypeX env t1 t2
2589 -- It's OK to use nonDetCmpType here and eqTypeX is deterministic,
2590 -- nonDetCmpTypeX does equality deterministically
2591
2592 -- | Type equality on lists of types, looking through type synonyms
2593 -- but not newtypes.
2594 eqTypes :: [Type] -> [Type] -> Bool
2595 eqTypes tys1 tys2 = isEqual $ nonDetCmpTypes tys1 tys2
2596 -- It's OK to use nonDetCmpType here and eqTypes is deterministic,
2597 -- nonDetCmpTypes does equality deterministically
2598
2599 eqVarBndrs :: RnEnv2 -> [Var] -> [Var] -> Maybe RnEnv2
2600 -- Check that the var lists are the same length
2601 -- and have matching kinds; if so, extend the RnEnv2
2602 -- Returns Nothing if they don't match
2603 eqVarBndrs env [] []
2604 = Just env
2605 eqVarBndrs env (tv1:tvs1) (tv2:tvs2)
2606 | eqTypeX env (varType tv1) (varType tv2)
2607 = eqVarBndrs (rnBndr2 env tv1 tv2) tvs1 tvs2
2608 eqVarBndrs _ _ _= Nothing
2609
2610 -- Now here comes the real worker
2611
2612 {-
2613 Note [nonDetCmpType nondeterminism]
2614 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2615 nonDetCmpType is implemented in terms of nonDetCmpTypeX. nonDetCmpTypeX
2616 uses nonDetCmpTc which compares TyCons by their Unique value. Using Uniques for
2617 ordering leads to nondeterminism. We hit the same problem in the TyVarTy case,
2618 comparing type variables is nondeterministic, note the call to nonDetCmpVar in
2619 nonDetCmpTypeX.
2620 See Note [Unique Determinism] for more details.
2621 -}
2622
2623 nonDetCmpType :: Type -> Type -> Ordering
2624 nonDetCmpType t1 t2
2625 -- we know k1 and k2 have the same kind, because they both have kind *.
2626 = nonDetCmpTypeX rn_env t1 t2
2627 where
2628 rn_env = mkRnEnv2 (mkInScopeSet (tyCoVarsOfTypes [t1, t2]))
2629
2630 nonDetCmpTypes :: [Type] -> [Type] -> Ordering
2631 nonDetCmpTypes ts1 ts2 = nonDetCmpTypesX rn_env ts1 ts2
2632 where
2633 rn_env = mkRnEnv2 (mkInScopeSet (tyCoVarsOfTypes (ts1 ++ ts2)))
2634
2635 -- | An ordering relation between two 'Type's (known below as @t1 :: k1@
2636 -- and @t2 :: k2@)
2637 data TypeOrdering = TLT -- ^ @t1 < t2@
2638 | TEQ -- ^ @t1 ~ t2@ and there are no casts in either,
2639 -- therefore we can conclude @k1 ~ k2@
2640 | TEQX -- ^ @t1 ~ t2@ yet one of the types contains a cast so
2641 -- they may differ in kind.
2642 | TGT -- ^ @t1 > t2@
2643 deriving (Eq, Ord, Enum, Bounded)
2644
2645 nonDetCmpTypeX :: RnEnv2 -> Type -> Type -> Ordering -- Main workhorse
2646 -- See Note [Non-trivial definitional equality] in TyCoRep
2647 nonDetCmpTypeX env orig_t1 orig_t2 =
2648 case go env orig_t1 orig_t2 of
2649 -- If there are casts then we also need to do a comparison of the kinds of
2650 -- the types being compared
2651 TEQX -> toOrdering $ go env k1 k2
2652 ty_ordering -> toOrdering ty_ordering
2653 where
2654 k1 = typeKind orig_t1
2655 k2 = typeKind orig_t2
2656
2657 toOrdering :: TypeOrdering -> Ordering
2658 toOrdering TLT = LT
2659 toOrdering TEQ = EQ
2660 toOrdering TEQX = EQ
2661 toOrdering TGT = GT
2662
2663 liftOrdering :: Ordering -> TypeOrdering
2664 liftOrdering LT = TLT
2665 liftOrdering EQ = TEQ
2666 liftOrdering GT = TGT
2667
2668 thenCmpTy :: TypeOrdering -> TypeOrdering -> TypeOrdering
2669 thenCmpTy TEQ rel = rel
2670 thenCmpTy TEQX rel = hasCast rel
2671 thenCmpTy rel _ = rel
2672
2673 hasCast :: TypeOrdering -> TypeOrdering
2674 hasCast TEQ = TEQX
2675 hasCast rel = rel
2676
2677 -- Returns both the resulting ordering relation between the two types
2678 -- and whether either contains a cast.
2679 go :: RnEnv2 -> Type -> Type -> TypeOrdering
2680 go env t1 t2
2681 | Just t1' <- coreView t1 = go env t1' t2
2682 | Just t2' <- coreView t2 = go env t1 t2'
2683
2684 go env (TyVarTy tv1) (TyVarTy tv2)
2685 = liftOrdering $ rnOccL env tv1 `nonDetCmpVar` rnOccR env tv2
2686 go env (ForAllTy (Bndr tv1 _) t1) (ForAllTy (Bndr tv2 _) t2)
2687 = go env (varType tv1) (varType tv2)
2688 `thenCmpTy` go (rnBndr2 env tv1 tv2) t1 t2
2689 -- See Note [Equality on AppTys]
2690 go env (AppTy s1 t1) ty2
2691 | Just (s2, t2) <- repSplitAppTy_maybe ty2
2692 = go env s1 s2 `thenCmpTy` go env t1 t2
2693 go env ty1 (AppTy s2 t2)
2694 | Just (s1, t1) <- repSplitAppTy_maybe ty1
2695 = go env s1 s2 `thenCmpTy` go env t1 t2
2696 go env (FunTy s1 t1) (FunTy s2 t2)
2697 = go env s1 s2 `thenCmpTy` go env t1 t2
2698 go env (TyConApp tc1 tys1) (TyConApp tc2 tys2)
2699 = liftOrdering (tc1 `nonDetCmpTc` tc2) `thenCmpTy` gos env tys1 tys2
2700 go _ (LitTy l1) (LitTy l2) = liftOrdering (compare l1 l2)
2701 go env (CastTy t1 _) t2 = hasCast $ go env t1 t2
2702 go env t1 (CastTy t2 _) = hasCast $ go env t1 t2
2703
2704 go _ (CoercionTy {}) (CoercionTy {}) = TEQ
2705
2706 -- Deal with the rest: TyVarTy < CoercionTy < AppTy < LitTy < TyConApp < ForAllTy
2707 go _ ty1 ty2
2708 = liftOrdering $ (get_rank ty1) `compare` (get_rank ty2)
2709 where get_rank :: Type -> Int
2710 get_rank (CastTy {})
2711 = pprPanic "nonDetCmpTypeX.get_rank" (ppr [ty1,ty2])
2712 get_rank (TyVarTy {}) = 0
2713 get_rank (CoercionTy {}) = 1
2714 get_rank (AppTy {}) = 3
2715 get_rank (LitTy {}) = 4
2716 get_rank (TyConApp {}) = 5
2717 get_rank (FunTy {}) = 6
2718 get_rank (ForAllTy {}) = 7
2719
2720 gos :: RnEnv2 -> [Type] -> [Type] -> TypeOrdering
2721 gos _ [] [] = TEQ
2722 gos _ [] _ = TLT
2723 gos _ _ [] = TGT
2724 gos env (ty1:tys1) (ty2:tys2) = go env ty1 ty2 `thenCmpTy` gos env tys1 tys2
2725
2726 -------------
2727 nonDetCmpTypesX :: RnEnv2 -> [Type] -> [Type] -> Ordering
2728 nonDetCmpTypesX _ [] [] = EQ
2729 nonDetCmpTypesX env (t1:tys1) (t2:tys2) = nonDetCmpTypeX env t1 t2
2730 `thenCmp`
2731 nonDetCmpTypesX env tys1 tys2
2732 nonDetCmpTypesX _ [] _ = LT
2733 nonDetCmpTypesX _ _ [] = GT
2734
2735 -------------
2736 -- | Compare two 'TyCon's. NB: This should /never/ see 'Constraint' (as
2737 -- recognized by Kind.isConstraintKindCon) which is considered a synonym for
2738 -- 'Type' in Core.
2739 -- See Note [Kind Constraint and kind Type] in Kind.
2740 -- See Note [nonDetCmpType nondeterminism]
2741 nonDetCmpTc :: TyCon -> TyCon -> Ordering
2742 nonDetCmpTc tc1 tc2
2743 = ASSERT( not (isConstraintKindCon tc1) && not (isConstraintKindCon tc2) )
2744 u1 `nonDetCmpUnique` u2
2745 where
2746 u1 = tyConUnique tc1
2747 u2 = tyConUnique tc2
2748
2749 {-
2750 ************************************************************************
2751 * *
2752 The kind of a type
2753 * *
2754 ************************************************************************
2755 -}
2756
2757 typeKind :: HasDebugCallStack => Type -> Kind
2758 typeKind (TyConApp tc tys) = piResultTys (tyConKind tc) tys
2759 typeKind (AppTy fun arg) = typeKind_apps fun [arg]
2760 typeKind (LitTy l) = typeLiteralKind l
2761 typeKind (FunTy {}) = liftedTypeKind
2762 typeKind (TyVarTy tyvar) = tyVarKind tyvar
2763 typeKind (CastTy _ty co) = pSnd $ coercionKind co
2764 typeKind (CoercionTy co) = coercionType co
2765 typeKind ty@(ForAllTy (Bndr tv _) _)
2766 | isTyVar tv -- See Note [Weird typing rule for ForAllTy].
2767 = case occCheckExpand tvs k of -- We must make sure tv does not occur in kind
2768 Just k' -> k' -- As it is already out of scope!
2769 Nothing -> pprPanic "typeKind"
2770 (ppr ty $$ ppr k $$ ppr tvs $$ ppr body)
2771 where
2772 (tvs, body) = splitTyVarForAllTys ty
2773 k = typeKind body
2774 typeKind (ForAllTy {}) = liftedTypeKind
2775
2776 typeKind_apps :: HasDebugCallStack => Type -> [Type] -> Kind
2777 -- The sole purpose of the function is to accumulate
2778 -- the type arugments, so we can call piResultTys, rather than
2779 -- a succession of calls to piResultTy (which is asymptotically
2780 -- less efficient as the number of arguments increases)
2781 typeKind_apps (AppTy fun arg) args = typeKind_apps fun (arg:args)
2782 typeKind_apps fun args = piResultTys (typeKind fun) args
2783
2784 --------------------------
2785 typeLiteralKind :: TyLit -> Kind
2786 typeLiteralKind l =
2787 case l of
2788 NumTyLit _ -> typeNatKind
2789 StrTyLit _ -> typeSymbolKind
2790
2791 -- | Returns True if a type is levity polymorphic. Should be the same
2792 -- as (isKindLevPoly . typeKind) but much faster.
2793 -- Precondition: The type has kind (TYPE blah)
2794 isTypeLevPoly :: Type -> Bool
2795 isTypeLevPoly = go
2796 where
2797 go ty@(TyVarTy {}) = check_kind ty
2798 go ty@(AppTy {}) = check_kind ty
2799 go ty@(TyConApp tc _) | not (isTcLevPoly tc) = False
2800 | otherwise = check_kind ty
2801 go (ForAllTy _ ty) = go ty
2802 go (FunTy {}) = False
2803 go (LitTy {}) = False
2804 go ty@(CastTy {}) = check_kind ty
2805 go ty@(CoercionTy {}) = pprPanic "isTypeLevPoly co" (ppr ty)
2806
2807 check_kind = isKindLevPoly . typeKind
2808
2809 -- | Looking past all pi-types, is the end result potentially levity polymorphic?
2810 -- Example: True for (forall r (a :: TYPE r). String -> a)
2811 -- Example: False for (forall r1 r2 (a :: TYPE r1) (b :: TYPE r2). a -> b -> Type)
2812 resultIsLevPoly :: Type -> Bool
2813 resultIsLevPoly = isTypeLevPoly . snd . splitPiTys
2814
2815
2816 {- **********************************************************************
2817 * *
2818 Occurs check expansion
2819 %* *
2820 %********************************************************************* -}
2821
2822 {- Note [Occurs check expansion]
2823 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2824 (occurCheckExpand tv xi) expands synonyms in xi just enough to get rid
2825 of occurrences of tv outside type function arguments, if that is
2826 possible; otherwise, it returns Nothing.
2827
2828 For example, suppose we have
2829 type F a b = [a]
2830 Then
2831 occCheckExpand b (F Int b) = Just [Int]
2832 but
2833 occCheckExpand a (F a Int) = Nothing
2834
2835 We don't promise to do the absolute minimum amount of expanding
2836 necessary, but we try not to do expansions we don't need to. We
2837 prefer doing inner expansions first. For example,
2838 type F a b = (a, Int, a, [a])
2839 type G b = Char
2840 We have
2841 occCheckExpand b (F (G b)) = Just (F Char)
2842 even though we could also expand F to get rid of b.
2843 -}
2844
2845 occCheckExpand :: [Var] -> Type -> Maybe Type
2846 -- See Note [Occurs check expansion]
2847 -- We may have needed to do some type synonym unfolding in order to
2848 -- get rid of the variable (or forall), so we also return the unfolded
2849 -- version of the type, which is guaranteed to be syntactically free
2850 -- of the given type variable. If the type is already syntactically
2851 -- free of the variable, then the same type is returned.
2852 occCheckExpand vs_to_avoid ty
2853 = go (mkVarSet vs_to_avoid, emptyVarEnv) ty
2854 where
2855 go :: (VarSet, VarEnv TyCoVar) -> Type -> Maybe Type
2856 -- The VarSet is the set of variables we are trying to avoid
2857 -- The VarEnv carries mappings necessary
2858 -- because of kind expansion
2859 go cxt@(as, env) (TyVarTy tv')
2860 | tv' `elemVarSet` as = Nothing
2861 | Just tv'' <- lookupVarEnv env tv' = return (mkTyVarTy tv'')
2862 | otherwise = do { tv'' <- go_var cxt tv'
2863 ; return (mkTyVarTy tv'') }
2864
2865 go _ ty@(LitTy {}) = return ty
2866 go cxt (AppTy ty1 ty2) = do { ty1' <- go cxt ty1
2867 ; ty2' <- go cxt ty2
2868 ; return (mkAppTy ty1' ty2') }
2869 go cxt (FunTy ty1 ty2) = do { ty1' <- go cxt ty1
2870 ; ty2' <- go cxt ty2
2871 ; return (mkFunTy ty1' ty2') }
2872 go cxt@(as, env) (ForAllTy (Bndr tv vis) body_ty)
2873 = do { ki' <- go cxt (varType tv)
2874 ; let tv' = setVarType tv ki'
2875 env' = extendVarEnv env tv tv'
2876 as' = as `delVarSet` tv
2877 ; body' <- go (as', env') body_ty
2878 ; return (ForAllTy (Bndr tv' vis) body') }
2879
2880 -- For a type constructor application, first try expanding away the
2881 -- offending variable from the arguments. If that doesn't work, next
2882 -- see if the type constructor is a type synonym, and if so, expand
2883 -- it and try again.
2884 go cxt ty@(TyConApp tc tys)
2885 = case mapM (go cxt) tys of
2886 Just tys' -> return (mkTyConApp tc tys')
2887 Nothing | Just ty' <- tcView ty -> go cxt ty'
2888 | otherwise -> Nothing
2889 -- Failing that, try to expand a synonym
2890
2891 go cxt (CastTy ty co) = do { ty' <- go cxt ty
2892 ; co' <- go_co cxt co
2893 ; return (mkCastTy ty' co') }
2894 go cxt (CoercionTy co) = do { co' <- go_co cxt co
2895 ; return (mkCoercionTy co') }
2896
2897 ------------------
2898 go_var cxt v = do { k' <- go cxt (varType v)
2899 ; return (setVarType v k') }
2900 -- Works for TyVar and CoVar
2901 -- See Note [Occurrence checking: look inside kinds]
2902
2903 ------------------
2904 go_mco _ MRefl = return MRefl
2905 go_mco ctx (MCo co) = MCo <$> go_co ctx co
2906
2907 ------------------
2908 go_co cxt (Refl ty) = do { ty' <- go cxt ty
2909 ; return (mkNomReflCo ty') }
2910 go_co cxt (GRefl r ty mco) = do { mco' <- go_mco cxt mco
2911 ; ty' <- go cxt ty
2912 ; return (mkGReflCo r ty' mco') }
2913 -- Note: Coercions do not contain type synonyms
2914 go_co cxt (TyConAppCo r tc args) = do { args' <- mapM (go_co cxt) args
2915 ; return (mkTyConAppCo r tc args') }
2916 go_co cxt (AppCo co arg) = do { co' <- go_co cxt co
2917 ; arg' <- go_co cxt arg
2918 ; return (mkAppCo co' arg') }
2919 go_co cxt@(as, env) (ForAllCo tv kind_co body_co)
2920 = do { kind_co' <- go_co cxt kind_co
2921 ; let tv' = setVarType tv $
2922 pFst (coercionKind kind_co')
2923 env' = extendVarEnv env tv tv'
2924 as' = as `delVarSet` tv
2925 ; body' <- go_co (as', env') body_co
2926 ; return (ForAllCo tv' kind_co' body') }
2927 go_co cxt (FunCo r co1 co2) = do { co1' <- go_co cxt co1
2928 ; co2' <- go_co cxt co2
2929 ; return (mkFunCo r co1' co2') }
2930 go_co cxt@(as,env) (CoVarCo c)
2931 | c `elemVarSet` as = Nothing
2932 | Just c' <- lookupVarEnv env c = return (mkCoVarCo c')
2933 | otherwise = do { c' <- go_var cxt c
2934 ; return (mkCoVarCo c') }
2935 go_co cxt (HoleCo h) = do { c' <- go_var cxt (ch_co_var h)
2936 ; return (HoleCo (h { ch_co_var = c' })) }
2937 go_co cxt (AxiomInstCo ax ind args) = do { args' <- mapM (go_co cxt) args
2938 ; return (mkAxiomInstCo ax ind args') }
2939 go_co cxt (UnivCo p r ty1 ty2) = do { p' <- go_prov cxt p
2940 ; ty1' <- go cxt ty1
2941 ; ty2' <- go cxt ty2
2942 ; return (mkUnivCo p' r ty1' ty2') }
2943 go_co cxt (SymCo co) = do { co' <- go_co cxt co
2944 ; return (mkSymCo co') }
2945 go_co cxt (TransCo co1 co2) = do { co1' <- go_co cxt co1
2946 ; co2' <- go_co cxt co2
2947 ; return (mkTransCo co1' co2') }
2948 go_co cxt (NthCo r n co) = do { co' <- go_co cxt co
2949 ; return (mkNthCo r n co') }
2950 go_co cxt (LRCo lr co) = do { co' <- go_co cxt co
2951 ; return (mkLRCo lr co') }
2952 go_co cxt (InstCo co arg) = do { co' <- go_co cxt co
2953 ; arg' <- go_co cxt arg
2954 ; return (mkInstCo co' arg') }
2955 go_co cxt (KindCo co) = do { co' <- go_co cxt co
2956 ; return (mkKindCo co') }
2957 go_co cxt (SubCo co) = do { co' <- go_co cxt co
2958 ; return (mkSubCo co') }
2959 go_co cxt (AxiomRuleCo ax cs) = do { cs' <- mapM (go_co cxt) cs
2960 ; return (mkAxiomRuleCo ax cs') }
2961
2962 ------------------
2963 go_prov _ UnsafeCoerceProv = return UnsafeCoerceProv
2964 go_prov cxt (PhantomProv co) = PhantomProv <$> go_co cxt co
2965 go_prov cxt (ProofIrrelProv co) = ProofIrrelProv <$> go_co cxt co
2966 go_prov _ p@(PluginProv _) = return p
2967
2968
2969 {-
2970 %************************************************************************
2971 %* *
2972 Miscellaneous functions
2973 %* *
2974 %************************************************************************
2975
2976 -}
2977 -- | All type constructors occurring in the type; looking through type
2978 -- synonyms, but not newtypes.
2979 -- When it finds a Class, it returns the class TyCon.
2980 tyConsOfType :: Type -> UniqSet TyCon
2981 tyConsOfType ty
2982 = go ty
2983 where
2984 go :: Type -> UniqSet TyCon -- The UniqSet does duplicate elim
2985 go ty | Just ty' <- coreView ty = go ty'
2986 go (TyVarTy {}) = emptyUniqSet
2987 go (LitTy {}) = emptyUniqSet
2988 go (TyConApp tc tys) = go_tc tc `unionUniqSets` go_s tys
2989 go (AppTy a b) = go a `unionUniqSets` go b
2990 go (FunTy a b) = go a `unionUniqSets` go b `unionUniqSets` go_tc funTyCon
2991 go (ForAllTy (Bndr tv _) ty) = go ty `unionUniqSets` go (varType tv)
2992 go (CastTy ty co) = go ty `unionUniqSets` go_co co
2993 go (CoercionTy co) = go_co co
2994
2995 go_co (Refl ty) = go ty
2996 go_co (GRefl _ ty mco) = go ty `unionUniqSets` go_mco mco
2997 go_co (TyConAppCo _ tc args) = go_tc tc `unionUniqSets` go_cos args
2998 go_co (AppCo co arg) = go_co co `unionUniqSets` go_co arg
2999 go_co (ForAllCo _ kind_co co) = go_co kind_co `unionUniqSets` go_co co
3000 go_co (FunCo _ co1 co2) = go_co co1 `unionUniqSets` go_co co2
3001 go_co (AxiomInstCo ax _ args) = go_ax ax `unionUniqSets` go_cos args
3002 go_co (UnivCo p _ t1 t2) = go_prov p `unionUniqSets` go t1 `unionUniqSets` go t2
3003 go_co (CoVarCo {}) = emptyUniqSet
3004 go_co (HoleCo {}) = emptyUniqSet
3005 go_co (SymCo co) = go_co co
3006 go_co (TransCo co1 co2) = go_co co1 `unionUniqSets` go_co co2
3007 go_co (NthCo _ _ co) = go_co co
3008 go_co (LRCo _ co) = go_co co
3009 go_co (InstCo co arg) = go_co co `unionUniqSets` go_co arg
3010 go_co (KindCo co) = go_co co
3011 go_co (SubCo co) = go_co co
3012 go_co (AxiomRuleCo _ cs) = go_cos cs
3013
3014 go_mco MRefl = emptyUniqSet
3015 go_mco (MCo co) = go_co co
3016
3017 go_prov UnsafeCoerceProv = emptyUniqSet
3018 go_prov (PhantomProv co) = go_co co
3019 go_prov (ProofIrrelProv co) = go_co co
3020 go_prov (PluginProv _) = emptyUniqSet
3021 -- this last case can happen from the tyConsOfType used from
3022 -- checkTauTvUpdate
3023
3024 go_s tys = foldr (unionUniqSets . go) emptyUniqSet tys
3025 go_cos cos = foldr (unionUniqSets . go_co) emptyUniqSet cos
3026
3027 go_tc tc = unitUniqSet tc
3028 go_ax ax = go_tc $ coAxiomTyCon ax
3029
3030 -- | Find the result 'Kind' of a type synonym,
3031 -- after applying it to its 'arity' number of type variables
3032 -- Actually this function works fine on data types too,
3033 -- but they'd always return '*', so we never need to ask
3034 synTyConResKind :: TyCon -> Kind
3035 synTyConResKind tycon = piResultTys (tyConKind tycon) (mkTyVarTys (tyConTyVars tycon))
3036
3037 -- | Retrieve the free variables in this type, splitting them based
3038 -- on whether they are used visibly or invisibly. Invisible ones come
3039 -- first.
3040 splitVisVarsOfType :: Type -> Pair TyCoVarSet
3041 splitVisVarsOfType orig_ty = Pair invis_vars vis_vars
3042 where
3043 Pair invis_vars1 vis_vars = go orig_ty
3044 invis_vars = invis_vars1 `minusVarSet` vis_vars
3045
3046 go (TyVarTy tv) = Pair (tyCoVarsOfType $ tyVarKind tv) (unitVarSet tv)
3047 go (AppTy t1 t2) = go t1 `mappend` go t2
3048 go (TyConApp tc tys) = go_tc tc tys
3049 go (FunTy t1 t2) = go t1 `mappend` go t2
3050 go (ForAllTy (Bndr tv _) ty)
3051 = ((`delVarSet` tv) <$> go ty) `mappend`
3052 (invisible (tyCoVarsOfType $ varType tv))
3053 go (LitTy {}) = mempty
3054 go (CastTy ty co) = go ty `mappend` invisible (tyCoVarsOfCo co)
3055 go (CoercionTy co) = invisible $ tyCoVarsOfCo co
3056
3057 invisible vs = Pair vs emptyVarSet
3058
3059 go_tc tc tys = let (invis, vis) = partitionInvisibleTypes tc tys in
3060 invisible (tyCoVarsOfTypes invis) `mappend` foldMap go vis
3061
3062 splitVisVarsOfTypes :: [Type] -> Pair TyCoVarSet
3063 splitVisVarsOfTypes = foldMap splitVisVarsOfType
3064
3065 modifyJoinResTy :: Int -- Number of binders to skip
3066 -> (Type -> Type) -- Function to apply to result type
3067 -> Type -- Type of join point
3068 -> Type -- New type
3069 -- INVARIANT: If any of the first n binders are foralls, those tyvars cannot
3070 -- appear in the original result type. See isValidJoinPointType.
3071 modifyJoinResTy orig_ar f orig_ty
3072 = go orig_ar orig_ty
3073 where
3074 go 0 ty = f ty
3075 go n ty | Just (arg_bndr, res_ty) <- splitPiTy_maybe ty
3076 = mkTyCoPiTy arg_bndr (go (n-1) res_ty)
3077 | otherwise
3078 = pprPanic "modifyJoinResTy" (ppr orig_ar <+> ppr orig_ty)
3079
3080 setJoinResTy :: Int -- Number of binders to skip
3081 -> Type -- New result type
3082 -> Type -- Type of join point
3083 -> Type -- New type
3084 -- INVARIANT: Same as for modifyJoinResTy
3085 setJoinResTy ar new_res_ty ty
3086 = modifyJoinResTy ar (const new_res_ty) ty
3087
3088
3089 {-
3090 %************************************************************************
3091 %* *
3092 Pretty-printing
3093 %* *
3094 %************************************************************************
3095
3096 Most pretty-printing is either in TyCoRep or IfaceType.
3097
3098 -}
3099
3100 -- | This variant preserves any use of TYPE in a type, effectively
3101 -- locally setting -fprint-explicit-runtime-reps.
3102 pprWithTYPE :: Type -> SDoc
3103 pprWithTYPE ty = updSDocDynFlags (flip gopt_set Opt_PrintExplicitRuntimeReps) $
3104 ppr ty