Improve panicking output
[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 {-
917 ---------------------------------------------------------------------
918 TyConApp
919 ~~~~~~~~
920 -}
921
922 -- | A key function: builds a 'TyConApp' or 'FunTy' as appropriate to
923 -- its arguments. Applies its arguments to the constructor from left to right.
924 mkTyConApp :: TyCon -> [Type] -> Type
925 mkTyConApp tycon tys
926 | isFunTyCon tycon, [ty1,ty2] <- tys
927 = ForAllTy (Anon ty1) ty2
928
929 | otherwise
930 = TyConApp tycon tys
931
932 -- splitTyConApp "looks through" synonyms, because they don't
933 -- mean a distinct type, but all other type-constructor applications
934 -- including functions are returned as Just ..
935
936 -- | Retrieve the tycon heading this type, if there is one. Does /not/
937 -- look through synonyms.
938 tyConAppTyConPicky_maybe :: Type -> Maybe TyCon
939 tyConAppTyConPicky_maybe (TyConApp tc _) = Just tc
940 tyConAppTyConPicky_maybe (ForAllTy (Anon _) _) = Just funTyCon
941 tyConAppTyConPicky_maybe _ = Nothing
942
943
944 -- | The same as @fst . splitTyConApp@
945 tyConAppTyCon_maybe :: Type -> Maybe TyCon
946 tyConAppTyCon_maybe ty | Just ty' <- coreView ty = tyConAppTyCon_maybe ty'
947 tyConAppTyCon_maybe (TyConApp tc _) = Just tc
948 tyConAppTyCon_maybe (ForAllTy (Anon _) _) = Just funTyCon
949 tyConAppTyCon_maybe _ = Nothing
950
951 tyConAppTyCon :: Type -> TyCon
952 tyConAppTyCon ty = tyConAppTyCon_maybe ty `orElse` pprPanic "tyConAppTyCon" (ppr ty)
953
954 -- | The same as @snd . splitTyConApp@
955 tyConAppArgs_maybe :: Type -> Maybe [Type]
956 tyConAppArgs_maybe ty | Just ty' <- coreView ty = tyConAppArgs_maybe ty'
957 tyConAppArgs_maybe (TyConApp _ tys) = Just tys
958 tyConAppArgs_maybe (ForAllTy (Anon arg) res) = Just [arg,res]
959 tyConAppArgs_maybe _ = Nothing
960
961 tyConAppArgs :: Type -> [Type]
962 tyConAppArgs ty = tyConAppArgs_maybe ty `orElse` pprPanic "tyConAppArgs" (ppr ty)
963
964 tyConAppArgN :: Int -> Type -> Type
965 -- Executing Nth
966 tyConAppArgN n ty
967 = case tyConAppArgs_maybe ty of
968 Just tys -> ASSERT2( n < length tys, ppr n <+> ppr tys ) tys `getNth` n
969 Nothing -> pprPanic "tyConAppArgN" (ppr n <+> ppr ty)
970
971 -- | Attempts to tease a type apart into a type constructor and the application
972 -- of a number of arguments to that constructor. Panics if that is not possible.
973 -- See also 'splitTyConApp_maybe'
974 splitTyConApp :: Type -> (TyCon, [Type])
975 splitTyConApp ty = case splitTyConApp_maybe ty of
976 Just stuff -> stuff
977 Nothing -> pprPanic "splitTyConApp" (ppr ty)
978
979 -- | Attempts to tease a type apart into a type constructor and the application
980 -- of a number of arguments to that constructor
981 splitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
982 splitTyConApp_maybe ty | Just ty' <- coreView ty = splitTyConApp_maybe ty'
983 splitTyConApp_maybe ty = repSplitTyConApp_maybe ty
984
985 -- | Like 'splitTyConApp_maybe', but doesn't look through synonyms. This
986 -- assumes the synonyms have already been dealt with.
987 repSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
988 repSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
989 repSplitTyConApp_maybe (ForAllTy (Anon arg) res) = Just (funTyCon, [arg,res])
990 repSplitTyConApp_maybe _ = Nothing
991
992 -- | Attempts to tease a list type apart and gives the type of the elements if
993 -- successful (looks through type synonyms)
994 splitListTyConApp_maybe :: Type -> Maybe Type
995 splitListTyConApp_maybe ty = case splitTyConApp_maybe ty of
996 Just (tc,[e]) | tc == listTyCon -> Just e
997 _other -> Nothing
998
999 -- | What is the role assigned to the next parameter of this type? Usually,
1000 -- this will be 'Nominal', but if the type is a 'TyConApp', we may be able to
1001 -- do better. The type does *not* have to be well-kinded when applied for this
1002 -- to work!
1003 nextRole :: Type -> Role
1004 nextRole ty
1005 | Just (tc, tys) <- splitTyConApp_maybe ty
1006 , let num_tys = length tys
1007 , num_tys < tyConArity tc
1008 = tyConRoles tc `getNth` num_tys
1009
1010 | otherwise
1011 = Nominal
1012
1013 newTyConInstRhs :: TyCon -> [Type] -> Type
1014 -- ^ Unwrap one 'layer' of newtype on a type constructor and its
1015 -- arguments, using an eta-reduced version of the @newtype@ if possible.
1016 -- This requires tys to have at least @newTyConInstArity tycon@ elements.
1017 newTyConInstRhs tycon tys
1018 = ASSERT2( tvs `leLength` tys, ppr tycon $$ ppr tys $$ ppr tvs )
1019 applyTysX tvs rhs tys
1020 where
1021 (tvs, rhs) = newTyConEtadRhs tycon
1022
1023 {-
1024 ---------------------------------------------------------------------
1025 CastTy
1026 ~~~~~~
1027 A casted type has its *kind* casted into something new.
1028
1029 Note [Weird typing rule for ForAllTy]
1030 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1031
1032 Here is the (truncated) typing rule for the dependent ForAllTy:
1033
1034 inner : kind
1035 ------------------------------------
1036 ForAllTy (Named tv vis) inner : kind
1037
1038 Note that neither the inner type nor for ForAllTy itself have to have
1039 kind *! But, it means that we should push any kind casts through the
1040 ForAllTy. The only trouble is avoiding capture.
1041
1042 -}
1043
1044 splitCastTy_maybe :: Type -> Maybe (Type, Coercion)
1045 splitCastTy_maybe ty | Just ty' <- coreView ty = splitCastTy_maybe ty'
1046 splitCastTy_maybe (CastTy ty co) = Just (ty, co)
1047 splitCastTy_maybe _ = Nothing
1048
1049 -- | Make a 'CastTy'. The Coercion must be nominal. This function looks
1050 -- at the entire structure of the type and coercion in an attempt to
1051 -- maintain representation invariance (that is, any two types that are `eqType`
1052 -- look the same). Be very wary of calling this in a loop.
1053 mkCastTy :: Type -> Coercion -> Type
1054 -- Running example:
1055 -- T :: forall k1. k1 -> forall k2. k2 -> Bool -> Maybe k1 -> *
1056 -- co :: * ~R X (maybe X is a newtype around *)
1057 -- ty = T Nat 3 Symbol "foo" True (Just 2)
1058 --
1059 -- We wish to "push" the cast down as far as possible. See also
1060 -- Note [Pushing down casts] in TyCoRep. Here is where we end
1061 -- up:
1062 --
1063 -- (T Nat 3 Symbol |> <Symbol> -> <Bool> -> <Maybe Nat> -> co)
1064 -- "foo" True (Just 2)
1065 --
1066 mkCastTy ty co | isReflexiveCo co = ty
1067 -- NB: Do the slow check here. This is important to keep the splitXXX
1068 -- functions working properly. Otherwise, we may end up with something
1069 -- like (((->) |> something_reflexive_but_not_obviously_so) biz baz)
1070 -- fails under splitFunTy_maybe. This happened with the cheaper check
1071 -- in test dependent/should_compile/dynamic-paper.
1072
1073 mkCastTy (CastTy ty co1) co2 = mkCastTy ty (co1 `mkTransCo` co2)
1074 -- See Note [Weird typing rule for ForAllTy]
1075 mkCastTy (ForAllTy (Named tv vis) inner_ty) co
1076 = -- have to make sure that pushing the co in doesn't capture the bound var
1077 let fvs = tyCoVarsOfCo co
1078 empty_subst = mkEmptyTCvSubst (mkInScopeSet fvs)
1079 (subst, tv') = substTyVarBndr empty_subst tv
1080 in
1081 ForAllTy (Named tv' vis) (substTy subst inner_ty `mkCastTy` co)
1082 mkCastTy ty co = -- NB: don't check if the coercion "from" type matches here;
1083 -- there may be unzonked variables about
1084 let result = split_apps [] ty co in
1085 ASSERT2( CastTy ty co `eqType` result
1086 , ppr ty <+> dcolon <+> ppr (typeKind ty) $$
1087 ppr co <+> dcolon <+> ppr (coercionKind co) $$
1088 ppr result <+> dcolon <+> ppr (typeKind result) )
1089 result
1090 where
1091 -- split_apps breaks apart any type applications, so we can see how far down
1092 -- to push the cast
1093 split_apps args (AppTy t1 t2) co
1094 = split_apps (t2:args) t1 co
1095 split_apps args (TyConApp tc tc_args) co
1096 | mightBeUnsaturatedTyCon tc
1097 = affix_co (tyConBinders tc) (mkTyConTy tc) (tc_args `chkAppend` args) co
1098 | otherwise -- not decomposable... but it may still be oversaturated
1099 = let (non_decomp_args, decomp_args) = splitAt (tyConArity tc) tc_args
1100 saturated_tc = mkTyConApp tc non_decomp_args
1101 in
1102 affix_co (fst $ splitPiTys $ typeKind saturated_tc)
1103 saturated_tc (decomp_args `chkAppend` args) co
1104
1105 split_apps args (ForAllTy (Anon arg) res) co
1106 = affix_co (tyConBinders funTyCon) (mkTyConTy funTyCon)
1107 (arg : res : args) co
1108 split_apps args ty co
1109 = affix_co (fst $ splitPiTys $ typeKind ty)
1110 ty args co
1111
1112 -- having broken everything apart, this figures out the point at which there
1113 -- are no more dependent quantifications, and puts the cast there
1114 affix_co _ ty [] co = no_double_casts ty co
1115 affix_co bndrs ty args co
1116 -- if kind contains any dependent quantifications, we can't push.
1117 -- apply arguments until it doesn't
1118 = let (no_dep_bndrs, some_dep_bndrs) = spanEnd isAnonBinder bndrs
1119 (some_dep_args, rest_args) = splitAtList some_dep_bndrs args
1120 dep_subst = zipTyBinderSubst some_dep_bndrs some_dep_args
1121 used_no_dep_bndrs = takeList rest_args no_dep_bndrs
1122 rest_arg_tys = substTys dep_subst (map binderType used_no_dep_bndrs)
1123 co' = mkFunCos Nominal
1124 (map (mkReflCo Nominal) rest_arg_tys)
1125 co
1126 in
1127 ((ty `mkAppTys` some_dep_args) `no_double_casts` co') `mkAppTys` rest_args
1128
1129 no_double_casts (CastTy ty co1) co2 = CastTy ty (co1 `mkTransCo` co2)
1130 no_double_casts ty co = CastTy ty co
1131
1132 {-
1133 --------------------------------------------------------------------
1134 CoercionTy
1135 ~~~~~~~~~~
1136 CoercionTy allows us to inject coercions into types. A CoercionTy
1137 should appear only in the right-hand side of an application.
1138 -}
1139
1140 mkCoercionTy :: Coercion -> Type
1141 mkCoercionTy = CoercionTy
1142
1143 isCoercionTy :: Type -> Bool
1144 isCoercionTy (CoercionTy _) = True
1145 isCoercionTy _ = False
1146
1147 isCoercionTy_maybe :: Type -> Maybe Coercion
1148 isCoercionTy_maybe (CoercionTy co) = Just co
1149 isCoercionTy_maybe _ = Nothing
1150
1151 stripCoercionTy :: Type -> Coercion
1152 stripCoercionTy (CoercionTy co) = co
1153 stripCoercionTy ty = pprPanic "stripCoercionTy" (ppr ty)
1154
1155 {-
1156 ---------------------------------------------------------------------
1157 SynTy
1158 ~~~~~
1159
1160 Notes on type synonyms
1161 ~~~~~~~~~~~~~~~~~~~~~~
1162 The various "split" functions (splitFunTy, splitRhoTy, splitForAllTy) try
1163 to return type synonyms wherever possible. Thus
1164
1165 type Foo a = a -> a
1166
1167 we want
1168 splitFunTys (a -> Foo a) = ([a], Foo a)
1169 not ([a], a -> a)
1170
1171 The reason is that we then get better (shorter) type signatures in
1172 interfaces. Notably this plays a role in tcTySigs in TcBinds.hs.
1173
1174
1175 Representation types
1176 ~~~~~~~~~~~~~~~~~~~~
1177
1178 Note [Nullary unboxed tuple]
1179 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1180 We represent the nullary unboxed tuple as the unary (but void) type
1181 Void#. The reason for this is that the ReprArity is never
1182 less than the Arity (as it would otherwise be for a function type like
1183 (# #) -> Int).
1184
1185 As a result, ReprArity is always strictly positive if Arity is. This
1186 is important because it allows us to distinguish at runtime between a
1187 thunk and a function takes a nullary unboxed tuple as an argument!
1188 -}
1189
1190 type UnaryType = Type
1191
1192 data RepType = UbxTupleRep [UnaryType] -- INVARIANT: never an empty list (see Note [Nullary unboxed tuple])
1193 | UnaryRep UnaryType
1194
1195 instance Outputable RepType where
1196 ppr (UbxTupleRep tys) = text "UbxTupleRep" <+> ppr tys
1197 ppr (UnaryRep ty) = text "UnaryRep" <+> ppr ty
1198
1199 flattenRepType :: RepType -> [UnaryType]
1200 flattenRepType (UbxTupleRep tys) = tys
1201 flattenRepType (UnaryRep ty) = [ty]
1202
1203 -- | Looks through:
1204 --
1205 -- 1. For-alls
1206 -- 2. Synonyms
1207 -- 3. Predicates
1208 -- 4. All newtypes, including recursive ones, but not newtype families
1209 -- 5. Casts
1210 --
1211 -- It's useful in the back end of the compiler.
1212 repType :: Type -> RepType
1213 repType ty
1214 = go initRecTc ty
1215 where
1216 go :: RecTcChecker -> Type -> RepType
1217 go rec_nts ty -- Expand predicates and synonyms
1218 | Just ty' <- coreView ty
1219 = go rec_nts ty'
1220
1221 go rec_nts (ForAllTy (Named {}) ty2) -- Drop type foralls
1222 = go rec_nts ty2
1223
1224 go rec_nts (TyConApp tc tys) -- Expand newtypes
1225 | isNewTyCon tc
1226 , tys `lengthAtLeast` tyConArity tc
1227 , Just rec_nts' <- checkRecTc rec_nts tc -- See Note [Expanding newtypes] in TyCon
1228 = go rec_nts' (newTyConInstRhs tc tys)
1229
1230 | isUnboxedTupleTyCon tc
1231 = if null tys
1232 then UnaryRep voidPrimTy -- See Note [Nullary unboxed tuple]
1233 else UbxTupleRep (concatMap (flattenRepType . go rec_nts) non_rr_tys)
1234 where
1235 -- See Note [Unboxed tuple RuntimeRep vars] in TyCon
1236 non_rr_tys = dropRuntimeRepArgs tys
1237
1238 go rec_nts (CastTy ty _)
1239 = go rec_nts ty
1240
1241 go _ ty@(CoercionTy _)
1242 = pprPanic "repType" (ppr ty)
1243
1244 go _ ty = UnaryRep ty
1245
1246 -- ToDo: this could be moved to the code generator, using splitTyConApp instead
1247 -- of inspecting the type directly.
1248
1249 -- | Discovers the primitive representation of a more abstract 'UnaryType'
1250 typePrimRep :: UnaryType -> PrimRep
1251 typePrimRep ty = kindPrimRep (typeKind ty)
1252
1253 -- | Find the primitive representation of a 'TyCon'. Defined here to
1254 -- avoid module loops. Call this only on unlifted tycons.
1255 tyConPrimRep :: TyCon -> PrimRep
1256 tyConPrimRep tc = kindPrimRep res_kind
1257 where
1258 res_kind = tyConResKind tc
1259
1260 -- | Take a kind (of shape @TYPE rr@) and produce the 'PrimRep' of values
1261 -- of types of this kind.
1262 kindPrimRep :: Kind -> PrimRep
1263 kindPrimRep ki | Just ki' <- coreViewOneStarKind ki = kindPrimRep ki'
1264 kindPrimRep (TyConApp typ [runtime_rep])
1265 = ASSERT( typ `hasKey` tYPETyConKey )
1266 go runtime_rep
1267 where
1268 go rr | Just rr' <- coreView rr = go rr'
1269 go (TyConApp rr_dc args)
1270 | RuntimeRep fun <- tyConRuntimeRepInfo rr_dc
1271 = fun args
1272 go rr = pprPanic "kindPrimRep.go" (ppr rr)
1273 kindPrimRep ki = WARN( True
1274 , text "kindPrimRep defaulting to PtrRep on" <+> ppr ki )
1275 PtrRep -- this can happen legitimately for, e.g., Any
1276
1277 typeRepArity :: Arity -> Type -> RepArity
1278 typeRepArity 0 _ = 0
1279 typeRepArity n ty = case repType ty of
1280 UnaryRep (ForAllTy bndr ty) -> length (flattenRepType (repType (binderType bndr))) + typeRepArity (n - 1) ty
1281 _ -> pprPanic "typeRepArity: arity greater than type can handle" (ppr (n, ty, repType ty))
1282
1283 isVoidTy :: Type -> Bool
1284 -- True if the type has zero width
1285 isVoidTy ty = case repType ty of
1286 UnaryRep (TyConApp tc _) -> isUnliftedTyCon tc &&
1287 isVoidRep (tyConPrimRep tc)
1288 _ -> False
1289
1290 {-
1291 Note [AppTy rep]
1292 ~~~~~~~~~~~~~~~~
1293 Types of the form 'f a' must be of kind *, not #, so we are guaranteed
1294 that they are represented by pointers. The reason is that f must have
1295 kind (kk -> kk) and kk cannot be unlifted; see Note [The kind invariant]
1296 in TyCoRep.
1297
1298 ---------------------------------------------------------------------
1299 ForAllTy
1300 ~~~~~~~~
1301 -}
1302
1303 mkForAllTy :: TyBinder -> Type -> Type
1304 mkForAllTy = ForAllTy
1305
1306 -- | Make a dependent forall.
1307 mkNamedForAllTy :: TyVar -> VisibilityFlag -> Type -> Type
1308 mkNamedForAllTy tv vis = ASSERT( isTyVar tv )
1309 ForAllTy (Named tv vis)
1310
1311 -- | Like mkForAllTys, but assumes all variables are dependent and invisible,
1312 -- a common case
1313 mkInvForAllTys :: [TyVar] -> Type -> Type
1314 mkInvForAllTys tvs = ASSERT( all isTyVar tvs )
1315 mkForAllTys (map (flip Named Invisible) tvs)
1316
1317 -- | Like mkForAllTys, but assumes all variables are dependent and specified,
1318 -- a common case
1319 mkSpecForAllTys :: [TyVar] -> Type -> Type
1320 mkSpecForAllTys tvs = ASSERT( all isTyVar tvs )
1321 mkForAllTys (map (flip Named Specified) tvs)
1322
1323 -- | Like mkForAllTys, but assumes all variables are dependent and visible
1324 mkVisForAllTys :: [TyVar] -> Type -> Type
1325 mkVisForAllTys tvs = ASSERT( all isTyVar tvs )
1326 mkForAllTys (map (flip Named Visible) tvs)
1327
1328 mkPiType :: Var -> Type -> Type
1329 -- ^ Makes a @(->)@ type or an implicit forall type, depending
1330 -- on whether it is given a type variable or a term variable.
1331 -- This is used, for example, when producing the type of a lambda.
1332 -- Always uses Invisible binders.
1333 mkPiTypes :: [Var] -> Type -> Type
1334 -- ^ 'mkPiType' for multiple type or value arguments
1335
1336 mkPiType v ty
1337 | isTyVar v = mkForAllTy (Named v Invisible) ty
1338 | otherwise = mkForAllTy (Anon (varType v)) ty
1339
1340 mkPiTypes vs ty = foldr mkPiType ty vs
1341
1342 -- | Given a list of type-level vars and a result type, makes TyBinders, preferring
1343 -- anonymous binders if the variable is, in fact, not dependent.
1344 -- All binders are /visible/.
1345 mkTyBindersPreferAnon :: [TyVar] -> Type -> [TyBinder]
1346 mkTyBindersPreferAnon vars inner_ty = fst $ go vars inner_ty
1347 where
1348 go :: [TyVar] -> Type -> ([TyBinder], VarSet) -- also returns the free vars
1349 go [] ty = ([], tyCoVarsOfType ty)
1350 go (v:vs) ty | v `elemVarSet` fvs
1351 = ( Named v Visible : binders
1352 , fvs `delVarSet` v `unionVarSet` kind_vars )
1353 | otherwise
1354 = ( Anon (tyVarKind v) : binders
1355 , fvs `unionVarSet` kind_vars )
1356 where
1357 (binders, fvs) = go vs ty
1358 kind_vars = tyCoVarsOfType $ tyVarKind v
1359
1360 -- | Take a ForAllTy apart, returning the list of tyvars and the result type.
1361 -- This always succeeds, even if it returns only an empty list. Note that the
1362 -- result type returned may have free variables that were bound by a forall.
1363 splitForAllTys :: Type -> ([TyVar], Type)
1364 splitForAllTys ty = split ty ty []
1365 where
1366 split orig_ty ty tvs | Just ty' <- coreView ty = split orig_ty ty' tvs
1367 split _ (ForAllTy (Named tv _) ty) tvs = split ty ty (tv:tvs)
1368 split orig_ty _ tvs = (reverse tvs, orig_ty)
1369
1370 -- | Split off all TyBinders to a type, splitting both proper foralls
1371 -- and functions
1372 splitPiTys :: Type -> ([TyBinder], Type)
1373 splitPiTys ty = split ty ty []
1374 where
1375 split orig_ty ty bs | Just ty' <- coreView ty = split orig_ty ty' bs
1376 split _ (ForAllTy b res) bs = split res res (b:bs)
1377 split orig_ty _ bs = (reverse bs, orig_ty)
1378
1379 -- | Like 'splitPiTys' but split off only /named/ binders.
1380 splitNamedPiTys :: Type -> ([TyBinder], Type)
1381 splitNamedPiTys ty = split ty ty []
1382 where
1383 split orig_ty ty bs | Just ty' <- coreView ty = split orig_ty ty' bs
1384 split _ (ForAllTy b@(Named {}) res) bs = split res res (b:bs)
1385 split orig_ty _ bs = (reverse bs, orig_ty)
1386
1387 -- | Checks whether this is a proper forall (with a named binder)
1388 isForAllTy :: Type -> Bool
1389 isForAllTy (ForAllTy (Named {}) _) = True
1390 isForAllTy _ = False
1391
1392 -- | Is this a function or forall?
1393 isPiTy :: Type -> Bool
1394 isPiTy (ForAllTy {}) = True
1395 isPiTy _ = False
1396
1397 -- | Take a forall type apart, or panics if that is not possible.
1398 splitForAllTy :: Type -> (TyVar, Type)
1399 splitForAllTy ty
1400 | Just answer <- splitForAllTy_maybe ty = answer
1401 | otherwise = pprPanic "splitForAllTy" (ppr ty)
1402
1403 -- | Attempts to take a forall type apart, but only if it's a proper forall,
1404 -- with a named binder
1405 splitForAllTy_maybe :: Type -> Maybe (TyVar, Type)
1406 splitForAllTy_maybe ty = splitFAT_m ty
1407 where
1408 splitFAT_m ty | Just ty' <- coreView ty = splitFAT_m ty'
1409 splitFAT_m (ForAllTy (Named tv _) ty) = Just (tv, ty)
1410 splitFAT_m _ = Nothing
1411
1412 -- | Attempts to take a forall type apart; works with proper foralls and
1413 -- functions
1414 splitPiTy_maybe :: Type -> Maybe (TyBinder, Type)
1415 splitPiTy_maybe ty = go ty
1416 where
1417 go ty | Just ty' <- coreView ty = go ty'
1418 go (ForAllTy bndr ty) = Just (bndr, ty)
1419 go _ = Nothing
1420
1421 -- | Takes a forall type apart, or panics
1422 splitPiTy :: Type -> (TyBinder, Type)
1423 splitPiTy ty
1424 | Just answer <- splitPiTy_maybe ty = answer
1425 | otherwise = pprPanic "splitPiTy" (ppr ty)
1426
1427 -- | Drops all non-anonymous ForAllTys
1428 dropForAlls :: Type -> Type
1429 dropForAlls ty | Just ty' <- coreView ty = dropForAlls ty'
1430 | otherwise = go ty
1431 where
1432 go (ForAllTy (Named {}) res) = go res
1433 go res = res
1434
1435 -- | Given a tycon and its arguments, filters out any invisible arguments
1436 filterOutInvisibleTypes :: TyCon -> [Type] -> [Type]
1437 filterOutInvisibleTypes tc tys = snd $ partitionInvisibles tc id tys
1438
1439 -- | Like 'filterOutInvisibles', but works on 'TyVar's
1440 filterOutInvisibleTyVars :: TyCon -> [TyVar] -> [TyVar]
1441 filterOutInvisibleTyVars tc tvs = snd $ partitionInvisibles tc mkTyVarTy tvs
1442
1443 -- | Given a tycon and a list of things (which correspond to arguments),
1444 -- partitions the things into the invisible ones and the visible ones.
1445 -- The callback function is necessary for this scenario:
1446 --
1447 -- > T :: forall k. k -> k
1448 -- > partitionInvisibles T [forall m. m -> m -> m, S, R, Q]
1449 --
1450 -- After substituting, we get
1451 --
1452 -- > T (forall m. m -> m -> m) :: (forall m. m -> m -> m) -> forall n. n -> n -> n
1453 --
1454 -- Thus, the first argument is invisible, @S@ is visible, @R@ is invisible again,
1455 -- and @Q@ is visible.
1456 --
1457 -- If you're absolutely sure that your tycon's kind doesn't end in a variable,
1458 -- it's OK if the callback function panics, as that's the only time it's
1459 -- consulted.
1460 partitionInvisibles :: TyCon -> (a -> Type) -> [a] -> ([a], [a])
1461 partitionInvisibles tc get_ty = go emptyTCvSubst (tyConKind tc)
1462 where
1463 go _ _ [] = ([], [])
1464 go subst (ForAllTy bndr res_ki) (x:xs)
1465 | isVisibleBinder bndr = second (x :) (go subst' res_ki xs)
1466 | otherwise = first (x :) (go subst' res_ki xs)
1467 where
1468 subst' = extendTvSubstBinder subst bndr (get_ty x)
1469 go subst (TyVarTy tv) xs
1470 | Just ki <- lookupTyVar subst tv = go subst ki xs
1471 go _ _ xs = ([], xs) -- something is ill-kinded. But this can happen
1472 -- when printing errors. Assume everything is visible.
1473
1474 -- like splitPiTys, but returns only *invisible* binders, including constraints
1475 splitPiTysInvisible :: Type -> ([TyBinder], Type)
1476 splitPiTysInvisible ty = split ty ty []
1477 where
1478 split orig_ty ty bndrs
1479 | Just ty' <- coreView ty = split orig_ty ty' bndrs
1480 split _ (ForAllTy bndr ty) bndrs
1481 | isInvisibleBinder bndr
1482 = split ty ty (bndr:bndrs)
1483
1484 split orig_ty _ bndrs
1485 = (reverse bndrs, orig_ty)
1486
1487 applyTysX :: [TyVar] -> Type -> [Type] -> Type
1488 -- applyTyxX beta-reduces (/\tvs. body_ty) arg_tys
1489 -- Assumes that (/\tvs. body_ty) is closed
1490 applyTysX tvs body_ty arg_tys
1491 = ASSERT2( length arg_tys >= n_tvs, pp_stuff )
1492 ASSERT2( tyCoVarsOfType body_ty `subVarSet` mkVarSet tvs, pp_stuff )
1493 mkAppTys (substTyWith tvs (take n_tvs arg_tys) body_ty)
1494 (drop n_tvs arg_tys)
1495 where
1496 pp_stuff = vcat [ppr tvs, ppr body_ty, ppr arg_tys]
1497 n_tvs = length tvs
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