never executed always true always false
1
2 {-# LANGUAGE FlexibleContexts #-}
3 {-# LANGUAGE ScopedTypeVariables #-}
4
5 {-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
6
7 {-
8 (c) The University of Glasgow 2006
9 (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
10
11 -}
12
13 -- | Types used in the typechecker
14 --
15 -- This module provides the Type interface for front-end parts of the
16 -- compiler. These parts
17 --
18 -- * treat "source types" as opaque:
19 -- newtypes, and predicates are meaningful.
20 -- * look through usage types
21 --
22 module GHC.Tc.Utils.TcType (
23 --------------------------------
24 -- Types
25 TcType, TcSigmaType, TcRhoType, TcTauType, TcPredType, TcThetaType,
26 TcTyVar, TcTyVarSet, TcDTyVarSet, TcTyCoVarSet, TcDTyCoVarSet,
27 TcKind, TcCoVar, TcTyCoVar, TcTyVarBinder, TcInvisTVBinder, TcReqTVBinder,
28 TcTyCon, KnotTied,
29
30 ExpType(..), InferResult(..), ExpSigmaType, ExpRhoType, mkCheckExpType,
31
32 SyntaxOpType(..), synKnownType, mkSynFunTys,
33
34 -- TcLevel
35 TcLevel(..), topTcLevel, pushTcLevel, isTopTcLevel,
36 strictlyDeeperThan, deeperThanOrSame, sameDepthAs,
37 tcTypeLevel, tcTyVarLevel, maxTcLevel,
38 promoteSkolem, promoteSkolemX, promoteSkolemsX,
39 --------------------------------
40 -- MetaDetails
41 TcTyVarDetails(..), pprTcTyVarDetails, vanillaSkolemTv, superSkolemTv,
42 MetaDetails(Flexi, Indirect), MetaInfo(..),
43 isImmutableTyVar, isSkolemTyVar, isMetaTyVar, isMetaTyVarTy, isTyVarTy,
44 tcIsTcTyVar, isTyVarTyVar, isOverlappableTyVar, isTyConableTyVar,
45 isAmbiguousTyVar, isCycleBreakerTyVar, metaTyVarRef, metaTyVarInfo,
46 isFlexi, isIndirect, isRuntimeUnkSkol,
47 metaTyVarTcLevel, setMetaTyVarTcLevel, metaTyVarTcLevel_maybe,
48 isTouchableMetaTyVar, isPromotableMetaTyVar,
49 findDupTyVarTvs, mkTyVarNamePairs,
50
51 --------------------------------
52 -- Builders
53 mkPhiTy, mkInfSigmaTy, mkSpecSigmaTy, mkSigmaTy,
54 mkTcAppTy, mkTcAppTys, mkTcCastTy,
55
56 --------------------------------
57 -- Splitters
58 -- These are important because they do not look through newtypes
59 getTyVar,
60 tcSplitForAllTyVarBinder_maybe,
61 tcSplitForAllTyVars, tcSplitForAllInvisTyVars, tcSplitSomeForAllTyVars,
62 tcSplitForAllReqTVBinders, tcSplitForAllInvisTVBinders,
63 tcSplitPiTys, tcSplitPiTy_maybe, tcSplitForAllTyVarBinders,
64 tcSplitPhiTy, tcSplitPredFunTy_maybe,
65 tcSplitFunTy_maybe, tcSplitFunTys, tcFunArgTy, tcFunResultTy, tcFunResultTyN,
66 tcSplitFunTysN,
67 tcSplitTyConApp, tcSplitTyConApp_maybe,
68 tcTyConAppTyCon, tcTyConAppTyCon_maybe, tcTyConAppArgs,
69 tcSplitAppTy_maybe, tcSplitAppTy, tcSplitAppTys, tcRepSplitAppTy_maybe,
70 tcRepGetNumAppTys,
71 tcGetCastedTyVar_maybe, tcGetTyVar_maybe, tcGetTyVar,
72 tcSplitSigmaTy, tcSplitNestedSigmaTys,
73
74 ---------------------------------
75 -- Predicates.
76 -- Again, newtypes are opaque
77 eqType, eqTypes, nonDetCmpType, nonDetCmpTypes, eqTypeX,
78 pickyEqType, tcEqType, tcEqKind, tcEqTypeNoKindCheck, tcEqTypeVis,
79 tcEqTyConApps,
80 isSigmaTy, isRhoTy, isRhoExpTy, isOverloadedTy,
81 isFloatingTy, isDoubleTy, isFloatTy, isIntTy, isWordTy, isStringTy,
82 isIntegerTy, isNaturalTy,
83 isBoolTy, isUnitTy, isCharTy,
84 isTauTy, isTauTyCon, tcIsTyVarTy, tcIsForAllTy,
85 isPredTy, isTyVarClassPred,
86 checkValidClsArgs, hasTyVarHead,
87 isRigidTy,
88
89 ---------------------------------
90 -- Misc type manipulators
91
92 deNoteType,
93 orphNamesOfType, orphNamesOfCo,
94 orphNamesOfTypes, orphNamesOfCoCon,
95 getDFunTyKey, evVarPred,
96
97 ---------------------------------
98 -- Predicate types
99 mkMinimalBySCs, transSuperClasses,
100 pickQuantifiablePreds, pickCapturedPreds,
101 immSuperClasses, boxEqPred,
102 isImprovementPred,
103
104 -- * Finding type instances
105 tcTyFamInsts, tcTyFamInstsAndVis, tcTyConAppTyFamInstsAndVis, isTyFamFree,
106
107 -- * Finding "exact" (non-dead) type variables
108 exactTyCoVarsOfType, exactTyCoVarsOfTypes,
109 anyRewritableTyVar, anyRewritableTyFamApp, anyRewritableCanEqLHS,
110
111 ---------------------------------
112 -- Foreign import and export
113 isFFIArgumentTy, -- :: DynFlags -> Safety -> Type -> Bool
114 isFFIImportResultTy, -- :: DynFlags -> Type -> Bool
115 isFFIExportResultTy, -- :: Type -> Bool
116 isFFIExternalTy, -- :: Type -> Bool
117 isFFIDynTy, -- :: Type -> Type -> Bool
118 isFFIPrimArgumentTy, -- :: DynFlags -> Type -> Bool
119 isFFIPrimResultTy, -- :: DynFlags -> Type -> Bool
120 isFFILabelTy, -- :: Type -> Bool
121 isFFITy, -- :: Type -> Bool
122 isFunPtrTy, -- :: Type -> Bool
123 tcSplitIOType_maybe, -- :: Type -> Maybe Type
124
125 --------------------------------
126 -- Reexported from Kind
127 Kind, tcTypeKind,
128 liftedTypeKind,
129 constraintKind,
130 isLiftedTypeKind, isUnliftedTypeKind, classifiesTypeWithValues,
131
132 --------------------------------
133 -- Reexported from Type
134 Type, PredType, ThetaType, TyCoBinder,
135 ArgFlag(..), AnonArgFlag(..),
136
137 mkForAllTy, mkForAllTys, mkInvisForAllTys, mkTyCoInvForAllTys,
138 mkSpecForAllTys, mkTyCoInvForAllTy,
139 mkInfForAllTy, mkInfForAllTys,
140 mkVisFunTy, mkVisFunTys, mkInvisFunTy, mkInvisFunTyMany,
141 mkVisFunTyMany, mkVisFunTysMany, mkInvisFunTysMany,
142 mkTyConApp, mkAppTy, mkAppTys,
143 mkTyConTy, mkTyVarTy, mkTyVarTys,
144 mkTyCoVarTy, mkTyCoVarTys,
145
146 isClassPred, isEqPrimPred, isIPLikePred, isEqPred, isEqPredClass,
147 mkClassPred,
148 tcSplitDFunTy, tcSplitDFunHead, tcSplitMethodTy,
149 isRuntimeRepVar, isFixedRuntimeRepKind,
150 isVisibleBinder, isInvisibleBinder,
151
152 -- Type substitutions
153 TCvSubst(..), -- Representation visible to a few friends
154 TvSubstEnv, emptyTCvSubst, mkEmptyTCvSubst,
155 zipTvSubst,
156 mkTvSubstPrs, notElemTCvSubst, unionTCvSubst,
157 getTvSubstEnv, setTvSubstEnv, getTCvInScope, extendTCvInScope,
158 extendTCvInScopeList, extendTCvInScopeSet, extendTvSubstAndInScope,
159 Type.lookupTyVar, Type.extendTCvSubst, Type.substTyVarBndr,
160 Type.extendTvSubst,
161 isInScope, mkTCvSubst, mkTvSubst, zipTyEnv, zipCoEnv,
162 Type.substTy, substTys, substScaledTys, substTyWith, substTyWithCoVars,
163 substTyAddInScope,
164 substTyUnchecked, substTysUnchecked, substScaledTyUnchecked,
165 substThetaUnchecked,
166 substTyWithUnchecked,
167 substCoUnchecked, substCoWithUnchecked,
168 substTheta,
169
170 isUnliftedType, -- Source types are always lifted
171 isUnboxedTupleType, -- Ditto
172 isPrimitiveType,
173
174 tcView, coreView,
175
176 tyCoVarsOfType, tyCoVarsOfTypes, closeOverKinds,
177 tyCoFVsOfType, tyCoFVsOfTypes,
178 tyCoVarsOfTypeDSet, tyCoVarsOfTypesDSet, closeOverKindsDSet,
179 tyCoVarsOfTypeList, tyCoVarsOfTypesList,
180 noFreeVarsOfType,
181
182 --------------------------------
183 pprKind, pprParendKind, pprSigmaType,
184 pprType, pprParendType, pprTypeApp,
185 pprTheta, pprParendTheta, pprThetaArrowTy, pprClassPred,
186 pprTCvBndr, pprTCvBndrs,
187
188 TypeSize, sizeType, sizeTypes, scopedSort,
189
190 ---------------------------------
191 -- argument visibility
192 tcTyConVisibilities, isNextTyConArgVisible, isNextArgVisible
193
194 ) where
195
196 -- friends:
197 import GHC.Prelude
198
199 import GHC.Core.TyCo.Rep
200 import GHC.Core.TyCo.Subst ( mkTvSubst, substTyWithCoVars )
201 import GHC.Core.TyCo.FVs
202 import GHC.Core.TyCo.Ppr
203 import GHC.Core.Class
204 import GHC.Types.Var
205 import GHC.Types.ForeignCall
206 import GHC.Types.Var.Set
207 import GHC.Core.Coercion
208 import GHC.Core.Type as Type
209 import GHC.Core.Predicate
210 import GHC.Types.RepType
211 import GHC.Core.TyCon
212
213 -- others:
214 import GHC.Driver.Session
215 import GHC.Core.FVs
216 import GHC.Types.Name as Name
217 -- We use this to make dictionaries for type literals.
218 -- Perhaps there's a better way to do this?
219 import GHC.Types.Name.Set
220 import GHC.Types.Var.Env
221 import GHC.Builtin.Names
222 import GHC.Builtin.Types ( coercibleClass, eqClass, heqClass, unitTyCon, unitTyConKey
223 , listTyCon, constraintKind )
224 import GHC.Types.Basic
225 import GHC.Utils.Misc
226 import GHC.Data.Maybe
227 import GHC.Data.List.SetOps ( getNth, findDupsEq )
228 import GHC.Utils.Outputable
229 import GHC.Utils.Panic
230 import GHC.Utils.Panic.Plain
231 import GHC.Utils.Error( Validity'(..), Validity, isValid )
232 import qualified GHC.LanguageExtensions as LangExt
233
234 import Data.List ( mapAccumL )
235 -- import Data.Functor.Identity( Identity(..) )
236 import Data.IORef
237 import Data.List.NonEmpty( NonEmpty(..) )
238
239 {-
240 ************************************************************************
241 * *
242 Types
243 * *
244 ************************************************************************
245
246 The type checker divides the generic Type world into the
247 following more structured beasts:
248
249 sigma ::= forall tyvars. phi
250 -- A sigma type is a qualified type
251 --
252 -- Note that even if 'tyvars' is empty, theta
253 -- may not be: e.g. (?x::Int) => Int
254
255 -- Note that 'sigma' is in prenex form:
256 -- all the foralls are at the front.
257 -- A 'phi' type has no foralls to the right of
258 -- an arrow
259
260 phi :: theta => rho
261
262 rho ::= sigma -> rho
263 | tau
264
265 -- A 'tau' type has no quantification anywhere
266 -- Note that the args of a type constructor must be taus
267 tau ::= tyvar
268 | tycon tau_1 .. tau_n
269 | tau_1 tau_2
270 | tau_1 -> tau_2
271
272 -- In all cases, a (saturated) type synonym application is legal,
273 -- provided it expands to the required form.
274
275 Note [TcTyVars and TyVars in the typechecker]
276 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
277 The typechecker uses a lot of type variables with special properties,
278 notably being a unification variable with a mutable reference. These
279 use the 'TcTyVar' variant of Var.Var.
280
281 Note, though, that a /bound/ type variable can (and probably should)
282 be a TyVar. E.g
283 forall a. a -> a
284 Here 'a' is really just a deBruijn-number; it certainly does not have
285 a significant TcLevel (as every TcTyVar does). So a forall-bound type
286 variable should be TyVars; and hence a TyVar can appear free in a TcType.
287
288 The type checker and constraint solver can also encounter /free/ type
289 variables that use the 'TyVar' variant of Var.Var, for a couple of
290 reasons:
291
292 - When typechecking a class decl, say
293 class C (a :: k) where
294 foo :: T a -> Int
295 We have first kind-check the header; fix k and (a:k) to be
296 TyVars, bring 'k' and 'a' into scope, and kind check the
297 signature for 'foo'. In doing so we call solveEqualities to
298 solve any kind equalities in foo's signature. So the solver
299 may see free occurrences of 'k'.
300
301 See calls to tcExtendTyVarEnv for other places that ordinary
302 TyVars are bought into scope, and hence may show up in the types
303 and kinds generated by GHC.Tc.Gen.HsType.
304
305 - The pattern-match overlap checker calls the constraint solver,
306 long after TcTyVars have been zonked away
307
308 It's convenient to simply treat these TyVars as skolem constants,
309 which of course they are. We give them a level number of "outermost",
310 so they behave as global constants. Specifically:
311
312 * Var.tcTyVarDetails succeeds on a TyVar, returning
313 vanillaSkolemTv, as well as on a TcTyVar.
314
315 * tcIsTcTyVar returns True for both TyVar and TcTyVar variants
316 of Var.Var. The "tc" prefix means "a type variable that can be
317 encountered by the typechecker".
318
319 This is a bit of a change from an earlier era when we remoselessly
320 insisted on real TcTyVars in the type checker. But that seems
321 unnecessary (for skolems, TyVars are fine) and it's now very hard
322 to guarantee, with the advent of kind equalities.
323
324 Note [Coercion variables in free variable lists]
325 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
326 There are several places in the GHC codebase where functions like
327 tyCoVarsOfType, tyCoVarsOfCt, et al. are used to compute the free type
328 variables of a type. The "Co" part of these functions' names shouldn't be
329 dismissed, as it is entirely possible that they will include coercion variables
330 in addition to type variables! As a result, there are some places in GHC.Tc.Utils.TcType
331 where we must take care to check that a variable is a _type_ variable (using
332 isTyVar) before calling tcTyVarDetails--a partial function that is not defined
333 for coercion variables--on the variable. Failing to do so led to
334 GHC #12785.
335 -}
336
337 -- See Note [TcTyVars and TyVars in the typechecker]
338 type TcCoVar = CoVar -- Used only during type inference
339 type TcType = Type -- A TcType can have mutable type variables
340 type TcTyCoVar = Var -- Either a TcTyVar or a CoVar
341
342 type TcTyVarBinder = TyVarBinder
343 type TcInvisTVBinder = InvisTVBinder
344 type TcReqTVBinder = ReqTVBinder
345 type TcTyCon = TyCon -- these can be the TcTyCon constructor
346
347 -- These types do not have boxy type variables in them
348 type TcPredType = PredType
349 type TcThetaType = ThetaType
350 type TcSigmaType = TcType
351 type TcRhoType = TcType -- Note [TcRhoType]
352 type TcTauType = TcType
353 type TcKind = Kind
354 type TcTyVarSet = TyVarSet
355 type TcTyCoVarSet = TyCoVarSet
356 type TcDTyVarSet = DTyVarSet
357 type TcDTyCoVarSet = DTyCoVarSet
358
359 {- *********************************************************************
360 * *
361 ExpType: an "expected type" in the type checker
362 * *
363 ********************************************************************* -}
364
365 -- | An expected type to check against during type-checking.
366 -- See Note [ExpType] in "GHC.Tc.Utils.TcMType", where you'll also find manipulators.
367 data ExpType = Check TcType
368 | Infer !InferResult
369
370 data InferResult
371 = IR { ir_uniq :: Unique -- For debugging only
372
373 , ir_lvl :: TcLevel -- See Note [TcLevel of ExpType] in GHC.Tc.Utils.TcMType
374
375 , ir_ref :: IORef (Maybe TcType) }
376 -- The type that fills in this hole should be a Type,
377 -- that is, its kind should be (TYPE rr) for some rr
378
379 type ExpSigmaType = ExpType
380 type ExpRhoType = ExpType
381
382 instance Outputable ExpType where
383 ppr (Check ty) = text "Check" <> braces (ppr ty)
384 ppr (Infer ir) = ppr ir
385
386 instance Outputable InferResult where
387 ppr (IR { ir_uniq = u, ir_lvl = lvl })
388 = text "Infer" <> braces (ppr u <> comma <> ppr lvl)
389
390 -- | Make an 'ExpType' suitable for checking.
391 mkCheckExpType :: TcType -> ExpType
392 mkCheckExpType = Check
393
394
395 {- *********************************************************************
396 * *
397 SyntaxOpType
398 * *
399 ********************************************************************* -}
400
401 -- | What to expect for an argument to a rebindable-syntax operator.
402 -- Quite like 'Type', but allows for holes to be filled in by tcSyntaxOp.
403 -- The callback called from tcSyntaxOp gets a list of types; the meaning
404 -- of these types is determined by a left-to-right depth-first traversal
405 -- of the 'SyntaxOpType' tree. So if you pass in
406 --
407 -- > SynAny `SynFun` (SynList `SynFun` SynType Int) `SynFun` SynAny
408 --
409 -- you'll get three types back: one for the first 'SynAny', the /element/
410 -- type of the list, and one for the last 'SynAny'. You don't get anything
411 -- for the 'SynType', because you've said positively that it should be an
412 -- Int, and so it shall be.
413 --
414 -- You'll also get three multiplicities back: one for each function arrow. See
415 -- also Note [Linear types] in Multiplicity.
416 --
417 -- This is defined here to avoid defining it in "GHC.Tc.Gen.Expr" boot file.
418 data SyntaxOpType
419 = SynAny -- ^ Any type
420 | SynRho -- ^ A rho type, skolemised or instantiated as appropriate
421 | SynList -- ^ A list type. You get back the element type of the list
422 | SynFun SyntaxOpType SyntaxOpType
423 -- ^ A function.
424 | SynType ExpType -- ^ A known type.
425 infixr 0 `SynFun`
426
427 -- | Like 'SynType' but accepts a regular TcType
428 synKnownType :: TcType -> SyntaxOpType
429 synKnownType = SynType . mkCheckExpType
430
431 -- | Like 'mkFunTys' but for 'SyntaxOpType'
432 mkSynFunTys :: [SyntaxOpType] -> ExpType -> SyntaxOpType
433 mkSynFunTys arg_tys res_ty = foldr SynFun (SynType res_ty) arg_tys
434
435
436 {-
437 Note [TcRhoType]
438 ~~~~~~~~~~~~~~~~
439 A TcRhoType has no foralls or contexts at the top
440 NO forall a. a -> Int
441 NO Eq a => a -> a
442 YES a -> a
443 YES (forall a. a->a) -> Int
444 YES Int -> forall a. a -> Int
445
446
447 ************************************************************************
448 * *
449 TyVarDetails, MetaDetails, MetaInfo
450 * *
451 ************************************************************************
452
453 TyVarDetails gives extra info about type variables, used during type
454 checking. It's attached to mutable type variables only.
455 It's knot-tied back to "GHC.Types.Var". There is no reason in principle
456 why "GHC.Types.Var" shouldn't actually have the definition, but it "belongs" here.
457
458 Note [TyVars and TcTyVars during type checking]
459 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
460 The Var type has constructors TyVar and TcTyVar. They are used
461 as follows:
462
463 * TcTyVar: used /only/ during type checking. Should never appear
464 afterwards. May contain a mutable field, in the MetaTv case.
465
466 * TyVar: is never seen by the constraint solver, except locally
467 inside a type like (forall a. [a] ->[a]), where 'a' is a TyVar.
468 We instantiate these with TcTyVars before exposing the type
469 to the constraint solver.
470
471 I have swithered about the latter invariant, excluding TyVars from the
472 constraint solver. It's not strictly essential, and indeed
473 (historically but still there) Var.tcTyVarDetails returns
474 vanillaSkolemTv for a TyVar.
475
476 But ultimately I want to seeparate Type from TcType, and in that case
477 we would need to enforce the separation.
478 -}
479
480 -- A TyVarDetails is inside a TyVar
481 -- See Note [TyVars and TcTyVars]
482 data TcTyVarDetails
483 = SkolemTv -- A skolem
484 TcLevel -- Level of the implication that binds it
485 -- See GHC.Tc.Utils.Unify Note [Deeper level on the left] for
486 -- how this level number is used
487 Bool -- True <=> this skolem type variable can be overlapped
488 -- when looking up instances
489 -- See Note [Binding when looking up instances] in GHC.Core.InstEnv
490
491 | RuntimeUnk -- Stands for an as-yet-unknown type in the GHCi
492 -- interactive context
493
494 | MetaTv { mtv_info :: MetaInfo
495 , mtv_ref :: IORef MetaDetails
496 , mtv_tclvl :: TcLevel } -- See Note [TcLevel invariants]
497
498 vanillaSkolemTv, superSkolemTv :: TcTyVarDetails
499 -- See Note [Binding when looking up instances] in GHC.Core.InstEnv
500 vanillaSkolemTv = SkolemTv topTcLevel False -- Might be instantiated
501 superSkolemTv = SkolemTv topTcLevel True -- Treat this as a completely distinct type
502 -- The choice of level number here is a bit dodgy, but
503 -- topTcLevel works in the places that vanillaSkolemTv is used
504
505 instance Outputable TcTyVarDetails where
506 ppr = pprTcTyVarDetails
507
508 pprTcTyVarDetails :: TcTyVarDetails -> SDoc
509 -- For debugging
510 pprTcTyVarDetails (RuntimeUnk {}) = text "rt"
511 pprTcTyVarDetails (SkolemTv lvl True) = text "ssk" <> colon <> ppr lvl
512 pprTcTyVarDetails (SkolemTv lvl False) = text "sk" <> colon <> ppr lvl
513 pprTcTyVarDetails (MetaTv { mtv_info = info, mtv_tclvl = tclvl })
514 = ppr info <> colon <> ppr tclvl
515
516 -----------------------------
517 data MetaDetails
518 = Flexi -- Flexi type variables unify to become Indirects
519 | Indirect TcType
520
521 data MetaInfo
522 = TauTv -- This MetaTv is an ordinary unification variable
523 -- A TauTv is always filled in with a tau-type, which
524 -- never contains any ForAlls.
525
526 | TyVarTv -- A variant of TauTv, except that it should not be
527 -- unified with a type, only with a type variable
528 -- See Note [TyVarTv] in GHC.Tc.Utils.TcMType
529
530 | RuntimeUnkTv -- A unification variable used in the GHCi debugger.
531 -- It /is/ allowed to unify with a polytype, unlike TauTv
532
533 | CycleBreakerTv -- Used to fix occurs-check problems in Givens
534 -- See Note [Type variable cycles] in
535 -- GHC.Tc.Solver.Canonical
536
537 instance Outputable MetaDetails where
538 ppr Flexi = text "Flexi"
539 ppr (Indirect ty) = text "Indirect" <+> ppr ty
540
541 instance Outputable MetaInfo where
542 ppr TauTv = text "tau"
543 ppr TyVarTv = text "tyv"
544 ppr RuntimeUnkTv = text "rutv"
545 ppr CycleBreakerTv = text "cbv"
546
547 {- *********************************************************************
548 * *
549 Untouchable type variables
550 * *
551 ********************************************************************* -}
552
553 newtype TcLevel = TcLevel Int deriving( Eq, Ord )
554 -- See Note [TcLevel invariants] for what this Int is
555 -- See also Note [TcLevel assignment]
556
557 {-
558 Note [TcLevel invariants]
559 ~~~~~~~~~~~~~~~~~~~~~~~~~
560 * Each unification variable (MetaTv)
561 and skolem (SkolemTv)
562 and each Implication
563 has a level number (of type TcLevel)
564
565 * INVARIANTS. In a tree of Implications,
566
567 (ImplicInv) The level number (ic_tclvl) of an Implication is
568 STRICTLY GREATER THAN that of its parent
569
570 (SkolInv) The level number of the skolems (ic_skols) of an
571 Implication is equal to the level of the implication
572 itself (ic_tclvl)
573
574 (GivenInv) The level number of a unification variable appearing
575 in the 'ic_given' of an implication I should be
576 STRICTLY LESS THAN the ic_tclvl of I
577 See Note [GivenInv]
578
579 (WantedInv) The level number of a unification variable appearing
580 in the 'ic_wanted' of an implication I should be
581 LESS THAN OR EQUAL TO the ic_tclvl of I
582 See Note [WantedInv]
583
584 The level of a MetaTyVar also governs its untouchability. See
585 Note [Unification preconditions] in GHC.Tc.Utils.Unify.
586
587 Note [TcLevel assignment]
588 ~~~~~~~~~~~~~~~~~~~~~~~~~
589 We arrange the TcLevels like this
590
591 0 Top level
592 1 First-level implication constraints
593 2 Second-level implication constraints
594 ...etc...
595
596 Note [GivenInv]
597 ~~~~~~~~~~~~~~~
598 Invariant (GivenInv) is not essential, but it is easy to guarantee, and
599 it is a useful extra piece of structure. It ensures that the Givens of
600 an implication don't change because of unifications /at the same level/
601 caused by Wanteds. (Wanteds can also cause unifications at an outer
602 level, but that will iterate the entire implication; see GHC.Tc.Solver.Monad
603 Note [The Unification Level Flag].)
604
605 Givens can certainly contain meta-tyvars from /outer/ levels. E.g.
606 data T a where
607 MkT :: Eq a => a -> MkT a
608
609 f x = case x of MkT y -> y && True
610
611 Then we'll infer (x :: T alpha[1]). The Givens from the implication
612 arising from the pattern match will look like this:
613
614 forall[2] . Eq alpha[1] => (alpha[1] ~ Bool)
615
616 But if we unify alpha (which in this case we will), we'll iterate
617 the entire implication via Note [The Unification Level Flag] in
618 GHC.Tc.Solver.Monad. That isn't true of unifications at the /ambient/
619 level.
620
621 It would be entirely possible to weaken (GivenInv), to LESS THAN OR
622 EQUAL TO, but we'd need to think carefully about
623 - kick-out for Givens
624 - GHC.Tc.Solver.Monad.isOuterTyVar
625 But in fact (GivenInv) is automatically true, so we're adhering to
626 it for now. See #18929.
627
628 * If a tyvar tv has level n, then the levels of all variables free
629 in tv's kind are <= n. Consequence: if tv is untouchable, so are
630 all variables in tv's kind.
631
632 Note [WantedInv]
633 ~~~~~~~~~~~~~~~~
634 Why is WantedInv important? Consider this implication, where
635 the constraint (C alpha[3]) disobeys WantedInv:
636
637 forall[2] a. blah => (C alpha[3])
638 (forall[3] b. alpha[3] ~ b)
639
640 We can unify alpha:=b in the inner implication, because 'alpha' is
641 touchable; but then 'b' has excaped its scope into the outer implication.
642 -}
643
644 maxTcLevel :: TcLevel -> TcLevel -> TcLevel
645 maxTcLevel (TcLevel a) (TcLevel b) = TcLevel (a `max` b)
646
647 topTcLevel :: TcLevel
648 -- See Note [TcLevel assignment]
649 topTcLevel = TcLevel 0 -- 0 = outermost level
650
651 isTopTcLevel :: TcLevel -> Bool
652 isTopTcLevel (TcLevel 0) = True
653 isTopTcLevel _ = False
654
655 pushTcLevel :: TcLevel -> TcLevel
656 -- See Note [TcLevel assignment]
657 pushTcLevel (TcLevel us) = TcLevel (us + 1)
658
659 strictlyDeeperThan :: TcLevel -> TcLevel -> Bool
660 strictlyDeeperThan (TcLevel tv_tclvl) (TcLevel ctxt_tclvl)
661 = tv_tclvl > ctxt_tclvl
662
663 deeperThanOrSame :: TcLevel -> TcLevel -> Bool
664 deeperThanOrSame (TcLevel tv_tclvl) (TcLevel ctxt_tclvl)
665 = tv_tclvl >= ctxt_tclvl
666
667 sameDepthAs :: TcLevel -> TcLevel -> Bool
668 sameDepthAs (TcLevel ctxt_tclvl) (TcLevel tv_tclvl)
669 = ctxt_tclvl == tv_tclvl -- NB: invariant ctxt_tclvl >= tv_tclvl
670 -- So <= would be equivalent
671
672 checkTcLevelInvariant :: TcLevel -> TcLevel -> Bool
673 -- Checks (WantedInv) from Note [TcLevel invariants]
674 checkTcLevelInvariant (TcLevel ctxt_tclvl) (TcLevel tv_tclvl)
675 = ctxt_tclvl >= tv_tclvl
676
677 -- Returns topTcLevel for non-TcTyVars
678 tcTyVarLevel :: TcTyVar -> TcLevel
679 tcTyVarLevel tv
680 = case tcTyVarDetails tv of
681 MetaTv { mtv_tclvl = tv_lvl } -> tv_lvl
682 SkolemTv tv_lvl _ -> tv_lvl
683 RuntimeUnk -> topTcLevel
684
685
686 tcTypeLevel :: TcType -> TcLevel
687 -- Max level of any free var of the type
688 tcTypeLevel ty
689 = nonDetStrictFoldDVarSet add topTcLevel (tyCoVarsOfTypeDSet ty)
690 -- It's safe to use a non-deterministic fold because `maxTcLevel` is
691 -- commutative.
692 where
693 add v lvl
694 | isTcTyVar v = lvl `maxTcLevel` tcTyVarLevel v
695 | otherwise = lvl
696
697 instance Outputable TcLevel where
698 ppr (TcLevel us) = ppr us
699
700 promoteSkolem :: TcLevel -> TcTyVar -> TcTyVar
701 promoteSkolem tclvl skol
702 | tclvl < tcTyVarLevel skol
703 = assert (isTcTyVar skol && isSkolemTyVar skol )
704 setTcTyVarDetails skol (SkolemTv tclvl (isOverlappableTyVar skol))
705
706 | otherwise
707 = skol
708
709 -- | Change the TcLevel in a skolem, extending a substitution
710 promoteSkolemX :: TcLevel -> TCvSubst -> TcTyVar -> (TCvSubst, TcTyVar)
711 promoteSkolemX tclvl subst skol
712 = assert (isTcTyVar skol && isSkolemTyVar skol )
713 (new_subst, new_skol)
714 where
715 new_skol
716 | tclvl < tcTyVarLevel skol
717 = setTcTyVarDetails (updateTyVarKind (substTy subst) skol)
718 (SkolemTv tclvl (isOverlappableTyVar skol))
719 | otherwise
720 = updateTyVarKind (substTy subst) skol
721 new_subst = extendTvSubstWithClone subst skol new_skol
722
723 promoteSkolemsX :: TcLevel -> TCvSubst -> [TcTyVar] -> (TCvSubst, [TcTyVar])
724 promoteSkolemsX tclvl = mapAccumL (promoteSkolemX tclvl)
725
726 {- *********************************************************************
727 * *
728 Finding type family instances
729 * *
730 ************************************************************************
731 -}
732
733 -- | Finds outermost type-family applications occurring in a type,
734 -- after expanding synonyms. In the list (F, tys) that is returned
735 -- we guarantee that tys matches F's arity. For example, given
736 -- type family F a :: * -> * (arity 1)
737 -- calling tcTyFamInsts on (Maybe (F Int Bool) will return
738 -- (F, [Int]), not (F, [Int,Bool])
739 --
740 -- This is important for its use in deciding termination of type
741 -- instances (see #11581). E.g.
742 -- type instance G [Int] = ...(F Int \<big type>)...
743 -- we don't need to take \<big type> into account when asking if
744 -- the calls on the RHS are smaller than the LHS
745 tcTyFamInsts :: Type -> [(TyCon, [Type])]
746 tcTyFamInsts = map (\(_,b,c) -> (b,c)) . tcTyFamInstsAndVis
747
748 -- | Like 'tcTyFamInsts', except that the output records whether the
749 -- type family and its arguments occur as an /invisible/ argument in
750 -- some type application. This information is useful because it helps GHC know
751 -- when to turn on @-fprint-explicit-kinds@ during error reporting so that
752 -- users can actually see the type family being mentioned.
753 --
754 -- As an example, consider:
755 --
756 -- @
757 -- class C a
758 -- data T (a :: k)
759 -- type family F a :: k
760 -- instance C (T @(F Int) (F Bool))
761 -- @
762 --
763 -- There are two occurrences of the type family `F` in that `C` instance, so
764 -- @'tcTyFamInstsAndVis' (C (T \@(F Int) (F Bool)))@ will return:
765 --
766 -- @
767 -- [ ('True', F, [Int])
768 -- , ('False', F, [Bool]) ]
769 -- @
770 --
771 -- @F Int@ is paired with 'True' since it appears as an /invisible/ argument
772 -- to @C@, whereas @F Bool@ is paired with 'False' since it appears an a
773 -- /visible/ argument to @C@.
774 --
775 -- See also @Note [Kind arguments in error messages]@ in "GHC.Tc.Errors".
776 tcTyFamInstsAndVis :: Type -> [(Bool, TyCon, [Type])]
777 tcTyFamInstsAndVis = tcTyFamInstsAndVisX False
778
779 tcTyFamInstsAndVisX
780 :: Bool -- ^ Is this an invisible argument to some type application?
781 -> Type -> [(Bool, TyCon, [Type])]
782 tcTyFamInstsAndVisX = go
783 where
784 go is_invis_arg ty
785 | Just exp_ty <- tcView ty = go is_invis_arg exp_ty
786 go _ (TyVarTy _) = []
787 go is_invis_arg (TyConApp tc tys)
788 | isTypeFamilyTyCon tc
789 = [(is_invis_arg, tc, take (tyConArity tc) tys)]
790 | otherwise
791 = tcTyConAppTyFamInstsAndVisX is_invis_arg tc tys
792 go _ (LitTy {}) = []
793 go is_invis_arg (ForAllTy bndr ty) = go is_invis_arg (binderType bndr)
794 ++ go is_invis_arg ty
795 go is_invis_arg (FunTy _ w ty1 ty2) = go is_invis_arg w
796 ++ go is_invis_arg ty1
797 ++ go is_invis_arg ty2
798 go is_invis_arg ty@(AppTy _ _) =
799 let (ty_head, ty_args) = splitAppTys ty
800 ty_arg_flags = appTyArgFlags ty_head ty_args
801 in go is_invis_arg ty_head
802 ++ concat (zipWith (\flag -> go (isInvisibleArgFlag flag))
803 ty_arg_flags ty_args)
804 go is_invis_arg (CastTy ty _) = go is_invis_arg ty
805 go _ (CoercionTy _) = [] -- don't count tyfams in coercions,
806 -- as they never get normalized,
807 -- anyway
808
809 -- | In an application of a 'TyCon' to some arguments, find the outermost
810 -- occurrences of type family applications within the arguments. This function
811 -- will not consider the 'TyCon' itself when checking for type family
812 -- applications.
813 --
814 -- See 'tcTyFamInstsAndVis' for more details on how this works (as this
815 -- function is called inside of 'tcTyFamInstsAndVis').
816 tcTyConAppTyFamInstsAndVis :: TyCon -> [Type] -> [(Bool, TyCon, [Type])]
817 tcTyConAppTyFamInstsAndVis = tcTyConAppTyFamInstsAndVisX False
818
819 tcTyConAppTyFamInstsAndVisX
820 :: Bool -- ^ Is this an invisible argument to some type application?
821 -> TyCon -> [Type] -> [(Bool, TyCon, [Type])]
822 tcTyConAppTyFamInstsAndVisX is_invis_arg tc tys =
823 let (invis_tys, vis_tys) = partitionInvisibleTypes tc tys
824 in concat $ map (tcTyFamInstsAndVisX True) invis_tys
825 ++ map (tcTyFamInstsAndVisX is_invis_arg) vis_tys
826
827 isTyFamFree :: Type -> Bool
828 -- ^ Check that a type does not contain any type family applications.
829 isTyFamFree = null . tcTyFamInsts
830
831 any_rewritable :: Bool -- Ignore casts and coercions
832 -> EqRel -- Ambient role
833 -> (EqRel -> TcTyVar -> Bool) -- check tyvar
834 -> (EqRel -> TyCon -> [TcType] -> Bool) -- check type family
835 -> (TyCon -> Bool) -- expand type synonym?
836 -> TcType -> Bool
837 -- Checks every tyvar and tyconapp (not including FunTys) within a type,
838 -- ORing the results of the predicates above together
839 -- Do not look inside casts and coercions if 'ignore_cos' is True
840 -- See Note [anyRewritableTyVar must be role-aware]
841 --
842 -- This looks like it should use foldTyCo, but that function is
843 -- role-agnostic, and this one must be role-aware. We could make
844 -- foldTyCon role-aware, but that may slow down more common usages.
845 --
846 -- See Note [Rewritable] in GHC.Tc.Solver.InertSet for a specification for this function.
847 {-# INLINE any_rewritable #-} -- this allows specialization of predicates
848 any_rewritable ignore_cos role tv_pred tc_pred should_expand
849 = go role emptyVarSet
850 where
851 go_tv rl bvs tv | tv `elemVarSet` bvs = False
852 | otherwise = tv_pred rl tv
853
854 go rl bvs ty@(TyConApp tc tys)
855 | isTypeSynonymTyCon tc
856 , should_expand tc
857 , Just ty' <- tcView ty -- should always match
858 = go rl bvs ty'
859
860 | tc_pred rl tc tys
861 = True
862
863 | otherwise
864 = go_tc rl bvs tc tys
865
866 go rl bvs (TyVarTy tv) = go_tv rl bvs tv
867 go _ _ (LitTy {}) = False
868 go rl bvs (AppTy fun arg) = go rl bvs fun || go NomEq bvs arg
869 go rl bvs (FunTy _ w arg res) = go NomEq bvs arg_rep || go NomEq bvs res_rep ||
870 go rl bvs arg || go rl bvs res || go NomEq bvs w
871 where arg_rep = getRuntimeRep arg -- forgetting these causes #17024
872 res_rep = getRuntimeRep res
873 go rl bvs (ForAllTy tv ty) = go rl (bvs `extendVarSet` binderVar tv) ty
874 go rl bvs (CastTy ty co) = go rl bvs ty || go_co rl bvs co
875 go rl bvs (CoercionTy co) = go_co rl bvs co -- ToDo: check
876
877 go_tc NomEq bvs _ tys = any (go NomEq bvs) tys
878 go_tc ReprEq bvs tc tys = any (go_arg bvs)
879 (tyConRolesRepresentational tc `zip` tys)
880
881 go_arg bvs (Nominal, ty) = go NomEq bvs ty
882 go_arg bvs (Representational, ty) = go ReprEq bvs ty
883 go_arg _ (Phantom, _) = False -- We never rewrite with phantoms
884
885 go_co rl bvs co
886 | ignore_cos = False
887 | otherwise = anyVarSet (go_tv rl bvs) (tyCoVarsOfCo co)
888 -- We don't have an equivalent of anyRewritableTyVar for coercions
889 -- (at least not yet) so take the free vars and test them
890
891 anyRewritableTyVar :: Bool -- Ignore casts and coercions
892 -> EqRel -- Ambient role
893 -> (EqRel -> TcTyVar -> Bool) -- check tyvar
894 -> TcType -> Bool
895 -- See Note [Rewritable] in GHC.Tc.Solver.InertSet for a specification for this function.
896 anyRewritableTyVar ignore_cos role pred
897 = any_rewritable ignore_cos role pred
898 (\ _ _ _ -> False) -- no special check for tyconapps
899 -- (this False is ORed with other results, so it
900 -- really means "do nothing special"; the arguments
901 -- are still inspected)
902 (\ _ -> False) -- don't expand synonyms
903 -- NB: No need to expand synonyms, because we can find
904 -- all free variables of a synonym by looking at its
905 -- arguments
906
907 anyRewritableTyFamApp :: EqRel -- Ambient role
908 -> (EqRel -> TyCon -> [TcType] -> Bool) -- check tyconapp
909 -- should return True only for type family applications
910 -> TcType -> Bool
911 -- always ignores casts & coercions
912 -- See Note [Rewritable] in GHC.Tc.Solver.InertSet for a specification for this function.
913 anyRewritableTyFamApp role check_tyconapp
914 = any_rewritable True role (\ _ _ -> False) check_tyconapp (not . isFamFreeTyCon)
915
916 -- This version is used by shouldSplitWD. It *does* look in casts
917 -- and coercions, and it always expands type synonyms whose RHSs mention
918 -- type families.
919 -- See Note [Rewritable] in GHC.Tc.Solver.InertSet for a specification for this function.
920 anyRewritableCanEqLHS :: EqRel -- Ambient role
921 -> (EqRel -> TcTyVar -> Bool) -- check tyvar
922 -> (EqRel -> TyCon -> [TcType] -> Bool) -- check type family
923 -> TcType -> Bool
924 anyRewritableCanEqLHS role check_tyvar check_tyconapp
925 = any_rewritable False role check_tyvar check_tyconapp (not . isFamFreeTyCon)
926
927 {- Note [anyRewritableTyVar must be role-aware]
928 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
929 anyRewritableTyVar is used during kick-out from the inert set,
930 to decide if, given a new equality (a ~ ty), we should kick out
931 a constraint C. Rather than gather free variables and see if 'a'
932 is among them, we instead pass in a predicate; this is just efficiency.
933
934 Moreover, consider
935 work item: [G] a ~R f b
936 inert item: [G] b ~R f a
937 We use anyRewritableTyVar to decide whether to kick out the inert item,
938 on the grounds that the work item might rewrite it. Well, 'a' is certainly
939 free in [G] b ~R f a. But because the role of a type variable ('f' in
940 this case) is nominal, the work item can't actually rewrite the inert item.
941 Moreover, if we were to kick out the inert item the exact same situation
942 would re-occur and we end up with an infinite loop in which each kicks
943 out the other (#14363).
944
945 -}
946
947 {- *********************************************************************
948 * *
949 The "exact" free variables of a type
950 * *
951 ********************************************************************* -}
952
953 {- Note [Silly type synonym]
954 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
955 Consider
956 type T a = Int
957 What are the free tyvars of (T x)? Empty, of course!
958
959 exactTyCoVarsOfType is used by the type checker to figure out exactly
960 which type variables are mentioned in a type. It only matters
961 occasionally -- see the calls to exactTyCoVarsOfType.
962
963 We place this function here in GHC.Tc.Utils.TcType, not in GHC.Core.TyCo.FVs,
964 because we want to "see" tcView (efficiency issue only).
965 -}
966
967 exactTyCoVarsOfType :: Type -> TyCoVarSet
968 exactTyCoVarsOfTypes :: [Type] -> TyCoVarSet
969 -- Find the free type variables (of any kind)
970 -- but *expand* type synonyms. See Note [Silly type synonym] above.
971
972 exactTyCoVarsOfType ty = runTyCoVars (exact_ty ty)
973 exactTyCoVarsOfTypes tys = runTyCoVars (exact_tys tys)
974
975 exact_ty :: Type -> Endo TyCoVarSet
976 exact_tys :: [Type] -> Endo TyCoVarSet
977 (exact_ty, exact_tys, _, _) = foldTyCo exactTcvFolder emptyVarSet
978
979 exactTcvFolder :: TyCoFolder TyCoVarSet (Endo TyCoVarSet)
980 exactTcvFolder = deepTcvFolder { tcf_view = tcView }
981 -- This is the key line
982
983 {-
984 ************************************************************************
985 * *
986 Predicates
987 * *
988 ************************************************************************
989 -}
990
991 tcIsTcTyVar :: TcTyVar -> Bool
992 -- See Note [TcTyVars and TyVars in the typechecker]
993 tcIsTcTyVar tv = isTyVar tv
994
995 isPromotableMetaTyVar :: TcTyVar -> Bool
996 -- True is this is a meta-tyvar that can be
997 -- promoted to an outer level
998 isPromotableMetaTyVar tv
999 | isTyVar tv -- See Note [Coercion variables in free variable lists]
1000 , MetaTv { mtv_info = info } <- tcTyVarDetails tv
1001 = isTouchableInfo info -- Can't promote cycle breakers
1002 | otherwise
1003 = False
1004
1005 isTouchableMetaTyVar :: TcLevel -> TcTyVar -> Bool
1006 isTouchableMetaTyVar ctxt_tclvl tv
1007 | isTyVar tv -- See Note [Coercion variables in free variable lists]
1008 , MetaTv { mtv_tclvl = tv_tclvl, mtv_info = info } <- tcTyVarDetails tv
1009 , isTouchableInfo info
1010 = assertPpr (checkTcLevelInvariant ctxt_tclvl tv_tclvl)
1011 (ppr tv $$ ppr tv_tclvl $$ ppr ctxt_tclvl) $
1012 tv_tclvl `sameDepthAs` ctxt_tclvl
1013
1014 | otherwise = False
1015
1016 isImmutableTyVar :: TyVar -> Bool
1017 isImmutableTyVar tv = isSkolemTyVar tv
1018
1019 isTyConableTyVar, isSkolemTyVar, isOverlappableTyVar,
1020 isMetaTyVar, isAmbiguousTyVar, isCycleBreakerTyVar :: TcTyVar -> Bool
1021
1022 isTyConableTyVar tv
1023 -- True of a meta-type variable that can be filled in
1024 -- with a type constructor application; in particular,
1025 -- not a TyVarTv
1026 | isTyVar tv -- See Note [Coercion variables in free variable lists]
1027 = case tcTyVarDetails tv of
1028 MetaTv { mtv_info = TyVarTv } -> False
1029 _ -> True
1030 | otherwise = True
1031
1032 isSkolemTyVar tv
1033 = assertPpr (tcIsTcTyVar tv) (ppr tv) $
1034 case tcTyVarDetails tv of
1035 MetaTv {} -> False
1036 _other -> True
1037
1038 isOverlappableTyVar tv
1039 | isTyVar tv -- See Note [Coercion variables in free variable lists]
1040 = case tcTyVarDetails tv of
1041 SkolemTv _ overlappable -> overlappable
1042 _ -> False
1043 | otherwise = False
1044
1045 isMetaTyVar tv
1046 | isTyVar tv -- See Note [Coercion variables in free variable lists]
1047 = case tcTyVarDetails tv of
1048 MetaTv {} -> True
1049 _ -> False
1050 | otherwise = False
1051
1052 -- isAmbiguousTyVar is used only when reporting type errors
1053 -- It picks out variables that are unbound, namely meta
1054 -- type variables and the RuntimUnk variables created by
1055 -- GHC.Runtime.Heap.Inspect.zonkRTTIType. These are "ambiguous" in
1056 -- the sense that they stand for an as-yet-unknown type
1057 isAmbiguousTyVar tv
1058 | isTyVar tv -- See Note [Coercion variables in free variable lists]
1059 = case tcTyVarDetails tv of
1060 MetaTv {} -> True
1061 RuntimeUnk {} -> True
1062 _ -> False
1063 | otherwise = False
1064
1065 isCycleBreakerTyVar tv
1066 | isTyVar tv -- See Note [Coercion variables in free variable lists]
1067 , MetaTv { mtv_info = CycleBreakerTv } <- tcTyVarDetails tv
1068 = True
1069
1070 | otherwise
1071 = False
1072
1073 isMetaTyVarTy :: TcType -> Bool
1074 isMetaTyVarTy (TyVarTy tv) = isMetaTyVar tv
1075 isMetaTyVarTy _ = False
1076
1077 metaTyVarInfo :: TcTyVar -> MetaInfo
1078 metaTyVarInfo tv
1079 = case tcTyVarDetails tv of
1080 MetaTv { mtv_info = info } -> info
1081 _ -> pprPanic "metaTyVarInfo" (ppr tv)
1082
1083 isTouchableInfo :: MetaInfo -> Bool
1084 isTouchableInfo info
1085 | CycleBreakerTv <- info = False
1086 | otherwise = True
1087
1088 metaTyVarTcLevel :: TcTyVar -> TcLevel
1089 metaTyVarTcLevel tv
1090 = case tcTyVarDetails tv of
1091 MetaTv { mtv_tclvl = tclvl } -> tclvl
1092 _ -> pprPanic "metaTyVarTcLevel" (ppr tv)
1093
1094 metaTyVarTcLevel_maybe :: TcTyVar -> Maybe TcLevel
1095 metaTyVarTcLevel_maybe tv
1096 = case tcTyVarDetails tv of
1097 MetaTv { mtv_tclvl = tclvl } -> Just tclvl
1098 _ -> Nothing
1099
1100 metaTyVarRef :: TyVar -> IORef MetaDetails
1101 metaTyVarRef tv
1102 = case tcTyVarDetails tv of
1103 MetaTv { mtv_ref = ref } -> ref
1104 _ -> pprPanic "metaTyVarRef" (ppr tv)
1105
1106 setMetaTyVarTcLevel :: TcTyVar -> TcLevel -> TcTyVar
1107 setMetaTyVarTcLevel tv tclvl
1108 = case tcTyVarDetails tv of
1109 details@(MetaTv {}) -> setTcTyVarDetails tv (details { mtv_tclvl = tclvl })
1110 _ -> pprPanic "metaTyVarTcLevel" (ppr tv)
1111
1112 isTyVarTyVar :: Var -> Bool
1113 isTyVarTyVar tv
1114 = case tcTyVarDetails tv of
1115 MetaTv { mtv_info = TyVarTv } -> True
1116 _ -> False
1117
1118 isFlexi, isIndirect :: MetaDetails -> Bool
1119 isFlexi Flexi = True
1120 isFlexi _ = False
1121
1122 isIndirect (Indirect _) = True
1123 isIndirect _ = False
1124
1125 isRuntimeUnkSkol :: TyVar -> Bool
1126 -- Called only in GHC.Tc.Errors; see Note [Runtime skolems] there
1127 isRuntimeUnkSkol x
1128 | RuntimeUnk <- tcTyVarDetails x = True
1129 | otherwise = False
1130
1131 mkTyVarNamePairs :: [TyVar] -> [(Name,TyVar)]
1132 -- Just pair each TyVar with its own name
1133 mkTyVarNamePairs tvs = [(tyVarName tv, tv) | tv <- tvs]
1134
1135 findDupTyVarTvs :: [(Name,TcTyVar)] -> [(Name,Name)]
1136 -- If we have [...(x1,tv)...(x2,tv)...]
1137 -- return (x1,x2) in the result list
1138 findDupTyVarTvs prs
1139 = concatMap mk_result_prs $
1140 findDupsEq eq_snd prs
1141 where
1142 eq_snd (_,tv1) (_,tv2) = tv1 == tv2
1143 mk_result_prs ((n1,_) :| xs) = map (\(n2,_) -> (n1,n2)) xs
1144
1145 {-
1146 ************************************************************************
1147 * *
1148 Tau, sigma and rho
1149 * *
1150 ************************************************************************
1151 -}
1152
1153 mkSigmaTy :: [TyCoVarBinder] -> [PredType] -> Type -> Type
1154 mkSigmaTy bndrs theta tau = mkForAllTys bndrs (mkPhiTy theta tau)
1155
1156 -- | Make a sigma ty where all type variables are 'Inferred'. That is,
1157 -- they cannot be used with visible type application.
1158 mkInfSigmaTy :: [TyCoVar] -> [PredType] -> Type -> Type
1159 mkInfSigmaTy tyvars theta ty = mkSigmaTy (mkTyCoVarBinders Inferred tyvars) theta ty
1160
1161 -- | Make a sigma ty where all type variables are "specified". That is,
1162 -- they can be used with visible type application
1163 mkSpecSigmaTy :: [TyVar] -> [PredType] -> Type -> Type
1164 mkSpecSigmaTy tyvars preds ty = mkSigmaTy (mkTyCoVarBinders Specified tyvars) preds ty
1165
1166 mkPhiTy :: [PredType] -> Type -> Type
1167 mkPhiTy = mkInvisFunTysMany
1168
1169 ---------------
1170 getDFunTyKey :: Type -> OccName -- Get some string from a type, to be used to
1171 -- construct a dictionary function name
1172 getDFunTyKey ty | Just ty' <- coreView ty = getDFunTyKey ty'
1173 getDFunTyKey (TyVarTy tv) = getOccName tv
1174 getDFunTyKey (TyConApp tc _) = getOccName tc
1175 getDFunTyKey (LitTy x) = getDFunTyLitKey x
1176 getDFunTyKey (AppTy fun _) = getDFunTyKey fun
1177 getDFunTyKey (FunTy {}) = getOccName funTyCon
1178 getDFunTyKey (ForAllTy _ t) = getDFunTyKey t
1179 getDFunTyKey (CastTy ty _) = getDFunTyKey ty
1180 getDFunTyKey t@(CoercionTy _) = pprPanic "getDFunTyKey" (ppr t)
1181
1182 getDFunTyLitKey :: TyLit -> OccName
1183 getDFunTyLitKey (NumTyLit n) = mkOccName Name.varName (show n)
1184 getDFunTyLitKey (StrTyLit n) = mkOccName Name.varName (show n) -- hm
1185 getDFunTyLitKey (CharTyLit n) = mkOccName Name.varName (show n)
1186
1187 {- *********************************************************************
1188 * *
1189 Building types
1190 * *
1191 ********************************************************************* -}
1192
1193 -- ToDo: I think we need Tc versions of these
1194 -- Reason: mkCastTy checks isReflexiveCastTy, which checks
1195 -- for equality; and that has a different answer
1196 -- depending on whether or not Type = Constraint
1197
1198 mkTcAppTys :: Type -> [Type] -> Type
1199 mkTcAppTys = mkAppTys
1200
1201 mkTcAppTy :: Type -> Type -> Type
1202 mkTcAppTy = mkAppTy
1203
1204 mkTcCastTy :: Type -> Coercion -> Type
1205 mkTcCastTy = mkCastTy -- Do we need a tc version of mkCastTy?
1206
1207 {-
1208 ************************************************************************
1209 * *
1210 Expanding and splitting
1211 * *
1212 ************************************************************************
1213
1214 These tcSplit functions are like their non-Tc analogues, but
1215 *) they do not look through newtypes
1216
1217 However, they are non-monadic and do not follow through mutable type
1218 variables. It's up to you to make sure this doesn't matter.
1219 -}
1220
1221 -- | Splits a forall type into a list of 'TyBinder's and the inner type.
1222 -- Always succeeds, even if it returns an empty list.
1223 tcSplitPiTys :: Type -> ([TyBinder], Type)
1224 tcSplitPiTys ty
1225 = assert (all isTyBinder (fst sty) ) sty
1226 where sty = splitPiTys ty
1227
1228 -- | Splits a type into a TyBinder and a body, if possible. Panics otherwise
1229 tcSplitPiTy_maybe :: Type -> Maybe (TyBinder, Type)
1230 tcSplitPiTy_maybe ty
1231 = assert (isMaybeTyBinder sty ) sty
1232 where
1233 sty = splitPiTy_maybe ty
1234 isMaybeTyBinder (Just (t,_)) = isTyBinder t
1235 isMaybeTyBinder _ = True
1236
1237 tcSplitForAllTyVarBinder_maybe :: Type -> Maybe (TyVarBinder, Type)
1238 tcSplitForAllTyVarBinder_maybe ty | Just ty' <- tcView ty = tcSplitForAllTyVarBinder_maybe ty'
1239 tcSplitForAllTyVarBinder_maybe (ForAllTy tv ty) = assert (isTyVarBinder tv ) Just (tv, ty)
1240 tcSplitForAllTyVarBinder_maybe _ = Nothing
1241
1242 -- | Like 'tcSplitPiTys', but splits off only named binders,
1243 -- returning just the tyvars.
1244 tcSplitForAllTyVars :: Type -> ([TyVar], Type)
1245 tcSplitForAllTyVars ty
1246 = assert (all isTyVar (fst sty) ) sty
1247 where sty = splitForAllTyCoVars ty
1248
1249 -- | Like 'tcSplitForAllTyVars', but only splits 'ForAllTy's with 'Invisible'
1250 -- type variable binders.
1251 tcSplitForAllInvisTyVars :: Type -> ([TyVar], Type)
1252 tcSplitForAllInvisTyVars ty = tcSplitSomeForAllTyVars isInvisibleArgFlag ty
1253
1254 -- | Like 'tcSplitForAllTyVars', but only splits a 'ForAllTy' if @argf_pred argf@
1255 -- is 'True', where @argf@ is the visibility of the @ForAllTy@'s binder and
1256 -- @argf_pred@ is a predicate over visibilities provided as an argument to this
1257 -- function.
1258 tcSplitSomeForAllTyVars :: (ArgFlag -> Bool) -> Type -> ([TyVar], Type)
1259 tcSplitSomeForAllTyVars argf_pred ty
1260 = split ty ty []
1261 where
1262 split _ (ForAllTy (Bndr tv argf) ty) tvs
1263 | argf_pred argf = split ty ty (tv:tvs)
1264 split orig_ty ty tvs | Just ty' <- coreView ty = split orig_ty ty' tvs
1265 split orig_ty _ tvs = (reverse tvs, orig_ty)
1266
1267 -- | Like 'tcSplitForAllTyVars', but only splits 'ForAllTy's with 'Required' type
1268 -- variable binders. All split tyvars are annotated with '()'.
1269 tcSplitForAllReqTVBinders :: Type -> ([TcReqTVBinder], Type)
1270 tcSplitForAllReqTVBinders ty = assert (all (isTyVar . binderVar) (fst sty) ) sty
1271 where sty = splitForAllReqTVBinders ty
1272
1273 -- | Like 'tcSplitForAllTyVars', but only splits 'ForAllTy's with 'Invisible' type
1274 -- variable binders. All split tyvars are annotated with their 'Specificity'.
1275 tcSplitForAllInvisTVBinders :: Type -> ([TcInvisTVBinder], Type)
1276 tcSplitForAllInvisTVBinders ty = assert (all (isTyVar . binderVar) (fst sty) ) sty
1277 where sty = splitForAllInvisTVBinders ty
1278
1279 -- | Like 'tcSplitForAllTyVars', but splits off only named binders.
1280 tcSplitForAllTyVarBinders :: Type -> ([TyVarBinder], Type)
1281 tcSplitForAllTyVarBinders ty = assert (all isTyVarBinder (fst sty)) sty
1282 where sty = splitForAllTyCoVarBinders ty
1283
1284 -- | Is this a ForAllTy with a named binder?
1285 tcIsForAllTy :: Type -> Bool
1286 tcIsForAllTy ty | Just ty' <- tcView ty = tcIsForAllTy ty'
1287 tcIsForAllTy (ForAllTy {}) = True
1288 tcIsForAllTy _ = False
1289
1290 tcSplitPredFunTy_maybe :: Type -> Maybe (PredType, Type)
1291 -- Split off the first predicate argument from a type
1292 tcSplitPredFunTy_maybe ty
1293 | Just ty' <- tcView ty = tcSplitPredFunTy_maybe ty'
1294 tcSplitPredFunTy_maybe (FunTy { ft_af = InvisArg
1295 , ft_arg = arg, ft_res = res })
1296 = Just (arg, res)
1297 tcSplitPredFunTy_maybe _
1298 = Nothing
1299
1300 tcSplitPhiTy :: Type -> (ThetaType, Type)
1301 tcSplitPhiTy ty
1302 = split ty []
1303 where
1304 split ty ts
1305 = case tcSplitPredFunTy_maybe ty of
1306 Just (pred, ty) -> split ty (pred:ts)
1307 Nothing -> (reverse ts, ty)
1308
1309 -- | Split a sigma type into its parts. This only splits /invisible/ type
1310 -- variable binders, as these are the only forms of binder that the typechecker
1311 -- will implicitly instantiate.
1312 tcSplitSigmaTy :: Type -> ([TyVar], ThetaType, Type)
1313 tcSplitSigmaTy ty = case tcSplitForAllInvisTyVars ty of
1314 (tvs, rho) -> case tcSplitPhiTy rho of
1315 (theta, tau) -> (tvs, theta, tau)
1316
1317 -- | Split a sigma type into its parts, going underneath as many @ForAllTy@s
1318 -- as possible. For example, given this type synonym:
1319 --
1320 -- @
1321 -- type Traversal s t a b = forall f. Applicative f => (a -> f b) -> s -> f t
1322 -- @
1323 --
1324 -- if you called @tcSplitSigmaTy@ on this type:
1325 --
1326 -- @
1327 -- forall s t a b. Each s t a b => Traversal s t a b
1328 -- @
1329 --
1330 -- then it would return @([s,t,a,b], [Each s t a b], Traversal s t a b)@. But
1331 -- if you instead called @tcSplitNestedSigmaTys@ on the type, it would return
1332 -- @([s,t,a,b,f], [Each s t a b, Applicative f], (a -> f b) -> s -> f t)@.
1333 tcSplitNestedSigmaTys :: Type -> ([TyVar], ThetaType, Type)
1334 -- NB: This is basically a pure version of topInstantiate (from Inst) that
1335 -- doesn't compute an HsWrapper.
1336 tcSplitNestedSigmaTys ty
1337 -- If there's a forall, split it apart and try splitting the rho type
1338 -- underneath it.
1339 | (tvs1, theta1, rho1) <- tcSplitSigmaTy ty
1340 , not (null tvs1 && null theta1)
1341 = let (tvs2, theta2, rho2) = tcSplitNestedSigmaTys rho1
1342 in (tvs1 ++ tvs2, theta1 ++ theta2, rho2)
1343 -- If there's no forall, we're done.
1344 | otherwise = ([], [], ty)
1345
1346 -----------------------
1347 tcTyConAppTyCon :: Type -> TyCon
1348 tcTyConAppTyCon ty
1349 = case tcTyConAppTyCon_maybe ty of
1350 Just tc -> tc
1351 Nothing -> pprPanic "tcTyConAppTyCon" (pprType ty)
1352
1353 -- | Like 'tcRepSplitTyConApp_maybe', but only returns the 'TyCon'.
1354 tcTyConAppTyCon_maybe :: Type -> Maybe TyCon
1355 tcTyConAppTyCon_maybe ty
1356 | Just ty' <- tcView ty = tcTyConAppTyCon_maybe ty'
1357 tcTyConAppTyCon_maybe (TyConApp tc _)
1358 = Just tc
1359 tcTyConAppTyCon_maybe (FunTy { ft_af = VisArg })
1360 = Just funTyCon -- (=>) is /not/ a TyCon in its own right
1361 -- C.f. tcRepSplitAppTy_maybe
1362 tcTyConAppTyCon_maybe _
1363 = Nothing
1364
1365 tcTyConAppArgs :: Type -> [Type]
1366 tcTyConAppArgs ty = case tcSplitTyConApp_maybe ty of
1367 Just (_, args) -> args
1368 Nothing -> pprPanic "tcTyConAppArgs" (pprType ty)
1369
1370 tcSplitTyConApp :: Type -> (TyCon, [Type])
1371 tcSplitTyConApp ty = case tcSplitTyConApp_maybe ty of
1372 Just stuff -> stuff
1373 Nothing -> pprPanic "tcSplitTyConApp" (pprType ty)
1374
1375 -----------------------
1376 tcSplitFunTys :: Type -> ([Scaled Type], Type)
1377 tcSplitFunTys ty = case tcSplitFunTy_maybe ty of
1378 Nothing -> ([], ty)
1379 Just (arg,res) -> (arg:args, res')
1380 where
1381 (args,res') = tcSplitFunTys res
1382
1383 tcSplitFunTy_maybe :: Type -> Maybe (Scaled Type, Type)
1384 tcSplitFunTy_maybe ty
1385 | Just ty' <- tcView ty = tcSplitFunTy_maybe ty'
1386 tcSplitFunTy_maybe (FunTy { ft_af = af, ft_mult = w, ft_arg = arg, ft_res = res })
1387 | VisArg <- af = Just (Scaled w arg, res)
1388 tcSplitFunTy_maybe _ = Nothing
1389 -- Note the VisArg guard
1390 -- Consider (?x::Int) => Bool
1391 -- We don't want to treat this as a function type!
1392 -- A concrete example is test tc230:
1393 -- f :: () -> (?p :: ()) => () -> ()
1394 --
1395 -- g = f () ()
1396
1397 tcSplitFunTysN :: Arity -- n: Number of desired args
1398 -> TcRhoType
1399 -> Either Arity -- Number of missing arrows
1400 ([Scaled TcSigmaType],-- Arg types (always N types)
1401 TcSigmaType) -- The rest of the type
1402 -- ^ Split off exactly the specified number argument types
1403 -- Returns
1404 -- (Left m) if there are 'm' missing arrows in the type
1405 -- (Right (tys,res)) if the type looks like t1 -> ... -> tn -> res
1406 tcSplitFunTysN n ty
1407 | n == 0
1408 = Right ([], ty)
1409 | Just (arg,res) <- tcSplitFunTy_maybe ty
1410 = case tcSplitFunTysN (n-1) res of
1411 Left m -> Left m
1412 Right (args,body) -> Right (arg:args, body)
1413 | otherwise
1414 = Left n
1415
1416 tcSplitFunTy :: Type -> (Scaled Type, Type)
1417 tcSplitFunTy ty = expectJust "tcSplitFunTy" (tcSplitFunTy_maybe ty)
1418
1419 tcFunArgTy :: Type -> Scaled Type
1420 tcFunArgTy ty = fst (tcSplitFunTy ty)
1421
1422 tcFunResultTy :: Type -> Type
1423 tcFunResultTy ty = snd (tcSplitFunTy ty)
1424
1425 -- | Strips off n *visible* arguments and returns the resulting type
1426 tcFunResultTyN :: HasDebugCallStack => Arity -> Type -> Type
1427 tcFunResultTyN n ty
1428 | Right (_, res_ty) <- tcSplitFunTysN n ty
1429 = res_ty
1430 | otherwise
1431 = pprPanic "tcFunResultTyN" (ppr n <+> ppr ty)
1432
1433 -----------------------
1434 tcSplitAppTy_maybe :: Type -> Maybe (Type, Type)
1435 tcSplitAppTy_maybe ty | Just ty' <- tcView ty = tcSplitAppTy_maybe ty'
1436 tcSplitAppTy_maybe ty = tcRepSplitAppTy_maybe ty
1437
1438 tcSplitAppTy :: Type -> (Type, Type)
1439 tcSplitAppTy ty = case tcSplitAppTy_maybe ty of
1440 Just stuff -> stuff
1441 Nothing -> pprPanic "tcSplitAppTy" (pprType ty)
1442
1443 tcSplitAppTys :: Type -> (Type, [Type])
1444 tcSplitAppTys ty
1445 = go ty []
1446 where
1447 go ty args = case tcSplitAppTy_maybe ty of
1448 Just (ty', arg) -> go ty' (arg:args)
1449 Nothing -> (ty,args)
1450
1451 -- | Returns the number of arguments in the given type, without
1452 -- looking through synonyms. This is used only for error reporting.
1453 -- We don't look through synonyms because of #11313.
1454 tcRepGetNumAppTys :: Type -> Arity
1455 tcRepGetNumAppTys = length . snd . repSplitAppTys
1456
1457 -----------------------
1458 -- | If the type is a tyvar, possibly under a cast, returns it, along
1459 -- with the coercion. Thus, the co is :: kind tv ~N kind type
1460 tcGetCastedTyVar_maybe :: Type -> Maybe (TyVar, CoercionN)
1461 tcGetCastedTyVar_maybe ty | Just ty' <- tcView ty = tcGetCastedTyVar_maybe ty'
1462 tcGetCastedTyVar_maybe (CastTy (TyVarTy tv) co) = Just (tv, co)
1463 tcGetCastedTyVar_maybe (TyVarTy tv) = Just (tv, mkNomReflCo (tyVarKind tv))
1464 tcGetCastedTyVar_maybe _ = Nothing
1465
1466 tcGetTyVar_maybe :: Type -> Maybe TyVar
1467 tcGetTyVar_maybe ty | Just ty' <- tcView ty = tcGetTyVar_maybe ty'
1468 tcGetTyVar_maybe (TyVarTy tv) = Just tv
1469 tcGetTyVar_maybe _ = Nothing
1470
1471 tcGetTyVar :: String -> Type -> TyVar
1472 tcGetTyVar msg ty
1473 = case tcGetTyVar_maybe ty of
1474 Just tv -> tv
1475 Nothing -> pprPanic msg (ppr ty)
1476
1477 tcIsTyVarTy :: Type -> Bool
1478 tcIsTyVarTy ty | Just ty' <- tcView ty = tcIsTyVarTy ty'
1479 tcIsTyVarTy (CastTy ty _) = tcIsTyVarTy ty -- look through casts, as
1480 -- this is only used for
1481 -- e.g., FlexibleContexts
1482 tcIsTyVarTy (TyVarTy _) = True
1483 tcIsTyVarTy _ = False
1484
1485 -----------------------
1486 tcSplitDFunTy :: Type -> ([TyVar], [Type], Class, [Type])
1487 -- Split the type of a dictionary function
1488 -- We don't use tcSplitSigmaTy, because a DFun may (with NDP)
1489 -- have non-Pred arguments, such as
1490 -- df :: forall m. (forall b. Eq b => Eq (m b)) -> C m
1491 --
1492 -- Also NB splitFunTys, not tcSplitFunTys;
1493 -- the latter specifically stops at PredTy arguments,
1494 -- and we don't want to do that here
1495 tcSplitDFunTy ty
1496 = case tcSplitForAllInvisTyVars ty of { (tvs, rho) ->
1497 case splitFunTys rho of { (theta, tau) ->
1498 case tcSplitDFunHead tau of { (clas, tys) ->
1499 (tvs, map scaledThing theta, clas, tys) }}}
1500
1501 tcSplitDFunHead :: Type -> (Class, [Type])
1502 tcSplitDFunHead = getClassPredTys
1503
1504 tcSplitMethodTy :: Type -> ([TyVar], PredType, Type)
1505 -- A class method (selector) always has a type like
1506 -- forall as. C as => blah
1507 -- So if the class looks like
1508 -- class C a where
1509 -- op :: forall b. (Eq a, Ix b) => a -> b
1510 -- the class method type looks like
1511 -- op :: forall a. C a => forall b. (Eq a, Ix b) => a -> b
1512 --
1513 -- tcSplitMethodTy just peels off the outer forall and
1514 -- that first predicate
1515 tcSplitMethodTy ty
1516 | (sel_tyvars,sel_rho) <- tcSplitForAllInvisTyVars ty
1517 , Just (first_pred, local_meth_ty) <- tcSplitPredFunTy_maybe sel_rho
1518 = (sel_tyvars, first_pred, local_meth_ty)
1519 | otherwise
1520 = pprPanic "tcSplitMethodTy" (ppr ty)
1521
1522
1523 {- *********************************************************************
1524 * *
1525 Type equalities
1526 * *
1527 ********************************************************************* -}
1528
1529 tcEqKind :: HasDebugCallStack => TcKind -> TcKind -> Bool
1530 tcEqKind = tcEqType
1531
1532 tcEqType :: HasDebugCallStack => TcType -> TcType -> Bool
1533 -- ^ tcEqType implements typechecker equality, as described in
1534 -- @Note [Typechecker equality vs definitional equality]@.
1535 tcEqType ty1 ty2
1536 = tcEqTypeNoSyns ki1 ki2
1537 && tcEqTypeNoSyns ty1 ty2
1538 where
1539 ki1 = tcTypeKind ty1
1540 ki2 = tcTypeKind ty2
1541
1542 -- | Just like 'tcEqType', but will return True for types of different kinds
1543 -- as long as their non-coercion structure is identical.
1544 tcEqTypeNoKindCheck :: TcType -> TcType -> Bool
1545 tcEqTypeNoKindCheck ty1 ty2
1546 = tcEqTypeNoSyns ty1 ty2
1547
1548 -- | Check whether two TyConApps are the same; if the number of arguments
1549 -- are different, just checks the common prefix of arguments.
1550 tcEqTyConApps :: TyCon -> [Type] -> TyCon -> [Type] -> Bool
1551 tcEqTyConApps tc1 args1 tc2 args2
1552 = tc1 == tc2 &&
1553 and (zipWith tcEqTypeNoKindCheck args1 args2)
1554 -- No kind check necessary: if both arguments are well typed, then
1555 -- any difference in the kinds of later arguments would show up
1556 -- as differences in earlier (dependent) arguments
1557
1558 {-
1559 Note [Specialising tc_eq_type]
1560 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1561 The type equality predicates in TcType are hit pretty hard during typechecking.
1562 Consequently we take pains to ensure that these paths are compiled to
1563 efficient, minimally-allocating code.
1564
1565 To this end we place an INLINE on tc_eq_type, ensuring that it is inlined into
1566 its publicly-visible interfaces (e.g. tcEqType). In addition to eliminating
1567 some dynamic branches, this allows the simplifier to eliminate the closure
1568 allocations that would otherwise be necessary to capture the two boolean "mode"
1569 flags. This reduces allocations by a good fraction of a percent when compiling
1570 Cabal.
1571
1572 See #19226.
1573 -}
1574
1575 -- | Type equality comparing both visible and invisible arguments and expanding
1576 -- type synonyms.
1577 tcEqTypeNoSyns :: TcType -> TcType -> Bool
1578 tcEqTypeNoSyns ta tb = tc_eq_type False False ta tb
1579
1580 -- | Like 'tcEqType', but returns True if the /visible/ part of the types
1581 -- are equal, even if they are really unequal (in the invisible bits)
1582 tcEqTypeVis :: TcType -> TcType -> Bool
1583 tcEqTypeVis ty1 ty2 = tc_eq_type False True ty1 ty2
1584
1585 -- | Like 'pickyEqTypeVis', but returns a Bool for convenience
1586 pickyEqType :: TcType -> TcType -> Bool
1587 -- Check when two types _look_ the same, _including_ synonyms.
1588 -- So (pickyEqType String [Char]) returns False
1589 -- This ignores kinds and coercions, because this is used only for printing.
1590 pickyEqType ty1 ty2 = tc_eq_type True False ty1 ty2
1591
1592 -- | Real worker for 'tcEqType'. No kind check!
1593 tc_eq_type :: Bool -- ^ True <=> do not expand type synonyms
1594 -> Bool -- ^ True <=> compare visible args only
1595 -> Type -> Type
1596 -> Bool
1597 -- Flags False, False is the usual setting for tc_eq_type
1598 -- See Note [Computing equality on types] in Type
1599 tc_eq_type keep_syns vis_only orig_ty1 orig_ty2
1600 = go orig_env orig_ty1 orig_ty2
1601 where
1602 go :: RnEnv2 -> Type -> Type -> Bool
1603 -- See Note [Comparing nullary type synonyms] in GHC.Core.Type.
1604 go _ (TyConApp tc1 []) (TyConApp tc2 [])
1605 | tc1 == tc2
1606 = True
1607
1608 go env t1 t2 | not keep_syns, Just t1' <- tcView t1 = go env t1' t2
1609 go env t1 t2 | not keep_syns, Just t2' <- tcView t2 = go env t1 t2'
1610
1611 go env (TyVarTy tv1) (TyVarTy tv2)
1612 = rnOccL env tv1 == rnOccR env tv2
1613
1614 go _ (LitTy lit1) (LitTy lit2)
1615 = lit1 == lit2
1616
1617 go env (ForAllTy (Bndr tv1 vis1) ty1)
1618 (ForAllTy (Bndr tv2 vis2) ty2)
1619 = vis1 `sameVis` vis2
1620 -- See Note [ForAllTy and typechecker equality] in
1621 -- GHC.Tc.Solver.Canonical for why we use `sameVis` here
1622 && (vis_only || go env (varType tv1) (varType tv2))
1623 && go (rnBndr2 env tv1 tv2) ty1 ty2
1624
1625 -- Make sure we handle all FunTy cases since falling through to the
1626 -- AppTy case means that tcRepSplitAppTy_maybe may see an unzonked
1627 -- kind variable, which causes things to blow up.
1628 -- See Note [Equality on FunTys] in GHC.Core.TyCo.Rep: we must check
1629 -- kinds here
1630 go env (FunTy _ w1 arg1 res1) (FunTy _ w2 arg2 res2)
1631 = kinds_eq && go env arg1 arg2 && go env res1 res2 && go env w1 w2
1632 where
1633 kinds_eq | vis_only = True
1634 | otherwise = go env (typeKind arg1) (typeKind arg2) &&
1635 go env (typeKind res1) (typeKind res2)
1636
1637 -- See Note [Equality on AppTys] in GHC.Core.Type
1638 go env (AppTy s1 t1) ty2
1639 | Just (s2, t2) <- tcRepSplitAppTy_maybe ty2
1640 = go env s1 s2 && go env t1 t2
1641 go env ty1 (AppTy s2 t2)
1642 | Just (s1, t1) <- tcRepSplitAppTy_maybe ty1
1643 = go env s1 s2 && go env t1 t2
1644
1645 go env (TyConApp tc1 ts1) (TyConApp tc2 ts2)
1646 = tc1 == tc2 && gos env (tc_vis tc1) ts1 ts2
1647
1648 go env (CastTy t1 _) t2 = go env t1 t2
1649 go env t1 (CastTy t2 _) = go env t1 t2
1650 go _ (CoercionTy {}) (CoercionTy {}) = True
1651
1652 go _ _ _ = False
1653
1654 gos _ _ [] [] = True
1655 gos env (ig:igs) (t1:ts1) (t2:ts2) = (ig || go env t1 t2)
1656 && gos env igs ts1 ts2
1657 gos _ _ _ _ = False
1658
1659 tc_vis :: TyCon -> [Bool] -- True for the fields we should ignore
1660 tc_vis tc | vis_only = inviss ++ repeat False -- Ignore invisibles
1661 | otherwise = repeat False -- Ignore nothing
1662 -- The repeat False is necessary because tycons
1663 -- can legitimately be oversaturated
1664 where
1665 bndrs = tyConBinders tc
1666 inviss = map isInvisibleTyConBinder bndrs
1667
1668 orig_env = mkRnEnv2 $ mkInScopeSet $ tyCoVarsOfTypes [orig_ty1, orig_ty2]
1669
1670 {-# INLINE tc_eq_type #-} -- See Note [Specialising tc_eq_type].
1671
1672 {- Note [Typechecker equality vs definitional equality]
1673 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1674 GHC has two notions of equality over Core types:
1675
1676 * Definitional equality, as implemented by GHC.Core.Type.eqType.
1677 See Note [Non-trivial definitional equality] in GHC.Core.TyCo.Rep.
1678 * Typechecker equality, as implemented by tcEqType (in GHC.Tc.Utils.TcType).
1679 GHC.Tc.Solver.Canonical.canEqNC also respects typechecker equality.
1680
1681 Typechecker equality implies definitional equality: if two types are equal
1682 according to typechecker equality, then they are also equal according to
1683 definitional equality. The converse is not always true, as typechecker equality
1684 is more finer-grained than definitional equality in two places:
1685
1686 * Unlike definitional equality, which equates Type and Constraint, typechecker
1687 treats them as distinct types. See Note [Kind Constraint and kind Type] in
1688 GHC.Core.Type.
1689 * Unlike definitional equality, which does not care about the ArgFlag of a
1690 ForAllTy, typechecker equality treats Required type variable binders as
1691 distinct from Invisible type variable binders.
1692 See Note [ForAllTy and typechecker equality] in GHC.Tc.Solver.Canonical.
1693 -}
1694
1695 {- *********************************************************************
1696 * *
1697 Predicate types
1698 * *
1699 ************************************************************************
1700
1701 Deconstructors and tests on predicate types
1702
1703 Note [Kind polymorphic type classes]
1704 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1705 class C f where... -- C :: forall k. k -> Constraint
1706 g :: forall (f::*). C f => f -> f
1707
1708 Here the (C f) in the signature is really (C * f), and we
1709 don't want to complain that the * isn't a type variable!
1710 -}
1711
1712 isTyVarClassPred :: PredType -> Bool
1713 isTyVarClassPred ty = case getClassPredTys_maybe ty of
1714 Just (_, tys) -> all isTyVarTy tys
1715 _ -> False
1716
1717 -------------------------
1718 checkValidClsArgs :: Bool -> Class -> [KindOrType] -> Bool
1719 -- If the Bool is True (flexible contexts), return True (i.e. ok)
1720 -- Otherwise, check that the type (not kind) args are all headed by a tyvar
1721 -- E.g. (Eq a) accepted, (Eq (f a)) accepted, but (Eq Int) rejected
1722 -- This function is here rather than in GHC.Tc.Validity because it is
1723 -- called from GHC.Tc.Solver, which itself is imported by GHC.Tc.Validity
1724 checkValidClsArgs flexible_contexts cls kts
1725 | flexible_contexts = True
1726 | otherwise = all hasTyVarHead tys
1727 where
1728 tys = filterOutInvisibleTypes (classTyCon cls) kts
1729
1730 hasTyVarHead :: Type -> Bool
1731 -- Returns true of (a t1 .. tn), where 'a' is a type variable
1732 hasTyVarHead ty -- Haskell 98 allows predicates of form
1733 | tcIsTyVarTy ty = True -- C (a ty1 .. tyn)
1734 | otherwise -- where a is a type variable
1735 = case tcSplitAppTy_maybe ty of
1736 Just (ty, _) -> hasTyVarHead ty
1737 Nothing -> False
1738
1739 evVarPred :: EvVar -> PredType
1740 evVarPred var = varType var
1741 -- Historical note: I used to have an ASSERT here,
1742 -- checking (isEvVarType (varType var)). But with something like
1743 -- f :: c => _ -> _
1744 -- we end up with (c :: kappa), and (kappa ~ Constraint). Until
1745 -- we solve and zonk (which there is no particular reason to do for
1746 -- partial signatures, (isEvVarType kappa) will return False. But
1747 -- nothing is wrong. So I just removed the ASSERT.
1748
1749 ------------------
1750 -- | When inferring types, should we quantify over a given predicate?
1751 -- Generally true of classes; generally false of equality constraints.
1752 -- Equality constraints that mention quantified type variables and
1753 -- implicit variables complicate the story. See Notes
1754 -- [Inheriting implicit parameters] and [Quantifying over equality constraints]
1755 pickQuantifiablePreds
1756 :: TyVarSet -- Quantifying over these
1757 -> TcThetaType -- Proposed constraints to quantify
1758 -> TcThetaType -- A subset that we can actually quantify
1759 -- This function decides whether a particular constraint should be
1760 -- quantified over, given the type variables that are being quantified
1761 pickQuantifiablePreds qtvs theta
1762 = let flex_ctxt = True in -- Quantify over non-tyvar constraints, even without
1763 -- -XFlexibleContexts: see #10608, #10351
1764 -- flex_ctxt <- xoptM Opt_FlexibleContexts
1765 mapMaybe (pick_me flex_ctxt) theta
1766 where
1767 pick_me flex_ctxt pred
1768 = case classifyPredType pred of
1769
1770 ClassPred cls tys
1771 | Just {} <- isCallStackPred cls tys
1772 -- NEVER infer a CallStack constraint. Otherwise we let
1773 -- the constraints bubble up to be solved from the outer
1774 -- context, or be defaulted when we reach the top-level.
1775 -- See Note [Overview of implicit CallStacks]
1776 -> Nothing
1777
1778 | isIPClass cls
1779 -> Just pred -- See note [Inheriting implicit parameters]
1780
1781 | pick_cls_pred flex_ctxt cls tys
1782 -> Just pred
1783
1784 EqPred eq_rel ty1 ty2
1785 | quantify_equality eq_rel ty1 ty2
1786 , Just (cls, tys) <- boxEqPred eq_rel ty1 ty2
1787 -- boxEqPred: See Note [Lift equality constraints when quantifying]
1788 , pick_cls_pred flex_ctxt cls tys
1789 -> Just (mkClassPred cls tys)
1790
1791 IrredPred ty
1792 | tyCoVarsOfType ty `intersectsVarSet` qtvs
1793 -> Just pred
1794
1795 _ -> Nothing
1796
1797
1798 pick_cls_pred flex_ctxt cls tys
1799 = tyCoVarsOfTypes tys `intersectsVarSet` qtvs
1800 && (checkValidClsArgs flex_ctxt cls tys)
1801 -- Only quantify over predicates that checkValidType
1802 -- will pass! See #10351.
1803
1804 -- See Note [Quantifying over equality constraints]
1805 quantify_equality NomEq ty1 ty2 = quant_fun ty1 || quant_fun ty2
1806 quantify_equality ReprEq _ _ = True
1807
1808 quant_fun ty
1809 = case tcSplitTyConApp_maybe ty of
1810 Just (tc, tys) | isTypeFamilyTyCon tc
1811 -> tyCoVarsOfTypes tys `intersectsVarSet` qtvs
1812 _ -> False
1813
1814 boxEqPred :: EqRel -> Type -> Type -> Maybe (Class, [Type])
1815 -- Given (t1 ~# t2) or (t1 ~R# t2) return the boxed version
1816 -- (t1 ~ t2) or (t1 `Coercible` t2)
1817 boxEqPred eq_rel ty1 ty2
1818 = case eq_rel of
1819 NomEq | homo_kind -> Just (eqClass, [k1, ty1, ty2])
1820 | otherwise -> Just (heqClass, [k1, k2, ty1, ty2])
1821 ReprEq | homo_kind -> Just (coercibleClass, [k1, ty1, ty2])
1822 | otherwise -> Nothing -- Sigh: we do not have hererogeneous Coercible
1823 -- so we can't abstract over it
1824 -- Nothing fundamental: we could add it
1825 where
1826 k1 = tcTypeKind ty1
1827 k2 = tcTypeKind ty2
1828 homo_kind = k1 `tcEqType` k2
1829
1830 pickCapturedPreds
1831 :: TyVarSet -- Quantifying over these
1832 -> TcThetaType -- Proposed constraints to quantify
1833 -> TcThetaType -- A subset that we can actually quantify
1834 -- A simpler version of pickQuantifiablePreds, used to winnow down
1835 -- the inferred constraints of a group of bindings, into those for
1836 -- one particular identifier
1837 pickCapturedPreds qtvs theta
1838 = filter captured theta
1839 where
1840 captured pred = isIPLikePred pred || (tyCoVarsOfType pred `intersectsVarSet` qtvs)
1841
1842
1843 -- Superclasses
1844
1845 type PredWithSCs a = (PredType, [PredType], a)
1846
1847 mkMinimalBySCs :: forall a. (a -> PredType) -> [a] -> [a]
1848 -- Remove predicates that
1849 --
1850 -- - are the same as another predicate
1851 --
1852 -- - can be deduced from another by superclasses,
1853 --
1854 -- - are a reflexive equality (e.g * ~ *)
1855 -- (see Note [Remove redundant provided dicts] in GHC.Tc.TyCl.PatSyn)
1856 --
1857 -- The result is a subset of the input.
1858 -- The 'a' is just paired up with the PredType;
1859 -- typically it might be a dictionary Id
1860 mkMinimalBySCs get_pred xs = go preds_with_scs []
1861 where
1862 preds_with_scs :: [PredWithSCs a]
1863 preds_with_scs = [ (pred, implicants pred, x)
1864 | x <- xs
1865 , let pred = get_pred x ]
1866
1867 go :: [PredWithSCs a] -- Work list
1868 -> [PredWithSCs a] -- Accumulating result
1869 -> [a]
1870 go [] min_preds
1871 = reverse (map thdOf3 min_preds)
1872 -- The 'reverse' isn't strictly necessary, but it
1873 -- means that the results are returned in the same
1874 -- order as the input, which is generally saner
1875 go (work_item@(p,_,_) : work_list) min_preds
1876 | EqPred _ t1 t2 <- classifyPredType p
1877 , t1 `tcEqType` t2 -- See GHC.Tc.TyCl.PatSyn
1878 -- Note [Remove redundant provided dicts]
1879 = go work_list min_preds
1880 | p `in_cloud` work_list || p `in_cloud` min_preds
1881 -- Why look at work-list too? Suppose work_item is Eq a,
1882 -- and work-list contains Ord a
1883 = go work_list min_preds
1884 | otherwise
1885 = go work_list (work_item : min_preds)
1886
1887 in_cloud :: PredType -> [PredWithSCs a] -> Bool
1888 in_cloud p ps = or [ p `tcEqType` p' | (_, scs, _) <- ps, p' <- scs ]
1889
1890 implicants pred
1891 = pred : eq_extras pred ++ transSuperClasses pred
1892
1893 -- Combine (a ~ b) and (b ~ a); no need to have both in one context
1894 -- These can arise when dealing with partial type signatures (e.g. T14715)
1895 eq_extras pred
1896 = case classifyPredType pred of
1897 EqPred r t1 t2 -> [mkPrimEqPredRole (eqRelRole r) t2 t1]
1898 ClassPred cls [k1,k2,t1,t2]
1899 | cls `hasKey` heqTyConKey -> [mkClassPred cls [k2, k1, t2, t1]]
1900 ClassPred cls [k,t1,t2]
1901 | cls `hasKey` eqTyConKey -> [mkClassPred cls [k, t2, t1]]
1902 _ -> []
1903
1904 transSuperClasses :: PredType -> [PredType]
1905 -- (transSuperClasses p) returns (p's superclasses) not including p
1906 -- Stop if you encounter the same class again
1907 -- See Note [Expanding superclasses]
1908 transSuperClasses p
1909 = go emptyNameSet p
1910 where
1911 go :: NameSet -> PredType -> [PredType]
1912 go rec_clss p
1913 | ClassPred cls tys <- classifyPredType p
1914 , let cls_nm = className cls
1915 , not (cls_nm `elemNameSet` rec_clss)
1916 , let rec_clss' | isCTupleClass cls = rec_clss
1917 | otherwise = rec_clss `extendNameSet` cls_nm
1918 = [ p' | sc <- immSuperClasses cls tys
1919 , p' <- sc : go rec_clss' sc ]
1920 | otherwise
1921 = []
1922
1923 immSuperClasses :: Class -> [Type] -> [PredType]
1924 immSuperClasses cls tys
1925 = substTheta (zipTvSubst tyvars tys) sc_theta
1926 where
1927 (tyvars,sc_theta,_,_) = classBigSig cls
1928
1929 isImprovementPred :: PredType -> Bool
1930 -- Either it's an equality, or has some functional dependency
1931 isImprovementPred ty
1932 = case classifyPredType ty of
1933 EqPred NomEq t1 t2 -> not (t1 `tcEqType` t2)
1934 EqPred ReprEq _ _ -> False
1935 ClassPred cls _ -> classHasFds cls
1936 IrredPred {} -> True -- Might have equalities after reduction?
1937 ForAllPred {} -> False
1938 SpecialPred {} -> False
1939
1940 {- Note [Expanding superclasses]
1941 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1942 When we expand superclasses, we use the following algorithm:
1943
1944 transSuperClasses( C tys ) returns the transitive superclasses
1945 of (C tys), not including C itself
1946
1947 For example
1948 class C a b => D a b
1949 class D b a => C a b
1950
1951 Then
1952 transSuperClasses( Ord ty ) = [Eq ty]
1953 transSuperClasses( C ta tb ) = [D tb ta, C tb ta]
1954
1955 Notice that in the recursive-superclass case we include C again at
1956 the end of the chain. One could exclude C in this case, but
1957 the code is more awkward and there seems no good reason to do so.
1958 (However C.f. GHC.Tc.Solver.Canonical.mk_strict_superclasses, which /does/
1959 appear to do so.)
1960
1961 The algorithm is expand( so_far, pred ):
1962
1963 1. If pred is not a class constraint, return empty set
1964 Otherwise pred = C ts
1965 2. If C is in so_far, return empty set (breaks loops)
1966 3. Find the immediate superclasses constraints of (C ts)
1967 4. For each such sc_pred, return (sc_pred : expand( so_far+C, D ss )
1968
1969 Notice that
1970
1971 * With normal Haskell-98 classes, the loop-detector will never bite,
1972 so we'll get all the superclasses.
1973
1974 * We need the loop-breaker in case we have UndecidableSuperClasses on
1975
1976 * Since there is only a finite number of distinct classes, expansion
1977 must terminate.
1978
1979 * The loop breaking is a bit conservative. Notably, a tuple class
1980 could contain many times without threatening termination:
1981 (Eq a, (Ord a, Ix a))
1982 And this is try of any class that we can statically guarantee
1983 as non-recursive (in some sense). For now, we just make a special
1984 case for tuples. Something better would be cool.
1985
1986 See also GHC.Tc.TyCl.Utils.checkClassCycles.
1987
1988 Note [Lift equality constraints when quantifying]
1989 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1990 We can't quantify over a constraint (t1 ~# t2) because that isn't a
1991 predicate type; see Note [Types for coercions, predicates, and evidence]
1992 in GHC.Core.TyCo.Rep.
1993
1994 So we have to 'lift' it to (t1 ~ t2). Similarly (~R#) must be lifted
1995 to Coercible.
1996
1997 This tiresome lifting is the reason that pick_me (in
1998 pickQuantifiablePreds) returns a Maybe rather than a Bool.
1999
2000 Note [Quantifying over equality constraints]
2001 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2002 Should we quantify over an equality constraint (s ~ t)? In general, we don't.
2003 Doing so may simply postpone a type error from the function definition site to
2004 its call site. (At worst, imagine (Int ~ Bool)).
2005
2006 However, consider this
2007 forall a. (F [a] ~ Int) => blah
2008 Should we quantify over the (F [a] ~ Int)? Perhaps yes, because at the call
2009 site we will know 'a', and perhaps we have instance F [Bool] = Int.
2010 So we *do* quantify over a type-family equality where the arguments mention
2011 the quantified variables.
2012
2013 Note [Inheriting implicit parameters]
2014 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2015 Consider this:
2016
2017 f x = (x::Int) + ?y
2018
2019 where f is *not* a top-level binding.
2020 From the RHS of f we'll get the constraint (?y::Int).
2021 There are two types we might infer for f:
2022
2023 f :: Int -> Int
2024
2025 (so we get ?y from the context of f's definition), or
2026
2027 f :: (?y::Int) => Int -> Int
2028
2029 At first you might think the first was better, because then
2030 ?y behaves like a free variable of the definition, rather than
2031 having to be passed at each call site. But of course, the WHOLE
2032 IDEA is that ?y should be passed at each call site (that's what
2033 dynamic binding means) so we'd better infer the second.
2034
2035 BOTTOM LINE: when *inferring types* you must quantify over implicit
2036 parameters, *even if* they don't mention the bound type variables.
2037 Reason: because implicit parameters, uniquely, have local instance
2038 declarations. See pickQuantifiablePreds.
2039
2040 Note [Quantifying over equality constraints]
2041 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2042 Should we quantify over an equality constraint (s ~ t)? In general, we don't.
2043 Doing so may simply postpone a type error from the function definition site to
2044 its call site. (At worst, imagine (Int ~ Bool)).
2045
2046 However, consider this
2047 forall a. (F [a] ~ Int) => blah
2048 Should we quantify over the (F [a] ~ Int). Perhaps yes, because at the call
2049 site we will know 'a', and perhaps we have instance F [Bool] = Int.
2050 So we *do* quantify over a type-family equality where the arguments mention
2051 the quantified variables.
2052
2053 ************************************************************************
2054 * *
2055 Classifying types
2056 * *
2057 ************************************************************************
2058 -}
2059
2060 isSigmaTy :: TcType -> Bool
2061 -- isSigmaTy returns true of any qualified type. It doesn't
2062 -- *necessarily* have any foralls. E.g
2063 -- f :: (?x::Int) => Int -> Int
2064 isSigmaTy ty | Just ty' <- tcView ty = isSigmaTy ty'
2065 isSigmaTy (ForAllTy {}) = True
2066 isSigmaTy (FunTy { ft_af = InvisArg }) = True
2067 isSigmaTy _ = False
2068
2069 isRhoTy :: TcType -> Bool -- True of TcRhoTypes; see Note [TcRhoType]
2070 isRhoTy ty | Just ty' <- tcView ty = isRhoTy ty'
2071 isRhoTy (ForAllTy {}) = False
2072 isRhoTy (FunTy { ft_af = InvisArg }) = False
2073 isRhoTy _ = True
2074
2075 -- | Like 'isRhoTy', but also says 'True' for 'Infer' types
2076 isRhoExpTy :: ExpType -> Bool
2077 isRhoExpTy (Check ty) = isRhoTy ty
2078 isRhoExpTy (Infer {}) = True
2079
2080 isOverloadedTy :: Type -> Bool
2081 -- Yes for a type of a function that might require evidence-passing
2082 -- Used only by bindLocalMethods
2083 isOverloadedTy ty | Just ty' <- tcView ty = isOverloadedTy ty'
2084 isOverloadedTy (ForAllTy _ ty) = isOverloadedTy ty
2085 isOverloadedTy (FunTy { ft_af = InvisArg }) = True
2086 isOverloadedTy _ = False
2087
2088 isFloatTy, isDoubleTy, isIntegerTy, isNaturalTy,
2089 isIntTy, isWordTy, isBoolTy,
2090 isUnitTy, isCharTy, isAnyTy :: Type -> Bool
2091 isFloatTy = is_tc floatTyConKey
2092 isDoubleTy = is_tc doubleTyConKey
2093 isIntegerTy = is_tc integerTyConKey
2094 isNaturalTy = is_tc naturalTyConKey
2095 isIntTy = is_tc intTyConKey
2096 isWordTy = is_tc wordTyConKey
2097 isBoolTy = is_tc boolTyConKey
2098 isUnitTy = is_tc unitTyConKey
2099 isCharTy = is_tc charTyConKey
2100 isAnyTy = is_tc anyTyConKey
2101
2102 -- | Does a type represent a floating-point number?
2103 isFloatingTy :: Type -> Bool
2104 isFloatingTy ty = isFloatTy ty || isDoubleTy ty
2105
2106 -- | Is a type 'String'?
2107 isStringTy :: Type -> Bool
2108 isStringTy ty
2109 = case tcSplitTyConApp_maybe ty of
2110 Just (tc, [arg_ty]) -> tc == listTyCon && isCharTy arg_ty
2111 _ -> False
2112
2113 is_tc :: Unique -> Type -> Bool
2114 -- Newtypes are opaque to this
2115 is_tc uniq ty = case tcSplitTyConApp_maybe ty of
2116 Just (tc, _) -> uniq == getUnique tc
2117 Nothing -> False
2118
2119 isRigidTy :: TcType -> Bool
2120 isRigidTy ty
2121 | Just (tc,_) <- tcSplitTyConApp_maybe ty = isGenerativeTyCon tc Nominal
2122 | Just {} <- tcSplitAppTy_maybe ty = True
2123 | isForAllTy ty = True
2124 | otherwise = False
2125
2126
2127 {-
2128 ************************************************************************
2129 * *
2130 Misc
2131 * *
2132 ************************************************************************
2133
2134 Note [Visible type application]
2135 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2136 GHC implements a generalisation of the algorithm described in the
2137 "Visible Type Application" paper (available from
2138 http://www.cis.upenn.edu/~sweirich/publications.html). A key part
2139 of that algorithm is to distinguish user-specified variables from inferred
2140 variables. For example, the following should typecheck:
2141
2142 f :: forall a b. a -> b -> b
2143 f = const id
2144
2145 g = const id
2146
2147 x = f @Int @Bool 5 False
2148 y = g 5 @Bool False
2149
2150 The idea is that we wish to allow visible type application when we are
2151 instantiating a specified, fixed variable. In practice, specified, fixed
2152 variables are either written in a type signature (or
2153 annotation), OR are imported from another module. (We could do better here,
2154 for example by doing SCC analysis on parts of a module and considering any
2155 type from outside one's SCC to be fully specified, but this is very confusing to
2156 users. The simple rule above is much more straightforward and predictable.)
2157
2158 So, both of f's quantified variables are specified and may be instantiated.
2159 But g has no type signature, so only id's variable is specified (because id
2160 is imported). We write the type of g as forall {a}. a -> forall b. b -> b.
2161 Note that the a is in braces, meaning it cannot be instantiated with
2162 visible type application.
2163
2164 Tracking specified vs. inferred variables is done conveniently by a field
2165 in TyBinder.
2166
2167 -}
2168
2169 deNoteType :: Type -> Type
2170 -- Remove all *outermost* type synonyms and other notes
2171 deNoteType ty | Just ty' <- coreView ty = deNoteType ty'
2172 deNoteType ty = ty
2173
2174 {-
2175 Find the free tycons and classes of a type. This is used in the front
2176 end of the compiler.
2177 -}
2178
2179 {-
2180 ************************************************************************
2181 * *
2182 External types
2183 * *
2184 ************************************************************************
2185
2186 The compiler's foreign function interface supports the passing of a
2187 restricted set of types as arguments and results (the restricting factor
2188 being the )
2189 -}
2190
2191 tcSplitIOType_maybe :: Type -> Maybe (TyCon, Type)
2192 -- (tcSplitIOType_maybe t) returns Just (IO,t',co)
2193 -- if co : t ~ IO t'
2194 -- returns Nothing otherwise
2195 tcSplitIOType_maybe ty
2196 = case tcSplitTyConApp_maybe ty of
2197 Just (io_tycon, [io_res_ty])
2198 | io_tycon `hasKey` ioTyConKey ->
2199 Just (io_tycon, io_res_ty)
2200 _ ->
2201 Nothing
2202
2203 isFFITy :: Type -> Bool
2204 -- True for any TyCon that can possibly be an arg or result of an FFI call
2205 isFFITy ty = isValid (checkRepTyCon legalFFITyCon ty)
2206
2207 isFFIArgumentTy :: DynFlags -> Safety -> Type -> Validity
2208 -- Checks for valid argument type for a 'foreign import'
2209 isFFIArgumentTy dflags safety ty
2210 = checkRepTyCon (legalOutgoingTyCon dflags safety) ty
2211
2212 isFFIExternalTy :: Type -> Validity
2213 -- Types that are allowed as arguments of a 'foreign export'
2214 isFFIExternalTy ty = checkRepTyCon legalFEArgTyCon ty
2215
2216 isFFIImportResultTy :: DynFlags -> Type -> Validity
2217 isFFIImportResultTy dflags ty
2218 = checkRepTyCon (legalFIResultTyCon dflags) ty
2219
2220 isFFIExportResultTy :: Type -> Validity
2221 isFFIExportResultTy ty = checkRepTyCon legalFEResultTyCon ty
2222
2223 isFFIDynTy :: Type -> Type -> Validity
2224 -- The type in a foreign import dynamic must be Ptr, FunPtr, or a newtype of
2225 -- either, and the wrapped function type must be equal to the given type.
2226 -- We assume that all types have been run through normaliseFfiType, so we don't
2227 -- need to worry about expanding newtypes here.
2228 isFFIDynTy expected ty
2229 -- Note [Foreign import dynamic]
2230 -- In the example below, expected would be 'CInt -> IO ()', while ty would
2231 -- be 'FunPtr (CDouble -> IO ())'.
2232 | Just (tc, [ty']) <- splitTyConApp_maybe ty
2233 , tyConUnique tc `elem` [ptrTyConKey, funPtrTyConKey]
2234 , eqType ty' expected
2235 = IsValid
2236 | otherwise
2237 = NotValid (vcat [ text "Expected: Ptr/FunPtr" <+> pprParendType expected <> comma
2238 , text " Actual:" <+> ppr ty ])
2239
2240 isFFILabelTy :: Type -> Validity
2241 -- The type of a foreign label must be Ptr, FunPtr, or a newtype of either.
2242 isFFILabelTy ty = checkRepTyCon ok ty
2243 where
2244 ok tc | tc `hasKey` funPtrTyConKey || tc `hasKey` ptrTyConKey
2245 = IsValid
2246 | otherwise
2247 = NotValid (text "A foreign-imported address (via &foo) must have type (Ptr a) or (FunPtr a)")
2248
2249 isFFIPrimArgumentTy :: DynFlags -> Type -> Validity
2250 -- Checks for valid argument type for a 'foreign import prim'
2251 -- Currently they must all be simple unlifted types, or the well-known type
2252 -- Any, which can be used to pass the address to a Haskell object on the heap to
2253 -- the foreign function.
2254 isFFIPrimArgumentTy dflags ty
2255 | isAnyTy ty = IsValid
2256 | otherwise = checkRepTyCon (legalFIPrimArgTyCon dflags) ty
2257
2258 isFFIPrimResultTy :: DynFlags -> Type -> Validity
2259 -- Checks for valid result type for a 'foreign import prim' Currently
2260 -- it must be an unlifted type, including unboxed tuples, unboxed
2261 -- sums, or the well-known type Any.
2262 isFFIPrimResultTy dflags ty
2263 | isAnyTy ty = IsValid
2264 | otherwise = checkRepTyCon (legalFIPrimResultTyCon dflags) ty
2265
2266 isFunPtrTy :: Type -> Bool
2267 isFunPtrTy ty
2268 | Just (tc, [_]) <- splitTyConApp_maybe ty
2269 = tc `hasKey` funPtrTyConKey
2270 | otherwise
2271 = False
2272
2273 -- normaliseFfiType gets run before checkRepTyCon, so we don't
2274 -- need to worry about looking through newtypes or type functions
2275 -- here; that's already been taken care of.
2276 checkRepTyCon :: (TyCon -> Validity) -> Type -> Validity
2277 checkRepTyCon check_tc ty
2278 = case splitTyConApp_maybe ty of
2279 Just (tc, tys)
2280 | isNewTyCon tc -> NotValid (hang msg 2 (mk_nt_reason tc tys $$ nt_fix))
2281 | otherwise -> case check_tc tc of
2282 IsValid -> IsValid
2283 NotValid extra -> NotValid (msg $$ extra)
2284 Nothing -> NotValid (quotes (ppr ty) <+> text "is not a data type")
2285 where
2286 msg = quotes (ppr ty) <+> text "cannot be marshalled in a foreign call"
2287 mk_nt_reason tc tys
2288 | null tys = text "because its data constructor is not in scope"
2289 | otherwise = text "because the data constructor for"
2290 <+> quotes (ppr tc) <+> text "is not in scope"
2291 nt_fix = text "Possible fix: import the data constructor to bring it into scope"
2292
2293 {-
2294 Note [Foreign import dynamic]
2295 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2296 A dynamic stub must be of the form 'FunPtr ft -> ft' where ft is any foreign
2297 type. Similarly, a wrapper stub must be of the form 'ft -> IO (FunPtr ft)'.
2298
2299 We use isFFIDynTy to check whether a signature is well-formed. For example,
2300 given a (illegal) declaration like:
2301
2302 foreign import ccall "dynamic"
2303 foo :: FunPtr (CDouble -> IO ()) -> CInt -> IO ()
2304
2305 isFFIDynTy will compare the 'FunPtr' type 'CDouble -> IO ()' with the curried
2306 result type 'CInt -> IO ()', and return False, as they are not equal.
2307
2308
2309 ----------------------------------------------
2310 These chaps do the work; they are not exported
2311 ----------------------------------------------
2312 -}
2313
2314 legalFEArgTyCon :: TyCon -> Validity
2315 legalFEArgTyCon tc
2316 -- It's illegal to make foreign exports that take unboxed
2317 -- arguments. The RTS API currently can't invoke such things. --SDM 7/2000
2318 = boxedMarshalableTyCon tc
2319
2320 legalFIResultTyCon :: DynFlags -> TyCon -> Validity
2321 legalFIResultTyCon dflags tc
2322 | tc == unitTyCon = IsValid
2323 | otherwise = marshalableTyCon dflags tc
2324
2325 legalFEResultTyCon :: TyCon -> Validity
2326 legalFEResultTyCon tc
2327 | tc == unitTyCon = IsValid
2328 | otherwise = boxedMarshalableTyCon tc
2329
2330 legalOutgoingTyCon :: DynFlags -> Safety -> TyCon -> Validity
2331 -- Checks validity of types going from Haskell -> external world
2332 legalOutgoingTyCon dflags _ tc
2333 = marshalableTyCon dflags tc
2334
2335 legalFFITyCon :: TyCon -> Validity
2336 -- True for any TyCon that can possibly be an arg or result of an FFI call
2337 legalFFITyCon tc
2338 | isUnliftedTyCon tc = IsValid
2339 | tc == unitTyCon = IsValid
2340 | otherwise = boxedMarshalableTyCon tc
2341
2342 marshalableTyCon :: DynFlags -> TyCon -> Validity
2343 marshalableTyCon dflags tc
2344 | isUnliftedTyCon tc
2345 , not (isUnboxedTupleTyCon tc || isUnboxedSumTyCon tc)
2346 , not (null (tyConPrimRep tc)) -- Note [Marshalling void]
2347 = validIfUnliftedFFITypes dflags
2348 | otherwise
2349 = boxedMarshalableTyCon tc
2350
2351 boxedMarshalableTyCon :: TyCon -> Validity
2352 boxedMarshalableTyCon tc
2353 | getUnique tc `elem` [ intTyConKey, int8TyConKey, int16TyConKey
2354 , int32TyConKey, int64TyConKey
2355 , wordTyConKey, word8TyConKey, word16TyConKey
2356 , word32TyConKey, word64TyConKey
2357 , floatTyConKey, doubleTyConKey
2358 , ptrTyConKey, funPtrTyConKey
2359 , charTyConKey
2360 , stablePtrTyConKey
2361 , boolTyConKey
2362 ]
2363 = IsValid
2364
2365 | otherwise = NotValid empty
2366
2367 legalFIPrimArgTyCon :: DynFlags -> TyCon -> Validity
2368 -- Check args of 'foreign import prim', only allow simple unlifted types.
2369 -- Strictly speaking it is unnecessary to ban unboxed tuples and sums here since
2370 -- currently they're of the wrong kind to use in function args anyway.
2371 legalFIPrimArgTyCon dflags tc
2372 | isUnliftedTyCon tc
2373 , not (isUnboxedTupleTyCon tc || isUnboxedSumTyCon tc)
2374 = validIfUnliftedFFITypes dflags
2375 | otherwise
2376 = NotValid unlifted_only
2377
2378 legalFIPrimResultTyCon :: DynFlags -> TyCon -> Validity
2379 -- Check result type of 'foreign import prim'. Allow simple unlifted
2380 -- types and also unboxed tuple and sum result types.
2381 legalFIPrimResultTyCon dflags tc
2382 | isUnliftedTyCon tc
2383 , isUnboxedTupleTyCon tc || isUnboxedSumTyCon tc
2384 || not (null (tyConPrimRep tc)) -- Note [Marshalling void]
2385 = validIfUnliftedFFITypes dflags
2386
2387 | otherwise
2388 = NotValid unlifted_only
2389
2390 unlifted_only :: SDoc
2391 unlifted_only = text "foreign import prim only accepts simple unlifted types"
2392
2393 validIfUnliftedFFITypes :: DynFlags -> Validity
2394 validIfUnliftedFFITypes dflags
2395 | xopt LangExt.UnliftedFFITypes dflags = IsValid
2396 | otherwise = NotValid (text "To marshal unlifted types, use UnliftedFFITypes")
2397
2398 {-
2399 Note [Marshalling void]
2400 ~~~~~~~~~~~~~~~~~~~~~~~
2401 We don't treat State# (whose PrimRep is VoidRep) as marshalable.
2402 In turn that means you can't write
2403 foreign import foo :: Int -> State# RealWorld
2404
2405 Reason: the back end falls over with panic "primRepHint:VoidRep";
2406 and there is no compelling reason to permit it
2407 -}
2408
2409 {-
2410 ************************************************************************
2411 * *
2412 The "Paterson size" of a type
2413 * *
2414 ************************************************************************
2415 -}
2416
2417 {-
2418 Note [Paterson conditions on PredTypes]
2419 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2420 We are considering whether *class* constraints terminate
2421 (see Note [Paterson conditions]). Precisely, the Paterson conditions
2422 would have us check that "the constraint has fewer constructors and variables
2423 (taken together and counting repetitions) than the head.".
2424
2425 However, we can be a bit more refined by looking at which kind of constraint
2426 this actually is. There are two main tricks:
2427
2428 1. It seems like it should be OK not to count the tuple type constructor
2429 for a PredType like (Show a, Eq a) :: Constraint, since we don't
2430 count the "implicit" tuple in the ThetaType itself.
2431
2432 In fact, the Paterson test just checks *each component* of the top level
2433 ThetaType against the size bound, one at a time. By analogy, it should be
2434 OK to return the size of the *largest* tuple component as the size of the
2435 whole tuple.
2436
2437 2. Once we get into an implicit parameter or equality we
2438 can't get back to a class constraint, so it's safe
2439 to say "size 0". See #4200.
2440
2441 NB: we don't want to detect PredTypes in sizeType (and then call
2442 sizePred on them), or we might get an infinite loop if that PredType
2443 is irreducible. See #5581.
2444 -}
2445
2446 type TypeSize = IntWithInf
2447
2448 sizeType :: Type -> TypeSize
2449 -- Size of a type: the number of variables and constructors
2450 -- Ignore kinds altogether
2451 sizeType = go
2452 where
2453 go ty | Just exp_ty <- tcView ty = go exp_ty
2454 go (TyVarTy {}) = 1
2455 go (TyConApp tc tys)
2456 | isTypeFamilyTyCon tc = infinity -- Type-family applications can
2457 -- expand to any arbitrary size
2458 | otherwise = sizeTypes (filterOutInvisibleTypes tc tys) + 1
2459 -- Why filter out invisible args? I suppose any
2460 -- size ordering is sound, but why is this better?
2461 -- I came across this when investigating #14010.
2462 go (LitTy {}) = 1
2463 go (FunTy _ w arg res) = go w + go arg + go res + 1
2464 go (AppTy fun arg) = go fun + go arg
2465 go (ForAllTy (Bndr tv vis) ty)
2466 | isVisibleArgFlag vis = go (tyVarKind tv) + go ty + 1
2467 | otherwise = go ty + 1
2468 go (CastTy ty _) = go ty
2469 go (CoercionTy {}) = 0
2470
2471 sizeTypes :: [Type] -> TypeSize
2472 sizeTypes tys = sum (map sizeType tys)
2473
2474 -----------------------------------------------------------------------------------
2475 -----------------------------------------------------------------------------------
2476 -----------------------
2477 -- | For every arg a tycon can take, the returned list says True if the argument
2478 -- is taken visibly, and False otherwise. Ends with an infinite tail of Trues to
2479 -- allow for oversaturation.
2480 tcTyConVisibilities :: TyCon -> [Bool]
2481 tcTyConVisibilities tc = tc_binder_viss ++ tc_return_kind_viss ++ repeat True
2482 where
2483 tc_binder_viss = map isVisibleTyConBinder (tyConBinders tc)
2484 tc_return_kind_viss = map isVisibleBinder (fst $ tcSplitPiTys (tyConResKind tc))
2485
2486 -- | If the tycon is applied to the types, is the next argument visible?
2487 isNextTyConArgVisible :: TyCon -> [Type] -> Bool
2488 isNextTyConArgVisible tc tys
2489 = tcTyConVisibilities tc `getNth` length tys
2490
2491 -- | Should this type be applied to a visible argument?
2492 isNextArgVisible :: TcType -> Bool
2493 isNextArgVisible ty
2494 | Just (bndr, _) <- tcSplitPiTy_maybe ty = isVisibleBinder bndr
2495 | otherwise = True
2496 -- this second case might happen if, say, we have an unzonked TauTv.
2497 -- But TauTvs can't range over types that take invisible arguments