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