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