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