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