Improve typechecking of let-bindings
[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, cmpType, cmpTypes, 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 mkNakedCastTy = CastTy
1190
1191 {-
1192 ************************************************************************
1193 * *
1194 \subsection{Expanding and splitting}
1195 * *
1196 ************************************************************************
1197
1198 These tcSplit functions are like their non-Tc analogues, but
1199 *) they do not look through newtypes
1200
1201 However, they are non-monadic and do not follow through mutable type
1202 variables. It's up to you to make sure this doesn't matter.
1203 -}
1204
1205 -- | Splits a forall type into a list of 'TyBinder's and the inner type.
1206 -- Always succeeds, even if it returns an empty list.
1207 tcSplitPiTys :: Type -> ([TyBinder], Type)
1208 tcSplitPiTys = splitPiTys
1209
1210 tcSplitForAllTy_maybe :: Type -> Maybe (TyBinder, Type)
1211 tcSplitForAllTy_maybe ty | Just ty' <- coreView ty = tcSplitForAllTy_maybe ty'
1212 tcSplitForAllTy_maybe (ForAllTy tv ty) = Just (tv, ty)
1213 tcSplitForAllTy_maybe _ = Nothing
1214
1215 -- | Like 'tcSplitPiTys', but splits off only named binders, returning
1216 -- just the tycovars.
1217 tcSplitForAllTys :: Type -> ([TyVar], Type)
1218 tcSplitForAllTys = splitForAllTys
1219
1220 -- | Like 'tcSplitForAllTys', but splits off only named binders.
1221 tcSplitNamedPiTys :: Type -> ([TyBinder], Type)
1222 tcSplitNamedPiTys = splitNamedPiTys
1223
1224 -- | Is this a ForAllTy with a named binder?
1225 tcIsForAllTy :: Type -> Bool
1226 tcIsForAllTy ty | Just ty' <- coreView ty = tcIsForAllTy ty'
1227 tcIsForAllTy (ForAllTy (Named {}) _) = True
1228 tcIsForAllTy _ = False
1229
1230 tcSplitPredFunTy_maybe :: Type -> Maybe (PredType, Type)
1231 -- Split off the first predicate argument from a type
1232 tcSplitPredFunTy_maybe ty
1233 | Just ty' <- coreView ty = tcSplitPredFunTy_maybe ty'
1234 tcSplitPredFunTy_maybe (ForAllTy (Anon arg) res)
1235 | isPredTy arg = Just (arg, res)
1236 tcSplitPredFunTy_maybe _
1237 = Nothing
1238
1239 tcSplitPhiTy :: Type -> (ThetaType, Type)
1240 tcSplitPhiTy ty
1241 = split ty []
1242 where
1243 split ty ts
1244 = case tcSplitPredFunTy_maybe ty of
1245 Just (pred, ty) -> split ty (pred:ts)
1246 Nothing -> (reverse ts, ty)
1247
1248 -- | Split a sigma type into its parts.
1249 tcSplitSigmaTy :: Type -> ([TyVar], ThetaType, Type)
1250 tcSplitSigmaTy ty = case tcSplitForAllTys ty of
1251 (tvs, rho) -> case tcSplitPhiTy rho of
1252 (theta, tau) -> (tvs, theta, tau)
1253
1254 -----------------------
1255 tcDeepSplitSigmaTy_maybe
1256 :: TcSigmaType -> Maybe ([TcType], [TyVar], ThetaType, TcSigmaType)
1257 -- Looks for a *non-trivial* quantified type, under zero or more function arrows
1258 -- By "non-trivial" we mean either tyvars or constraints are non-empty
1259
1260 tcDeepSplitSigmaTy_maybe ty
1261 | Just (arg_ty, res_ty) <- tcSplitFunTy_maybe ty
1262 , Just (arg_tys, tvs, theta, rho) <- tcDeepSplitSigmaTy_maybe res_ty
1263 = Just (arg_ty:arg_tys, tvs, theta, rho)
1264
1265 | (tvs, theta, rho) <- tcSplitSigmaTy ty
1266 , not (null tvs && null theta)
1267 = Just ([], tvs, theta, rho)
1268
1269 | otherwise = Nothing
1270
1271 -----------------------
1272 tcTyConAppTyCon :: Type -> TyCon
1273 tcTyConAppTyCon ty = case tcSplitTyConApp_maybe ty of
1274 Just (tc, _) -> tc
1275 Nothing -> pprPanic "tcTyConAppTyCon" (pprType ty)
1276
1277 tcTyConAppArgs :: Type -> [Type]
1278 tcTyConAppArgs ty = case tcSplitTyConApp_maybe ty of
1279 Just (_, args) -> args
1280 Nothing -> pprPanic "tcTyConAppArgs" (pprType ty)
1281
1282 tcSplitTyConApp :: Type -> (TyCon, [Type])
1283 tcSplitTyConApp ty = case tcSplitTyConApp_maybe ty of
1284 Just stuff -> stuff
1285 Nothing -> pprPanic "tcSplitTyConApp" (pprType ty)
1286
1287 tcSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
1288 tcSplitTyConApp_maybe ty | Just ty' <- coreView ty = tcSplitTyConApp_maybe ty'
1289 tcSplitTyConApp_maybe ty = tcRepSplitTyConApp_maybe ty
1290
1291 tcRepSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
1292 tcRepSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
1293 tcRepSplitTyConApp_maybe (ForAllTy (Anon arg) res) = Just (funTyCon, [arg,res])
1294 tcRepSplitTyConApp_maybe _ = Nothing
1295
1296
1297 -----------------------
1298 tcSplitFunTys :: Type -> ([Type], Type)
1299 tcSplitFunTys ty = case tcSplitFunTy_maybe ty of
1300 Nothing -> ([], ty)
1301 Just (arg,res) -> (arg:args, res')
1302 where
1303 (args,res') = tcSplitFunTys res
1304
1305 tcSplitFunTy_maybe :: Type -> Maybe (Type, Type)
1306 tcSplitFunTy_maybe ty | Just ty' <- coreView ty = tcSplitFunTy_maybe ty'
1307 tcSplitFunTy_maybe (ForAllTy (Anon arg) res)
1308 | not (isPredTy arg) = Just (arg, res)
1309 tcSplitFunTy_maybe _ = Nothing
1310 -- Note the typeKind guard
1311 -- Consider (?x::Int) => Bool
1312 -- We don't want to treat this as a function type!
1313 -- A concrete example is test tc230:
1314 -- f :: () -> (?p :: ()) => () -> ()
1315 --
1316 -- g = f () ()
1317
1318 tcSplitFunTysN :: Arity -- N: Number of desired args
1319 -> TcRhoType
1320 -> Either Arity -- Number of missing arrows
1321 ([TcSigmaType], -- Arg types (N or fewer)
1322 TcSigmaType) -- The rest of the type
1323 -- ^ Split off exactly the specified number argument types
1324 -- Returns
1325 -- (Left m) if there are 'm' missing arrows in the type
1326 -- (Right (tys,res)) if the type looks like t1 -> ... -> tn -> res
1327 tcSplitFunTysN n ty
1328 | n == 0
1329 = Right ([], ty)
1330 | Just (arg,res) <- tcSplitFunTy_maybe ty
1331 = case tcSplitFunTysN (n-1) res of
1332 Left m -> Left m
1333 Right (args,body) -> Right (arg:args, body)
1334 | otherwise
1335 = Left n
1336
1337 tcSplitFunTy :: Type -> (Type, Type)
1338 tcSplitFunTy ty = expectJust "tcSplitFunTy" (tcSplitFunTy_maybe ty)
1339
1340 tcFunArgTy :: Type -> Type
1341 tcFunArgTy ty = fst (tcSplitFunTy ty)
1342
1343 tcFunResultTy :: Type -> Type
1344 tcFunResultTy ty = snd (tcSplitFunTy ty)
1345
1346 -----------------------
1347 tcSplitAppTy_maybe :: Type -> Maybe (Type, Type)
1348 tcSplitAppTy_maybe ty | Just ty' <- coreView ty = tcSplitAppTy_maybe ty'
1349 tcSplitAppTy_maybe ty = tcRepSplitAppTy_maybe ty
1350
1351 tcSplitAppTy :: Type -> (Type, Type)
1352 tcSplitAppTy ty = case tcSplitAppTy_maybe ty of
1353 Just stuff -> stuff
1354 Nothing -> pprPanic "tcSplitAppTy" (pprType ty)
1355
1356 tcSplitAppTys :: Type -> (Type, [Type])
1357 tcSplitAppTys ty
1358 = go ty []
1359 where
1360 go ty args = case tcSplitAppTy_maybe ty of
1361 Just (ty', arg) -> go ty' (arg:args)
1362 Nothing -> (ty,args)
1363
1364 -----------------------
1365 tcGetTyVar_maybe :: Type -> Maybe TyVar
1366 tcGetTyVar_maybe ty | Just ty' <- coreView ty = tcGetTyVar_maybe ty'
1367 tcGetTyVar_maybe (TyVarTy tv) = Just tv
1368 tcGetTyVar_maybe _ = Nothing
1369
1370 tcGetTyVar :: String -> Type -> TyVar
1371 tcGetTyVar msg ty = expectJust msg (tcGetTyVar_maybe ty)
1372
1373 tcIsTyVarTy :: Type -> Bool
1374 tcIsTyVarTy ty | Just ty' <- coreView ty = tcIsTyVarTy ty'
1375 tcIsTyVarTy (CastTy ty _) = tcIsTyVarTy ty -- look through casts, as
1376 -- this is only used for
1377 -- e.g., FlexibleContexts
1378 tcIsTyVarTy (TyVarTy _) = True
1379 tcIsTyVarTy _ = False
1380
1381 -----------------------
1382 tcSplitDFunTy :: Type -> ([TyVar], [Type], Class, [Type])
1383 -- Split the type of a dictionary function
1384 -- We don't use tcSplitSigmaTy, because a DFun may (with NDP)
1385 -- have non-Pred arguments, such as
1386 -- df :: forall m. (forall b. Eq b => Eq (m b)) -> C m
1387 --
1388 -- Also NB splitFunTys, not tcSplitFunTys;
1389 -- the latter specifically stops at PredTy arguments,
1390 -- and we don't want to do that here
1391 tcSplitDFunTy ty
1392 = case tcSplitForAllTys ty of { (tvs, rho) ->
1393 case splitFunTys rho of { (theta, tau) ->
1394 case tcSplitDFunHead tau of { (clas, tys) ->
1395 (tvs, theta, clas, tys) }}}
1396
1397 tcSplitDFunHead :: Type -> (Class, [Type])
1398 tcSplitDFunHead = getClassPredTys
1399
1400 tcSplitMethodTy :: Type -> ([TyVar], PredType, Type)
1401 -- A class method (selector) always has a type like
1402 -- forall as. C as => blah
1403 -- So if the class looks like
1404 -- class C a where
1405 -- op :: forall b. (Eq a, Ix b) => a -> b
1406 -- the class method type looks like
1407 -- op :: forall a. C a => forall b. (Eq a, Ix b) => a -> b
1408 --
1409 -- tcSplitMethodTy just peels off the outer forall and
1410 -- that first predicate
1411 tcSplitMethodTy ty
1412 | (sel_tyvars,sel_rho) <- tcSplitForAllTys ty
1413 , Just (first_pred, local_meth_ty) <- tcSplitPredFunTy_maybe sel_rho
1414 = (sel_tyvars, first_pred, local_meth_ty)
1415 | otherwise
1416 = pprPanic "tcSplitMethodTy" (ppr ty)
1417
1418 -----------------------
1419 tcEqKind :: TcKind -> TcKind -> Bool
1420 tcEqKind = tcEqType
1421
1422 tcEqType :: TcType -> TcType -> Bool
1423 -- tcEqType is a proper implements the same Note [Non-trivial definitional
1424 -- equality] (in TyCoRep) as `eqType`, but Type.eqType believes (* ==
1425 -- Constraint), and that is NOT what we want in the type checker!
1426 tcEqType ty1 ty2
1427 = isNothing (tc_eq_type coreView ki1 ki2) &&
1428 isNothing (tc_eq_type coreView ty1 ty2)
1429 where
1430 ki1 = typeKind ty1
1431 ki2 = typeKind ty2
1432
1433 -- | Just like 'tcEqType', but will return True for types of different kinds
1434 -- as long as their non-coercion structure is identical.
1435 tcEqTypeNoKindCheck :: TcType -> TcType -> Bool
1436 tcEqTypeNoKindCheck ty1 ty2
1437 = isNothing $ tc_eq_type coreView ty1 ty2
1438
1439 -- | Like 'tcEqType', but returns information about whether the difference
1440 -- is visible in the case of a mismatch. A return of Nothing means the types
1441 -- are 'tcEqType'.
1442 tcEqTypeVis :: TcType -> TcType -> Maybe VisibilityFlag
1443 tcEqTypeVis ty1 ty2
1444 = tc_eq_type coreView ty1 ty2 <!> invis (tc_eq_type coreView ki1 ki2)
1445 where
1446 ki1 = typeKind ty1
1447 ki2 = typeKind ty2
1448
1449 -- convert Just Visible to Just Invisible
1450 invis :: Maybe VisibilityFlag -> Maybe VisibilityFlag
1451 invis = fmap (const Invisible)
1452
1453 (<!>) :: Maybe VisibilityFlag -> Maybe VisibilityFlag -> Maybe VisibilityFlag
1454 Nothing <!> x = x
1455 Just Visible <!> _ = Just Visible
1456 Just _inv <!> Just Visible = Just Visible
1457 Just inv <!> _ = Just inv
1458 infixr 3 <!>
1459
1460 -- | Real worker for 'tcEqType'. No kind check!
1461 tc_eq_type :: (TcType -> Maybe TcType) -- ^ @coreView@, if you want unwrapping
1462 -> Type -> Type -> Maybe VisibilityFlag
1463 tc_eq_type view_fun orig_ty1 orig_ty2 = go Visible orig_env orig_ty1 orig_ty2
1464 where
1465 go vis env t1 t2 | Just t1' <- view_fun t1 = go vis env t1' t2
1466 go vis env t1 t2 | Just t2' <- view_fun t2 = go vis env t1 t2'
1467
1468 go vis env (TyVarTy tv1) (TyVarTy tv2)
1469 = check vis $ rnOccL env tv1 == rnOccR env tv2
1470
1471 go vis _ (LitTy lit1) (LitTy lit2)
1472 = check vis $ lit1 == lit2
1473
1474 go vis env (ForAllTy (Named tv1 vis1) ty1)
1475 (ForAllTy (Named tv2 vis2) ty2)
1476 = go vis1 env (tyVarKind tv1) (tyVarKind tv2)
1477 <!> go vis (rnBndr2 env tv1 tv2) ty1 ty2
1478 <!> check vis (vis1 == vis2)
1479 go vis env (ForAllTy (Anon arg1) res1) (ForAllTy (Anon arg2) res2)
1480 = go vis env arg1 arg2 <!> go vis env res1 res2
1481
1482 -- See Note [Equality on AppTys] in Type
1483 go vis env (AppTy s1 t1) ty2
1484 | Just (s2, t2) <- tcRepSplitAppTy_maybe ty2
1485 = go vis env s1 s2 <!> go vis env t1 t2
1486 go vis env ty1 (AppTy s2 t2)
1487 | Just (s1, t1) <- tcRepSplitAppTy_maybe ty1
1488 = go vis env s1 s2 <!> go vis env t1 t2
1489 go vis env (TyConApp tc1 ts1) (TyConApp tc2 ts2)
1490 = check vis (tc1 == tc2) <!> gos (tc_vis vis tc1) env ts1 ts2
1491 go vis env (CastTy t1 _) t2 = go vis env t1 t2
1492 go vis env t1 (CastTy t2 _) = go vis env t1 t2
1493 go _ _ (CoercionTy {}) (CoercionTy {}) = Nothing
1494 go vis _ _ _ = Just vis
1495
1496 gos _ _ [] [] = Nothing
1497 gos (v:vs) env (t1:ts1) (t2:ts2) = go v env t1 t2 <!> gos vs env ts1 ts2
1498 gos (v:_) _ _ _ = Just v
1499 gos _ _ _ _ = panic "tc_eq_type"
1500
1501 tc_vis :: VisibilityFlag -> TyCon -> [VisibilityFlag]
1502 tc_vis Visible tc = viss ++ repeat Visible
1503 -- the repeat Visible is necessary because tycons can legitimately
1504 -- be oversaturated
1505 where
1506 bndrs = tyConBinders tc
1507 viss = map binderVisibility bndrs
1508 tc_vis vis _ = repeat vis -- if we're not in a visible context, our args
1509 -- aren't either
1510
1511 check :: VisibilityFlag -> Bool -> Maybe VisibilityFlag
1512 check _ True = Nothing
1513 check vis False = Just vis
1514
1515 orig_env = mkRnEnv2 $ mkInScopeSet $ tyCoVarsOfTypes [orig_ty1, orig_ty2]
1516
1517 -- | Like 'pickyEqTypeVis', but returns a Bool for convenience
1518 pickyEqType :: TcType -> TcType -> Bool
1519 -- Check when two types _look_ the same, _including_ synonyms.
1520 -- So (pickyEqType String [Char]) returns False
1521 -- This ignores kinds and coercions, because this is used only for printing.
1522 pickyEqType ty1 ty2
1523 = isNothing $
1524 tc_eq_type (const Nothing) ty1 ty2
1525
1526 {-
1527 Note [Occurs check expansion]
1528 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1529 (occurCheckExpand tv xi) expands synonyms in xi just enough to get rid
1530 of occurrences of tv outside type function arguments, if that is
1531 possible; otherwise, it returns Nothing.
1532
1533 For example, suppose we have
1534 type F a b = [a]
1535 Then
1536 occurCheckExpand b (F Int b) = Just [Int]
1537 but
1538 occurCheckExpand a (F a Int) = Nothing
1539
1540 We don't promise to do the absolute minimum amount of expanding
1541 necessary, but we try not to do expansions we don't need to. We
1542 prefer doing inner expansions first. For example,
1543 type F a b = (a, Int, a, [a])
1544 type G b = Char
1545 We have
1546 occurCheckExpand b (F (G b)) = F Char
1547 even though we could also expand F to get rid of b.
1548
1549 The two variants of the function are to support TcUnify.checkTauTvUpdate,
1550 which wants to prevent unification with type families. For more on this
1551 point, see Note [Prevent unification with type families] in TcUnify.
1552
1553 See also Note [occurCheckExpand] in TcCanonical
1554 -}
1555
1556 data OccCheckResult a
1557 = OC_OK a
1558 | OC_Forall
1559 | OC_Occurs
1560
1561 instance Functor OccCheckResult where
1562 fmap = liftM
1563
1564 instance Applicative OccCheckResult where
1565 pure = OC_OK
1566 (<*>) = ap
1567
1568 instance Monad OccCheckResult where
1569 OC_OK x >>= k = k x
1570 OC_Forall >>= _ = OC_Forall
1571 OC_Occurs >>= _ = OC_Occurs
1572
1573 occurCheckExpand :: DynFlags -> TcTyVar -> Type -> OccCheckResult Type
1574 -- See Note [Occurs check expansion]
1575 -- Check whether
1576 -- a) the given variable occurs in the given type.
1577 -- b) there is a forall in the type (unless we have -XImpredicativeTypes)
1578 --
1579 -- We may have needed to do some type synonym unfolding in order to
1580 -- get rid of the variable (or forall), so we also return the unfolded
1581 -- version of the type, which is guaranteed to be syntactically free
1582 -- of the given type variable. If the type is already syntactically
1583 -- free of the variable, then the same type is returned.
1584 --
1585 -- NB: in the past we also rejected a SigTv matched with a non-tyvar
1586 -- But it is wrong to reject that for Givens;
1587 -- and SigTv is in any case handled separately by
1588 -- - TcUnify.checkTauTvUpdate (on-the-fly unifier)
1589 -- - TcInteract.canSolveByUnification (main constraint solver)
1590 occurCheckExpand dflags tv ty
1591 | fast_check ty = return ty
1592 | otherwise = go emptyVarEnv ty
1593 where
1594 details = tcTyVarDetails tv
1595
1596 impredicative = canUnifyWithPolyType dflags details
1597
1598 -- True => fine
1599 fast_check (LitTy {}) = True
1600 fast_check (TyVarTy tv') = tv /= tv' && fast_check (tyVarKind tv')
1601 fast_check (TyConApp tc tys) = all fast_check tys
1602 && (isTauTyCon tc || impredicative)
1603 fast_check (ForAllTy (Anon a) r) = fast_check a && fast_check r
1604 fast_check (AppTy fun arg) = fast_check fun && fast_check arg
1605 fast_check (ForAllTy (Named tv' _) ty)
1606 = impredicative
1607 && fast_check (tyVarKind tv')
1608 && (tv == tv' || fast_check ty)
1609 fast_check (CastTy ty co) = fast_check ty && fast_check_co co
1610 fast_check (CoercionTy co) = fast_check_co co
1611
1612 -- we really are only doing an occurs check here; no bother about
1613 -- impredicativity in coercions, as they're inferred
1614 fast_check_co co = not (tv `elemVarSet` tyCoVarsOfCo co)
1615
1616 go :: VarEnv TyVar -- carries mappings necessary because of kind expansion
1617 -> Type -> OccCheckResult Type
1618 go env (TyVarTy tv')
1619 | tv == tv' = OC_Occurs
1620 | Just tv'' <- lookupVarEnv env tv' = return (mkTyVarTy tv'')
1621 | otherwise = do { k' <- go env (tyVarKind tv')
1622 ; return (mkTyVarTy $
1623 setTyVarKind tv' k') }
1624 go _ ty@(LitTy {}) = return ty
1625 go env (AppTy ty1 ty2) = do { ty1' <- go env ty1
1626 ; ty2' <- go env ty2
1627 ; return (mkAppTy ty1' ty2') }
1628 go env (ForAllTy (Anon ty1) ty2)
1629 = do { ty1' <- go env ty1
1630 ; ty2' <- go env ty2
1631 ; return (mkFunTy ty1' ty2') }
1632 go env ty@(ForAllTy (Named tv' vis) body_ty)
1633 | not impredicative = OC_Forall
1634 | tv == tv' = return ty
1635 | otherwise = do { ki' <- go env ki
1636 ; let tv'' = setTyVarKind tv' ki'
1637 env' = extendVarEnv env tv' tv''
1638 ; body' <- go env' body_ty
1639 ; return (ForAllTy (Named tv'' vis) body') }
1640 where ki = tyVarKind tv'
1641
1642 -- For a type constructor application, first try expanding away the
1643 -- offending variable from the arguments. If that doesn't work, next
1644 -- see if the type constructor is a type synonym, and if so, expand
1645 -- it and try again.
1646 go env ty@(TyConApp tc tys)
1647 = case do { tys <- mapM (go env) tys
1648 ; return (mkTyConApp tc tys) } of
1649 OC_OK ty
1650 | impredicative || isTauTyCon tc
1651 -> return ty -- First try to eliminate the tyvar from the args
1652 | otherwise
1653 -> OC_Forall -- A type synonym with a forall on the RHS
1654 bad | Just ty' <- coreView ty -> go env ty'
1655 | otherwise -> bad
1656 -- Failing that, try to expand a synonym
1657
1658 go env (CastTy ty co) = do { ty' <- go env ty
1659 ; co' <- go_co env co
1660 ; return (mkCastTy ty' co') }
1661 go env (CoercionTy co) = do { co' <- go_co env co
1662 ; return (mkCoercionTy co') }
1663
1664 go_co env (Refl r ty) = do { ty' <- go env ty
1665 ; return (mkReflCo r ty') }
1666 -- Note: Coercions do not contain type synonyms
1667 go_co env (TyConAppCo r tc args) = do { args' <- mapM (go_co env) args
1668 ; return (mkTyConAppCo r tc args') }
1669 go_co env (AppCo co arg) = do { co' <- go_co env co
1670 ; arg' <- go_co env arg
1671 ; return (mkAppCo co' arg') }
1672 go_co env co@(ForAllCo tv' kind_co body_co)
1673 | not impredicative = OC_Forall
1674 | tv == tv' = return co
1675 | otherwise = do { kind_co' <- go_co env kind_co
1676 ; let tv'' = setTyVarKind tv' $
1677 pFst (coercionKind kind_co')
1678 env' = extendVarEnv env tv' tv''
1679 ; body' <- go_co env' body_co
1680 ; return (ForAllCo tv'' kind_co' body') }
1681 go_co env (CoVarCo c) = do { k' <- go env (varType c)
1682 ; return (mkCoVarCo (setVarType c k')) }
1683 go_co env (AxiomInstCo ax ind args) = do { args' <- mapM (go_co env) args
1684 ; return (mkAxiomInstCo ax ind args') }
1685 go_co env (UnivCo p r ty1 ty2) = do { p' <- go_prov env p
1686 ; ty1' <- go env ty1
1687 ; ty2' <- go env ty2
1688 ; return (mkUnivCo p' r ty1' ty2') }
1689 go_co env (SymCo co) = do { co' <- go_co env co
1690 ; return (mkSymCo co') }
1691 go_co env (TransCo co1 co2) = do { co1' <- go_co env co1
1692 ; co2' <- go_co env co2
1693 ; return (mkTransCo co1' co2') }
1694 go_co env (NthCo n co) = do { co' <- go_co env co
1695 ; return (mkNthCo n co') }
1696 go_co env (LRCo lr co) = do { co' <- go_co env co
1697 ; return (mkLRCo lr co') }
1698 go_co env (InstCo co arg) = do { co' <- go_co env co
1699 ; arg' <- go_co env arg
1700 ; return (mkInstCo co' arg') }
1701 go_co env (CoherenceCo co1 co2) = do { co1' <- go_co env co1
1702 ; co2' <- go_co env co2
1703 ; return (mkCoherenceCo co1' co2') }
1704 go_co env (KindCo co) = do { co' <- go_co env co
1705 ; return (mkKindCo co') }
1706 go_co env (SubCo co) = do { co' <- go_co env co
1707 ; return (mkSubCo co') }
1708 go_co env (AxiomRuleCo ax cs) = do { cs' <- mapM (go_co env) cs
1709 ; return (mkAxiomRuleCo ax cs') }
1710
1711 go_prov _ UnsafeCoerceProv = return UnsafeCoerceProv
1712 go_prov env (PhantomProv co) = PhantomProv <$> go_co env co
1713 go_prov env (ProofIrrelProv co) = ProofIrrelProv <$> go_co env co
1714 go_prov _ p@(PluginProv _) = return p
1715 go_prov _ p@(HoleProv _) = return p
1716
1717 canUnifyWithPolyType :: DynFlags -> TcTyVarDetails -> Bool
1718 canUnifyWithPolyType dflags details
1719 = case details of
1720 MetaTv { mtv_info = SigTv } -> False
1721 MetaTv { mtv_info = TauTv } -> xopt LangExt.ImpredicativeTypes dflags
1722 _other -> True
1723 -- We can have non-meta tyvars in given constraints
1724
1725 {- Note [Expanding superclasses]
1726 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1727 When we expand superclasses, we use the following algorithm:
1728
1729 expand( so_far, pred ) returns the transitive superclasses of pred,
1730 not including pred itself
1731 1. If pred is not a class constraint, return empty set
1732 Otherwise pred = C ts
1733 2. If C is in so_far, return empty set (breaks loops)
1734 3. Find the immediate superclasses constraints of (C ts)
1735 4. For each such sc_pred, return (sc_pred : expand( so_far+C, D ss )
1736
1737 Notice that
1738
1739 * With normal Haskell-98 classes, the loop-detector will never bite,
1740 so we'll get all the superclasses.
1741
1742 * Since there is only a finite number of distinct classes, expansion
1743 must terminate.
1744
1745 * The loop breaking is a bit conservative. Notably, a tuple class
1746 could contain many times without threatening termination:
1747 (Eq a, (Ord a, Ix a))
1748 And this is try of any class that we can statically guarantee
1749 as non-recursive (in some sense). For now, we just make a special
1750 case for tuples. Somthing better would be cool.
1751
1752 See also TcTyDecls.checkClassCycles.
1753
1754
1755 ************************************************************************
1756 * *
1757 \subsection{Predicate types}
1758 * *
1759 ************************************************************************
1760
1761 Deconstructors and tests on predicate types
1762
1763 Note [Kind polymorphic type classes]
1764 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1765 class C f where... -- C :: forall k. k -> Constraint
1766 g :: forall (f::*). C f => f -> f
1767
1768 Here the (C f) in the signature is really (C * f), and we
1769 don't want to complain that the * isn't a type variable!
1770 -}
1771
1772 isTyVarClassPred :: PredType -> Bool
1773 isTyVarClassPred ty = case getClassPredTys_maybe ty of
1774 Just (_, tys) -> all isTyVarTy tys
1775 _ -> False
1776
1777 -------------------------
1778 checkValidClsArgs :: Bool -> Class -> [KindOrType] -> Bool
1779 -- If the Bool is True (flexible contexts), return True (i.e. ok)
1780 -- Otherwise, check that the type (not kind) args are all headed by a tyvar
1781 -- E.g. (Eq a) accepted, (Eq (f a)) accepted, but (Eq Int) rejected
1782 -- This function is here rather than in TcValidity because it is
1783 -- called from TcSimplify, which itself is imported by TcValidity
1784 checkValidClsArgs flexible_contexts cls kts
1785 | flexible_contexts = True
1786 | otherwise = all hasTyVarHead tys
1787 where
1788 tys = filterOutInvisibleTypes (classTyCon cls) kts
1789
1790 hasTyVarHead :: Type -> Bool
1791 -- Returns true of (a t1 .. tn), where 'a' is a type variable
1792 hasTyVarHead ty -- Haskell 98 allows predicates of form
1793 | tcIsTyVarTy ty = True -- C (a ty1 .. tyn)
1794 | otherwise -- where a is a type variable
1795 = case tcSplitAppTy_maybe ty of
1796 Just (ty, _) -> hasTyVarHead ty
1797 Nothing -> False
1798
1799 evVarPred_maybe :: EvVar -> Maybe PredType
1800 evVarPred_maybe v = if isPredTy ty then Just ty else Nothing
1801 where ty = varType v
1802
1803 evVarPred :: EvVar -> PredType
1804 evVarPred var
1805 | debugIsOn
1806 = case evVarPred_maybe var of
1807 Just pred -> pred
1808 Nothing -> pprPanic "tcEvVarPred" (ppr var <+> ppr (varType var))
1809 | otherwise
1810 = varType var
1811
1812 ------------------
1813 -- | When inferring types, should we quantify over a given predicate?
1814 -- Generally true of classes; generally false of equality constraints.
1815 -- Equality constraints that mention quantified type variables and
1816 -- implicit variables complicate the story. See Notes
1817 -- [Inheriting implicit parameters] and [Quantifying over equality constraints]
1818 pickQuantifiablePreds
1819 :: TyVarSet -- Quantifying over these
1820 -> TcThetaType -- Proposed constraints to quantify
1821 -> TcThetaType -- A subset that we can actually quantify
1822 -- This function decides whether a particular constraint should be
1823 -- quantified over, given the type variables that are being quantified
1824 pickQuantifiablePreds qtvs theta
1825 = let flex_ctxt = True in -- Quantify over non-tyvar constraints, even without
1826 -- -XFlexibleContexts: see Trac #10608, #10351
1827 -- flex_ctxt <- xoptM Opt_FlexibleContexts
1828 filter (pick_me flex_ctxt) theta
1829 where
1830 pick_me flex_ctxt pred
1831 = case classifyPredType pred of
1832
1833 ClassPred cls tys
1834 | Just {} <- isCallStackPred pred
1835 -- NEVER infer a CallStack constraint
1836 -- Otherwise, we let the constraints bubble up to be
1837 -- solved from the outer context, or be defaulted when we
1838 -- reach the top-level.
1839 -- see Note [Overview of implicit CallStacks]
1840 -> False
1841
1842 | isIPClass cls -> True -- See note [Inheriting implicit parameters]
1843
1844 | otherwise
1845 -> pick_cls_pred flex_ctxt cls tys
1846
1847 EqPred ReprEq ty1 ty2 -> pick_cls_pred flex_ctxt coercibleClass [ty1, ty2]
1848 -- representational equality is like a class constraint
1849
1850 EqPred NomEq ty1 ty2 -> quant_fun ty1 || quant_fun ty2
1851 IrredPred ty -> tyCoVarsOfType ty `intersectsVarSet` qtvs
1852
1853 pick_cls_pred flex_ctxt cls tys
1854 = tyCoVarsOfTypes tys `intersectsVarSet` qtvs
1855 && (checkValidClsArgs flex_ctxt cls tys)
1856 -- Only quantify over predicates that checkValidType
1857 -- will pass! See Trac #10351.
1858
1859 -- See Note [Quantifying over equality constraints]
1860 quant_fun ty
1861 = case tcSplitTyConApp_maybe ty of
1862 Just (tc, tys) | isTypeFamilyTyCon tc
1863 -> tyCoVarsOfTypes tys `intersectsVarSet` qtvs
1864 _ -> False
1865
1866 pickCapturedPreds
1867 :: TyVarSet -- Quantifying over these
1868 -> TcThetaType -- Proposed constraints to quantify
1869 -> TcThetaType -- A subset that we can actually quantify
1870 -- A simpler version of pickQuantifiablePreds, used to winnow down
1871 -- the inferred constrains of a group of bindings, into those for
1872 -- one particular identifier
1873 pickCapturedPreds qtvs theta
1874 = filter captured theta
1875 where
1876 captured pred = isIPPred pred || (tyCoVarsOfType pred `intersectsVarSet` qtvs)
1877
1878
1879 -- Superclasses
1880
1881 type PredWithSCs = (PredType, [PredType])
1882
1883 mkMinimalBySCs :: [PredType] -> [PredType]
1884 -- Remove predicates that can be deduced from others by superclasses
1885 -- Result is a subset of the input
1886 mkMinimalBySCs ptys = go preds_with_scs []
1887 where
1888 preds_with_scs :: [PredWithSCs]
1889 preds_with_scs = [ (pred, transSuperClasses pred)
1890 | pred <- ptys ]
1891
1892 go :: [PredWithSCs] -- Work list
1893 -> [PredWithSCs] -- Accumulating result
1894 -> [PredType]
1895 go [] min_preds = map fst min_preds
1896 go (work_item@(p,_) : work_list) min_preds
1897 | p `in_cloud` work_list || p `in_cloud` min_preds
1898 = go work_list min_preds
1899 | otherwise
1900 = go work_list (work_item : min_preds)
1901
1902 in_cloud :: PredType -> [PredWithSCs] -> Bool
1903 in_cloud p ps = or [ p `eqType` p' | (_, scs) <- ps, p' <- scs ]
1904
1905 transSuperClasses :: PredType -> [PredType]
1906 -- (transSuperClasses p) returns (p's superclasses) not including p
1907 -- Stop if you encounter the same class again
1908 -- See Note [Expanding superclasses]
1909 transSuperClasses p
1910 = go emptyNameSet p
1911 where
1912 go :: NameSet -> PredType -> [PredType]
1913 go rec_clss p
1914 | ClassPred cls tys <- classifyPredType p
1915 , let cls_nm = className cls
1916 , not (cls_nm `elemNameSet` rec_clss)
1917 , let rec_clss' | isCTupleClass cls = rec_clss
1918 | otherwise = rec_clss `extendNameSet` cls_nm
1919 = [ p' | sc <- immSuperClasses cls tys
1920 , p' <- sc : go rec_clss' sc ]
1921 | otherwise
1922 = []
1923
1924 immSuperClasses :: Class -> [Type] -> [PredType]
1925 immSuperClasses cls tys
1926 = substTheta (zipTvSubst tyvars tys) sc_theta
1927 where
1928 (tyvars,sc_theta,_,_) = classBigSig cls
1929
1930 isImprovementPred :: PredType -> Bool
1931 -- Either it's an equality, or has some functional dependency
1932 isImprovementPred ty
1933 = case classifyPredType ty of
1934 EqPred NomEq t1 t2 -> not (t1 `tcEqType` t2)
1935 EqPred ReprEq _ _ -> False
1936 ClassPred cls _ -> classHasFds cls
1937 IrredPred {} -> True -- Might have equalities after reduction?
1938
1939 {-
1940 Note [Inheriting implicit parameters]
1941 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1942 Consider this:
1943
1944 f x = (x::Int) + ?y
1945
1946 where f is *not* a top-level binding.
1947 From the RHS of f we'll get the constraint (?y::Int).
1948 There are two types we might infer for f:
1949
1950 f :: Int -> Int
1951
1952 (so we get ?y from the context of f's definition), or
1953
1954 f :: (?y::Int) => Int -> Int
1955
1956 At first you might think the first was better, because then
1957 ?y behaves like a free variable of the definition, rather than
1958 having to be passed at each call site. But of course, the WHOLE
1959 IDEA is that ?y should be passed at each call site (that's what
1960 dynamic binding means) so we'd better infer the second.
1961
1962 BOTTOM LINE: when *inferring types* you must quantify over implicit
1963 parameters, *even if* they don't mention the bound type variables.
1964 Reason: because implicit parameters, uniquely, have local instance
1965 declarations. See pickQuantifiablePreds.
1966
1967 Note [Quantifying over equality constraints]
1968 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1969 Should we quantify over an equality constraint (s ~ t)? In general, we don't.
1970 Doing so may simply postpone a type error from the function definition site to
1971 its call site. (At worst, imagine (Int ~ Bool)).
1972
1973 However, consider this
1974 forall a. (F [a] ~ Int) => blah
1975 Should we quantify over the (F [a] ~ Int). Perhaps yes, because at the call
1976 site we will know 'a', and perhaps we have instance F [Bool] = Int.
1977 So we *do* quantify over a type-family equality where the arguments mention
1978 the quantified variables.
1979
1980 ************************************************************************
1981 * *
1982 \subsection{Predicates}
1983 * *
1984 ************************************************************************
1985 -}
1986
1987 isSigmaTy :: TcType -> Bool
1988 -- isSigmaTy returns true of any qualified type. It doesn't
1989 -- *necessarily* have any foralls. E.g
1990 -- f :: (?x::Int) => Int -> Int
1991 isSigmaTy ty | Just ty' <- coreView ty = isSigmaTy ty'
1992 isSigmaTy (ForAllTy (Named {}) _) = True
1993 isSigmaTy (ForAllTy (Anon a) _) = isPredTy a
1994 isSigmaTy _ = False
1995
1996 isRhoTy :: TcType -> Bool -- True of TcRhoTypes; see Note [TcRhoType]
1997 isRhoTy ty | Just ty' <- coreView ty = isRhoTy ty'
1998 isRhoTy (ForAllTy (Named {}) _) = False
1999 isRhoTy (ForAllTy (Anon a) r) = not (isPredTy a) && isRhoTy r
2000 isRhoTy _ = True
2001
2002 -- | Like 'isRhoTy', but also says 'True' for 'Infer' types
2003 isRhoExpTy :: ExpType -> Bool
2004 isRhoExpTy (Check ty) = isRhoTy ty
2005 isRhoExpTy (Infer {}) = True
2006
2007 isOverloadedTy :: Type -> Bool
2008 -- Yes for a type of a function that might require evidence-passing
2009 -- Used only by bindLocalMethods
2010 isOverloadedTy ty | Just ty' <- coreView ty = isOverloadedTy ty'
2011 isOverloadedTy (ForAllTy (Named {}) ty) = isOverloadedTy ty
2012 isOverloadedTy (ForAllTy (Anon a) _) = isPredTy a
2013 isOverloadedTy _ = False
2014
2015 isFloatTy, isDoubleTy, isIntegerTy, isIntTy, isWordTy, isBoolTy,
2016 isUnitTy, isCharTy, isAnyTy :: Type -> Bool
2017 isFloatTy = is_tc floatTyConKey
2018 isDoubleTy = is_tc doubleTyConKey
2019 isIntegerTy = is_tc integerTyConKey
2020 isIntTy = is_tc intTyConKey
2021 isWordTy = is_tc wordTyConKey
2022 isBoolTy = is_tc boolTyConKey
2023 isUnitTy = is_tc unitTyConKey
2024 isCharTy = is_tc charTyConKey
2025 isAnyTy = is_tc anyTyConKey
2026
2027 -- | Does a type represent a floating-point number?
2028 isFloatingTy :: Type -> Bool
2029 isFloatingTy ty = isFloatTy ty || isDoubleTy ty
2030
2031 -- | Is a type 'String'?
2032 isStringTy :: Type -> Bool
2033 isStringTy ty
2034 = case tcSplitTyConApp_maybe ty of
2035 Just (tc, [arg_ty]) -> tc == listTyCon && isCharTy arg_ty
2036 _ -> False
2037
2038 -- | Is a type a 'CallStack'?
2039 isCallStackTy :: Type -> Bool
2040 isCallStackTy ty
2041 | Just tc <- tyConAppTyCon_maybe ty
2042 = tc `hasKey` callStackTyConKey
2043 | otherwise
2044 = False
2045
2046 -- | Is a 'PredType' a 'CallStack' implicit parameter?
2047 --
2048 -- If so, return the name of the parameter.
2049 isCallStackPred :: PredType -> Maybe FastString
2050 isCallStackPred pred
2051 | Just (str, ty) <- isIPPred_maybe pred
2052 , isCallStackTy ty
2053 = Just str
2054 | otherwise
2055 = Nothing
2056
2057 is_tc :: Unique -> Type -> Bool
2058 -- Newtypes are opaque to this
2059 is_tc uniq ty = case tcSplitTyConApp_maybe ty of
2060 Just (tc, _) -> uniq == getUnique tc
2061 Nothing -> False
2062
2063 -- | Does the given tyvar appear in the given type outside of any
2064 -- non-newtypes? Assume we're looking for @a@. Says "yes" for
2065 -- @a@, @N a@, @b a@, @a b@, @b (N a)@. Says "no" for
2066 -- @[a]@, @Maybe a@, @T a@, where @N@ is a newtype and @T@ is a datatype.
2067 isTyVarExposed :: TcTyVar -> TcType -> Bool
2068 isTyVarExposed tv (TyVarTy tv') = tv == tv'
2069 isTyVarExposed tv (TyConApp tc tys)
2070 | isNewTyCon tc = any (isTyVarExposed tv) tys
2071 | otherwise = False
2072 isTyVarExposed _ (LitTy {}) = False
2073 isTyVarExposed tv (AppTy fun arg) = isTyVarExposed tv fun
2074 || isTyVarExposed tv arg
2075 isTyVarExposed _ (ForAllTy {}) = False
2076 isTyVarExposed tv (CastTy ty _) = isTyVarExposed tv ty
2077 isTyVarExposed _ (CoercionTy {}) = False
2078
2079 -- | Does the given tyvar appear under a type generative w.r.t.
2080 -- representational equality? See Note [Occurs check error] in
2081 -- TcCanonical for the motivation for this function.
2082 isTyVarUnderDatatype :: TcTyVar -> TcType -> Bool
2083 isTyVarUnderDatatype tv = go False
2084 where
2085 go under_dt ty | Just ty' <- coreView ty = go under_dt ty'
2086 go under_dt (TyVarTy tv') = under_dt && (tv == tv')
2087 go under_dt (TyConApp tc tys) = let under_dt' = under_dt ||
2088 isGenerativeTyCon tc
2089 Representational
2090 in any (go under_dt') tys
2091 go _ (LitTy {}) = False
2092 go _ (ForAllTy (Anon arg) res) = go True arg || go True res
2093 go under_dt (AppTy fun arg) = go under_dt fun || go under_dt arg
2094 go under_dt (ForAllTy (Named tv' _) inner_ty)
2095 | tv' == tv = False
2096 | otherwise = go under_dt inner_ty
2097 go under_dt (CastTy ty _) = go under_dt ty
2098 go _ (CoercionTy {}) = False
2099
2100 isRigidTy :: TcType -> Bool
2101 isRigidTy ty
2102 | Just (tc,_) <- tcSplitTyConApp_maybe ty = isGenerativeTyCon tc Nominal
2103 | Just {} <- tcSplitAppTy_maybe ty = True
2104 | isForAllTy ty = True
2105 | otherwise = False
2106
2107 isRigidEqPred :: TcLevel -> PredTree -> Bool
2108 -- ^ True of all Nominal equalities that are solidly insoluble
2109 -- This means all equalities *except*
2110 -- * Meta-tv non-SigTv on LHS
2111 -- * Meta-tv SigTv on LHS, tyvar on right
2112 isRigidEqPred tc_lvl (EqPred NomEq ty1 _)
2113 | Just tv1 <- tcGetTyVar_maybe ty1
2114 = ASSERT2( isTcTyVar tv1, ppr tv1 )
2115 not (isMetaTyVar tv1) || isTouchableMetaTyVar tc_lvl tv1
2116
2117 | otherwise -- LHS is not a tyvar
2118 = True
2119
2120 isRigidEqPred _ _ = False -- Not an equality
2121
2122 {-
2123 ************************************************************************
2124 * *
2125 \subsection{Transformation of Types to TcTypes}
2126 * *
2127 ************************************************************************
2128 -}
2129
2130 toTcType :: Type -> TcType
2131 -- The constraint solver expects EvVars to have TcType, in which the
2132 -- free type variables are TcTyVars. So we convert from Type to TcType here
2133 -- A bit tiresome; but one day I expect the two types to be entirely separate
2134 -- in which case we'll definitely need to do this
2135 toTcType = runIdentity . to_tc_type emptyVarSet
2136
2137 toTcTypeBag :: Bag EvVar -> Bag EvVar -- All TyVars are transformed to TcTyVars
2138 toTcTypeBag evvars = mapBag (\tv -> setTyVarKind tv (toTcType (tyVarKind tv))) evvars
2139
2140 to_tc_mapper :: TyCoMapper VarSet Identity
2141 to_tc_mapper
2142 = TyCoMapper { tcm_smart = False -- more efficient not to use smart ctors
2143 , tcm_tyvar = tyvar
2144 , tcm_covar = covar
2145 , tcm_hole = hole
2146 , tcm_tybinder = tybinder }
2147 where
2148 tyvar :: VarSet -> TyVar -> Identity Type
2149 tyvar ftvs tv
2150 | Just var <- lookupVarSet ftvs tv = return $ TyVarTy var
2151 | isTcTyVar tv = TyVarTy <$> updateTyVarKindM (to_tc_type ftvs) tv
2152 | otherwise
2153 = do { kind' <- to_tc_type ftvs (tyVarKind tv)
2154 ; return $ TyVarTy $ mkTcTyVar (tyVarName tv) kind' vanillaSkolemTv }
2155
2156 covar :: VarSet -> CoVar -> Identity Coercion
2157 covar ftvs cv
2158 | Just var <- lookupVarSet ftvs cv = return $ CoVarCo var
2159 | otherwise = CoVarCo <$> updateVarTypeM (to_tc_type ftvs) cv
2160
2161 hole :: VarSet -> CoercionHole -> Role -> Type -> Type
2162 -> Identity Coercion
2163 hole ftvs h r t1 t2 = mkHoleCo h r <$> to_tc_type ftvs t1
2164 <*> to_tc_type ftvs t2
2165
2166 tybinder :: VarSet -> TyVar -> VisibilityFlag -> Identity (VarSet, TyVar)
2167 tybinder ftvs tv _vis = do { kind' <- to_tc_type ftvs (tyVarKind tv)
2168 ; let tv' = mkTcTyVar (tyVarName tv) kind'
2169 vanillaSkolemTv
2170 ; return (ftvs `extendVarSet` tv', tv') }
2171
2172 to_tc_type :: VarSet -> Type -> Identity TcType
2173 to_tc_type = mapType to_tc_mapper
2174
2175 {-
2176 ************************************************************************
2177 * *
2178 \subsection{Misc}
2179 * *
2180 ************************************************************************
2181
2182 Note [Visible type application]
2183 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2184 GHC implements a generalisation of the algorithm described in the
2185 "Visible Type Application" paper (available from
2186 http://www.cis.upenn.edu/~sweirich/publications.html). A key part
2187 of that algorithm is to distinguish user-specified variables from inferred
2188 variables. For example, the following should typecheck:
2189
2190 f :: forall a b. a -> b -> b
2191 f = const id
2192
2193 g = const id
2194
2195 x = f @Int @Bool 5 False
2196 y = g 5 @Bool False
2197
2198 The idea is that we wish to allow visible type application when we are
2199 instantiating a specified, fixed variable. In practice, specified, fixed
2200 variables are either written in a type signature (or
2201 annotation), OR are imported from another module. (We could do better here,
2202 for example by doing SCC analysis on parts of a module and considering any
2203 type from outside one's SCC to be fully specified, but this is very confusing to
2204 users. The simple rule above is much more straightforward and predictable.)
2205
2206 So, both of f's quantified variables are specified and may be instantiated.
2207 But g has no type signature, so only id's variable is specified (because id
2208 is imported). We write the type of g as forall {a}. a -> forall b. b -> b.
2209 Note that the a is in braces, meaning it cannot be instantiated with
2210 visible type application.
2211
2212 Tracking specified vs. inferred variables is done conveniently by a field
2213 in TyBinder.
2214
2215 -}
2216
2217 deNoteType :: Type -> Type
2218 -- Remove all *outermost* type synonyms and other notes
2219 deNoteType ty | Just ty' <- coreView ty = deNoteType ty'
2220 deNoteType ty = ty
2221
2222 {-
2223 Find the free tycons and classes of a type. This is used in the front
2224 end of the compiler.
2225 -}
2226
2227 {-
2228 ************************************************************************
2229 * *
2230 \subsection[TysWiredIn-ext-type]{External types}
2231 * *
2232 ************************************************************************
2233
2234 The compiler's foreign function interface supports the passing of a
2235 restricted set of types as arguments and results (the restricting factor
2236 being the )
2237 -}
2238
2239 tcSplitIOType_maybe :: Type -> Maybe (TyCon, Type)
2240 -- (tcSplitIOType_maybe t) returns Just (IO,t',co)
2241 -- if co : t ~ IO t'
2242 -- returns Nothing otherwise
2243 tcSplitIOType_maybe ty
2244 = case tcSplitTyConApp_maybe ty of
2245 Just (io_tycon, [io_res_ty])
2246 | io_tycon `hasKey` ioTyConKey ->
2247 Just (io_tycon, io_res_ty)
2248 _ ->
2249 Nothing
2250
2251 isFFITy :: Type -> Bool
2252 -- True for any TyCon that can possibly be an arg or result of an FFI call
2253 isFFITy ty = isValid (checkRepTyCon legalFFITyCon ty)
2254
2255 isFFIArgumentTy :: DynFlags -> Safety -> Type -> Validity
2256 -- Checks for valid argument type for a 'foreign import'
2257 isFFIArgumentTy dflags safety ty
2258 = checkRepTyCon (legalOutgoingTyCon dflags safety) ty
2259
2260 isFFIExternalTy :: Type -> Validity
2261 -- Types that are allowed as arguments of a 'foreign export'
2262 isFFIExternalTy ty = checkRepTyCon legalFEArgTyCon ty
2263
2264 isFFIImportResultTy :: DynFlags -> Type -> Validity
2265 isFFIImportResultTy dflags ty
2266 = checkRepTyCon (legalFIResultTyCon dflags) ty
2267
2268 isFFIExportResultTy :: Type -> Validity
2269 isFFIExportResultTy ty = checkRepTyCon legalFEResultTyCon ty
2270
2271 isFFIDynTy :: Type -> Type -> Validity
2272 -- The type in a foreign import dynamic must be Ptr, FunPtr, or a newtype of
2273 -- either, and the wrapped function type must be equal to the given type.
2274 -- We assume that all types have been run through normaliseFfiType, so we don't
2275 -- need to worry about expanding newtypes here.
2276 isFFIDynTy expected ty
2277 -- Note [Foreign import dynamic]
2278 -- In the example below, expected would be 'CInt -> IO ()', while ty would
2279 -- be 'FunPtr (CDouble -> IO ())'.
2280 | Just (tc, [ty']) <- splitTyConApp_maybe ty
2281 , tyConUnique tc `elem` [ptrTyConKey, funPtrTyConKey]
2282 , eqType ty' expected
2283 = IsValid
2284 | otherwise
2285 = NotValid (vcat [ text "Expected: Ptr/FunPtr" <+> pprParendType expected <> comma
2286 , text " Actual:" <+> ppr ty ])
2287
2288 isFFILabelTy :: Type -> Validity
2289 -- The type of a foreign label must be Ptr, FunPtr, or a newtype of either.
2290 isFFILabelTy ty = checkRepTyCon ok ty
2291 where
2292 ok tc | tc `hasKey` funPtrTyConKey || tc `hasKey` ptrTyConKey
2293 = IsValid
2294 | otherwise
2295 = NotValid (text "A foreign-imported address (via &foo) must have type (Ptr a) or (FunPtr a)")
2296
2297 isFFIPrimArgumentTy :: DynFlags -> Type -> Validity
2298 -- Checks for valid argument type for a 'foreign import prim'
2299 -- Currently they must all be simple unlifted types, or the well-known type
2300 -- Any, which can be used to pass the address to a Haskell object on the heap to
2301 -- the foreign function.
2302 isFFIPrimArgumentTy dflags ty
2303 | isAnyTy ty = IsValid
2304 | otherwise = checkRepTyCon (legalFIPrimArgTyCon dflags) ty
2305
2306 isFFIPrimResultTy :: DynFlags -> Type -> Validity
2307 -- Checks for valid result type for a 'foreign import prim'
2308 -- Currently it must be an unlifted type, including unboxed tuples,
2309 -- or the well-known type Any.
2310 isFFIPrimResultTy dflags ty
2311 | isAnyTy ty = IsValid
2312 | otherwise = checkRepTyCon (legalFIPrimResultTyCon dflags) ty
2313
2314 isFunPtrTy :: Type -> Bool
2315 isFunPtrTy ty
2316 | Just (tc, [_]) <- splitTyConApp_maybe ty
2317 = tc `hasKey` funPtrTyConKey
2318 | otherwise
2319 = False
2320
2321 -- normaliseFfiType gets run before checkRepTyCon, so we don't
2322 -- need to worry about looking through newtypes or type functions
2323 -- here; that's already been taken care of.
2324 checkRepTyCon :: (TyCon -> Validity) -> Type -> Validity
2325 checkRepTyCon check_tc ty
2326 = case splitTyConApp_maybe ty of
2327 Just (tc, tys)
2328 | isNewTyCon tc -> NotValid (hang msg 2 (mk_nt_reason tc tys $$ nt_fix))
2329 | otherwise -> case check_tc tc of
2330 IsValid -> IsValid
2331 NotValid extra -> NotValid (msg $$ extra)
2332 Nothing -> NotValid (quotes (ppr ty) <+> text "is not a data type")
2333 where
2334 msg = quotes (ppr ty) <+> text "cannot be marshalled in a foreign call"
2335 mk_nt_reason tc tys
2336 | null tys = text "because its data constructor is not in scope"
2337 | otherwise = text "because the data constructor for"
2338 <+> quotes (ppr tc) <+> text "is not in scope"
2339 nt_fix = text "Possible fix: import the data constructor to bring it into scope"
2340
2341 {-
2342 Note [Foreign import dynamic]
2343 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2344 A dynamic stub must be of the form 'FunPtr ft -> ft' where ft is any foreign
2345 type. Similarly, a wrapper stub must be of the form 'ft -> IO (FunPtr ft)'.
2346
2347 We use isFFIDynTy to check whether a signature is well-formed. For example,
2348 given a (illegal) declaration like:
2349
2350 foreign import ccall "dynamic"
2351 foo :: FunPtr (CDouble -> IO ()) -> CInt -> IO ()
2352
2353 isFFIDynTy will compare the 'FunPtr' type 'CDouble -> IO ()' with the curried
2354 result type 'CInt -> IO ()', and return False, as they are not equal.
2355
2356
2357 ----------------------------------------------
2358 These chaps do the work; they are not exported
2359 ----------------------------------------------
2360 -}
2361
2362 legalFEArgTyCon :: TyCon -> Validity
2363 legalFEArgTyCon tc
2364 -- It's illegal to make foreign exports that take unboxed
2365 -- arguments. The RTS API currently can't invoke such things. --SDM 7/2000
2366 = boxedMarshalableTyCon tc
2367
2368 legalFIResultTyCon :: DynFlags -> TyCon -> Validity
2369 legalFIResultTyCon dflags tc
2370 | tc == unitTyCon = IsValid
2371 | otherwise = marshalableTyCon dflags tc
2372
2373 legalFEResultTyCon :: TyCon -> Validity
2374 legalFEResultTyCon tc
2375 | tc == unitTyCon = IsValid
2376 | otherwise = boxedMarshalableTyCon tc
2377
2378 legalOutgoingTyCon :: DynFlags -> Safety -> TyCon -> Validity
2379 -- Checks validity of types going from Haskell -> external world
2380 legalOutgoingTyCon dflags _ tc
2381 = marshalableTyCon dflags tc
2382
2383 legalFFITyCon :: TyCon -> Validity
2384 -- True for any TyCon that can possibly be an arg or result of an FFI call
2385 legalFFITyCon tc
2386 | isUnliftedTyCon tc = IsValid
2387 | tc == unitTyCon = IsValid
2388 | otherwise = boxedMarshalableTyCon tc
2389
2390 marshalableTyCon :: DynFlags -> TyCon -> Validity
2391 marshalableTyCon dflags tc
2392 | isUnliftedTyCon tc
2393 , not (isUnboxedTupleTyCon tc)
2394 , case tyConPrimRep tc of -- Note [Marshalling VoidRep]
2395 VoidRep -> False
2396 _ -> True
2397 = validIfUnliftedFFITypes dflags
2398 | otherwise
2399 = boxedMarshalableTyCon tc
2400
2401 boxedMarshalableTyCon :: TyCon -> Validity
2402 boxedMarshalableTyCon tc
2403 | getUnique tc `elem` [ intTyConKey, int8TyConKey, int16TyConKey
2404 , int32TyConKey, int64TyConKey
2405 , wordTyConKey, word8TyConKey, word16TyConKey
2406 , word32TyConKey, word64TyConKey
2407 , floatTyConKey, doubleTyConKey
2408 , ptrTyConKey, funPtrTyConKey
2409 , charTyConKey
2410 , stablePtrTyConKey
2411 , boolTyConKey
2412 ]
2413 = IsValid
2414
2415 | otherwise = NotValid empty
2416
2417 legalFIPrimArgTyCon :: DynFlags -> TyCon -> Validity
2418 -- Check args of 'foreign import prim', only allow simple unlifted types.
2419 -- Strictly speaking it is unnecessary to ban unboxed tuples here since
2420 -- currently they're of the wrong kind to use in function args anyway.
2421 legalFIPrimArgTyCon dflags tc
2422 | isUnliftedTyCon tc
2423 , not (isUnboxedTupleTyCon tc)
2424 = validIfUnliftedFFITypes dflags
2425 | otherwise
2426 = NotValid unlifted_only
2427
2428 legalFIPrimResultTyCon :: DynFlags -> TyCon -> Validity
2429 -- Check result type of 'foreign import prim'. Allow simple unlifted
2430 -- types and also unboxed tuple result types '... -> (# , , #)'
2431 legalFIPrimResultTyCon dflags tc
2432 | isUnliftedTyCon tc
2433 , (isUnboxedTupleTyCon tc
2434 || case tyConPrimRep tc of -- Note [Marshalling VoidRep]
2435 VoidRep -> False
2436 _ -> True)
2437 = validIfUnliftedFFITypes dflags
2438
2439 | otherwise
2440 = NotValid unlifted_only
2441
2442 unlifted_only :: MsgDoc
2443 unlifted_only = text "foreign import prim only accepts simple unlifted types"
2444
2445 validIfUnliftedFFITypes :: DynFlags -> Validity
2446 validIfUnliftedFFITypes dflags
2447 | xopt LangExt.UnliftedFFITypes dflags = IsValid
2448 | otherwise = NotValid (text "To marshal unlifted types, use UnliftedFFITypes")
2449
2450 {-
2451 Note [Marshalling VoidRep]
2452 ~~~~~~~~~~~~~~~~~~~~~~~~~~
2453 We don't treat State# (whose PrimRep is VoidRep) as marshalable.
2454 In turn that means you can't write
2455 foreign import foo :: Int -> State# RealWorld
2456
2457 Reason: the back end falls over with panic "primRepHint:VoidRep";
2458 and there is no compelling reason to permit it
2459 -}
2460
2461 {-
2462 ************************************************************************
2463 * *
2464 The "Paterson size" of a type
2465 * *
2466 ************************************************************************
2467 -}
2468
2469 {-
2470 Note [Paterson conditions on PredTypes]
2471 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2472 We are considering whether *class* constraints terminate
2473 (see Note [Paterson conditions]). Precisely, the Paterson conditions
2474 would have us check that "the constraint has fewer constructors and variables
2475 (taken together and counting repetitions) than the head.".
2476
2477 However, we can be a bit more refined by looking at which kind of constraint
2478 this actually is. There are two main tricks:
2479
2480 1. It seems like it should be OK not to count the tuple type constructor
2481 for a PredType like (Show a, Eq a) :: Constraint, since we don't
2482 count the "implicit" tuple in the ThetaType itself.
2483
2484 In fact, the Paterson test just checks *each component* of the top level
2485 ThetaType against the size bound, one at a time. By analogy, it should be
2486 OK to return the size of the *largest* tuple component as the size of the
2487 whole tuple.
2488
2489 2. Once we get into an implicit parameter or equality we
2490 can't get back to a class constraint, so it's safe
2491 to say "size 0". See Trac #4200.
2492
2493 NB: we don't want to detect PredTypes in sizeType (and then call
2494 sizePred on them), or we might get an infinite loop if that PredType
2495 is irreducible. See Trac #5581.
2496 -}
2497
2498 type TypeSize = IntWithInf
2499
2500 sizeType :: Type -> TypeSize
2501 -- Size of a type: the number of variables and constructors
2502 -- Ignore kinds altogether
2503 sizeType = go
2504 where
2505 go ty | Just exp_ty <- coreView ty = go exp_ty
2506 go (TyVarTy {}) = 1
2507 go (TyConApp tc tys)
2508 | isTypeFamilyTyCon tc = infinity -- Type-family applications can
2509 -- expand to any arbitrary size
2510 | otherwise = sizeTypes (filterOutInvisibleTypes tc tys) + 1
2511 go (LitTy {}) = 1
2512 go (ForAllTy (Anon arg) res) = go arg + go res + 1
2513 go (AppTy fun arg) = go fun + go arg
2514 go (ForAllTy (Named tv vis) ty)
2515 | Visible <- vis = go (tyVarKind tv) + go ty + 1
2516 | otherwise = go ty + 1
2517 go (CastTy ty _) = go ty
2518 go (CoercionTy {}) = 0
2519
2520 sizeTypes :: [Type] -> TypeSize
2521 sizeTypes tys = sum (map sizeType tys)