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