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