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