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