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