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