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