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