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