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