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