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