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