e0ceb24b069eb54ce4e940a10bb5e687966204d8
[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,
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 tyCoBinderVar_maybe :: TyCoBinder -> Maybe TyCoVar
1685 tyCoBinderVar_maybe (Named tv) = Just $ binderVar tv
1686 tyCoBinderVar_maybe _ = Nothing
1687
1688 tyCoBinderType :: TyCoBinder -> Type
1689 -- Barely used
1690 tyCoBinderType (Named tvb) = binderType tvb
1691 tyCoBinderType (Anon ty) = ty
1692
1693 tyBinderType :: TyBinder -> Type
1694 tyBinderType (Named (Bndr tv _))
1695 = ASSERT( isTyVar tv )
1696 tyVarKind tv
1697 tyBinderType (Anon ty) = ty
1698
1699 -- | Extract a relevant type, if there is one.
1700 binderRelevantType_maybe :: TyCoBinder -> Maybe Type
1701 binderRelevantType_maybe (Named {}) = Nothing
1702 binderRelevantType_maybe (Anon ty) = Just ty
1703
1704 -- | Like 'maybe', but for binders.
1705 caseBinder :: TyCoBinder -- ^ binder to scrutinize
1706 -> (TyCoVarBinder -> a) -- ^ named case
1707 -> (Type -> a) -- ^ anonymous case
1708 -> a
1709 caseBinder (Named v) f _ = f v
1710 caseBinder (Anon t) _ d = d t
1711
1712
1713 {-
1714 %************************************************************************
1715 %* *
1716 Pred
1717 * *
1718 ************************************************************************
1719
1720 Predicates on PredType
1721
1722 Note [Types for coercions, predicates, and evidence]
1723 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1724 We treat differently:
1725
1726 (a) Predicate types
1727 Test: isPredTy
1728 Binders: DictIds
1729 Kind: Constraint
1730 Examples: (Eq a), and (a ~ b)
1731
1732 (b) Coercion types are primitive, unboxed equalities
1733 Test: isCoVarTy
1734 Binders: CoVars (can appear in coercions)
1735 Kind: TYPE (TupleRep [])
1736 Examples: (t1 ~# t2) or (t1 ~R# t2)
1737
1738 (c) Evidence types is the type of evidence manipulated by
1739 the type constraint solver.
1740 Test: isEvVarType
1741 Binders: EvVars
1742 Kind: Constraint or TYPE (TupleRep [])
1743 Examples: all coercion types and predicate types
1744
1745 Coercion types and predicate types are mutually exclusive,
1746 but evidence types are a superset of both.
1747
1748 When treated as a user type, predicates are invisible and are
1749 implicitly instantiated; but coercion types, and non-pred evidence
1750 types, are just regular old types.
1751
1752 Note [Evidence for quantified constraints]
1753 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1754 The superclass mechanism in TcCanonical.makeSuperClasses risks
1755 taking a quantified constraint like
1756 (forall a. C a => a ~ b)
1757 and generate superclass evidence
1758 (forall a. C a => a ~# b)
1759
1760 This is a funny thing: neither isPredTy nor isCoVarType are true
1761 of it. So we are careful not to generate it in the first place:
1762 see Note [Equality superclasses in quantified constraints]
1763 in TcCanonical.
1764 -}
1765
1766 -- | Split a type constructor application into its type constructor and
1767 -- applied types. Note that this may fail in the case of a 'FunTy' with an
1768 -- argument of unknown kind 'FunTy' (e.g. @FunTy (a :: k) Int@. since the kind
1769 -- of @a@ isn't of the form @TYPE rep@). Consequently, you may need to zonk your
1770 -- type before using this function.
1771 --
1772 -- If you only need the 'TyCon', consider using 'tcTyConAppTyCon_maybe'.
1773 tcSplitTyConApp_maybe :: HasCallStack => Type -> Maybe (TyCon, [Type])
1774 -- Defined here to avoid module loops between Unify and TcType.
1775 tcSplitTyConApp_maybe ty | Just ty' <- tcView ty = tcSplitTyConApp_maybe ty'
1776 tcSplitTyConApp_maybe ty = tcRepSplitTyConApp_maybe ty
1777
1778 -- tcIsConstraintKind stuf only makes sense in the typechecker
1779 -- After that Constraint = Type
1780 -- See Note [coreView vs tcView]
1781 -- Defined here because it is used in isPredTy and tcRepSplitAppTy_maybe (sigh)
1782 tcIsConstraintKind :: Kind -> Bool
1783 tcIsConstraintKind ty
1784 | Just (tc, args) <- tcSplitTyConApp_maybe ty -- Note: tcSplit here
1785 , isConstraintKindCon tc
1786 = ASSERT2( null args, ppr ty ) True
1787
1788 | otherwise
1789 = False
1790
1791 -- | Is this kind equivalent to @*@?
1792 --
1793 -- This considers 'Constraint' to be distinct from @*@. For a version that
1794 -- treats them as the same type, see 'isLiftedTypeKind'.
1795 tcIsLiftedTypeKind :: Kind -> Bool
1796 tcIsLiftedTypeKind ty
1797 | Just (tc, [arg]) <- tcSplitTyConApp_maybe ty -- Note: tcSplit here
1798 , tc `hasKey` tYPETyConKey
1799 = isLiftedRuntimeRep arg
1800 | otherwise
1801 = False
1802
1803 tcReturnsConstraintKind :: Kind -> Bool
1804 -- True <=> the Kind ultimately returns a Constraint
1805 -- E.g. * -> Constraint
1806 -- forall k. k -> Constraint
1807 tcReturnsConstraintKind kind
1808 | Just kind' <- tcView kind = tcReturnsConstraintKind kind'
1809 tcReturnsConstraintKind (ForAllTy _ ty) = tcReturnsConstraintKind ty
1810 tcReturnsConstraintKind (FunTy _ ty) = tcReturnsConstraintKind ty
1811 tcReturnsConstraintKind (TyConApp tc _) = isConstraintKindCon tc
1812 tcReturnsConstraintKind _ = False
1813
1814 isEvVarType :: Type -> Bool
1815 -- True of (a) predicates, of kind Constraint, such as (Eq a), and (a ~ b)
1816 -- (b) coercion types, such as (t1 ~# t2) or (t1 ~R# t2)
1817 -- See Note [Types for coercions, predicates, and evidence]
1818 -- See Note [Evidence for quantified constraints]
1819 isEvVarType ty = isCoVarType ty || isPredTy ty
1820
1821 -- | Does this type classify a core (unlifted) Coercion?
1822 -- At either role nominal or representational
1823 -- (t1 ~# t2) or (t1 ~R# t2)
1824 -- See Note [Types for coercions, predicates, and evidence]
1825 isCoVarType :: Type -> Bool
1826 isCoVarType ty
1827 | Just (tc,tys) <- splitTyConApp_maybe ty
1828 , (tc `hasKey` eqPrimTyConKey) || (tc `hasKey` eqReprPrimTyConKey)
1829 , tys `lengthIs` 4
1830 = True
1831 isCoVarType _ = False
1832
1833 isClassPred, isEqPred, isNomEqPred, isIPPred :: PredType -> Bool
1834 isClassPred ty = case tyConAppTyCon_maybe ty of
1835 Just tyCon | isClassTyCon tyCon -> True
1836 _ -> False
1837 isEqPred ty = case tyConAppTyCon_maybe ty of
1838 Just tyCon -> tyCon `hasKey` eqPrimTyConKey
1839 || tyCon `hasKey` eqReprPrimTyConKey
1840 _ -> False
1841
1842 isNomEqPred ty = case tyConAppTyCon_maybe ty of
1843 Just tyCon -> tyCon `hasKey` eqPrimTyConKey
1844 _ -> False
1845
1846 isIPPred ty = case tyConAppTyCon_maybe ty of
1847 Just tc -> isIPTyCon tc
1848 _ -> False
1849
1850 isIPTyCon :: TyCon -> Bool
1851 isIPTyCon tc = tc `hasKey` ipClassKey
1852 -- Class and its corresponding TyCon have the same Unique
1853
1854 isIPClass :: Class -> Bool
1855 isIPClass cls = cls `hasKey` ipClassKey
1856
1857 isCTupleClass :: Class -> Bool
1858 isCTupleClass cls = isTupleTyCon (classTyCon cls)
1859
1860 isIPPred_maybe :: Type -> Maybe (FastString, Type)
1861 isIPPred_maybe ty =
1862 do (tc,[t1,t2]) <- splitTyConApp_maybe ty
1863 guard (isIPTyCon tc)
1864 x <- isStrLitTy t1
1865 return (x,t2)
1866
1867 {-
1868 Make PredTypes
1869
1870 --------------------- Equality types ---------------------------------
1871 -}
1872
1873 -- | Makes a lifted equality predicate at the given role
1874 mkPrimEqPredRole :: Role -> Type -> Type -> PredType
1875 mkPrimEqPredRole Nominal = mkPrimEqPred
1876 mkPrimEqPredRole Representational = mkReprPrimEqPred
1877 mkPrimEqPredRole Phantom = panic "mkPrimEqPredRole phantom"
1878
1879 -- | Creates a primitive type equality predicate.
1880 -- Invariant: the types are not Coercions
1881 mkPrimEqPred :: Type -> Type -> Type
1882 mkPrimEqPred ty1 ty2
1883 = TyConApp eqPrimTyCon [k1, k2, ty1, ty2]
1884 where
1885 k1 = typeKind ty1
1886 k2 = typeKind ty2
1887
1888 -- | Creates a primite type equality predicate with explicit kinds
1889 mkHeteroPrimEqPred :: Kind -> Kind -> Type -> Type -> Type
1890 mkHeteroPrimEqPred k1 k2 ty1 ty2 = TyConApp eqPrimTyCon [k1, k2, ty1, ty2]
1891
1892 -- | Creates a primitive representational type equality predicate
1893 -- with explicit kinds
1894 mkHeteroReprPrimEqPred :: Kind -> Kind -> Type -> Type -> Type
1895 mkHeteroReprPrimEqPred k1 k2 ty1 ty2
1896 = TyConApp eqReprPrimTyCon [k1, k2, ty1, ty2]
1897
1898 -- | Try to split up a coercion type into the types that it coerces
1899 splitCoercionType_maybe :: Type -> Maybe (Type, Type)
1900 splitCoercionType_maybe ty
1901 = do { (tc, [_, _, ty1, ty2]) <- splitTyConApp_maybe ty
1902 ; guard $ tc `hasKey` eqPrimTyConKey || tc `hasKey` eqReprPrimTyConKey
1903 ; return (ty1, ty2) }
1904
1905 mkReprPrimEqPred :: Type -> Type -> Type
1906 mkReprPrimEqPred ty1 ty2
1907 = TyConApp eqReprPrimTyCon [k1, k2, ty1, ty2]
1908 where
1909 k1 = typeKind ty1
1910 k2 = typeKind ty2
1911
1912 equalityTyCon :: Role -> TyCon
1913 equalityTyCon Nominal = eqPrimTyCon
1914 equalityTyCon Representational = eqReprPrimTyCon
1915 equalityTyCon Phantom = eqPhantPrimTyCon
1916
1917 -- --------------------- Dictionary types ---------------------------------
1918
1919 mkClassPred :: Class -> [Type] -> PredType
1920 mkClassPred clas tys = TyConApp (classTyCon clas) tys
1921
1922 isDictTy :: Type -> Bool
1923 isDictTy = isClassPred
1924
1925 isDictLikeTy :: Type -> Bool
1926 -- Note [Dictionary-like types]
1927 isDictLikeTy ty | Just ty' <- coreView ty = isDictLikeTy ty'
1928 isDictLikeTy ty = case splitTyConApp_maybe ty of
1929 Just (tc, tys) | isClassTyCon tc -> True
1930 | isTupleTyCon tc -> all isDictLikeTy tys
1931 _other -> False
1932
1933 {-
1934 Note [Dictionary-like types]
1935 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1936 Being "dictionary-like" means either a dictionary type or a tuple thereof.
1937 In GHC 6.10 we build implication constraints which construct such tuples,
1938 and if we land up with a binding
1939 t :: (C [a], Eq [a])
1940 t = blah
1941 then we want to treat t as cheap under "-fdicts-cheap" for example.
1942 (Implication constraints are normally inlined, but sadly not if the
1943 occurrence is itself inside an INLINE function! Until we revise the
1944 handling of implication constraints, that is.) This turned out to
1945 be important in getting good arities in DPH code. Example:
1946
1947 class C a
1948 class D a where { foo :: a -> a }
1949 instance C a => D (Maybe a) where { foo x = x }
1950
1951 bar :: (C a, C b) => a -> b -> (Maybe a, Maybe b)
1952 {-# INLINE bar #-}
1953 bar x y = (foo (Just x), foo (Just y))
1954
1955 Then 'bar' should jolly well have arity 4 (two dicts, two args), but
1956 we ended up with something like
1957 bar = __inline_me__ (\d1,d2. let t :: (D (Maybe a), D (Maybe b)) = ...
1958 in \x,y. <blah>)
1959
1960 This is all a bit ad-hoc; eg it relies on knowing that implication
1961 constraints build tuples.
1962
1963
1964 Decomposing PredType
1965 -}
1966
1967 -- | A choice of equality relation. This is separate from the type 'Role'
1968 -- because 'Phantom' does not define a (non-trivial) equality relation.
1969 data EqRel = NomEq | ReprEq
1970 deriving (Eq, Ord)
1971
1972 instance Outputable EqRel where
1973 ppr NomEq = text "nominal equality"
1974 ppr ReprEq = text "representational equality"
1975
1976 eqRelRole :: EqRel -> Role
1977 eqRelRole NomEq = Nominal
1978 eqRelRole ReprEq = Representational
1979
1980 data PredTree
1981 = ClassPred Class [Type]
1982 | EqPred EqRel Type Type
1983 | IrredPred PredType
1984 | ForAllPred [TyCoVarBinder] [PredType] PredType
1985 -- ForAllPred: see Note [Quantified constraints] in TcCanonical
1986 -- NB: There is no TuplePred case
1987 -- Tuple predicates like (Eq a, Ord b) are just treated
1988 -- as ClassPred, as if we had a tuple class with two superclasses
1989 -- class (c1, c2) => (%,%) c1 c2
1990
1991 classifyPredType :: PredType -> PredTree
1992 classifyPredType ev_ty = case splitTyConApp_maybe ev_ty of
1993 Just (tc, [_, _, ty1, ty2])
1994 | tc `hasKey` eqReprPrimTyConKey -> EqPred ReprEq ty1 ty2
1995 | tc `hasKey` eqPrimTyConKey -> EqPred NomEq ty1 ty2
1996
1997 Just (tc, tys)
1998 | Just clas <- tyConClass_maybe tc
1999 -> ClassPred clas tys
2000
2001 _ | (tvs, rho) <- splitForAllVarBndrs ev_ty
2002 , (theta, pred) <- splitFunTys rho
2003 , not (null tvs && null theta)
2004 -> ForAllPred tvs theta pred
2005
2006 | otherwise
2007 -> IrredPred ev_ty
2008
2009 getClassPredTys :: HasDebugCallStack => PredType -> (Class, [Type])
2010 getClassPredTys ty = case getClassPredTys_maybe ty of
2011 Just (clas, tys) -> (clas, tys)
2012 Nothing -> pprPanic "getClassPredTys" (ppr ty)
2013
2014 getClassPredTys_maybe :: PredType -> Maybe (Class, [Type])
2015 getClassPredTys_maybe ty = case splitTyConApp_maybe ty of
2016 Just (tc, tys) | Just clas <- tyConClass_maybe tc -> Just (clas, tys)
2017 _ -> Nothing
2018
2019 getEqPredTys :: PredType -> (Type, Type)
2020 getEqPredTys ty
2021 = case splitTyConApp_maybe ty of
2022 Just (tc, [_, _, ty1, ty2])
2023 | tc `hasKey` eqPrimTyConKey
2024 || tc `hasKey` eqReprPrimTyConKey
2025 -> (ty1, ty2)
2026 _ -> pprPanic "getEqPredTys" (ppr ty)
2027
2028 getEqPredTys_maybe :: PredType -> Maybe (Role, Type, Type)
2029 getEqPredTys_maybe ty
2030 = case splitTyConApp_maybe ty of
2031 Just (tc, [_, _, ty1, ty2])
2032 | tc `hasKey` eqPrimTyConKey -> Just (Nominal, ty1, ty2)
2033 | tc `hasKey` eqReprPrimTyConKey -> Just (Representational, ty1, ty2)
2034 _ -> Nothing
2035
2036 getEqPredRole :: PredType -> Role
2037 getEqPredRole ty = eqRelRole (predTypeEqRel ty)
2038
2039 -- | Get the equality relation relevant for a pred type.
2040 predTypeEqRel :: PredType -> EqRel
2041 predTypeEqRel ty
2042 | Just (tc, _) <- splitTyConApp_maybe ty
2043 , tc `hasKey` eqReprPrimTyConKey
2044 = ReprEq
2045 | otherwise
2046 = NomEq
2047
2048 {-
2049 %************************************************************************
2050 %* *
2051 Well-scoped tyvars
2052 * *
2053 ************************************************************************
2054
2055 Note [ScopedSort]
2056 ~~~~~~~~~~~~~~~~~
2057 Consider
2058
2059 foo :: Proxy a -> Proxy (b :: k) -> Proxy (a :: k2) -> ()
2060
2061 This function type is implicitly generalised over [a, b, k, k2]. These
2062 variables will be Specified; that is, they will be available for visible
2063 type application. This is because they are written in the type signature
2064 by the user.
2065
2066 However, we must ask: what order will they appear in? In cases without
2067 dependency, this is easy: we just use the lexical left-to-right ordering
2068 of first occurrence. With dependency, we cannot get off the hook so
2069 easily.
2070
2071 We thus state:
2072
2073 * These variables appear in the order as given by ScopedSort, where
2074 the input to ScopedSort is the left-to-right order of first occurrence.
2075
2076 Note that this applies only to *implicit* quantification, without a
2077 `forall`. If the user writes a `forall`, then we just use the order given.
2078
2079 ScopedSort is defined thusly (as proposed in #15743):
2080 * Work left-to-right through the input list, with a cursor.
2081 * If variable v at the cursor is depended on by any earlier variable w,
2082 move v immediately before the leftmost such w.
2083
2084 INVARIANT: The prefix of variables before the cursor form a valid telescope.
2085
2086 Note that ScopedSort makes sense only after type inference is done and all
2087 types/kinds are fully settled and zonked.
2088
2089 -}
2090
2091 -- | Do a topological sort on a list of tyvars,
2092 -- so that binders occur before occurrences
2093 -- E.g. given [ a::k, k::*, b::k ]
2094 -- it'll return a well-scoped list [ k::*, a::k, b::k ]
2095 --
2096 -- This is a deterministic sorting operation
2097 -- (that is, doesn't depend on Uniques).
2098 --
2099 -- It is also meant to be stable: that is, variables should not
2100 -- be reordered unnecessarily. This is specified in Note [ScopedSort]
2101 -- See also Note [Ordering of implicit variables] in RnTypes
2102
2103 scopedSort :: [TyCoVar] -> [TyCoVar]
2104 scopedSort = go [] []
2105 where
2106 go :: [TyCoVar] -- already sorted, in reverse order
2107 -> [TyCoVarSet] -- each set contains all the variables which must be placed
2108 -- before the tv corresponding to the set; they are accumulations
2109 -- of the fvs in the sorted tvs' kinds
2110
2111 -- This list is in 1-to-1 correspondence with the sorted tyvars
2112 -- INVARIANT:
2113 -- all (\tl -> all (`subVarSet` head tl) (tail tl)) (tails fv_list)
2114 -- That is, each set in the list is a superset of all later sets.
2115
2116 -> [TyCoVar] -- yet to be sorted
2117 -> [TyCoVar]
2118 go acc _fv_list [] = reverse acc
2119 go acc fv_list (tv:tvs)
2120 = go acc' fv_list' tvs
2121 where
2122 (acc', fv_list') = insert tv acc fv_list
2123
2124 insert :: TyCoVar -- var to insert
2125 -> [TyCoVar] -- sorted list, in reverse order
2126 -> [TyCoVarSet] -- list of fvs, as above
2127 -> ([TyCoVar], [TyCoVarSet]) -- augmented lists
2128 insert tv [] [] = ([tv], [tyCoVarsOfType (tyVarKind tv)])
2129 insert tv (a:as) (fvs:fvss)
2130 | tv `elemVarSet` fvs
2131 , (as', fvss') <- insert tv as fvss
2132 = (a:as', fvs `unionVarSet` fv_tv : fvss')
2133
2134 | otherwise
2135 = (tv:a:as, fvs `unionVarSet` fv_tv : fvs : fvss)
2136 where
2137 fv_tv = tyCoVarsOfType (tyVarKind tv)
2138
2139 -- lists not in correspondence
2140 insert _ _ _ = panic "scopedSort"
2141
2142 -- | Extract a well-scoped list of variables from a deterministic set of
2143 -- variables. The result is deterministic.
2144 -- NB: There used to exist varSetElemsWellScoped :: VarSet -> [Var] which
2145 -- took a non-deterministic set and produced a non-deterministic
2146 -- well-scoped list. If you care about the list being well-scoped you also
2147 -- most likely care about it being in deterministic order.
2148 dVarSetElemsWellScoped :: DVarSet -> [Var]
2149 dVarSetElemsWellScoped = scopedSort . dVarSetElems
2150
2151 -- | Get the free vars of a type in scoped order
2152 tyCoVarsOfTypeWellScoped :: Type -> [TyVar]
2153 tyCoVarsOfTypeWellScoped = scopedSort . tyCoVarsOfTypeList
2154
2155 -- | Get the free vars of types in scoped order
2156 tyCoVarsOfTypesWellScoped :: [Type] -> [TyVar]
2157 tyCoVarsOfTypesWellScoped = scopedSort . tyCoVarsOfTypesList
2158
2159 -- | Given the suffix of a telescope, returns the prefix.
2160 -- Ex: given [(k :: j), (a :: Proxy k)], returns [(j :: *)].
2161 tyCoVarsOfBindersWellScoped :: [TyVar] -> [TyVar]
2162 tyCoVarsOfBindersWellScoped tvs
2163 = tyCoVarsOfTypeWellScoped (mkInvForAllTys tvs unitTy)
2164
2165 ------------- Closing over kinds -----------------
2166
2167 -- | Add the kind variables free in the kinds of the tyvars in the given set.
2168 -- Returns a non-deterministic set.
2169 closeOverKinds :: TyVarSet -> TyVarSet
2170 closeOverKinds = fvVarSet . closeOverKindsFV . nonDetEltsUniqSet
2171 -- It's OK to use nonDetEltsUniqSet here because we immediately forget
2172 -- about the ordering by returning a set.
2173
2174 -- | Given a list of tyvars returns a deterministic FV computation that
2175 -- returns the given tyvars with the kind variables free in the kinds of the
2176 -- given tyvars.
2177 closeOverKindsFV :: [TyVar] -> FV
2178 closeOverKindsFV tvs =
2179 mapUnionFV (tyCoFVsOfType . tyVarKind) tvs `unionFV` mkFVs tvs
2180
2181 -- | Add the kind variables free in the kinds of the tyvars in the given set.
2182 -- Returns a deterministically ordered list.
2183 closeOverKindsList :: [TyVar] -> [TyVar]
2184 closeOverKindsList tvs = fvVarList $ closeOverKindsFV tvs
2185
2186 -- | Add the kind variables free in the kinds of the tyvars in the given set.
2187 -- Returns a deterministic set.
2188 closeOverKindsDSet :: DTyVarSet -> DTyVarSet
2189 closeOverKindsDSet = fvDVarSet . closeOverKindsFV . dVarSetElems
2190
2191 {-
2192 ************************************************************************
2193 * *
2194 \subsection{Type families}
2195 * *
2196 ************************************************************************
2197 -}
2198
2199 mkFamilyTyConApp :: TyCon -> [Type] -> Type
2200 -- ^ Given a family instance TyCon and its arg types, return the
2201 -- corresponding family type. E.g:
2202 --
2203 -- > data family T a
2204 -- > data instance T (Maybe b) = MkT b
2205 --
2206 -- Where the instance tycon is :RTL, so:
2207 --
2208 -- > mkFamilyTyConApp :RTL Int = T (Maybe Int)
2209 mkFamilyTyConApp tc tys
2210 | Just (fam_tc, fam_tys) <- tyConFamInst_maybe tc
2211 , let tvs = tyConTyVars tc
2212 fam_subst = ASSERT2( tvs `equalLength` tys, ppr tc <+> ppr tys )
2213 zipTvSubst tvs tys
2214 = mkTyConApp fam_tc (substTys fam_subst fam_tys)
2215 | otherwise
2216 = mkTyConApp tc tys
2217
2218 -- | Get the type on the LHS of a coercion induced by a type/data
2219 -- family instance.
2220 coAxNthLHS :: CoAxiom br -> Int -> Type
2221 coAxNthLHS ax ind =
2222 mkTyConApp (coAxiomTyCon ax) (coAxBranchLHS (coAxiomNthBranch ax ind))
2223
2224 -- | Pretty prints a 'TyCon', using the family instance in case of a
2225 -- representation tycon. For example:
2226 --
2227 -- > data T [a] = ...
2228 --
2229 -- In that case we want to print @T [a]@, where @T@ is the family 'TyCon'
2230 pprSourceTyCon :: TyCon -> SDoc
2231 pprSourceTyCon tycon
2232 | Just (fam_tc, tys) <- tyConFamInst_maybe tycon
2233 = ppr $ fam_tc `TyConApp` tys -- can't be FunTyCon
2234 | otherwise
2235 = ppr tycon
2236
2237 isFamFreeTy :: Type -> Bool
2238 isFamFreeTy ty | Just ty' <- coreView ty = isFamFreeTy ty'
2239 isFamFreeTy (TyVarTy _) = True
2240 isFamFreeTy (LitTy {}) = True
2241 isFamFreeTy (TyConApp tc tys) = all isFamFreeTy tys && isFamFreeTyCon tc
2242 isFamFreeTy (AppTy a b) = isFamFreeTy a && isFamFreeTy b
2243 isFamFreeTy (FunTy a b) = isFamFreeTy a && isFamFreeTy b
2244 isFamFreeTy (ForAllTy _ ty) = isFamFreeTy ty
2245 isFamFreeTy (CastTy ty _) = isFamFreeTy ty
2246 isFamFreeTy (CoercionTy _) = False -- Not sure about this
2247
2248 {-
2249 ************************************************************************
2250 * *
2251 \subsection{Liftedness}
2252 * *
2253 ************************************************************************
2254 -}
2255
2256 -- | Returns Just True if this type is surely lifted, Just False
2257 -- if it is surely unlifted, Nothing if we can't be sure (i.e., it is
2258 -- levity polymorphic), and panics if the kind does not have the shape
2259 -- TYPE r.
2260 isLiftedType_maybe :: HasDebugCallStack => Type -> Maybe Bool
2261 isLiftedType_maybe ty = go (getRuntimeRep ty)
2262 where
2263 go rr | Just rr' <- coreView rr = go rr'
2264 | isLiftedRuntimeRep rr = Just True
2265 | TyConApp {} <- rr = Just False -- Everything else is unlifted
2266 | otherwise = Nothing -- levity polymorphic
2267
2268 -- | See "Type#type_classification" for what an unlifted type is.
2269 -- Panics on levity polymorphic types.
2270 isUnliftedType :: HasDebugCallStack => Type -> Bool
2271 -- isUnliftedType returns True for forall'd unlifted types:
2272 -- x :: forall a. Int#
2273 -- I found bindings like these were getting floated to the top level.
2274 -- They are pretty bogus types, mind you. It would be better never to
2275 -- construct them
2276 isUnliftedType ty
2277 = not (isLiftedType_maybe ty `orElse`
2278 pprPanic "isUnliftedType" (ppr ty <+> dcolon <+> ppr (typeKind ty)))
2279
2280 -- | Is this a type of kind RuntimeRep? (e.g. LiftedRep)
2281 isRuntimeRepKindedTy :: Type -> Bool
2282 isRuntimeRepKindedTy = isRuntimeRepTy . typeKind
2283
2284 -- | Drops prefix of RuntimeRep constructors in 'TyConApp's. Useful for e.g.
2285 -- dropping 'LiftedRep arguments of unboxed tuple TyCon applications:
2286 --
2287 -- dropRuntimeRepArgs [ 'LiftedRep, 'IntRep
2288 -- , String, Int# ] == [String, Int#]
2289 --
2290 dropRuntimeRepArgs :: [Type] -> [Type]
2291 dropRuntimeRepArgs = dropWhile isRuntimeRepKindedTy
2292
2293 -- | Extract the RuntimeRep classifier of a type. For instance,
2294 -- @getRuntimeRep_maybe Int = LiftedRep@. Returns 'Nothing' if this is not
2295 -- possible.
2296 getRuntimeRep_maybe :: HasDebugCallStack
2297 => Type -> Maybe Type
2298 getRuntimeRep_maybe = kindRep_maybe . typeKind
2299
2300 -- | Extract the RuntimeRep classifier of a type. For instance,
2301 -- @getRuntimeRep_maybe Int = LiftedRep@. Panics if this is not possible.
2302 getRuntimeRep :: HasDebugCallStack => Type -> Type
2303 getRuntimeRep ty
2304 = case getRuntimeRep_maybe ty of
2305 Just r -> r
2306 Nothing -> pprPanic "getRuntimeRep" (ppr ty <+> dcolon <+> ppr (typeKind ty))
2307
2308 isUnboxedTupleType :: Type -> Bool
2309 isUnboxedTupleType ty
2310 = tyConAppTyCon (getRuntimeRep ty) `hasKey` tupleRepDataConKey
2311 -- NB: Do not use typePrimRep, as that can't tell the difference between
2312 -- unboxed tuples and unboxed sums
2313
2314
2315 isUnboxedSumType :: Type -> Bool
2316 isUnboxedSumType ty
2317 = tyConAppTyCon (getRuntimeRep ty) `hasKey` sumRepDataConKey
2318
2319 -- | See "Type#type_classification" for what an algebraic type is.
2320 -- Should only be applied to /types/, as opposed to e.g. partially
2321 -- saturated type constructors
2322 isAlgType :: Type -> Bool
2323 isAlgType ty
2324 = case splitTyConApp_maybe ty of
2325 Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
2326 isAlgTyCon tc
2327 _other -> False
2328
2329 -- | Check whether a type is a data family type
2330 isDataFamilyAppType :: Type -> Bool
2331 isDataFamilyAppType ty = case tyConAppTyCon_maybe ty of
2332 Just tc -> isDataFamilyTyCon tc
2333 _ -> False
2334
2335 -- | Computes whether an argument (or let right hand side) should
2336 -- be computed strictly or lazily, based only on its type.
2337 -- Currently, it's just 'isUnliftedType'. Panics on levity-polymorphic types.
2338 isStrictType :: HasDebugCallStack => Type -> Bool
2339 isStrictType = isUnliftedType
2340
2341 isPrimitiveType :: Type -> Bool
2342 -- ^ Returns true of types that are opaque to Haskell.
2343 isPrimitiveType ty = case splitTyConApp_maybe ty of
2344 Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
2345 isPrimTyCon tc
2346 _ -> False
2347
2348 {-
2349 ************************************************************************
2350 * *
2351 \subsection{Join points}
2352 * *
2353 ************************************************************************
2354 -}
2355
2356 -- | Determine whether a type could be the type of a join point of given total
2357 -- arity, according to the polymorphism rule. A join point cannot be polymorphic
2358 -- in its return type, since given
2359 -- join j @a @b x y z = e1 in e2,
2360 -- the types of e1 and e2 must be the same, and a and b are not in scope for e2.
2361 -- (See Note [The polymorphism rule of join points] in CoreSyn.) Returns False
2362 -- also if the type simply doesn't have enough arguments.
2363 --
2364 -- Note that we need to know how many arguments (type *and* value) the putative
2365 -- join point takes; for instance, if
2366 -- j :: forall a. a -> Int
2367 -- then j could be a binary join point returning an Int, but it could *not* be a
2368 -- unary join point returning a -> Int.
2369 --
2370 -- TODO: See Note [Excess polymorphism and join points]
2371 isValidJoinPointType :: JoinArity -> Type -> Bool
2372 isValidJoinPointType arity ty
2373 = valid_under emptyVarSet arity ty
2374 where
2375 valid_under tvs arity ty
2376 | arity == 0
2377 = isEmptyVarSet (tvs `intersectVarSet` tyCoVarsOfType ty)
2378 | Just (t, ty') <- splitForAllTy_maybe ty
2379 = valid_under (tvs `extendVarSet` t) (arity-1) ty'
2380 | Just (_, res_ty) <- splitFunTy_maybe ty
2381 = valid_under tvs (arity-1) res_ty
2382 | otherwise
2383 = False
2384
2385 {- Note [Excess polymorphism and join points]
2386 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2387 In principle, if a function would be a join point except that it fails
2388 the polymorphism rule (see Note [The polymorphism rule of join points] in
2389 CoreSyn), it can still be made a join point with some effort. This is because
2390 all tail calls must return the same type (they return to the same context!), and
2391 thus if the return type depends on an argument, that argument must always be the
2392 same.
2393
2394 For instance, consider:
2395
2396 let f :: forall a. a -> Char -> [a]
2397 f @a x c = ... f @a y 'a' ...
2398 in ... f @Int 1 'b' ... f @Int 2 'c' ...
2399
2400 (where the calls are tail calls). `f` fails the polymorphism rule because its
2401 return type is [a], where [a] is bound. But since the type argument is always
2402 'Int', we can rewrite it as:
2403
2404 let f' :: Int -> Char -> [Int]
2405 f' x c = ... f' y 'a' ...
2406 in ... f' 1 'b' ... f 2 'c' ...
2407
2408 and now we can make f' a join point:
2409
2410 join f' :: Int -> Char -> [Int]
2411 f' x c = ... jump f' y 'a' ...
2412 in ... jump f' 1 'b' ... jump f' 2 'c' ...
2413
2414 It's not clear that this comes up often, however. TODO: Measure how often and
2415 add this analysis if necessary. See Trac #14620.
2416
2417
2418 ************************************************************************
2419 * *
2420 \subsection{Sequencing on types}
2421 * *
2422 ************************************************************************
2423 -}
2424
2425 seqType :: Type -> ()
2426 seqType (LitTy n) = n `seq` ()
2427 seqType (TyVarTy tv) = tv `seq` ()
2428 seqType (AppTy t1 t2) = seqType t1 `seq` seqType t2
2429 seqType (FunTy t1 t2) = seqType t1 `seq` seqType t2
2430 seqType (TyConApp tc tys) = tc `seq` seqTypes tys
2431 seqType (ForAllTy (Bndr tv _) ty) = seqType (varType tv) `seq` seqType ty
2432 seqType (CastTy ty co) = seqType ty `seq` seqCo co
2433 seqType (CoercionTy co) = seqCo co
2434
2435 seqTypes :: [Type] -> ()
2436 seqTypes [] = ()
2437 seqTypes (ty:tys) = seqType ty `seq` seqTypes tys
2438
2439 {-
2440 ************************************************************************
2441 * *
2442 Comparison for types
2443 (We don't use instances so that we know where it happens)
2444 * *
2445 ************************************************************************
2446
2447 Note [Equality on AppTys]
2448 ~~~~~~~~~~~~~~~~~~~~~~~~~
2449 In our cast-ignoring equality, we want to say that the following two
2450 are equal:
2451
2452 (Maybe |> co) (Int |> co') ~? Maybe Int
2453
2454 But the left is an AppTy while the right is a TyConApp. The solution is
2455 to use repSplitAppTy_maybe to break up the TyConApp into its pieces and
2456 then continue. Easy to do, but also easy to forget to do.
2457
2458 -}
2459
2460 eqType :: Type -> Type -> Bool
2461 -- ^ Type equality on source types. Does not look through @newtypes@ or
2462 -- 'PredType's, but it does look through type synonyms.
2463 -- This first checks that the kinds of the types are equal and then
2464 -- checks whether the types are equal, ignoring casts and coercions.
2465 -- (The kind check is a recursive call, but since all kinds have type
2466 -- @Type@, there is no need to check the types of kinds.)
2467 -- See also Note [Non-trivial definitional equality] in TyCoRep.
2468 eqType t1 t2 = isEqual $ nonDetCmpType t1 t2
2469 -- It's OK to use nonDetCmpType here and eqType is deterministic,
2470 -- nonDetCmpType does equality deterministically
2471
2472 -- | Compare types with respect to a (presumably) non-empty 'RnEnv2'.
2473 eqTypeX :: RnEnv2 -> Type -> Type -> Bool
2474 eqTypeX env t1 t2 = isEqual $ nonDetCmpTypeX env t1 t2
2475 -- It's OK to use nonDetCmpType here and eqTypeX is deterministic,
2476 -- nonDetCmpTypeX does equality deterministically
2477
2478 -- | Type equality on lists of types, looking through type synonyms
2479 -- but not newtypes.
2480 eqTypes :: [Type] -> [Type] -> Bool
2481 eqTypes tys1 tys2 = isEqual $ nonDetCmpTypes tys1 tys2
2482 -- It's OK to use nonDetCmpType here and eqTypes is deterministic,
2483 -- nonDetCmpTypes does equality deterministically
2484
2485 eqVarBndrs :: RnEnv2 -> [Var] -> [Var] -> Maybe RnEnv2
2486 -- Check that the var lists are the same length
2487 -- and have matching kinds; if so, extend the RnEnv2
2488 -- Returns Nothing if they don't match
2489 eqVarBndrs env [] []
2490 = Just env
2491 eqVarBndrs env (tv1:tvs1) (tv2:tvs2)
2492 | eqTypeX env (varType tv1) (varType tv2)
2493 = eqVarBndrs (rnBndr2 env tv1 tv2) tvs1 tvs2
2494 eqVarBndrs _ _ _= Nothing
2495
2496 -- Now here comes the real worker
2497
2498 {-
2499 Note [nonDetCmpType nondeterminism]
2500 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2501 nonDetCmpType is implemented in terms of nonDetCmpTypeX. nonDetCmpTypeX
2502 uses nonDetCmpTc which compares TyCons by their Unique value. Using Uniques for
2503 ordering leads to nondeterminism. We hit the same problem in the TyVarTy case,
2504 comparing type variables is nondeterministic, note the call to nonDetCmpVar in
2505 nonDetCmpTypeX.
2506 See Note [Unique Determinism] for more details.
2507 -}
2508
2509 nonDetCmpType :: Type -> Type -> Ordering
2510 nonDetCmpType t1 t2
2511 -- we know k1 and k2 have the same kind, because they both have kind *.
2512 = nonDetCmpTypeX rn_env t1 t2
2513 where
2514 rn_env = mkRnEnv2 (mkInScopeSet (tyCoVarsOfTypes [t1, t2]))
2515
2516 nonDetCmpTypes :: [Type] -> [Type] -> Ordering
2517 nonDetCmpTypes ts1 ts2 = nonDetCmpTypesX rn_env ts1 ts2
2518 where
2519 rn_env = mkRnEnv2 (mkInScopeSet (tyCoVarsOfTypes (ts1 ++ ts2)))
2520
2521 -- | An ordering relation between two 'Type's (known below as @t1 :: k1@
2522 -- and @t2 :: k2@)
2523 data TypeOrdering = TLT -- ^ @t1 < t2@
2524 | TEQ -- ^ @t1 ~ t2@ and there are no casts in either,
2525 -- therefore we can conclude @k1 ~ k2@
2526 | TEQX -- ^ @t1 ~ t2@ yet one of the types contains a cast so
2527 -- they may differ in kind.
2528 | TGT -- ^ @t1 > t2@
2529 deriving (Eq, Ord, Enum, Bounded)
2530
2531 nonDetCmpTypeX :: RnEnv2 -> Type -> Type -> Ordering -- Main workhorse
2532 -- See Note [Non-trivial definitional equality] in TyCoRep
2533 nonDetCmpTypeX env orig_t1 orig_t2 =
2534 case go env orig_t1 orig_t2 of
2535 -- If there are casts then we also need to do a comparison of the kinds of
2536 -- the types being compared
2537 TEQX -> toOrdering $ go env k1 k2
2538 ty_ordering -> toOrdering ty_ordering
2539 where
2540 k1 = typeKind orig_t1
2541 k2 = typeKind orig_t2
2542
2543 toOrdering :: TypeOrdering -> Ordering
2544 toOrdering TLT = LT
2545 toOrdering TEQ = EQ
2546 toOrdering TEQX = EQ
2547 toOrdering TGT = GT
2548
2549 liftOrdering :: Ordering -> TypeOrdering
2550 liftOrdering LT = TLT
2551 liftOrdering EQ = TEQ
2552 liftOrdering GT = TGT
2553
2554 thenCmpTy :: TypeOrdering -> TypeOrdering -> TypeOrdering
2555 thenCmpTy TEQ rel = rel
2556 thenCmpTy TEQX rel = hasCast rel
2557 thenCmpTy rel _ = rel
2558
2559 hasCast :: TypeOrdering -> TypeOrdering
2560 hasCast TEQ = TEQX
2561 hasCast rel = rel
2562
2563 -- Returns both the resulting ordering relation between the two types
2564 -- and whether either contains a cast.
2565 go :: RnEnv2 -> Type -> Type -> TypeOrdering
2566 go env t1 t2
2567 | Just t1' <- coreView t1 = go env t1' t2
2568 | Just t2' <- coreView t2 = go env t1 t2'
2569
2570 go env (TyVarTy tv1) (TyVarTy tv2)
2571 = liftOrdering $ rnOccL env tv1 `nonDetCmpVar` rnOccR env tv2
2572 go env (ForAllTy (Bndr tv1 _) t1) (ForAllTy (Bndr tv2 _) t2)
2573 = go env (varType tv1) (varType tv2)
2574 `thenCmpTy` go (rnBndr2 env tv1 tv2) t1 t2
2575 -- See Note [Equality on AppTys]
2576 go env (AppTy s1 t1) ty2
2577 | Just (s2, t2) <- repSplitAppTy_maybe ty2
2578 = go env s1 s2 `thenCmpTy` go env t1 t2
2579 go env ty1 (AppTy s2 t2)
2580 | Just (s1, t1) <- repSplitAppTy_maybe ty1
2581 = go env s1 s2 `thenCmpTy` go env t1 t2
2582 go env (FunTy s1 t1) (FunTy s2 t2)
2583 = go env s1 s2 `thenCmpTy` go env t1 t2
2584 go env (TyConApp tc1 tys1) (TyConApp tc2 tys2)
2585 = liftOrdering (tc1 `nonDetCmpTc` tc2) `thenCmpTy` gos env tys1 tys2
2586 go _ (LitTy l1) (LitTy l2) = liftOrdering (compare l1 l2)
2587 go env (CastTy t1 _) t2 = hasCast $ go env t1 t2
2588 go env t1 (CastTy t2 _) = hasCast $ go env t1 t2
2589
2590 go _ (CoercionTy {}) (CoercionTy {}) = TEQ
2591
2592 -- Deal with the rest: TyVarTy < CoercionTy < AppTy < LitTy < TyConApp < ForAllTy
2593 go _ ty1 ty2
2594 = liftOrdering $ (get_rank ty1) `compare` (get_rank ty2)
2595 where get_rank :: Type -> Int
2596 get_rank (CastTy {})
2597 = pprPanic "nonDetCmpTypeX.get_rank" (ppr [ty1,ty2])
2598 get_rank (TyVarTy {}) = 0
2599 get_rank (CoercionTy {}) = 1
2600 get_rank (AppTy {}) = 3
2601 get_rank (LitTy {}) = 4
2602 get_rank (TyConApp {}) = 5
2603 get_rank (FunTy {}) = 6
2604 get_rank (ForAllTy {}) = 7
2605
2606 gos :: RnEnv2 -> [Type] -> [Type] -> TypeOrdering
2607 gos _ [] [] = TEQ
2608 gos _ [] _ = TLT
2609 gos _ _ [] = TGT
2610 gos env (ty1:tys1) (ty2:tys2) = go env ty1 ty2 `thenCmpTy` gos env tys1 tys2
2611
2612 -------------
2613 nonDetCmpTypesX :: RnEnv2 -> [Type] -> [Type] -> Ordering
2614 nonDetCmpTypesX _ [] [] = EQ
2615 nonDetCmpTypesX env (t1:tys1) (t2:tys2) = nonDetCmpTypeX env t1 t2
2616 `thenCmp`
2617 nonDetCmpTypesX env tys1 tys2
2618 nonDetCmpTypesX _ [] _ = LT
2619 nonDetCmpTypesX _ _ [] = GT
2620
2621 -------------
2622 -- | Compare two 'TyCon's. NB: This should /never/ see 'Constraint' (as
2623 -- recognized by Kind.isConstraintKindCon) which is considered a synonym for
2624 -- 'Type' in Core.
2625 -- See Note [Kind Constraint and kind Type] in Kind.
2626 -- See Note [nonDetCmpType nondeterminism]
2627 nonDetCmpTc :: TyCon -> TyCon -> Ordering
2628 nonDetCmpTc tc1 tc2
2629 = ASSERT( not (isConstraintKindCon tc1) && not (isConstraintKindCon tc2) )
2630 u1 `nonDetCmpUnique` u2
2631 where
2632 u1 = tyConUnique tc1
2633 u2 = tyConUnique tc2
2634
2635 {-
2636 ************************************************************************
2637 * *
2638 The kind of a type
2639 * *
2640 ************************************************************************
2641
2642 Note [typeKind vs tcTypeKind]
2643 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2644 We have two functions to get the kind of a type
2645
2646 * typeKind ignores the distinction between Constraint and *
2647 * tcTypeKind respects the distinction between Constraint and *
2648
2649 tcTypeKind is used by the type inference engine, for which Constraint
2650 and * are different; after that we use typeKind.
2651
2652 See also Note [coreView vs tcView]
2653
2654 Note [Kinding rules for types]
2655 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2656 In typeKind we consider Constraint and (TYPE LiftedRep) to be identical.
2657 We then have
2658
2659 t1 : TYPE rep1
2660 t2 : TYPE rep2
2661 (FUN) ----------------
2662 t1 -> t2 : Type
2663
2664 ty : TYPE rep
2665 `a` is not free in rep
2666 (FORALL) -----------------------
2667 forall a. ty : TYPE rep
2668
2669 In tcTypeKind we consider Constraint and (TYPE LiftedRep) to be distinct:
2670
2671 t1 : TYPE rep1
2672 t2 : TYPE rep2
2673 (FUN) ----------------
2674 t1 -> t2 : Type
2675
2676 t1 : Constraint
2677 t2 : TYPE rep
2678 (PRED1) ----------------
2679 t1 => t2 : Type
2680
2681 t1 : Constraint
2682 t2 : Constraint
2683 (PRED2) ---------------------
2684 t1 => t2 : Constraint
2685
2686 ty : TYPE rep
2687 `a` is not free in rep
2688 (FORALL1) -----------------------
2689 forall a. ty : TYPE rep
2690
2691 ty : Constraint
2692 (FORALL2) -------------------------
2693 forall a. ty : Constraint
2694
2695 Note that:
2696 * The only way we distinguish '->' from '=>' is by the fact
2697 that the argument is a PredTy. Both are FunTys
2698 -}
2699
2700 -----------------------------
2701 typeKind :: HasDebugCallStack => Type -> Kind
2702 typeKind (TyConApp tc tys) = piResultTys (tyConKind tc) tys
2703 typeKind (LitTy l) = typeLiteralKind l
2704 typeKind (FunTy {}) = liftedTypeKind
2705 typeKind (TyVarTy tyvar) = tyVarKind tyvar
2706 typeKind (CastTy _ty co) = pSnd $ coercionKind co
2707 typeKind (CoercionTy co) = coercionType co
2708
2709 typeKind (AppTy fun arg)
2710 = go fun [arg]
2711 where
2712 -- Accumulate the type arugments, so we can call piResultTys,
2713 -- rather than a succession of calls to piResultTy (which is
2714 -- asymptotically costly as the number of arguments increases)
2715 go (AppTy fun arg) args = go fun (arg:args)
2716 go fun args = piResultTys (typeKind fun) args
2717
2718 typeKind ty@(ForAllTy {})
2719 = case occCheckExpand tvs body_kind of -- We must make sure tv does not occur in kind
2720 Just k' -> k' -- As it is already out of scope!
2721 Nothing -> pprPanic "typeKind"
2722 (ppr ty $$ ppr tvs $$ ppr body <+> dcolon <+> ppr body_kind)
2723 where
2724 (tvs, body) = splitTyVarForAllTys ty
2725 body_kind = typeKind body
2726
2727 -----------------------------
2728 tcTypeKind :: HasDebugCallStack => Type -> Kind
2729 tcTypeKind (TyConApp tc tys) = piResultTys (tyConKind tc) tys
2730 tcTypeKind (LitTy l) = typeLiteralKind l
2731 tcTypeKind (TyVarTy tyvar) = tyVarKind tyvar
2732 tcTypeKind (CastTy _ty co) = pSnd $ coercionKind co
2733 tcTypeKind (CoercionTy co) = coercionType co
2734
2735 tcTypeKind (FunTy arg res)
2736 | isPredTy arg && isPredTy res = constraintKind
2737 | otherwise = liftedTypeKind
2738
2739 tcTypeKind (AppTy fun arg)
2740 = go fun [arg]
2741 where
2742 -- Accumulate the type arugments, so we can call piResultTys,
2743 -- rather than a succession of calls to piResultTy (which is
2744 -- asymptotically costly as the number of arguments increases)
2745 go (AppTy fun arg) args = go fun (arg:args)
2746 go fun args = piResultTys (tcTypeKind fun) args
2747
2748 tcTypeKind ty@(ForAllTy {})
2749 | tcIsConstraintKind body_kind
2750 = constraintKind
2751
2752 | otherwise
2753 = case occCheckExpand tvs body_kind of -- We must make sure tv does not occur in kind
2754 Just k' -> k' -- As it is already out of scope!
2755 Nothing -> pprPanic "tcTypeKind"
2756 (ppr ty $$ ppr tvs $$ ppr body <+> dcolon <+> ppr body_kind)
2757 where
2758 (tvs, body) = splitTyVarForAllTys ty
2759 body_kind = tcTypeKind body
2760
2761
2762 isPredTy :: Type -> Bool
2763 -- See Note [Types for coercions, predicates, and evidence]
2764 isPredTy ty = tcIsConstraintKind (tcTypeKind ty)
2765
2766 --------------------------
2767 typeLiteralKind :: TyLit -> Kind
2768 typeLiteralKind l =
2769 case l of
2770 NumTyLit _ -> typeNatKind
2771 StrTyLit _ -> typeSymbolKind
2772
2773 -- | Returns True if a type is levity polymorphic. Should be the same
2774 -- as (isKindLevPoly . typeKind) but much faster.
2775 -- Precondition: The type has kind (TYPE blah)
2776 isTypeLevPoly :: Type -> Bool
2777 isTypeLevPoly = go
2778 where
2779 go ty@(TyVarTy {}) = check_kind ty
2780 go ty@(AppTy {}) = check_kind ty
2781 go ty@(TyConApp tc _) | not (isTcLevPoly tc) = False
2782 | otherwise = check_kind ty
2783 go (ForAllTy _ ty) = go ty
2784 go (FunTy {}) = False
2785 go (LitTy {}) = False
2786 go ty@(CastTy {}) = check_kind ty
2787 go ty@(CoercionTy {}) = pprPanic "isTypeLevPoly co" (ppr ty)
2788
2789 check_kind = isKindLevPoly . typeKind
2790
2791 -- | Looking past all pi-types, is the end result potentially levity polymorphic?
2792 -- Example: True for (forall r (a :: TYPE r). String -> a)
2793 -- Example: False for (forall r1 r2 (a :: TYPE r1) (b :: TYPE r2). a -> b -> Type)
2794 resultIsLevPoly :: Type -> Bool
2795 resultIsLevPoly = isTypeLevPoly . snd . splitPiTys
2796
2797
2798 {- **********************************************************************
2799 * *
2800 Occurs check expansion
2801 %* *
2802 %********************************************************************* -}
2803
2804 {- Note [Occurs check expansion]
2805 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2806 (occurCheckExpand tv xi) expands synonyms in xi just enough to get rid
2807 of occurrences of tv outside type function arguments, if that is
2808 possible; otherwise, it returns Nothing.
2809
2810 For example, suppose we have
2811 type F a b = [a]
2812 Then
2813 occCheckExpand b (F Int b) = Just [Int]
2814 but
2815 occCheckExpand a (F a Int) = Nothing
2816
2817 We don't promise to do the absolute minimum amount of expanding
2818 necessary, but we try not to do expansions we don't need to. We
2819 prefer doing inner expansions first. For example,
2820 type F a b = (a, Int, a, [a])
2821 type G b = Char
2822 We have
2823 occCheckExpand b (F (G b)) = Just (F Char)
2824 even though we could also expand F to get rid of b.
2825 -}
2826
2827 occCheckExpand :: [Var] -> Type -> Maybe Type
2828 -- See Note [Occurs check expansion]
2829 -- We may have needed to do some type synonym unfolding in order to
2830 -- get rid of the variable (or forall), so we also return the unfolded
2831 -- version of the type, which is guaranteed to be syntactically free
2832 -- of the given type variable. If the type is already syntactically
2833 -- free of the variable, then the same type is returned.
2834 occCheckExpand vs_to_avoid ty
2835 = go (mkVarSet vs_to_avoid, emptyVarEnv) ty
2836 where
2837 go :: (VarSet, VarEnv TyCoVar) -> Type -> Maybe Type
2838 -- The VarSet is the set of variables we are trying to avoid
2839 -- The VarEnv carries mappings necessary
2840 -- because of kind expansion
2841 go cxt@(as, env) (TyVarTy tv')
2842 | tv' `elemVarSet` as = Nothing
2843 | Just tv'' <- lookupVarEnv env tv' = return (mkTyVarTy tv'')
2844 | otherwise = do { tv'' <- go_var cxt tv'
2845 ; return (mkTyVarTy tv'') }
2846
2847 go _ ty@(LitTy {}) = return ty
2848 go cxt (AppTy ty1 ty2) = do { ty1' <- go cxt ty1
2849 ; ty2' <- go cxt ty2
2850 ; return (mkAppTy ty1' ty2') }
2851 go cxt (FunTy ty1 ty2) = do { ty1' <- go cxt ty1
2852 ; ty2' <- go cxt ty2
2853 ; return (mkFunTy ty1' ty2') }
2854 go cxt@(as, env) (ForAllTy (Bndr tv vis) body_ty)
2855 = do { ki' <- go cxt (varType tv)
2856 ; let tv' = setVarType tv ki'
2857 env' = extendVarEnv env tv tv'
2858 as' = as `delVarSet` tv
2859 ; body' <- go (as', env') body_ty
2860 ; return (ForAllTy (Bndr tv' vis) body') }
2861
2862 -- For a type constructor application, first try expanding away the
2863 -- offending variable from the arguments. If that doesn't work, next
2864 -- see if the type constructor is a type synonym, and if so, expand
2865 -- it and try again.
2866 go cxt ty@(TyConApp tc tys)
2867 = case mapM (go cxt) tys of
2868 Just tys' -> return (mkTyConApp tc tys')
2869 Nothing | Just ty' <- tcView ty -> go cxt ty'
2870 | otherwise -> Nothing
2871 -- Failing that, try to expand a synonym
2872
2873 go cxt (CastTy ty co) = do { ty' <- go cxt ty
2874 ; co' <- go_co cxt co
2875 ; return (mkCastTy ty' co') }
2876 go cxt (CoercionTy co) = do { co' <- go_co cxt co
2877 ; return (mkCoercionTy co') }
2878
2879 ------------------
2880 go_var cxt v = do { k' <- go cxt (varType v)
2881 ; return (setVarType v k') }
2882 -- Works for TyVar and CoVar
2883 -- See Note [Occurrence checking: look inside kinds]
2884
2885 ------------------
2886 go_mco _ MRefl = return MRefl
2887 go_mco ctx (MCo co) = MCo <$> go_co ctx co
2888
2889 ------------------
2890 go_co cxt (Refl ty) = do { ty' <- go cxt ty
2891 ; return (mkNomReflCo ty') }
2892 go_co cxt (GRefl r ty mco) = do { mco' <- go_mco cxt mco
2893 ; ty' <- go cxt ty
2894 ; return (mkGReflCo r ty' mco') }
2895 -- Note: Coercions do not contain type synonyms
2896 go_co cxt (TyConAppCo r tc args) = do { args' <- mapM (go_co cxt) args
2897 ; return (mkTyConAppCo r tc args') }
2898 go_co cxt (AppCo co arg) = do { co' <- go_co cxt co
2899 ; arg' <- go_co cxt arg
2900 ; return (mkAppCo co' arg') }
2901 go_co cxt@(as, env) (ForAllCo tv kind_co body_co)
2902 = do { kind_co' <- go_co cxt kind_co
2903 ; let tv' = setVarType tv $
2904 pFst (coercionKind kind_co')
2905 env' = extendVarEnv env tv tv'
2906 as' = as `delVarSet` tv
2907 ; body' <- go_co (as', env') body_co
2908 ; return (ForAllCo tv' kind_co' body') }
2909 go_co cxt (FunCo r co1 co2) = do { co1' <- go_co cxt co1
2910 ; co2' <- go_co cxt co2
2911 ; return (mkFunCo r co1' co2') }
2912 go_co cxt@(as,env) (CoVarCo c)
2913 | c `elemVarSet` as = Nothing
2914 | Just c' <- lookupVarEnv env c = return (mkCoVarCo c')
2915 | otherwise = do { c' <- go_var cxt c
2916 ; return (mkCoVarCo c') }
2917 go_co cxt (HoleCo h) = do { c' <- go_var cxt (ch_co_var h)
2918 ; return (HoleCo (h { ch_co_var = c' })) }
2919 go_co cxt (AxiomInstCo ax ind args) = do { args' <- mapM (go_co cxt) args
2920 ; return (mkAxiomInstCo ax ind args') }
2921 go_co cxt (UnivCo p r ty1 ty2) = do { p' <- go_prov cxt p
2922 ; ty1' <- go cxt ty1
2923 ; ty2' <- go cxt ty2
2924 ; return (mkUnivCo p' r ty1' ty2') }
2925 go_co cxt (SymCo co) = do { co' <- go_co cxt co
2926 ; return (mkSymCo co') }
2927 go_co cxt (TransCo co1 co2) = do { co1' <- go_co cxt co1
2928 ; co2' <- go_co cxt co2
2929 ; return (mkTransCo co1' co2') }
2930 go_co cxt (NthCo r n co) = do { co' <- go_co cxt co
2931 ; return (mkNthCo r n co') }
2932 go_co cxt (LRCo lr co) = do { co' <- go_co cxt co
2933 ; return (mkLRCo lr co') }
2934 go_co cxt (InstCo co arg) = do { co' <- go_co cxt co
2935 ; arg' <- go_co cxt arg
2936 ; return (mkInstCo co' arg') }
2937 go_co cxt (KindCo co) = do { co' <- go_co cxt co
2938 ; return (mkKindCo co') }
2939 go_co cxt (SubCo co) = do { co' <- go_co cxt co
2940 ; return (mkSubCo co') }
2941 go_co cxt (AxiomRuleCo ax cs) = do { cs' <- mapM (go_co cxt) cs
2942 ; return (mkAxiomRuleCo ax cs') }
2943
2944 ------------------
2945 go_prov _ UnsafeCoerceProv = return UnsafeCoerceProv
2946 go_prov cxt (PhantomProv co) = PhantomProv <$> go_co cxt co
2947 go_prov cxt (ProofIrrelProv co) = ProofIrrelProv <$> go_co cxt co
2948 go_prov _ p@(PluginProv _) = return p
2949
2950
2951 {-
2952 %************************************************************************
2953 %* *
2954 Miscellaneous functions
2955 %* *
2956 %************************************************************************
2957
2958 -}
2959 -- | All type constructors occurring in the type; looking through type
2960 -- synonyms, but not newtypes.
2961 -- When it finds a Class, it returns the class TyCon.
2962 tyConsOfType :: Type -> UniqSet TyCon
2963 tyConsOfType ty
2964 = go ty
2965 where
2966 go :: Type -> UniqSet TyCon -- The UniqSet does duplicate elim
2967 go ty | Just ty' <- coreView ty = go ty'
2968 go (TyVarTy {}) = emptyUniqSet
2969 go (LitTy {}) = emptyUniqSet
2970 go (TyConApp tc tys) = go_tc tc `unionUniqSets` go_s tys
2971 go (AppTy a b) = go a `unionUniqSets` go b
2972 go (FunTy a b) = go a `unionUniqSets` go b `unionUniqSets` go_tc funTyCon
2973 go (ForAllTy (Bndr tv _) ty) = go ty `unionUniqSets` go (varType tv)
2974 go (CastTy ty co) = go ty `unionUniqSets` go_co co
2975 go (CoercionTy co) = go_co co
2976
2977 go_co (Refl ty) = go ty
2978 go_co (GRefl _ ty mco) = go ty `unionUniqSets` go_mco mco
2979 go_co (TyConAppCo _ tc args) = go_tc tc `unionUniqSets` go_cos args
2980 go_co (AppCo co arg) = go_co co `unionUniqSets` go_co arg
2981 go_co (ForAllCo _ kind_co co) = go_co kind_co `unionUniqSets` go_co co
2982 go_co (FunCo _ co1 co2) = go_co co1 `unionUniqSets` go_co co2
2983 go_co (AxiomInstCo ax _ args) = go_ax ax `unionUniqSets` go_cos args
2984 go_co (UnivCo p _ t1 t2) = go_prov p `unionUniqSets` go t1 `unionUniqSets` go t2
2985 go_co (CoVarCo {}) = emptyUniqSet
2986 go_co (HoleCo {}) = emptyUniqSet
2987 go_co (SymCo co) = go_co co
2988 go_co (TransCo co1 co2) = go_co co1 `unionUniqSets` go_co co2
2989 go_co (NthCo _ _ co) = go_co co
2990 go_co (LRCo _ co) = go_co co
2991 go_co (InstCo co arg) = go_co co `unionUniqSets` go_co arg
2992 go_co (KindCo co) = go_co co
2993 go_co (SubCo co) = go_co co
2994 go_co (AxiomRuleCo _ cs) = go_cos cs
2995
2996 go_mco MRefl = emptyUniqSet
2997 go_mco (MCo co) = go_co co
2998
2999 go_prov UnsafeCoerceProv = emptyUniqSet
3000 go_prov (PhantomProv co) = go_co co
3001 go_prov (ProofIrrelProv co) = go_co co
3002 go_prov (PluginProv _) = emptyUniqSet
3003 -- this last case can happen from the tyConsOfType used from
3004 -- checkTauTvUpdate
3005
3006 go_s tys = foldr (unionUniqSets . go) emptyUniqSet tys
3007 go_cos cos = foldr (unionUniqSets . go_co) emptyUniqSet cos
3008
3009 go_tc tc = unitUniqSet tc
3010 go_ax ax = go_tc $ coAxiomTyCon ax
3011
3012 -- | Find the result 'Kind' of a type synonym,
3013 -- after applying it to its 'arity' number of type variables
3014 -- Actually this function works fine on data types too,
3015 -- but they'd always return '*', so we never need to ask
3016 synTyConResKind :: TyCon -> Kind
3017 synTyConResKind tycon = piResultTys (tyConKind tycon) (mkTyVarTys (tyConTyVars tycon))
3018
3019 -- | Retrieve the free variables in this type, splitting them based
3020 -- on whether they are used visibly or invisibly. Invisible ones come
3021 -- first.
3022 splitVisVarsOfType :: Type -> Pair TyCoVarSet
3023 splitVisVarsOfType orig_ty = Pair invis_vars vis_vars
3024 where
3025 Pair invis_vars1 vis_vars = go orig_ty
3026 invis_vars = invis_vars1 `minusVarSet` vis_vars
3027
3028 go (TyVarTy tv) = Pair (tyCoVarsOfType $ tyVarKind tv) (unitVarSet tv)
3029 go (AppTy t1 t2) = go t1 `mappend` go t2
3030 go (TyConApp tc tys) = go_tc tc tys
3031 go (FunTy t1 t2) = go t1 `mappend` go t2
3032 go (ForAllTy (Bndr tv _) ty)
3033 = ((`delVarSet` tv) <$> go ty) `mappend`
3034 (invisible (tyCoVarsOfType $ varType tv))
3035 go (LitTy {}) = mempty
3036 go (CastTy ty co) = go ty `mappend` invisible (tyCoVarsOfCo co)
3037 go (CoercionTy co) = invisible $ tyCoVarsOfCo co
3038
3039 invisible vs = Pair vs emptyVarSet
3040
3041 go_tc tc tys = let (invis, vis) = partitionInvisibleTypes tc tys in
3042 invisible (tyCoVarsOfTypes invis) `mappend` foldMap go vis
3043
3044 splitVisVarsOfTypes :: [Type] -> Pair TyCoVarSet
3045 splitVisVarsOfTypes = foldMap splitVisVarsOfType
3046
3047 modifyJoinResTy :: Int -- Number of binders to skip
3048 -> (Type -> Type) -- Function to apply to result type
3049 -> Type -- Type of join point
3050 -> Type -- New type
3051 -- INVARIANT: If any of the first n binders are foralls, those tyvars cannot
3052 -- appear in the original result type. See isValidJoinPointType.
3053 modifyJoinResTy orig_ar f orig_ty
3054 = go orig_ar orig_ty
3055 where
3056 go 0 ty = f ty
3057 go n ty | Just (arg_bndr, res_ty) <- splitPiTy_maybe ty
3058 = mkTyCoPiTy arg_bndr (go (n-1) res_ty)
3059 | otherwise
3060 = pprPanic "modifyJoinResTy" (ppr orig_ar <+> ppr orig_ty)
3061
3062 setJoinResTy :: Int -- Number of binders to skip
3063 -> Type -- New result type
3064 -> Type -- Type of join point
3065 -> Type -- New type
3066 -- INVARIANT: Same as for modifyJoinResTy
3067 setJoinResTy ar new_res_ty ty
3068 = modifyJoinResTy ar (const new_res_ty) ty
3069
3070
3071 {-
3072 %************************************************************************
3073 %* *
3074 Pretty-printing
3075 %* *
3076 %************************************************************************
3077
3078 Most pretty-printing is either in TyCoRep or IfaceType.
3079
3080 -}
3081
3082 -- | This variant preserves any use of TYPE in a type, effectively
3083 -- locally setting -fprint-explicit-runtime-reps.
3084 pprWithTYPE :: Type -> SDoc
3085 pprWithTYPE ty = updSDocDynFlags (flip gopt_set Opt_PrintExplicitRuntimeReps) $
3086 ppr ty