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