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