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