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