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