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