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