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