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