Get rid of varSetElemsWellScoped in abstractFloats
[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 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, tyCoFVsOfType,
120 tyCoVarsOfTypeDSet,
121 coVarsOfType,
122 coVarsOfTypes, closeOverKinds, closeOverKindsList,
123 splitVisVarsOfType, splitVisVarsOfTypes,
124 expandTypeSynonyms,
125 typeSize,
126
127 -- * Well-scoped lists of variables
128 varSetElemsWellScoped, toposortTyVars, tyCoVarsOfTypeWellScoped,
129 tyCoVarsOfTypesWellScoped,
130
131 -- * Type comparison
132 eqType, eqTypeX, eqTypes, cmpType, cmpTypes, cmpTypeX, cmpTypesX, cmpTc,
133 eqVarBndrs,
134
135 -- * Forcing evaluation of types
136 seqType, seqTypes,
137
138 -- * Other views onto Types
139 coreView, coreViewOneStarKind,
140
141 UnaryType, RepType(..), flattenRepType, repType,
142 tyConsOfType,
143
144 -- * Type representation for the code generator
145 typePrimRep, typeRepArity, kindPrimRep, tyConPrimRep,
146
147 -- * Main type substitution data types
148 TvSubstEnv, -- Representation widely visible
149 TCvSubst(..), -- Representation visible to a few friends
150
151 -- ** Manipulating type substitutions
152 emptyTvSubstEnv, emptyTCvSubst, mkEmptyTCvSubst,
153
154 mkTCvSubst, zipTvSubst, mkTvSubstPrs,
155 notElemTCvSubst,
156 getTvSubstEnv, setTvSubstEnv,
157 zapTCvSubst, getTCvInScope,
158 extendTCvInScope, extendTCvInScopeList, extendTCvInScopeSet,
159 extendTCvSubst, extendCvSubst,
160 extendTvSubst, extendTvSubstList, extendTvSubstAndInScope,
161 extendTvSubstWithClone,
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, ppSuggestExplicitKinds,
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 tidyTyBinder, tidyTyBinders
193 ) where
194
195 #include "HsVersions.h"
196
197 -- We import the representation and primitive functions from TyCoRep.
198 -- Many things are reexported, but not the representation!
199
200 import Kind
201 import TyCoRep
202
203 -- friends:
204 import Var
205 import VarEnv
206 import VarSet
207 import NameEnv
208
209 import Class
210 import TyCon
211 import TysPrim
212 import {-# SOURCE #-} TysWiredIn ( listTyCon, typeNatKind
213 , typeSymbolKind, liftedTypeKind )
214 import PrelNames
215 import CoAxiom
216 import {-# SOURCE #-} Coercion
217
218 -- others
219 import BasicTypes ( Arity, RepArity )
220 import Util
221 import Outputable
222 import FastString
223 import Pair
224 import ListSetOps
225 import Digraph
226
227 import Maybes ( orElse )
228 import Data.Maybe ( isJust, mapMaybe )
229 import Control.Monad ( guard )
230 import Control.Arrow ( first, second )
231
232 -- $type_classification
233 -- #type_classification#
234 --
235 -- Types are one of:
236 --
237 -- [Unboxed] Iff its representation is other than a pointer
238 -- Unboxed types are also unlifted.
239 --
240 -- [Lifted] Iff it has bottom as an element.
241 -- Closures always have lifted types: i.e. any
242 -- let-bound identifier in Core must have a lifted
243 -- type. Operationally, a lifted object is one that
244 -- can be entered.
245 -- Only lifted types may be unified with a type variable.
246 --
247 -- [Algebraic] Iff it is a type with one or more constructors, whether
248 -- declared with @data@ or @newtype@.
249 -- An algebraic type is one that can be deconstructed
250 -- with a case expression. This is /not/ the same as
251 -- lifted types, because we also include unboxed
252 -- tuples in this classification.
253 --
254 -- [Data] Iff it is a type declared with @data@, or a boxed tuple.
255 --
256 -- [Primitive] Iff it is a built-in type that can't be expressed in Haskell.
257 --
258 -- Currently, all primitive types are unlifted, but that's not necessarily
259 -- the case: for example, @Int@ could be primitive.
260 --
261 -- Some primitive types are unboxed, such as @Int#@, whereas some are boxed
262 -- but unlifted (such as @ByteArray#@). The only primitive types that we
263 -- classify as algebraic are the unboxed tuples.
264 --
265 -- Some examples of type classifications that may make this a bit clearer are:
266 --
267 -- @
268 -- Type primitive boxed lifted algebraic
269 -- -----------------------------------------------------------------------------
270 -- Int# Yes No No No
271 -- ByteArray# Yes Yes No No
272 -- (\# a, b \#) Yes No No Yes
273 -- ( a, b ) No Yes Yes Yes
274 -- [a] No Yes Yes Yes
275 -- @
276
277 -- $representation_types
278 -- A /source type/ is a type that is a separate type as far as the type checker is
279 -- concerned, but which has a more low-level representation as far as Core-to-Core
280 -- passes and the rest of the back end is concerned.
281 --
282 -- You don't normally have to worry about this, as the utility functions in
283 -- this module will automatically convert a source into a representation type
284 -- if they are spotted, to the best of it's abilities. If you don't want this
285 -- to happen, use the equivalent functions from the "TcType" module.
286
287 {-
288 ************************************************************************
289 * *
290 Type representation
291 * *
292 ************************************************************************
293 -}
294
295 {-# INLINE coreView #-}
296 coreView :: Type -> Maybe Type
297 -- ^ This function Strips off the /top layer only/ of a type synonym
298 -- application (if any) its underlying representation type.
299 -- Returns Nothing if there is nothing to look through.
300 --
301 -- By being non-recursive and inlined, this case analysis gets efficiently
302 -- joined onto the case analysis that the caller is already doing
303 coreView (TyConApp tc tys) | Just (tenv, rhs, tys') <- expandSynTyCon_maybe tc tys
304 = Just (mkAppTys (substTy (mkTvSubstPrs tenv) rhs) tys')
305 -- The free vars of 'rhs' should all be bound by 'tenv', so it's
306 -- ok to use 'substTy' here.
307 -- See also Note [The substitution invariant] in TyCoRep.
308 -- Its important to use mkAppTys, rather than (foldl AppTy),
309 -- because the function part might well return a
310 -- partially-applied type constructor; indeed, usually will!
311 coreView _ = Nothing
312
313 -- | Like 'coreView', but it also "expands" @Constraint@ to become
314 -- @TYPE PtrRepLifted@.
315 {-# INLINE coreViewOneStarKind #-}
316 coreViewOneStarKind :: Type -> Maybe Type
317 coreViewOneStarKind ty
318 | Just ty' <- coreView ty = Just ty'
319 | TyConApp tc [] <- ty
320 , isStarKindSynonymTyCon tc = Just liftedTypeKind
321 | otherwise = Nothing
322
323 -----------------------------------------------
324 expandTypeSynonyms :: Type -> Type
325 -- ^ Expand out all type synonyms. Actually, it'd suffice to expand out
326 -- just the ones that discard type variables (e.g. type Funny a = Int)
327 -- But we don't know which those are currently, so we just expand all.
328 --
329 -- 'expandTypeSynonyms' only expands out type synonyms mentioned in the type,
330 -- not in the kinds of any TyCon or TyVar mentioned in the type.
331 expandTypeSynonyms ty
332 = go (mkEmptyTCvSubst in_scope) ty
333 where
334 in_scope = mkInScopeSet (tyCoVarsOfType ty)
335
336 go subst (TyConApp tc tys)
337 | Just (tenv, rhs, tys') <- expandSynTyCon_maybe tc expanded_tys
338 = let subst' = mkTvSubst in_scope (mkVarEnv tenv)
339 -- Make a fresh substitution; rhs has nothing to
340 -- do with anything that has happened so far
341 -- NB: if you make changes here, be sure to build an
342 -- /idempotent/ substitution, even in the nested case
343 -- type T a b = a -> b
344 -- type S x y = T y x
345 -- (Trac #11665)
346 in mkAppTys (go subst' rhs) tys'
347 | otherwise
348 = TyConApp tc expanded_tys
349 where
350 expanded_tys = (map (go subst) tys)
351
352 go _ (LitTy l) = LitTy l
353 go subst (TyVarTy tv) = substTyVar subst tv
354 go subst (AppTy t1 t2) = mkAppTy (go subst t1) (go subst t2)
355 go subst (ForAllTy (Anon arg) res)
356 = mkFunTy (go subst arg) (go subst res)
357 go subst (ForAllTy (Named tv vis) t)
358 = let (subst', tv') = substTyVarBndrCallback go subst tv in
359 ForAllTy (Named tv' vis) (go subst' t)
360 go subst (CastTy ty co) = mkCastTy (go subst ty) (go_co subst co)
361 go subst (CoercionTy co) = mkCoercionTy (go_co subst co)
362
363 go_co subst (Refl r ty)
364 = mkReflCo r (go subst ty)
365 -- NB: coercions are always expanded upon creation
366 go_co subst (TyConAppCo r tc args)
367 = mkTyConAppCo r tc (map (go_co subst) args)
368 go_co subst (AppCo co arg)
369 = mkAppCo (go_co subst co) (go_co subst arg)
370 go_co subst (ForAllCo tv kind_co co)
371 = let (subst', tv', kind_co') = go_cobndr subst tv kind_co in
372 mkForAllCo tv' kind_co' (go_co subst' co)
373 go_co subst (CoVarCo cv)
374 = substCoVar subst cv
375 go_co subst (AxiomInstCo ax ind args)
376 = mkAxiomInstCo ax ind (map (go_co subst) args)
377 go_co subst (UnivCo p r t1 t2)
378 = mkUnivCo (go_prov subst p) r (go subst t1) (go subst t2)
379 go_co subst (SymCo co)
380 = mkSymCo (go_co subst co)
381 go_co subst (TransCo co1 co2)
382 = mkTransCo (go_co subst co1) (go_co subst co2)
383 go_co subst (NthCo n co)
384 = mkNthCo n (go_co subst co)
385 go_co subst (LRCo lr co)
386 = mkLRCo lr (go_co subst co)
387 go_co subst (InstCo co arg)
388 = mkInstCo (go_co subst co) (go_co subst arg)
389 go_co subst (CoherenceCo co1 co2)
390 = mkCoherenceCo (go_co subst co1) (go_co subst co2)
391 go_co subst (KindCo co)
392 = mkKindCo (go_co subst co)
393 go_co subst (SubCo co)
394 = mkSubCo (go_co subst co)
395 go_co subst (AxiomRuleCo ax cs) = AxiomRuleCo ax (map (go_co subst) cs)
396
397 go_prov _ UnsafeCoerceProv = UnsafeCoerceProv
398 go_prov subst (PhantomProv co) = PhantomProv (go_co subst co)
399 go_prov subst (ProofIrrelProv co) = ProofIrrelProv (go_co subst co)
400 go_prov _ p@(PluginProv _) = p
401 go_prov _ (HoleProv h) = pprPanic "expandTypeSynonyms hit a hole" (ppr h)
402
403 -- the "False" and "const" are to accommodate the type of
404 -- substForAllCoBndrCallback, which is general enough to
405 -- handle coercion optimization (which sometimes swaps the
406 -- order of a coercion)
407 go_cobndr subst = substForAllCoBndrCallback False (go_co subst) subst
408
409 {-
410 ************************************************************************
411 * *
412 Analyzing types
413 * *
414 ************************************************************************
415
416 These functions do a map-like operation over types, performing some operation
417 on all variables and binding sites. Primarily used for zonking.
418
419 Note [Efficiency for mapCoercion ForAllCo case]
420 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
421 As noted in Note [Forall coercions] in TyCoRep, a ForAllCo is a bit redundant.
422 It stores a TyVar and a Coercion, where the kind of the TyVar always matches
423 the left-hand kind of the coercion. This is convenient lots of the time, but
424 not when mapping a function over a coercion.
425
426 The problem is that tcm_tybinder will affect the TyVar's kind and
427 mapCoercion will affect the Coercion, and we hope that the results will be
428 the same. Even if they are the same (which should generally happen with
429 correct algorithms), then there is an efficiency issue. In particular,
430 this problem seems to make what should be a linear algorithm into a potentially
431 exponential one. But it's only going to be bad in the case where there's
432 lots of foralls in the kinds of other foralls. Like this:
433
434 forall a : (forall b : (forall c : ...). ...). ...
435
436 This construction seems unlikely. So we'll do the inefficient, easy way
437 for now.
438
439 Note [Specialising mappers]
440 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
441 These INLINABLE pragmas are indispensable. mapType/mapCoercion are used
442 to implement zonking, and it's vital that they get specialised to the TcM
443 monad. This specialisation happens automatically (that is, without a
444 SPECIALISE pragma) as long as the definitions are INLINABLE. For example,
445 this one change made a 20% allocation difference in perf/compiler/T5030.
446
447 -}
448
449 -- | This describes how a "map" operation over a type/coercion should behave
450 data TyCoMapper env m
451 = TyCoMapper
452 { tcm_smart :: Bool -- ^ Should the new type be created with smart
453 -- constructors?
454 , tcm_tyvar :: env -> TyVar -> m Type
455 , tcm_covar :: env -> CoVar -> m Coercion
456 , tcm_hole :: env -> CoercionHole -> Role
457 -> Type -> Type -> m Coercion
458 -- ^ What to do with coercion holes. See Note [Coercion holes] in
459 -- TyCoRep.
460
461 , tcm_tybinder :: env -> TyVar -> VisibilityFlag -> m (env, TyVar)
462 -- ^ The returned env is used in the extended scope
463 }
464
465 {-# INLINABLE mapType #-} -- See Note [Specialising mappers]
466 mapType :: Monad m => TyCoMapper env m -> env -> Type -> m Type
467 mapType mapper@(TyCoMapper { tcm_smart = smart, tcm_tyvar = tyvar
468 , tcm_tybinder = tybinder })
469 env ty
470 = go ty
471 where
472 go (TyVarTy tv) = tyvar env tv
473 go (AppTy t1 t2) = mkappty <$> go t1 <*> go t2
474 go t@(TyConApp _ []) = return t -- avoid allocation in this exceedingly
475 -- common case (mostly, for *)
476 go (TyConApp tc tys) = mktyconapp tc <$> mapM go tys
477 go (ForAllTy (Anon arg) res) = mkfunty <$> go arg <*> go res
478 go (ForAllTy (Named tv vis) inner)
479 = do { (env', tv') <- tybinder env tv vis
480 ; inner' <- mapType mapper env' inner
481 ; return $ ForAllTy (Named tv' vis) inner' }
482 go ty@(LitTy {}) = return ty
483 go (CastTy ty co) = mkcastty <$> go ty <*> mapCoercion mapper env co
484 go (CoercionTy co) = CoercionTy <$> mapCoercion mapper env co
485
486 (mktyconapp, mkappty, mkcastty, mkfunty)
487 | smart = (mkTyConApp, mkAppTy, mkCastTy, mkFunTy)
488 | otherwise = (TyConApp, AppTy, CastTy, ForAllTy . Anon)
489
490 {-# INLINABLE mapCoercion #-} -- See Note [Specialising mappers]
491 mapCoercion :: Monad m
492 => TyCoMapper env m -> env -> Coercion -> m Coercion
493 mapCoercion mapper@(TyCoMapper { tcm_smart = smart, tcm_covar = covar
494 , tcm_hole = cohole, tcm_tybinder = tybinder })
495 env co
496 = go co
497 where
498 go (Refl r ty) = Refl r <$> mapType mapper env ty
499 go (TyConAppCo r tc args)
500 = mktyconappco r tc <$> mapM go args
501 go (AppCo c1 c2) = mkappco <$> go c1 <*> go c2
502 go (ForAllCo tv kind_co co)
503 = do { kind_co' <- go kind_co
504 ; (env', tv') <- tybinder env tv Invisible
505 ; co' <- mapCoercion mapper env' co
506 ; return $ mkforallco tv' kind_co' co' }
507 -- See Note [Efficiency for mapCoercion ForAllCo case]
508 go (CoVarCo cv) = covar env cv
509 go (AxiomInstCo ax i args)
510 = mkaxiominstco ax i <$> mapM go args
511 go (UnivCo (HoleProv hole) r t1 t2)
512 = cohole env hole r t1 t2
513 go (UnivCo p r t1 t2)
514 = mkunivco <$> go_prov p <*> pure r
515 <*> mapType mapper env t1 <*> mapType mapper env t2
516 go (SymCo co) = mksymco <$> go co
517 go (TransCo c1 c2) = mktransco <$> go c1 <*> go c2
518 go (AxiomRuleCo r cos) = AxiomRuleCo r <$> mapM go cos
519 go (NthCo i co) = mknthco i <$> go co
520 go (LRCo lr co) = mklrco lr <$> go co
521 go (InstCo co arg) = mkinstco <$> go co <*> go arg
522 go (CoherenceCo c1 c2) = mkcoherenceco <$> go c1 <*> go c2
523 go (KindCo co) = mkkindco <$> go co
524 go (SubCo co) = mksubco <$> go co
525
526 go_prov UnsafeCoerceProv = return UnsafeCoerceProv
527 go_prov (PhantomProv co) = PhantomProv <$> go co
528 go_prov (ProofIrrelProv co) = ProofIrrelProv <$> go co
529 go_prov p@(PluginProv _) = return p
530 go_prov (HoleProv _) = panic "mapCoercion"
531
532 ( mktyconappco, mkappco, mkaxiominstco, mkunivco
533 , mksymco, mktransco, mknthco, mklrco, mkinstco, mkcoherenceco
534 , mkkindco, mksubco, mkforallco)
535 | smart
536 = ( mkTyConAppCo, mkAppCo, mkAxiomInstCo, mkUnivCo
537 , mkSymCo, mkTransCo, mkNthCo, mkLRCo, mkInstCo, mkCoherenceCo
538 , mkKindCo, mkSubCo, mkForAllCo )
539 | otherwise
540 = ( TyConAppCo, AppCo, AxiomInstCo, UnivCo
541 , SymCo, TransCo, NthCo, LRCo, InstCo, CoherenceCo
542 , KindCo, SubCo, ForAllCo )
543
544 {-
545 ************************************************************************
546 * *
547 \subsection{Constructor-specific functions}
548 * *
549 ************************************************************************
550
551
552 ---------------------------------------------------------------------
553 TyVarTy
554 ~~~~~~~
555 -}
556
557 -- | Attempts to obtain the type variable underlying a 'Type', and panics with the
558 -- given message if this is not a type variable type. See also 'getTyVar_maybe'
559 getTyVar :: String -> Type -> TyVar
560 getTyVar msg ty = case getTyVar_maybe ty of
561 Just tv -> tv
562 Nothing -> panic ("getTyVar: " ++ msg)
563
564 isTyVarTy :: Type -> Bool
565 isTyVarTy ty = isJust (getTyVar_maybe ty)
566
567 -- | Attempts to obtain the type variable underlying a 'Type'
568 getTyVar_maybe :: Type -> Maybe TyVar
569 getTyVar_maybe ty | Just ty' <- coreView ty = getTyVar_maybe ty'
570 | otherwise = repGetTyVar_maybe ty
571
572 -- | If the type is a tyvar, possibly under a cast, returns it, along
573 -- with the coercion. Thus, the co is :: kind tv ~R kind type
574 getCastedTyVar_maybe :: Type -> Maybe (TyVar, Coercion)
575 getCastedTyVar_maybe ty | Just ty' <- coreView ty = getCastedTyVar_maybe ty'
576 getCastedTyVar_maybe (CastTy (TyVarTy tv) co) = Just (tv, co)
577 getCastedTyVar_maybe (TyVarTy tv)
578 = Just (tv, mkReflCo Nominal (tyVarKind tv))
579 getCastedTyVar_maybe _ = Nothing
580
581 -- | Attempts to obtain the type variable underlying a 'Type', without
582 -- any expansion
583 repGetTyVar_maybe :: Type -> Maybe TyVar
584 repGetTyVar_maybe (TyVarTy tv) = Just tv
585 repGetTyVar_maybe _ = Nothing
586
587 {-
588 ---------------------------------------------------------------------
589 AppTy
590 ~~~~~
591 We need to be pretty careful with AppTy to make sure we obey the
592 invariant that a TyConApp is always visibly so. mkAppTy maintains the
593 invariant: use it.
594
595 Note [Decomposing fat arrow c=>t]
596 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
597 Can we unify (a b) with (Eq a => ty)? If we do so, we end up with
598 a partial application like ((=>) Eq a) which doesn't make sense in
599 source Haskell. In constrast, we *can* unify (a b) with (t1 -> t2).
600 Here's an example (Trac #9858) of how you might do it:
601 i :: (Typeable a, Typeable b) => Proxy (a b) -> TypeRep
602 i p = typeRep p
603
604 j = i (Proxy :: Proxy (Eq Int => Int))
605 The type (Proxy (Eq Int => Int)) is only accepted with -XImpredicativeTypes,
606 but suppose we want that. But then in the call to 'i', we end
607 up decomposing (Eq Int => Int), and we definitely don't want that.
608
609 This really only applies to the type checker; in Core, '=>' and '->'
610 are the same, as are 'Constraint' and '*'. But for now I've put
611 the test in repSplitAppTy_maybe, which applies throughout, because
612 the other calls to splitAppTy are in Unify, which is also used by
613 the type checker (e.g. when matching type-function equations).
614
615 -}
616
617 -- | Applies a type to another, as in e.g. @k a@
618 mkAppTy :: Type -> Type -> Type
619 mkAppTy (TyConApp tc tys) ty2 = mkTyConApp tc (tys ++ [ty2])
620 mkAppTy ty1 ty2 = AppTy ty1 ty2
621 -- Note that the TyConApp could be an
622 -- under-saturated type synonym. GHC allows that; e.g.
623 -- type Foo k = k a -> k a
624 -- type Id x = x
625 -- foo :: Foo Id -> Foo Id
626 --
627 -- Here Id is partially applied in the type sig for Foo,
628 -- but once the type synonyms are expanded all is well
629
630 mkAppTys :: Type -> [Type] -> Type
631 mkAppTys ty1 [] = ty1
632 mkAppTys (TyConApp tc tys1) tys2 = mkTyConApp tc (tys1 ++ tys2)
633 mkAppTys ty1 tys2 = foldl AppTy ty1 tys2
634
635 -------------
636 splitAppTy_maybe :: Type -> Maybe (Type, Type)
637 -- ^ Attempt to take a type application apart, whether it is a
638 -- function, type constructor, or plain type application. Note
639 -- that type family applications are NEVER unsaturated by this!
640 splitAppTy_maybe ty | Just ty' <- coreView ty
641 = splitAppTy_maybe ty'
642 splitAppTy_maybe ty = repSplitAppTy_maybe ty
643
644 -------------
645 repSplitAppTy_maybe :: Type -> Maybe (Type,Type)
646 -- ^ Does the AppTy split as in 'splitAppTy_maybe', but assumes that
647 -- any Core view stuff is already done
648 repSplitAppTy_maybe (ForAllTy (Anon ty1) ty2)
649 = Just (TyConApp funTyCon [ty1], ty2)
650 repSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2)
651 repSplitAppTy_maybe (TyConApp tc tys)
652 | mightBeUnsaturatedTyCon tc || tys `lengthExceeds` tyConArity tc
653 , Just (tys', ty') <- snocView tys
654 = Just (TyConApp tc tys', ty') -- Never create unsaturated type family apps!
655 repSplitAppTy_maybe _other = Nothing
656
657 -- this one doesn't braek apart (c => t).
658 -- See Note [Decomposing fat arrow c=>t]
659 -- Defined here to avoid module loops between Unify and TcType.
660 tcRepSplitAppTy_maybe :: Type -> Maybe (Type,Type)
661 -- ^ Does the AppTy split as in 'tcSplitAppTy_maybe', but assumes that
662 -- any coreView stuff is already done. Refuses to look through (c => t)
663 tcRepSplitAppTy_maybe (ForAllTy (Anon ty1) ty2)
664 | isConstraintKind (typeKind ty1) = Nothing -- See Note [Decomposing fat arrow c=>t]
665 | otherwise = Just (TyConApp funTyCon [ty1], ty2)
666 tcRepSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2)
667 tcRepSplitAppTy_maybe (TyConApp tc tys)
668 | mightBeUnsaturatedTyCon tc || tys `lengthExceeds` tyConArity tc
669 , Just (tys', ty') <- snocView tys
670 = Just (TyConApp tc tys', ty') -- Never create unsaturated type family apps!
671 tcRepSplitAppTy_maybe _other = Nothing
672 -------------
673 splitAppTy :: Type -> (Type, Type)
674 -- ^ Attempts to take a type application apart, as in 'splitAppTy_maybe',
675 -- and panics if this is not possible
676 splitAppTy ty = case splitAppTy_maybe ty of
677 Just pr -> pr
678 Nothing -> panic "splitAppTy"
679
680 -------------
681 splitAppTys :: Type -> (Type, [Type])
682 -- ^ Recursively splits a type as far as is possible, leaving a residual
683 -- type being applied to and the type arguments applied to it. Never fails,
684 -- even if that means returning an empty list of type applications.
685 splitAppTys ty = split ty ty []
686 where
687 split orig_ty ty args | Just ty' <- coreView ty = split orig_ty ty' args
688 split _ (AppTy ty arg) args = split ty ty (arg:args)
689 split _ (TyConApp tc tc_args) args
690 = let -- keep type families saturated
691 n | mightBeUnsaturatedTyCon tc = 0
692 | otherwise = tyConArity tc
693 (tc_args1, tc_args2) = splitAt n tc_args
694 in
695 (TyConApp tc tc_args1, tc_args2 ++ args)
696 split _ (ForAllTy (Anon ty1) ty2) args = ASSERT( null args )
697 (TyConApp funTyCon [], [ty1,ty2])
698 split orig_ty _ args = (orig_ty, args)
699
700 -- | Like 'splitAppTys', but doesn't look through type synonyms
701 repSplitAppTys :: Type -> (Type, [Type])
702 repSplitAppTys ty = split ty []
703 where
704 split (AppTy ty arg) args = split ty (arg:args)
705 split (TyConApp tc tc_args) args
706 = let n | mightBeUnsaturatedTyCon tc = 0
707 | otherwise = tyConArity tc
708 (tc_args1, tc_args2) = splitAt n tc_args
709 in
710 (TyConApp tc tc_args1, tc_args2 ++ args)
711 split (ForAllTy (Anon ty1) ty2) args = ASSERT( null args )
712 (TyConApp funTyCon [], [ty1, ty2])
713 split ty args = (ty, args)
714
715 {-
716 LitTy
717 ~~~~~
718 -}
719
720 mkNumLitTy :: Integer -> Type
721 mkNumLitTy n = LitTy (NumTyLit n)
722
723 -- | Is this a numeric literal. We also look through type synonyms.
724 isNumLitTy :: Type -> Maybe Integer
725 isNumLitTy ty | Just ty1 <- coreView ty = isNumLitTy ty1
726 isNumLitTy (LitTy (NumTyLit n)) = Just n
727 isNumLitTy _ = Nothing
728
729 mkStrLitTy :: FastString -> Type
730 mkStrLitTy s = LitTy (StrTyLit s)
731
732 -- | Is this a symbol literal. We also look through type synonyms.
733 isStrLitTy :: Type -> Maybe FastString
734 isStrLitTy ty | Just ty1 <- coreView ty = isStrLitTy ty1
735 isStrLitTy (LitTy (StrTyLit s)) = Just s
736 isStrLitTy _ = Nothing
737
738
739 -- | Is this type a custom user error?
740 -- If so, give us the kind and the error message.
741 userTypeError_maybe :: Type -> Maybe Type
742 userTypeError_maybe t
743 = do { (tc, _kind : msg : _) <- splitTyConApp_maybe t
744 -- There may be more than 2 arguments, if the type error is
745 -- used as a type constructor (e.g. at kind `Type -> Type`).
746
747 ; guard (tyConName tc == errorMessageTypeErrorFamName)
748 ; return msg }
749
750 -- | Render a type corresponding to a user type error into a SDoc.
751 pprUserTypeErrorTy :: Type -> SDoc
752 pprUserTypeErrorTy ty =
753 case splitTyConApp_maybe ty of
754
755 -- Text "Something"
756 Just (tc,[txt])
757 | tyConName tc == typeErrorTextDataConName
758 , Just str <- isStrLitTy txt -> ftext str
759
760 -- ShowType t
761 Just (tc,[_k,t])
762 | tyConName tc == typeErrorShowTypeDataConName -> ppr t
763
764 -- t1 :<>: t2
765 Just (tc,[t1,t2])
766 | tyConName tc == typeErrorAppendDataConName ->
767 pprUserTypeErrorTy t1 <> pprUserTypeErrorTy t2
768
769 -- t1 :$$: t2
770 Just (tc,[t1,t2])
771 | tyConName tc == typeErrorVAppendDataConName ->
772 pprUserTypeErrorTy t1 $$ pprUserTypeErrorTy t2
773
774 -- An uneavaluated type function
775 _ -> ppr ty
776
777
778
779
780 {-
781 ---------------------------------------------------------------------
782 FunTy
783 ~~~~~
784
785 Function types are represented with (ForAllTy (Anon ...) ...)
786 -}
787
788 isFunTy :: Type -> Bool
789 isFunTy ty = isJust (splitFunTy_maybe ty)
790
791 splitFunTy :: Type -> (Type, Type)
792 -- ^ Attempts to extract the argument and result types from a type, and
793 -- panics if that is not possible. See also 'splitFunTy_maybe'
794 splitFunTy ty | Just ty' <- coreView ty = splitFunTy ty'
795 splitFunTy (ForAllTy (Anon arg) res) = (arg, res)
796 splitFunTy other = pprPanic "splitFunTy" (ppr other)
797
798 splitFunTy_maybe :: Type -> Maybe (Type, Type)
799 -- ^ Attempts to extract the argument and result types from a type
800 splitFunTy_maybe ty | Just ty' <- coreView ty = splitFunTy_maybe ty'
801 splitFunTy_maybe (ForAllTy (Anon arg) res) = Just (arg, res)
802 splitFunTy_maybe _ = Nothing
803
804 splitFunTys :: Type -> ([Type], Type)
805 splitFunTys ty = split [] ty ty
806 where
807 split args orig_ty ty | Just ty' <- coreView ty = split args orig_ty ty'
808 split args _ (ForAllTy (Anon arg) res) = split (arg:args) res res
809 split args orig_ty _ = (reverse args, orig_ty)
810
811 splitFunTysN :: Int -> Type -> ([Type], Type)
812 -- ^ Split off exactly the given number argument types, and panics if that is not possible
813 splitFunTysN 0 ty = ([], ty)
814 splitFunTysN n ty = ASSERT2( isFunTy ty, int n <+> ppr ty )
815 case splitFunTy ty of { (arg, res) ->
816 case splitFunTysN (n-1) res of { (args, res) ->
817 (arg:args, res) }}
818
819 funResultTy :: Type -> Type
820 -- ^ Extract the function result type and panic if that is not possible
821 funResultTy ty | Just ty' <- coreView ty = funResultTy ty'
822 funResultTy (ForAllTy (Anon {}) res) = res
823 funResultTy ty = pprPanic "funResultTy" (ppr ty)
824
825 funArgTy :: Type -> Type
826 -- ^ Extract the function argument type and panic if that is not possible
827 funArgTy ty | Just ty' <- coreView ty = funArgTy ty'
828 funArgTy (ForAllTy (Anon arg) _res) = arg
829 funArgTy ty = pprPanic "funArgTy" (ppr ty)
830
831 piResultTy :: Type -> Type -> Type
832 -- ^ Just like 'piResultTys' but for a single argument
833 -- Try not to iterate 'piResultTy', because it's inefficient to substitute
834 -- one variable at a time; instead use 'piResultTys"
835 piResultTy ty arg
836 | Just ty' <- coreView ty = piResultTy ty' arg
837
838 | ForAllTy bndr res <- ty
839 = case bndr of
840 Anon {} -> res
841 Named tv _ -> substTy (extendTvSubst empty_subst tv arg) res
842 where
843 empty_subst = mkEmptyTCvSubst $ mkInScopeSet $
844 tyCoVarsOfTypes [arg,res]
845 | otherwise
846 = pprPanic "piResultTy" (ppr ty $$ ppr arg)
847
848 -- | (piResultTys f_ty [ty1, .., tyn]) gives the type of (f ty1 .. tyn)
849 -- where f :: f_ty
850 -- 'piResultTys' is interesting because:
851 -- 1. 'f_ty' may have more for-alls than there are args
852 -- 2. Less obviously, it may have fewer for-alls
853 -- For case 2. think of:
854 -- piResultTys (forall a.a) [forall b.b, Int]
855 -- This really can happen, but only (I think) in situations involving
856 -- undefined. For example:
857 -- undefined :: forall a. a
858 -- Term: undefined @(forall b. b->b) @Int
859 -- This term should have type (Int -> Int), but notice that
860 -- there are more type args than foralls in 'undefined's type.
861
862 -- If you edit this function, you may need to update the GHC formalism
863 -- See Note [GHC Formalism] in coreSyn/CoreLint.hs
864
865 -- This is a heavily used function (e.g. from typeKind),
866 -- so we pay attention to efficiency, especially in the special case
867 -- where there are no for-alls so we are just dropping arrows from
868 -- a function type/kind.
869 piResultTys :: Type -> [Type] -> Type
870 piResultTys ty [] = ty
871 piResultTys ty orig_args@(arg:args)
872 | Just ty' <- coreView ty
873 = piResultTys ty' orig_args
874
875 | ForAllTy bndr res <- ty
876 = case bndr of
877 Anon {} -> piResultTys res args
878 Named tv _ -> go (extendVarEnv emptyTvSubstEnv tv arg) res args
879
880 | otherwise
881 = pprPanic "piResultTys1" (ppr ty $$ ppr orig_args)
882 where
883 go :: TvSubstEnv -> Type -> [Type] -> Type
884 go tv_env ty [] = substTy (mkTvSubst in_scope tv_env) ty
885 where
886 in_scope = mkInScopeSet (tyCoVarsOfTypes (ty:orig_args))
887
888 go tv_env ty all_args@(arg:args)
889 | Just ty' <- coreView ty
890 = go tv_env ty' all_args
891
892 | ForAllTy bndr res <- ty
893 = case bndr of
894 Anon _ -> go tv_env res args
895 Named tv _ -> go (extendVarEnv tv_env tv arg) res args
896
897 | TyVarTy tv <- ty
898 , Just ty' <- lookupVarEnv tv_env tv
899 -- Deals with piResultTys (forall a. a) [forall b.b, Int]
900 = piResultTys ty' all_args
901
902 | otherwise
903 = pprPanic "piResultTys2" (ppr ty $$ ppr orig_args $$ ppr all_args)
904
905 applyTysX :: [TyVar] -> Type -> [Type] -> Type
906 -- applyTyxX beta-reduces (/\tvs. body_ty) arg_tys
907 -- Assumes that (/\tvs. body_ty) is closed
908 applyTysX tvs body_ty arg_tys
909 = ASSERT2( length arg_tys >= n_tvs, pp_stuff )
910 ASSERT2( tyCoVarsOfType body_ty `subVarSet` mkVarSet tvs, pp_stuff )
911 mkAppTys (substTyWith tvs (take n_tvs arg_tys) body_ty)
912 (drop n_tvs arg_tys)
913 where
914 pp_stuff = vcat [ppr tvs, ppr body_ty, ppr arg_tys]
915 n_tvs = length tvs
916
917 {-
918 ---------------------------------------------------------------------
919 TyConApp
920 ~~~~~~~~
921 -}
922
923 -- | A key function: builds a 'TyConApp' or 'FunTy' as appropriate to
924 -- its arguments. Applies its arguments to the constructor from left to right.
925 mkTyConApp :: TyCon -> [Type] -> Type
926 mkTyConApp tycon tys
927 | isFunTyCon tycon, [ty1,ty2] <- tys
928 = ForAllTy (Anon ty1) ty2
929
930 | otherwise
931 = TyConApp tycon tys
932
933 -- splitTyConApp "looks through" synonyms, because they don't
934 -- mean a distinct type, but all other type-constructor applications
935 -- including functions are returned as Just ..
936
937 -- | Retrieve the tycon heading this type, if there is one. Does /not/
938 -- look through synonyms.
939 tyConAppTyConPicky_maybe :: Type -> Maybe TyCon
940 tyConAppTyConPicky_maybe (TyConApp tc _) = Just tc
941 tyConAppTyConPicky_maybe (ForAllTy (Anon _) _) = Just funTyCon
942 tyConAppTyConPicky_maybe _ = Nothing
943
944
945 -- | The same as @fst . splitTyConApp@
946 tyConAppTyCon_maybe :: Type -> Maybe TyCon
947 tyConAppTyCon_maybe ty | Just ty' <- coreView ty = tyConAppTyCon_maybe ty'
948 tyConAppTyCon_maybe (TyConApp tc _) = Just tc
949 tyConAppTyCon_maybe (ForAllTy (Anon _) _) = Just funTyCon
950 tyConAppTyCon_maybe _ = Nothing
951
952 tyConAppTyCon :: Type -> TyCon
953 tyConAppTyCon ty = tyConAppTyCon_maybe ty `orElse` pprPanic "tyConAppTyCon" (ppr ty)
954
955 -- | The same as @snd . splitTyConApp@
956 tyConAppArgs_maybe :: Type -> Maybe [Type]
957 tyConAppArgs_maybe ty | Just ty' <- coreView ty = tyConAppArgs_maybe ty'
958 tyConAppArgs_maybe (TyConApp _ tys) = Just tys
959 tyConAppArgs_maybe (ForAllTy (Anon arg) res) = Just [arg,res]
960 tyConAppArgs_maybe _ = Nothing
961
962 tyConAppArgs :: Type -> [Type]
963 tyConAppArgs ty = tyConAppArgs_maybe ty `orElse` pprPanic "tyConAppArgs" (ppr ty)
964
965 tyConAppArgN :: Int -> Type -> Type
966 -- Executing Nth
967 tyConAppArgN n ty
968 = case tyConAppArgs_maybe ty of
969 Just tys -> ASSERT2( n < length tys, ppr n <+> ppr tys ) tys `getNth` n
970 Nothing -> pprPanic "tyConAppArgN" (ppr n <+> ppr ty)
971
972 -- | Attempts to tease a type apart into a type constructor and the application
973 -- of a number of arguments to that constructor. Panics if that is not possible.
974 -- See also 'splitTyConApp_maybe'
975 splitTyConApp :: Type -> (TyCon, [Type])
976 splitTyConApp ty = case splitTyConApp_maybe ty of
977 Just stuff -> stuff
978 Nothing -> pprPanic "splitTyConApp" (ppr ty)
979
980 -- | Attempts to tease a type apart into a type constructor and the application
981 -- of a number of arguments to that constructor
982 splitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
983 splitTyConApp_maybe ty | Just ty' <- coreView ty = splitTyConApp_maybe ty'
984 splitTyConApp_maybe ty = repSplitTyConApp_maybe ty
985
986 -- | Like 'splitTyConApp_maybe', but doesn't look through synonyms. This
987 -- assumes the synonyms have already been dealt with.
988 repSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
989 repSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
990 repSplitTyConApp_maybe (ForAllTy (Anon arg) res) = Just (funTyCon, [arg,res])
991 repSplitTyConApp_maybe _ = Nothing
992
993 -- | Attempts to tease a list type apart and gives the type of the elements if
994 -- successful (looks through type synonyms)
995 splitListTyConApp_maybe :: Type -> Maybe Type
996 splitListTyConApp_maybe ty = case splitTyConApp_maybe ty of
997 Just (tc,[e]) | tc == listTyCon -> Just e
998 _other -> Nothing
999
1000 -- | What is the role assigned to the next parameter of this type? Usually,
1001 -- this will be 'Nominal', but if the type is a 'TyConApp', we may be able to
1002 -- do better. The type does *not* have to be well-kinded when applied for this
1003 -- to work!
1004 nextRole :: Type -> Role
1005 nextRole ty
1006 | Just (tc, tys) <- splitTyConApp_maybe ty
1007 , let num_tys = length tys
1008 , num_tys < tyConArity tc
1009 = tyConRoles tc `getNth` num_tys
1010
1011 | otherwise
1012 = Nominal
1013
1014 newTyConInstRhs :: TyCon -> [Type] -> Type
1015 -- ^ Unwrap one 'layer' of newtype on a type constructor and its
1016 -- arguments, using an eta-reduced version of the @newtype@ if possible.
1017 -- This requires tys to have at least @newTyConInstArity tycon@ elements.
1018 newTyConInstRhs tycon tys
1019 = ASSERT2( tvs `leLength` tys, ppr tycon $$ ppr tys $$ ppr tvs )
1020 applyTysX tvs rhs tys
1021 where
1022 (tvs, rhs) = newTyConEtadRhs tycon
1023
1024 {-
1025 ---------------------------------------------------------------------
1026 CastTy
1027 ~~~~~~
1028 A casted type has its *kind* casted into something new.
1029
1030 Note [Weird typing rule for ForAllTy]
1031 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1032
1033 Here is the (truncated) typing rule for the dependent ForAllTy:
1034
1035 inner : kind
1036 ------------------------------------
1037 ForAllTy (Named tv vis) inner : kind
1038
1039 Note that neither the inner type nor for ForAllTy itself have to have
1040 kind *! But, it means that we should push any kind casts through the
1041 ForAllTy. The only trouble is avoiding capture.
1042
1043 -}
1044
1045 splitCastTy_maybe :: Type -> Maybe (Type, Coercion)
1046 splitCastTy_maybe ty | Just ty' <- coreView ty = splitCastTy_maybe ty'
1047 splitCastTy_maybe (CastTy ty co) = Just (ty, co)
1048 splitCastTy_maybe _ = Nothing
1049
1050 -- | Make a 'CastTy'. The Coercion must be nominal. This function looks
1051 -- at the entire structure of the type and coercion in an attempt to
1052 -- maintain representation invariance (that is, any two types that are `eqType`
1053 -- look the same). Be very wary of calling this in a loop.
1054 mkCastTy :: Type -> Coercion -> Type
1055 -- Running example:
1056 -- T :: forall k1. k1 -> forall k2. k2 -> Bool -> Maybe k1 -> *
1057 -- co :: * ~R X (maybe X is a newtype around *)
1058 -- ty = T Nat 3 Symbol "foo" True (Just 2)
1059 --
1060 -- We wish to "push" the cast down as far as possible. See also
1061 -- Note [Pushing down casts] in TyCoRep. Here is where we end
1062 -- up:
1063 --
1064 -- (T Nat 3 Symbol |> <Symbol> -> <Bool> -> <Maybe Nat> -> co)
1065 -- "foo" True (Just 2)
1066 --
1067 mkCastTy ty co | isReflexiveCo co = ty
1068 -- NB: Do the slow check here. This is important to keep the splitXXX
1069 -- functions working properly. Otherwise, we may end up with something
1070 -- like (((->) |> something_reflexive_but_not_obviously_so) biz baz)
1071 -- fails under splitFunTy_maybe. This happened with the cheaper check
1072 -- in test dependent/should_compile/dynamic-paper.
1073
1074 mkCastTy (CastTy ty co1) co2 = mkCastTy ty (co1 `mkTransCo` co2)
1075 -- See Note [Weird typing rule for ForAllTy]
1076 mkCastTy outer_ty@(ForAllTy (Named tv vis) inner_ty) co
1077 = -- have to make sure that pushing the co in doesn't capture the bound var
1078 let fvs = tyCoVarsOfCo co `unionVarSet` tyCoVarsOfType outer_ty
1079 empty_subst = mkEmptyTCvSubst (mkInScopeSet fvs)
1080 (subst, tv') = substTyVarBndr empty_subst tv
1081 in
1082 ForAllTy (Named tv' vis) (substTy subst inner_ty `mkCastTy` co)
1083 mkCastTy ty co = -- NB: don't check if the coercion "from" type matches here;
1084 -- there may be unzonked variables about
1085 let result = split_apps [] ty co in
1086 ASSERT2( CastTy ty co `eqType` result
1087 , ppr ty <+> dcolon <+> ppr (typeKind ty) $$
1088 ppr co <+> dcolon <+> ppr (coercionKind co) $$
1089 ppr result <+> dcolon <+> ppr (typeKind result) )
1090 result
1091 where
1092 -- split_apps breaks apart any type applications, so we can see how far down
1093 -- to push the cast
1094 split_apps args (AppTy t1 t2) co
1095 = split_apps (t2:args) t1 co
1096 split_apps args (TyConApp tc tc_args) co
1097 | mightBeUnsaturatedTyCon tc
1098 = affix_co (tyConBinders tc) (mkTyConTy tc) (tc_args `chkAppend` args) co
1099 | otherwise -- not decomposable... but it may still be oversaturated
1100 = let (non_decomp_args, decomp_args) = splitAt (tyConArity tc) tc_args
1101 saturated_tc = mkTyConApp tc non_decomp_args
1102 in
1103 affix_co (fst $ splitPiTys $ typeKind saturated_tc)
1104 saturated_tc (decomp_args `chkAppend` args) co
1105
1106 split_apps args (ForAllTy (Anon arg) res) co
1107 = affix_co (tyConBinders funTyCon) (mkTyConTy funTyCon)
1108 (arg : res : args) co
1109 split_apps args ty co
1110 = affix_co (fst $ splitPiTys $ typeKind ty)
1111 ty args co
1112
1113 -- having broken everything apart, this figures out the point at which there
1114 -- are no more dependent quantifications, and puts the cast there
1115 affix_co _ ty [] co = no_double_casts ty co
1116 affix_co bndrs ty args co
1117 -- if kind contains any dependent quantifications, we can't push.
1118 -- apply arguments until it doesn't
1119 = let (no_dep_bndrs, some_dep_bndrs) = spanEnd isAnonBinder bndrs
1120 (some_dep_args, rest_args) = splitAtList some_dep_bndrs args
1121 dep_subst = zipTyBinderSubst some_dep_bndrs some_dep_args
1122 used_no_dep_bndrs = takeList rest_args no_dep_bndrs
1123 rest_arg_tys = substTys dep_subst (map binderType used_no_dep_bndrs)
1124 co' = mkFunCos Nominal
1125 (map (mkReflCo Nominal) rest_arg_tys)
1126 co
1127 in
1128 ((ty `mkAppTys` some_dep_args) `no_double_casts` co') `mkAppTys` rest_args
1129
1130 no_double_casts (CastTy ty co1) co2 = CastTy ty (co1 `mkTransCo` co2)
1131 no_double_casts ty co = CastTy ty co
1132
1133 {-
1134 --------------------------------------------------------------------
1135 CoercionTy
1136 ~~~~~~~~~~
1137 CoercionTy allows us to inject coercions into types. A CoercionTy
1138 should appear only in the right-hand side of an application.
1139 -}
1140
1141 mkCoercionTy :: Coercion -> Type
1142 mkCoercionTy = CoercionTy
1143
1144 isCoercionTy :: Type -> Bool
1145 isCoercionTy (CoercionTy _) = True
1146 isCoercionTy _ = False
1147
1148 isCoercionTy_maybe :: Type -> Maybe Coercion
1149 isCoercionTy_maybe (CoercionTy co) = Just co
1150 isCoercionTy_maybe _ = Nothing
1151
1152 stripCoercionTy :: Type -> Coercion
1153 stripCoercionTy (CoercionTy co) = co
1154 stripCoercionTy ty = pprPanic "stripCoercionTy" (ppr ty)
1155
1156 {-
1157 ---------------------------------------------------------------------
1158 SynTy
1159 ~~~~~
1160
1161 Notes on type synonyms
1162 ~~~~~~~~~~~~~~~~~~~~~~
1163 The various "split" functions (splitFunTy, splitRhoTy, splitForAllTy) try
1164 to return type synonyms wherever possible. Thus
1165
1166 type Foo a = a -> a
1167
1168 we want
1169 splitFunTys (a -> Foo a) = ([a], Foo a)
1170 not ([a], a -> a)
1171
1172 The reason is that we then get better (shorter) type signatures in
1173 interfaces. Notably this plays a role in tcTySigs in TcBinds.hs.
1174
1175
1176 Representation types
1177 ~~~~~~~~~~~~~~~~~~~~
1178
1179 Note [Nullary unboxed tuple]
1180 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1181 We represent the nullary unboxed tuple as the unary (but void) type
1182 Void#. The reason for this is that the ReprArity is never
1183 less than the Arity (as it would otherwise be for a function type like
1184 (# #) -> Int).
1185
1186 As a result, ReprArity is always strictly positive if Arity is. This
1187 is important because it allows us to distinguish at runtime between a
1188 thunk and a function takes a nullary unboxed tuple as an argument!
1189 -}
1190
1191 type UnaryType = Type
1192
1193 data RepType = UbxTupleRep [UnaryType] -- INVARIANT: never an empty list (see Note [Nullary unboxed tuple])
1194 | UnaryRep UnaryType
1195
1196 instance Outputable RepType where
1197 ppr (UbxTupleRep tys) = text "UbxTupleRep" <+> ppr tys
1198 ppr (UnaryRep ty) = text "UnaryRep" <+> ppr ty
1199
1200 flattenRepType :: RepType -> [UnaryType]
1201 flattenRepType (UbxTupleRep tys) = tys
1202 flattenRepType (UnaryRep ty) = [ty]
1203
1204 -- | Looks through:
1205 --
1206 -- 1. For-alls
1207 -- 2. Synonyms
1208 -- 3. Predicates
1209 -- 4. All newtypes, including recursive ones, but not newtype families
1210 -- 5. Casts
1211 --
1212 -- It's useful in the back end of the compiler.
1213 repType :: Type -> RepType
1214 repType ty
1215 = go initRecTc ty
1216 where
1217 go :: RecTcChecker -> Type -> RepType
1218 go rec_nts ty -- Expand predicates and synonyms
1219 | Just ty' <- coreView ty
1220 = go rec_nts ty'
1221
1222 go rec_nts (ForAllTy (Named {}) ty2) -- Drop type foralls
1223 = go rec_nts ty2
1224
1225 go rec_nts (TyConApp tc tys) -- Expand newtypes
1226 | isNewTyCon tc
1227 , tys `lengthAtLeast` tyConArity tc
1228 , Just rec_nts' <- checkRecTc rec_nts tc -- See Note [Expanding newtypes] in TyCon
1229 = go rec_nts' (newTyConInstRhs tc tys)
1230
1231 | isUnboxedTupleTyCon tc
1232 = if null tys
1233 then UnaryRep voidPrimTy -- See Note [Nullary unboxed tuple]
1234 else UbxTupleRep (concatMap (flattenRepType . go rec_nts) non_rr_tys)
1235 where
1236 -- See Note [Unboxed tuple RuntimeRep vars] in TyCon
1237 non_rr_tys = dropRuntimeRepArgs tys
1238
1239 go rec_nts (CastTy ty _)
1240 = go rec_nts ty
1241
1242 go _ ty@(CoercionTy _)
1243 = pprPanic "repType" (ppr ty)
1244
1245 go _ ty = UnaryRep ty
1246
1247 -- ToDo: this could be moved to the code generator, using splitTyConApp instead
1248 -- of inspecting the type directly.
1249
1250 -- | Discovers the primitive representation of a more abstract 'UnaryType'
1251 typePrimRep :: UnaryType -> PrimRep
1252 typePrimRep ty = kindPrimRep (typeKind ty)
1253
1254 -- | Find the primitive representation of a 'TyCon'. Defined here to
1255 -- avoid module loops. Call this only on unlifted tycons.
1256 tyConPrimRep :: TyCon -> PrimRep
1257 tyConPrimRep tc = kindPrimRep res_kind
1258 where
1259 res_kind = tyConResKind tc
1260
1261 -- | Take a kind (of shape @TYPE rr@) and produce the 'PrimRep' of values
1262 -- of types of this kind.
1263 kindPrimRep :: Kind -> PrimRep
1264 kindPrimRep ki | Just ki' <- coreViewOneStarKind ki = kindPrimRep ki'
1265 kindPrimRep (TyConApp typ [runtime_rep])
1266 = ASSERT( typ `hasKey` tYPETyConKey )
1267 go runtime_rep
1268 where
1269 go rr | Just rr' <- coreView rr = go rr'
1270 go (TyConApp rr_dc args)
1271 | RuntimeRep fun <- tyConRuntimeRepInfo rr_dc
1272 = fun args
1273 go rr = pprPanic "kindPrimRep.go" (ppr rr)
1274 kindPrimRep ki = WARN( True
1275 , text "kindPrimRep defaulting to PtrRep on" <+> ppr ki )
1276 PtrRep -- this can happen legitimately for, e.g., Any
1277
1278 typeRepArity :: Arity -> Type -> RepArity
1279 typeRepArity 0 _ = 0
1280 typeRepArity n ty = case repType ty of
1281 UnaryRep (ForAllTy bndr ty) -> length (flattenRepType (repType (binderType bndr))) + typeRepArity (n - 1) ty
1282 _ -> pprPanic "typeRepArity: arity greater than type can handle" (ppr (n, ty, repType ty))
1283
1284 isVoidTy :: Type -> Bool
1285 -- True if the type has zero width
1286 isVoidTy ty = case repType ty of
1287 UnaryRep (TyConApp tc _) -> isUnliftedTyCon tc &&
1288 isVoidRep (tyConPrimRep tc)
1289 _ -> False
1290
1291 {-
1292 Note [AppTy rep]
1293 ~~~~~~~~~~~~~~~~
1294 Types of the form 'f a' must be of kind *, not #, so we are guaranteed
1295 that they are represented by pointers. The reason is that f must have
1296 kind (kk -> kk) and kk cannot be unlifted; see Note [The kind invariant]
1297 in TyCoRep.
1298
1299 ---------------------------------------------------------------------
1300 ForAllTy
1301 ~~~~~~~~
1302 -}
1303
1304 mkForAllTy :: TyBinder -> Type -> Type
1305 mkForAllTy = ForAllTy
1306
1307 -- | Make a dependent forall.
1308 mkNamedForAllTy :: TyVar -> VisibilityFlag -> Type -> Type
1309 mkNamedForAllTy tv vis = ASSERT( isTyVar tv )
1310 ForAllTy (Named tv vis)
1311
1312 -- | Like mkForAllTys, but assumes all variables are dependent and invisible,
1313 -- a common case
1314 mkInvForAllTys :: [TyVar] -> Type -> Type
1315 mkInvForAllTys tvs = ASSERT( all isTyVar tvs )
1316 mkForAllTys (map (flip Named Invisible) tvs)
1317
1318 -- | Like mkForAllTys, but assumes all variables are dependent and specified,
1319 -- a common case
1320 mkSpecForAllTys :: [TyVar] -> Type -> Type
1321 mkSpecForAllTys tvs = ASSERT( all isTyVar tvs )
1322 mkForAllTys (map (flip Named Specified) tvs)
1323
1324 -- | Like mkForAllTys, but assumes all variables are dependent and visible
1325 mkVisForAllTys :: [TyVar] -> Type -> Type
1326 mkVisForAllTys tvs = ASSERT( all isTyVar tvs )
1327 mkForAllTys (map (flip Named Visible) tvs)
1328
1329 mkPiType :: Var -> Type -> Type
1330 -- ^ Makes a @(->)@ type or an implicit forall type, depending
1331 -- on whether it is given a type variable or a term variable.
1332 -- This is used, for example, when producing the type of a lambda.
1333 -- Always uses Invisible binders.
1334 mkPiTypes :: [Var] -> Type -> Type
1335 -- ^ 'mkPiType' for multiple type or value arguments
1336
1337 mkPiType v ty
1338 | isTyVar v = mkForAllTy (Named v Invisible) ty
1339 | otherwise = mkForAllTy (Anon (varType v)) ty
1340
1341 mkPiTypes vs ty = foldr mkPiType ty vs
1342
1343 -- | Given a list of type-level vars and a result type, makes TyBinders, preferring
1344 -- anonymous binders if the variable is, in fact, not dependent.
1345 -- All binders are /visible/.
1346 mkTyBindersPreferAnon :: [TyVar] -> Type -> [TyBinder]
1347 mkTyBindersPreferAnon vars inner_ty = fst $ go vars inner_ty
1348 where
1349 go :: [TyVar] -> Type -> ([TyBinder], VarSet) -- also returns the free vars
1350 go [] ty = ([], tyCoVarsOfType ty)
1351 go (v:vs) ty | v `elemVarSet` fvs
1352 = ( Named v Visible : binders
1353 , fvs `delVarSet` v `unionVarSet` kind_vars )
1354 | otherwise
1355 = ( Anon (tyVarKind v) : binders
1356 , fvs `unionVarSet` kind_vars )
1357 where
1358 (binders, fvs) = go vs ty
1359 kind_vars = tyCoVarsOfType $ tyVarKind v
1360
1361 -- | Take a ForAllTy apart, returning the list of tyvars and the result type.
1362 -- This always succeeds, even if it returns only an empty list. Note that the
1363 -- result type returned may have free variables that were bound by a forall.
1364 splitForAllTys :: Type -> ([TyVar], Type)
1365 splitForAllTys ty = split ty ty []
1366 where
1367 split orig_ty ty tvs | Just ty' <- coreView ty = split orig_ty ty' tvs
1368 split _ (ForAllTy (Named tv _) ty) tvs = split ty ty (tv:tvs)
1369 split orig_ty _ tvs = (reverse tvs, orig_ty)
1370
1371 -- | Split off all TyBinders to a type, splitting both proper foralls
1372 -- and functions
1373 splitPiTys :: Type -> ([TyBinder], Type)
1374 splitPiTys ty = split ty ty []
1375 where
1376 split orig_ty ty bs | Just ty' <- coreView ty = split orig_ty ty' bs
1377 split _ (ForAllTy b res) bs = split res res (b:bs)
1378 split orig_ty _ bs = (reverse bs, orig_ty)
1379
1380 -- | Like 'splitPiTys' but split off only /named/ binders.
1381 splitNamedPiTys :: Type -> ([TyBinder], Type)
1382 splitNamedPiTys ty = split ty ty []
1383 where
1384 split orig_ty ty bs | Just ty' <- coreView ty = split orig_ty ty' bs
1385 split _ (ForAllTy b@(Named {}) res) bs = split res res (b:bs)
1386 split orig_ty _ bs = (reverse bs, orig_ty)
1387
1388 -- | Checks whether this is a proper forall (with a named binder)
1389 isForAllTy :: Type -> Bool
1390 isForAllTy (ForAllTy (Named {}) _) = True
1391 isForAllTy _ = False
1392
1393 -- | Is this a function or forall?
1394 isPiTy :: Type -> Bool
1395 isPiTy (ForAllTy {}) = True
1396 isPiTy _ = False
1397
1398 -- | Take a forall type apart, or panics if that is not possible.
1399 splitForAllTy :: Type -> (TyVar, Type)
1400 splitForAllTy ty
1401 | Just answer <- splitForAllTy_maybe ty = answer
1402 | otherwise = pprPanic "splitForAllTy" (ppr ty)
1403
1404 -- | Attempts to take a forall type apart, but only if it's a proper forall,
1405 -- with a named binder
1406 splitForAllTy_maybe :: Type -> Maybe (TyVar, Type)
1407 splitForAllTy_maybe ty = splitFAT_m ty
1408 where
1409 splitFAT_m ty | Just ty' <- coreView ty = splitFAT_m ty'
1410 splitFAT_m (ForAllTy (Named tv _) ty) = Just (tv, ty)
1411 splitFAT_m _ = Nothing
1412
1413 -- | Attempts to take a forall type apart; works with proper foralls and
1414 -- functions
1415 splitPiTy_maybe :: Type -> Maybe (TyBinder, Type)
1416 splitPiTy_maybe ty = go ty
1417 where
1418 go ty | Just ty' <- coreView ty = go ty'
1419 go (ForAllTy bndr ty) = Just (bndr, ty)
1420 go _ = Nothing
1421
1422 -- | Takes a forall type apart, or panics
1423 splitPiTy :: Type -> (TyBinder, Type)
1424 splitPiTy ty
1425 | Just answer <- splitPiTy_maybe ty = answer
1426 | otherwise = pprPanic "splitPiTy" (ppr ty)
1427
1428 -- | Drops all non-anonymous ForAllTys
1429 dropForAlls :: Type -> Type
1430 dropForAlls ty | Just ty' <- coreView ty = dropForAlls ty'
1431 | otherwise = go ty
1432 where
1433 go (ForAllTy (Named {}) res) = go res
1434 go res = res
1435
1436 -- | Given a tycon and its arguments, filters out any invisible arguments
1437 filterOutInvisibleTypes :: TyCon -> [Type] -> [Type]
1438 filterOutInvisibleTypes tc tys = snd $ partitionInvisibles tc id tys
1439
1440 -- | Like 'filterOutInvisibles', but works on 'TyVar's
1441 filterOutInvisibleTyVars :: TyCon -> [TyVar] -> [TyVar]
1442 filterOutInvisibleTyVars tc tvs = snd $ partitionInvisibles tc mkTyVarTy tvs
1443
1444 -- | Given a tycon and a list of things (which correspond to arguments),
1445 -- partitions the things into the invisible ones and the visible ones.
1446 -- The callback function is necessary for this scenario:
1447 --
1448 -- > T :: forall k. k -> k
1449 -- > partitionInvisibles T [forall m. m -> m -> m, S, R, Q]
1450 --
1451 -- After substituting, we get
1452 --
1453 -- > T (forall m. m -> m -> m) :: (forall m. m -> m -> m) -> forall n. n -> n -> n
1454 --
1455 -- Thus, the first argument is invisible, @S@ is visible, @R@ is invisible again,
1456 -- and @Q@ is visible.
1457 --
1458 -- If you're absolutely sure that your tycon's kind doesn't end in a variable,
1459 -- it's OK if the callback function panics, as that's the only time it's
1460 -- consulted.
1461 partitionInvisibles :: TyCon -> (a -> Type) -> [a] -> ([a], [a])
1462 partitionInvisibles tc get_ty = go emptyTCvSubst (tyConKind tc)
1463 where
1464 go _ _ [] = ([], [])
1465 go subst (ForAllTy bndr res_ki) (x:xs)
1466 | isVisibleBinder bndr = second (x :) (go subst' res_ki xs)
1467 | otherwise = first (x :) (go subst' res_ki xs)
1468 where
1469 subst' = extendTvSubstBinder subst bndr (get_ty x)
1470 go subst (TyVarTy tv) xs
1471 | Just ki <- lookupTyVar subst tv = go subst ki xs
1472 go _ _ xs = ([], xs) -- something is ill-kinded. But this can happen
1473 -- when printing errors. Assume everything is visible.
1474
1475 -- like splitPiTys, but returns only *invisible* binders, including constraints
1476 splitPiTysInvisible :: Type -> ([TyBinder], Type)
1477 splitPiTysInvisible ty = split ty ty []
1478 where
1479 split orig_ty ty bndrs
1480 | Just ty' <- coreView ty = split orig_ty ty' bndrs
1481 split _ (ForAllTy bndr ty) bndrs
1482 | isInvisibleBinder bndr
1483 = split ty ty (bndr:bndrs)
1484
1485 split orig_ty _ bndrs
1486 = (reverse bndrs, orig_ty)
1487
1488 {-
1489 %************************************************************************
1490 %* *
1491 TyBinders
1492 %* *
1493 %************************************************************************
1494 -}
1495
1496 -- | Make a named binder
1497 mkNamedBinder :: VisibilityFlag -> Var -> TyBinder
1498 mkNamedBinder vis var = Named var vis
1499
1500 -- | Make many named binders
1501 mkNamedBinders :: VisibilityFlag -> [TyVar] -> [TyBinder]
1502 mkNamedBinders vis = map (mkNamedBinder vis)
1503
1504 -- | Make an anonymous binder
1505 mkAnonBinder :: Type -> TyBinder
1506 mkAnonBinder = Anon
1507
1508 -- | Does this binder bind a variable that is /not/ erased? Returns
1509 -- 'True' for anonymous binders.
1510 isIdLikeBinder :: TyBinder -> Bool
1511 isIdLikeBinder (Named {}) = False
1512 isIdLikeBinder (Anon {}) = True
1513
1514 -- | Does this type, when used to the left of an arrow, require
1515 -- a visible argument? This checks to see if the kind of the type
1516 -- is constraint.
1517 isVisibleType :: Type -> Bool
1518 isVisibleType = not . isPredTy
1519
1520 binderVisibility :: TyBinder -> VisibilityFlag
1521 binderVisibility (Named _ vis) = vis
1522 binderVisibility (Anon ty)
1523 | isVisibleType ty = Visible
1524 | otherwise = Invisible
1525
1526 -- | Extract a bound variable in a binder, if any
1527 binderVar_maybe :: TyBinder -> Maybe Var
1528 binderVar_maybe (Named v _) = Just v
1529 binderVar_maybe (Anon {}) = Nothing
1530
1531 -- | Extract a bound variable in a binder, or panics
1532 binderVar :: String -- ^ printed if there is a panic
1533 -> TyBinder -> Var
1534 binderVar _ (Named v _) = v
1535 binderVar e (Anon t) = pprPanic ("binderVar (" ++ e ++ ")") (ppr t)
1536
1537 -- | Extract a relevant type, if there is one.
1538 binderRelevantType_maybe :: TyBinder -> Maybe Type
1539 binderRelevantType_maybe (Named {}) = Nothing
1540 binderRelevantType_maybe (Anon ty) = Just ty
1541
1542 -- | Like 'maybe', but for binders.
1543 caseBinder :: TyBinder -- ^ binder to scrutinize
1544 -> (TyVar -> a) -- ^ named case
1545 -> (Type -> a) -- ^ anonymous case
1546 -> a
1547 caseBinder (Named v _) f _ = f v
1548 caseBinder (Anon t) _ d = d t
1549
1550 -- | Break apart a list of binders into tyvars and anonymous types.
1551 partitionBinders :: [TyBinder] -> ([TyVar], [Type])
1552 partitionBinders = partitionWith named_or_anon
1553 where
1554 named_or_anon bndr = caseBinder bndr Left Right
1555
1556 -- | Break apart a list of binders into a list of named binders and
1557 -- a list of anonymous types.
1558 partitionBindersIntoBinders :: [TyBinder] -> ([TyBinder], [Type])
1559 partitionBindersIntoBinders = partitionWith named_or_anon
1560 where
1561 named_or_anon bndr = caseBinder bndr (\_ -> Left bndr) Right
1562
1563 {-
1564 %************************************************************************
1565 %* *
1566 Pred
1567 * *
1568 ************************************************************************
1569
1570 Predicates on PredType
1571
1572 Note [isPredTy complications]
1573 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1574 You would think that we could define
1575 isPredTy ty = isConstraintKind (typeKind ty)
1576 But there are a number of complications:
1577
1578 * isPredTy is used when printing types, which can happen in debug
1579 printing during type checking of not-fully-zonked types. So it's
1580 not cool to say isConstraintKind (typeKind ty) because, absent
1581 zonking, the type might be ill-kinded, and typeKind crashes. Hence the
1582 rather tiresome story here
1583
1584 * isPredTy must return "True" to *unlifted* coercions, such as (t1 ~# t2)
1585 and (t1 ~R# t2), which are not of kind Constraint! Currently they are
1586 of kind #.
1587
1588 * If we do form the type '(C a => C [a]) => blah', then we'd like to
1589 print it as such. But that means that isPredTy must return True for
1590 (C a => C [a]). Admittedly that type is illegal in Haskell, but we
1591 want to print it nicely in error messages.
1592 -}
1593
1594 -- | Is the type suitable to classify a given/wanted in the typechecker?
1595 isPredTy :: Type -> Bool
1596 -- See Note [isPredTy complications]
1597 isPredTy ty = go ty []
1598 where
1599 go :: Type -> [KindOrType] -> Bool
1600 go (AppTy ty1 ty2) args = go ty1 (ty2 : args)
1601 go (TyVarTy tv) args = go_k (tyVarKind tv) args
1602 go (TyConApp tc tys) args = ASSERT( null args ) -- TyConApp invariant
1603 go_tc tc tys
1604 go (ForAllTy (Anon arg) res) []
1605 | isPredTy arg = isPredTy res -- (Eq a => C a)
1606 | otherwise = False -- (Int -> Bool)
1607 go (ForAllTy (Named {}) ty) [] = go ty []
1608 go _ _ = False
1609
1610 go_tc :: TyCon -> [KindOrType] -> Bool
1611 go_tc tc args
1612 | tc `hasKey` eqPrimTyConKey || tc `hasKey` eqReprPrimTyConKey
1613 = length args == 4 -- ~# and ~R# sadly have result kind #
1614 -- not Contraint; but we still want
1615 -- isPredTy to reply True.
1616 | otherwise = go_k (tyConKind tc) args
1617
1618 go_k :: Kind -> [KindOrType] -> Bool
1619 -- True <=> ('k' applied to 'kts') = Constraint
1620 go_k k args = isConstraintKind (piResultTys k args)
1621
1622 isClassPred, isEqPred, isNomEqPred, isIPPred :: PredType -> Bool
1623 isClassPred ty = case tyConAppTyCon_maybe ty of
1624 Just tyCon | isClassTyCon tyCon -> True
1625 _ -> False
1626 isEqPred ty = case tyConAppTyCon_maybe ty of
1627 Just tyCon -> tyCon `hasKey` eqPrimTyConKey
1628 || tyCon `hasKey` eqReprPrimTyConKey
1629 _ -> False
1630
1631 isNomEqPred ty = case tyConAppTyCon_maybe ty of
1632 Just tyCon -> tyCon `hasKey` eqPrimTyConKey
1633 _ -> False
1634
1635 isIPPred ty = case tyConAppTyCon_maybe ty of
1636 Just tc -> isIPTyCon tc
1637 _ -> False
1638
1639 isIPTyCon :: TyCon -> Bool
1640 isIPTyCon tc = tc `hasKey` ipClassKey
1641 -- Class and its corresponding TyCon have the same Unique
1642
1643 isIPClass :: Class -> Bool
1644 isIPClass cls = cls `hasKey` ipClassKey
1645
1646 isCTupleClass :: Class -> Bool
1647 isCTupleClass cls = isTupleTyCon (classTyCon cls)
1648
1649 isIPPred_maybe :: Type -> Maybe (FastString, Type)
1650 isIPPred_maybe ty =
1651 do (tc,[t1,t2]) <- splitTyConApp_maybe ty
1652 guard (isIPTyCon tc)
1653 x <- isStrLitTy t1
1654 return (x,t2)
1655
1656 {-
1657 Make PredTypes
1658
1659 --------------------- Equality types ---------------------------------
1660 -}
1661
1662 -- | Makes a lifted equality predicate at the given role
1663 mkPrimEqPredRole :: Role -> Type -> Type -> PredType
1664 mkPrimEqPredRole Nominal = mkPrimEqPred
1665 mkPrimEqPredRole Representational = mkReprPrimEqPred
1666 mkPrimEqPredRole Phantom = panic "mkPrimEqPredRole phantom"
1667
1668 -- | Creates a primitive type equality predicate.
1669 -- Invariant: the types are not Coercions
1670 mkPrimEqPred :: Type -> Type -> Type
1671 mkPrimEqPred ty1 ty2
1672 = TyConApp eqPrimTyCon [k1, k2, ty1, ty2]
1673 where
1674 k1 = typeKind ty1
1675 k2 = typeKind ty2
1676
1677 -- | Creates a primite type equality predicate with explicit kinds
1678 mkHeteroPrimEqPred :: Kind -> Kind -> Type -> Type -> Type
1679 mkHeteroPrimEqPred k1 k2 ty1 ty2 = TyConApp eqPrimTyCon [k1, k2, ty1, ty2]
1680
1681 -- | Creates a primitive representational type equality predicate
1682 -- with explicit kinds
1683 mkHeteroReprPrimEqPred :: Kind -> Kind -> Type -> Type -> Type
1684 mkHeteroReprPrimEqPred k1 k2 ty1 ty2
1685 = TyConApp eqReprPrimTyCon [k1, k2, ty1, ty2]
1686
1687 -- | Try to split up a coercion type into the types that it coerces
1688 splitCoercionType_maybe :: Type -> Maybe (Type, Type)
1689 splitCoercionType_maybe ty
1690 = do { (tc, [_, _, ty1, ty2]) <- splitTyConApp_maybe ty
1691 ; guard $ tc `hasKey` eqPrimTyConKey || tc `hasKey` eqReprPrimTyConKey
1692 ; return (ty1, ty2) }
1693
1694 mkReprPrimEqPred :: Type -> Type -> Type
1695 mkReprPrimEqPred ty1 ty2
1696 = TyConApp eqReprPrimTyCon [k1, k2, ty1, ty2]
1697 where
1698 k1 = typeKind ty1
1699 k2 = typeKind ty2
1700
1701 equalityTyCon :: Role -> TyCon
1702 equalityTyCon Nominal = eqPrimTyCon
1703 equalityTyCon Representational = eqReprPrimTyCon
1704 equalityTyCon Phantom = eqPhantPrimTyCon
1705
1706 -- --------------------- Dictionary types ---------------------------------
1707
1708 mkClassPred :: Class -> [Type] -> PredType
1709 mkClassPred clas tys = TyConApp (classTyCon clas) tys
1710
1711 isDictTy :: Type -> Bool
1712 isDictTy = isClassPred
1713
1714 isDictLikeTy :: Type -> Bool
1715 -- Note [Dictionary-like types]
1716 isDictLikeTy ty | Just ty' <- coreView ty = isDictLikeTy ty'
1717 isDictLikeTy ty = case splitTyConApp_maybe ty of
1718 Just (tc, tys) | isClassTyCon tc -> True
1719 | isTupleTyCon tc -> all isDictLikeTy tys
1720 _other -> False
1721
1722 {-
1723 Note [Dictionary-like types]
1724 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1725 Being "dictionary-like" means either a dictionary type or a tuple thereof.
1726 In GHC 6.10 we build implication constraints which construct such tuples,
1727 and if we land up with a binding
1728 t :: (C [a], Eq [a])
1729 t = blah
1730 then we want to treat t as cheap under "-fdicts-cheap" for example.
1731 (Implication constraints are normally inlined, but sadly not if the
1732 occurrence is itself inside an INLINE function! Until we revise the
1733 handling of implication constraints, that is.) This turned out to
1734 be important in getting good arities in DPH code. Example:
1735
1736 class C a
1737 class D a where { foo :: a -> a }
1738 instance C a => D (Maybe a) where { foo x = x }
1739
1740 bar :: (C a, C b) => a -> b -> (Maybe a, Maybe b)
1741 {-# INLINE bar #-}
1742 bar x y = (foo (Just x), foo (Just y))
1743
1744 Then 'bar' should jolly well have arity 4 (two dicts, two args), but
1745 we ended up with something like
1746 bar = __inline_me__ (\d1,d2. let t :: (D (Maybe a), D (Maybe b)) = ...
1747 in \x,y. <blah>)
1748
1749 This is all a bit ad-hoc; eg it relies on knowing that implication
1750 constraints build tuples.
1751
1752
1753 Decomposing PredType
1754 -}
1755
1756 -- | A choice of equality relation. This is separate from the type 'Role'
1757 -- because 'Phantom' does not define a (non-trivial) equality relation.
1758 data EqRel = NomEq | ReprEq
1759 deriving (Eq, Ord)
1760
1761 instance Outputable EqRel where
1762 ppr NomEq = text "nominal equality"
1763 ppr ReprEq = text "representational equality"
1764
1765 eqRelRole :: EqRel -> Role
1766 eqRelRole NomEq = Nominal
1767 eqRelRole ReprEq = Representational
1768
1769 data PredTree = ClassPred Class [Type]
1770 | EqPred EqRel Type Type
1771 | IrredPred PredType
1772
1773 classifyPredType :: PredType -> PredTree
1774 classifyPredType ev_ty = case splitTyConApp_maybe ev_ty of
1775 Just (tc, [_, _, ty1, ty2])
1776 | tc `hasKey` eqReprPrimTyConKey -> EqPred ReprEq ty1 ty2
1777 | tc `hasKey` eqPrimTyConKey -> EqPred NomEq ty1 ty2
1778 Just (tc, tys)
1779 | Just clas <- tyConClass_maybe tc -> ClassPred clas tys
1780 _ -> IrredPred ev_ty
1781
1782 getClassPredTys :: PredType -> (Class, [Type])
1783 getClassPredTys ty = case getClassPredTys_maybe ty of
1784 Just (clas, tys) -> (clas, tys)
1785 Nothing -> pprPanic "getClassPredTys" (ppr ty)
1786
1787 getClassPredTys_maybe :: PredType -> Maybe (Class, [Type])
1788 getClassPredTys_maybe ty = case splitTyConApp_maybe ty of
1789 Just (tc, tys) | Just clas <- tyConClass_maybe tc -> Just (clas, tys)
1790 _ -> Nothing
1791
1792 getEqPredTys :: PredType -> (Type, Type)
1793 getEqPredTys ty
1794 = case splitTyConApp_maybe ty of
1795 Just (tc, [_, _, ty1, ty2])
1796 | tc `hasKey` eqPrimTyConKey
1797 || tc `hasKey` eqReprPrimTyConKey
1798 -> (ty1, ty2)
1799 _ -> pprPanic "getEqPredTys" (ppr ty)
1800
1801 getEqPredTys_maybe :: PredType -> Maybe (Role, Type, Type)
1802 getEqPredTys_maybe ty
1803 = case splitTyConApp_maybe ty of
1804 Just (tc, [_, _, ty1, ty2])
1805 | tc `hasKey` eqPrimTyConKey -> Just (Nominal, ty1, ty2)
1806 | tc `hasKey` eqReprPrimTyConKey -> Just (Representational, ty1, ty2)
1807 _ -> Nothing
1808
1809 getEqPredRole :: PredType -> Role
1810 getEqPredRole ty = eqRelRole (predTypeEqRel ty)
1811
1812 -- | Get the equality relation relevant for a pred type.
1813 predTypeEqRel :: PredType -> EqRel
1814 predTypeEqRel ty
1815 | Just (tc, _) <- splitTyConApp_maybe ty
1816 , tc `hasKey` eqReprPrimTyConKey
1817 = ReprEq
1818 | otherwise
1819 = NomEq
1820
1821 {-
1822 %************************************************************************
1823 %* *
1824 Size
1825 * *
1826 ************************************************************************
1827 -}
1828
1829 -- NB: This function does not respect `eqType`, in that two types that
1830 -- are `eqType` may return different sizes. This is OK, because this
1831 -- function is used only in reporting, not decision-making.
1832 typeSize :: Type -> Int
1833 typeSize (LitTy {}) = 1
1834 typeSize (TyVarTy {}) = 1
1835 typeSize (AppTy t1 t2) = typeSize t1 + typeSize t2
1836 typeSize (ForAllTy b t) = typeSize (binderType b) + typeSize t
1837 typeSize (TyConApp _ ts) = 1 + sum (map typeSize ts)
1838 typeSize (CastTy ty co) = typeSize ty + coercionSize co
1839 typeSize (CoercionTy co) = coercionSize co
1840
1841 {-
1842 %************************************************************************
1843 %* *
1844 Well-scoped tyvars
1845 * *
1846 ************************************************************************
1847 -}
1848
1849 -- | Do a topological sort on a list of tyvars,
1850 -- so that binders occur before occurrences
1851 -- E.g. given [ a::k, k::*, b::k ]
1852 -- it'll return a well-scoped list [ k::*, a::k, b::k ]
1853 --
1854 -- This is a deterministic sorting operation
1855 -- (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 they are used visibly or invisibly. Invisible ones come
2300 -- first.
2301 splitVisVarsOfType :: Type -> Pair TyCoVarSet
2302 splitVisVarsOfType orig_ty = Pair invis_vars vis_vars
2303 where
2304 Pair invis_vars1 vis_vars = go orig_ty
2305 invis_vars = invis_vars1 `minusVarSet` vis_vars
2306
2307 go (TyVarTy tv) = Pair (tyCoVarsOfType $ tyVarKind tv) (unitVarSet tv)
2308 go (AppTy t1 t2) = go t1 `mappend` go t2
2309 go (TyConApp tc tys) = go_tc tc tys
2310 go (ForAllTy (Anon t1) t2) = go t1 `mappend` go t2
2311 go (ForAllTy (Named tv _) ty)
2312 = ((`delVarSet` tv) <$> go ty) `mappend`
2313 (invisible (tyCoVarsOfType $ tyVarKind tv))
2314 go (LitTy {}) = mempty
2315 go (CastTy ty co) = go ty `mappend` invisible (tyCoVarsOfCo co)
2316 go (CoercionTy co) = invisible $ tyCoVarsOfCo co
2317
2318 invisible vs = Pair vs emptyVarSet
2319
2320 go_tc tc tys = let (invis, vis) = partitionInvisibles tc id tys in
2321 invisible (tyCoVarsOfTypes invis) `mappend` foldMap go vis
2322
2323 splitVisVarsOfTypes :: [Type] -> Pair TyCoVarSet
2324 splitVisVarsOfTypes = foldMap splitVisVarsOfType