Add two small optimizations. (#11196)
[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 #-}
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, VisibilityFlag(..), KindOrType, PredType, ThetaType,
18 Var, TyVar, isTyVar, TyCoVar, TyBinder,
19
20 -- ** Constructing and deconstructing types
21 mkTyVarTy, mkTyVarTys, getTyVar, getTyVar_maybe, repGetTyVar_maybe,
22 getCastedTyVar_maybe, tyVarKind,
23
24 mkAppTy, mkAppTys, splitAppTy, splitAppTys, repSplitAppTys,
25 splitAppTy_maybe, repSplitAppTy_maybe, tcRepSplitAppTy_maybe,
26
27 mkFunTy, mkFunTys, splitFunTy, splitFunTy_maybe,
28 splitFunTys, splitFunTysN,
29 funResultTy, funArgTy,
30
31 mkTyConApp, mkTyConTy,
32 tyConAppTyCon_maybe, tyConAppTyConPicky_maybe,
33 tyConAppArgs_maybe, tyConAppTyCon, tyConAppArgs,
34 splitTyConApp_maybe, splitTyConApp, tyConAppArgN, nextRole,
35 splitListTyConApp_maybe,
36 repSplitTyConApp_maybe,
37
38 mkForAllTy, mkForAllTys, mkInvForAllTys, mkSpecForAllTys,
39 mkVisForAllTys,
40 mkNamedForAllTy,
41 splitForAllTy_maybe, splitForAllTys, splitForAllTy,
42 splitPiTy_maybe, splitPiTys, splitPiTy,
43 splitNamedPiTys,
44 mkPiType, mkPiTypes, mkTyBindersPreferAnon,
45 piResultTy, piResultTys,
46 applyTysX, dropForAlls,
47
48 mkNumLitTy, isNumLitTy,
49 mkStrLitTy, isStrLitTy,
50
51 mkCastTy, mkCoercionTy, splitCastTy_maybe,
52
53 userTypeError_maybe, pprUserTypeErrorTy,
54
55 coAxNthLHS,
56 stripCoercionTy, splitCoercionType_maybe,
57
58 splitPiTysInvisible, filterOutInvisibleTypes,
59 filterOutInvisibleTyVars, partitionInvisibles,
60 synTyConResKind,
61
62 -- Analyzing types
63 TyCoMapper(..), mapType, mapCoercion,
64
65 -- (Newtypes)
66 newTyConInstRhs,
67
68 -- Pred types
69 mkFamilyTyConApp,
70 isDictLikeTy,
71 mkPrimEqPred, mkReprPrimEqPred, mkPrimEqPredRole,
72 equalityTyCon,
73 mkHeteroPrimEqPred, mkHeteroReprPrimEqPred,
74 mkClassPred,
75 isClassPred, isEqPred, isNomEqPred,
76 isIPPred, isIPPred_maybe, isIPTyCon, isIPClass,
77 isCTupleClass,
78
79 -- Deconstructing predicate types
80 PredTree(..), EqRel(..), eqRelRole, classifyPredType,
81 getClassPredTys, getClassPredTys_maybe,
82 getEqPredTys, getEqPredTys_maybe, getEqPredRole,
83 predTypeEqRel,
84
85 -- ** Binders
86 sameVis,
87 mkNamedBinder, mkAnonBinder, isNamedBinder, isAnonBinder,
88 isIdLikeBinder, binderVisibility, binderVar_maybe,
89 binderVar, binderRelevantType_maybe, caseBinder,
90 partitionBinders, partitionBindersIntoBinders,
91 binderType, isVisibleBinder, isInvisibleBinder,
92
93 -- ** Common type constructors
94 funTyCon,
95
96 -- ** Predicates on types
97 allDistinctTyVars,
98 isTyVarTy, isFunTy, isDictTy, isPredTy, isVoidTy, isCoercionTy,
99 isCoercionTy_maybe, isCoercionType, isForAllTy,
100 isPiTy,
101
102 -- (Lifting and boxity)
103 isUnliftedType, isUnboxedTupleType, isAlgType, isClosedAlgType,
104 isPrimitiveType, isStrictType,
105 isRuntimeRepTy, isRuntimeRepVar, isRuntimeRepKindedTy,
106 dropRuntimeRepArgs,
107 getRuntimeRep, getRuntimeRepFromKind,
108
109 -- * Main data types representing Kinds
110 Kind,
111
112 -- ** Finding the kind of a type
113 typeKind,
114
115 -- ** Common Kind
116 liftedTypeKind,
117
118 -- * Type free variables
119 tyCoVarsOfType, tyCoVarsOfTypes, tyCoVarsOfTypeAcc,
120 tyCoVarsOfTypeDSet,
121 coVarsOfType,
122 coVarsOfTypes, closeOverKinds,
123 splitDepVarsOfType, splitDepVarsOfTypes,
124 splitVisVarsOfType, splitVisVarsOfTypes,
125 expandTypeSynonyms,
126 typeSize,
127
128 -- * Well-scoped lists of variables
129 varSetElemsWellScoped, toposortTyVars, tyCoVarsOfTypeWellScoped,
130 tyCoVarsOfTypesWellScoped,
131
132 -- * Type comparison
133 eqType, eqTypeX, eqTypes, cmpType, cmpTypes, cmpTypeX, cmpTypesX, cmpTc,
134 eqVarBndrs,
135
136 -- * Forcing evaluation of types
137 seqType, seqTypes,
138
139 -- * Other views onto Types
140 coreView, coreViewOneStarKind,
141
142 UnaryType, RepType(..), flattenRepType, repType,
143 tyConsOfType,
144
145 -- * Type representation for the code generator
146 typePrimRep, typeRepArity, kindPrimRep, tyConPrimRep,
147
148 -- * Main type substitution data types
149 TvSubstEnv, -- Representation widely visible
150 TCvSubst(..), -- Representation visible to a few friends
151
152 -- ** Manipulating type substitutions
153 emptyTvSubstEnv, emptyTCvSubst, mkEmptyTCvSubst,
154
155 mkTCvSubst, zipTvSubst, mkTvSubstPrs,
156 notElemTCvSubst,
157 getTvSubstEnv, setTvSubstEnv,
158 zapTCvSubst, getTCvInScope,
159 extendTCvInScope, extendTCvInScopeList, extendTCvInScopeSet,
160 extendTCvSubst, extendCvSubst,
161 extendTvSubst, extendTvSubstList, extendTvSubstAndInScope,
162 isInScope, composeTCvSubstEnv, composeTCvSubst, zipTyEnv, zipCoEnv,
163 isEmptyTCvSubst, unionTCvSubst,
164
165 -- ** Performing substitution on types and kinds
166 substTy, substTys, substTyWith, substTysWith, substTheta,
167 substTyAddInScope,
168 substTyUnchecked, substTysUnchecked, substThetaUnchecked,
169 substTyWithUnchecked,
170 substCoUnchecked, substCoWithUnchecked,
171 substTyVarBndr, substTyVar, substTyVars,
172 cloneTyVarBndr, cloneTyVarBndrs, lookupTyVar,
173
174 -- * Pretty-printing
175 pprType, pprParendType, pprTypeApp, pprTyThingCategory, pprTyThing,
176 pprTvBndr, pprTvBndrs, pprForAll, pprForAllImplicit, pprUserForAll,
177 pprSigmaType,
178 pprTheta, pprThetaArrowTy, pprClassPred,
179 pprKind, pprParendKind, pprSourceTyCon,
180 TyPrec(..), maybeParen,
181 pprTyVar, pprTcAppTy, pprPrefixApp, pprArrowChain,
182
183 -- * Tidying type related things up for printing
184 tidyType, tidyTypes,
185 tidyOpenType, tidyOpenTypes,
186 tidyOpenKind,
187 tidyTyCoVarBndr, tidyTyCoVarBndrs, tidyFreeTyCoVars,
188 tidyOpenTyCoVar, tidyOpenTyCoVars,
189 tidyTyVarOcc,
190 tidyTopType,
191 tidyKind
192 ) where
193
194 #include "HsVersions.h"
195
196 -- We import the representation and primitive functions from TyCoRep.
197 -- Many things are reexported, but not the representation!
198
199 import Kind
200 import TyCoRep
201
202 -- friends:
203 import Var
204 import VarEnv
205 import VarSet
206 import NameEnv
207
208 import Class
209 import TyCon
210 import TysPrim
211 import {-# SOURCE #-} TysWiredIn ( listTyCon, typeNatKind
212 , typeSymbolKind, liftedTypeKind )
213 import PrelNames
214 import CoAxiom
215 import {-# SOURCE #-} Coercion
216
217 -- others
218 import BasicTypes ( Arity, RepArity )
219 import Util
220 import Outputable
221 import FastString
222 import Pair
223 import ListSetOps
224 import Digraph
225
226 import Maybes ( orElse )
227 import Data.Maybe ( isJust, mapMaybe )
228 import Control.Monad ( guard )
229 import Control.Arrow ( first, second )
230
231 -- $type_classification
232 -- #type_classification#
233 --
234 -- Types are one of:
235 --
236 -- [Unboxed] Iff its representation is other than a pointer
237 -- Unboxed types are also unlifted.
238 --
239 -- [Lifted] Iff it has bottom as an element.
240 -- Closures always have lifted types: i.e. any
241 -- let-bound identifier in Core must have a lifted
242 -- type. Operationally, a lifted object is one that
243 -- can be entered.
244 -- Only lifted types may be unified with a type variable.
245 --
246 -- [Algebraic] Iff it is a type with one or more constructors, whether
247 -- declared with @data@ or @newtype@.
248 -- An algebraic type is one that can be deconstructed
249 -- with a case expression. This is /not/ the same as
250 -- lifted types, because we also include unboxed
251 -- tuples in this classification.
252 --
253 -- [Data] Iff it is a type declared with @data@, or a boxed tuple.
254 --
255 -- [Primitive] Iff it is a built-in type that can't be expressed in Haskell.
256 --
257 -- Currently, all primitive types are unlifted, but that's not necessarily
258 -- the case: for example, @Int@ could be primitive.
259 --
260 -- Some primitive types are unboxed, such as @Int#@, whereas some are boxed
261 -- but unlifted (such as @ByteArray#@). The only primitive types that we
262 -- classify as algebraic are the unboxed tuples.
263 --
264 -- Some examples of type classifications that may make this a bit clearer are:
265 --
266 -- @
267 -- Type primitive boxed lifted algebraic
268 -- -----------------------------------------------------------------------------
269 -- Int# Yes No No No
270 -- ByteArray# Yes Yes No No
271 -- (\# a, b \#) Yes No No Yes
272 -- ( a, b ) No Yes Yes Yes
273 -- [a] No Yes Yes Yes
274 -- @
275
276 -- $representation_types
277 -- A /source type/ is a type that is a separate type as far as the type checker is
278 -- concerned, but which has a more low-level representation as far as Core-to-Core
279 -- passes and the rest of the back end is concerned.
280 --
281 -- You don't normally have to worry about this, as the utility functions in
282 -- this module will automatically convert a source into a representation type
283 -- if they are spotted, to the best of it's abilities. If you don't want this
284 -- to happen, use the equivalent functions from the "TcType" module.
285
286 {-
287 ************************************************************************
288 * *
289 Type representation
290 * *
291 ************************************************************************
292 -}
293
294 {-# INLINE coreView #-}
295 coreView :: Type -> Maybe Type
296 -- ^ This function Strips off the /top layer only/ of a type synonym
297 -- application (if any) its underlying representation type.
298 -- Returns Nothing if there is nothing to look through.
299 --
300 -- By being non-recursive and inlined, this case analysis gets efficiently
301 -- joined onto the case analysis that the caller is already doing
302 coreView (TyConApp tc tys) | Just (tenv, rhs, tys') <- expandSynTyCon_maybe tc tys
303 = Just (mkAppTys (substTy (mkTvSubstPrs tenv) rhs) tys')
304 -- The free vars of 'rhs' should all be bound by 'tenv', so it's
305 -- ok to use 'substTy' here.
306 -- See also Note [The substitution invariant] in TyCoRep.
307 -- Its important to use mkAppTys, rather than (foldl AppTy),
308 -- because the function part might well return a
309 -- partially-applied type constructor; indeed, usually will!
310 coreView _ = Nothing
311
312 -- | Like 'coreView', but it also "expands" @Constraint@ to become
313 -- @TYPE PtrRepLifted@.
314 {-# INLINE coreViewOneStarKind #-}
315 coreViewOneStarKind :: Type -> Maybe Type
316 coreViewOneStarKind ty
317 | Just ty' <- coreView ty = Just ty'
318 | TyConApp tc [] <- ty
319 , isStarKindSynonymTyCon tc = Just liftedTypeKind
320 | otherwise = Nothing
321
322 -----------------------------------------------
323 expandTypeSynonyms :: Type -> Type
324 -- ^ Expand out all type synonyms. Actually, it'd suffice to expand out
325 -- just the ones that discard type variables (e.g. type Funny a = Int)
326 -- But we don't know which those are currently, so we just expand all.
327 --
328 -- 'expandTypeSynonyms' only expands out type synonyms mentioned in the type,
329 -- not in the kinds of any TyCon or TyVar mentioned in the type.
330 expandTypeSynonyms ty
331 = go (mkEmptyTCvSubst in_scope) ty
332 where
333 in_scope = mkInScopeSet (tyCoVarsOfType ty)
334
335 go subst (TyConApp tc tys)
336 | Just (tenv, rhs, tys') <- expandSynTyCon_maybe tc expanded_tys
337 = let subst' = mkTvSubst in_scope (mkVarEnv tenv)
338 -- Make a fresh substitution; rhs has nothing to
339 -- do with anything that has happened so far
340 -- NB: if you make changes here, be sure to build an
341 -- /idempotent/ substitution, even in the nested case
342 -- type T a b = a -> b
343 -- type S x y = T y x
344 -- (Trac #11665)
345 in mkAppTys (go subst' rhs) tys'
346 | otherwise
347 = TyConApp tc expanded_tys
348 where
349 expanded_tys = (map (go subst) tys)
350
351 go _ (LitTy l) = LitTy l
352 go subst (TyVarTy tv) = substTyVar subst tv
353 go subst (AppTy t1 t2) = mkAppTy (go subst t1) (go subst t2)
354 go subst (ForAllTy (Anon arg) res)
355 = mkFunTy (go subst arg) (go subst res)
356 go subst (ForAllTy (Named tv vis) t)
357 = let (subst', tv') = substTyVarBndrCallback go subst tv in
358 ForAllTy (Named tv' vis) (go subst' t)
359 go subst (CastTy ty co) = mkCastTy (go subst ty) (go_co subst co)
360 go subst (CoercionTy co) = mkCoercionTy (go_co subst co)
361
362 go_co subst (Refl r ty)
363 = mkReflCo r (go subst ty)
364 -- NB: coercions are always expanded upon creation
365 go_co subst (TyConAppCo r tc args)
366 = mkTyConAppCo r tc (map (go_co subst) args)
367 go_co subst (AppCo co arg)
368 = mkAppCo (go_co subst co) (go_co subst arg)
369 go_co subst (ForAllCo tv kind_co co)
370 = let (subst', tv', kind_co') = go_cobndr subst tv kind_co in
371 mkForAllCo tv' kind_co' (go_co subst' co)
372 go_co subst (CoVarCo cv)
373 = substCoVar subst cv
374 go_co subst (AxiomInstCo ax ind args)
375 = mkAxiomInstCo ax ind (map (go_co subst) args)
376 go_co subst (UnivCo p r t1 t2)
377 = mkUnivCo (go_prov subst p) r (go subst t1) (go subst t2)
378 go_co subst (SymCo co)
379 = mkSymCo (go_co subst co)
380 go_co subst (TransCo co1 co2)
381 = mkTransCo (go_co subst co1) (go_co subst co2)
382 go_co subst (NthCo n co)
383 = mkNthCo n (go_co subst co)
384 go_co subst (LRCo lr co)
385 = mkLRCo lr (go_co subst co)
386 go_co subst (InstCo co arg)
387 = mkInstCo (go_co subst co) (go_co subst arg)
388 go_co subst (CoherenceCo co1 co2)
389 = mkCoherenceCo (go_co subst co1) (go_co subst co2)
390 go_co subst (KindCo co)
391 = mkKindCo (go_co subst co)
392 go_co subst (SubCo co)
393 = mkSubCo (go_co subst co)
394 go_co subst (AxiomRuleCo ax cs) = AxiomRuleCo ax (map (go_co subst) cs)
395
396 go_prov _ UnsafeCoerceProv = UnsafeCoerceProv
397 go_prov subst (PhantomProv co) = PhantomProv (go_co subst co)
398 go_prov subst (ProofIrrelProv co) = ProofIrrelProv (go_co subst co)
399 go_prov _ p@(PluginProv _) = p
400 go_prov _ (HoleProv h) = pprPanic "expandTypeSynonyms hit a hole" (ppr h)
401
402 -- the "False" and "const" are to accommodate the type of
403 -- substForAllCoBndrCallback, which is general enough to
404 -- handle coercion optimization (which sometimes swaps the
405 -- order of a coercion)
406 go_cobndr subst = substForAllCoBndrCallback False (go_co subst) subst
407
408 {-
409 ************************************************************************
410 * *
411 Analyzing types
412 * *
413 ************************************************************************
414
415 These functions do a map-like operation over types, performing some operation
416 on all variables and binding sites. Primarily used for zonking.
417
418 Note [Efficiency for mapCoercion ForAllCo case]
419 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
420 As noted in Note [Forall coercions] in TyCoRep, a ForAllCo is a bit redundant.
421 It stores a TyVar and a Coercion, where the kind of the TyVar always matches
422 the left-hand kind of the coercion. This is convenient lots of the time, but
423 not when mapping a function over a coercion.
424
425 The problem is that tcm_tybinder will affect the TyVar's kind and
426 mapCoercion will affect the Coercion, and we hope that the results will be
427 the same. Even if they are the same (which should generally happen with
428 correct algorithms), then there is an efficiency issue. In particular,
429 this problem seems to make what should be a linear algorithm into a potentially
430 exponential one. But it's only going to be bad in the case where there's
431 lots of foralls in the kinds of other foralls. Like this:
432
433 forall a : (forall b : (forall c : ...). ...). ...
434
435 This construction seems unlikely. So we'll do the inefficient, easy way
436 for now.
437
438 Note [Specialising mappers]
439 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
440 These INLINABLE pragmas are indispensable. mapType/mapCoercion are used
441 to implement zonking, and it's vital that they get specialised to the TcM
442 monad. This specialisation happens automatically (that is, without a
443 SPECIALISE pragma) as long as the definitions are INLINABLE. For example,
444 this one change made a 20% allocation difference in perf/compiler/T5030.
445
446 -}
447
448 -- | This describes how a "map" operation over a type/coercion should behave
449 data TyCoMapper env m
450 = TyCoMapper
451 { tcm_smart :: Bool -- ^ Should the new type be created with smart
452 -- constructors?
453 , tcm_tyvar :: env -> TyVar -> m Type
454 , tcm_covar :: env -> CoVar -> m Coercion
455 , tcm_hole :: env -> CoercionHole -> Role
456 -> Type -> Type -> m Coercion
457 -- ^ What to do with coercion holes. See Note [Coercion holes] in
458 -- TyCoRep.
459
460 , tcm_tybinder :: env -> TyVar -> VisibilityFlag -> m (env, TyVar)
461 -- ^ The returned env is used in the extended scope
462 }
463
464 {-# INLINABLE mapType #-} -- See Note [Specialising mappers]
465 mapType :: Monad m => TyCoMapper env m -> env -> Type -> m Type
466 mapType mapper@(TyCoMapper { tcm_smart = smart, tcm_tyvar = tyvar
467 , tcm_tybinder = tybinder })
468 env ty
469 = go ty
470 where
471 go (TyVarTy tv) = tyvar env tv
472 go (AppTy t1 t2) = mkappty <$> go t1 <*> go t2
473 go t@(TyConApp _ []) = return t -- avoid allocation in this exceedingly
474 -- common case (mostly, for *)
475 go (TyConApp tc tys) = mktyconapp tc <$> mapM go tys
476 go (ForAllTy (Anon arg) res) = mkfunty <$> go arg <*> go res
477 go (ForAllTy (Named tv vis) inner)
478 = do { (env', tv') <- tybinder env tv vis
479 ; inner' <- mapType mapper env' inner
480 ; return $ ForAllTy (Named tv' vis) inner' }
481 go ty@(LitTy {}) = return ty
482 go (CastTy ty co) = mkcastty <$> go ty <*> mapCoercion mapper env co
483 go (CoercionTy co) = CoercionTy <$> mapCoercion mapper env co
484
485 (mktyconapp, mkappty, mkcastty, mkfunty)
486 | smart = (mkTyConApp, mkAppTy, mkCastTy, mkFunTy)
487 | otherwise = (TyConApp, AppTy, CastTy, ForAllTy . Anon)
488
489 {-# INLINABLE mapCoercion #-} -- See Note [Specialising mappers]
490 mapCoercion :: Monad m
491 => TyCoMapper env m -> env -> Coercion -> m Coercion
492 mapCoercion mapper@(TyCoMapper { tcm_smart = smart, tcm_covar = covar
493 , tcm_hole = cohole, tcm_tybinder = tybinder })
494 env co
495 = go co
496 where
497 go (Refl r ty) = Refl r <$> mapType mapper env ty
498 go (TyConAppCo r tc args)
499 = mktyconappco r tc <$> mapM go args
500 go (AppCo c1 c2) = mkappco <$> go c1 <*> go c2
501 go (ForAllCo tv kind_co co)
502 = do { kind_co' <- go kind_co
503 ; (env', tv') <- tybinder env tv Invisible
504 ; co' <- mapCoercion mapper env' co
505 ; return $ mkforallco tv' kind_co' co' }
506 -- See Note [Efficiency for mapCoercion ForAllCo case]
507 go (CoVarCo cv) = covar env cv
508 go (AxiomInstCo ax i args)
509 = mkaxiominstco ax i <$> mapM go args
510 go (UnivCo (HoleProv hole) r t1 t2)
511 = cohole env hole r t1 t2
512 go (UnivCo p r t1 t2)
513 = mkunivco <$> go_prov p <*> pure r
514 <*> mapType mapper env t1 <*> mapType mapper env t2
515 go (SymCo co) = mksymco <$> go co
516 go (TransCo c1 c2) = mktransco <$> go c1 <*> go c2
517 go (AxiomRuleCo r cos) = AxiomRuleCo r <$> mapM go cos
518 go (NthCo i co) = mknthco i <$> go co
519 go (LRCo lr co) = mklrco lr <$> go co
520 go (InstCo co arg) = mkinstco <$> go co <*> go arg
521 go (CoherenceCo c1 c2) = mkcoherenceco <$> go c1 <*> go c2
522 go (KindCo co) = mkkindco <$> go co
523 go (SubCo co) = mksubco <$> go co
524
525 go_prov UnsafeCoerceProv = return UnsafeCoerceProv
526 go_prov (PhantomProv co) = PhantomProv <$> go co
527 go_prov (ProofIrrelProv co) = ProofIrrelProv <$> go co
528 go_prov p@(PluginProv _) = return p
529 go_prov (HoleProv _) = panic "mapCoercion"
530
531 ( mktyconappco, mkappco, mkaxiominstco, mkunivco
532 , mksymco, mktransco, mknthco, mklrco, mkinstco, mkcoherenceco
533 , mkkindco, mksubco, mkforallco)
534 | smart
535 = ( mkTyConAppCo, mkAppCo, mkAxiomInstCo, mkUnivCo
536 , mkSymCo, mkTransCo, mkNthCo, mkLRCo, mkInstCo, mkCoherenceCo
537 , mkKindCo, mkSubCo, mkForAllCo )
538 | otherwise
539 = ( TyConAppCo, AppCo, AxiomInstCo, UnivCo
540 , SymCo, TransCo, NthCo, LRCo, InstCo, CoherenceCo
541 , KindCo, SubCo, ForAllCo )
542
543 {-
544 ************************************************************************
545 * *
546 \subsection{Constructor-specific functions}
547 * *
548 ************************************************************************
549
550
551 ---------------------------------------------------------------------
552 TyVarTy
553 ~~~~~~~
554 -}
555
556 -- | Attempts to obtain the type variable underlying a 'Type', and panics with the
557 -- given message if this is not a type variable type. See also 'getTyVar_maybe'
558 getTyVar :: String -> Type -> TyVar
559 getTyVar msg ty = case getTyVar_maybe ty of
560 Just tv -> tv
561 Nothing -> panic ("getTyVar: " ++ msg)
562
563 isTyVarTy :: Type -> Bool
564 isTyVarTy ty = isJust (getTyVar_maybe ty)
565
566 -- | Attempts to obtain the type variable underlying a 'Type'
567 getTyVar_maybe :: Type -> Maybe TyVar
568 getTyVar_maybe ty | Just ty' <- coreView ty = getTyVar_maybe ty'
569 | otherwise = repGetTyVar_maybe ty
570
571 -- | If the type is a tyvar, possibly under a cast, returns it, along
572 -- with the coercion. Thus, the co is :: kind tv ~R kind type
573 getCastedTyVar_maybe :: Type -> Maybe (TyVar, Coercion)
574 getCastedTyVar_maybe ty | Just ty' <- coreView ty = getCastedTyVar_maybe ty'
575 getCastedTyVar_maybe (CastTy (TyVarTy tv) co) = Just (tv, co)
576 getCastedTyVar_maybe (TyVarTy tv)
577 = Just (tv, mkReflCo Nominal (tyVarKind tv))
578 getCastedTyVar_maybe _ = Nothing
579
580 -- | Attempts to obtain the type variable underlying a 'Type', without
581 -- any expansion
582 repGetTyVar_maybe :: Type -> Maybe TyVar
583 repGetTyVar_maybe (TyVarTy tv) = Just tv
584 repGetTyVar_maybe _ = Nothing
585
586 allDistinctTyVars :: [KindOrType] -> Bool
587 allDistinctTyVars tkvs = go emptyVarSet tkvs
588 where
589 go _ [] = True
590 go so_far (ty : tys)
591 = case getTyVar_maybe ty of
592 Nothing -> False
593 Just tv | tv `elemVarSet` so_far -> False
594 | otherwise -> go (so_far `extendVarSet` tv) tys
595
596 {-
597 ---------------------------------------------------------------------
598 AppTy
599 ~~~~~
600 We need to be pretty careful with AppTy to make sure we obey the
601 invariant that a TyConApp is always visibly so. mkAppTy maintains the
602 invariant: use it.
603
604 Note [Decomposing fat arrow c=>t]
605 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
606 Can we unify (a b) with (Eq a => ty)? If we do so, we end up with
607 a partial application like ((=>) Eq a) which doesn't make sense in
608 source Haskell. In constrast, we *can* unify (a b) with (t1 -> t2).
609 Here's an example (Trac #9858) of how you might do it:
610 i :: (Typeable a, Typeable b) => Proxy (a b) -> TypeRep
611 i p = typeRep p
612
613 j = i (Proxy :: Proxy (Eq Int => Int))
614 The type (Proxy (Eq Int => Int)) is only accepted with -XImpredicativeTypes,
615 but suppose we want that. But then in the call to 'i', we end
616 up decomposing (Eq Int => Int), and we definitely don't want that.
617
618 This really only applies to the type checker; in Core, '=>' and '->'
619 are the same, as are 'Constraint' and '*'. But for now I've put
620 the test in repSplitAppTy_maybe, which applies throughout, because
621 the other calls to splitAppTy are in Unify, which is also used by
622 the type checker (e.g. when matching type-function equations).
623
624 -}
625
626 -- | Applies a type to another, as in e.g. @k a@
627 mkAppTy :: Type -> Type -> Type
628 mkAppTy (TyConApp tc tys) ty2 = mkTyConApp tc (tys ++ [ty2])
629 mkAppTy ty1 ty2 = AppTy ty1 ty2
630 -- Note that the TyConApp could be an
631 -- under-saturated type synonym. GHC allows that; e.g.
632 -- type Foo k = k a -> k a
633 -- type Id x = x
634 -- foo :: Foo Id -> Foo Id
635 --
636 -- Here Id is partially applied in the type sig for Foo,
637 -- but once the type synonyms are expanded all is well
638
639 mkAppTys :: Type -> [Type] -> Type
640 mkAppTys ty1 [] = ty1
641 mkAppTys (TyConApp tc tys1) tys2 = mkTyConApp tc (tys1 ++ tys2)
642 mkAppTys ty1 tys2 = foldl AppTy ty1 tys2
643
644 -------------
645 splitAppTy_maybe :: Type -> Maybe (Type, Type)
646 -- ^ Attempt to take a type application apart, whether it is a
647 -- function, type constructor, or plain type application. Note
648 -- that type family applications are NEVER unsaturated by this!
649 splitAppTy_maybe ty | Just ty' <- coreView ty
650 = splitAppTy_maybe ty'
651 splitAppTy_maybe ty = repSplitAppTy_maybe ty
652
653 -------------
654 repSplitAppTy_maybe :: Type -> Maybe (Type,Type)
655 -- ^ Does the AppTy split as in 'splitAppTy_maybe', but assumes that
656 -- any Core view stuff is already done
657 repSplitAppTy_maybe (ForAllTy (Anon ty1) ty2)
658 = Just (TyConApp funTyCon [ty1], ty2)
659 repSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2)
660 repSplitAppTy_maybe (TyConApp tc tys)
661 | mightBeUnsaturatedTyCon tc || tys `lengthExceeds` tyConArity tc
662 , Just (tys', ty') <- snocView tys
663 = Just (TyConApp tc tys', ty') -- Never create unsaturated type family apps!
664 repSplitAppTy_maybe _other = Nothing
665
666 -- this one doesn't braek apart (c => t).
667 -- See Note [Decomposing fat arrow c=>t]
668 -- Defined here to avoid module loops between Unify and TcType.
669 tcRepSplitAppTy_maybe :: Type -> Maybe (Type,Type)
670 -- ^ Does the AppTy split as in 'tcSplitAppTy_maybe', but assumes that
671 -- any coreView stuff is already done. Refuses to look through (c => t)
672 tcRepSplitAppTy_maybe (ForAllTy (Anon ty1) ty2)
673 | isConstraintKind (typeKind ty1) = Nothing -- See Note [Decomposing fat arrow c=>t]
674 | otherwise = Just (TyConApp funTyCon [ty1], ty2)
675 tcRepSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2)
676 tcRepSplitAppTy_maybe (TyConApp tc tys)
677 | mightBeUnsaturatedTyCon tc || tys `lengthExceeds` tyConArity tc
678 , Just (tys', ty') <- snocView tys
679 = Just (TyConApp tc tys', ty') -- Never create unsaturated type family apps!
680 tcRepSplitAppTy_maybe _other = Nothing
681 -------------
682 splitAppTy :: Type -> (Type, Type)
683 -- ^ Attempts to take a type application apart, as in 'splitAppTy_maybe',
684 -- and panics if this is not possible
685 splitAppTy ty = case splitAppTy_maybe ty of
686 Just pr -> pr
687 Nothing -> panic "splitAppTy"
688
689 -------------
690 splitAppTys :: Type -> (Type, [Type])
691 -- ^ Recursively splits a type as far as is possible, leaving a residual
692 -- type being applied to and the type arguments applied to it. Never fails,
693 -- even if that means returning an empty list of type applications.
694 splitAppTys ty = split ty ty []
695 where
696 split orig_ty ty args | Just ty' <- coreView ty = split orig_ty ty' args
697 split _ (AppTy ty arg) args = split ty ty (arg:args)
698 split _ (TyConApp tc tc_args) args
699 = let -- keep type families saturated
700 n | mightBeUnsaturatedTyCon tc = 0
701 | otherwise = tyConArity tc
702 (tc_args1, tc_args2) = splitAt n tc_args
703 in
704 (TyConApp tc tc_args1, tc_args2 ++ args)
705 split _ (ForAllTy (Anon ty1) ty2) args = ASSERT( null args )
706 (TyConApp funTyCon [], [ty1,ty2])
707 split orig_ty _ args = (orig_ty, args)
708
709 -- | Like 'splitAppTys', but doesn't look through type synonyms
710 repSplitAppTys :: Type -> (Type, [Type])
711 repSplitAppTys ty = split ty []
712 where
713 split (AppTy ty arg) args = split ty (arg:args)
714 split (TyConApp tc tc_args) args
715 = let n | mightBeUnsaturatedTyCon tc = 0
716 | otherwise = tyConArity tc
717 (tc_args1, tc_args2) = splitAt n tc_args
718 in
719 (TyConApp tc tc_args1, tc_args2 ++ args)
720 split (ForAllTy (Anon ty1) ty2) args = ASSERT( null args )
721 (TyConApp funTyCon [], [ty1, ty2])
722 split ty args = (ty, args)
723
724 {-
725 LitTy
726 ~~~~~
727 -}
728
729 mkNumLitTy :: Integer -> Type
730 mkNumLitTy n = LitTy (NumTyLit n)
731
732 -- | Is this a numeric literal. We also look through type synonyms.
733 isNumLitTy :: Type -> Maybe Integer
734 isNumLitTy ty | Just ty1 <- coreView ty = isNumLitTy ty1
735 isNumLitTy (LitTy (NumTyLit n)) = Just n
736 isNumLitTy _ = Nothing
737
738 mkStrLitTy :: FastString -> Type
739 mkStrLitTy s = LitTy (StrTyLit s)
740
741 -- | Is this a symbol literal. We also look through type synonyms.
742 isStrLitTy :: Type -> Maybe FastString
743 isStrLitTy ty | Just ty1 <- coreView ty = isStrLitTy ty1
744 isStrLitTy (LitTy (StrTyLit s)) = Just s
745 isStrLitTy _ = Nothing
746
747
748 -- | Is this type a custom user error?
749 -- If so, give us the kind and the error message.
750 userTypeError_maybe :: Type -> Maybe Type
751 userTypeError_maybe t
752 = do { (tc, _kind : msg : _) <- splitTyConApp_maybe t
753 -- There may be more than 2 arguments, if the type error is
754 -- used as a type constructor (e.g. at kind `Type -> Type`).
755
756 ; guard (tyConName tc == errorMessageTypeErrorFamName)
757 ; return msg }
758
759 -- | Render a type corresponding to a user type error into a SDoc.
760 pprUserTypeErrorTy :: Type -> SDoc
761 pprUserTypeErrorTy ty =
762 case splitTyConApp_maybe ty of
763
764 -- Text "Something"
765 Just (tc,[txt])
766 | tyConName tc == typeErrorTextDataConName
767 , Just str <- isStrLitTy txt -> ftext str
768
769 -- ShowType t
770 Just (tc,[_k,t])
771 | tyConName tc == typeErrorShowTypeDataConName -> ppr t
772
773 -- t1 :<>: t2
774 Just (tc,[t1,t2])
775 | tyConName tc == typeErrorAppendDataConName ->
776 pprUserTypeErrorTy t1 <> pprUserTypeErrorTy t2
777
778 -- t1 :$$: t2
779 Just (tc,[t1,t2])
780 | tyConName tc == typeErrorVAppendDataConName ->
781 pprUserTypeErrorTy t1 $$ pprUserTypeErrorTy t2
782
783 -- An uneavaluated type function
784 _ -> ppr ty
785
786
787
788
789 {-
790 ---------------------------------------------------------------------
791 FunTy
792 ~~~~~
793
794 Function types are represented with (ForAllTy (Anon ...) ...)
795 -}
796
797 isFunTy :: Type -> Bool
798 isFunTy ty = isJust (splitFunTy_maybe ty)
799
800 splitFunTy :: Type -> (Type, Type)
801 -- ^ Attempts to extract the argument and result types from a type, and
802 -- panics if that is not possible. See also 'splitFunTy_maybe'
803 splitFunTy ty | Just ty' <- coreView ty = splitFunTy ty'
804 splitFunTy (ForAllTy (Anon arg) res) = (arg, res)
805 splitFunTy other = pprPanic "splitFunTy" (ppr other)
806
807 splitFunTy_maybe :: Type -> Maybe (Type, Type)
808 -- ^ Attempts to extract the argument and result types from a type
809 splitFunTy_maybe ty | Just ty' <- coreView ty = splitFunTy_maybe ty'
810 splitFunTy_maybe (ForAllTy (Anon arg) res) = Just (arg, res)
811 splitFunTy_maybe _ = Nothing
812
813 splitFunTys :: Type -> ([Type], Type)
814 splitFunTys ty = split [] ty ty
815 where
816 split args orig_ty ty | Just ty' <- coreView ty = split args orig_ty ty'
817 split args _ (ForAllTy (Anon arg) res) = split (arg:args) res res
818 split args orig_ty _ = (reverse args, orig_ty)
819
820 splitFunTysN :: Int -> Type -> ([Type], Type)
821 -- ^ Split off exactly the given number argument types, and panics if that is not possible
822 splitFunTysN 0 ty = ([], ty)
823 splitFunTysN n ty = ASSERT2( isFunTy ty, int n <+> ppr ty )
824 case splitFunTy ty of { (arg, res) ->
825 case splitFunTysN (n-1) res of { (args, res) ->
826 (arg:args, res) }}
827
828 funResultTy :: Type -> Type
829 -- ^ Extract the function result type and panic if that is not possible
830 funResultTy ty | Just ty' <- coreView ty = funResultTy ty'
831 funResultTy (ForAllTy (Anon {}) res) = res
832 funResultTy ty = pprPanic "funResultTy" (ppr ty)
833
834 funArgTy :: Type -> Type
835 -- ^ Extract the function argument type and panic if that is not possible
836 funArgTy ty | Just ty' <- coreView ty = funArgTy ty'
837 funArgTy (ForAllTy (Anon arg) _res) = arg
838 funArgTy ty = pprPanic "funArgTy" (ppr ty)
839
840 piResultTy :: Type -> Type -> Type
841 -- ^ Just like 'piResultTys' but for a single argument
842 -- Try not to iterate 'piResultTy', because it's inefficient to substitute
843 -- one variable at a time; instead use 'piResultTys"
844 piResultTy ty arg
845 | Just ty' <- coreView ty = piResultTy ty' arg
846
847 | ForAllTy bndr res <- ty
848 = case bndr of
849 Anon {} -> res
850 Named tv _ -> substTy (extendTvSubst empty_subst tv arg) res
851 where
852 empty_subst = mkEmptyTCvSubst $ mkInScopeSet $
853 tyCoVarsOfTypes [arg,res]
854 | otherwise
855 = panic "piResultTys"
856
857 -- | (piResultTys f_ty [ty1, .., tyn]) gives the type of (f ty1 .. tyn)
858 -- where f :: f_ty
859 -- 'piResultTys' is interesting because:
860 -- 1. 'f_ty' may have more for-alls than there are args
861 -- 2. Less obviously, it may have fewer for-alls
862 -- For case 2. think of:
863 -- piResultTys (forall a.a) [forall b.b, Int]
864 -- This really can happen, but only (I think) in situations involving
865 -- undefined. For example:
866 -- undefined :: forall a. a
867 -- Term: undefined @(forall b. b->b) @Int
868 -- This term should have type (Int -> Int), but notice that
869 -- there are more type args than foralls in 'undefined's type.
870
871 -- If you edit this function, you may need to update the GHC formalism
872 -- See Note [GHC Formalism] in coreSyn/CoreLint.hs
873
874 -- This is a heavily used function (e.g. from typeKind),
875 -- so we pay attention to efficiency, especially in the special case
876 -- where there are no for-alls so we are just dropping arrows from
877 -- a function type/kind.
878 piResultTys :: Type -> [Type] -> Type
879 piResultTys ty [] = ty
880 piResultTys ty orig_args@(arg:args)
881 | Just ty' <- coreView ty
882 = piResultTys ty' orig_args
883
884 | ForAllTy bndr res <- ty
885 = case bndr of
886 Anon {} -> piResultTys res args
887 Named tv _ -> go (extendVarEnv emptyTvSubstEnv tv arg) res args
888
889 | otherwise
890 = panic "piResultTys"
891 where
892 go :: TvSubstEnv -> Type -> [Type] -> Type
893 go tv_env ty [] = substTy (mkTvSubst in_scope tv_env) ty
894 where
895 in_scope = mkInScopeSet (tyCoVarsOfTypes (ty:orig_args))
896
897 go tv_env ty all_args@(arg:args)
898 | Just ty' <- coreView ty
899 = go tv_env ty' all_args
900
901 | ForAllTy bndr res <- ty
902 = case bndr of
903 Anon _ -> go tv_env res args
904 Named tv _ -> go (extendVarEnv tv_env tv arg) res args
905
906 | TyVarTy tv <- ty
907 , Just ty' <- lookupVarEnv tv_env tv
908 -- Deals with piResultTys (forall a. a) [forall b.b, Int]
909 = piResultTys ty' all_args
910
911 | otherwise
912 = panic "piResultTys"
913
914 {-
915 ---------------------------------------------------------------------
916 TyConApp
917 ~~~~~~~~
918 -}
919
920 -- | A key function: builds a 'TyConApp' or 'FunTy' as appropriate to
921 -- its arguments. Applies its arguments to the constructor from left to right.
922 mkTyConApp :: TyCon -> [Type] -> Type
923 mkTyConApp tycon tys
924 | isFunTyCon tycon, [ty1,ty2] <- tys
925 = ForAllTy (Anon ty1) ty2
926
927 | otherwise
928 = TyConApp tycon tys
929
930 -- splitTyConApp "looks through" synonyms, because they don't
931 -- mean a distinct type, but all other type-constructor applications
932 -- including functions are returned as Just ..
933
934 -- | Retrieve the tycon heading this type, if there is one. Does /not/
935 -- look through synonyms.
936 tyConAppTyConPicky_maybe :: Type -> Maybe TyCon
937 tyConAppTyConPicky_maybe (TyConApp tc _) = Just tc
938 tyConAppTyConPicky_maybe (ForAllTy (Anon _) _) = Just funTyCon
939 tyConAppTyConPicky_maybe _ = Nothing
940
941
942 -- | The same as @fst . splitTyConApp@
943 tyConAppTyCon_maybe :: Type -> Maybe TyCon
944 tyConAppTyCon_maybe ty | Just ty' <- coreView ty = tyConAppTyCon_maybe ty'
945 tyConAppTyCon_maybe (TyConApp tc _) = Just tc
946 tyConAppTyCon_maybe (ForAllTy (Anon _) _) = Just funTyCon
947 tyConAppTyCon_maybe _ = Nothing
948
949 tyConAppTyCon :: Type -> TyCon
950 tyConAppTyCon ty = tyConAppTyCon_maybe ty `orElse` pprPanic "tyConAppTyCon" (ppr ty)
951
952 -- | The same as @snd . splitTyConApp@
953 tyConAppArgs_maybe :: Type -> Maybe [Type]
954 tyConAppArgs_maybe ty | Just ty' <- coreView ty = tyConAppArgs_maybe ty'
955 tyConAppArgs_maybe (TyConApp _ tys) = Just tys
956 tyConAppArgs_maybe (ForAllTy (Anon arg) res) = Just [arg,res]
957 tyConAppArgs_maybe _ = Nothing
958
959 tyConAppArgs :: Type -> [Type]
960 tyConAppArgs ty = tyConAppArgs_maybe ty `orElse` pprPanic "tyConAppArgs" (ppr ty)
961
962 tyConAppArgN :: Int -> Type -> Type
963 -- Executing Nth
964 tyConAppArgN n ty
965 = case tyConAppArgs_maybe ty of
966 Just tys -> ASSERT2( n < length tys, ppr n <+> ppr tys ) tys `getNth` n
967 Nothing -> pprPanic "tyConAppArgN" (ppr n <+> ppr ty)
968
969 -- | Attempts to tease a type apart into a type constructor and the application
970 -- of a number of arguments to that constructor. Panics if that is not possible.
971 -- See also 'splitTyConApp_maybe'
972 splitTyConApp :: Type -> (TyCon, [Type])
973 splitTyConApp ty = case splitTyConApp_maybe ty of
974 Just stuff -> stuff
975 Nothing -> pprPanic "splitTyConApp" (ppr ty)
976
977 -- | Attempts to tease a type apart into a type constructor and the application
978 -- of a number of arguments to that constructor
979 splitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
980 splitTyConApp_maybe ty | Just ty' <- coreView ty = splitTyConApp_maybe ty'
981 splitTyConApp_maybe ty = repSplitTyConApp_maybe ty
982
983 -- | Like 'splitTyConApp_maybe', but doesn't look through synonyms. This
984 -- assumes the synonyms have already been dealt with.
985 repSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
986 repSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
987 repSplitTyConApp_maybe (ForAllTy (Anon arg) res) = Just (funTyCon, [arg,res])
988 repSplitTyConApp_maybe _ = Nothing
989
990 -- | Attempts to tease a list type apart and gives the type of the elements if
991 -- successful (looks through type synonyms)
992 splitListTyConApp_maybe :: Type -> Maybe Type
993 splitListTyConApp_maybe ty = case splitTyConApp_maybe ty of
994 Just (tc,[e]) | tc == listTyCon -> Just e
995 _other -> Nothing
996
997 -- | What is the role assigned to the next parameter of this type? Usually,
998 -- this will be 'Nominal', but if the type is a 'TyConApp', we may be able to
999 -- do better. The type does *not* have to be well-kinded when applied for this
1000 -- to work!
1001 nextRole :: Type -> Role
1002 nextRole ty
1003 | Just (tc, tys) <- splitTyConApp_maybe ty
1004 , let num_tys = length tys
1005 , num_tys < tyConArity tc
1006 = tyConRoles tc `getNth` num_tys
1007
1008 | otherwise
1009 = Nominal
1010
1011 newTyConInstRhs :: TyCon -> [Type] -> Type
1012 -- ^ Unwrap one 'layer' of newtype on a type constructor and its
1013 -- arguments, using an eta-reduced version of the @newtype@ if possible.
1014 -- This requires tys to have at least @newTyConInstArity tycon@ elements.
1015 newTyConInstRhs tycon tys
1016 = ASSERT2( tvs `leLength` tys, ppr tycon $$ ppr tys $$ ppr tvs )
1017 applyTysX tvs rhs tys
1018 where
1019 (tvs, rhs) = newTyConEtadRhs tycon
1020
1021 {-
1022 ---------------------------------------------------------------------
1023 CastTy
1024 ~~~~~~
1025 A casted type has its *kind* casted into something new.
1026
1027 Note [Weird typing rule for ForAllTy]
1028 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1029
1030 Here is the (truncated) typing rule for the dependent ForAllTy:
1031
1032 inner : kind
1033 ------------------------------------
1034 ForAllTy (Named tv vis) inner : kind
1035
1036 Note that neither the inner type nor for ForAllTy itself have to have
1037 kind *! But, it means that we should push any kind casts through the
1038 ForAllTy. The only trouble is avoiding capture.
1039
1040 -}
1041
1042 splitCastTy_maybe :: Type -> Maybe (Type, Coercion)
1043 splitCastTy_maybe ty | Just ty' <- coreView ty = splitCastTy_maybe ty'
1044 splitCastTy_maybe (CastTy ty co) = Just (ty, co)
1045 splitCastTy_maybe _ = Nothing
1046
1047 -- | Make a 'CastTy'. The Coercion must be nominal. This function looks
1048 -- at the entire structure of the type and coercion in an attempt to
1049 -- maintain representation invariance (that is, any two types that are `eqType`
1050 -- look the same). Be very wary of calling this in a loop.
1051 mkCastTy :: Type -> Coercion -> Type
1052 -- Running example:
1053 -- T :: forall k1. k1 -> forall k2. k2 -> Bool -> Maybe k1 -> *
1054 -- co :: * ~R X (maybe X is a newtype around *)
1055 -- ty = T Nat 3 Symbol "foo" True (Just 2)
1056 --
1057 -- We wish to "push" the cast down as far as possible. See also
1058 -- Note [Pushing down casts] in TyCoRep. Here is where we end
1059 -- up:
1060 --
1061 -- (T Nat 3 Symbol |> <Symbol> -> <Bool> -> <Maybe Nat> -> co)
1062 -- "foo" True (Just 2)
1063 --
1064 mkCastTy ty co | isReflexiveCo co = ty
1065 -- NB: Do the slow check here. This is important to keep the splitXXX
1066 -- functions working properly. Otherwise, we may end up with something
1067 -- like (((->) |> something_reflexive_but_not_obviously_so) biz baz)
1068 -- fails under splitFunTy_maybe. This happened with the cheaper check
1069 -- in test dependent/should_compile/dynamic-paper.
1070
1071 mkCastTy (CastTy ty co1) co2 = mkCastTy ty (co1 `mkTransCo` co2)
1072 -- See Note [Weird typing rule for ForAllTy]
1073 mkCastTy (ForAllTy (Named tv vis) inner_ty) co
1074 = -- have to make sure that pushing the co in doesn't capture the bound var
1075 let fvs = tyCoVarsOfCo co
1076 empty_subst = mkEmptyTCvSubst (mkInScopeSet fvs)
1077 (subst, tv') = substTyVarBndr empty_subst tv
1078 in
1079 ForAllTy (Named tv' vis) (substTy subst inner_ty `mkCastTy` co)
1080 mkCastTy ty co = -- NB: don't check if the coercion "from" type matches here;
1081 -- there may be unzonked variables about
1082 let result = split_apps [] ty co in
1083 ASSERT2( CastTy ty co `eqType` result
1084 , ppr ty <+> dcolon <+> ppr (typeKind ty) $$
1085 ppr co <+> dcolon <+> ppr (coercionKind co) $$
1086 ppr result <+> dcolon <+> ppr (typeKind result) )
1087 result
1088 where
1089 -- split_apps breaks apart any type applications, so we can see how far down
1090 -- to push the cast
1091 split_apps args (AppTy t1 t2) co
1092 = split_apps (t2:args) t1 co
1093 split_apps args (TyConApp tc tc_args) co
1094 | mightBeUnsaturatedTyCon tc
1095 = affix_co (tyConBinders tc) (mkTyConTy tc) (tc_args `chkAppend` args) co
1096 | otherwise -- not decomposable... but it may still be oversaturated
1097 = let (non_decomp_args, decomp_args) = splitAt (tyConArity tc) tc_args
1098 saturated_tc = mkTyConApp tc non_decomp_args
1099 in
1100 affix_co (fst $ splitPiTys $ typeKind saturated_tc)
1101 saturated_tc (decomp_args `chkAppend` args) co
1102
1103 split_apps args (ForAllTy (Anon arg) res) co
1104 = affix_co (tyConBinders funTyCon) (mkTyConTy funTyCon)
1105 (arg : res : args) co
1106 split_apps args ty co
1107 = affix_co (fst $ splitPiTys $ typeKind ty)
1108 ty args co
1109
1110 -- having broken everything apart, this figures out the point at which there
1111 -- are no more dependent quantifications, and puts the cast there
1112 affix_co _ ty [] co = no_double_casts ty co
1113 affix_co bndrs ty args co
1114 -- if kind contains any dependent quantifications, we can't push.
1115 -- apply arguments until it doesn't
1116 = let (no_dep_bndrs, some_dep_bndrs) = spanEnd isAnonBinder bndrs
1117 (some_dep_args, rest_args) = splitAtList some_dep_bndrs args
1118 dep_subst = zipTyBinderSubst some_dep_bndrs some_dep_args
1119 used_no_dep_bndrs = takeList rest_args no_dep_bndrs
1120 rest_arg_tys = substTys dep_subst (map binderType used_no_dep_bndrs)
1121 co' = mkFunCos Nominal
1122 (map (mkReflCo Nominal) rest_arg_tys)
1123 co
1124 in
1125 ((ty `mkAppTys` some_dep_args) `no_double_casts` co') `mkAppTys` rest_args
1126
1127 no_double_casts (CastTy ty co1) co2 = CastTy ty (co1 `mkTransCo` co2)
1128 no_double_casts ty co = CastTy ty co
1129
1130 {-
1131 --------------------------------------------------------------------
1132 CoercionTy
1133 ~~~~~~~~~~
1134 CoercionTy allows us to inject coercions into types. A CoercionTy
1135 should appear only in the right-hand side of an application.
1136 -}
1137
1138 mkCoercionTy :: Coercion -> Type
1139 mkCoercionTy = CoercionTy
1140
1141 isCoercionTy :: Type -> Bool
1142 isCoercionTy (CoercionTy _) = True
1143 isCoercionTy _ = False
1144
1145 isCoercionTy_maybe :: Type -> Maybe Coercion
1146 isCoercionTy_maybe (CoercionTy co) = Just co
1147 isCoercionTy_maybe _ = Nothing
1148
1149 stripCoercionTy :: Type -> Coercion
1150 stripCoercionTy (CoercionTy co) = co
1151 stripCoercionTy ty = pprPanic "stripCoercionTy" (ppr ty)
1152
1153 {-
1154 ---------------------------------------------------------------------
1155 SynTy
1156 ~~~~~
1157
1158 Notes on type synonyms
1159 ~~~~~~~~~~~~~~~~~~~~~~
1160 The various "split" functions (splitFunTy, splitRhoTy, splitForAllTy) try
1161 to return type synonyms wherever possible. Thus
1162
1163 type Foo a = a -> a
1164
1165 we want
1166 splitFunTys (a -> Foo a) = ([a], Foo a)
1167 not ([a], a -> a)
1168
1169 The reason is that we then get better (shorter) type signatures in
1170 interfaces. Notably this plays a role in tcTySigs in TcBinds.hs.
1171
1172
1173 Representation types
1174 ~~~~~~~~~~~~~~~~~~~~
1175
1176 Note [Nullary unboxed tuple]
1177 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1178 We represent the nullary unboxed tuple as the unary (but void) type
1179 Void#. The reason for this is that the ReprArity is never
1180 less than the Arity (as it would otherwise be for a function type like
1181 (# #) -> Int).
1182
1183 As a result, ReprArity is always strictly positive if Arity is. This
1184 is important because it allows us to distinguish at runtime between a
1185 thunk and a function takes a nullary unboxed tuple as an argument!
1186 -}
1187
1188 type UnaryType = Type
1189
1190 data RepType = UbxTupleRep [UnaryType] -- INVARIANT: never an empty list (see Note [Nullary unboxed tuple])
1191 | UnaryRep UnaryType
1192
1193 instance Outputable RepType where
1194 ppr (UbxTupleRep tys) = text "UbxTupleRep" <+> ppr tys
1195 ppr (UnaryRep ty) = text "UnaryRep" <+> ppr ty
1196
1197 flattenRepType :: RepType -> [UnaryType]
1198 flattenRepType (UbxTupleRep tys) = tys
1199 flattenRepType (UnaryRep ty) = [ty]
1200
1201 -- | Looks through:
1202 --
1203 -- 1. For-alls
1204 -- 2. Synonyms
1205 -- 3. Predicates
1206 -- 4. All newtypes, including recursive ones, but not newtype families
1207 -- 5. Casts
1208 --
1209 -- It's useful in the back end of the compiler.
1210 repType :: Type -> RepType
1211 repType ty
1212 = go initRecTc ty
1213 where
1214 go :: RecTcChecker -> Type -> RepType
1215 go rec_nts ty -- Expand predicates and synonyms
1216 | Just ty' <- coreView ty
1217 = go rec_nts ty'
1218
1219 go rec_nts (ForAllTy (Named {}) ty2) -- Drop type foralls
1220 = go rec_nts ty2
1221
1222 go rec_nts (TyConApp tc tys) -- Expand newtypes
1223 | isNewTyCon tc
1224 , tys `lengthAtLeast` tyConArity tc
1225 , Just rec_nts' <- checkRecTc rec_nts tc -- See Note [Expanding newtypes] in TyCon
1226 = go rec_nts' (newTyConInstRhs tc tys)
1227
1228 | isUnboxedTupleTyCon tc
1229 = if null tys
1230 then UnaryRep voidPrimTy -- See Note [Nullary unboxed tuple]
1231 else UbxTupleRep (concatMap (flattenRepType . go rec_nts) non_rr_tys)
1232 where
1233 -- See Note [Unboxed tuple RuntimeRep vars] in TyCon
1234 non_rr_tys = dropRuntimeRepArgs tys
1235
1236 go rec_nts (CastTy ty _)
1237 = go rec_nts ty
1238
1239 go _ ty@(CoercionTy _)
1240 = pprPanic "repType" (ppr ty)
1241
1242 go _ ty = UnaryRep ty
1243
1244 -- ToDo: this could be moved to the code generator, using splitTyConApp instead
1245 -- of inspecting the type directly.
1246
1247 -- | Discovers the primitive representation of a more abstract 'UnaryType'
1248 typePrimRep :: UnaryType -> PrimRep
1249 typePrimRep ty = kindPrimRep (typeKind ty)
1250
1251 -- | Find the primitive representation of a 'TyCon'. Defined here to
1252 -- avoid module loops. Call this only on unlifted tycons.
1253 tyConPrimRep :: TyCon -> PrimRep
1254 tyConPrimRep tc = kindPrimRep res_kind
1255 where
1256 res_kind = tyConResKind tc
1257
1258 -- | Take a kind (of shape @TYPE rr@) and produce the 'PrimRep' of values
1259 -- of types of this kind.
1260 kindPrimRep :: Kind -> PrimRep
1261 kindPrimRep ki | Just ki' <- coreViewOneStarKind ki = kindPrimRep ki'
1262 kindPrimRep (TyConApp typ [runtime_rep])
1263 = ASSERT( typ `hasKey` tYPETyConKey )
1264 go runtime_rep
1265 where
1266 go rr | Just rr' <- coreView rr = go rr'
1267 go (TyConApp rr_dc args)
1268 | RuntimeRep fun <- tyConRuntimeRepInfo rr_dc
1269 = fun args
1270 go rr = pprPanic "kindPrimRep.go" (ppr rr)
1271 kindPrimRep ki = WARN( True
1272 , text "kindPrimRep defaulting to PtrRep on" <+> ppr ki )
1273 PtrRep -- this can happen legitimately for, e.g., Any
1274
1275 typeRepArity :: Arity -> Type -> RepArity
1276 typeRepArity 0 _ = 0
1277 typeRepArity n ty = case repType ty of
1278 UnaryRep (ForAllTy bndr ty) -> length (flattenRepType (repType (binderType bndr))) + typeRepArity (n - 1) ty
1279 _ -> pprPanic "typeRepArity: arity greater than type can handle" (ppr (n, ty, repType ty))
1280
1281 isVoidTy :: Type -> Bool
1282 -- True if the type has zero width
1283 isVoidTy ty = case repType ty of
1284 UnaryRep (TyConApp tc _) -> isUnliftedTyCon tc &&
1285 isVoidRep (tyConPrimRep tc)
1286 _ -> False
1287
1288 {-
1289 Note [AppTy rep]
1290 ~~~~~~~~~~~~~~~~
1291 Types of the form 'f a' must be of kind *, not #, so we are guaranteed
1292 that they are represented by pointers. The reason is that f must have
1293 kind (kk -> kk) and kk cannot be unlifted; see Note [The kind invariant]
1294 in TyCoRep.
1295
1296 ---------------------------------------------------------------------
1297 ForAllTy
1298 ~~~~~~~~
1299 -}
1300
1301 mkForAllTy :: TyBinder -> Type -> Type
1302 mkForAllTy = ForAllTy
1303
1304 -- | Make a dependent forall.
1305 mkNamedForAllTy :: TyVar -> VisibilityFlag -> Type -> Type
1306 mkNamedForAllTy tv vis = ASSERT( isTyVar tv )
1307 ForAllTy (Named tv vis)
1308
1309 -- | Like mkForAllTys, but assumes all variables are dependent and invisible,
1310 -- a common case
1311 mkInvForAllTys :: [TyVar] -> Type -> Type
1312 mkInvForAllTys tvs = ASSERT( all isTyVar tvs )
1313 mkForAllTys (map (flip Named Invisible) tvs)
1314
1315 -- | Like mkForAllTys, but assumes all variables are dependent and specified,
1316 -- a common case
1317 mkSpecForAllTys :: [TyVar] -> Type -> Type
1318 mkSpecForAllTys tvs = ASSERT( all isTyVar tvs )
1319 mkForAllTys (map (flip Named Specified) tvs)
1320
1321 -- | Like mkForAllTys, but assumes all variables are dependent and visible
1322 mkVisForAllTys :: [TyVar] -> Type -> Type
1323 mkVisForAllTys tvs = ASSERT( all isTyVar tvs )
1324 mkForAllTys (map (flip Named Visible) tvs)
1325
1326 mkPiType :: Var -> Type -> Type
1327 -- ^ Makes a @(->)@ type or an implicit forall type, depending
1328 -- on whether it is given a type variable or a term variable.
1329 -- This is used, for example, when producing the type of a lambda.
1330 -- Always uses Invisible binders.
1331 mkPiTypes :: [Var] -> Type -> Type
1332 -- ^ 'mkPiType' for multiple type or value arguments
1333
1334 mkPiType v ty
1335 | isTyVar v = mkForAllTy (Named v Invisible) ty
1336 | otherwise = mkForAllTy (Anon (varType v)) ty
1337
1338 mkPiTypes vs ty = foldr mkPiType ty vs
1339
1340 -- | Given a list of type-level vars and a result type, makes TyBinders, preferring
1341 -- anonymous binders if the variable is, in fact, not dependent.
1342 -- All binders are /visible/.
1343 mkTyBindersPreferAnon :: [TyVar] -> Type -> [TyBinder]
1344 mkTyBindersPreferAnon vars inner_ty = fst $ go vars inner_ty
1345 where
1346 go :: [TyVar] -> Type -> ([TyBinder], VarSet) -- also returns the free vars
1347 go [] ty = ([], tyCoVarsOfType ty)
1348 go (v:vs) ty | v `elemVarSet` fvs
1349 = ( Named v Visible : binders
1350 , fvs `delVarSet` v `unionVarSet` kind_vars )
1351 | otherwise
1352 = ( Anon (tyVarKind v) : binders
1353 , fvs `unionVarSet` kind_vars )
1354 where
1355 (binders, fvs) = go vs ty
1356 kind_vars = tyCoVarsOfType $ tyVarKind v
1357
1358 -- | Take a ForAllTy apart, returning the list of tyvars and the result type.
1359 -- This always succeeds, even if it returns only an empty list. Note that the
1360 -- result type returned may have free variables that were bound by a forall.
1361 splitForAllTys :: Type -> ([TyVar], Type)
1362 splitForAllTys ty = split ty ty []
1363 where
1364 split orig_ty ty tvs | Just ty' <- coreView ty = split orig_ty ty' tvs
1365 split _ (ForAllTy (Named tv _) ty) tvs = split ty ty (tv:tvs)
1366 split orig_ty _ tvs = (reverse tvs, orig_ty)
1367
1368 -- | Split off all TyBinders to a type, splitting both proper foralls
1369 -- and functions
1370 splitPiTys :: Type -> ([TyBinder], Type)
1371 splitPiTys ty = split ty ty []
1372 where
1373 split orig_ty ty bs | Just ty' <- coreView ty = split orig_ty ty' bs
1374 split _ (ForAllTy b res) bs = split res res (b:bs)
1375 split orig_ty _ bs = (reverse bs, orig_ty)
1376
1377 -- | Like 'splitPiTys' but split off only /named/ binders.
1378 splitNamedPiTys :: Type -> ([TyBinder], Type)
1379 splitNamedPiTys ty = split ty ty []
1380 where
1381 split orig_ty ty bs | Just ty' <- coreView ty = split orig_ty ty' bs
1382 split _ (ForAllTy b@(Named {}) res) bs = split res res (b:bs)
1383 split orig_ty _ bs = (reverse bs, orig_ty)
1384
1385 -- | Checks whether this is a proper forall (with a named binder)
1386 isForAllTy :: Type -> Bool
1387 isForAllTy (ForAllTy (Named {}) _) = True
1388 isForAllTy _ = False
1389
1390 -- | Is this a function or forall?
1391 isPiTy :: Type -> Bool
1392 isPiTy (ForAllTy {}) = True
1393 isPiTy _ = False
1394
1395 -- | Take a forall type apart, or panics if that is not possible.
1396 splitForAllTy :: Type -> (TyVar, Type)
1397 splitForAllTy ty
1398 | Just answer <- splitForAllTy_maybe ty = answer
1399 | otherwise = pprPanic "splitForAllTy" (ppr ty)
1400
1401 -- | Attempts to take a forall type apart, but only if it's a proper forall,
1402 -- with a named binder
1403 splitForAllTy_maybe :: Type -> Maybe (TyVar, Type)
1404 splitForAllTy_maybe ty = splitFAT_m ty
1405 where
1406 splitFAT_m ty | Just ty' <- coreView ty = splitFAT_m ty'
1407 splitFAT_m (ForAllTy (Named tv _) ty) = Just (tv, ty)
1408 splitFAT_m _ = Nothing
1409
1410 -- | Attempts to take a forall type apart; works with proper foralls and
1411 -- functions
1412 splitPiTy_maybe :: Type -> Maybe (TyBinder, Type)
1413 splitPiTy_maybe ty = go ty
1414 where
1415 go ty | Just ty' <- coreView ty = go ty'
1416 go (ForAllTy bndr ty) = Just (bndr, ty)
1417 go _ = Nothing
1418
1419 -- | Takes a forall type apart, or panics
1420 splitPiTy :: Type -> (TyBinder, Type)
1421 splitPiTy ty
1422 | Just answer <- splitPiTy_maybe ty = answer
1423 | otherwise = pprPanic "splitPiTy" (ppr ty)
1424
1425 -- | Drops all non-anonymous ForAllTys
1426 dropForAlls :: Type -> Type
1427 dropForAlls ty | Just ty' <- coreView ty = dropForAlls ty'
1428 | otherwise = go ty
1429 where
1430 go (ForAllTy (Named {}) res) = go res
1431 go res = res
1432
1433 -- | Given a tycon and its arguments, filters out any invisible arguments
1434 filterOutInvisibleTypes :: TyCon -> [Type] -> [Type]
1435 filterOutInvisibleTypes tc tys = snd $ partitionInvisibles tc id tys
1436
1437 -- | Like 'filterOutInvisibles', but works on 'TyVar's
1438 filterOutInvisibleTyVars :: TyCon -> [TyVar] -> [TyVar]
1439 filterOutInvisibleTyVars tc tvs = snd $ partitionInvisibles tc mkTyVarTy tvs
1440
1441 -- | Given a tycon and a list of things (which correspond to arguments),
1442 -- partitions the things into the invisible ones and the visible ones.
1443 -- The callback function is necessary for this scenario:
1444 --
1445 -- > T :: forall k. k -> k
1446 -- > partitionInvisibles T [forall m. m -> m -> m, S, R, Q]
1447 --
1448 -- After substituting, we get
1449 --
1450 -- > T (forall m. m -> m -> m) :: (forall m. m -> m -> m) -> forall n. n -> n -> n
1451 --
1452 -- Thus, the first argument is invisible, @S@ is visible, @R@ is invisible again,
1453 -- and @Q@ is visible.
1454 --
1455 -- If you're absolutely sure that your tycon's kind doesn't end in a variable,
1456 -- it's OK if the callback function panics, as that's the only time it's
1457 -- consulted.
1458 partitionInvisibles :: TyCon -> (a -> Type) -> [a] -> ([a], [a])
1459 partitionInvisibles tc get_ty = go emptyTCvSubst (tyConKind tc)
1460 where
1461 go _ _ [] = ([], [])
1462 go subst (ForAllTy bndr res_ki) (x:xs)
1463 | isVisibleBinder bndr = second (x :) (go subst' res_ki xs)
1464 | otherwise = first (x :) (go subst' res_ki xs)
1465 where
1466 subst' = extendTvSubstBinder subst bndr (get_ty x)
1467 go subst (TyVarTy tv) xs
1468 | Just ki <- lookupTyVar subst tv = go subst ki xs
1469 go _ _ xs = ([], xs) -- something is ill-kinded. But this can happen
1470 -- when printing errors. Assume everything is visible.
1471
1472 -- like splitPiTys, but returns only *invisible* binders, including constraints
1473 splitPiTysInvisible :: Type -> ([TyBinder], Type)
1474 splitPiTysInvisible ty = split ty ty []
1475 where
1476 split orig_ty ty bndrs
1477 | Just ty' <- coreView ty = split orig_ty ty' bndrs
1478 split _ (ForAllTy bndr ty) bndrs
1479 | isInvisibleBinder bndr
1480 = split ty ty (bndr:bndrs)
1481
1482 split orig_ty _ bndrs
1483 = (reverse bndrs, orig_ty)
1484
1485 applyTysX :: [TyVar] -> Type -> [Type] -> Type
1486 -- applyTyxX beta-reduces (/\tvs. body_ty) arg_tys
1487 -- Assumes that (/\tvs. body_ty) is closed
1488 applyTysX tvs body_ty arg_tys
1489 = ASSERT2( length arg_tys >= n_tvs, pp_stuff )
1490 ASSERT2( tyCoVarsOfType body_ty `subVarSet` mkVarSet tvs, pp_stuff )
1491 mkAppTys (substTyWith tvs (take n_tvs arg_tys) body_ty)
1492 (drop n_tvs arg_tys)
1493 where
1494 pp_stuff = vcat [ppr tvs, ppr body_ty, ppr arg_tys]
1495 n_tvs = length tvs
1496
1497 {-
1498 %************************************************************************
1499 %* *
1500 TyBinders
1501 %* *
1502 %************************************************************************
1503 -}
1504
1505 -- | Make a named binder
1506 mkNamedBinder :: VisibilityFlag -> Var -> TyBinder
1507 mkNamedBinder vis var = Named var vis
1508
1509 -- | Make an anonymous binder
1510 mkAnonBinder :: Type -> TyBinder
1511 mkAnonBinder = Anon
1512
1513 -- | Does this binder bind a variable that is /not/ erased? Returns
1514 -- 'True' for anonymous binders.
1515 isIdLikeBinder :: TyBinder -> Bool
1516 isIdLikeBinder (Named {}) = False
1517 isIdLikeBinder (Anon {}) = True
1518
1519 -- | Does this type, when used to the left of an arrow, require
1520 -- a visible argument? This checks to see if the kind of the type
1521 -- is constraint.
1522 isVisibleType :: Type -> Bool
1523 isVisibleType = not . isPredTy
1524
1525 binderVisibility :: TyBinder -> VisibilityFlag
1526 binderVisibility (Named _ vis) = vis
1527 binderVisibility (Anon ty)
1528 | isVisibleType ty = Visible
1529 | otherwise = Invisible
1530
1531 -- | Extract a bound variable in a binder, if any
1532 binderVar_maybe :: TyBinder -> Maybe Var
1533 binderVar_maybe (Named v _) = Just v
1534 binderVar_maybe (Anon {}) = Nothing
1535
1536 -- | Extract a bound variable in a binder, or panics
1537 binderVar :: String -- ^ printed if there is a panic
1538 -> TyBinder -> Var
1539 binderVar _ (Named v _) = v
1540 binderVar e (Anon t) = pprPanic ("binderVar (" ++ e ++ ")") (ppr t)
1541
1542 -- | Extract a relevant type, if there is one.
1543 binderRelevantType_maybe :: TyBinder -> Maybe Type
1544 binderRelevantType_maybe (Named {}) = Nothing
1545 binderRelevantType_maybe (Anon ty) = Just ty
1546
1547 -- | Like 'maybe', but for binders.
1548 caseBinder :: TyBinder -- ^ binder to scrutinize
1549 -> (TyVar -> a) -- ^ named case
1550 -> (Type -> a) -- ^ anonymous case
1551 -> a
1552 caseBinder (Named v _) f _ = f v
1553 caseBinder (Anon t) _ d = d t
1554
1555 -- | Break apart a list of binders into tyvars and anonymous types.
1556 partitionBinders :: [TyBinder] -> ([TyVar], [Type])
1557 partitionBinders = partitionWith named_or_anon
1558 where
1559 named_or_anon bndr = caseBinder bndr Left Right
1560
1561 -- | Break apart a list of binders into a list of named binders and
1562 -- a list of anonymous types.
1563 partitionBindersIntoBinders :: [TyBinder] -> ([TyBinder], [Type])
1564 partitionBindersIntoBinders = partitionWith named_or_anon
1565 where
1566 named_or_anon bndr = caseBinder bndr (\_ -> Left bndr) Right
1567
1568 {-
1569 %************************************************************************
1570 %* *
1571 Pred
1572 * *
1573 ************************************************************************
1574
1575 Predicates on PredType
1576
1577 Note [isPredTy complications]
1578 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1579 You would think that we could define
1580 isPredTy ty = isConstraintKind (typeKind ty)
1581 But there are a number of complications:
1582
1583 * isPredTy is used when printing types, which can happen in debug
1584 printing during type checking of not-fully-zonked types. So it's
1585 not cool to say isConstraintKind (typeKind ty) because, absent
1586 zonking, the type might be ill-kinded, and typeKind crashes. Hence the
1587 rather tiresome story here
1588
1589 * isPredTy must return "True" to *unlifted* coercions, such as (t1 ~# t2)
1590 and (t1 ~R# t2), which are not of kind Constraint! Currently they are
1591 of kind #.
1592
1593 * If we do form the type '(C a => C [a]) => blah', then we'd like to
1594 print it as such. But that means that isPredTy must return True for
1595 (C a => C [a]). Admittedly that type is illegal in Haskell, but we
1596 want to print it nicely in error messages.
1597 -}
1598
1599 -- | Is the type suitable to classify a given/wanted in the typechecker?
1600 isPredTy :: Type -> Bool
1601 -- See Note [isPredTy complications]
1602 isPredTy ty = go ty []
1603 where
1604 go :: Type -> [KindOrType] -> Bool
1605 go (AppTy ty1 ty2) args = go ty1 (ty2 : args)
1606 go (TyVarTy tv) args = go_k (tyVarKind tv) args
1607 go (TyConApp tc tys) args = ASSERT( null args ) -- TyConApp invariant
1608 go_tc tc tys
1609 go (ForAllTy (Anon arg) res) []
1610 | isPredTy arg = isPredTy res -- (Eq a => C a)
1611 | otherwise = False -- (Int -> Bool)
1612 go (ForAllTy (Named {}) ty) [] = go ty []
1613 go _ _ = False
1614
1615 go_tc :: TyCon -> [KindOrType] -> Bool
1616 go_tc tc args
1617 | tc `hasKey` eqPrimTyConKey || tc `hasKey` eqReprPrimTyConKey
1618 = length args == 4 -- ~# and ~R# sadly have result kind #
1619 -- not Contraint; but we still want
1620 -- isPredTy to reply True.
1621 | otherwise = go_k (tyConKind tc) args
1622
1623 go_k :: Kind -> [KindOrType] -> Bool
1624 -- True <=> ('k' applied to 'kts') = Constraint
1625 go_k k args = isConstraintKind (piResultTys k args)
1626
1627 isClassPred, isEqPred, isNomEqPred, isIPPred :: PredType -> Bool
1628 isClassPred ty = case tyConAppTyCon_maybe ty of
1629 Just tyCon | isClassTyCon tyCon -> True
1630 _ -> False
1631 isEqPred ty = case tyConAppTyCon_maybe ty of
1632 Just tyCon -> tyCon `hasKey` eqPrimTyConKey
1633 || tyCon `hasKey` eqReprPrimTyConKey
1634 _ -> False
1635
1636 isNomEqPred ty = case tyConAppTyCon_maybe ty of
1637 Just tyCon -> tyCon `hasKey` eqPrimTyConKey
1638 _ -> False
1639
1640 isIPPred ty = case tyConAppTyCon_maybe ty of
1641 Just tc -> isIPTyCon tc
1642 _ -> False
1643
1644 isIPTyCon :: TyCon -> Bool
1645 isIPTyCon tc = tc `hasKey` ipClassKey
1646 -- Class and its corresponding TyCon have the same Unique
1647
1648 isIPClass :: Class -> Bool
1649 isIPClass cls = cls `hasKey` ipClassKey
1650
1651 isCTupleClass :: Class -> Bool
1652 isCTupleClass cls = isTupleTyCon (classTyCon cls)
1653
1654 isIPPred_maybe :: Type -> Maybe (FastString, Type)
1655 isIPPred_maybe ty =
1656 do (tc,[t1,t2]) <- splitTyConApp_maybe ty
1657 guard (isIPTyCon tc)
1658 x <- isStrLitTy t1
1659 return (x,t2)
1660
1661 {-
1662 Make PredTypes
1663
1664 --------------------- Equality types ---------------------------------
1665 -}
1666
1667 -- | Makes a lifted equality predicate at the given role
1668 mkPrimEqPredRole :: Role -> Type -> Type -> PredType
1669 mkPrimEqPredRole Nominal = mkPrimEqPred
1670 mkPrimEqPredRole Representational = mkReprPrimEqPred
1671 mkPrimEqPredRole Phantom = panic "mkPrimEqPredRole phantom"
1672
1673 -- | Creates a primitive type equality predicate.
1674 -- Invariant: the types are not Coercions
1675 mkPrimEqPred :: Type -> Type -> Type
1676 mkPrimEqPred ty1 ty2
1677 = TyConApp eqPrimTyCon [k1, k2, ty1, ty2]
1678 where
1679 k1 = typeKind ty1
1680 k2 = typeKind ty2
1681
1682 -- | Creates a primite type equality predicate with explicit kinds
1683 mkHeteroPrimEqPred :: Kind -> Kind -> Type -> Type -> Type
1684 mkHeteroPrimEqPred k1 k2 ty1 ty2 = TyConApp eqPrimTyCon [k1, k2, ty1, ty2]
1685
1686 -- | Creates a primitive representational type equality predicate
1687 -- with explicit kinds
1688 mkHeteroReprPrimEqPred :: Kind -> Kind -> Type -> Type -> Type
1689 mkHeteroReprPrimEqPred k1 k2 ty1 ty2
1690 = TyConApp eqReprPrimTyCon [k1, k2, ty1, ty2]
1691
1692 -- | Try to split up a coercion type into the types that it coerces
1693 splitCoercionType_maybe :: Type -> Maybe (Type, Type)
1694 splitCoercionType_maybe ty
1695 = do { (tc, [_, _, ty1, ty2]) <- splitTyConApp_maybe ty
1696 ; guard $ tc `hasKey` eqPrimTyConKey || tc `hasKey` eqReprPrimTyConKey
1697 ; return (ty1, ty2) }
1698
1699 mkReprPrimEqPred :: Type -> Type -> Type
1700 mkReprPrimEqPred ty1 ty2
1701 = TyConApp eqReprPrimTyCon [k1, k2, ty1, ty2]
1702 where
1703 k1 = typeKind ty1
1704 k2 = typeKind ty2
1705
1706 equalityTyCon :: Role -> TyCon
1707 equalityTyCon Nominal = eqPrimTyCon
1708 equalityTyCon Representational = eqReprPrimTyCon
1709 equalityTyCon Phantom = eqPhantPrimTyCon
1710
1711 -- --------------------- Dictionary types ---------------------------------
1712
1713 mkClassPred :: Class -> [Type] -> PredType
1714 mkClassPred clas tys = TyConApp (classTyCon clas) tys
1715
1716 isDictTy :: Type -> Bool
1717 isDictTy = isClassPred
1718
1719 isDictLikeTy :: Type -> Bool
1720 -- Note [Dictionary-like types]
1721 isDictLikeTy ty | Just ty' <- coreView ty = isDictLikeTy ty'
1722 isDictLikeTy ty = case splitTyConApp_maybe ty of
1723 Just (tc, tys) | isClassTyCon tc -> True
1724 | isTupleTyCon tc -> all isDictLikeTy tys
1725 _other -> False
1726
1727 {-
1728 Note [Dictionary-like types]
1729 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1730 Being "dictionary-like" means either a dictionary type or a tuple thereof.
1731 In GHC 6.10 we build implication constraints which construct such tuples,
1732 and if we land up with a binding
1733 t :: (C [a], Eq [a])
1734 t = blah
1735 then we want to treat t as cheap under "-fdicts-cheap" for example.
1736 (Implication constraints are normally inlined, but sadly not if the
1737 occurrence is itself inside an INLINE function! Until we revise the
1738 handling of implication constraints, that is.) This turned out to
1739 be important in getting good arities in DPH code. Example:
1740
1741 class C a
1742 class D a where { foo :: a -> a }
1743 instance C a => D (Maybe a) where { foo x = x }
1744
1745 bar :: (C a, C b) => a -> b -> (Maybe a, Maybe b)
1746 {-# INLINE bar #-}
1747 bar x y = (foo (Just x), foo (Just y))
1748
1749 Then 'bar' should jolly well have arity 4 (two dicts, two args), but
1750 we ended up with something like
1751 bar = __inline_me__ (\d1,d2. let t :: (D (Maybe a), D (Maybe b)) = ...
1752 in \x,y. <blah>)
1753
1754 This is all a bit ad-hoc; eg it relies on knowing that implication
1755 constraints build tuples.
1756
1757
1758 Decomposing PredType
1759 -}
1760
1761 -- | A choice of equality relation. This is separate from the type 'Role'
1762 -- because 'Phantom' does not define a (non-trivial) equality relation.
1763 data EqRel = NomEq | ReprEq
1764 deriving (Eq, Ord)
1765
1766 instance Outputable EqRel where
1767 ppr NomEq = text "nominal equality"
1768 ppr ReprEq = text "representational equality"
1769
1770 eqRelRole :: EqRel -> Role
1771 eqRelRole NomEq = Nominal
1772 eqRelRole ReprEq = Representational
1773
1774 data PredTree = ClassPred Class [Type]
1775 | EqPred EqRel Type Type
1776 | IrredPred PredType
1777
1778 classifyPredType :: PredType -> PredTree
1779 classifyPredType ev_ty = case splitTyConApp_maybe ev_ty of
1780 Just (tc, [_, _, ty1, ty2])
1781 | tc `hasKey` eqReprPrimTyConKey -> EqPred ReprEq ty1 ty2
1782 | tc `hasKey` eqPrimTyConKey -> EqPred NomEq ty1 ty2
1783 Just (tc, tys)
1784 | Just clas <- tyConClass_maybe tc -> ClassPred clas tys
1785 _ -> IrredPred ev_ty
1786
1787 getClassPredTys :: PredType -> (Class, [Type])
1788 getClassPredTys ty = case getClassPredTys_maybe ty of
1789 Just (clas, tys) -> (clas, tys)
1790 Nothing -> pprPanic "getClassPredTys" (ppr ty)
1791
1792 getClassPredTys_maybe :: PredType -> Maybe (Class, [Type])
1793 getClassPredTys_maybe ty = case splitTyConApp_maybe ty of
1794 Just (tc, tys) | Just clas <- tyConClass_maybe tc -> Just (clas, tys)
1795 _ -> Nothing
1796
1797 getEqPredTys :: PredType -> (Type, Type)
1798 getEqPredTys ty
1799 = case splitTyConApp_maybe ty of
1800 Just (tc, [_, _, ty1, ty2])
1801 | tc `hasKey` eqPrimTyConKey
1802 || tc `hasKey` eqReprPrimTyConKey
1803 -> (ty1, ty2)
1804 _ -> pprPanic "getEqPredTys" (ppr ty)
1805
1806 getEqPredTys_maybe :: PredType -> Maybe (Role, Type, Type)
1807 getEqPredTys_maybe ty
1808 = case splitTyConApp_maybe ty of
1809 Just (tc, [_, _, ty1, ty2])
1810 | tc `hasKey` eqPrimTyConKey -> Just (Nominal, ty1, ty2)
1811 | tc `hasKey` eqReprPrimTyConKey -> Just (Representational, ty1, ty2)
1812 _ -> Nothing
1813
1814 getEqPredRole :: PredType -> Role
1815 getEqPredRole ty = eqRelRole (predTypeEqRel ty)
1816
1817 -- | Get the equality relation relevant for a pred type.
1818 predTypeEqRel :: PredType -> EqRel
1819 predTypeEqRel ty
1820 | Just (tc, _) <- splitTyConApp_maybe ty
1821 , tc `hasKey` eqReprPrimTyConKey
1822 = ReprEq
1823 | otherwise
1824 = NomEq
1825
1826 {-
1827 %************************************************************************
1828 %* *
1829 Size
1830 * *
1831 ************************************************************************
1832 -}
1833
1834 -- NB: This function does not respect `eqType`, in that two types that
1835 -- are `eqType` may return different sizes. This is OK, because this
1836 -- function is used only in reporting, not decision-making.
1837 typeSize :: Type -> Int
1838 typeSize (LitTy {}) = 1
1839 typeSize (TyVarTy {}) = 1
1840 typeSize (AppTy t1 t2) = typeSize t1 + typeSize t2
1841 typeSize (ForAllTy b t) = typeSize (binderType b) + typeSize t
1842 typeSize (TyConApp _ ts) = 1 + sum (map typeSize ts)
1843 typeSize (CastTy ty co) = typeSize ty + coercionSize co
1844 typeSize (CoercionTy co) = coercionSize co
1845
1846 {-
1847 %************************************************************************
1848 %* *
1849 Well-scoped tyvars
1850 * *
1851 ************************************************************************
1852 -}
1853
1854 -- | Do a topological sort on a list of tyvars. This is a deterministic
1855 -- sorting operation (that is, doesn't depend on Uniques).
1856 toposortTyVars :: [TyVar] -> [TyVar]
1857 toposortTyVars tvs = reverse $
1858 [ tv | (tv, _, _) <- topologicalSortG $
1859 graphFromEdgedVertices nodes ]
1860 where
1861 var_ids :: VarEnv Int
1862 var_ids = mkVarEnv (zip tvs [1..])
1863
1864 nodes = [ ( tv
1865 , lookupVarEnv_NF var_ids tv
1866 , mapMaybe (lookupVarEnv var_ids)
1867 (tyCoVarsOfTypeList (tyVarKind tv)) )
1868 | tv <- tvs ]
1869
1870 -- | Extract a well-scoped list of variables from a set of variables.
1871 varSetElemsWellScoped :: VarSet -> [Var]
1872 varSetElemsWellScoped = toposortTyVars . varSetElems
1873
1874 -- | Get the free vars of a type in scoped order
1875 tyCoVarsOfTypeWellScoped :: Type -> [TyVar]
1876 tyCoVarsOfTypeWellScoped = toposortTyVars . tyCoVarsOfTypeList
1877
1878 -- | Get the free vars of types in scoped order
1879 tyCoVarsOfTypesWellScoped :: [Type] -> [TyVar]
1880 tyCoVarsOfTypesWellScoped = toposortTyVars . tyCoVarsOfTypesList
1881
1882 {-
1883 ************************************************************************
1884 * *
1885 \subsection{Type families}
1886 * *
1887 ************************************************************************
1888 -}
1889
1890 mkFamilyTyConApp :: TyCon -> [Type] -> Type
1891 -- ^ Given a family instance TyCon and its arg types, return the
1892 -- corresponding family type. E.g:
1893 --
1894 -- > data family T a
1895 -- > data instance T (Maybe b) = MkT b
1896 --
1897 -- Where the instance tycon is :RTL, so:
1898 --
1899 -- > mkFamilyTyConApp :RTL Int = T (Maybe Int)
1900 mkFamilyTyConApp tc tys
1901 | Just (fam_tc, fam_tys) <- tyConFamInst_maybe tc
1902 , let tvs = tyConTyVars tc
1903 fam_subst = ASSERT2( length tvs == length tys, ppr tc <+> ppr tys )
1904 zipTvSubst tvs tys
1905 = mkTyConApp fam_tc (substTys fam_subst fam_tys)
1906 | otherwise
1907 = mkTyConApp tc tys
1908
1909 -- | Get the type on the LHS of a coercion induced by a type/data
1910 -- family instance.
1911 coAxNthLHS :: CoAxiom br -> Int -> Type
1912 coAxNthLHS ax ind =
1913 mkTyConApp (coAxiomTyCon ax) (coAxBranchLHS (coAxiomNthBranch ax ind))
1914
1915 -- | Pretty prints a 'TyCon', using the family instance in case of a
1916 -- representation tycon. For example:
1917 --
1918 -- > data T [a] = ...
1919 --
1920 -- In that case we want to print @T [a]@, where @T@ is the family 'TyCon'
1921 pprSourceTyCon :: TyCon -> SDoc
1922 pprSourceTyCon tycon
1923 | Just (fam_tc, tys) <- tyConFamInst_maybe tycon
1924 = ppr $ fam_tc `TyConApp` tys -- can't be FunTyCon
1925 | otherwise
1926 = ppr tycon
1927
1928 {-
1929 ************************************************************************
1930 * *
1931 \subsection{Liftedness}
1932 * *
1933 ************************************************************************
1934 -}
1935
1936 -- | See "Type#type_classification" for what an unlifted type is
1937 isUnliftedType :: Type -> Bool
1938 -- isUnliftedType returns True for forall'd unlifted types:
1939 -- x :: forall a. Int#
1940 -- I found bindings like these were getting floated to the top level.
1941 -- They are pretty bogus types, mind you. It would be better never to
1942 -- construct them
1943
1944 isUnliftedType ty | Just ty' <- coreView ty = isUnliftedType ty'
1945 isUnliftedType (ForAllTy (Named {}) ty) = isUnliftedType ty
1946 isUnliftedType (TyConApp tc _) = isUnliftedTyCon tc
1947 isUnliftedType _ = False
1948
1949 -- | Extract the RuntimeRep classifier of a type. Panics if this is not possible.
1950 getRuntimeRep :: String -- ^ Printed in case of an error
1951 -> Type -> Type
1952 getRuntimeRep err ty = getRuntimeRepFromKind err (typeKind ty)
1953
1954 -- | Extract the RuntimeRep classifier of a type from its kind.
1955 -- For example, getRuntimeRepFromKind * = PtrRepLifted;
1956 -- getRuntimeRepFromKind # = PtrRepUnlifted.
1957 -- Panics if this is not possible.
1958 getRuntimeRepFromKind :: String -- ^ Printed in case of an error
1959 -> Type -> Type
1960 getRuntimeRepFromKind err = go
1961 where
1962 go k | Just k' <- coreViewOneStarKind k = go k'
1963 go k
1964 | Just (tc, [arg]) <- splitTyConApp_maybe k
1965 , tc `hasKey` tYPETyConKey
1966 = arg
1967 go k = pprPanic "getRuntimeRep" (text err $$
1968 ppr k <+> dcolon <+> ppr (typeKind k))
1969
1970 isUnboxedTupleType :: Type -> Bool
1971 isUnboxedTupleType ty = case tyConAppTyCon_maybe ty of
1972 Just tc -> isUnboxedTupleTyCon tc
1973 _ -> False
1974
1975 -- | See "Type#type_classification" for what an algebraic type is.
1976 -- Should only be applied to /types/, as opposed to e.g. partially
1977 -- saturated type constructors
1978 isAlgType :: Type -> Bool
1979 isAlgType ty
1980 = case splitTyConApp_maybe ty of
1981 Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
1982 isAlgTyCon tc
1983 _other -> False
1984
1985 -- | See "Type#type_classification" for what an algebraic type is.
1986 -- Should only be applied to /types/, as opposed to e.g. partially
1987 -- saturated type constructors. Closed type constructors are those
1988 -- with a fixed right hand side, as opposed to e.g. associated types
1989 isClosedAlgType :: Type -> Bool
1990 isClosedAlgType ty
1991 = case splitTyConApp_maybe ty of
1992 Just (tc, ty_args) | isAlgTyCon tc && not (isFamilyTyCon tc)
1993 -> ASSERT2( ty_args `lengthIs` tyConArity tc, ppr ty ) True
1994 _other -> False
1995
1996 -- | Computes whether an argument (or let right hand side) should
1997 -- be computed strictly or lazily, based only on its type.
1998 -- Currently, it's just 'isUnliftedType'.
1999
2000 isStrictType :: Type -> Bool
2001 isStrictType = isUnliftedType
2002
2003 isPrimitiveType :: Type -> Bool
2004 -- ^ Returns true of types that are opaque to Haskell.
2005 isPrimitiveType ty = case splitTyConApp_maybe ty of
2006 Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
2007 isPrimTyCon tc
2008 _ -> False
2009
2010 {-
2011 ************************************************************************
2012 * *
2013 \subsection{Sequencing on types}
2014 * *
2015 ************************************************************************
2016 -}
2017
2018 seqType :: Type -> ()
2019 seqType (LitTy n) = n `seq` ()
2020 seqType (TyVarTy tv) = tv `seq` ()
2021 seqType (AppTy t1 t2) = seqType t1 `seq` seqType t2
2022 seqType (TyConApp tc tys) = tc `seq` seqTypes tys
2023 seqType (ForAllTy bndr ty) = seqType (binderType bndr) `seq` seqType ty
2024 seqType (CastTy ty co) = seqType ty `seq` seqCo co
2025 seqType (CoercionTy co) = seqCo co
2026
2027 seqTypes :: [Type] -> ()
2028 seqTypes [] = ()
2029 seqTypes (ty:tys) = seqType ty `seq` seqTypes tys
2030
2031 {-
2032 ************************************************************************
2033 * *
2034 Comparison for types
2035 (We don't use instances so that we know where it happens)
2036 * *
2037 ************************************************************************
2038
2039 Note [Equality on AppTys]
2040 ~~~~~~~~~~~~~~~~~~~~~~~~~
2041 In our cast-ignoring equality, we want to say that the following two
2042 are equal:
2043
2044 (Maybe |> co) (Int |> co') ~? Maybe Int
2045
2046 But the left is an AppTy while the right is a TyConApp. The solution is
2047 to use repSplitAppTy_maybe to break up the TyConApp into its pieces and
2048 then continue. Easy to do, but also easy to forget to do.
2049
2050 -}
2051
2052 eqType :: Type -> Type -> Bool
2053 -- ^ Type equality on source types. Does not look through @newtypes@ or
2054 -- 'PredType's, but it does look through type synonyms.
2055 -- This first checks that the kinds of the types are equal and then
2056 -- checks whether the types are equal, ignoring casts and coercions.
2057 -- (The kind check is a recursive call, but since all kinds have type
2058 -- @Type@, there is no need to check the types of kinds.)
2059 -- See also Note [Non-trivial definitional equality] in TyCoRep.
2060 eqType t1 t2 = isEqual $ cmpType t1 t2
2061
2062 -- | Compare types with respect to a (presumably) non-empty 'RnEnv2'.
2063 eqTypeX :: RnEnv2 -> Type -> Type -> Bool
2064 eqTypeX env t1 t2 = isEqual $ cmpTypeX env t1 t2
2065
2066 -- | Type equality on lists of types, looking through type synonyms
2067 -- but not newtypes.
2068 eqTypes :: [Type] -> [Type] -> Bool
2069 eqTypes tys1 tys2 = isEqual $ cmpTypes tys1 tys2
2070
2071 eqVarBndrs :: RnEnv2 -> [Var] -> [Var] -> Maybe RnEnv2
2072 -- Check that the var lists are the same length
2073 -- and have matching kinds; if so, extend the RnEnv2
2074 -- Returns Nothing if they don't match
2075 eqVarBndrs env [] []
2076 = Just env
2077 eqVarBndrs env (tv1:tvs1) (tv2:tvs2)
2078 | eqTypeX env (tyVarKind tv1) (tyVarKind tv2)
2079 = eqVarBndrs (rnBndr2 env tv1 tv2) tvs1 tvs2
2080 eqVarBndrs _ _ _= Nothing
2081
2082 -- Now here comes the real worker
2083
2084 cmpType :: Type -> Type -> Ordering
2085 cmpType t1 t2
2086 -- we know k1 and k2 have the same kind, because they both have kind *.
2087 = cmpTypeX rn_env t1 t2
2088 where
2089 rn_env = mkRnEnv2 (mkInScopeSet (tyCoVarsOfTypes [t1, t2]))
2090
2091 cmpTypes :: [Type] -> [Type] -> Ordering
2092 cmpTypes ts1 ts2 = cmpTypesX rn_env ts1 ts2
2093 where
2094 rn_env = mkRnEnv2 (mkInScopeSet (tyCoVarsOfTypes (ts1 ++ ts2)))
2095
2096 -- | An ordering relation between two 'Type's (known below as @t1 :: k1@
2097 -- and @t2 :: k2@)
2098 data TypeOrdering = TLT -- ^ @t1 < t2@
2099 | TEQ -- ^ @t1 ~ t2@ and there are no casts in either,
2100 -- therefore we can conclude @k1 ~ k2@
2101 | TEQX -- ^ @t1 ~ t2@ yet one of the types contains a cast so
2102 -- they may differ in kind.
2103 | TGT -- ^ @t1 > t2@
2104 deriving (Eq, Ord, Enum, Bounded)
2105
2106 cmpTypeX :: RnEnv2 -> Type -> Type -> Ordering -- Main workhorse
2107 -- See Note [Non-trivial definitional equality] in TyCoRep
2108 cmpTypeX env orig_t1 orig_t2 =
2109 case go env orig_t1 orig_t2 of
2110 -- If there are casts then we also need to do a comparison of the kinds of
2111 -- the types being compared
2112 TEQX -> toOrdering $ go env k1 k2
2113 ty_ordering -> toOrdering ty_ordering
2114 where
2115 k1 = typeKind orig_t1
2116 k2 = typeKind orig_t2
2117
2118 toOrdering :: TypeOrdering -> Ordering
2119 toOrdering TLT = LT
2120 toOrdering TEQ = EQ
2121 toOrdering TEQX = EQ
2122 toOrdering TGT = GT
2123
2124 liftOrdering :: Ordering -> TypeOrdering
2125 liftOrdering LT = TLT
2126 liftOrdering EQ = TEQ
2127 liftOrdering GT = TGT
2128
2129 thenCmpTy :: TypeOrdering -> TypeOrdering -> TypeOrdering
2130 thenCmpTy TEQ rel = rel
2131 thenCmpTy TEQX rel = hasCast rel
2132 thenCmpTy rel _ = rel
2133
2134 hasCast :: TypeOrdering -> TypeOrdering
2135 hasCast TEQ = TEQX
2136 hasCast rel = rel
2137
2138 -- Returns both the resulting ordering relation between the two types
2139 -- and whether either contains a cast.
2140 go :: RnEnv2 -> Type -> Type -> TypeOrdering
2141 go env t1 t2
2142 | Just t1' <- coreViewOneStarKind t1 = go env t1' t2
2143 | Just t2' <- coreViewOneStarKind t2 = go env t1 t2'
2144
2145 go env (TyVarTy tv1) (TyVarTy tv2)
2146 = liftOrdering $ rnOccL env tv1 `compare` rnOccR env tv2
2147 go env (ForAllTy (Named tv1 _) t1) (ForAllTy (Named tv2 _) t2)
2148 = go env (tyVarKind tv1) (tyVarKind tv2)
2149 `thenCmpTy` go (rnBndr2 env tv1 tv2) t1 t2
2150 -- See Note [Equality on AppTys]
2151 go env (AppTy s1 t1) ty2
2152 | Just (s2, t2) <- repSplitAppTy_maybe ty2
2153 = go env s1 s2 `thenCmpTy` go env t1 t2
2154 go env ty1 (AppTy s2 t2)
2155 | Just (s1, t1) <- repSplitAppTy_maybe ty1
2156 = go env s1 s2 `thenCmpTy` go env t1 t2
2157 go env (ForAllTy (Anon s1) t1) (ForAllTy (Anon s2) t2)
2158 = go env s1 s2 `thenCmpTy` go env t1 t2
2159 go env (TyConApp tc1 tys1) (TyConApp tc2 tys2)
2160 = liftOrdering (tc1 `cmpTc` tc2) `thenCmpTy` gos env tys1 tys2
2161 go _ (LitTy l1) (LitTy l2) = liftOrdering (compare l1 l2)
2162 go env (CastTy t1 _) t2 = hasCast $ go env t1 t2
2163 go env t1 (CastTy t2 _) = hasCast $ go env t1 t2
2164 go _ (CoercionTy {}) (CoercionTy {}) = TEQ
2165
2166 -- Deal with the rest: TyVarTy < CoercionTy < AppTy < LitTy < TyConApp < ForAllTy
2167 go _ ty1 ty2
2168 = liftOrdering $ (get_rank ty1) `compare` (get_rank ty2)
2169 where get_rank :: Type -> Int
2170 get_rank (CastTy {})
2171 = pprPanic "cmpTypeX.get_rank" (ppr [ty1,ty2])
2172 get_rank (TyVarTy {}) = 0
2173 get_rank (CoercionTy {}) = 1
2174 get_rank (AppTy {}) = 3
2175 get_rank (LitTy {}) = 4
2176 get_rank (TyConApp {}) = 5
2177 get_rank (ForAllTy (Anon {}) _) = 6
2178 get_rank (ForAllTy (Named {}) _) = 7
2179
2180 gos :: RnEnv2 -> [Type] -> [Type] -> TypeOrdering
2181 gos _ [] [] = TEQ
2182 gos _ [] _ = TLT
2183 gos _ _ [] = TGT
2184 gos env (ty1:tys1) (ty2:tys2) = go env ty1 ty2 `thenCmpTy` gos env tys1 tys2
2185
2186 -------------
2187 cmpTypesX :: RnEnv2 -> [Type] -> [Type] -> Ordering
2188 cmpTypesX _ [] [] = EQ
2189 cmpTypesX env (t1:tys1) (t2:tys2) = cmpTypeX env t1 t2
2190 `thenCmp` cmpTypesX env tys1 tys2
2191 cmpTypesX _ [] _ = LT
2192 cmpTypesX _ _ [] = GT
2193
2194 -------------
2195 -- | Compare two 'TyCon's. NB: This should /never/ see the "star synonyms",
2196 -- as recognized by Kind.isStarKindSynonymTyCon. See Note
2197 -- [Kind Constraint and kind *] in Kind.
2198 cmpTc :: TyCon -> TyCon -> Ordering
2199 cmpTc tc1 tc2
2200 = ASSERT( not (isStarKindSynonymTyCon tc1) && not (isStarKindSynonymTyCon tc2) )
2201 u1 `compare` u2
2202 where
2203 u1 = tyConUnique tc1
2204 u2 = tyConUnique tc2
2205
2206 {-
2207 ************************************************************************
2208 * *
2209 The kind of a type
2210 * *
2211 ************************************************************************
2212 -}
2213
2214 typeKind :: Type -> Kind
2215 typeKind (TyConApp tc tys) = piResultTys (tyConKind tc) tys
2216 typeKind (AppTy fun arg) = piResultTy (typeKind fun) arg
2217 typeKind (LitTy l) = typeLiteralKind l
2218 typeKind (ForAllTy (Anon _) _) = liftedTypeKind
2219 typeKind (ForAllTy _ ty) = typeKind ty
2220 typeKind (TyVarTy tyvar) = tyVarKind tyvar
2221 typeKind (CastTy _ty co) = pSnd $ coercionKind co
2222 typeKind (CoercionTy co) = coercionType co
2223
2224 typeLiteralKind :: TyLit -> Kind
2225 typeLiteralKind l =
2226 case l of
2227 NumTyLit _ -> typeNatKind
2228 StrTyLit _ -> typeSymbolKind
2229
2230 -- | Print a tyvar with its kind
2231 pprTyVar :: TyVar -> SDoc
2232 pprTyVar tv = ppr tv <+> dcolon <+> ppr (tyVarKind tv)
2233
2234 {-
2235 %************************************************************************
2236 %* *
2237 Miscellaneous functions
2238 %* *
2239 %************************************************************************
2240
2241 -}
2242 -- | All type constructors occurring in the type; looking through type
2243 -- synonyms, but not newtypes.
2244 -- When it finds a Class, it returns the class TyCon.
2245 tyConsOfType :: Type -> NameEnv TyCon
2246 tyConsOfType ty
2247 = go ty
2248 where
2249 go :: Type -> NameEnv TyCon -- The NameEnv does duplicate elim
2250 go ty | Just ty' <- coreView ty = go ty'
2251 go (TyVarTy {}) = emptyNameEnv
2252 go (LitTy {}) = emptyNameEnv
2253 go (TyConApp tc tys) = go_tc tc `plusNameEnv` go_s tys
2254 go (AppTy a b) = go a `plusNameEnv` go b
2255 go (ForAllTy (Anon a) b) = go a `plusNameEnv` go b `plusNameEnv` go_tc funTyCon
2256 go (ForAllTy (Named tv _) ty) = go ty `plusNameEnv` go (tyVarKind tv)
2257 go (CastTy ty co) = go ty `plusNameEnv` go_co co
2258 go (CoercionTy co) = go_co co
2259
2260 go_co (Refl _ ty) = go ty
2261 go_co (TyConAppCo _ tc args) = go_tc tc `plusNameEnv` go_cos args
2262 go_co (AppCo co arg) = go_co co `plusNameEnv` go_co arg
2263 go_co (ForAllCo _ kind_co co) = go_co kind_co `plusNameEnv` go_co co
2264 go_co (CoVarCo {}) = emptyNameEnv
2265 go_co (AxiomInstCo ax _ args) = go_ax ax `plusNameEnv` go_cos args
2266 go_co (UnivCo p _ t1 t2) = go_prov p `plusNameEnv` go t1 `plusNameEnv` go t2
2267 go_co (SymCo co) = go_co co
2268 go_co (TransCo co1 co2) = go_co co1 `plusNameEnv` go_co co2
2269 go_co (NthCo _ co) = go_co co
2270 go_co (LRCo _ co) = go_co co
2271 go_co (InstCo co arg) = go_co co `plusNameEnv` go_co arg
2272 go_co (CoherenceCo co1 co2) = go_co co1 `plusNameEnv` go_co co2
2273 go_co (KindCo co) = go_co co
2274 go_co (SubCo co) = go_co co
2275 go_co (AxiomRuleCo _ cs) = go_cos cs
2276
2277 go_prov UnsafeCoerceProv = emptyNameEnv
2278 go_prov (PhantomProv co) = go_co co
2279 go_prov (ProofIrrelProv co) = go_co co
2280 go_prov (PluginProv _) = emptyNameEnv
2281 go_prov (HoleProv _) = emptyNameEnv
2282 -- this last case can happen from the tyConsOfType used from
2283 -- checkTauTvUpdate
2284
2285 go_s tys = foldr (plusNameEnv . go) emptyNameEnv tys
2286 go_cos cos = foldr (plusNameEnv . go_co) emptyNameEnv cos
2287
2288 go_tc tc = unitNameEnv (tyConName tc) tc
2289 go_ax ax = go_tc $ coAxiomTyCon ax
2290
2291 -- | Find the result 'Kind' of a type synonym,
2292 -- after applying it to its 'arity' number of type variables
2293 -- Actually this function works fine on data types too,
2294 -- but they'd always return '*', so we never need to ask
2295 synTyConResKind :: TyCon -> Kind
2296 synTyConResKind tycon = piResultTys (tyConKind tycon) (mkTyVarTys (tyConTyVars tycon))
2297
2298 -- | Retrieve the free variables in this type, splitting them based
2299 -- on whether the variable was used in a dependent context. It's possible
2300 -- for a variable to be reported twice, if it's used both dependently
2301 -- and non-dependently. (This isn't the most precise analysis, because
2302 -- it's used in the typechecking knot. It might list some dependent
2303 -- variables as also non-dependent.)
2304 splitDepVarsOfType :: Type -> Pair TyCoVarSet
2305 splitDepVarsOfType = go
2306 where
2307 go (TyVarTy tv) = Pair (tyCoVarsOfType $ tyVarKind tv)
2308 (unitVarSet tv)
2309 go (AppTy t1 t2) = go t1 `mappend` go t2
2310 go (TyConApp _ tys) = foldMap go tys
2311 go (ForAllTy (Anon arg) res) = go arg `mappend` go res
2312 go (ForAllTy (Named tv _) ty)
2313 = let Pair kvs tvs = go ty in
2314 Pair (kvs `delVarSet` tv `unionVarSet` tyCoVarsOfType (tyVarKind tv))
2315 (tvs `delVarSet` tv)
2316 go (LitTy {}) = mempty
2317 go (CastTy ty co) = go ty `mappend` Pair (tyCoVarsOfCo co)
2318 emptyVarSet
2319 go (CoercionTy co) = go_co co
2320
2321 go_co co = let Pair ty1 ty2 = coercionKind co in
2322 go ty1 `mappend` go ty2 -- NB: the Pairs separate along different
2323 -- dimensions here. Be careful!
2324
2325 -- | Like 'splitDepVarsOfType', but over a list of types
2326 splitDepVarsOfTypes :: [Type] -> Pair TyCoVarSet
2327 splitDepVarsOfTypes = foldMap splitDepVarsOfType
2328
2329 -- | Retrieve the free variables in this type, splitting them based
2330 -- on whether they are used visibly or invisibly. Invisible ones come
2331 -- first.
2332 splitVisVarsOfType :: Type -> Pair TyCoVarSet
2333 splitVisVarsOfType orig_ty = Pair invis_vars vis_vars
2334 where
2335 Pair invis_vars1 vis_vars = go orig_ty
2336 invis_vars = invis_vars1 `minusVarSet` vis_vars
2337
2338 go (TyVarTy tv) = Pair (tyCoVarsOfType $ tyVarKind tv) (unitVarSet tv)
2339 go (AppTy t1 t2) = go t1 `mappend` go t2
2340 go (TyConApp tc tys) = go_tc tc tys
2341 go (ForAllTy (Anon t1) t2) = go t1 `mappend` go t2
2342 go (ForAllTy (Named tv _) ty)
2343 = ((`delVarSet` tv) <$> go ty) `mappend`
2344 (invisible (tyCoVarsOfType $ tyVarKind tv))
2345 go (LitTy {}) = mempty
2346 go (CastTy ty co) = go ty `mappend` invisible (tyCoVarsOfCo co)
2347 go (CoercionTy co) = invisible $ tyCoVarsOfCo co
2348
2349 invisible vs = Pair vs emptyVarSet
2350
2351 go_tc tc tys = let (invis, vis) = partitionInvisibles tc id tys in
2352 invisible (tyCoVarsOfTypes invis) `mappend` foldMap go vis
2353
2354 splitVisVarsOfTypes :: [Type] -> Pair TyCoVarSet
2355 splitVisVarsOfTypes = foldMap splitVisVarsOfType