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