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