8ce60a50bb835de59478696b23ebff7894d803eb
[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, funResultTy, funArgTy,
29
30 mkTyConApp, mkTyConTy,
31 tyConAppTyCon_maybe, tyConAppTyConPicky_maybe,
32 tyConAppArgs_maybe, tyConAppTyCon, tyConAppArgs,
33 splitTyConApp_maybe, splitTyConApp, tyConAppArgN, nextRole,
34 splitListTyConApp_maybe,
35 repSplitTyConApp_maybe,
36
37 mkForAllTy, mkForAllTys, mkInvForAllTys, mkSpecForAllTys,
38 mkVisForAllTys,
39 mkNamedForAllTy,
40 splitForAllTy_maybe, splitForAllTys, splitForAllTy,
41 splitPiTy_maybe, splitPiTys, splitPiTy,
42 splitNamedPiTys,
43 mkPiType, mkPiTypes, mkTyBindersPreferAnon,
44 piResultTy, piResultTys,
45 applyTysX, dropForAlls,
46
47 mkNumLitTy, isNumLitTy,
48 mkStrLitTy, isStrLitTy,
49
50 mkCastTy, mkCoercionTy, splitCastTy_maybe,
51
52 userTypeError_maybe, pprUserTypeErrorTy,
53
54 coAxNthLHS,
55 stripCoercionTy, splitCoercionType_maybe,
56
57 splitPiTysInvisible, filterOutInvisibleTypes,
58 filterOutInvisibleTyVars, partitionInvisibles,
59 synTyConResKind,
60
61 -- Analyzing types
62 TyCoMapper(..), mapType, mapCoercion,
63
64 -- (Newtypes)
65 newTyConInstRhs,
66
67 -- Pred types
68 mkFamilyTyConApp,
69 isDictLikeTy,
70 mkPrimEqPred, mkReprPrimEqPred, mkPrimEqPredRole,
71 equalityTyCon,
72 mkHeteroPrimEqPred, mkHeteroReprPrimEqPred,
73 mkClassPred,
74 isClassPred, isEqPred, isNomEqPred,
75 isIPPred, isIPPred_maybe, isIPTyCon, isIPClass,
76 isCTupleClass,
77
78 -- Deconstructing predicate types
79 PredTree(..), EqRel(..), eqRelRole, classifyPredType,
80 getClassPredTys, getClassPredTys_maybe,
81 getEqPredTys, getEqPredTys_maybe, getEqPredRole,
82 predTypeEqRel,
83
84 -- ** Binders
85 sameVis,
86 mkNamedBinder, mkNamedBinders,
87 mkAnonBinder, isNamedBinder, isAnonBinder,
88 isIdLikeBinder, binderVisibility, binderVar_maybe,
89 binderVar, binderRelevantType_maybe, caseBinder,
90 partitionBinders, partitionBindersIntoBinders,
91 binderType, isVisibleBinder, isInvisibleBinder,
92
93 -- ** Common type constructors
94 funTyCon,
95
96 -- ** Predicates on types
97 isTyVarTy, isFunTy, isDictTy, isPredTy, isVoidTy, isCoercionTy,
98 isCoercionTy_maybe, isCoercionType, isForAllTy,
99 isPiTy,
100
101 -- (Lifting and boxity)
102 isUnliftedType, isUnboxedTupleType, isAlgType, isClosedAlgType,
103 isPrimitiveType, isStrictType,
104 isRuntimeRepTy, isRuntimeRepVar, isRuntimeRepKindedTy,
105 dropRuntimeRepArgs,
106 getRuntimeRep, getRuntimeRepFromKind,
107
108 -- * Main data types representing Kinds
109 Kind,
110
111 -- ** Finding the kind of a type
112 typeKind,
113
114 -- ** Common Kind
115 liftedTypeKind,
116
117 -- * Type free variables
118 tyCoVarsOfType, tyCoVarsOfTypes, tyCoFVsOfType,
119 tyCoVarsOfTypeDSet,
120 coVarsOfType,
121 coVarsOfTypes, closeOverKinds, closeOverKindsList,
122 splitVisVarsOfType, splitVisVarsOfTypes,
123 expandTypeSynonyms,
124 typeSize,
125
126 -- * Well-scoped lists of variables
127 dVarSetElemsWellScoped, toposortTyVars, tyCoVarsOfTypeWellScoped,
128 tyCoVarsOfTypesWellScoped,
129
130 -- * Type comparison
131 eqType, eqTypeX, eqTypes, nonDetCmpType, nonDetCmpTypes, nonDetCmpTypeX,
132 nonDetCmpTypesX, nonDetCmpTc,
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, 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, getTCvSubstRangeFVs,
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 import Unique ( nonDetCmpUnique )
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 {-
589 ---------------------------------------------------------------------
590 AppTy
591 ~~~~~
592 We need to be pretty careful with AppTy to make sure we obey the
593 invariant that a TyConApp is always visibly so. mkAppTy maintains the
594 invariant: use it.
595
596 Note [Decomposing fat arrow c=>t]
597 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
598 Can we unify (a b) with (Eq a => ty)? If we do so, we end up with
599 a partial application like ((=>) Eq a) which doesn't make sense in
600 source Haskell. In constrast, we *can* unify (a b) with (t1 -> t2).
601 Here's an example (Trac #9858) of how you might do it:
602 i :: (Typeable a, Typeable b) => Proxy (a b) -> TypeRep
603 i p = typeRep p
604
605 j = i (Proxy :: Proxy (Eq Int => Int))
606 The type (Proxy (Eq Int => Int)) is only accepted with -XImpredicativeTypes,
607 but suppose we want that. But then in the call to 'i', we end
608 up decomposing (Eq Int => Int), and we definitely don't want that.
609
610 This really only applies to the type checker; in Core, '=>' and '->'
611 are the same, as are 'Constraint' and '*'. But for now I've put
612 the test in repSplitAppTy_maybe, which applies throughout, because
613 the other calls to splitAppTy are in Unify, which is also used by
614 the type checker (e.g. when matching type-function equations).
615
616 -}
617
618 -- | Applies a type to another, as in e.g. @k a@
619 mkAppTy :: Type -> Type -> Type
620 mkAppTy (TyConApp tc tys) ty2 = mkTyConApp tc (tys ++ [ty2])
621 mkAppTy ty1 ty2 = AppTy ty1 ty2
622 -- Note that the TyConApp could be an
623 -- under-saturated type synonym. GHC allows that; e.g.
624 -- type Foo k = k a -> k a
625 -- type Id x = x
626 -- foo :: Foo Id -> Foo Id
627 --
628 -- Here Id is partially applied in the type sig for Foo,
629 -- but once the type synonyms are expanded all is well
630
631 mkAppTys :: Type -> [Type] -> Type
632 mkAppTys ty1 [] = ty1
633 mkAppTys (TyConApp tc tys1) tys2 = mkTyConApp tc (tys1 ++ tys2)
634 mkAppTys ty1 tys2 = foldl AppTy ty1 tys2
635
636 -------------
637 splitAppTy_maybe :: Type -> Maybe (Type, Type)
638 -- ^ Attempt to take a type application apart, whether it is a
639 -- function, type constructor, or plain type application. Note
640 -- that type family applications are NEVER unsaturated by this!
641 splitAppTy_maybe ty | Just ty' <- coreView ty
642 = splitAppTy_maybe ty'
643 splitAppTy_maybe ty = repSplitAppTy_maybe ty
644
645 -------------
646 repSplitAppTy_maybe :: Type -> Maybe (Type,Type)
647 -- ^ Does the AppTy split as in 'splitAppTy_maybe', but assumes that
648 -- any Core view stuff is already done
649 repSplitAppTy_maybe (ForAllTy (Anon ty1) ty2)
650 = Just (TyConApp funTyCon [ty1], ty2)
651 repSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2)
652 repSplitAppTy_maybe (TyConApp tc tys)
653 | mightBeUnsaturatedTyCon tc || tys `lengthExceeds` tyConArity tc
654 , Just (tys', ty') <- snocView tys
655 = Just (TyConApp tc tys', ty') -- Never create unsaturated type family apps!
656 repSplitAppTy_maybe _other = Nothing
657
658 -- this one doesn't braek apart (c => t).
659 -- See Note [Decomposing fat arrow c=>t]
660 -- Defined here to avoid module loops between Unify and TcType.
661 tcRepSplitAppTy_maybe :: Type -> Maybe (Type,Type)
662 -- ^ Does the AppTy split as in 'tcSplitAppTy_maybe', but assumes that
663 -- any coreView stuff is already done. Refuses to look through (c => t)
664 tcRepSplitAppTy_maybe (ForAllTy (Anon ty1) ty2)
665 | isConstraintKind (typeKind ty1) = Nothing -- See Note [Decomposing fat arrow c=>t]
666 | otherwise = Just (TyConApp funTyCon [ty1], ty2)
667 tcRepSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2)
668 tcRepSplitAppTy_maybe (TyConApp tc tys)
669 | mightBeUnsaturatedTyCon tc || tys `lengthExceeds` tyConArity tc
670 , Just (tys', ty') <- snocView tys
671 = Just (TyConApp tc tys', ty') -- Never create unsaturated type family apps!
672 tcRepSplitAppTy_maybe _other = Nothing
673 -------------
674 splitAppTy :: Type -> (Type, Type)
675 -- ^ Attempts to take a type application apart, as in 'splitAppTy_maybe',
676 -- and panics if this is not possible
677 splitAppTy ty = case splitAppTy_maybe ty of
678 Just pr -> pr
679 Nothing -> panic "splitAppTy"
680
681 -------------
682 splitAppTys :: Type -> (Type, [Type])
683 -- ^ Recursively splits a type as far as is possible, leaving a residual
684 -- type being applied to and the type arguments applied to it. Never fails,
685 -- even if that means returning an empty list of type applications.
686 splitAppTys ty = split ty ty []
687 where
688 split orig_ty ty args | Just ty' <- coreView ty = split orig_ty ty' args
689 split _ (AppTy ty arg) args = split ty ty (arg:args)
690 split _ (TyConApp tc tc_args) args
691 = let -- keep type families saturated
692 n | mightBeUnsaturatedTyCon tc = 0
693 | otherwise = tyConArity tc
694 (tc_args1, tc_args2) = splitAt n tc_args
695 in
696 (TyConApp tc tc_args1, tc_args2 ++ args)
697 split _ (ForAllTy (Anon ty1) ty2) args = ASSERT( null args )
698 (TyConApp funTyCon [], [ty1,ty2])
699 split orig_ty _ args = (orig_ty, args)
700
701 -- | Like 'splitAppTys', but doesn't look through type synonyms
702 repSplitAppTys :: Type -> (Type, [Type])
703 repSplitAppTys ty = split ty []
704 where
705 split (AppTy ty arg) args = split ty (arg:args)
706 split (TyConApp tc tc_args) args
707 = let n | mightBeUnsaturatedTyCon tc = 0
708 | otherwise = tyConArity tc
709 (tc_args1, tc_args2) = splitAt n tc_args
710 in
711 (TyConApp tc tc_args1, tc_args2 ++ args)
712 split (ForAllTy (Anon ty1) ty2) args = ASSERT( null args )
713 (TyConApp funTyCon [], [ty1, ty2])
714 split ty args = (ty, args)
715
716 {-
717 LitTy
718 ~~~~~
719 -}
720
721 mkNumLitTy :: Integer -> Type
722 mkNumLitTy n = LitTy (NumTyLit n)
723
724 -- | Is this a numeric literal. We also look through type synonyms.
725 isNumLitTy :: Type -> Maybe Integer
726 isNumLitTy ty | Just ty1 <- coreView ty = isNumLitTy ty1
727 isNumLitTy (LitTy (NumTyLit n)) = Just n
728 isNumLitTy _ = Nothing
729
730 mkStrLitTy :: FastString -> Type
731 mkStrLitTy s = LitTy (StrTyLit s)
732
733 -- | Is this a symbol literal. We also look through type synonyms.
734 isStrLitTy :: Type -> Maybe FastString
735 isStrLitTy ty | Just ty1 <- coreView ty = isStrLitTy ty1
736 isStrLitTy (LitTy (StrTyLit s)) = Just s
737 isStrLitTy _ = Nothing
738
739
740 -- | Is this type a custom user error?
741 -- If so, give us the kind and the error message.
742 userTypeError_maybe :: Type -> Maybe Type
743 userTypeError_maybe t
744 = do { (tc, _kind : msg : _) <- splitTyConApp_maybe t
745 -- There may be more than 2 arguments, if the type error is
746 -- used as a type constructor (e.g. at kind `Type -> Type`).
747
748 ; guard (tyConName tc == errorMessageTypeErrorFamName)
749 ; return msg }
750
751 -- | Render a type corresponding to a user type error into a SDoc.
752 pprUserTypeErrorTy :: Type -> SDoc
753 pprUserTypeErrorTy ty =
754 case splitTyConApp_maybe ty of
755
756 -- Text "Something"
757 Just (tc,[txt])
758 | tyConName tc == typeErrorTextDataConName
759 , Just str <- isStrLitTy txt -> ftext str
760
761 -- ShowType t
762 Just (tc,[_k,t])
763 | tyConName tc == typeErrorShowTypeDataConName -> ppr t
764
765 -- t1 :<>: t2
766 Just (tc,[t1,t2])
767 | tyConName tc == typeErrorAppendDataConName ->
768 pprUserTypeErrorTy t1 <> pprUserTypeErrorTy t2
769
770 -- t1 :$$: t2
771 Just (tc,[t1,t2])
772 | tyConName tc == typeErrorVAppendDataConName ->
773 pprUserTypeErrorTy t1 $$ pprUserTypeErrorTy t2
774
775 -- An uneavaluated type function
776 _ -> ppr ty
777
778
779
780
781 {-
782 ---------------------------------------------------------------------
783 FunTy
784 ~~~~~
785
786 Function types are represented with (ForAllTy (Anon ...) ...)
787 -}
788
789 isFunTy :: Type -> Bool
790 isFunTy ty = isJust (splitFunTy_maybe ty)
791
792 splitFunTy :: Type -> (Type, Type)
793 -- ^ Attempts to extract the argument and result types from a type, and
794 -- panics if that is not possible. See also 'splitFunTy_maybe'
795 splitFunTy ty | Just ty' <- coreView ty = splitFunTy ty'
796 splitFunTy (ForAllTy (Anon arg) res) = (arg, res)
797 splitFunTy other = pprPanic "splitFunTy" (ppr other)
798
799 splitFunTy_maybe :: Type -> Maybe (Type, Type)
800 -- ^ Attempts to extract the argument and result types from a type
801 splitFunTy_maybe ty | Just ty' <- coreView ty = splitFunTy_maybe ty'
802 splitFunTy_maybe (ForAllTy (Anon arg) res) = Just (arg, res)
803 splitFunTy_maybe _ = Nothing
804
805 splitFunTys :: Type -> ([Type], Type)
806 splitFunTys ty = split [] ty ty
807 where
808 split args orig_ty ty | Just ty' <- coreView ty = split args orig_ty ty'
809 split args _ (ForAllTy (Anon arg) res) = split (arg:args) res res
810 split args orig_ty _ = (reverse args, orig_ty)
811
812 funResultTy :: Type -> Type
813 -- ^ Extract the function result type and panic if that is not possible
814 funResultTy ty | Just ty' <- coreView ty = funResultTy ty'
815 funResultTy (ForAllTy (Anon {}) res) = res
816 funResultTy ty = pprPanic "funResultTy" (ppr ty)
817
818 funArgTy :: Type -> Type
819 -- ^ Extract the function argument type and panic if that is not possible
820 funArgTy ty | Just ty' <- coreView ty = funArgTy ty'
821 funArgTy (ForAllTy (Anon arg) _res) = arg
822 funArgTy ty = pprPanic "funArgTy" (ppr ty)
823
824 piResultTy :: Type -> Type -> Type
825 piResultTy ty arg = case piResultTy_maybe ty arg of
826 Just res -> res
827 Nothing -> pprPanic "piResultTy" (ppr ty $$ ppr arg)
828
829 piResultTy_maybe :: Type -> Type -> Maybe Type
830
831 -- ^ Just like 'piResultTys' but for a single argument
832 -- Try not to iterate 'piResultTy', because it's inefficient to substitute
833 -- one variable at a time; instead use 'piResultTys"
834 piResultTy_maybe ty arg
835 | Just ty' <- coreView ty = piResultTy_maybe ty' arg
836
837 | ForAllTy bndr res <- ty
838 = case bndr of
839 Anon {} -> Just res
840 Named tv _ -> Just (substTy (extendTvSubst empty_subst tv arg) res)
841 where
842 empty_subst = mkEmptyTCvSubst $ mkInScopeSet $
843 tyCoVarsOfTypes [arg,res]
844 | otherwise
845 = Nothing
846
847 -- | (piResultTys f_ty [ty1, .., tyn]) gives the type of (f ty1 .. tyn)
848 -- where f :: f_ty
849 -- 'piResultTys' is interesting because:
850 -- 1. 'f_ty' may have more for-alls than there are args
851 -- 2. Less obviously, it may have fewer for-alls
852 -- For case 2. think of:
853 -- piResultTys (forall a.a) [forall b.b, Int]
854 -- This really can happen, but only (I think) in situations involving
855 -- undefined. For example:
856 -- undefined :: forall a. a
857 -- Term: undefined @(forall b. b->b) @Int
858 -- This term should have type (Int -> Int), but notice that
859 -- there are more type args than foralls in 'undefined's type.
860
861 -- If you edit this function, you may need to update the GHC formalism
862 -- See Note [GHC Formalism] in coreSyn/CoreLint.hs
863
864 -- This is a heavily used function (e.g. from typeKind),
865 -- so we pay attention to efficiency, especially in the special case
866 -- where there are no for-alls so we are just dropping arrows from
867 -- a function type/kind.
868 piResultTys :: Type -> [Type] -> Type
869 piResultTys ty [] = ty
870 piResultTys ty orig_args@(arg:args)
871 | Just ty' <- coreView ty
872 = piResultTys ty' orig_args
873
874 | ForAllTy bndr res <- ty
875 = case bndr of
876 Anon {} -> piResultTys res args
877 Named tv _ -> go (extendVarEnv emptyTvSubstEnv tv arg) res args
878
879 | otherwise
880 = pprPanic "piResultTys1" (ppr ty $$ ppr orig_args)
881 where
882 go :: TvSubstEnv -> Type -> [Type] -> Type
883 go tv_env ty [] = substTy (mkTvSubst in_scope tv_env) ty
884 where
885 in_scope = mkInScopeSet (tyCoVarsOfTypes (ty:orig_args))
886
887 go tv_env ty all_args@(arg:args)
888 | Just ty' <- coreView ty
889 = go tv_env ty' all_args
890
891 | ForAllTy bndr res <- ty
892 = case bndr of
893 Anon _ -> go tv_env res args
894 Named tv _ -> go (extendVarEnv tv_env tv arg) res args
895
896 | TyVarTy tv <- ty
897 , Just ty' <- lookupVarEnv tv_env tv
898 -- Deals with piResultTys (forall a. a) [forall b.b, Int]
899 = piResultTys ty' all_args
900
901 | otherwise
902 = pprPanic "piResultTys2" (ppr ty $$ ppr orig_args $$ ppr all_args)
903
904 applyTysX :: [TyVar] -> Type -> [Type] -> Type
905 -- applyTyxX beta-reduces (/\tvs. body_ty) arg_tys
906 -- Assumes that (/\tvs. body_ty) is closed
907 applyTysX tvs body_ty arg_tys
908 = ASSERT2( length arg_tys >= n_tvs, pp_stuff )
909 ASSERT2( tyCoVarsOfType body_ty `subVarSet` mkVarSet tvs, pp_stuff )
910 mkAppTys (substTyWith tvs (take n_tvs arg_tys) body_ty)
911 (drop n_tvs arg_tys)
912 where
913 pp_stuff = vcat [ppr tvs, ppr body_ty, ppr arg_tys]
914 n_tvs = length tvs
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 outer_ty@(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 `unionVarSet` tyCoVarsOfType outer_ty
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 ---------------------------------------------------------------------
1176 ForAllTy
1177 ~~~~~~~~
1178 -}
1179
1180 mkForAllTy :: TyBinder -> Type -> Type
1181 mkForAllTy = ForAllTy
1182
1183 -- | Make a dependent forall.
1184 mkNamedForAllTy :: TyVar -> VisibilityFlag -> Type -> Type
1185 mkNamedForAllTy tv vis = ASSERT( isTyVar tv )
1186 ForAllTy (Named tv vis)
1187
1188 -- | Like mkForAllTys, but assumes all variables are dependent and invisible,
1189 -- a common case
1190 mkInvForAllTys :: [TyVar] -> Type -> Type
1191 mkInvForAllTys tvs = ASSERT( all isTyVar tvs )
1192 mkForAllTys (map (flip Named Invisible) tvs)
1193
1194 -- | Like mkForAllTys, but assumes all variables are dependent and specified,
1195 -- a common case
1196 mkSpecForAllTys :: [TyVar] -> Type -> Type
1197 mkSpecForAllTys tvs = ASSERT( all isTyVar tvs )
1198 mkForAllTys (map (flip Named Specified) tvs)
1199
1200 -- | Like mkForAllTys, but assumes all variables are dependent and visible
1201 mkVisForAllTys :: [TyVar] -> Type -> Type
1202 mkVisForAllTys tvs = ASSERT( all isTyVar tvs )
1203 mkForAllTys (map (flip Named Visible) tvs)
1204
1205 mkPiType :: Var -> Type -> Type
1206 -- ^ Makes a @(->)@ type or an implicit forall type, depending
1207 -- on whether it is given a type variable or a term variable.
1208 -- This is used, for example, when producing the type of a lambda.
1209 -- Always uses Invisible binders.
1210 mkPiTypes :: [Var] -> Type -> Type
1211 -- ^ 'mkPiType' for multiple type or value arguments
1212
1213 mkPiType v ty
1214 | isTyVar v = mkForAllTy (Named v Invisible) ty
1215 | otherwise = mkForAllTy (Anon (varType v)) ty
1216
1217 mkPiTypes vs ty = foldr mkPiType ty vs
1218
1219 -- | Given a list of type-level vars and a result type, makes TyBinders, preferring
1220 -- anonymous binders if the variable is, in fact, not dependent.
1221 -- All binders are /visible/.
1222 mkTyBindersPreferAnon :: [TyVar] -> Type -> [TyBinder]
1223 mkTyBindersPreferAnon vars inner_ty = fst $ go vars inner_ty
1224 where
1225 go :: [TyVar] -> Type -> ([TyBinder], VarSet) -- also returns the free vars
1226 go [] ty = ([], tyCoVarsOfType ty)
1227 go (v:vs) ty | v `elemVarSet` fvs
1228 = ( Named v Visible : binders
1229 , fvs `delVarSet` v `unionVarSet` kind_vars )
1230 | otherwise
1231 = ( Anon (tyVarKind v) : binders
1232 , fvs `unionVarSet` kind_vars )
1233 where
1234 (binders, fvs) = go vs ty
1235 kind_vars = tyCoVarsOfType $ tyVarKind v
1236
1237 -- | Take a ForAllTy apart, returning the list of tyvars and the result type.
1238 -- This always succeeds, even if it returns only an empty list. Note that the
1239 -- result type returned may have free variables that were bound by a forall.
1240 splitForAllTys :: Type -> ([TyVar], Type)
1241 splitForAllTys ty = split ty ty []
1242 where
1243 split orig_ty ty tvs | Just ty' <- coreView ty = split orig_ty ty' tvs
1244 split _ (ForAllTy (Named tv _) ty) tvs = split ty ty (tv:tvs)
1245 split orig_ty _ tvs = (reverse tvs, orig_ty)
1246
1247 -- | Split off all TyBinders to a type, splitting both proper foralls
1248 -- and functions
1249 splitPiTys :: Type -> ([TyBinder], Type)
1250 splitPiTys ty = split ty ty []
1251 where
1252 split orig_ty ty bs | Just ty' <- coreView ty = split orig_ty ty' bs
1253 split _ (ForAllTy b res) bs = split res res (b:bs)
1254 split orig_ty _ bs = (reverse bs, orig_ty)
1255
1256 -- | Like 'splitPiTys' but split off only /named/ binders.
1257 splitNamedPiTys :: Type -> ([TyBinder], Type)
1258 splitNamedPiTys ty = split ty ty []
1259 where
1260 split orig_ty ty bs | Just ty' <- coreView ty = split orig_ty ty' bs
1261 split _ (ForAllTy b@(Named {}) res) bs = split res res (b:bs)
1262 split orig_ty _ bs = (reverse bs, orig_ty)
1263
1264 -- | Checks whether this is a proper forall (with a named binder)
1265 isForAllTy :: Type -> Bool
1266 isForAllTy (ForAllTy (Named {}) _) = True
1267 isForAllTy _ = False
1268
1269 -- | Is this a function or forall?
1270 isPiTy :: Type -> Bool
1271 isPiTy (ForAllTy {}) = True
1272 isPiTy _ = False
1273
1274 -- | Take a forall type apart, or panics if that is not possible.
1275 splitForAllTy :: Type -> (TyVar, Type)
1276 splitForAllTy ty
1277 | Just answer <- splitForAllTy_maybe ty = answer
1278 | otherwise = pprPanic "splitForAllTy" (ppr ty)
1279
1280 -- | Attempts to take a forall type apart, but only if it's a proper forall,
1281 -- with a named binder
1282 splitForAllTy_maybe :: Type -> Maybe (TyVar, Type)
1283 splitForAllTy_maybe ty = splitFAT_m ty
1284 where
1285 splitFAT_m ty | Just ty' <- coreView ty = splitFAT_m ty'
1286 splitFAT_m (ForAllTy (Named tv _) ty) = Just (tv, ty)
1287 splitFAT_m _ = Nothing
1288
1289 -- | Attempts to take a forall type apart; works with proper foralls and
1290 -- functions
1291 splitPiTy_maybe :: Type -> Maybe (TyBinder, Type)
1292 splitPiTy_maybe ty = go ty
1293 where
1294 go ty | Just ty' <- coreView ty = go ty'
1295 go (ForAllTy bndr ty) = Just (bndr, ty)
1296 go _ = Nothing
1297
1298 -- | Takes a forall type apart, or panics
1299 splitPiTy :: Type -> (TyBinder, Type)
1300 splitPiTy ty
1301 | Just answer <- splitPiTy_maybe ty = answer
1302 | otherwise = pprPanic "splitPiTy" (ppr ty)
1303
1304 -- | Drops all non-anonymous ForAllTys
1305 dropForAlls :: Type -> Type
1306 dropForAlls ty | Just ty' <- coreView ty = dropForAlls ty'
1307 | otherwise = go ty
1308 where
1309 go (ForAllTy (Named {}) res) = go res
1310 go res = res
1311
1312 -- | Given a tycon and its arguments, filters out any invisible arguments
1313 filterOutInvisibleTypes :: TyCon -> [Type] -> [Type]
1314 filterOutInvisibleTypes tc tys = snd $ partitionInvisibles tc id tys
1315
1316 -- | Like 'filterOutInvisibles', but works on 'TyVar's
1317 filterOutInvisibleTyVars :: TyCon -> [TyVar] -> [TyVar]
1318 filterOutInvisibleTyVars tc tvs = snd $ partitionInvisibles tc mkTyVarTy tvs
1319
1320 -- | Given a tycon and a list of things (which correspond to arguments),
1321 -- partitions the things into the invisible ones and the visible ones.
1322 -- The callback function is necessary for this scenario:
1323 --
1324 -- > T :: forall k. k -> k
1325 -- > partitionInvisibles T [forall m. m -> m -> m, S, R, Q]
1326 --
1327 -- After substituting, we get
1328 --
1329 -- > T (forall m. m -> m -> m) :: (forall m. m -> m -> m) -> forall n. n -> n -> n
1330 --
1331 -- Thus, the first argument is invisible, @S@ is visible, @R@ is invisible again,
1332 -- and @Q@ is visible.
1333 --
1334 -- If you're absolutely sure that your tycon's kind doesn't end in a variable,
1335 -- it's OK if the callback function panics, as that's the only time it's
1336 -- consulted.
1337 partitionInvisibles :: TyCon -> (a -> Type) -> [a] -> ([a], [a])
1338 partitionInvisibles tc get_ty = go emptyTCvSubst (tyConKind tc)
1339 where
1340 go _ _ [] = ([], [])
1341 go subst (ForAllTy bndr res_ki) (x:xs)
1342 | isVisibleBinder bndr = second (x :) (go subst' res_ki xs)
1343 | otherwise = first (x :) (go subst' res_ki xs)
1344 where
1345 subst' = extendTvSubstBinder subst bndr (get_ty x)
1346 go subst (TyVarTy tv) xs
1347 | Just ki <- lookupTyVar subst tv = go subst ki xs
1348 go _ _ xs = ([], xs) -- something is ill-kinded. But this can happen
1349 -- when printing errors. Assume everything is visible.
1350
1351 -- like splitPiTys, but returns only *invisible* binders, including constraints
1352 splitPiTysInvisible :: Type -> ([TyBinder], Type)
1353 splitPiTysInvisible ty = split ty ty []
1354 where
1355 split orig_ty ty bndrs
1356 | Just ty' <- coreView ty = split orig_ty ty' bndrs
1357 split _ (ForAllTy bndr ty) bndrs
1358 | isInvisibleBinder bndr
1359 = split ty ty (bndr:bndrs)
1360
1361 split orig_ty _ bndrs
1362 = (reverse bndrs, orig_ty)
1363
1364 {-
1365 %************************************************************************
1366 %* *
1367 TyBinders
1368 %* *
1369 %************************************************************************
1370 -}
1371
1372 -- | Make a named binder
1373 mkNamedBinder :: VisibilityFlag -> Var -> TyBinder
1374 mkNamedBinder vis var = Named var vis
1375
1376 -- | Make many named binders
1377 mkNamedBinders :: VisibilityFlag -> [TyVar] -> [TyBinder]
1378 mkNamedBinders vis = map (mkNamedBinder vis)
1379
1380 -- | Make an anonymous binder
1381 mkAnonBinder :: Type -> TyBinder
1382 mkAnonBinder = Anon
1383
1384 -- | Does this binder bind a variable that is /not/ erased? Returns
1385 -- 'True' for anonymous binders.
1386 isIdLikeBinder :: TyBinder -> Bool
1387 isIdLikeBinder (Named {}) = False
1388 isIdLikeBinder (Anon {}) = True
1389
1390 -- | Does this type, when used to the left of an arrow, require
1391 -- a visible argument? This checks to see if the kind of the type
1392 -- is constraint.
1393 isVisibleType :: Type -> Bool
1394 isVisibleType = not . isPredTy
1395
1396 binderVisibility :: TyBinder -> VisibilityFlag
1397 binderVisibility (Named _ vis) = vis
1398 binderVisibility (Anon ty)
1399 | isVisibleType ty = Visible
1400 | otherwise = Invisible
1401
1402 -- | Extract a bound variable in a binder, if any
1403 binderVar_maybe :: TyBinder -> Maybe Var
1404 binderVar_maybe (Named v _) = Just v
1405 binderVar_maybe (Anon {}) = Nothing
1406
1407 -- | Extract a bound variable in a binder, or panics
1408 binderVar :: String -- ^ printed if there is a panic
1409 -> TyBinder -> Var
1410 binderVar _ (Named v _) = v
1411 binderVar e (Anon t) = pprPanic ("binderVar (" ++ e ++ ")") (ppr t)
1412
1413 -- | Extract a relevant type, if there is one.
1414 binderRelevantType_maybe :: TyBinder -> Maybe Type
1415 binderRelevantType_maybe (Named {}) = Nothing
1416 binderRelevantType_maybe (Anon ty) = Just ty
1417
1418 -- | Like 'maybe', but for binders.
1419 caseBinder :: TyBinder -- ^ binder to scrutinize
1420 -> (TyVar -> a) -- ^ named case
1421 -> (Type -> a) -- ^ anonymous case
1422 -> a
1423 caseBinder (Named v _) f _ = f v
1424 caseBinder (Anon t) _ d = d t
1425
1426 -- | Break apart a list of binders into tyvars and anonymous types.
1427 partitionBinders :: [TyBinder] -> ([TyVar], [Type])
1428 partitionBinders = partitionWith named_or_anon
1429 where
1430 named_or_anon bndr = caseBinder bndr Left Right
1431
1432 -- | Break apart a list of binders into a list of named binders and
1433 -- a list of anonymous types.
1434 partitionBindersIntoBinders :: [TyBinder] -> ([TyBinder], [Type])
1435 partitionBindersIntoBinders = partitionWith named_or_anon
1436 where
1437 named_or_anon bndr = caseBinder bndr (\_ -> Left bndr) Right
1438
1439 {-
1440 %************************************************************************
1441 %* *
1442 Pred
1443 * *
1444 ************************************************************************
1445
1446 Predicates on PredType
1447
1448 Note [isPredTy complications]
1449 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1450 You would think that we could define
1451 isPredTy ty = isConstraintKind (typeKind ty)
1452 But there are a number of complications:
1453
1454 * isPredTy is used when printing types, which can happen in debug
1455 printing during type checking of not-fully-zonked types. So it's
1456 not cool to say isConstraintKind (typeKind ty) because, absent
1457 zonking, the type might be ill-kinded, and typeKind crashes. Hence the
1458 rather tiresome story here
1459
1460 * isPredTy must return "True" to *unlifted* coercions, such as (t1 ~# t2)
1461 and (t1 ~R# t2), which are not of kind Constraint! Currently they are
1462 of kind #.
1463
1464 * If we do form the type '(C a => C [a]) => blah', then we'd like to
1465 print it as such. But that means that isPredTy must return True for
1466 (C a => C [a]). Admittedly that type is illegal in Haskell, but we
1467 want to print it nicely in error messages.
1468 -}
1469
1470 -- | Is the type suitable to classify a given/wanted in the typechecker?
1471 isPredTy :: Type -> Bool
1472 -- See Note [isPredTy complications]
1473 isPredTy ty = go ty []
1474 where
1475 go :: Type -> [KindOrType] -> Bool
1476 go (AppTy ty1 ty2) args = go ty1 (ty2 : args)
1477 go (TyVarTy tv) args = go_k (tyVarKind tv) args
1478 go (TyConApp tc tys) args = ASSERT( null args ) -- TyConApp invariant
1479 go_tc tc tys
1480 go (ForAllTy (Anon arg) res) []
1481 | isPredTy arg = isPredTy res -- (Eq a => C a)
1482 | otherwise = False -- (Int -> Bool)
1483 go (ForAllTy (Named {}) ty) [] = go ty []
1484 go (CastTy _ co) args = go_k (pSnd (coercionKind co)) args
1485 go _ _ = False
1486
1487 go_tc :: TyCon -> [KindOrType] -> Bool
1488 go_tc tc args
1489 | tc `hasKey` eqPrimTyConKey || tc `hasKey` eqReprPrimTyConKey
1490 = length args == 4 -- ~# and ~R# sadly have result kind #
1491 -- not Contraint; but we still want
1492 -- isPredTy to reply True.
1493 | otherwise = go_k (tyConKind tc) args
1494
1495 go_k :: Kind -> [KindOrType] -> Bool
1496 -- True <=> ('k' applied to 'kts') = Constraint
1497 go_k k [] = isConstraintKind k
1498 go_k k (arg:args) = case piResultTy_maybe k arg of
1499 Just k' -> go_k k' args
1500 Nothing -> pprTrace "isPredTy" (ppr ty)
1501 False
1502 -- This last case should not happen; but it does if we
1503 -- we call isPredTy during kind checking, especially if
1504 -- there is actually a kind error. Example that showed
1505 -- this up: polykinds/T11399
1506
1507 isClassPred, isEqPred, isNomEqPred, isIPPred :: PredType -> Bool
1508 isClassPred ty = case tyConAppTyCon_maybe ty of
1509 Just tyCon | isClassTyCon tyCon -> True
1510 _ -> False
1511 isEqPred ty = case tyConAppTyCon_maybe ty of
1512 Just tyCon -> tyCon `hasKey` eqPrimTyConKey
1513 || tyCon `hasKey` eqReprPrimTyConKey
1514 _ -> False
1515
1516 isNomEqPred ty = case tyConAppTyCon_maybe ty of
1517 Just tyCon -> tyCon `hasKey` eqPrimTyConKey
1518 _ -> False
1519
1520 isIPPred ty = case tyConAppTyCon_maybe ty of
1521 Just tc -> isIPTyCon tc
1522 _ -> False
1523
1524 isIPTyCon :: TyCon -> Bool
1525 isIPTyCon tc = tc `hasKey` ipClassKey
1526 -- Class and its corresponding TyCon have the same Unique
1527
1528 isIPClass :: Class -> Bool
1529 isIPClass cls = cls `hasKey` ipClassKey
1530
1531 isCTupleClass :: Class -> Bool
1532 isCTupleClass cls = isTupleTyCon (classTyCon cls)
1533
1534 isIPPred_maybe :: Type -> Maybe (FastString, Type)
1535 isIPPred_maybe ty =
1536 do (tc,[t1,t2]) <- splitTyConApp_maybe ty
1537 guard (isIPTyCon tc)
1538 x <- isStrLitTy t1
1539 return (x,t2)
1540
1541 {-
1542 Make PredTypes
1543
1544 --------------------- Equality types ---------------------------------
1545 -}
1546
1547 -- | Makes a lifted equality predicate at the given role
1548 mkPrimEqPredRole :: Role -> Type -> Type -> PredType
1549 mkPrimEqPredRole Nominal = mkPrimEqPred
1550 mkPrimEqPredRole Representational = mkReprPrimEqPred
1551 mkPrimEqPredRole Phantom = panic "mkPrimEqPredRole phantom"
1552
1553 -- | Creates a primitive type equality predicate.
1554 -- Invariant: the types are not Coercions
1555 mkPrimEqPred :: Type -> Type -> Type
1556 mkPrimEqPred ty1 ty2
1557 = TyConApp eqPrimTyCon [k1, k2, ty1, ty2]
1558 where
1559 k1 = typeKind ty1
1560 k2 = typeKind ty2
1561
1562 -- | Creates a primite type equality predicate with explicit kinds
1563 mkHeteroPrimEqPred :: Kind -> Kind -> Type -> Type -> Type
1564 mkHeteroPrimEqPred k1 k2 ty1 ty2 = TyConApp eqPrimTyCon [k1, k2, ty1, ty2]
1565
1566 -- | Creates a primitive representational type equality predicate
1567 -- with explicit kinds
1568 mkHeteroReprPrimEqPred :: Kind -> Kind -> Type -> Type -> Type
1569 mkHeteroReprPrimEqPred k1 k2 ty1 ty2
1570 = TyConApp eqReprPrimTyCon [k1, k2, ty1, ty2]
1571
1572 -- | Try to split up a coercion type into the types that it coerces
1573 splitCoercionType_maybe :: Type -> Maybe (Type, Type)
1574 splitCoercionType_maybe ty
1575 = do { (tc, [_, _, ty1, ty2]) <- splitTyConApp_maybe ty
1576 ; guard $ tc `hasKey` eqPrimTyConKey || tc `hasKey` eqReprPrimTyConKey
1577 ; return (ty1, ty2) }
1578
1579 mkReprPrimEqPred :: Type -> Type -> Type
1580 mkReprPrimEqPred ty1 ty2
1581 = TyConApp eqReprPrimTyCon [k1, k2, ty1, ty2]
1582 where
1583 k1 = typeKind ty1
1584 k2 = typeKind ty2
1585
1586 equalityTyCon :: Role -> TyCon
1587 equalityTyCon Nominal = eqPrimTyCon
1588 equalityTyCon Representational = eqReprPrimTyCon
1589 equalityTyCon Phantom = eqPhantPrimTyCon
1590
1591 -- --------------------- Dictionary types ---------------------------------
1592
1593 mkClassPred :: Class -> [Type] -> PredType
1594 mkClassPred clas tys = TyConApp (classTyCon clas) tys
1595
1596 isDictTy :: Type -> Bool
1597 isDictTy = isClassPred
1598
1599 isDictLikeTy :: Type -> Bool
1600 -- Note [Dictionary-like types]
1601 isDictLikeTy ty | Just ty' <- coreView ty = isDictLikeTy ty'
1602 isDictLikeTy ty = case splitTyConApp_maybe ty of
1603 Just (tc, tys) | isClassTyCon tc -> True
1604 | isTupleTyCon tc -> all isDictLikeTy tys
1605 _other -> False
1606
1607 {-
1608 Note [Dictionary-like types]
1609 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1610 Being "dictionary-like" means either a dictionary type or a tuple thereof.
1611 In GHC 6.10 we build implication constraints which construct such tuples,
1612 and if we land up with a binding
1613 t :: (C [a], Eq [a])
1614 t = blah
1615 then we want to treat t as cheap under "-fdicts-cheap" for example.
1616 (Implication constraints are normally inlined, but sadly not if the
1617 occurrence is itself inside an INLINE function! Until we revise the
1618 handling of implication constraints, that is.) This turned out to
1619 be important in getting good arities in DPH code. Example:
1620
1621 class C a
1622 class D a where { foo :: a -> a }
1623 instance C a => D (Maybe a) where { foo x = x }
1624
1625 bar :: (C a, C b) => a -> b -> (Maybe a, Maybe b)
1626 {-# INLINE bar #-}
1627 bar x y = (foo (Just x), foo (Just y))
1628
1629 Then 'bar' should jolly well have arity 4 (two dicts, two args), but
1630 we ended up with something like
1631 bar = __inline_me__ (\d1,d2. let t :: (D (Maybe a), D (Maybe b)) = ...
1632 in \x,y. <blah>)
1633
1634 This is all a bit ad-hoc; eg it relies on knowing that implication
1635 constraints build tuples.
1636
1637
1638 Decomposing PredType
1639 -}
1640
1641 -- | A choice of equality relation. This is separate from the type 'Role'
1642 -- because 'Phantom' does not define a (non-trivial) equality relation.
1643 data EqRel = NomEq | ReprEq
1644 deriving (Eq, Ord)
1645
1646 instance Outputable EqRel where
1647 ppr NomEq = text "nominal equality"
1648 ppr ReprEq = text "representational equality"
1649
1650 eqRelRole :: EqRel -> Role
1651 eqRelRole NomEq = Nominal
1652 eqRelRole ReprEq = Representational
1653
1654 data PredTree = ClassPred Class [Type]
1655 | EqPred EqRel Type Type
1656 | IrredPred PredType
1657
1658 classifyPredType :: PredType -> PredTree
1659 classifyPredType ev_ty = case splitTyConApp_maybe ev_ty of
1660 Just (tc, [_, _, ty1, ty2])
1661 | tc `hasKey` eqReprPrimTyConKey -> EqPred ReprEq ty1 ty2
1662 | tc `hasKey` eqPrimTyConKey -> EqPred NomEq ty1 ty2
1663 Just (tc, tys)
1664 | Just clas <- tyConClass_maybe tc -> ClassPred clas tys
1665 _ -> IrredPred ev_ty
1666
1667 getClassPredTys :: PredType -> (Class, [Type])
1668 getClassPredTys ty = case getClassPredTys_maybe ty of
1669 Just (clas, tys) -> (clas, tys)
1670 Nothing -> pprPanic "getClassPredTys" (ppr ty)
1671
1672 getClassPredTys_maybe :: PredType -> Maybe (Class, [Type])
1673 getClassPredTys_maybe ty = case splitTyConApp_maybe ty of
1674 Just (tc, tys) | Just clas <- tyConClass_maybe tc -> Just (clas, tys)
1675 _ -> Nothing
1676
1677 getEqPredTys :: PredType -> (Type, Type)
1678 getEqPredTys ty
1679 = case splitTyConApp_maybe ty of
1680 Just (tc, [_, _, ty1, ty2])
1681 | tc `hasKey` eqPrimTyConKey
1682 || tc `hasKey` eqReprPrimTyConKey
1683 -> (ty1, ty2)
1684 _ -> pprPanic "getEqPredTys" (ppr ty)
1685
1686 getEqPredTys_maybe :: PredType -> Maybe (Role, Type, Type)
1687 getEqPredTys_maybe ty
1688 = case splitTyConApp_maybe ty of
1689 Just (tc, [_, _, ty1, ty2])
1690 | tc `hasKey` eqPrimTyConKey -> Just (Nominal, ty1, ty2)
1691 | tc `hasKey` eqReprPrimTyConKey -> Just (Representational, ty1, ty2)
1692 _ -> Nothing
1693
1694 getEqPredRole :: PredType -> Role
1695 getEqPredRole ty = eqRelRole (predTypeEqRel ty)
1696
1697 -- | Get the equality relation relevant for a pred type.
1698 predTypeEqRel :: PredType -> EqRel
1699 predTypeEqRel ty
1700 | Just (tc, _) <- splitTyConApp_maybe ty
1701 , tc `hasKey` eqReprPrimTyConKey
1702 = ReprEq
1703 | otherwise
1704 = NomEq
1705
1706 {-
1707 %************************************************************************
1708 %* *
1709 Size
1710 * *
1711 ************************************************************************
1712 -}
1713
1714 -- NB: This function does not respect `eqType`, in that two types that
1715 -- are `eqType` may return different sizes. This is OK, because this
1716 -- function is used only in reporting, not decision-making.
1717 typeSize :: Type -> Int
1718 typeSize (LitTy {}) = 1
1719 typeSize (TyVarTy {}) = 1
1720 typeSize (AppTy t1 t2) = typeSize t1 + typeSize t2
1721 typeSize (ForAllTy b t) = typeSize (binderType b) + typeSize t
1722 typeSize (TyConApp _ ts) = 1 + sum (map typeSize ts)
1723 typeSize (CastTy ty co) = typeSize ty + coercionSize co
1724 typeSize (CoercionTy co) = coercionSize co
1725
1726
1727 {- **********************************************************************
1728 * *
1729 Representation types
1730 * *
1731 ********************************************************************** -}
1732
1733 type UnaryType = Type
1734
1735 data RepType
1736 = UbxTupleRep [UnaryType] -- Represented by multiple values
1737 -- Can be zero, one, or more
1738 | UnaryRep UnaryType -- Represented by a single value
1739
1740 instance Outputable RepType where
1741 ppr (UbxTupleRep tys) = text "UbxTupleRep" <+> ppr tys
1742 ppr (UnaryRep ty) = text "UnaryRep" <+> ppr ty
1743
1744 flattenRepType :: RepType -> [UnaryType]
1745 flattenRepType (UbxTupleRep tys) = tys
1746 flattenRepType (UnaryRep ty) = [ty]
1747
1748 -- | 'repType' figure out how a type will be represented
1749 -- at runtime. It looks through
1750 --
1751 -- 1. For-alls
1752 -- 2. Synonyms
1753 -- 3. Predicates
1754 -- 4. All newtypes, including recursive ones, but not newtype families
1755 -- 5. Casts
1756 --
1757 repType :: Type -> RepType
1758 repType ty
1759 = go initRecTc ty
1760 where
1761 go :: RecTcChecker -> Type -> RepType
1762 go rec_nts ty -- Expand predicates and synonyms
1763 | Just ty' <- coreView ty
1764 = go rec_nts ty'
1765
1766 go rec_nts (ForAllTy (Named {}) ty2) -- Drop type foralls
1767 = go rec_nts ty2
1768
1769 go rec_nts (TyConApp tc tys) -- Expand newtypes
1770 | isNewTyCon tc
1771 , tys `lengthAtLeast` tyConArity tc
1772 , Just rec_nts' <- checkRecTc rec_nts tc -- See Note [Expanding newtypes] in TyCon
1773 = go rec_nts' (newTyConInstRhs tc tys)
1774
1775 | isUnboxedTupleTyCon tc
1776 = UbxTupleRep (concatMap (flattenRepType . go rec_nts) non_rr_tys)
1777 where
1778 -- See Note [Unboxed tuple RuntimeRep vars] in TyCon
1779 non_rr_tys = dropRuntimeRepArgs tys
1780
1781 go rec_nts (CastTy ty _)
1782 = go rec_nts ty
1783
1784 go _ ty@(CoercionTy _)
1785 = pprPanic "repType" (ppr ty)
1786
1787 go _ ty = UnaryRep ty
1788
1789 -- ToDo: this could be moved to the code generator, using splitTyConApp instead
1790 -- of inspecting the type directly.
1791
1792 -- | Discovers the primitive representation of a more abstract 'UnaryType'
1793 typePrimRep :: UnaryType -> PrimRep
1794 typePrimRep ty = kindPrimRep (typeKind ty)
1795
1796 -- | Find the primitive representation of a 'TyCon'. Defined here to
1797 -- avoid module loops. Call this only on unlifted tycons.
1798 tyConPrimRep :: TyCon -> PrimRep
1799 tyConPrimRep tc = kindPrimRep res_kind
1800 where
1801 res_kind = tyConResKind tc
1802
1803 -- | Take a kind (of shape @TYPE rr@) and produce the 'PrimRep' of values
1804 -- of types of this kind.
1805 kindPrimRep :: Kind -> PrimRep
1806 kindPrimRep ki | Just ki' <- coreViewOneStarKind ki = kindPrimRep ki'
1807 kindPrimRep (TyConApp typ [runtime_rep])
1808 = ASSERT( typ `hasKey` tYPETyConKey )
1809 go runtime_rep
1810 where
1811 go rr | Just rr' <- coreView rr = go rr'
1812 go (TyConApp rr_dc args)
1813 | RuntimeRep fun <- tyConRuntimeRepInfo rr_dc
1814 = fun args
1815 go rr = pprPanic "kindPrimRep.go" (ppr rr)
1816 kindPrimRep ki = WARN( True
1817 , text "kindPrimRep defaulting to PtrRep on" <+> ppr ki )
1818 PtrRep -- this can happen legitimately for, e.g., Any
1819
1820 typeRepArity :: Arity -> Type -> RepArity
1821 typeRepArity 0 _ = 0
1822 typeRepArity n ty = case repType ty of
1823 UnaryRep (ForAllTy bndr ty) -> length (flattenRepType (repType (binderType bndr)))
1824 + typeRepArity (n - 1) ty
1825 _ -> pprPanic "typeRepArity: arity greater than type can handle" (ppr (n, ty, repType ty))
1826
1827 isVoidTy :: Type -> Bool
1828 -- True if the type has zero width
1829 isVoidTy ty = case repType ty of
1830 UnaryRep (TyConApp tc _) -> isUnliftedTyCon tc &&
1831 isVoidRep (tyConPrimRep tc)
1832 _ -> False
1833
1834
1835 {-
1836 %************************************************************************
1837 %* *
1838 Well-scoped tyvars
1839 * *
1840 ************************************************************************
1841 -}
1842
1843 -- | Do a topological sort on a list of tyvars,
1844 -- so that binders occur before occurrences
1845 -- E.g. given [ a::k, k::*, b::k ]
1846 -- it'll return a well-scoped list [ k::*, a::k, b::k ]
1847 --
1848 -- This is a deterministic sorting operation
1849 -- (that is, doesn't depend on Uniques).
1850 toposortTyVars :: [TyVar] -> [TyVar]
1851 toposortTyVars tvs = reverse $
1852 [ tv | (tv, _, _) <- topologicalSortG $
1853 graphFromEdgedVertices nodes ]
1854 where
1855 var_ids :: VarEnv Int
1856 var_ids = mkVarEnv (zip tvs [1..])
1857
1858 nodes = [ ( tv
1859 , lookupVarEnv_NF var_ids tv
1860 , mapMaybe (lookupVarEnv var_ids)
1861 (tyCoVarsOfTypeList (tyVarKind tv)) )
1862 | tv <- tvs ]
1863
1864 -- | Extract a well-scoped list of variables from a deterministic set of
1865 -- variables. The result is deterministic.
1866 -- NB: There used to exist varSetElemsWellScoped :: VarSet -> [Var] which
1867 -- took a non-deterministic set and produced a non-deterministic
1868 -- well-scoped list. If you care about the list being well-scoped you also
1869 -- most likely care about it being in deterministic order.
1870 dVarSetElemsWellScoped :: DVarSet -> [Var]
1871 dVarSetElemsWellScoped = toposortTyVars . dVarSetElems
1872
1873 -- | Get the free vars of a type in scoped order
1874 tyCoVarsOfTypeWellScoped :: Type -> [TyVar]
1875 tyCoVarsOfTypeWellScoped = toposortTyVars . tyCoVarsOfTypeList
1876
1877 -- | Get the free vars of types in scoped order
1878 tyCoVarsOfTypesWellScoped :: [Type] -> [TyVar]
1879 tyCoVarsOfTypesWellScoped = toposortTyVars . tyCoVarsOfTypesList
1880
1881 {-
1882 ************************************************************************
1883 * *
1884 \subsection{Type families}
1885 * *
1886 ************************************************************************
1887 -}
1888
1889 mkFamilyTyConApp :: TyCon -> [Type] -> Type
1890 -- ^ Given a family instance TyCon and its arg types, return the
1891 -- corresponding family type. E.g:
1892 --
1893 -- > data family T a
1894 -- > data instance T (Maybe b) = MkT b
1895 --
1896 -- Where the instance tycon is :RTL, so:
1897 --
1898 -- > mkFamilyTyConApp :RTL Int = T (Maybe Int)
1899 mkFamilyTyConApp tc tys
1900 | Just (fam_tc, fam_tys) <- tyConFamInst_maybe tc
1901 , let tvs = tyConTyVars tc
1902 fam_subst = ASSERT2( length tvs == length tys, ppr tc <+> ppr tys )
1903 zipTvSubst tvs tys
1904 = mkTyConApp fam_tc (substTys fam_subst fam_tys)
1905 | otherwise
1906 = mkTyConApp tc tys
1907
1908 -- | Get the type on the LHS of a coercion induced by a type/data
1909 -- family instance.
1910 coAxNthLHS :: CoAxiom br -> Int -> Type
1911 coAxNthLHS ax ind =
1912 mkTyConApp (coAxiomTyCon ax) (coAxBranchLHS (coAxiomNthBranch ax ind))
1913
1914 -- | Pretty prints a 'TyCon', using the family instance in case of a
1915 -- representation tycon. For example:
1916 --
1917 -- > data T [a] = ...
1918 --
1919 -- In that case we want to print @T [a]@, where @T@ is the family 'TyCon'
1920 pprSourceTyCon :: TyCon -> SDoc
1921 pprSourceTyCon tycon
1922 | Just (fam_tc, tys) <- tyConFamInst_maybe tycon
1923 = ppr $ fam_tc `TyConApp` tys -- can't be FunTyCon
1924 | otherwise
1925 = ppr tycon
1926
1927 {-
1928 ************************************************************************
1929 * *
1930 \subsection{Liftedness}
1931 * *
1932 ************************************************************************
1933 -}
1934
1935 -- | See "Type#type_classification" for what an unlifted type is
1936 isUnliftedType :: Type -> Bool
1937 -- isUnliftedType returns True for forall'd unlifted types:
1938 -- x :: forall a. Int#
1939 -- I found bindings like these were getting floated to the top level.
1940 -- They are pretty bogus types, mind you. It would be better never to
1941 -- construct them
1942
1943 isUnliftedType ty | Just ty' <- coreView ty = isUnliftedType ty'
1944 isUnliftedType (ForAllTy (Named {}) ty) = isUnliftedType ty
1945 isUnliftedType (TyConApp tc _) = isUnliftedTyCon tc
1946 isUnliftedType _ = False
1947
1948 -- | Extract the RuntimeRep classifier of a type. Panics if this is not possible.
1949 getRuntimeRep :: String -- ^ Printed in case of an error
1950 -> Type -> Type
1951 getRuntimeRep err ty = getRuntimeRepFromKind err (typeKind ty)
1952
1953 -- | Extract the RuntimeRep classifier of a type from its kind.
1954 -- For example, getRuntimeRepFromKind * = PtrRepLifted;
1955 -- getRuntimeRepFromKind # = PtrRepUnlifted.
1956 -- Panics if this is not possible.
1957 getRuntimeRepFromKind :: String -- ^ Printed in case of an error
1958 -> Type -> Type
1959 getRuntimeRepFromKind err = go
1960 where
1961 go k | Just k' <- coreViewOneStarKind k = go k'
1962 go k
1963 | Just (tc, [arg]) <- splitTyConApp_maybe k
1964 , tc `hasKey` tYPETyConKey
1965 = arg
1966 go k = pprPanic "getRuntimeRep" (text err $$
1967 ppr k <+> dcolon <+> ppr (typeKind k))
1968
1969 isUnboxedTupleType :: Type -> Bool
1970 isUnboxedTupleType ty = case tyConAppTyCon_maybe ty of
1971 Just tc -> isUnboxedTupleTyCon tc
1972 _ -> False
1973
1974 -- | See "Type#type_classification" for what an algebraic type is.
1975 -- Should only be applied to /types/, as opposed to e.g. partially
1976 -- saturated type constructors
1977 isAlgType :: Type -> Bool
1978 isAlgType ty
1979 = case splitTyConApp_maybe ty of
1980 Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
1981 isAlgTyCon tc
1982 _other -> False
1983
1984 -- | See "Type#type_classification" for what an algebraic type is.
1985 -- Should only be applied to /types/, as opposed to e.g. partially
1986 -- saturated type constructors. Closed type constructors are those
1987 -- with a fixed right hand side, as opposed to e.g. associated types
1988 isClosedAlgType :: Type -> Bool
1989 isClosedAlgType ty
1990 = case splitTyConApp_maybe ty of
1991 Just (tc, ty_args) | isAlgTyCon tc && not (isFamilyTyCon tc)
1992 -> ASSERT2( ty_args `lengthIs` tyConArity tc, ppr ty ) True
1993 _other -> False
1994
1995 -- | Computes whether an argument (or let right hand side) should
1996 -- be computed strictly or lazily, based only on its type.
1997 -- Currently, it's just 'isUnliftedType'.
1998
1999 isStrictType :: Type -> Bool
2000 isStrictType = isUnliftedType
2001
2002 isPrimitiveType :: Type -> Bool
2003 -- ^ Returns true of types that are opaque to Haskell.
2004 isPrimitiveType ty = case splitTyConApp_maybe ty of
2005 Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
2006 isPrimTyCon tc
2007 _ -> False
2008
2009 {-
2010 ************************************************************************
2011 * *
2012 \subsection{Sequencing on types}
2013 * *
2014 ************************************************************************
2015 -}
2016
2017 seqType :: Type -> ()
2018 seqType (LitTy n) = n `seq` ()
2019 seqType (TyVarTy tv) = tv `seq` ()
2020 seqType (AppTy t1 t2) = seqType t1 `seq` seqType t2
2021 seqType (TyConApp tc tys) = tc `seq` seqTypes tys
2022 seqType (ForAllTy bndr ty) = seqType (binderType bndr) `seq` seqType ty
2023 seqType (CastTy ty co) = seqType ty `seq` seqCo co
2024 seqType (CoercionTy co) = seqCo co
2025
2026 seqTypes :: [Type] -> ()
2027 seqTypes [] = ()
2028 seqTypes (ty:tys) = seqType ty `seq` seqTypes tys
2029
2030 {-
2031 ************************************************************************
2032 * *
2033 Comparison for types
2034 (We don't use instances so that we know where it happens)
2035 * *
2036 ************************************************************************
2037
2038 Note [Equality on AppTys]
2039 ~~~~~~~~~~~~~~~~~~~~~~~~~
2040 In our cast-ignoring equality, we want to say that the following two
2041 are equal:
2042
2043 (Maybe |> co) (Int |> co') ~? Maybe Int
2044
2045 But the left is an AppTy while the right is a TyConApp. The solution is
2046 to use repSplitAppTy_maybe to break up the TyConApp into its pieces and
2047 then continue. Easy to do, but also easy to forget to do.
2048
2049 -}
2050
2051 eqType :: Type -> Type -> Bool
2052 -- ^ Type equality on source types. Does not look through @newtypes@ or
2053 -- 'PredType's, but it does look through type synonyms.
2054 -- This first checks that the kinds of the types are equal and then
2055 -- checks whether the types are equal, ignoring casts and coercions.
2056 -- (The kind check is a recursive call, but since all kinds have type
2057 -- @Type@, there is no need to check the types of kinds.)
2058 -- See also Note [Non-trivial definitional equality] in TyCoRep.
2059 eqType t1 t2 = isEqual $ nonDetCmpType t1 t2
2060 -- It's OK to use nonDetCmpType here and eqType is deterministic,
2061 -- nonDetCmpType does equality deterministically
2062
2063 -- | Compare types with respect to a (presumably) non-empty 'RnEnv2'.
2064 eqTypeX :: RnEnv2 -> Type -> Type -> Bool
2065 eqTypeX env t1 t2 = isEqual $ nonDetCmpTypeX env t1 t2
2066 -- It's OK to use nonDetCmpType here and eqTypeX is deterministic,
2067 -- nonDetCmpTypeX does equality deterministically
2068
2069 -- | Type equality on lists of types, looking through type synonyms
2070 -- but not newtypes.
2071 eqTypes :: [Type] -> [Type] -> Bool
2072 eqTypes tys1 tys2 = isEqual $ nonDetCmpTypes tys1 tys2
2073 -- It's OK to use nonDetCmpType here and eqTypes is deterministic,
2074 -- nonDetCmpTypes does equality deterministically
2075
2076 eqVarBndrs :: RnEnv2 -> [Var] -> [Var] -> Maybe RnEnv2
2077 -- Check that the var lists are the same length
2078 -- and have matching kinds; if so, extend the RnEnv2
2079 -- Returns Nothing if they don't match
2080 eqVarBndrs env [] []
2081 = Just env
2082 eqVarBndrs env (tv1:tvs1) (tv2:tvs2)
2083 | eqTypeX env (tyVarKind tv1) (tyVarKind tv2)
2084 = eqVarBndrs (rnBndr2 env tv1 tv2) tvs1 tvs2
2085 eqVarBndrs _ _ _= Nothing
2086
2087 -- Now here comes the real worker
2088
2089 {-
2090 Note [nonDetCmpType nondeterminism]
2091 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2092 nonDetCmpType is implemented in terms of nonDetCmpTypeX. nonDetCmpTypeX
2093 uses nonDetCmpTc which compares TyCons by their Unique value. Using Uniques for
2094 ordering leads to nondeterminism. We hit the same problem in the TyVarTy case,
2095 comparing type variables is nondeterministic, note the call to nonDetCmpVar in
2096 nonDetCmpTypeX.
2097 See Note [Unique Determinism] for more details.
2098 -}
2099
2100 nonDetCmpType :: Type -> Type -> Ordering
2101 nonDetCmpType t1 t2
2102 -- we know k1 and k2 have the same kind, because they both have kind *.
2103 = nonDetCmpTypeX rn_env t1 t2
2104 where
2105 rn_env = mkRnEnv2 (mkInScopeSet (tyCoVarsOfTypes [t1, t2]))
2106
2107 nonDetCmpTypes :: [Type] -> [Type] -> Ordering
2108 nonDetCmpTypes ts1 ts2 = nonDetCmpTypesX rn_env ts1 ts2
2109 where
2110 rn_env = mkRnEnv2 (mkInScopeSet (tyCoVarsOfTypes (ts1 ++ ts2)))
2111
2112 -- | An ordering relation between two 'Type's (known below as @t1 :: k1@
2113 -- and @t2 :: k2@)
2114 data TypeOrdering = TLT -- ^ @t1 < t2@
2115 | TEQ -- ^ @t1 ~ t2@ and there are no casts in either,
2116 -- therefore we can conclude @k1 ~ k2@
2117 | TEQX -- ^ @t1 ~ t2@ yet one of the types contains a cast so
2118 -- they may differ in kind.
2119 | TGT -- ^ @t1 > t2@
2120 deriving (Eq, Ord, Enum, Bounded)
2121
2122 nonDetCmpTypeX :: RnEnv2 -> Type -> Type -> Ordering -- Main workhorse
2123 -- See Note [Non-trivial definitional equality] in TyCoRep
2124 nonDetCmpTypeX env orig_t1 orig_t2 =
2125 case go env orig_t1 orig_t2 of
2126 -- If there are casts then we also need to do a comparison of the kinds of
2127 -- the types being compared
2128 TEQX -> toOrdering $ go env k1 k2
2129 ty_ordering -> toOrdering ty_ordering
2130 where
2131 k1 = typeKind orig_t1
2132 k2 = typeKind orig_t2
2133
2134 toOrdering :: TypeOrdering -> Ordering
2135 toOrdering TLT = LT
2136 toOrdering TEQ = EQ
2137 toOrdering TEQX = EQ
2138 toOrdering TGT = GT
2139
2140 liftOrdering :: Ordering -> TypeOrdering
2141 liftOrdering LT = TLT
2142 liftOrdering EQ = TEQ
2143 liftOrdering GT = TGT
2144
2145 thenCmpTy :: TypeOrdering -> TypeOrdering -> TypeOrdering
2146 thenCmpTy TEQ rel = rel
2147 thenCmpTy TEQX rel = hasCast rel
2148 thenCmpTy rel _ = rel
2149
2150 hasCast :: TypeOrdering -> TypeOrdering
2151 hasCast TEQ = TEQX
2152 hasCast rel = rel
2153
2154 -- Returns both the resulting ordering relation between the two types
2155 -- and whether either contains a cast.
2156 go :: RnEnv2 -> Type -> Type -> TypeOrdering
2157 go env t1 t2
2158 | Just t1' <- coreViewOneStarKind t1 = go env t1' t2
2159 | Just t2' <- coreViewOneStarKind t2 = go env t1 t2'
2160
2161 go env (TyVarTy tv1) (TyVarTy tv2)
2162 = liftOrdering $ rnOccL env tv1 `nonDetCmpVar` rnOccR env tv2
2163 go env (ForAllTy (Named tv1 _) t1) (ForAllTy (Named tv2 _) t2)
2164 = go env (tyVarKind tv1) (tyVarKind tv2)
2165 `thenCmpTy` go (rnBndr2 env tv1 tv2) t1 t2
2166 -- See Note [Equality on AppTys]
2167 go env (AppTy s1 t1) ty2
2168 | Just (s2, t2) <- repSplitAppTy_maybe ty2
2169 = go env s1 s2 `thenCmpTy` go env t1 t2
2170 go env ty1 (AppTy s2 t2)
2171 | Just (s1, t1) <- repSplitAppTy_maybe ty1
2172 = go env s1 s2 `thenCmpTy` go env t1 t2
2173 go env (ForAllTy (Anon s1) t1) (ForAllTy (Anon s2) t2)
2174 = go env s1 s2 `thenCmpTy` go env t1 t2
2175 go env (TyConApp tc1 tys1) (TyConApp tc2 tys2)
2176 = liftOrdering (tc1 `nonDetCmpTc` tc2) `thenCmpTy` gos env tys1 tys2
2177 go _ (LitTy l1) (LitTy l2) = liftOrdering (compare l1 l2)
2178 go env (CastTy t1 _) t2 = hasCast $ go env t1 t2
2179 go env t1 (CastTy t2 _) = hasCast $ go env t1 t2
2180 go _ (CoercionTy {}) (CoercionTy {}) = TEQ
2181
2182 -- Deal with the rest: TyVarTy < CoercionTy < AppTy < LitTy < TyConApp < ForAllTy
2183 go _ ty1 ty2
2184 = liftOrdering $ (get_rank ty1) `compare` (get_rank ty2)
2185 where get_rank :: Type -> Int
2186 get_rank (CastTy {})
2187 = pprPanic "nonDetCmpTypeX.get_rank" (ppr [ty1,ty2])
2188 get_rank (TyVarTy {}) = 0
2189 get_rank (CoercionTy {}) = 1
2190 get_rank (AppTy {}) = 3
2191 get_rank (LitTy {}) = 4
2192 get_rank (TyConApp {}) = 5
2193 get_rank (ForAllTy (Anon {}) _) = 6
2194 get_rank (ForAllTy (Named {}) _) = 7
2195
2196 gos :: RnEnv2 -> [Type] -> [Type] -> TypeOrdering
2197 gos _ [] [] = TEQ
2198 gos _ [] _ = TLT
2199 gos _ _ [] = TGT
2200 gos env (ty1:tys1) (ty2:tys2) = go env ty1 ty2 `thenCmpTy` gos env tys1 tys2
2201
2202 -------------
2203 nonDetCmpTypesX :: RnEnv2 -> [Type] -> [Type] -> Ordering
2204 nonDetCmpTypesX _ [] [] = EQ
2205 nonDetCmpTypesX env (t1:tys1) (t2:tys2) = nonDetCmpTypeX env t1 t2
2206 `thenCmp` nonDetCmpTypesX env tys1 tys2
2207 nonDetCmpTypesX _ [] _ = LT
2208 nonDetCmpTypesX _ _ [] = GT
2209
2210 -------------
2211 -- | Compare two 'TyCon's. NB: This should /never/ see the "star synonyms",
2212 -- as recognized by Kind.isStarKindSynonymTyCon. See Note
2213 -- [Kind Constraint and kind *] in Kind.
2214 -- See Note [nonDetCmpType nondeterminism]
2215 nonDetCmpTc :: TyCon -> TyCon -> Ordering
2216 nonDetCmpTc tc1 tc2
2217 = ASSERT( not (isStarKindSynonymTyCon tc1) && not (isStarKindSynonymTyCon tc2) )
2218 u1 `nonDetCmpUnique` u2
2219 where
2220 u1 = tyConUnique tc1
2221 u2 = tyConUnique tc2
2222
2223 {-
2224 ************************************************************************
2225 * *
2226 The kind of a type
2227 * *
2228 ************************************************************************
2229 -}
2230
2231 typeKind :: Type -> Kind
2232 typeKind (TyConApp tc tys) = piResultTys (tyConKind tc) tys
2233 typeKind (AppTy fun arg) = piResultTy (typeKind fun) arg
2234 typeKind (LitTy l) = typeLiteralKind l
2235 typeKind (ForAllTy (Anon _) _) = liftedTypeKind
2236 typeKind (ForAllTy _ ty) = typeKind ty
2237 typeKind (TyVarTy tyvar) = tyVarKind tyvar
2238 typeKind (CastTy _ty co) = pSnd $ coercionKind co
2239 typeKind (CoercionTy co) = coercionType co
2240
2241 typeLiteralKind :: TyLit -> Kind
2242 typeLiteralKind l =
2243 case l of
2244 NumTyLit _ -> typeNatKind
2245 StrTyLit _ -> typeSymbolKind
2246
2247 -- | Print a tyvar with its kind
2248 pprTyVar :: TyVar -> SDoc
2249 pprTyVar tv = ppr tv <+> dcolon <+> ppr (tyVarKind tv)
2250
2251 {-
2252 %************************************************************************
2253 %* *
2254 Miscellaneous functions
2255 %* *
2256 %************************************************************************
2257
2258 -}
2259 -- | All type constructors occurring in the type; looking through type
2260 -- synonyms, but not newtypes.
2261 -- When it finds a Class, it returns the class TyCon.
2262 tyConsOfType :: Type -> NameEnv TyCon
2263 tyConsOfType ty
2264 = go ty
2265 where
2266 go :: Type -> NameEnv TyCon -- The NameEnv does duplicate elim
2267 go ty | Just ty' <- coreView ty = go ty'
2268 go (TyVarTy {}) = emptyNameEnv
2269 go (LitTy {}) = emptyNameEnv
2270 go (TyConApp tc tys) = go_tc tc `plusNameEnv` go_s tys
2271 go (AppTy a b) = go a `plusNameEnv` go b
2272 go (ForAllTy (Anon a) b) = go a `plusNameEnv` go b `plusNameEnv` go_tc funTyCon
2273 go (ForAllTy (Named tv _) ty) = go ty `plusNameEnv` go (tyVarKind tv)
2274 go (CastTy ty co) = go ty `plusNameEnv` go_co co
2275 go (CoercionTy co) = go_co co
2276
2277 go_co (Refl _ ty) = go ty
2278 go_co (TyConAppCo _ tc args) = go_tc tc `plusNameEnv` go_cos args
2279 go_co (AppCo co arg) = go_co co `plusNameEnv` go_co arg
2280 go_co (ForAllCo _ kind_co co) = go_co kind_co `plusNameEnv` go_co co
2281 go_co (CoVarCo {}) = emptyNameEnv
2282 go_co (AxiomInstCo ax _ args) = go_ax ax `plusNameEnv` go_cos args
2283 go_co (UnivCo p _ t1 t2) = go_prov p `plusNameEnv` go t1 `plusNameEnv` go t2
2284 go_co (SymCo co) = go_co co
2285 go_co (TransCo co1 co2) = go_co co1 `plusNameEnv` go_co co2
2286 go_co (NthCo _ co) = go_co co
2287 go_co (LRCo _ co) = go_co co
2288 go_co (InstCo co arg) = go_co co `plusNameEnv` go_co arg
2289 go_co (CoherenceCo co1 co2) = go_co co1 `plusNameEnv` go_co co2
2290 go_co (KindCo co) = go_co co
2291 go_co (SubCo co) = go_co co
2292 go_co (AxiomRuleCo _ cs) = go_cos cs
2293
2294 go_prov UnsafeCoerceProv = emptyNameEnv
2295 go_prov (PhantomProv co) = go_co co
2296 go_prov (ProofIrrelProv co) = go_co co
2297 go_prov (PluginProv _) = emptyNameEnv
2298 go_prov (HoleProv _) = emptyNameEnv
2299 -- this last case can happen from the tyConsOfType used from
2300 -- checkTauTvUpdate
2301
2302 go_s tys = foldr (plusNameEnv . go) emptyNameEnv tys
2303 go_cos cos = foldr (plusNameEnv . go_co) emptyNameEnv cos
2304
2305 go_tc tc = unitNameEnv (tyConName tc) tc
2306 go_ax ax = go_tc $ coAxiomTyCon ax
2307
2308 -- | Find the result 'Kind' of a type synonym,
2309 -- after applying it to its 'arity' number of type variables
2310 -- Actually this function works fine on data types too,
2311 -- but they'd always return '*', so we never need to ask
2312 synTyConResKind :: TyCon -> Kind
2313 synTyConResKind tycon = piResultTys (tyConKind tycon) (mkTyVarTys (tyConTyVars tycon))
2314
2315 -- | Retrieve the free variables in this type, splitting them based
2316 -- on whether they are used visibly or invisibly. Invisible ones come
2317 -- first.
2318 splitVisVarsOfType :: Type -> Pair TyCoVarSet
2319 splitVisVarsOfType orig_ty = Pair invis_vars vis_vars
2320 where
2321 Pair invis_vars1 vis_vars = go orig_ty
2322 invis_vars = invis_vars1 `minusVarSet` vis_vars
2323
2324 go (TyVarTy tv) = Pair (tyCoVarsOfType $ tyVarKind tv) (unitVarSet tv)
2325 go (AppTy t1 t2) = go t1 `mappend` go t2
2326 go (TyConApp tc tys) = go_tc tc tys
2327 go (ForAllTy (Anon t1) t2) = go t1 `mappend` go t2
2328 go (ForAllTy (Named tv _) ty)
2329 = ((`delVarSet` tv) <$> go ty) `mappend`
2330 (invisible (tyCoVarsOfType $ tyVarKind tv))
2331 go (LitTy {}) = mempty
2332 go (CastTy ty co) = go ty `mappend` invisible (tyCoVarsOfCo co)
2333 go (CoercionTy co) = invisible $ tyCoVarsOfCo co
2334
2335 invisible vs = Pair vs emptyVarSet
2336
2337 go_tc tc tys = let (invis, vis) = partitionInvisibles tc id tys in
2338 invisible (tyCoVarsOfTypes invis) `mappend` foldMap go vis
2339
2340 splitVisVarsOfTypes :: [Type] -> Pair TyCoVarSet
2341 splitVisVarsOfTypes = foldMap splitVisVarsOfType