Coercion Quantification
[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,
66 partitionInvisibleTypes, partitionInvisibles,
67 synTyConResKind,
68
69 modifyJoinResTy, setJoinResTy,
70
71 -- Analyzing types
72 TyCoMapper(..), mapType, mapCoercion,
73
74 -- (Newtypes)
75 newTyConInstRhs,
76
77 -- Pred types
78 mkFamilyTyConApp,
79 isDictLikeTy,
80 mkPrimEqPred, mkReprPrimEqPred, mkPrimEqPredRole,
81 equalityTyCon,
82 mkHeteroPrimEqPred, mkHeteroReprPrimEqPred,
83 mkClassPred,
84 isClassPred, isEqPred, isNomEqPred,
85 isIPPred, isIPPred_maybe, isIPTyCon, isIPClass,
86 isCTupleClass,
87
88 -- Deconstructing predicate types
89 PredTree(..), EqRel(..), eqRelRole, classifyPredType,
90 getClassPredTys, getClassPredTys_maybe,
91 getEqPredTys, getEqPredTys_maybe, getEqPredRole,
92 predTypeEqRel,
93
94 -- ** Binders
95 sameVis,
96 mkTyCoVarBinder, mkTyCoVarBinders,
97 mkTyVarBinders,
98 mkAnonBinder,
99 isAnonTyCoBinder, isNamedTyCoBinder,
100 binderVar, binderVars, binderType, binderArgFlag,
101 tyCoBinderType, tyCoBinderVar_maybe,
102 tyBinderType,
103 binderRelevantType_maybe, caseBinder,
104 isVisibleArgFlag, isInvisibleArgFlag, isVisibleBinder, isInvisibleBinder,
105 tyConBindersTyCoBinders,
106
107 -- ** Common type constructors
108 funTyCon,
109
110 -- ** Predicates on types
111 isTyVarTy, isFunTy, isDictTy, isPredTy, isCoercionTy,
112 isCoercionTy_maybe, isCoercionType, isForAllTy,
113 isForAllTy_ty, isForAllTy_co,
114 isPiTy, isTauTy, isFamFreeTy,
115
116 isValidJoinPointType,
117
118 -- (Lifting and boxity)
119 isLiftedType_maybe, isUnliftedType, isUnboxedTupleType, isUnboxedSumType,
120 isAlgType, isDataFamilyAppType,
121 isPrimitiveType, isStrictType,
122 isRuntimeRepTy, isRuntimeRepVar, isRuntimeRepKindedTy,
123 dropRuntimeRepArgs,
124 getRuntimeRep, getRuntimeRepFromKind,
125
126 -- * Main data types representing Kinds
127 Kind,
128
129 -- ** Finding the kind of a type
130 typeKind, isTypeLevPoly, resultIsLevPoly,
131 tcIsLiftedTypeKind, tcIsConstraintKind, tcReturnsConstraintKind,
132
133 -- ** Common Kind
134 liftedTypeKind,
135
136 -- * Type free variables
137 tyCoFVsOfType, tyCoFVsBndr,
138 tyCoVarsOfType, tyCoVarsOfTypes,
139 tyCoVarsOfTypeDSet,
140 coVarsOfType,
141 coVarsOfTypes, closeOverKinds, closeOverKindsList,
142 noFreeVarsOfType,
143 splitVisVarsOfType, splitVisVarsOfTypes,
144 expandTypeSynonyms,
145 typeSize, occCheckExpand,
146
147 -- * Well-scoped lists of variables
148 dVarSetElemsWellScoped, toposortTyVars, tyCoVarsOfTypeWellScoped,
149 tyCoVarsOfTypesWellScoped,
150
151 -- * Type comparison
152 eqType, eqTypeX, eqTypes, nonDetCmpType, nonDetCmpTypes, nonDetCmpTypeX,
153 nonDetCmpTypesX, nonDetCmpTc,
154 eqVarBndrs,
155
156 -- * Forcing evaluation of types
157 seqType, seqTypes,
158
159 -- * Other views onto Types
160 coreView, tcView,
161
162 tyConsOfType,
163
164 -- * Main type substitution data types
165 TvSubstEnv, -- Representation widely visible
166 TCvSubst(..), -- Representation visible to a few friends
167
168 -- ** Manipulating type substitutions
169 emptyTvSubstEnv, emptyTCvSubst, mkEmptyTCvSubst,
170
171 mkTCvSubst, zipTvSubst, mkTvSubstPrs,
172 zipTCvSubst,
173 notElemTCvSubst,
174 getTvSubstEnv, setTvSubstEnv,
175 zapTCvSubst, getTCvInScope, getTCvSubstRangeFVs,
176 extendTCvInScope, extendTCvInScopeList, extendTCvInScopeSet,
177 extendTCvSubst, extendCvSubst,
178 extendTvSubst, extendTvSubstBinderAndInScope,
179 extendTvSubstList, extendTvSubstAndInScope,
180 extendTCvSubstList,
181 extendTvSubstWithClone,
182 extendTCvSubstWithClone,
183 isInScope, composeTCvSubstEnv, composeTCvSubst, zipTyEnv, zipCoEnv,
184 isEmptyTCvSubst, unionTCvSubst,
185
186 -- ** Performing substitution on types and kinds
187 substTy, substTys, substTyWith, substTysWith, substTheta,
188 substTyAddInScope,
189 substTyUnchecked, substTysUnchecked, substThetaUnchecked,
190 substTyWithUnchecked,
191 substCoUnchecked, substCoWithUnchecked,
192 substTyVarBndr, substTyVarBndrs, substTyVar, substTyVars,
193 substVarBndr, substVarBndrs,
194 cloneTyVarBndr, cloneTyVarBndrs, lookupTyVar,
195
196 -- * Pretty-printing
197 pprType, pprParendType, pprPrecType,
198 pprTypeApp, pprTyThingCategory, pprShortTyThing,
199 pprTCvBndr, pprTCvBndrs, pprForAll, pprUserForAll,
200 pprSigmaType, ppSuggestExplicitKinds,
201 pprTheta, pprThetaArrowTy, pprClassPred,
202 pprKind, pprParendKind, pprSourceTyCon,
203 PprPrec(..), topPrec, sigPrec, opPrec, funPrec, appPrec, maybeParen,
204 pprTyVar, pprTyVars,
205 pprWithTYPE,
206
207 -- * Tidying type related things up for printing
208 tidyType, tidyTypes,
209 tidyOpenType, tidyOpenTypes,
210 tidyOpenKind,
211 tidyVarBndr, tidyVarBndrs, tidyFreeTyCoVars,
212 tidyOpenTyCoVar, tidyOpenTyCoVars,
213 tidyTyCoVarOcc,
214 tidyTopType,
215 tidyKind,
216 tidyTyCoVarBinder, tidyTyCoVarBinders
217 ) where
218
219 #include "HsVersions.h"
220
221 import GhcPrelude
222
223 import BasicTypes
224
225 -- We import the representation and primitive functions from TyCoRep.
226 -- Many things are reexported, but not the representation!
227
228 import Kind
229 import TyCoRep
230
231 -- friends:
232 import Var
233 import VarEnv
234 import VarSet
235 import UniqSet
236
237 import Class
238 import TyCon
239 import TysPrim
240 import {-# SOURCE #-} TysWiredIn ( listTyCon, typeNatKind
241 , typeSymbolKind, liftedTypeKind )
242 import PrelNames
243 import CoAxiom
244 import {-# SOURCE #-} Coercion( mkNomReflCo, mkGReflCo, mkReflCo
245 , mkTyConAppCo, mkAppCo, mkCoVarCo, mkAxiomRuleCo
246 , mkForAllCo, mkFunCo, mkAxiomInstCo, mkUnivCo
247 , mkSymCo, mkTransCo, mkNthCo, mkLRCo, mkInstCo
248 , mkKindCo, mkSubCo, mkFunCo, mkAxiomInstCo
249 , decomposePiCos, coercionKind, coercionType
250 , isReflexiveCo, seqCo )
251
252 -- others
253 import Util
254 import Outputable
255 import FastString
256 import Pair
257 import DynFlags ( gopt_set, GeneralFlag(Opt_PrintExplicitRuntimeReps) )
258 import ListSetOps
259 import Digraph
260 import Unique ( nonDetCmpUnique )
261
262 import Maybes ( orElse )
263 import Data.Maybe ( isJust, mapMaybe )
264 import Control.Monad ( guard )
265 import Control.Arrow ( first, second )
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 its arguments, filters out any invisible arguments
1548 filterOutInvisibleTypes :: TyCon -> [Type] -> [Type]
1549 filterOutInvisibleTypes tc tys = snd $ partitionInvisibleTypes tc tys
1550
1551 -- | Given a 'TyCon' and its arguments, partition the arguments into
1552 -- (invisible arguments, visible arguments).
1553 partitionInvisibleTypes :: TyCon -> [Type] -> ([Type], [Type])
1554 partitionInvisibleTypes tc tys = partitionInvisibles tc id tys
1555
1556 -- | Given a tycon and a list of things (which correspond to arguments),
1557 -- partitions the things into
1558 -- Inferred or Specified ones and
1559 -- Required ones
1560 -- The callback function is necessary for this scenario:
1561 --
1562 -- > T :: forall k. k -> k
1563 -- > partitionInvisibles T [forall m. m -> m -> m, S, R, Q]
1564 --
1565 -- After substituting, we get
1566 --
1567 -- > T (forall m. m -> m -> m) :: (forall m. m -> m -> m) -> forall n. n -> n -> n
1568 --
1569 -- Thus, the first argument is invisible, @S@ is visible, @R@ is invisible again,
1570 -- and @Q@ is visible.
1571 --
1572 -- If you're absolutely sure that your tycon's kind doesn't end in a variable,
1573 -- it's OK if the callback function panics, as that's the only time it's
1574 -- consulted.
1575 partitionInvisibles :: TyCon -> (a -> Type) -> [a] -> ([a], [a])
1576 partitionInvisibles tc get_ty = go emptyTCvSubst (tyConKind tc)
1577 where
1578 go _ _ [] = ([], [])
1579 go subst (ForAllTy (Bndr tv vis) res_ki) (x:xs)
1580 | isVisibleArgFlag vis = second (x :) (go subst' res_ki xs)
1581 | otherwise = first (x :) (go subst' res_ki xs)
1582 where
1583 subst' = extendTCvSubst subst tv (get_ty x)
1584 go subst (TyVarTy tv) xs
1585 | Just ki <- lookupTyVar subst tv = go subst ki xs
1586 go _ _ xs = ([], xs) -- something is ill-kinded. But this can happen
1587 -- when printing errors. Assume everything is visible.
1588
1589 -- @isTauTy@ tests if a type has no foralls
1590 isTauTy :: Type -> Bool
1591 isTauTy ty | Just ty' <- coreView ty = isTauTy ty'
1592 isTauTy (TyVarTy _) = True
1593 isTauTy (LitTy {}) = True
1594 isTauTy (TyConApp tc tys) = all isTauTy tys && isTauTyCon tc
1595 isTauTy (AppTy a b) = isTauTy a && isTauTy b
1596 isTauTy (FunTy a b) = isTauTy a && isTauTy b
1597 isTauTy (ForAllTy {}) = False
1598 isTauTy (CastTy ty _) = isTauTy ty
1599 isTauTy (CoercionTy _) = False -- Not sure about this
1600
1601 {-
1602 %************************************************************************
1603 %* *
1604 TyCoBinders
1605 %* *
1606 %************************************************************************
1607 -}
1608
1609 -- | Make an anonymous binder
1610 mkAnonBinder :: Type -> TyCoBinder
1611 mkAnonBinder = Anon
1612
1613 -- | Does this binder bind a variable that is /not/ erased? Returns
1614 -- 'True' for anonymous binders.
1615 isAnonTyCoBinder :: TyCoBinder -> Bool
1616 isAnonTyCoBinder (Named {}) = False
1617 isAnonTyCoBinder (Anon {}) = True
1618
1619 isNamedTyCoBinder :: TyCoBinder -> Bool
1620 isNamedTyCoBinder (Named {}) = True
1621 isNamedTyCoBinder (Anon {}) = False
1622
1623 tyCoBinderVar_maybe :: TyCoBinder -> Maybe TyCoVar
1624 tyCoBinderVar_maybe (Named tv) = Just $ binderVar tv
1625 tyCoBinderVar_maybe _ = Nothing
1626
1627 tyCoBinderType :: TyCoBinder -> Type
1628 -- Barely used
1629 tyCoBinderType (Named tvb) = binderType tvb
1630 tyCoBinderType (Anon ty) = ty
1631
1632 tyBinderType :: TyBinder -> Type
1633 tyBinderType (Named (Bndr tv _))
1634 = ASSERT( isTyVar tv )
1635 tyVarKind tv
1636 tyBinderType (Anon ty) = ty
1637
1638 -- | Extract a relevant type, if there is one.
1639 binderRelevantType_maybe :: TyCoBinder -> Maybe Type
1640 binderRelevantType_maybe (Named {}) = Nothing
1641 binderRelevantType_maybe (Anon ty) = Just ty
1642
1643 -- | Like 'maybe', but for binders.
1644 caseBinder :: TyCoBinder -- ^ binder to scrutinize
1645 -> (TyCoVarBinder -> a) -- ^ named case
1646 -> (Type -> a) -- ^ anonymous case
1647 -> a
1648 caseBinder (Named v) f _ = f v
1649 caseBinder (Anon t) _ d = d t
1650
1651
1652 {-
1653 %************************************************************************
1654 %* *
1655 Pred
1656 * *
1657 ************************************************************************
1658
1659 Predicates on PredType
1660
1661 Note [isPredTy complications]
1662 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1663 You would think that we could define
1664 isPredTy ty = isConstraintKind (typeKind ty)
1665 But there are a number of complications:
1666
1667 * isPredTy is used when printing types, which can happen in debug
1668 printing during type checking of not-fully-zonked types. So it's
1669 not cool to say isConstraintKind (typeKind ty) because, absent
1670 zonking, the type might be ill-kinded, and typeKind crashes. Hence the
1671 rather tiresome story here
1672
1673 * isPredTy must return "True" to *unlifted* coercions, such as (t1 ~# t2)
1674 and (t1 ~R# t2), which are not of kind Constraint! Currently they are
1675 of kind #.
1676
1677 * If we do form the type '(C a => C [a]) => blah', then we'd like to
1678 print it as such. But that means that isPredTy must return True for
1679 (C a => C [a]). Admittedly that type is illegal in Haskell, but we
1680 want to print it nicely in error messages.
1681 -}
1682
1683 -- | Split a type constructor application into its type constructor and
1684 -- applied types. Note that this may fail in the case of a 'FunTy' with an
1685 -- argument of unknown kind 'FunTy' (e.g. @FunTy (a :: k) Int@. since the kind
1686 -- of @a@ isn't of the form @TYPE rep@). Consequently, you may need to zonk your
1687 -- type before using this function.
1688 --
1689 -- If you only need the 'TyCon', consider using 'tcTyConAppTyCon_maybe'.
1690 tcSplitTyConApp_maybe :: HasCallStack => Type -> Maybe (TyCon, [Type])
1691 -- Defined here to avoid module loops between Unify and TcType.
1692 tcSplitTyConApp_maybe ty | Just ty' <- tcView ty = tcSplitTyConApp_maybe ty'
1693 tcSplitTyConApp_maybe ty = tcRepSplitTyConApp_maybe ty
1694
1695 -- tcIsConstraintKind stuf only makes sense in the typechecker
1696 -- After that Constraint = Type
1697 -- See Note [coreView vs tcView]
1698 -- Defined here because it is used in isPredTy and tcRepSplitAppTy_maybe (sigh)
1699 tcIsConstraintKind :: Kind -> Bool
1700 tcIsConstraintKind ty
1701 | Just (tc, args) <- tcSplitTyConApp_maybe ty -- Note: tcSplit here
1702 , isConstraintKindCon tc
1703 = ASSERT2( null args, ppr ty ) True
1704
1705 | otherwise
1706 = False
1707
1708 -- | Is this kind equivalent to @*@?
1709 --
1710 -- This considers 'Constraint' to be distinct from @*@. For a version that
1711 -- treats them as the same type, see 'isLiftedTypeKind'.
1712 tcIsLiftedTypeKind :: Kind -> Bool
1713 tcIsLiftedTypeKind ty
1714 | Just (type_tc, [arg]) <- tcSplitTyConApp_maybe ty
1715 , type_tc `hasKey` tYPETyConKey
1716 , Just (lifted_rep_tc, args) <- tcSplitTyConApp_maybe arg
1717 , lifted_rep_tc `hasKey` liftedRepDataConKey
1718 = ASSERT2( null args, ppr ty ) True
1719 | otherwise
1720 = False
1721
1722 tcReturnsConstraintKind :: Kind -> Bool
1723 -- True <=> the Kind ultimately returns a Constraint
1724 -- E.g. * -> Constraint
1725 -- forall k. k -> Constraint
1726 tcReturnsConstraintKind kind
1727 | Just kind' <- tcView kind = tcReturnsConstraintKind kind'
1728 tcReturnsConstraintKind (ForAllTy _ ty) = tcReturnsConstraintKind ty
1729 tcReturnsConstraintKind (FunTy _ ty) = tcReturnsConstraintKind ty
1730 tcReturnsConstraintKind (TyConApp tc _) = isConstraintKindCon tc
1731 tcReturnsConstraintKind _ = False
1732
1733 -- | Is the type suitable to classify a given/wanted in the typechecker?
1734 isPredTy :: Type -> Bool
1735 -- See Note [isPredTy complications]
1736 isPredTy ty = go ty []
1737 where
1738 go :: Type -> [KindOrType] -> Bool
1739 go (AppTy ty1 ty2) args = go ty1 (ty2 : args)
1740 go (TyVarTy tv) args = go_k (tyVarKind tv) args
1741 go (TyConApp tc tys) args = ASSERT( null args ) -- TyConApp invariant
1742 go_tc tc tys
1743 go (FunTy arg res) []
1744 | isPredTy arg = isPredTy res -- (Eq a => C a)
1745 | otherwise = False -- (Int -> Bool)
1746 go (ForAllTy _ ty) [] = go ty []
1747 go (CastTy _ co) args = go_k (pSnd (coercionKind co)) args
1748 go _ _ = False
1749
1750 go_tc :: TyCon -> [KindOrType] -> Bool
1751 go_tc tc args
1752 | tc `hasKey` eqPrimTyConKey || tc `hasKey` eqReprPrimTyConKey
1753 = args `lengthIs` 4 -- ~# and ~R# sadly have result kind #
1754 -- not Constraint; but we still want
1755 -- isPredTy to reply True.
1756 | otherwise = go_k (tyConKind tc) args
1757
1758 go_k :: Kind -> [KindOrType] -> Bool
1759 -- True <=> ('k' applied to 'kts') = Constraint
1760 go_k k [] = tcIsConstraintKind k
1761 go_k k (arg:args) = case piResultTy_maybe k arg of
1762 Just k' -> go_k k' args
1763 Nothing -> WARN( True, text "isPredTy" <+> ppr ty )
1764 False
1765 -- This last case shouldn't happen under most circumstances. It can
1766 -- occur if we call isPredTy during kind checking, especially if one
1767 -- of the following happens:
1768 --
1769 -- 1. There is actually a kind error. Example in which this showed up:
1770 -- polykinds/T11399
1771 --
1772 -- 2. A type constructor application appears to be oversaturated. An
1773 -- example of this occurred in GHC Trac #13187:
1774 --
1775 -- {-# LANGUAGE PolyKinds #-}
1776 -- type Const a b = b
1777 -- f :: Const Int (,) Bool Char -> Char
1778 --
1779 -- We call isPredTy (Const k1 k2 Int (,) Bool Char
1780 -- where k1,k2 are unification variables that have been
1781 -- unified to *, and (*->*->*) resp, /but not zonked/.
1782 -- This shows that isPredTy can report a false negative
1783 -- if a constraint is similarly oversaturated, but
1784 -- it's hard to do better than isPredTy currently does without
1785 -- zonking, so we punt on such cases for now. This only happens
1786 -- during debug-printing, so it doesn't matter.
1787
1788 isClassPred, isEqPred, isNomEqPred, isIPPred :: PredType -> Bool
1789 isClassPred ty = case tyConAppTyCon_maybe ty of
1790 Just tyCon | isClassTyCon tyCon -> True
1791 _ -> False
1792 isEqPred ty = case tyConAppTyCon_maybe ty of
1793 Just tyCon -> tyCon `hasKey` eqPrimTyConKey
1794 || tyCon `hasKey` eqReprPrimTyConKey
1795 _ -> False
1796
1797 isNomEqPred ty = case tyConAppTyCon_maybe ty of
1798 Just tyCon -> tyCon `hasKey` eqPrimTyConKey
1799 _ -> False
1800
1801 isIPPred ty = case tyConAppTyCon_maybe ty of
1802 Just tc -> isIPTyCon tc
1803 _ -> False
1804
1805 isIPTyCon :: TyCon -> Bool
1806 isIPTyCon tc = tc `hasKey` ipClassKey
1807 -- Class and its corresponding TyCon have the same Unique
1808
1809 isIPClass :: Class -> Bool
1810 isIPClass cls = cls `hasKey` ipClassKey
1811
1812 isCTupleClass :: Class -> Bool
1813 isCTupleClass cls = isTupleTyCon (classTyCon cls)
1814
1815 isIPPred_maybe :: Type -> Maybe (FastString, Type)
1816 isIPPred_maybe ty =
1817 do (tc,[t1,t2]) <- splitTyConApp_maybe ty
1818 guard (isIPTyCon tc)
1819 x <- isStrLitTy t1
1820 return (x,t2)
1821
1822 {-
1823 Make PredTypes
1824
1825 --------------------- Equality types ---------------------------------
1826 -}
1827
1828 -- | Makes a lifted equality predicate at the given role
1829 mkPrimEqPredRole :: Role -> Type -> Type -> PredType
1830 mkPrimEqPredRole Nominal = mkPrimEqPred
1831 mkPrimEqPredRole Representational = mkReprPrimEqPred
1832 mkPrimEqPredRole Phantom = panic "mkPrimEqPredRole phantom"
1833
1834 -- | Creates a primitive type equality predicate.
1835 -- Invariant: the types are not Coercions
1836 mkPrimEqPred :: Type -> Type -> Type
1837 mkPrimEqPred ty1 ty2
1838 = TyConApp eqPrimTyCon [k1, k2, ty1, ty2]
1839 where
1840 k1 = typeKind ty1
1841 k2 = typeKind ty2
1842
1843 -- | Creates a primite type equality predicate with explicit kinds
1844 mkHeteroPrimEqPred :: Kind -> Kind -> Type -> Type -> Type
1845 mkHeteroPrimEqPred k1 k2 ty1 ty2 = TyConApp eqPrimTyCon [k1, k2, ty1, ty2]
1846
1847 -- | Creates a primitive representational type equality predicate
1848 -- with explicit kinds
1849 mkHeteroReprPrimEqPred :: Kind -> Kind -> Type -> Type -> Type
1850 mkHeteroReprPrimEqPred k1 k2 ty1 ty2
1851 = TyConApp eqReprPrimTyCon [k1, k2, ty1, ty2]
1852
1853 -- | Try to split up a coercion type into the types that it coerces
1854 splitCoercionType_maybe :: Type -> Maybe (Type, Type)
1855 splitCoercionType_maybe ty
1856 = do { (tc, [_, _, ty1, ty2]) <- splitTyConApp_maybe ty
1857 ; guard $ tc `hasKey` eqPrimTyConKey || tc `hasKey` eqReprPrimTyConKey
1858 ; return (ty1, ty2) }
1859
1860 mkReprPrimEqPred :: Type -> Type -> Type
1861 mkReprPrimEqPred ty1 ty2
1862 = TyConApp eqReprPrimTyCon [k1, k2, ty1, ty2]
1863 where
1864 k1 = typeKind ty1
1865 k2 = typeKind ty2
1866
1867 equalityTyCon :: Role -> TyCon
1868 equalityTyCon Nominal = eqPrimTyCon
1869 equalityTyCon Representational = eqReprPrimTyCon
1870 equalityTyCon Phantom = eqPhantPrimTyCon
1871
1872 -- --------------------- Dictionary types ---------------------------------
1873
1874 mkClassPred :: Class -> [Type] -> PredType
1875 mkClassPred clas tys = TyConApp (classTyCon clas) tys
1876
1877 isDictTy :: Type -> Bool
1878 isDictTy = isClassPred
1879
1880 isDictLikeTy :: Type -> Bool
1881 -- Note [Dictionary-like types]
1882 isDictLikeTy ty | Just ty' <- coreView ty = isDictLikeTy ty'
1883 isDictLikeTy ty = case splitTyConApp_maybe ty of
1884 Just (tc, tys) | isClassTyCon tc -> True
1885 | isTupleTyCon tc -> all isDictLikeTy tys
1886 _other -> False
1887
1888 {-
1889 Note [Dictionary-like types]
1890 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1891 Being "dictionary-like" means either a dictionary type or a tuple thereof.
1892 In GHC 6.10 we build implication constraints which construct such tuples,
1893 and if we land up with a binding
1894 t :: (C [a], Eq [a])
1895 t = blah
1896 then we want to treat t as cheap under "-fdicts-cheap" for example.
1897 (Implication constraints are normally inlined, but sadly not if the
1898 occurrence is itself inside an INLINE function! Until we revise the
1899 handling of implication constraints, that is.) This turned out to
1900 be important in getting good arities in DPH code. Example:
1901
1902 class C a
1903 class D a where { foo :: a -> a }
1904 instance C a => D (Maybe a) where { foo x = x }
1905
1906 bar :: (C a, C b) => a -> b -> (Maybe a, Maybe b)
1907 {-# INLINE bar #-}
1908 bar x y = (foo (Just x), foo (Just y))
1909
1910 Then 'bar' should jolly well have arity 4 (two dicts, two args), but
1911 we ended up with something like
1912 bar = __inline_me__ (\d1,d2. let t :: (D (Maybe a), D (Maybe b)) = ...
1913 in \x,y. <blah>)
1914
1915 This is all a bit ad-hoc; eg it relies on knowing that implication
1916 constraints build tuples.
1917
1918
1919 Decomposing PredType
1920 -}
1921
1922 -- | A choice of equality relation. This is separate from the type 'Role'
1923 -- because 'Phantom' does not define a (non-trivial) equality relation.
1924 data EqRel = NomEq | ReprEq
1925 deriving (Eq, Ord)
1926
1927 instance Outputable EqRel where
1928 ppr NomEq = text "nominal equality"
1929 ppr ReprEq = text "representational equality"
1930
1931 eqRelRole :: EqRel -> Role
1932 eqRelRole NomEq = Nominal
1933 eqRelRole ReprEq = Representational
1934
1935 data PredTree
1936 = ClassPred Class [Type]
1937 | EqPred EqRel Type Type
1938 | IrredPred PredType
1939 | ForAllPred [TyCoVarBinder] [PredType] PredType
1940 -- ForAllPred: see Note [Quantified constraints] in TcCanonical
1941 -- NB: There is no TuplePred case
1942 -- Tuple predicates like (Eq a, Ord b) are just treated
1943 -- as ClassPred, as if we had a tuple class with two superclasses
1944 -- class (c1, c2) => (%,%) c1 c2
1945
1946 classifyPredType :: PredType -> PredTree
1947 classifyPredType ev_ty = case splitTyConApp_maybe ev_ty of
1948 Just (tc, [_, _, ty1, ty2])
1949 | tc `hasKey` eqReprPrimTyConKey -> EqPred ReprEq ty1 ty2
1950 | tc `hasKey` eqPrimTyConKey -> EqPred NomEq ty1 ty2
1951
1952 Just (tc, tys)
1953 | Just clas <- tyConClass_maybe tc
1954 -> ClassPred clas tys
1955
1956 _ | (tvs, rho) <- splitForAllVarBndrs ev_ty
1957 , (theta, pred) <- splitFunTys rho
1958 , not (null tvs && null theta)
1959 -> ForAllPred tvs theta pred
1960
1961 | otherwise
1962 -> IrredPred ev_ty
1963
1964 getClassPredTys :: HasDebugCallStack => PredType -> (Class, [Type])
1965 getClassPredTys ty = case getClassPredTys_maybe ty of
1966 Just (clas, tys) -> (clas, tys)
1967 Nothing -> pprPanic "getClassPredTys" (ppr ty)
1968
1969 getClassPredTys_maybe :: PredType -> Maybe (Class, [Type])
1970 getClassPredTys_maybe ty = case splitTyConApp_maybe ty of
1971 Just (tc, tys) | Just clas <- tyConClass_maybe tc -> Just (clas, tys)
1972 _ -> Nothing
1973
1974 getEqPredTys :: PredType -> (Type, Type)
1975 getEqPredTys ty
1976 = case splitTyConApp_maybe ty of
1977 Just (tc, [_, _, ty1, ty2])
1978 | tc `hasKey` eqPrimTyConKey
1979 || tc `hasKey` eqReprPrimTyConKey
1980 -> (ty1, ty2)
1981 _ -> pprPanic "getEqPredTys" (ppr ty)
1982
1983 getEqPredTys_maybe :: PredType -> Maybe (Role, Type, Type)
1984 getEqPredTys_maybe ty
1985 = case splitTyConApp_maybe ty of
1986 Just (tc, [_, _, ty1, ty2])
1987 | tc `hasKey` eqPrimTyConKey -> Just (Nominal, ty1, ty2)
1988 | tc `hasKey` eqReprPrimTyConKey -> Just (Representational, ty1, ty2)
1989 _ -> Nothing
1990
1991 getEqPredRole :: PredType -> Role
1992 getEqPredRole ty = eqRelRole (predTypeEqRel ty)
1993
1994 -- | Get the equality relation relevant for a pred type.
1995 predTypeEqRel :: PredType -> EqRel
1996 predTypeEqRel ty
1997 | Just (tc, _) <- splitTyConApp_maybe ty
1998 , tc `hasKey` eqReprPrimTyConKey
1999 = ReprEq
2000 | otherwise
2001 = NomEq
2002
2003 {-
2004 %************************************************************************
2005 %* *
2006 Well-scoped tyvars
2007 * *
2008 ************************************************************************
2009 -}
2010
2011 -- | Do a topological sort on a list of tyvars,
2012 -- so that binders occur before occurrences
2013 -- E.g. given [ a::k, k::*, b::k ]
2014 -- it'll return a well-scoped list [ k::*, a::k, b::k ]
2015 --
2016 -- This is a deterministic sorting operation
2017 -- (that is, doesn't depend on Uniques).
2018 --
2019 -- It is also meant to be stable: that is, variables should not
2020 -- be reordered unnecessarily. The implementation of this
2021 -- has been observed to be stable, though it is not proven to
2022 -- be so. See also Note [Ordering of implicit variables] in RnTypes
2023 toposortTyVars :: [TyCoVar] -> [TyCoVar]
2024 toposortTyVars tvs = reverse $
2025 [ node_payload node | node <- topologicalSortG $
2026 graphFromEdgedVerticesOrd nodes ]
2027 where
2028 var_ids :: VarEnv Int
2029 var_ids = mkVarEnv (zip tvs [1..])
2030
2031 nodes :: [ Node Int TyVar ]
2032 nodes = [ DigraphNode
2033 tv
2034 (lookupVarEnv_NF var_ids tv)
2035 (mapMaybe (lookupVarEnv var_ids)
2036 (tyCoVarsOfTypeList (tyVarKind tv)))
2037 | tv <- tvs ]
2038
2039 -- | Extract a well-scoped list of variables from a deterministic set of
2040 -- variables. The result is deterministic.
2041 -- NB: There used to exist varSetElemsWellScoped :: VarSet -> [Var] which
2042 -- took a non-deterministic set and produced a non-deterministic
2043 -- well-scoped list. If you care about the list being well-scoped you also
2044 -- most likely care about it being in deterministic order.
2045 dVarSetElemsWellScoped :: DVarSet -> [Var]
2046 dVarSetElemsWellScoped = toposortTyVars . dVarSetElems
2047
2048 -- | Get the free vars of a type in scoped order
2049 tyCoVarsOfTypeWellScoped :: Type -> [TyVar]
2050 tyCoVarsOfTypeWellScoped = toposortTyVars . tyCoVarsOfTypeList
2051
2052 -- | Get the free vars of types in scoped order
2053 tyCoVarsOfTypesWellScoped :: [Type] -> [TyVar]
2054 tyCoVarsOfTypesWellScoped = toposortTyVars . tyCoVarsOfTypesList
2055
2056 {-
2057 ************************************************************************
2058 * *
2059 \subsection{Type families}
2060 * *
2061 ************************************************************************
2062 -}
2063
2064 mkFamilyTyConApp :: TyCon -> [Type] -> Type
2065 -- ^ Given a family instance TyCon and its arg types, return the
2066 -- corresponding family type. E.g:
2067 --
2068 -- > data family T a
2069 -- > data instance T (Maybe b) = MkT b
2070 --
2071 -- Where the instance tycon is :RTL, so:
2072 --
2073 -- > mkFamilyTyConApp :RTL Int = T (Maybe Int)
2074 mkFamilyTyConApp tc tys
2075 | Just (fam_tc, fam_tys) <- tyConFamInst_maybe tc
2076 , let tvs = tyConTyVars tc
2077 fam_subst = ASSERT2( tvs `equalLength` tys, ppr tc <+> ppr tys )
2078 zipTvSubst tvs tys
2079 = mkTyConApp fam_tc (substTys fam_subst fam_tys)
2080 | otherwise
2081 = mkTyConApp tc tys
2082
2083 -- | Get the type on the LHS of a coercion induced by a type/data
2084 -- family instance.
2085 coAxNthLHS :: CoAxiom br -> Int -> Type
2086 coAxNthLHS ax ind =
2087 mkTyConApp (coAxiomTyCon ax) (coAxBranchLHS (coAxiomNthBranch ax ind))
2088
2089 -- | Pretty prints a 'TyCon', using the family instance in case of a
2090 -- representation tycon. For example:
2091 --
2092 -- > data T [a] = ...
2093 --
2094 -- In that case we want to print @T [a]@, where @T@ is the family 'TyCon'
2095 pprSourceTyCon :: TyCon -> SDoc
2096 pprSourceTyCon tycon
2097 | Just (fam_tc, tys) <- tyConFamInst_maybe tycon
2098 = ppr $ fam_tc `TyConApp` tys -- can't be FunTyCon
2099 | otherwise
2100 = ppr tycon
2101
2102 isFamFreeTy :: Type -> Bool
2103 isFamFreeTy ty | Just ty' <- coreView ty = isFamFreeTy ty'
2104 isFamFreeTy (TyVarTy _) = True
2105 isFamFreeTy (LitTy {}) = True
2106 isFamFreeTy (TyConApp tc tys) = all isFamFreeTy tys && isFamFreeTyCon tc
2107 isFamFreeTy (AppTy a b) = isFamFreeTy a && isFamFreeTy b
2108 isFamFreeTy (FunTy a b) = isFamFreeTy a && isFamFreeTy b
2109 isFamFreeTy (ForAllTy _ ty) = isFamFreeTy ty
2110 isFamFreeTy (CastTy ty _) = isFamFreeTy ty
2111 isFamFreeTy (CoercionTy _) = False -- Not sure about this
2112
2113 {-
2114 ************************************************************************
2115 * *
2116 \subsection{Liftedness}
2117 * *
2118 ************************************************************************
2119 -}
2120
2121 -- | Returns Just True if this type is surely lifted, Just False
2122 -- if it is surely unlifted, Nothing if we can't be sure (i.e., it is
2123 -- levity polymorphic), and panics if the kind does not have the shape
2124 -- TYPE r.
2125 isLiftedType_maybe :: HasDebugCallStack => Type -> Maybe Bool
2126 isLiftedType_maybe ty = go (getRuntimeRep ty)
2127 where
2128 go rr | Just rr' <- coreView rr = go rr'
2129 go (TyConApp lifted_rep [])
2130 | lifted_rep `hasKey` liftedRepDataConKey = Just True
2131 go (TyConApp {}) = Just False -- everything else is unlifted
2132 go _ = Nothing -- levity polymorphic
2133
2134 -- | See "Type#type_classification" for what an unlifted type is.
2135 -- Panics on levity polymorphic types.
2136 isUnliftedType :: HasDebugCallStack => Type -> Bool
2137 -- isUnliftedType returns True for forall'd unlifted types:
2138 -- x :: forall a. Int#
2139 -- I found bindings like these were getting floated to the top level.
2140 -- They are pretty bogus types, mind you. It would be better never to
2141 -- construct them
2142 isUnliftedType ty
2143 = not (isLiftedType_maybe ty `orElse`
2144 pprPanic "isUnliftedType" (ppr ty <+> dcolon <+> ppr (typeKind ty)))
2145
2146 -- | Is this a type of kind RuntimeRep? (e.g. LiftedRep)
2147 isRuntimeRepKindedTy :: Type -> Bool
2148 isRuntimeRepKindedTy = isRuntimeRepTy . typeKind
2149
2150 -- | Drops prefix of RuntimeRep constructors in 'TyConApp's. Useful for e.g.
2151 -- dropping 'LiftedRep arguments of unboxed tuple TyCon applications:
2152 --
2153 -- dropRuntimeRepArgs [ 'LiftedRep, 'IntRep
2154 -- , String, Int# ] == [String, Int#]
2155 --
2156 dropRuntimeRepArgs :: [Type] -> [Type]
2157 dropRuntimeRepArgs = dropWhile isRuntimeRepKindedTy
2158
2159 -- | Extract the RuntimeRep classifier of a type. For instance,
2160 -- @getRuntimeRep_maybe Int = LiftedRep@. Returns 'Nothing' if this is not
2161 -- possible.
2162 getRuntimeRep_maybe :: HasDebugCallStack
2163 => Type -> Maybe Type
2164 getRuntimeRep_maybe = getRuntimeRepFromKind_maybe . typeKind
2165
2166 -- | Extract the RuntimeRep classifier of a type. For instance,
2167 -- @getRuntimeRep_maybe Int = LiftedRep@. Panics if this is not possible.
2168 getRuntimeRep :: HasDebugCallStack => Type -> Type
2169 getRuntimeRep ty
2170 = case getRuntimeRep_maybe ty of
2171 Just r -> r
2172 Nothing -> pprPanic "getRuntimeRep" (ppr ty <+> dcolon <+> ppr (typeKind ty))
2173
2174 -- | Extract the RuntimeRep classifier of a type from its kind. For example,
2175 -- @getRuntimeRepFromKind * = LiftedRep@; Panics if this is not possible.
2176 getRuntimeRepFromKind :: HasDebugCallStack
2177 => Type -> Type
2178 getRuntimeRepFromKind k =
2179 case getRuntimeRepFromKind_maybe k of
2180 Just r -> r
2181 Nothing -> pprPanic "getRuntimeRepFromKind"
2182 (ppr k <+> dcolon <+> ppr (typeKind k))
2183
2184 -- | Extract the RuntimeRep classifier of a type from its kind. For example,
2185 -- @getRuntimeRepFromKind * = LiftedRep@; Returns 'Nothing' if this is not
2186 -- possible.
2187 getRuntimeRepFromKind_maybe :: HasDebugCallStack
2188 => Type -> Maybe Type
2189 getRuntimeRepFromKind_maybe = go
2190 where
2191 go k | Just k' <- coreView k = go k'
2192 go k
2193 | Just (_tc, [arg]) <- splitTyConApp_maybe k
2194 = ASSERT2( _tc `hasKey` tYPETyConKey, ppr k )
2195 Just arg
2196 go _ = Nothing
2197
2198 isUnboxedTupleType :: Type -> Bool
2199 isUnboxedTupleType ty
2200 = tyConAppTyCon (getRuntimeRep ty) `hasKey` tupleRepDataConKey
2201 -- NB: Do not use typePrimRep, as that can't tell the difference between
2202 -- unboxed tuples and unboxed sums
2203
2204
2205 isUnboxedSumType :: Type -> Bool
2206 isUnboxedSumType ty
2207 = tyConAppTyCon (getRuntimeRep ty) `hasKey` sumRepDataConKey
2208
2209 -- | See "Type#type_classification" for what an algebraic type is.
2210 -- Should only be applied to /types/, as opposed to e.g. partially
2211 -- saturated type constructors
2212 isAlgType :: Type -> Bool
2213 isAlgType ty
2214 = case splitTyConApp_maybe ty of
2215 Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
2216 isAlgTyCon tc
2217 _other -> False
2218
2219 -- | Check whether a type is a data family type
2220 isDataFamilyAppType :: Type -> Bool
2221 isDataFamilyAppType ty = case tyConAppTyCon_maybe ty of
2222 Just tc -> isDataFamilyTyCon tc
2223 _ -> False
2224
2225 -- | Computes whether an argument (or let right hand side) should
2226 -- be computed strictly or lazily, based only on its type.
2227 -- Currently, it's just 'isUnliftedType'. Panics on levity-polymorphic types.
2228 isStrictType :: HasDebugCallStack => Type -> Bool
2229 isStrictType = isUnliftedType
2230
2231 isPrimitiveType :: Type -> Bool
2232 -- ^ Returns true of types that are opaque to Haskell.
2233 isPrimitiveType ty = case splitTyConApp_maybe ty of
2234 Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
2235 isPrimTyCon tc
2236 _ -> False
2237
2238 {-
2239 ************************************************************************
2240 * *
2241 \subsection{Join points}
2242 * *
2243 ************************************************************************
2244 -}
2245
2246 -- | Determine whether a type could be the type of a join point of given total
2247 -- arity, according to the polymorphism rule. A join point cannot be polymorphic
2248 -- in its return type, since given
2249 -- join j @a @b x y z = e1 in e2,
2250 -- the types of e1 and e2 must be the same, and a and b are not in scope for e2.
2251 -- (See Note [The polymorphism rule of join points] in CoreSyn.) Returns False
2252 -- also if the type simply doesn't have enough arguments.
2253 --
2254 -- Note that we need to know how many arguments (type *and* value) the putative
2255 -- join point takes; for instance, if
2256 -- j :: forall a. a -> Int
2257 -- then j could be a binary join point returning an Int, but it could *not* be a
2258 -- unary join point returning a -> Int.
2259 --
2260 -- TODO: See Note [Excess polymorphism and join points]
2261 isValidJoinPointType :: JoinArity -> Type -> Bool
2262 isValidJoinPointType arity ty
2263 = valid_under emptyVarSet arity ty
2264 where
2265 valid_under tvs arity ty
2266 | arity == 0
2267 = isEmptyVarSet (tvs `intersectVarSet` tyCoVarsOfType ty)
2268 | Just (t, ty') <- splitForAllTy_maybe ty
2269 = valid_under (tvs `extendVarSet` t) (arity-1) ty'
2270 | Just (_, res_ty) <- splitFunTy_maybe ty
2271 = valid_under tvs (arity-1) res_ty
2272 | otherwise
2273 = False
2274
2275 {- Note [Excess polymorphism and join points]
2276 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2277 In principle, if a function would be a join point except that it fails
2278 the polymorphism rule (see Note [The polymorphism rule of join points] in
2279 CoreSyn), it can still be made a join point with some effort. This is because
2280 all tail calls must return the same type (they return to the same context!), and
2281 thus if the return type depends on an argument, that argument must always be the
2282 same.
2283
2284 For instance, consider:
2285
2286 let f :: forall a. a -> Char -> [a]
2287 f @a x c = ... f @a y 'a' ...
2288 in ... f @Int 1 'b' ... f @Int 2 'c' ...
2289
2290 (where the calls are tail calls). `f` fails the polymorphism rule because its
2291 return type is [a], where [a] is bound. But since the type argument is always
2292 'Int', we can rewrite it as:
2293
2294 let f' :: Int -> Char -> [Int]
2295 f' x c = ... f' y 'a' ...
2296 in ... f' 1 'b' ... f 2 'c' ...
2297
2298 and now we can make f' a join point:
2299
2300 join f' :: Int -> Char -> [Int]
2301 f' x c = ... jump f' y 'a' ...
2302 in ... jump f' 1 'b' ... jump f' 2 'c' ...
2303
2304 It's not clear that this comes up often, however. TODO: Measure how often and
2305 add this analysis if necessary. See Trac #14620.
2306
2307
2308 ************************************************************************
2309 * *
2310 \subsection{Sequencing on types}
2311 * *
2312 ************************************************************************
2313 -}
2314
2315 seqType :: Type -> ()
2316 seqType (LitTy n) = n `seq` ()
2317 seqType (TyVarTy tv) = tv `seq` ()
2318 seqType (AppTy t1 t2) = seqType t1 `seq` seqType t2
2319 seqType (FunTy t1 t2) = seqType t1 `seq` seqType t2
2320 seqType (TyConApp tc tys) = tc `seq` seqTypes tys
2321 seqType (ForAllTy (Bndr tv _) ty) = seqType (varType tv) `seq` seqType ty
2322 seqType (CastTy ty co) = seqType ty `seq` seqCo co
2323 seqType (CoercionTy co) = seqCo co
2324
2325 seqTypes :: [Type] -> ()
2326 seqTypes [] = ()
2327 seqTypes (ty:tys) = seqType ty `seq` seqTypes tys
2328
2329 {-
2330 ************************************************************************
2331 * *
2332 Comparison for types
2333 (We don't use instances so that we know where it happens)
2334 * *
2335 ************************************************************************
2336
2337 Note [Equality on AppTys]
2338 ~~~~~~~~~~~~~~~~~~~~~~~~~
2339 In our cast-ignoring equality, we want to say that the following two
2340 are equal:
2341
2342 (Maybe |> co) (Int |> co') ~? Maybe Int
2343
2344 But the left is an AppTy while the right is a TyConApp. The solution is
2345 to use repSplitAppTy_maybe to break up the TyConApp into its pieces and
2346 then continue. Easy to do, but also easy to forget to do.
2347
2348 -}
2349
2350 eqType :: Type -> Type -> Bool
2351 -- ^ Type equality on source types. Does not look through @newtypes@ or
2352 -- 'PredType's, but it does look through type synonyms.
2353 -- This first checks that the kinds of the types are equal and then
2354 -- checks whether the types are equal, ignoring casts and coercions.
2355 -- (The kind check is a recursive call, but since all kinds have type
2356 -- @Type@, there is no need to check the types of kinds.)
2357 -- See also Note [Non-trivial definitional equality] in TyCoRep.
2358 eqType t1 t2 = isEqual $ nonDetCmpType t1 t2
2359 -- It's OK to use nonDetCmpType here and eqType is deterministic,
2360 -- nonDetCmpType does equality deterministically
2361
2362 -- | Compare types with respect to a (presumably) non-empty 'RnEnv2'.
2363 eqTypeX :: RnEnv2 -> Type -> Type -> Bool
2364 eqTypeX env t1 t2 = isEqual $ nonDetCmpTypeX env t1 t2
2365 -- It's OK to use nonDetCmpType here and eqTypeX is deterministic,
2366 -- nonDetCmpTypeX does equality deterministically
2367
2368 -- | Type equality on lists of types, looking through type synonyms
2369 -- but not newtypes.
2370 eqTypes :: [Type] -> [Type] -> Bool
2371 eqTypes tys1 tys2 = isEqual $ nonDetCmpTypes tys1 tys2
2372 -- It's OK to use nonDetCmpType here and eqTypes is deterministic,
2373 -- nonDetCmpTypes does equality deterministically
2374
2375 eqVarBndrs :: RnEnv2 -> [Var] -> [Var] -> Maybe RnEnv2
2376 -- Check that the var lists are the same length
2377 -- and have matching kinds; if so, extend the RnEnv2
2378 -- Returns Nothing if they don't match
2379 eqVarBndrs env [] []
2380 = Just env
2381 eqVarBndrs env (tv1:tvs1) (tv2:tvs2)
2382 | eqTypeX env (varType tv1) (varType tv2)
2383 = eqVarBndrs (rnBndr2 env tv1 tv2) tvs1 tvs2
2384 eqVarBndrs _ _ _= Nothing
2385
2386 -- Now here comes the real worker
2387
2388 {-
2389 Note [nonDetCmpType nondeterminism]
2390 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2391 nonDetCmpType is implemented in terms of nonDetCmpTypeX. nonDetCmpTypeX
2392 uses nonDetCmpTc which compares TyCons by their Unique value. Using Uniques for
2393 ordering leads to nondeterminism. We hit the same problem in the TyVarTy case,
2394 comparing type variables is nondeterministic, note the call to nonDetCmpVar in
2395 nonDetCmpTypeX.
2396 See Note [Unique Determinism] for more details.
2397 -}
2398
2399 nonDetCmpType :: Type -> Type -> Ordering
2400 nonDetCmpType t1 t2
2401 -- we know k1 and k2 have the same kind, because they both have kind *.
2402 = nonDetCmpTypeX rn_env t1 t2
2403 where
2404 rn_env = mkRnEnv2 (mkInScopeSet (tyCoVarsOfTypes [t1, t2]))
2405
2406 nonDetCmpTypes :: [Type] -> [Type] -> Ordering
2407 nonDetCmpTypes ts1 ts2 = nonDetCmpTypesX rn_env ts1 ts2
2408 where
2409 rn_env = mkRnEnv2 (mkInScopeSet (tyCoVarsOfTypes (ts1 ++ ts2)))
2410
2411 -- | An ordering relation between two 'Type's (known below as @t1 :: k1@
2412 -- and @t2 :: k2@)
2413 data TypeOrdering = TLT -- ^ @t1 < t2@
2414 | TEQ -- ^ @t1 ~ t2@ and there are no casts in either,
2415 -- therefore we can conclude @k1 ~ k2@
2416 | TEQX -- ^ @t1 ~ t2@ yet one of the types contains a cast so
2417 -- they may differ in kind.
2418 | TGT -- ^ @t1 > t2@
2419 deriving (Eq, Ord, Enum, Bounded)
2420
2421 nonDetCmpTypeX :: RnEnv2 -> Type -> Type -> Ordering -- Main workhorse
2422 -- See Note [Non-trivial definitional equality] in TyCoRep
2423 nonDetCmpTypeX env orig_t1 orig_t2 =
2424 case go env orig_t1 orig_t2 of
2425 -- If there are casts then we also need to do a comparison of the kinds of
2426 -- the types being compared
2427 TEQX -> toOrdering $ go env k1 k2
2428 ty_ordering -> toOrdering ty_ordering
2429 where
2430 k1 = typeKind orig_t1
2431 k2 = typeKind orig_t2
2432
2433 toOrdering :: TypeOrdering -> Ordering
2434 toOrdering TLT = LT
2435 toOrdering TEQ = EQ
2436 toOrdering TEQX = EQ
2437 toOrdering TGT = GT
2438
2439 liftOrdering :: Ordering -> TypeOrdering
2440 liftOrdering LT = TLT
2441 liftOrdering EQ = TEQ
2442 liftOrdering GT = TGT
2443
2444 thenCmpTy :: TypeOrdering -> TypeOrdering -> TypeOrdering
2445 thenCmpTy TEQ rel = rel
2446 thenCmpTy TEQX rel = hasCast rel
2447 thenCmpTy rel _ = rel
2448
2449 hasCast :: TypeOrdering -> TypeOrdering
2450 hasCast TEQ = TEQX
2451 hasCast rel = rel
2452
2453 -- Returns both the resulting ordering relation between the two types
2454 -- and whether either contains a cast.
2455 go :: RnEnv2 -> Type -> Type -> TypeOrdering
2456 go env t1 t2
2457 | Just t1' <- coreView t1 = go env t1' t2
2458 | Just t2' <- coreView t2 = go env t1 t2'
2459
2460 go env (TyVarTy tv1) (TyVarTy tv2)
2461 = liftOrdering $ rnOccL env tv1 `nonDetCmpVar` rnOccR env tv2
2462 go env (ForAllTy (Bndr tv1 _) t1) (ForAllTy (Bndr tv2 _) t2)
2463 = go env (varType tv1) (varType tv2)
2464 `thenCmpTy` go (rnBndr2 env tv1 tv2) t1 t2
2465 -- See Note [Equality on AppTys]
2466 go env (AppTy s1 t1) ty2
2467 | Just (s2, t2) <- repSplitAppTy_maybe ty2
2468 = go env s1 s2 `thenCmpTy` go env t1 t2
2469 go env ty1 (AppTy s2 t2)
2470 | Just (s1, t1) <- repSplitAppTy_maybe ty1
2471 = go env s1 s2 `thenCmpTy` go env t1 t2
2472 go env (FunTy s1 t1) (FunTy s2 t2)
2473 = go env s1 s2 `thenCmpTy` go env t1 t2
2474 go env (TyConApp tc1 tys1) (TyConApp tc2 tys2)
2475 = liftOrdering (tc1 `nonDetCmpTc` tc2) `thenCmpTy` gos env tys1 tys2
2476 go _ (LitTy l1) (LitTy l2) = liftOrdering (compare l1 l2)
2477 go env (CastTy t1 _) t2 = hasCast $ go env t1 t2
2478 go env t1 (CastTy t2 _) = hasCast $ go env t1 t2
2479
2480 go _ (CoercionTy {}) (CoercionTy {}) = TEQ
2481
2482 -- Deal with the rest: TyVarTy < CoercionTy < AppTy < LitTy < TyConApp < ForAllTy
2483 go _ ty1 ty2
2484 = liftOrdering $ (get_rank ty1) `compare` (get_rank ty2)
2485 where get_rank :: Type -> Int
2486 get_rank (CastTy {})
2487 = pprPanic "nonDetCmpTypeX.get_rank" (ppr [ty1,ty2])
2488 get_rank (TyVarTy {}) = 0
2489 get_rank (CoercionTy {}) = 1
2490 get_rank (AppTy {}) = 3
2491 get_rank (LitTy {}) = 4
2492 get_rank (TyConApp {}) = 5
2493 get_rank (FunTy {}) = 6
2494 get_rank (ForAllTy {}) = 7
2495
2496 gos :: RnEnv2 -> [Type] -> [Type] -> TypeOrdering
2497 gos _ [] [] = TEQ
2498 gos _ [] _ = TLT
2499 gos _ _ [] = TGT
2500 gos env (ty1:tys1) (ty2:tys2) = go env ty1 ty2 `thenCmpTy` gos env tys1 tys2
2501
2502 -------------
2503 nonDetCmpTypesX :: RnEnv2 -> [Type] -> [Type] -> Ordering
2504 nonDetCmpTypesX _ [] [] = EQ
2505 nonDetCmpTypesX env (t1:tys1) (t2:tys2) = nonDetCmpTypeX env t1 t2
2506 `thenCmp`
2507 nonDetCmpTypesX env tys1 tys2
2508 nonDetCmpTypesX _ [] _ = LT
2509 nonDetCmpTypesX _ _ [] = GT
2510
2511 -------------
2512 -- | Compare two 'TyCon's. NB: This should /never/ see 'Constraint' (as
2513 -- recognized by Kind.isConstraintKindCon) which is considered a synonym for
2514 -- 'Type' in Core.
2515 -- See Note [Kind Constraint and kind Type] in Kind.
2516 -- See Note [nonDetCmpType nondeterminism]
2517 nonDetCmpTc :: TyCon -> TyCon -> Ordering
2518 nonDetCmpTc tc1 tc2
2519 = ASSERT( not (isConstraintKindCon tc1) && not (isConstraintKindCon tc2) )
2520 u1 `nonDetCmpUnique` u2
2521 where
2522 u1 = tyConUnique tc1
2523 u2 = tyConUnique tc2
2524
2525 {-
2526 ************************************************************************
2527 * *
2528 The kind of a type
2529 * *
2530 ************************************************************************
2531 -}
2532
2533 typeKind :: HasDebugCallStack => Type -> Kind
2534 typeKind (TyConApp tc tys) = piResultTys (tyConKind tc) tys
2535 typeKind (AppTy fun arg) = typeKind_apps fun [arg]
2536 typeKind (LitTy l) = typeLiteralKind l
2537 typeKind (FunTy {}) = liftedTypeKind
2538 typeKind (TyVarTy tyvar) = tyVarKind tyvar
2539 typeKind (CastTy _ty co) = pSnd $ coercionKind co
2540 typeKind (CoercionTy co) = coercionType co
2541 typeKind ty@(ForAllTy (Bndr tv _) _)
2542 | isTyVar tv -- See Note [Weird typing rule for ForAllTy].
2543 = case occCheckExpand tvs k of -- We must make sure tv does not occur in kind
2544 Just k' -> k' -- As it is already out of scope!
2545 Nothing -> pprPanic "typeKind"
2546 (ppr ty $$ ppr k $$ ppr tvs $$ ppr body)
2547 where
2548 (tvs, body) = splitTyVarForAllTys ty
2549 k = typeKind body
2550 typeKind (ForAllTy {}) = liftedTypeKind
2551
2552 typeKind_apps :: HasDebugCallStack => Type -> [Type] -> Kind
2553 -- The sole purpose of the function is to accumulate
2554 -- the type arugments, so we can call piResultTys, rather than
2555 -- a succession of calls to piResultTy (which is asymptotically
2556 -- less efficient as the number of arguments increases)
2557 typeKind_apps (AppTy fun arg) args = typeKind_apps fun (arg:args)
2558 typeKind_apps fun args = piResultTys (typeKind fun) args
2559
2560 --------------------------
2561 typeLiteralKind :: TyLit -> Kind
2562 typeLiteralKind l =
2563 case l of
2564 NumTyLit _ -> typeNatKind
2565 StrTyLit _ -> typeSymbolKind
2566
2567 -- | Returns True if a type is levity polymorphic. Should be the same
2568 -- as (isKindLevPoly . typeKind) but much faster.
2569 -- Precondition: The type has kind (TYPE blah)
2570 isTypeLevPoly :: Type -> Bool
2571 isTypeLevPoly = go
2572 where
2573 go ty@(TyVarTy {}) = check_kind ty
2574 go ty@(AppTy {}) = check_kind ty
2575 go ty@(TyConApp tc _) | not (isTcLevPoly tc) = False
2576 | otherwise = check_kind ty
2577 go (ForAllTy _ ty) = go ty
2578 go (FunTy {}) = False
2579 go (LitTy {}) = False
2580 go ty@(CastTy {}) = check_kind ty
2581 go ty@(CoercionTy {}) = pprPanic "isTypeLevPoly co" (ppr ty)
2582
2583 check_kind = isKindLevPoly . typeKind
2584
2585 -- | Looking past all pi-types, is the end result potentially levity polymorphic?
2586 -- Example: True for (forall r (a :: TYPE r). String -> a)
2587 -- Example: False for (forall r1 r2 (a :: TYPE r1) (b :: TYPE r2). a -> b -> Type)
2588 resultIsLevPoly :: Type -> Bool
2589 resultIsLevPoly = isTypeLevPoly . snd . splitPiTys
2590
2591
2592 {- **********************************************************************
2593 * *
2594 Occurs check expansion
2595 %* *
2596 %********************************************************************* -}
2597
2598 {- Note [Occurs check expansion]
2599 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2600 (occurCheckExpand tv xi) expands synonyms in xi just enough to get rid
2601 of occurrences of tv outside type function arguments, if that is
2602 possible; otherwise, it returns Nothing.
2603
2604 For example, suppose we have
2605 type F a b = [a]
2606 Then
2607 occCheckExpand b (F Int b) = Just [Int]
2608 but
2609 occCheckExpand a (F a Int) = Nothing
2610
2611 We don't promise to do the absolute minimum amount of expanding
2612 necessary, but we try not to do expansions we don't need to. We
2613 prefer doing inner expansions first. For example,
2614 type F a b = (a, Int, a, [a])
2615 type G b = Char
2616 We have
2617 occCheckExpand b (F (G b)) = Just (F Char)
2618 even though we could also expand F to get rid of b.
2619 -}
2620
2621 occCheckExpand :: [Var] -> Type -> Maybe Type
2622 -- See Note [Occurs check expansion]
2623 -- We may have needed to do some type synonym unfolding in order to
2624 -- get rid of the variable (or forall), so we also return the unfolded
2625 -- version of the type, which is guaranteed to be syntactically free
2626 -- of the given type variable. If the type is already syntactically
2627 -- free of the variable, then the same type is returned.
2628 occCheckExpand vs_to_avoid ty
2629 = go (mkVarSet vs_to_avoid, emptyVarEnv) ty
2630 where
2631 go :: (VarSet, VarEnv TyCoVar) -> Type -> Maybe Type
2632 -- The VarSet is the set of variables we are trying to avoid
2633 -- The VarEnv carries mappings necessary
2634 -- because of kind expansion
2635 go cxt@(as, env) (TyVarTy tv')
2636 | tv' `elemVarSet` as = Nothing
2637 | Just tv'' <- lookupVarEnv env tv' = return (mkTyVarTy tv'')
2638 | otherwise = do { tv'' <- go_var cxt tv'
2639 ; return (mkTyVarTy tv'') }
2640
2641 go _ ty@(LitTy {}) = return ty
2642 go cxt (AppTy ty1 ty2) = do { ty1' <- go cxt ty1
2643 ; ty2' <- go cxt ty2
2644 ; return (mkAppTy ty1' ty2') }
2645 go cxt (FunTy ty1 ty2) = do { ty1' <- go cxt ty1
2646 ; ty2' <- go cxt ty2
2647 ; return (mkFunTy ty1' ty2') }
2648 go cxt@(as, env) (ForAllTy (Bndr tv vis) body_ty)
2649 = do { ki' <- go cxt (varType tv)
2650 ; let tv' = setVarType tv ki'
2651 env' = extendVarEnv env tv tv'
2652 as' = as `delVarSet` tv
2653 ; body' <- go (as', env') body_ty
2654 ; return (ForAllTy (Bndr tv' vis) body') }
2655
2656 -- For a type constructor application, first try expanding away the
2657 -- offending variable from the arguments. If that doesn't work, next
2658 -- see if the type constructor is a type synonym, and if so, expand
2659 -- it and try again.
2660 go cxt ty@(TyConApp tc tys)
2661 = case mapM (go cxt) tys of
2662 Just tys' -> return (mkTyConApp tc tys')
2663 Nothing | Just ty' <- tcView ty -> go cxt ty'
2664 | otherwise -> Nothing
2665 -- Failing that, try to expand a synonym
2666
2667 go cxt (CastTy ty co) = do { ty' <- go cxt ty
2668 ; co' <- go_co cxt co
2669 ; return (mkCastTy ty' co') }
2670 go cxt (CoercionTy co) = do { co' <- go_co cxt co
2671 ; return (mkCoercionTy co') }
2672
2673 ------------------
2674 go_var cxt v = do { k' <- go cxt (varType v)
2675 ; return (setVarType v k') }
2676 -- Works for TyVar and CoVar
2677 -- See Note [Occurrence checking: look inside kinds]
2678
2679 ------------------
2680 go_mco _ MRefl = return MRefl
2681 go_mco ctx (MCo co) = MCo <$> go_co ctx co
2682
2683 ------------------
2684 go_co cxt (Refl ty) = do { ty' <- go cxt ty
2685 ; return (mkNomReflCo ty') }
2686 go_co cxt (GRefl r ty mco) = do { mco' <- go_mco cxt mco
2687 ; ty' <- go cxt ty
2688 ; return (mkGReflCo r ty' mco') }
2689 -- Note: Coercions do not contain type synonyms
2690 go_co cxt (TyConAppCo r tc args) = do { args' <- mapM (go_co cxt) args
2691 ; return (mkTyConAppCo r tc args') }
2692 go_co cxt (AppCo co arg) = do { co' <- go_co cxt co
2693 ; arg' <- go_co cxt arg
2694 ; return (mkAppCo co' arg') }
2695 go_co cxt@(as, env) (ForAllCo tv kind_co body_co)
2696 = do { kind_co' <- go_co cxt kind_co
2697 ; let tv' = setVarType tv $
2698 pFst (coercionKind kind_co')
2699 env' = extendVarEnv env tv tv'
2700 as' = as `delVarSet` tv
2701 ; body' <- go_co (as', env') body_co
2702 ; return (ForAllCo tv' kind_co' body') }
2703 go_co cxt (FunCo r co1 co2) = do { co1' <- go_co cxt co1
2704 ; co2' <- go_co cxt co2
2705 ; return (mkFunCo r co1' co2') }
2706 go_co cxt@(as,env) (CoVarCo c)
2707 | c `elemVarSet` as = Nothing
2708 | Just c' <- lookupVarEnv env c = return (mkCoVarCo c')
2709 | otherwise = do { c' <- go_var cxt c
2710 ; return (mkCoVarCo c') }
2711 go_co cxt (HoleCo h) = do { c' <- go_var cxt (ch_co_var h)
2712 ; return (HoleCo (h { ch_co_var = c' })) }
2713 go_co cxt (AxiomInstCo ax ind args) = do { args' <- mapM (go_co cxt) args
2714 ; return (mkAxiomInstCo ax ind args') }
2715 go_co cxt (UnivCo p r ty1 ty2) = do { p' <- go_prov cxt p
2716 ; ty1' <- go cxt ty1
2717 ; ty2' <- go cxt ty2
2718 ; return (mkUnivCo p' r ty1' ty2') }
2719 go_co cxt (SymCo co) = do { co' <- go_co cxt co
2720 ; return (mkSymCo co') }
2721 go_co cxt (TransCo co1 co2) = do { co1' <- go_co cxt co1
2722 ; co2' <- go_co cxt co2
2723 ; return (mkTransCo co1' co2') }
2724 go_co cxt (NthCo r n co) = do { co' <- go_co cxt co
2725 ; return (mkNthCo r n co') }
2726 go_co cxt (LRCo lr co) = do { co' <- go_co cxt co
2727 ; return (mkLRCo lr co') }
2728 go_co cxt (InstCo co arg) = do { co' <- go_co cxt co
2729 ; arg' <- go_co cxt arg
2730 ; return (mkInstCo co' arg') }
2731 go_co cxt (KindCo co) = do { co' <- go_co cxt co
2732 ; return (mkKindCo co') }
2733 go_co cxt (SubCo co) = do { co' <- go_co cxt co
2734 ; return (mkSubCo co') }
2735 go_co cxt (AxiomRuleCo ax cs) = do { cs' <- mapM (go_co cxt) cs
2736 ; return (mkAxiomRuleCo ax cs') }
2737
2738 ------------------
2739 go_prov _ UnsafeCoerceProv = return UnsafeCoerceProv
2740 go_prov cxt (PhantomProv co) = PhantomProv <$> go_co cxt co
2741 go_prov cxt (ProofIrrelProv co) = ProofIrrelProv <$> go_co cxt co
2742 go_prov _ p@(PluginProv _) = return p
2743
2744
2745 {-
2746 %************************************************************************
2747 %* *
2748 Miscellaneous functions
2749 %* *
2750 %************************************************************************
2751
2752 -}
2753 -- | All type constructors occurring in the type; looking through type
2754 -- synonyms, but not newtypes.
2755 -- When it finds a Class, it returns the class TyCon.
2756 tyConsOfType :: Type -> UniqSet TyCon
2757 tyConsOfType ty
2758 = go ty
2759 where
2760 go :: Type -> UniqSet TyCon -- The UniqSet does duplicate elim
2761 go ty | Just ty' <- coreView ty = go ty'
2762 go (TyVarTy {}) = emptyUniqSet
2763 go (LitTy {}) = emptyUniqSet
2764 go (TyConApp tc tys) = go_tc tc `unionUniqSets` go_s tys
2765 go (AppTy a b) = go a `unionUniqSets` go b
2766 go (FunTy a b) = go a `unionUniqSets` go b `unionUniqSets` go_tc funTyCon
2767 go (ForAllTy (Bndr tv _) ty) = go ty `unionUniqSets` go (varType tv)
2768 go (CastTy ty co) = go ty `unionUniqSets` go_co co
2769 go (CoercionTy co) = go_co co
2770
2771 go_co (Refl ty) = go ty
2772 go_co (GRefl _ ty mco) = go ty `unionUniqSets` go_mco mco
2773 go_co (TyConAppCo _ tc args) = go_tc tc `unionUniqSets` go_cos args
2774 go_co (AppCo co arg) = go_co co `unionUniqSets` go_co arg
2775 go_co (ForAllCo _ kind_co co) = go_co kind_co `unionUniqSets` go_co co
2776 go_co (FunCo _ co1 co2) = go_co co1 `unionUniqSets` go_co co2
2777 go_co (AxiomInstCo ax _ args) = go_ax ax `unionUniqSets` go_cos args
2778 go_co (UnivCo p _ t1 t2) = go_prov p `unionUniqSets` go t1 `unionUniqSets` go t2
2779 go_co (CoVarCo {}) = emptyUniqSet
2780 go_co (HoleCo {}) = emptyUniqSet
2781 go_co (SymCo co) = go_co co
2782 go_co (TransCo co1 co2) = go_co co1 `unionUniqSets` go_co co2
2783 go_co (NthCo _ _ co) = go_co co
2784 go_co (LRCo _ co) = go_co co
2785 go_co (InstCo co arg) = go_co co `unionUniqSets` go_co arg
2786 go_co (KindCo co) = go_co co
2787 go_co (SubCo co) = go_co co
2788 go_co (AxiomRuleCo _ cs) = go_cos cs
2789
2790 go_mco MRefl = emptyUniqSet
2791 go_mco (MCo co) = go_co co
2792
2793 go_prov UnsafeCoerceProv = emptyUniqSet
2794 go_prov (PhantomProv co) = go_co co
2795 go_prov (ProofIrrelProv co) = go_co co
2796 go_prov (PluginProv _) = emptyUniqSet
2797 -- this last case can happen from the tyConsOfType used from
2798 -- checkTauTvUpdate
2799
2800 go_s tys = foldr (unionUniqSets . go) emptyUniqSet tys
2801 go_cos cos = foldr (unionUniqSets . go_co) emptyUniqSet cos
2802
2803 go_tc tc = unitUniqSet tc
2804 go_ax ax = go_tc $ coAxiomTyCon ax
2805
2806 -- | Find the result 'Kind' of a type synonym,
2807 -- after applying it to its 'arity' number of type variables
2808 -- Actually this function works fine on data types too,
2809 -- but they'd always return '*', so we never need to ask
2810 synTyConResKind :: TyCon -> Kind
2811 synTyConResKind tycon = piResultTys (tyConKind tycon) (mkTyVarTys (tyConTyVars tycon))
2812
2813 -- | Retrieve the free variables in this type, splitting them based
2814 -- on whether they are used visibly or invisibly. Invisible ones come
2815 -- first.
2816 splitVisVarsOfType :: Type -> Pair TyCoVarSet
2817 splitVisVarsOfType orig_ty = Pair invis_vars vis_vars
2818 where
2819 Pair invis_vars1 vis_vars = go orig_ty
2820 invis_vars = invis_vars1 `minusVarSet` vis_vars
2821
2822 go (TyVarTy tv) = Pair (tyCoVarsOfType $ tyVarKind tv) (unitVarSet tv)
2823 go (AppTy t1 t2) = go t1 `mappend` go t2
2824 go (TyConApp tc tys) = go_tc tc tys
2825 go (FunTy t1 t2) = go t1 `mappend` go t2
2826 go (ForAllTy (Bndr tv _) ty)
2827 = ((`delVarSet` tv) <$> go ty) `mappend`
2828 (invisible (tyCoVarsOfType $ varType tv))
2829 go (LitTy {}) = mempty
2830 go (CastTy ty co) = go ty `mappend` invisible (tyCoVarsOfCo co)
2831 go (CoercionTy co) = invisible $ tyCoVarsOfCo co
2832
2833 invisible vs = Pair vs emptyVarSet
2834
2835 go_tc tc tys = let (invis, vis) = partitionInvisibles tc id tys in
2836 invisible (tyCoVarsOfTypes invis) `mappend` foldMap go vis
2837
2838 splitVisVarsOfTypes :: [Type] -> Pair TyCoVarSet
2839 splitVisVarsOfTypes = foldMap splitVisVarsOfType
2840
2841 modifyJoinResTy :: Int -- Number of binders to skip
2842 -> (Type -> Type) -- Function to apply to result type
2843 -> Type -- Type of join point
2844 -> Type -- New type
2845 -- INVARIANT: If any of the first n binders are foralls, those tyvars cannot
2846 -- appear in the original result type. See isValidJoinPointType.
2847 modifyJoinResTy orig_ar f orig_ty
2848 = go orig_ar orig_ty
2849 where
2850 go 0 ty = f ty
2851 go n ty | Just (arg_bndr, res_ty) <- splitPiTy_maybe ty
2852 = mkTyCoPiTy arg_bndr (go (n-1) res_ty)
2853 | otherwise
2854 = pprPanic "modifyJoinResTy" (ppr orig_ar <+> ppr orig_ty)
2855
2856 setJoinResTy :: Int -- Number of binders to skip
2857 -> Type -- New result type
2858 -> Type -- Type of join point
2859 -> Type -- New type
2860 -- INVARIANT: Same as for modifyJoinResTy
2861 setJoinResTy ar new_res_ty ty
2862 = modifyJoinResTy ar (const new_res_ty) ty
2863
2864 {-
2865 %************************************************************************
2866 %* *
2867 Pretty-printing
2868 %* *
2869 %************************************************************************
2870
2871 Most pretty-printing is either in TyCoRep or IfaceType.
2872
2873 -}
2874
2875 -- | This variant preserves any use of TYPE in a type, effectively
2876 -- locally setting -fprint-explicit-runtime-reps.
2877 pprWithTYPE :: Type -> SDoc
2878 pprWithTYPE ty = updSDocDynFlags (flip gopt_set Opt_PrintExplicitRuntimeReps) $
2879 ppr ty