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