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