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