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