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