Implement -fprint-expanded-synonyms
[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 #-}
19
20 module TcType (
21 --------------------------------
22 -- Types
23 TcType, TcSigmaType, TcRhoType, TcTauType, TcPredType, TcThetaType,
24 TcTyVar, TcTyVarSet, TcKind, TcCoVar,
25
26 -- TcLevel
27 TcLevel(..), topTcLevel, pushTcLevel,
28 strictlyDeeperThan, sameDepthAs, fmvTcLevel,
29
30 --------------------------------
31 -- MetaDetails
32 UserTypeCtxt(..), pprUserTypeCtxt, pprSigCtxt,
33 TcTyVarDetails(..), pprTcTyVarDetails, vanillaSkolemTv, superSkolemTv,
34 MetaDetails(Flexi, Indirect), MetaInfo(..),
35 isImmutableTyVar, isSkolemTyVar, isMetaTyVar, isMetaTyVarTy, isTyVarTy,
36 isSigTyVar, isOverlappableTyVar, isTyConableTyVar,
37 isFskTyVar, isFmvTyVar, isFlattenTyVar, isReturnTyVar,
38 isAmbiguousTyVar, metaTvRef, metaTyVarInfo,
39 isFlexi, isIndirect, isRuntimeUnkSkol,
40 isTypeVar, isKindVar,
41 metaTyVarTcLevel, setMetaTyVarTcLevel, metaTyVarTcLevel_maybe,
42 isTouchableMetaTyVar, isTouchableOrFmv,
43 isFloatedTouchableMetaTyVar,
44 canUnifyWithPolyType,
45
46 --------------------------------
47 -- Builders
48 mkPhiTy, mkSigmaTy, mkTcEqPred, mkTcReprEqPred, mkTcEqPredRole,
49
50 --------------------------------
51 -- Splitters
52 -- These are important because they do not look through newtypes
53 tcView,
54 tcSplitForAllTys, tcSplitPhiTy, tcSplitPredFunTy_maybe,
55 tcSplitFunTy_maybe, tcSplitFunTys, tcFunArgTy, tcFunResultTy, tcSplitFunTysN,
56 tcSplitTyConApp, tcSplitTyConApp_maybe, tcTyConAppTyCon, tcTyConAppArgs,
57 tcSplitAppTy_maybe, tcSplitAppTy, tcSplitAppTys, repSplitAppTy_maybe,
58 tcInstHeadTyNotSynonym, tcInstHeadTyAppAllTyVars,
59 tcGetTyVar_maybe, tcGetTyVar, nextRole,
60 tcSplitSigmaTy, tcDeepSplitSigmaTy_maybe,
61
62 ---------------------------------
63 -- Predicates.
64 -- Again, newtypes are opaque
65 eqType, eqTypes, eqPred, cmpType, cmpTypes, cmpPred, eqTypeX,
66 tcEqType, tcEqKind,
67 isSigmaTy, isRhoTy, isOverloadedTy,
68 isDoubleTy, isFloatTy, isIntTy, isWordTy, isStringTy,
69 isIntegerTy, isBoolTy, isUnitTy, isCharTy,
70 isTauTy, isTauTyCon, tcIsTyVarTy, tcIsForAllTy,
71 isPredTy, isTyVarClassPred, isTyVarExposed,
72 checkValidClsArgs, hasTyVarHead,
73 isRigidEqPred, isRigidTy,
74
75 ---------------------------------
76 -- Misc type manipulators
77 deNoteType, occurCheckExpand, OccCheckResult(..),
78 orphNamesOfType, orphNamesOfDFunHead, orphNamesOfCo,
79 orphNamesOfTypes, orphNamesOfCoCon,
80 getDFunTyKey,
81 evVarPred_maybe, evVarPred,
82
83 ---------------------------------
84 -- Predicate types
85 mkMinimalBySCs, transSuperClasses, transSuperClassesPred,
86 immSuperClasses,
87 isImprovementPred,
88
89 -- * Finding type instances
90 tcTyFamInsts,
91
92 -- * Finding "exact" (non-dead) type variables
93 exactTyVarsOfType, exactTyVarsOfTypes,
94
95 ---------------------------------
96 -- Foreign import and export
97 isFFIArgumentTy, -- :: DynFlags -> Safety -> Type -> Bool
98 isFFIImportResultTy, -- :: DynFlags -> Type -> Bool
99 isFFIExportResultTy, -- :: Type -> Bool
100 isFFIExternalTy, -- :: Type -> Bool
101 isFFIDynTy, -- :: Type -> Type -> Bool
102 isFFIPrimArgumentTy, -- :: DynFlags -> Type -> Bool
103 isFFIPrimResultTy, -- :: DynFlags -> Type -> Bool
104 isFFILabelTy, -- :: Type -> Bool
105 isFFITy, -- :: Type -> Bool
106 isFunPtrTy, -- :: Type -> Bool
107 tcSplitIOType_maybe, -- :: Type -> Maybe Type
108
109 --------------------------------
110 -- Rexported from Kind
111 Kind, typeKind,
112 unliftedTypeKind, liftedTypeKind,
113 openTypeKind, constraintKind, mkArrowKind, mkArrowKinds,
114 isLiftedTypeKind, isUnliftedTypeKind, isSubOpenTypeKind,
115 tcIsSubKind, splitKindFunTys, defaultKind,
116
117 --------------------------------
118 -- Rexported from Type
119 Type, PredType, ThetaType,
120 mkForAllTy, mkForAllTys,
121 mkFunTy, mkFunTys, zipFunTys,
122 mkTyConApp, mkAppTy, mkAppTys, applyTy, applyTys,
123 mkTyVarTy, mkTyVarTys, mkTyConTy,
124
125 isClassPred, isEqPred, isIPPred,
126 mkClassPred,
127 isDictLikeTy,
128 tcSplitDFunTy, tcSplitDFunHead,
129 mkEqPred,
130
131 -- Type substitutions
132 TvSubst(..), -- Representation visible to a few friends
133 TvSubstEnv, emptyTvSubst,
134 mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst,
135 mkTopTvSubst, notElemTvSubst, unionTvSubst,
136 getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope,
137 Type.lookupTyVar, Type.extendTvSubst, Type.substTyVarBndr,
138 extendTvSubstList, isInScope, mkTvSubst, zipTyEnv,
139 Type.substTy, substTys, substTyWith, substTheta, substTyVar, substTyVars,
140
141 isUnLiftedType, -- Source types are always lifted
142 isUnboxedTupleType, -- Ditto
143 isPrimitiveType,
144
145 tyVarsOfType, tyVarsOfTypes, closeOverKinds,
146 tcTyVarsOfType, tcTyVarsOfTypes,
147
148 pprKind, pprParendKind, pprSigmaType,
149 pprType, pprParendType, pprTypeApp, pprTyThingCategory,
150 pprTheta, pprThetaArrowTy, pprClassPred,
151
152 TypeSize, sizeType, sizeTypes
153
154 ) where
155
156 #include "HsVersions.h"
157
158 -- friends:
159 import Kind
160 import TypeRep
161 import Class
162 import Var
163 import ForeignCall
164 import VarSet
165 import Coercion
166 import Type
167 import TyCon
168 import CoAxiom
169
170 -- others:
171 import DynFlags
172 import Name -- hiding (varName)
173 -- We use this to make dictionaries for type literals.
174 -- Perhaps there's a better way to do this?
175 import NameSet
176 import VarEnv
177 import PrelNames
178 import TysWiredIn
179 import BasicTypes
180 import Util
181 import Maybes
182 import ListSetOps
183 import Outputable
184 import FastString
185 import ErrUtils( Validity(..), MsgDoc, isValid )
186
187 import Data.IORef
188 import Control.Monad (liftM, ap)
189 #if __GLASGOW_HASKELL__ < 709
190 import Control.Applicative (Applicative(..))
191 #endif
192
193 {-
194 ************************************************************************
195 * *
196 \subsection{Types}
197 * *
198 ************************************************************************
199
200 The type checker divides the generic Type world into the
201 following more structured beasts:
202
203 sigma ::= forall tyvars. phi
204 -- A sigma type is a qualified type
205 --
206 -- Note that even if 'tyvars' is empty, theta
207 -- may not be: e.g. (?x::Int) => Int
208
209 -- Note that 'sigma' is in prenex form:
210 -- all the foralls are at the front.
211 -- A 'phi' type has no foralls to the right of
212 -- an arrow
213
214 phi :: theta => rho
215
216 rho ::= sigma -> rho
217 | tau
218
219 -- A 'tau' type has no quantification anywhere
220 -- Note that the args of a type constructor must be taus
221 tau ::= tyvar
222 | tycon tau_1 .. tau_n
223 | tau_1 tau_2
224 | tau_1 -> tau_2
225
226 -- In all cases, a (saturated) type synonym application is legal,
227 -- provided it expands to the required form.
228 -}
229
230 type TcTyVar = TyVar -- Used only during type inference
231 type TcCoVar = CoVar -- Used only during type inference; mutable
232 type TcType = Type -- A TcType can have mutable type variables
233 -- Invariant on ForAllTy in TcTypes:
234 -- forall a. T
235 -- a cannot occur inside a MutTyVar in T; that is,
236 -- T is "flattened" before quantifying over a
237
238 -- These types do not have boxy type variables in them
239 type TcPredType = PredType
240 type TcThetaType = ThetaType
241 type TcSigmaType = TcType
242 type TcRhoType = TcType -- Note [TcRhoType]
243 type TcTauType = TcType
244 type TcKind = Kind
245 type TcTyVarSet = TyVarSet
246
247 {-
248 Note [TcRhoType]
249 ~~~~~~~~~~~~~~~~
250 A TcRhoType has no foralls or contexts at the top, or to the right of an arrow
251 YES (forall a. a->a) -> Int
252 NO forall a. a -> Int
253 NO Eq a => a -> a
254 NO Int -> forall a. a -> Int
255
256
257 ************************************************************************
258 * *
259 \subsection{TyVarDetails}
260 * *
261 ************************************************************************
262
263 TyVarDetails gives extra info about type variables, used during type
264 checking. It's attached to mutable type variables only.
265 It's knot-tied back to Var.hs. There is no reason in principle
266 why Var.hs shouldn't actually have the definition, but it "belongs" here.
267
268 Note [Signature skolems]
269 ~~~~~~~~~~~~~~~~~~~~~~~~
270 Consider this
271
272 f :: forall a. [a] -> Int
273 f (x::b : xs) = 3
274
275 Here 'b' is a lexically scoped type variable, but it turns out to be
276 the same as the skolem 'a'. So we have a special kind of skolem
277 constant, SigTv, which can unify with other SigTvs. They are used
278 *only* for pattern type signatures.
279
280 Similarly consider
281 data T (a:k1) = MkT (S a)
282 data S (b:k2) = MkS (T b)
283 When doing kind inference on {S,T} we don't want *skolems* for k1,k2,
284 because they end up unifying; we want those SigTvs again.
285
286 Note [ReturnTv]
287 ~~~~~~~~~~~~~~~
288 We sometimes want to convert a checking algorithm into an inference
289 algorithm. An easy way to do this is to "check" that a term has a
290 metavariable as a type. But, we must be careful to allow that metavariable
291 to unify with *anything*. (Well, anything that doesn't fail an occurs-check.)
292 This is what ReturnTv means.
293
294 For example, if we have
295
296 (undefined :: (forall a. TF1 a ~ TF2 a => a)) x
297
298 we'll call (tcInfer . tcExpr) on the function expression. tcInfer will
299 create a ReturnTv to represent the expression's type. We really need this
300 ReturnTv to become set to (forall a. TF1 a ~ TF2 a => a) despite the fact
301 that this type mentions type families and is a polytype.
302
303 However, we must also be careful to make sure that the ReturnTvs really
304 always do get unified with something -- we don't want these floating
305 around in the solver. So, we check after running the checker to make
306 sure the ReturnTv is filled. If it's not, we set it to a TauTv.
307
308 We can't ASSERT that no ReturnTvs hit the solver, because they
309 can if there's, say, a kind error that stops checkTauTvUpdate from
310 working. This happens in test case typecheck/should_fail/T5570, for
311 example.
312
313 See also the commentary on #9404.
314 -}
315
316 -- A TyVarDetails is inside a TyVar
317 data TcTyVarDetails
318 = SkolemTv -- A skolem
319 Bool -- True <=> this skolem type variable can be overlapped
320 -- when looking up instances
321 -- See Note [Binding when looking up instances] in InstEnv
322
323 | FlatSkol -- A flatten-skolem. It stands for the TcType, and zonking
324 TcType -- will replace it by that type.
325 -- See Note [The flattening story] in TcFlatten
326
327 | RuntimeUnk -- Stands for an as-yet-unknown type in the GHCi
328 -- interactive context
329
330 | MetaTv { mtv_info :: MetaInfo
331 , mtv_ref :: IORef MetaDetails
332 , mtv_tclvl :: TcLevel } -- See Note [TcLevel and untouchable type variables]
333
334 vanillaSkolemTv, superSkolemTv :: TcTyVarDetails
335 -- See Note [Binding when looking up instances] in InstEnv
336 vanillaSkolemTv = SkolemTv False -- Might be instantiated
337 superSkolemTv = SkolemTv True -- Treat this as a completely distinct type
338
339 -----------------------------
340 data MetaDetails
341 = Flexi -- Flexi type variables unify to become Indirects
342 | Indirect TcType
343
344 instance Outputable MetaDetails where
345 ppr Flexi = ptext (sLit "Flexi")
346 ppr (Indirect ty) = ptext (sLit "Indirect") <+> ppr ty
347
348 data MetaInfo
349 = TauTv Bool -- This MetaTv is an ordinary unification variable
350 -- A TauTv is always filled in with a tau-type, which
351 -- never contains any ForAlls.
352 -- The boolean is true when the meta var originates
353 -- from a wildcard.
354
355 | ReturnTv -- Can unify with *anything*. Used to convert a
356 -- type "checking" algorithm into a type inference algorithm.
357 -- See Note [ReturnTv]
358
359 | SigTv -- A variant of TauTv, except that it should not be
360 -- unified with a type, only with a type variable
361 -- SigTvs are only distinguished to improve error messages
362 -- see Note [Signature skolems]
363 -- The MetaDetails, if filled in, will
364 -- always be another SigTv or a SkolemTv
365
366 | FlatMetaTv -- A flatten meta-tyvar
367 -- It is a meta-tyvar, but it is always untouchable, with level 0
368 -- See Note [The flattening story] in TcFlatten
369
370 -------------------------------------
371 -- UserTypeCtxt describes the origin of the polymorphic type
372 -- in the places where we need to an expression has that type
373
374 data UserTypeCtxt
375 = FunSigCtxt Name Bool -- Function type signature, when checking the type
376 -- Also used for types in SPECIALISE pragmas
377 -- Bool = True <=> report redundant class constraints
378 -- False <=> do not
379 -- See Note [Tracking redundant constraints] in TcSimplify
380
381 | InfSigCtxt Name -- Inferred type for function
382 | ExprSigCtxt -- Expression type signature
383 | ConArgCtxt Name -- Data constructor argument
384 | TySynCtxt Name -- RHS of a type synonym decl
385 | PatSigCtxt -- Type sig in pattern
386 -- eg f (x::t) = ...
387 -- or (x::t, y) = e
388 | RuleSigCtxt Name -- LHS of a RULE forall
389 -- RULE "foo" forall (x :: a -> a). f (Just x) = ...
390 | ResSigCtxt -- Result type sig
391 -- f x :: t = ....
392 | ForSigCtxt Name -- Foreign import or export signature
393 | DefaultDeclCtxt -- Types in a default declaration
394 | InstDeclCtxt -- An instance declaration
395 | SpecInstCtxt -- SPECIALISE instance pragma
396 | ThBrackCtxt -- Template Haskell type brackets [t| ... |]
397 | GenSigCtxt -- Higher-rank or impredicative situations
398 -- e.g. (f e) where f has a higher-rank type
399 -- We might want to elaborate this
400 | GhciCtxt -- GHCi command :kind <type>
401
402 | ClassSCCtxt Name -- Superclasses of a class
403 | SigmaCtxt -- Theta part of a normal for-all type
404 -- f :: <S> => a -> a
405 | DataTyCtxt Name -- Theta part of a data decl
406 -- data <S> => T a = MkT a
407
408 {-
409 -- Notes re TySynCtxt
410 -- We allow type synonyms that aren't types; e.g. type List = []
411 --
412 -- If the RHS mentions tyvars that aren't in scope, we'll
413 -- quantify over them:
414 -- e.g. type T = a->a
415 -- will become type T = forall a. a->a
416 --
417 -- With gla-exts that's right, but for H98 we should complain.
418
419
420 ************************************************************************
421 * *
422 Untoucable type variables
423 * *
424 ************************************************************************
425 -}
426
427 newtype TcLevel = TcLevel Int deriving( Eq, Ord )
428 -- See Note [TcLevel and untouchable type variables] for what this Int is
429
430 {-
431 Note [TcLevel and untouchable type variables]
432 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
433 * Each unification variable (MetaTv)
434 and each Implication
435 has a level number (of type TcLevel)
436
437 * INVARIANTS. In a tree of Implications,
438
439 (ImplicInv) The level number of an Implication is
440 STRICTLY GREATER THAN that of its parent
441
442 (MetaTvInv) The level number of a unification variable is
443 LESS THAN OR EQUAL TO that of its parent
444 implication
445
446 * A unification variable is *touchable* if its level number
447 is EQUAL TO that of its immediate parent implication.
448
449 * INVARIANT
450 (GivenInv) The free variables of the ic_given of an
451 implication are all untouchable; ie their level
452 numbers are LESS THAN the ic_tclvl of the implication
453
454
455 Note [Skolem escape prevention]
456 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
457 We only unify touchable unification variables. Because of
458 (MetaTvInv), there can be no occurrences of the variable further out,
459 so the unification can't cause the skolems to escape. Example:
460 data T = forall a. MkT a (a->Int)
461 f x (MkT v f) = length [v,x]
462 We decide (x::alpha), and generate an implication like
463 [1]forall a. (a ~ alpha[0])
464 But we must not unify alpha:=a, because the skolem would escape.
465
466 For the cases where we DO want to unify, we rely on floating the
467 equality. Example (with same T)
468 g x (MkT v f) = x && True
469 We decide (x::alpha), and generate an implication like
470 [1]forall a. (Bool ~ alpha[0])
471 We do NOT unify directly, bur rather float out (if the constraint
472 does not mention 'a') to get
473 (Bool ~ alpha[0]) /\ [1]forall a.()
474 and NOW we can unify alpha.
475
476 The same idea of only unifying touchables solves another problem.
477 Suppose we had
478 (F Int ~ uf[0]) /\ [1](forall a. C a => F Int ~ beta[1])
479 In this example, beta is touchable inside the implication. The
480 first solveSimpleWanteds step leaves 'uf' un-unified. Then we move inside
481 the implication where a new constraint
482 uf ~ beta
483 emerges. If we (wrongly) spontaneously solved it to get uf := beta,
484 the whole implication disappears but when we pop out again we are left with
485 (F Int ~ uf) which will be unified by our final zonking stage and
486 uf will get unified *once more* to (F Int).
487 -}
488
489 fmvTcLevel :: TcLevel -> TcLevel
490 fmvTcLevel (TcLevel n) = TcLevel (n-1)
491
492 topTcLevel :: TcLevel
493 topTcLevel = TcLevel 1 -- 1 = outermost level
494
495 pushTcLevel :: TcLevel -> TcLevel
496 pushTcLevel (TcLevel us) = TcLevel (us + 2)
497
498 strictlyDeeperThan :: TcLevel -> TcLevel -> Bool
499 strictlyDeeperThan (TcLevel tv_tclvl) (TcLevel ctxt_tclvl)
500 = tv_tclvl > ctxt_tclvl
501
502 sameDepthAs :: TcLevel -> TcLevel -> Bool
503 sameDepthAs (TcLevel ctxt_tclvl) (TcLevel tv_tclvl)
504 = ctxt_tclvl == tv_tclvl -- NB: invariant ctxt_tclvl >= tv_tclvl
505 -- So <= would be equivalent
506
507 checkTcLevelInvariant :: TcLevel -> TcLevel -> Bool
508 -- Checks (MetaTvInv) from Note [TcLevel and untouchable type variables]
509 checkTcLevelInvariant (TcLevel ctxt_tclvl) (TcLevel tv_tclvl)
510 = ctxt_tclvl >= tv_tclvl
511
512 instance Outputable TcLevel where
513 ppr (TcLevel us) = ppr us
514
515 {-
516 ************************************************************************
517 * *
518 Pretty-printing
519 * *
520 ************************************************************************
521 -}
522
523 pprTcTyVarDetails :: TcTyVarDetails -> SDoc
524 -- For debugging
525 pprTcTyVarDetails (SkolemTv True) = ptext (sLit "ssk")
526 pprTcTyVarDetails (SkolemTv False) = ptext (sLit "sk")
527 pprTcTyVarDetails (RuntimeUnk {}) = ptext (sLit "rt")
528 pprTcTyVarDetails (FlatSkol {}) = ptext (sLit "fsk")
529 pprTcTyVarDetails (MetaTv { mtv_info = info, mtv_tclvl = tclvl })
530 = pp_info <> colon <> ppr tclvl
531 where
532 pp_info = case info of
533 ReturnTv -> ptext (sLit "ret")
534 TauTv True -> ptext (sLit "twc")
535 TauTv False -> ptext (sLit "tau")
536 SigTv -> ptext (sLit "sig")
537 FlatMetaTv -> ptext (sLit "fuv")
538
539 pprUserTypeCtxt :: UserTypeCtxt -> SDoc
540 pprUserTypeCtxt (FunSigCtxt n _) = ptext (sLit "the type signature for") <+> quotes (ppr n)
541 pprUserTypeCtxt (InfSigCtxt n) = ptext (sLit "the inferred type for") <+> quotes (ppr n)
542 pprUserTypeCtxt (RuleSigCtxt n) = ptext (sLit "a RULE for") <+> quotes (ppr n)
543 pprUserTypeCtxt ExprSigCtxt = ptext (sLit "an expression type signature")
544 pprUserTypeCtxt (ConArgCtxt c) = ptext (sLit "the type of the constructor") <+> quotes (ppr c)
545 pprUserTypeCtxt (TySynCtxt c) = ptext (sLit "the RHS of the type synonym") <+> quotes (ppr c)
546 pprUserTypeCtxt ThBrackCtxt = ptext (sLit "a Template Haskell quotation [t|...|]")
547 pprUserTypeCtxt PatSigCtxt = ptext (sLit "a pattern type signature")
548 pprUserTypeCtxt ResSigCtxt = ptext (sLit "a result type signature")
549 pprUserTypeCtxt (ForSigCtxt n) = ptext (sLit "the foreign declaration for") <+> quotes (ppr n)
550 pprUserTypeCtxt DefaultDeclCtxt = ptext (sLit "a type in a `default' declaration")
551 pprUserTypeCtxt InstDeclCtxt = ptext (sLit "an instance declaration")
552 pprUserTypeCtxt SpecInstCtxt = ptext (sLit "a SPECIALISE instance pragma")
553 pprUserTypeCtxt GenSigCtxt = ptext (sLit "a type expected by the context")
554 pprUserTypeCtxt GhciCtxt = ptext (sLit "a type in a GHCi command")
555 pprUserTypeCtxt (ClassSCCtxt c) = ptext (sLit "the super-classes of class") <+> quotes (ppr c)
556 pprUserTypeCtxt SigmaCtxt = ptext (sLit "the context of a polymorphic type")
557 pprUserTypeCtxt (DataTyCtxt tc) = ptext (sLit "the context of the data type declaration for") <+> quotes (ppr tc)
558
559 pprSigCtxt :: UserTypeCtxt -> SDoc -> SDoc -> SDoc
560 -- (pprSigCtxt ctxt <extra> <type>)
561 -- prints In <extra> the type signature for 'f':
562 -- f :: <type>
563 -- The <extra> is either empty or "the ambiguity check for"
564 pprSigCtxt ctxt extra pp_ty
565 = sep [ ptext (sLit "In") <+> extra <+> pprUserTypeCtxt ctxt <> colon
566 , nest 2 (pp_sig ctxt) ]
567 where
568 pp_sig (FunSigCtxt n _) = pp_n_colon n
569 pp_sig (ConArgCtxt n) = pp_n_colon n
570 pp_sig (ForSigCtxt n) = pp_n_colon n
571 pp_sig _ = pp_ty
572
573 pp_n_colon n = pprPrefixOcc n <+> dcolon <+> pp_ty
574
575 {-
576 ************************************************************************
577 * *
578 Finding type family instances
579 * *
580 ************************************************************************
581 -}
582
583 -- | Finds outermost type-family applications occuring in a type,
584 -- after expanding synonyms.
585 tcTyFamInsts :: Type -> [(TyCon, [Type])]
586 tcTyFamInsts ty
587 | Just exp_ty <- tcView ty = tcTyFamInsts exp_ty
588 tcTyFamInsts (TyVarTy _) = []
589 tcTyFamInsts (TyConApp tc tys)
590 | isTypeFamilyTyCon tc = [(tc, tys)]
591 | otherwise = concat (map tcTyFamInsts tys)
592 tcTyFamInsts (LitTy {}) = []
593 tcTyFamInsts (FunTy ty1 ty2) = tcTyFamInsts ty1 ++ tcTyFamInsts ty2
594 tcTyFamInsts (AppTy ty1 ty2) = tcTyFamInsts ty1 ++ tcTyFamInsts ty2
595 tcTyFamInsts (ForAllTy _ ty) = tcTyFamInsts ty
596
597 {-
598 ************************************************************************
599 * *
600 The "exact" free variables of a type
601 * *
602 ************************************************************************
603
604 Note [Silly type synonym]
605 ~~~~~~~~~~~~~~~~~~~~~~~~~
606 Consider
607 type T a = Int
608 What are the free tyvars of (T x)? Empty, of course!
609 Here's the example that Ralf Laemmel showed me:
610 foo :: (forall a. C u a -> C u a) -> u
611 mappend :: Monoid u => u -> u -> u
612
613 bar :: Monoid u => u
614 bar = foo (\t -> t `mappend` t)
615 We have to generalise at the arg to f, and we don't
616 want to capture the constraint (Monad (C u a)) because
617 it appears to mention a. Pretty silly, but it was useful to him.
618
619 exactTyVarsOfType is used by the type checker to figure out exactly
620 which type variables are mentioned in a type. It's also used in the
621 smart-app checking code --- see TcExpr.tcIdApp
622
623 On the other hand, consider a *top-level* definition
624 f = (\x -> x) :: T a -> T a
625 If we don't abstract over 'a' it'll get fixed to GHC.Prim.Any, and then
626 if we have an application like (f "x") we get a confusing error message
627 involving Any. So the conclusion is this: when generalising
628 - at top level use tyVarsOfType
629 - in nested bindings use exactTyVarsOfType
630 See Trac #1813 for example.
631 -}
632
633 exactTyVarsOfType :: Type -> TyVarSet
634 -- Find the free type variables (of any kind)
635 -- but *expand* type synonyms. See Note [Silly type synonym] above.
636 exactTyVarsOfType ty
637 = go ty
638 where
639 go ty | Just ty' <- tcView ty = go ty' -- This is the key line
640 go (TyVarTy tv) = unitVarSet tv
641 go (TyConApp _ tys) = exactTyVarsOfTypes tys
642 go (LitTy {}) = emptyVarSet
643 go (FunTy arg res) = go arg `unionVarSet` go res
644 go (AppTy fun arg) = go fun `unionVarSet` go arg
645 go (ForAllTy tyvar ty) = delVarSet (go ty) tyvar
646
647 exactTyVarsOfTypes :: [Type] -> TyVarSet
648 exactTyVarsOfTypes = mapUnionVarSet exactTyVarsOfType
649
650 {-
651 ************************************************************************
652 * *
653 Predicates
654 * *
655 ************************************************************************
656 -}
657
658 isTouchableOrFmv :: TcLevel -> TcTyVar -> Bool
659 isTouchableOrFmv ctxt_tclvl tv
660 = ASSERT2( isTcTyVar tv, ppr tv )
661 case tcTyVarDetails tv of
662 MetaTv { mtv_tclvl = tv_tclvl, mtv_info = info }
663 -> ASSERT2( checkTcLevelInvariant ctxt_tclvl tv_tclvl,
664 ppr tv $$ ppr tv_tclvl $$ ppr ctxt_tclvl )
665 case info of
666 FlatMetaTv -> True
667 _ -> tv_tclvl `sameDepthAs` ctxt_tclvl
668 _ -> False
669
670 isTouchableMetaTyVar :: TcLevel -> TcTyVar -> Bool
671 isTouchableMetaTyVar ctxt_tclvl tv
672 = ASSERT2( isTcTyVar tv, ppr tv )
673 case tcTyVarDetails tv of
674 MetaTv { mtv_tclvl = tv_tclvl }
675 -> ASSERT2( checkTcLevelInvariant ctxt_tclvl tv_tclvl,
676 ppr tv $$ ppr tv_tclvl $$ ppr ctxt_tclvl )
677 tv_tclvl `sameDepthAs` ctxt_tclvl
678 _ -> False
679
680 isFloatedTouchableMetaTyVar :: TcLevel -> TcTyVar -> Bool
681 isFloatedTouchableMetaTyVar ctxt_tclvl tv
682 = ASSERT2( isTcTyVar tv, ppr tv )
683 case tcTyVarDetails tv of
684 MetaTv { mtv_tclvl = tv_tclvl } -> tv_tclvl `strictlyDeeperThan` ctxt_tclvl
685 _ -> False
686
687 isImmutableTyVar :: TyVar -> Bool
688 isImmutableTyVar tv
689 | isTcTyVar tv = isSkolemTyVar tv
690 | otherwise = True
691
692 isTyConableTyVar, isSkolemTyVar, isOverlappableTyVar,
693 isMetaTyVar, isAmbiguousTyVar,
694 isFmvTyVar, isFskTyVar, isFlattenTyVar, isReturnTyVar :: TcTyVar -> Bool
695
696 isTyConableTyVar tv
697 -- True of a meta-type variable that can be filled in
698 -- with a type constructor application; in particular,
699 -- not a SigTv
700 = ASSERT( isTcTyVar tv)
701 case tcTyVarDetails tv of
702 MetaTv { mtv_info = SigTv } -> False
703 _ -> True
704
705 isFmvTyVar tv
706 = ASSERT2( isTcTyVar tv, ppr tv )
707 case tcTyVarDetails tv of
708 MetaTv { mtv_info = FlatMetaTv } -> True
709 _ -> False
710
711 -- | True of both given and wanted flatten-skolems (fak and usk)
712 isFlattenTyVar tv
713 = ASSERT2( isTcTyVar tv, ppr tv )
714 case tcTyVarDetails tv of
715 FlatSkol {} -> True
716 MetaTv { mtv_info = FlatMetaTv } -> True
717 _ -> False
718
719 -- | True of FlatSkol skolems only
720 isFskTyVar tv
721 = ASSERT2( isTcTyVar tv, ppr tv )
722 case tcTyVarDetails tv of
723 FlatSkol {} -> True
724 _ -> False
725
726 isSkolemTyVar tv
727 = ASSERT2( isTcTyVar tv, ppr tv )
728 case tcTyVarDetails tv of
729 MetaTv {} -> False
730 _other -> True
731
732 isOverlappableTyVar tv
733 = ASSERT( isTcTyVar tv )
734 case tcTyVarDetails tv of
735 SkolemTv overlappable -> overlappable
736 _ -> False
737
738 isMetaTyVar tv
739 = ASSERT2( isTcTyVar tv, ppr tv )
740 case tcTyVarDetails tv of
741 MetaTv {} -> True
742 _ -> False
743
744 isReturnTyVar tv
745 = ASSERT2( isTcTyVar tv, ppr tv )
746 case tcTyVarDetails tv of
747 MetaTv { mtv_info = ReturnTv } -> True
748 _ -> False
749
750 -- isAmbiguousTyVar is used only when reporting type errors
751 -- It picks out variables that are unbound, namely meta
752 -- type variables and the RuntimUnk variables created by
753 -- RtClosureInspect.zonkRTTIType. These are "ambiguous" in
754 -- the sense that they stand for an as-yet-unknown type
755 isAmbiguousTyVar tv
756 = ASSERT2( isTcTyVar tv, ppr tv )
757 case tcTyVarDetails tv of
758 MetaTv {} -> True
759 RuntimeUnk {} -> True
760 _ -> False
761
762 isMetaTyVarTy :: TcType -> Bool
763 isMetaTyVarTy (TyVarTy tv) = isMetaTyVar tv
764 isMetaTyVarTy _ = False
765
766 metaTyVarInfo :: TcTyVar -> MetaInfo
767 metaTyVarInfo tv
768 = ASSERT( isTcTyVar tv )
769 case tcTyVarDetails tv of
770 MetaTv { mtv_info = info } -> info
771 _ -> pprPanic "metaTyVarInfo" (ppr tv)
772
773 metaTyVarTcLevel :: TcTyVar -> TcLevel
774 metaTyVarTcLevel tv
775 = ASSERT( isTcTyVar tv )
776 case tcTyVarDetails tv of
777 MetaTv { mtv_tclvl = tclvl } -> tclvl
778 _ -> pprPanic "metaTyVarTcLevel" (ppr tv)
779
780 metaTyVarTcLevel_maybe :: TcTyVar -> Maybe TcLevel
781 metaTyVarTcLevel_maybe tv
782 = ASSERT( isTcTyVar tv )
783 case tcTyVarDetails tv of
784 MetaTv { mtv_tclvl = tclvl } -> Just tclvl
785 _ -> Nothing
786
787 setMetaTyVarTcLevel :: TcTyVar -> TcLevel -> TcTyVar
788 setMetaTyVarTcLevel tv tclvl
789 = ASSERT( isTcTyVar tv )
790 case tcTyVarDetails tv of
791 details@(MetaTv {}) -> setTcTyVarDetails tv (details { mtv_tclvl = tclvl })
792 _ -> pprPanic "metaTyVarTcLevel" (ppr tv)
793
794 isSigTyVar :: Var -> Bool
795 isSigTyVar tv
796 = ASSERT( isTcTyVar tv )
797 case tcTyVarDetails tv of
798 MetaTv { mtv_info = SigTv } -> True
799 _ -> False
800
801 metaTvRef :: TyVar -> IORef MetaDetails
802 metaTvRef tv
803 = ASSERT2( isTcTyVar tv, ppr tv )
804 case tcTyVarDetails tv of
805 MetaTv { mtv_ref = ref } -> ref
806 _ -> pprPanic "metaTvRef" (ppr tv)
807
808 isFlexi, isIndirect :: MetaDetails -> Bool
809 isFlexi Flexi = True
810 isFlexi _ = False
811
812 isIndirect (Indirect _) = True
813 isIndirect _ = False
814
815 isRuntimeUnkSkol :: TyVar -> Bool
816 -- Called only in TcErrors; see Note [Runtime skolems] there
817 isRuntimeUnkSkol x
818 | isTcTyVar x, RuntimeUnk <- tcTyVarDetails x = True
819 | otherwise = False
820
821 {-
822 ************************************************************************
823 * *
824 \subsection{Tau, sigma and rho}
825 * *
826 ************************************************************************
827 -}
828
829 mkSigmaTy :: [TyVar] -> [PredType] -> Type -> Type
830 mkSigmaTy tyvars theta tau = mkForAllTys tyvars (mkPhiTy theta tau)
831
832 mkPhiTy :: [PredType] -> Type -> Type
833 mkPhiTy theta ty = foldr mkFunTy ty theta
834
835 mkTcEqPred :: TcType -> TcType -> Type
836 -- During type checking we build equalities between
837 -- type variables with OpenKind or ArgKind. Ultimately
838 -- they will all settle, but we want the equality predicate
839 -- itself to have kind '*'. I think.
840 --
841 -- But for now we call mkTyConApp, not mkEqPred, because the invariants
842 -- of the latter might not be satisfied during type checking.
843 -- Notably when we form an equalty (a : OpenKind) ~ (Int : *)
844 --
845 -- But this is horribly delicate: what about type variables
846 -- that turn out to be bound to Int#?
847 mkTcEqPred ty1 ty2
848 = mkTyConApp eqTyCon [k, ty1, ty2]
849 where
850 k = typeKind ty1
851
852 -- | Make a representational equality predicate
853 mkTcReprEqPred :: TcType -> TcType -> Type
854 mkTcReprEqPred ty1 ty2
855 = mkTyConApp coercibleTyCon [k, ty1, ty2]
856 where
857 k = typeKind ty1
858
859 -- | Make an equality predicate at a given role. The role must not be Phantom.
860 mkTcEqPredRole :: Role -> TcType -> TcType -> Type
861 mkTcEqPredRole Nominal = mkTcEqPred
862 mkTcEqPredRole Representational = mkTcReprEqPred
863 mkTcEqPredRole Phantom = panic "mkTcEqPredRole Phantom"
864
865 -- @isTauTy@ tests for nested for-alls.
866
867 isTauTy :: Type -> Bool
868 isTauTy ty | Just ty' <- tcView ty = isTauTy ty'
869 isTauTy (TyVarTy _) = True
870 isTauTy (LitTy {}) = True
871 isTauTy (TyConApp tc tys) = all isTauTy tys && isTauTyCon tc
872 isTauTy (AppTy a b) = isTauTy a && isTauTy b
873 isTauTy (FunTy a b) = isTauTy a && isTauTy b
874 isTauTy (ForAllTy {}) = False
875
876 isTauTyCon :: TyCon -> Bool
877 -- Returns False for type synonyms whose expansion is a polytype
878 isTauTyCon tc
879 | Just (_, rhs) <- synTyConDefn_maybe tc = isTauTy rhs
880 | otherwise = True
881
882 ---------------
883 getDFunTyKey :: Type -> OccName -- Get some string from a type, to be used to
884 -- construct a dictionary function name
885 getDFunTyKey ty | Just ty' <- tcView ty = getDFunTyKey ty'
886 getDFunTyKey (TyVarTy tv) = getOccName tv
887 getDFunTyKey (TyConApp tc _) = getOccName tc
888 getDFunTyKey (LitTy x) = getDFunTyLitKey x
889 getDFunTyKey (AppTy fun _) = getDFunTyKey fun
890 getDFunTyKey (FunTy _ _) = getOccName funTyCon
891 getDFunTyKey (ForAllTy _ t) = getDFunTyKey t
892
893 getDFunTyLitKey :: TyLit -> OccName
894 getDFunTyLitKey (NumTyLit n) = mkOccName Name.varName (show n)
895 getDFunTyLitKey (StrTyLit n) = mkOccName Name.varName (show n) -- hm
896
897 {-
898 ************************************************************************
899 * *
900 \subsection{Expanding and splitting}
901 * *
902 ************************************************************************
903
904 These tcSplit functions are like their non-Tc analogues, but
905 *) they do not look through newtypes
906
907 However, they are non-monadic and do not follow through mutable type
908 variables. It's up to you to make sure this doesn't matter.
909 -}
910
911 tcSplitForAllTys :: Type -> ([TyVar], Type)
912 tcSplitForAllTys ty = split ty ty []
913 where
914 split orig_ty ty tvs | Just ty' <- tcView ty = split orig_ty ty' tvs
915 split _ (ForAllTy tv ty) tvs = split ty ty (tv:tvs)
916 split orig_ty _ tvs = (reverse tvs, orig_ty)
917
918 tcIsForAllTy :: Type -> Bool
919 tcIsForAllTy ty | Just ty' <- tcView ty = tcIsForAllTy ty'
920 tcIsForAllTy (ForAllTy {}) = True
921 tcIsForAllTy _ = False
922
923 tcSplitPredFunTy_maybe :: Type -> Maybe (PredType, Type)
924 -- Split off the first predicate argument from a type
925 tcSplitPredFunTy_maybe ty
926 | Just ty' <- tcView ty = tcSplitPredFunTy_maybe ty'
927 tcSplitPredFunTy_maybe (FunTy arg res)
928 | isPredTy arg = Just (arg, res)
929 tcSplitPredFunTy_maybe _
930 = Nothing
931
932 tcSplitPhiTy :: Type -> (ThetaType, Type)
933 tcSplitPhiTy ty
934 = split ty []
935 where
936 split ty ts
937 = case tcSplitPredFunTy_maybe ty of
938 Just (pred, ty) -> split ty (pred:ts)
939 Nothing -> (reverse ts, ty)
940
941 tcSplitSigmaTy :: Type -> ([TyVar], ThetaType, Type)
942 tcSplitSigmaTy ty = case tcSplitForAllTys ty of
943 (tvs, rho) -> case tcSplitPhiTy rho of
944 (theta, tau) -> (tvs, theta, tau)
945
946 -----------------------
947 tcDeepSplitSigmaTy_maybe
948 :: TcSigmaType -> Maybe ([TcType], [TyVar], ThetaType, TcSigmaType)
949 -- Looks for a *non-trivial* quantified type, under zero or more function arrows
950 -- By "non-trivial" we mean either tyvars or constraints are non-empty
951
952 tcDeepSplitSigmaTy_maybe ty
953 | Just (arg_ty, res_ty) <- tcSplitFunTy_maybe ty
954 , Just (arg_tys, tvs, theta, rho) <- tcDeepSplitSigmaTy_maybe res_ty
955 = Just (arg_ty:arg_tys, tvs, theta, rho)
956
957 | (tvs, theta, rho) <- tcSplitSigmaTy ty
958 , not (null tvs && null theta)
959 = Just ([], tvs, theta, rho)
960
961 | otherwise = Nothing
962
963 -----------------------
964 tcTyConAppTyCon :: Type -> TyCon
965 tcTyConAppTyCon ty = case tcSplitTyConApp_maybe ty of
966 Just (tc, _) -> tc
967 Nothing -> pprPanic "tcTyConAppTyCon" (pprType ty)
968
969 tcTyConAppArgs :: Type -> [Type]
970 tcTyConAppArgs ty = case tcSplitTyConApp_maybe ty of
971 Just (_, args) -> args
972 Nothing -> pprPanic "tcTyConAppArgs" (pprType ty)
973
974 tcSplitTyConApp :: Type -> (TyCon, [Type])
975 tcSplitTyConApp ty = case tcSplitTyConApp_maybe ty of
976 Just stuff -> stuff
977 Nothing -> pprPanic "tcSplitTyConApp" (pprType ty)
978
979 tcSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
980 tcSplitTyConApp_maybe ty | Just ty' <- tcView ty = tcSplitTyConApp_maybe ty'
981 tcSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
982 tcSplitTyConApp_maybe (FunTy arg res) = Just (funTyCon, [arg,res])
983 -- Newtypes are opaque, so they may be split
984 -- However, predicates are not treated
985 -- as tycon applications by the type checker
986 tcSplitTyConApp_maybe _ = Nothing
987
988 -----------------------
989 tcSplitFunTys :: Type -> ([Type], Type)
990 tcSplitFunTys ty = case tcSplitFunTy_maybe ty of
991 Nothing -> ([], ty)
992 Just (arg,res) -> (arg:args, res')
993 where
994 (args,res') = tcSplitFunTys res
995
996 tcSplitFunTy_maybe :: Type -> Maybe (Type, Type)
997 tcSplitFunTy_maybe ty | Just ty' <- tcView ty = tcSplitFunTy_maybe ty'
998 tcSplitFunTy_maybe (FunTy arg res) | not (isPredTy arg) = Just (arg, res)
999 tcSplitFunTy_maybe _ = Nothing
1000 -- Note the typeKind guard
1001 -- Consider (?x::Int) => Bool
1002 -- We don't want to treat this as a function type!
1003 -- A concrete example is test tc230:
1004 -- f :: () -> (?p :: ()) => () -> ()
1005 --
1006 -- g = f () ()
1007
1008 tcSplitFunTysN
1009 :: TcRhoType
1010 -> Arity -- N: Number of desired args
1011 -> ([TcSigmaType], -- Arg types (N or fewer)
1012 TcSigmaType) -- The rest of the type
1013
1014 tcSplitFunTysN ty n_args
1015 | n_args == 0
1016 = ([], ty)
1017 | Just (arg,res) <- tcSplitFunTy_maybe ty
1018 = case tcSplitFunTysN res (n_args - 1) of
1019 (args, res) -> (arg:args, res)
1020 | otherwise
1021 = ([], ty)
1022
1023 tcSplitFunTy :: Type -> (Type, Type)
1024 tcSplitFunTy ty = expectJust "tcSplitFunTy" (tcSplitFunTy_maybe ty)
1025
1026 tcFunArgTy :: Type -> Type
1027 tcFunArgTy ty = fst (tcSplitFunTy ty)
1028
1029 tcFunResultTy :: Type -> Type
1030 tcFunResultTy ty = snd (tcSplitFunTy ty)
1031
1032 -----------------------
1033 tcSplitAppTy_maybe :: Type -> Maybe (Type, Type)
1034 tcSplitAppTy_maybe ty | Just ty' <- tcView ty = tcSplitAppTy_maybe ty'
1035 tcSplitAppTy_maybe ty = repSplitAppTy_maybe ty
1036
1037 tcSplitAppTy :: Type -> (Type, Type)
1038 tcSplitAppTy ty = case tcSplitAppTy_maybe ty of
1039 Just stuff -> stuff
1040 Nothing -> pprPanic "tcSplitAppTy" (pprType ty)
1041
1042 tcSplitAppTys :: Type -> (Type, [Type])
1043 tcSplitAppTys ty
1044 = go ty []
1045 where
1046 go ty args = case tcSplitAppTy_maybe ty of
1047 Just (ty', arg) -> go ty' (arg:args)
1048 Nothing -> (ty,args)
1049
1050 -----------------------
1051 tcGetTyVar_maybe :: Type -> Maybe TyVar
1052 tcGetTyVar_maybe ty | Just ty' <- tcView ty = tcGetTyVar_maybe ty'
1053 tcGetTyVar_maybe (TyVarTy tv) = Just tv
1054 tcGetTyVar_maybe _ = Nothing
1055
1056 tcGetTyVar :: String -> Type -> TyVar
1057 tcGetTyVar msg ty = expectJust msg (tcGetTyVar_maybe ty)
1058
1059 tcIsTyVarTy :: Type -> Bool
1060 tcIsTyVarTy ty = isJust (tcGetTyVar_maybe ty)
1061
1062 -----------------------
1063 tcSplitDFunTy :: Type -> ([TyVar], [Type], Class, [Type])
1064 -- Split the type of a dictionary function
1065 -- We don't use tcSplitSigmaTy, because a DFun may (with NDP)
1066 -- have non-Pred arguments, such as
1067 -- df :: forall m. (forall b. Eq b => Eq (m b)) -> C m
1068 --
1069 -- Also NB splitFunTys, not tcSplitFunTys;
1070 -- the latter specifically stops at PredTy arguments,
1071 -- and we don't want to do that here
1072 tcSplitDFunTy ty
1073 = case tcSplitForAllTys ty of { (tvs, rho) ->
1074 case splitFunTys rho of { (theta, tau) ->
1075 case tcSplitDFunHead tau of { (clas, tys) ->
1076 (tvs, theta, clas, tys) }}}
1077
1078 tcSplitDFunHead :: Type -> (Class, [Type])
1079 tcSplitDFunHead = getClassPredTys
1080
1081 tcInstHeadTyNotSynonym :: Type -> Bool
1082 -- Used in Haskell-98 mode, for the argument types of an instance head
1083 -- These must not be type synonyms, but everywhere else type synonyms
1084 -- are transparent, so we need a special function here
1085 tcInstHeadTyNotSynonym ty
1086 = case ty of
1087 TyConApp tc _ -> not (isTypeSynonymTyCon tc)
1088 _ -> True
1089
1090 tcInstHeadTyAppAllTyVars :: Type -> Bool
1091 -- Used in Haskell-98 mode, for the argument types of an instance head
1092 -- These must be a constructor applied to type variable arguments.
1093 -- But we allow kind instantiations.
1094 tcInstHeadTyAppAllTyVars ty
1095 | Just ty' <- tcView ty -- Look through synonyms
1096 = tcInstHeadTyAppAllTyVars ty'
1097 | otherwise
1098 = case ty of
1099 TyConApp _ tys -> ok (filter (not . isKind) tys) -- avoid kinds
1100 FunTy arg res -> ok [arg, res]
1101 _ -> False
1102 where
1103 -- Check that all the types are type variables,
1104 -- and that each is distinct
1105 ok tys = equalLength tvs tys && hasNoDups tvs
1106 where
1107 tvs = mapMaybe get_tv tys
1108
1109 get_tv (TyVarTy tv) = Just tv -- through synonyms
1110 get_tv _ = Nothing
1111
1112 tcEqKind :: TcKind -> TcKind -> Bool
1113 tcEqKind = tcEqType
1114
1115 tcEqType :: TcType -> TcType -> Bool
1116 -- tcEqType is a proper, sensible type-equality function, that does
1117 -- just what you'd expect The function Type.eqType (currently) has a
1118 -- grotesque hack that makes OpenKind = *, and that is NOT what we
1119 -- want in the type checker! Otherwise, for example, TcCanonical.reOrient
1120 -- thinks the LHS and RHS have the same kinds, when they don't, and
1121 -- fails to re-orient. That in turn caused Trac #8553.
1122
1123 tcEqType ty1 ty2
1124 = go init_env ty1 ty2
1125 where
1126 init_env = mkRnEnv2 (mkInScopeSet (tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2))
1127 go env t1 t2 | Just t1' <- tcView t1 = go env t1' t2
1128 | Just t2' <- tcView t2 = go env t1 t2'
1129 go env (TyVarTy tv1) (TyVarTy tv2) = rnOccL env tv1 == rnOccR env tv2
1130 go _ (LitTy lit1) (LitTy lit2) = lit1 == lit2
1131 go env (ForAllTy tv1 t1) (ForAllTy tv2 t2) = go env (tyVarKind tv1) (tyVarKind tv2)
1132 && go (rnBndr2 env tv1 tv2) t1 t2
1133 go env (AppTy s1 t1) (AppTy s2 t2) = go env s1 s2 && go env t1 t2
1134 go env (FunTy s1 t1) (FunTy s2 t2) = go env s1 s2 && go env t1 t2
1135 go env (TyConApp tc1 ts1) (TyConApp tc2 ts2) = (tc1 == tc2) && gos env ts1 ts2
1136 go _ _ _ = False
1137
1138 gos _ [] [] = True
1139 gos env (t1:ts1) (t2:ts2) = go env t1 t2 && gos env ts1 ts2
1140 gos _ _ _ = False
1141
1142 {-
1143 Note [Occurs check expansion]
1144 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1145 (occurCheckExpand tv xi) expands synonyms in xi just enough to get rid
1146 of occurrences of tv outside type function arguments, if that is
1147 possible; otherwise, it returns Nothing.
1148
1149 For example, suppose we have
1150 type F a b = [a]
1151 Then
1152 occurCheckExpand b (F Int b) = Just [Int]
1153 but
1154 occurCheckExpand a (F a Int) = Nothing
1155
1156 We don't promise to do the absolute minimum amount of expanding
1157 necessary, but we try not to do expansions we don't need to. We
1158 prefer doing inner expansions first. For example,
1159 type F a b = (a, Int, a, [a])
1160 type G b = Char
1161 We have
1162 occurCheckExpand b (F (G b)) = F Char
1163 even though we could also expand F to get rid of b.
1164
1165 See also Note [occurCheckExpand] in TcCanonical
1166 -}
1167
1168 data OccCheckResult a
1169 = OC_OK a
1170 | OC_Forall
1171 | OC_NonTyVar
1172 | OC_Occurs
1173
1174 instance Functor OccCheckResult where
1175 fmap = liftM
1176
1177 instance Applicative OccCheckResult where
1178 pure = return
1179 (<*>) = ap
1180
1181 instance Monad OccCheckResult where
1182 return x = OC_OK x
1183 OC_OK x >>= k = k x
1184 OC_Forall >>= _ = OC_Forall
1185 OC_NonTyVar >>= _ = OC_NonTyVar
1186 OC_Occurs >>= _ = OC_Occurs
1187
1188 occurCheckExpand :: DynFlags -> TcTyVar -> Type -> OccCheckResult Type
1189 -- See Note [Occurs check expansion]
1190 -- Check whether
1191 -- a) the given variable occurs in the given type.
1192 -- b) there is a forall in the type (unless we have -XImpredicativeTypes
1193 -- or it's a ReturnTv
1194 -- c) if it's a SigTv, ty should be a tyvar
1195 --
1196 -- We may have needed to do some type synonym unfolding in order to
1197 -- get rid of the variable (or forall), so we also return the unfolded
1198 -- version of the type, which is guaranteed to be syntactically free
1199 -- of the given type variable. If the type is already syntactically
1200 -- free of the variable, then the same type is returned.
1201
1202 occurCheckExpand dflags tv ty
1203 | MetaTv { mtv_info = SigTv } <- details
1204 = go_sig_tv ty
1205 | fast_check ty = return ty
1206 | otherwise = go ty
1207 where
1208 details = ASSERT2( isTcTyVar tv, ppr tv ) tcTyVarDetails tv
1209
1210 impredicative = canUnifyWithPolyType dflags details (tyVarKind tv)
1211
1212 -- Check 'ty' is a tyvar, or can be expanded into one
1213 go_sig_tv ty@(TyVarTy {}) = OC_OK ty
1214 go_sig_tv ty | Just ty' <- tcView ty = go_sig_tv ty'
1215 go_sig_tv _ = OC_NonTyVar
1216
1217 -- True => fine
1218 fast_check (LitTy {}) = True
1219 fast_check (TyVarTy tv') = tv /= tv'
1220 fast_check (TyConApp tc tys) = all fast_check tys && (isTauTyCon tc || impredicative)
1221 fast_check (FunTy arg res) = fast_check arg && fast_check res
1222 fast_check (AppTy fun arg) = fast_check fun && fast_check arg
1223 fast_check (ForAllTy tv' ty) = impredicative
1224 && fast_check (tyVarKind tv')
1225 && (tv == tv' || fast_check ty)
1226
1227 go t@(TyVarTy tv') | tv == tv' = OC_Occurs
1228 | otherwise = return t
1229 go ty@(LitTy {}) = return ty
1230 go (AppTy ty1 ty2) = do { ty1' <- go ty1
1231 ; ty2' <- go ty2
1232 ; return (mkAppTy ty1' ty2') }
1233 go (FunTy ty1 ty2) = do { ty1' <- go ty1
1234 ; ty2' <- go ty2
1235 ; return (mkFunTy ty1' ty2') }
1236 go ty@(ForAllTy tv' body_ty)
1237 | not impredicative = OC_Forall
1238 | not (fast_check (tyVarKind tv')) = OC_Occurs
1239 -- Can't expand away the kinds unless we create
1240 -- fresh variables which we don't want to do at this point.
1241 -- In principle fast_check might fail because of a for-all
1242 -- but we don't yet have poly-kinded tyvars so I'm not
1243 -- going to worry about that now
1244 | tv == tv' = return ty
1245 | otherwise = do { body' <- go body_ty
1246 ; return (ForAllTy tv' body') }
1247
1248 -- For a type constructor application, first try expanding away the
1249 -- offending variable from the arguments. If that doesn't work, next
1250 -- see if the type constructor is a type synonym, and if so, expand
1251 -- it and try again.
1252 go ty@(TyConApp tc tys)
1253 = case do { tys <- mapM go tys; return (mkTyConApp tc tys) } of
1254 OC_OK ty
1255 | impredicative || isTauTyCon tc
1256 -> return ty -- First try to eliminate the tyvar from the args
1257 | otherwise
1258 -> OC_Forall -- A type synonym with a forall on the RHS
1259 bad | Just ty' <- tcView ty -> go ty'
1260 | otherwise -> bad
1261 -- Failing that, try to expand a synonym
1262
1263 canUnifyWithPolyType :: DynFlags -> TcTyVarDetails -> TcKind -> Bool
1264 canUnifyWithPolyType dflags details kind
1265 = case details of
1266 MetaTv { mtv_info = ReturnTv } -> True -- See Note [ReturnTv]
1267 MetaTv { mtv_info = SigTv } -> False
1268 MetaTv { mtv_info = TauTv _ } -> xopt Opt_ImpredicativeTypes dflags
1269 || isOpenTypeKind kind
1270 -- Note [OpenTypeKind accepts foralls]
1271 _other -> True
1272 -- We can have non-meta tyvars in given constraints
1273
1274 {-
1275 Note [OpenTypeKind accepts foralls]
1276 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1277 Here is a common paradigm:
1278 foo :: (forall a. a -> a) -> Int
1279 foo = error "urk"
1280 To make this work we need to instantiate 'error' with a polytype.
1281 A similar case is
1282 bar :: Bool -> (forall a. a->a) -> Int
1283 bar True = \x. (x 3)
1284 bar False = error "urk"
1285 Here we need to instantiate 'error' with a polytype.
1286
1287 But 'error' has an OpenTypeKind type variable, precisely so that
1288 we can instantiate it with Int#. So we also allow such type variables
1289 to be instantiated with foralls. It's a bit of a hack, but seems
1290 straightforward.
1291
1292 ************************************************************************
1293 * *
1294 \subsection{Predicate types}
1295 * *
1296 ************************************************************************
1297
1298 Deconstructors and tests on predicate types
1299
1300 Note [Kind polymorphic type classes]
1301 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1302 class C f where... -- C :: forall k. k -> Constraint
1303 g :: forall (f::*). C f => f -> f
1304
1305 Here the (C f) in the signature is really (C * f), and we
1306 don't want to complain that the * isn't a type variable!
1307 -}
1308
1309 isTyVarClassPred :: PredType -> Bool
1310 isTyVarClassPred ty = case getClassPredTys_maybe ty of
1311 Just (_, tys) -> all isTyVarTy tys
1312 _ -> False
1313
1314 -------------------------
1315 checkValidClsArgs :: Bool -> [KindOrType] -> Bool
1316 -- If the Bool is True (flexible contexts), return True (i.e. ok)
1317 -- Otherwise, check that the type (not kind) args are all headed by a tyvar
1318 -- E.g. (Eq a) accepted, (Eq (f a)) accepted, but (Eq Int) rejected
1319 -- This function is here rather than in TcValidity because it is
1320 -- called from TcSimplify, which itself is imported by TcValidity
1321 checkValidClsArgs flexible_contexts kts
1322 | flexible_contexts = True
1323 | otherwise = all hasTyVarHead tys
1324 where
1325 (_, tys) = span isKind kts -- see Note [Kind polymorphic type classes]
1326
1327 hasTyVarHead :: Type -> Bool
1328 -- Returns true of (a t1 .. tn), where 'a' is a type variable
1329 hasTyVarHead ty -- Haskell 98 allows predicates of form
1330 | tcIsTyVarTy ty = True -- C (a ty1 .. tyn)
1331 | otherwise -- where a is a type variable
1332 = case tcSplitAppTy_maybe ty of
1333 Just (ty, _) -> hasTyVarHead ty
1334 Nothing -> False
1335
1336 evVarPred_maybe :: EvVar -> Maybe PredType
1337 evVarPred_maybe v = if isPredTy ty then Just ty else Nothing
1338 where ty = varType v
1339
1340 evVarPred :: EvVar -> PredType
1341 evVarPred var
1342 | debugIsOn
1343 = case evVarPred_maybe var of
1344 Just pred -> pred
1345 Nothing -> pprPanic "tcEvVarPred" (ppr var <+> ppr (varType var))
1346 | otherwise
1347 = varType var
1348
1349 -- Superclasses
1350
1351 mkMinimalBySCs :: [PredType] -> [PredType]
1352 -- Remove predicates that can be deduced from others by superclasses
1353 mkMinimalBySCs ptys = [ ploc | ploc <- ptys
1354 , ploc `not_in_preds` rec_scs ]
1355 where
1356 rec_scs = concatMap trans_super_classes ptys
1357 not_in_preds p ps = not (any (eqPred p) ps)
1358
1359 trans_super_classes pred -- Superclasses of pred, excluding pred itself
1360 = case classifyPredType pred of
1361 ClassPred cls tys -> transSuperClasses cls tys
1362 _ -> []
1363
1364 transSuperClasses :: Class -> [Type] -> [PredType]
1365 transSuperClasses cls tys -- Superclasses of (cls tys),
1366 -- excluding (cls tys) itself
1367 = concatMap transSuperClassesPred (immSuperClasses cls tys)
1368
1369 transSuperClassesPred :: PredType -> [PredType]
1370 -- (transSuperClassesPred p) returns (p : p's superclasses)
1371 transSuperClassesPred p
1372 = case classifyPredType p of
1373 ClassPred cls tys -> p : transSuperClasses cls tys
1374 _ -> [p]
1375
1376 immSuperClasses :: Class -> [Type] -> [PredType]
1377 immSuperClasses cls tys
1378 = substTheta (zipTopTvSubst tyvars tys) sc_theta
1379 where
1380 (tyvars,sc_theta,_,_) = classBigSig cls
1381
1382 isImprovementPred :: PredType -> Bool
1383 -- Either it's an equality, or has some functional dependency
1384 isImprovementPred ty
1385 = case classifyPredType ty of
1386 EqPred NomEq t1 t2 -> not (t1 `tcEqType` t2)
1387 EqPred ReprEq _ _ -> False
1388 ClassPred cls _ -> classHasFds cls
1389 IrredPred {} -> True -- Might have equalities after reduction?
1390
1391 {-
1392 ************************************************************************
1393 * *
1394 \subsection{Predicates}
1395 * *
1396 ************************************************************************
1397 -}
1398
1399 isSigmaTy :: TcType -> Bool
1400 -- isSigmaTy returns true of any qualified type. It doesn't
1401 -- *necessarily* have any foralls. E.g
1402 -- f :: (?x::Int) => Int -> Int
1403 isSigmaTy ty | Just ty' <- tcView ty = isSigmaTy ty'
1404 isSigmaTy (ForAllTy _ _) = True
1405 isSigmaTy (FunTy a _) = isPredTy a
1406 isSigmaTy _ = False
1407
1408 isRhoTy :: TcType -> Bool -- True of TcRhoTypes; see Note [TcRhoType]
1409 isRhoTy ty | Just ty' <- tcView ty = isRhoTy ty'
1410 isRhoTy (ForAllTy {}) = False
1411 isRhoTy (FunTy a r) = not (isPredTy a) && isRhoTy r
1412 isRhoTy _ = True
1413
1414 isOverloadedTy :: Type -> Bool
1415 -- Yes for a type of a function that might require evidence-passing
1416 -- Used only by bindLocalMethods
1417 isOverloadedTy ty | Just ty' <- tcView ty = isOverloadedTy ty'
1418 isOverloadedTy (ForAllTy _ ty) = isOverloadedTy ty
1419 isOverloadedTy (FunTy a _) = isPredTy a
1420 isOverloadedTy _ = False
1421
1422 isFloatTy, isDoubleTy, isIntegerTy, isIntTy, isWordTy, isBoolTy,
1423 isUnitTy, isCharTy, isAnyTy :: Type -> Bool
1424 isFloatTy = is_tc floatTyConKey
1425 isDoubleTy = is_tc doubleTyConKey
1426 isIntegerTy = is_tc integerTyConKey
1427 isIntTy = is_tc intTyConKey
1428 isWordTy = is_tc wordTyConKey
1429 isBoolTy = is_tc boolTyConKey
1430 isUnitTy = is_tc unitTyConKey
1431 isCharTy = is_tc charTyConKey
1432 isAnyTy = is_tc anyTyConKey
1433
1434 isStringTy :: Type -> Bool
1435 isStringTy ty
1436 = case tcSplitTyConApp_maybe ty of
1437 Just (tc, [arg_ty]) -> tc == listTyCon && isCharTy arg_ty
1438 _ -> False
1439
1440 is_tc :: Unique -> Type -> Bool
1441 -- Newtypes are opaque to this
1442 is_tc uniq ty = case tcSplitTyConApp_maybe ty of
1443 Just (tc, _) -> uniq == getUnique tc
1444 Nothing -> False
1445
1446 -- | Does the given tyvar appear in the given type outside of any
1447 -- non-newtypes? Assume we're looking for @a@. Says "yes" for
1448 -- @a@, @N a@, @b a@, @a b@, @b (N a)@. Says "no" for
1449 -- @[a]@, @Maybe a@, @T a@, where @N@ is a newtype and @T@ is a datatype.
1450 isTyVarExposed :: TcTyVar -> TcType -> Bool
1451 isTyVarExposed tv (TyVarTy tv') = tv == tv'
1452 isTyVarExposed tv (TyConApp tc tys)
1453 | isNewTyCon tc = any (isTyVarExposed tv) tys
1454 | otherwise = False
1455 isTyVarExposed _ (LitTy {}) = False
1456 isTyVarExposed _ (FunTy {}) = False
1457 isTyVarExposed tv (AppTy fun arg) = isTyVarExposed tv fun
1458 || isTyVarExposed tv arg
1459 isTyVarExposed _ (ForAllTy {}) = False
1460
1461 isRigidTy :: TcType -> Bool
1462 isRigidTy ty
1463 | Just (tc,_) <- tcSplitTyConApp_maybe ty = isGenerativeTyCon tc Nominal
1464 | Just {} <- tcSplitAppTy_maybe ty = True
1465 | isForAllTy ty = True
1466 | otherwise = False
1467
1468 isRigidEqPred :: TcLevel -> PredTree -> Bool
1469 -- ^ True of all Nominal equalities that are solidly insoluble
1470 -- This means all equalities *except*
1471 -- * Meta-tv non-SigTv on LHS
1472 -- * Meta-tv SigTv on LHS, tyvar on right
1473 isRigidEqPred tc_lvl (EqPred NomEq ty1 _)
1474 | Just tv1 <- tcGetTyVar_maybe ty1
1475 = ASSERT2( isTcTyVar tv1, ppr tv1 )
1476 not (isMetaTyVar tv1) || isTouchableMetaTyVar tc_lvl tv1
1477
1478 | otherwise -- LHS is not a tyvar
1479 = True
1480
1481 isRigidEqPred _ _ = False -- Not an equality
1482
1483 {-
1484 ************************************************************************
1485 * *
1486 \subsection{Misc}
1487 * *
1488 ************************************************************************
1489 -}
1490
1491 deNoteType :: Type -> Type
1492 -- Remove all *outermost* type synonyms and other notes
1493 deNoteType ty | Just ty' <- tcView ty = deNoteType ty'
1494 deNoteType ty = ty
1495
1496 tcTyVarsOfType :: Type -> TcTyVarSet
1497 -- Just the *TcTyVars* free in the type
1498 -- (Types.tyVarsOfTypes finds all free TyVars)
1499 tcTyVarsOfType (TyVarTy tv) = if isTcTyVar tv then unitVarSet tv
1500 else emptyVarSet
1501 tcTyVarsOfType (TyConApp _ tys) = tcTyVarsOfTypes tys
1502 tcTyVarsOfType (LitTy {}) = emptyVarSet
1503 tcTyVarsOfType (FunTy arg res) = tcTyVarsOfType arg `unionVarSet` tcTyVarsOfType res
1504 tcTyVarsOfType (AppTy fun arg) = tcTyVarsOfType fun `unionVarSet` tcTyVarsOfType arg
1505 tcTyVarsOfType (ForAllTy tyvar ty) = tcTyVarsOfType ty `delVarSet` tyvar
1506 -- We do sometimes quantify over skolem TcTyVars
1507
1508 tcTyVarsOfTypes :: [Type] -> TyVarSet
1509 tcTyVarsOfTypes = mapUnionVarSet tcTyVarsOfType
1510
1511 {-
1512 Find the free tycons and classes of a type. This is used in the front
1513 end of the compiler.
1514 -}
1515
1516 orphNamesOfTyCon :: TyCon -> NameSet
1517 orphNamesOfTyCon tycon = unitNameSet (getName tycon) `unionNameSet` case tyConClass_maybe tycon of
1518 Nothing -> emptyNameSet
1519 Just cls -> unitNameSet (getName cls)
1520
1521 orphNamesOfType :: Type -> NameSet
1522 orphNamesOfType ty | Just ty' <- tcView ty = orphNamesOfType ty'
1523 -- Look through type synonyms (Trac #4912)
1524 orphNamesOfType (TyVarTy _) = emptyNameSet
1525 orphNamesOfType (LitTy {}) = emptyNameSet
1526 orphNamesOfType (TyConApp tycon tys) = orphNamesOfTyCon tycon
1527 `unionNameSet` orphNamesOfTypes tys
1528 orphNamesOfType (FunTy arg res) = orphNamesOfTyCon funTyCon -- NB! See Trac #8535
1529 `unionNameSet` orphNamesOfType arg
1530 `unionNameSet` orphNamesOfType res
1531 orphNamesOfType (AppTy fun arg) = orphNamesOfType fun `unionNameSet` orphNamesOfType arg
1532 orphNamesOfType (ForAllTy _ ty) = orphNamesOfType ty
1533
1534 orphNamesOfThings :: (a -> NameSet) -> [a] -> NameSet
1535 orphNamesOfThings f = foldr (unionNameSet . f) emptyNameSet
1536
1537 orphNamesOfTypes :: [Type] -> NameSet
1538 orphNamesOfTypes = orphNamesOfThings orphNamesOfType
1539
1540 orphNamesOfDFunHead :: Type -> NameSet
1541 -- Find the free type constructors and classes
1542 -- of the head of the dfun instance type
1543 -- The 'dfun_head_type' is because of
1544 -- instance Foo a => Baz T where ...
1545 -- The decl is an orphan if Baz and T are both not locally defined,
1546 -- even if Foo *is* locally defined
1547 orphNamesOfDFunHead dfun_ty
1548 = case tcSplitSigmaTy dfun_ty of
1549 (_, _, head_ty) -> orphNamesOfType head_ty
1550
1551 orphNamesOfCo :: Coercion -> NameSet
1552 orphNamesOfCo (Refl _ ty) = orphNamesOfType ty
1553 orphNamesOfCo (TyConAppCo _ tc cos) = unitNameSet (getName tc) `unionNameSet` orphNamesOfCos cos
1554 orphNamesOfCo (AppCo co1 co2) = orphNamesOfCo co1 `unionNameSet` orphNamesOfCo co2
1555 orphNamesOfCo (ForAllCo _ co) = orphNamesOfCo co
1556 orphNamesOfCo (CoVarCo _) = emptyNameSet
1557 orphNamesOfCo (AxiomInstCo con _ cos) = orphNamesOfCoCon con `unionNameSet` orphNamesOfCos cos
1558 orphNamesOfCo (UnivCo _ _ ty1 ty2) = orphNamesOfType ty1 `unionNameSet` orphNamesOfType ty2
1559 orphNamesOfCo (SymCo co) = orphNamesOfCo co
1560 orphNamesOfCo (TransCo co1 co2) = orphNamesOfCo co1 `unionNameSet` orphNamesOfCo co2
1561 orphNamesOfCo (NthCo _ co) = orphNamesOfCo co
1562 orphNamesOfCo (LRCo _ co) = orphNamesOfCo co
1563 orphNamesOfCo (InstCo co ty) = orphNamesOfCo co `unionNameSet` orphNamesOfType ty
1564 orphNamesOfCo (SubCo co) = orphNamesOfCo co
1565 orphNamesOfCo (AxiomRuleCo _ ts cs) = orphNamesOfTypes ts `unionNameSet`
1566 orphNamesOfCos cs
1567
1568 orphNamesOfCos :: [Coercion] -> NameSet
1569 orphNamesOfCos = orphNamesOfThings orphNamesOfCo
1570
1571 orphNamesOfCoCon :: CoAxiom br -> NameSet
1572 orphNamesOfCoCon (CoAxiom { co_ax_tc = tc, co_ax_branches = branches })
1573 = orphNamesOfTyCon tc `unionNameSet` orphNamesOfCoAxBranches branches
1574
1575 orphNamesOfCoAxBranches :: BranchList CoAxBranch br -> NameSet
1576 orphNamesOfCoAxBranches = brListFoldr (unionNameSet . orphNamesOfCoAxBranch) emptyNameSet
1577
1578 orphNamesOfCoAxBranch :: CoAxBranch -> NameSet
1579 orphNamesOfCoAxBranch (CoAxBranch { cab_lhs = lhs, cab_rhs = rhs })
1580 = orphNamesOfTypes lhs `unionNameSet` orphNamesOfType rhs
1581
1582 {-
1583 ************************************************************************
1584 * *
1585 \subsection[TysWiredIn-ext-type]{External types}
1586 * *
1587 ************************************************************************
1588
1589 The compiler's foreign function interface supports the passing of a
1590 restricted set of types as arguments and results (the restricting factor
1591 being the )
1592 -}
1593
1594 tcSplitIOType_maybe :: Type -> Maybe (TyCon, Type)
1595 -- (tcSplitIOType_maybe t) returns Just (IO,t',co)
1596 -- if co : t ~ IO t'
1597 -- returns Nothing otherwise
1598 tcSplitIOType_maybe ty
1599 = case tcSplitTyConApp_maybe ty of
1600 Just (io_tycon, [io_res_ty])
1601 | io_tycon `hasKey` ioTyConKey ->
1602 Just (io_tycon, io_res_ty)
1603 _ ->
1604 Nothing
1605
1606 isFFITy :: Type -> Bool
1607 -- True for any TyCon that can possibly be an arg or result of an FFI call
1608 isFFITy ty = isValid (checkRepTyCon legalFFITyCon ty)
1609
1610 isFFIArgumentTy :: DynFlags -> Safety -> Type -> Validity
1611 -- Checks for valid argument type for a 'foreign import'
1612 isFFIArgumentTy dflags safety ty
1613 = checkRepTyCon (legalOutgoingTyCon dflags safety) ty
1614
1615 isFFIExternalTy :: Type -> Validity
1616 -- Types that are allowed as arguments of a 'foreign export'
1617 isFFIExternalTy ty = checkRepTyCon legalFEArgTyCon ty
1618
1619 isFFIImportResultTy :: DynFlags -> Type -> Validity
1620 isFFIImportResultTy dflags ty
1621 = checkRepTyCon (legalFIResultTyCon dflags) ty
1622
1623 isFFIExportResultTy :: Type -> Validity
1624 isFFIExportResultTy ty = checkRepTyCon legalFEResultTyCon ty
1625
1626 isFFIDynTy :: Type -> Type -> Validity
1627 -- The type in a foreign import dynamic must be Ptr, FunPtr, or a newtype of
1628 -- either, and the wrapped function type must be equal to the given type.
1629 -- We assume that all types have been run through normaliseFfiType, so we don't
1630 -- need to worry about expanding newtypes here.
1631 isFFIDynTy expected ty
1632 -- Note [Foreign import dynamic]
1633 -- In the example below, expected would be 'CInt -> IO ()', while ty would
1634 -- be 'FunPtr (CDouble -> IO ())'.
1635 | Just (tc, [ty']) <- splitTyConApp_maybe ty
1636 , tyConUnique tc `elem` [ptrTyConKey, funPtrTyConKey]
1637 , eqType ty' expected
1638 = IsValid
1639 | otherwise
1640 = NotValid (vcat [ ptext (sLit "Expected: Ptr/FunPtr") <+> pprParendType expected <> comma
1641 , ptext (sLit " Actual:") <+> ppr ty ])
1642
1643 isFFILabelTy :: Type -> Validity
1644 -- The type of a foreign label must be Ptr, FunPtr, or a newtype of either.
1645 isFFILabelTy ty = checkRepTyCon ok ty
1646 where
1647 ok tc | tc `hasKey` funPtrTyConKey || tc `hasKey` ptrTyConKey
1648 = IsValid
1649 | otherwise
1650 = NotValid (ptext (sLit "A foreign-imported address (via &foo) must have type (Ptr a) or (FunPtr a)"))
1651
1652 isFFIPrimArgumentTy :: DynFlags -> Type -> Validity
1653 -- Checks for valid argument type for a 'foreign import prim'
1654 -- Currently they must all be simple unlifted types, or the well-known type
1655 -- Any, which can be used to pass the address to a Haskell object on the heap to
1656 -- the foreign function.
1657 isFFIPrimArgumentTy dflags ty
1658 | isAnyTy ty = IsValid
1659 | otherwise = checkRepTyCon (legalFIPrimArgTyCon dflags) ty
1660
1661 isFFIPrimResultTy :: DynFlags -> Type -> Validity
1662 -- Checks for valid result type for a 'foreign import prim'
1663 -- Currently it must be an unlifted type, including unboxed tuples,
1664 -- or the well-known type Any.
1665 isFFIPrimResultTy dflags ty
1666 | isAnyTy ty = IsValid
1667 | otherwise = checkRepTyCon (legalFIPrimResultTyCon dflags) ty
1668
1669 isFunPtrTy :: Type -> Bool
1670 isFunPtrTy ty
1671 | Just (tc, [_]) <- splitTyConApp_maybe ty
1672 = tc `hasKey` funPtrTyConKey
1673 | otherwise
1674 = False
1675
1676 -- normaliseFfiType gets run before checkRepTyCon, so we don't
1677 -- need to worry about looking through newtypes or type functions
1678 -- here; that's already been taken care of.
1679 checkRepTyCon :: (TyCon -> Validity) -> Type -> Validity
1680 checkRepTyCon check_tc ty
1681 = case splitTyConApp_maybe ty of
1682 Just (tc, tys)
1683 | isNewTyCon tc -> NotValid (hang msg 2 (mk_nt_reason tc tys $$ nt_fix))
1684 | otherwise -> case check_tc tc of
1685 IsValid -> IsValid
1686 NotValid extra -> NotValid (msg $$ extra)
1687 Nothing -> NotValid (quotes (ppr ty) <+> ptext (sLit "is not a data type"))
1688 where
1689 msg = quotes (ppr ty) <+> ptext (sLit "cannot be marshalled in a foreign call")
1690 mk_nt_reason tc tys
1691 | null tys = ptext (sLit "because its data constructor is not in scope")
1692 | otherwise = ptext (sLit "because the data constructor for")
1693 <+> quotes (ppr tc) <+> ptext (sLit "is not in scope")
1694 nt_fix = ptext (sLit "Possible fix: import the data constructor to bring it into scope")
1695
1696 {-
1697 Note [Foreign import dynamic]
1698 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1699 A dynamic stub must be of the form 'FunPtr ft -> ft' where ft is any foreign
1700 type. Similarly, a wrapper stub must be of the form 'ft -> IO (FunPtr ft)'.
1701
1702 We use isFFIDynTy to check whether a signature is well-formed. For example,
1703 given a (illegal) declaration like:
1704
1705 foreign import ccall "dynamic"
1706 foo :: FunPtr (CDouble -> IO ()) -> CInt -> IO ()
1707
1708 isFFIDynTy will compare the 'FunPtr' type 'CDouble -> IO ()' with the curried
1709 result type 'CInt -> IO ()', and return False, as they are not equal.
1710
1711
1712 ----------------------------------------------
1713 These chaps do the work; they are not exported
1714 ----------------------------------------------
1715 -}
1716
1717 legalFEArgTyCon :: TyCon -> Validity
1718 legalFEArgTyCon tc
1719 -- It's illegal to make foreign exports that take unboxed
1720 -- arguments. The RTS API currently can't invoke such things. --SDM 7/2000
1721 = boxedMarshalableTyCon tc
1722
1723 legalFIResultTyCon :: DynFlags -> TyCon -> Validity
1724 legalFIResultTyCon dflags tc
1725 | tc == unitTyCon = IsValid
1726 | otherwise = marshalableTyCon dflags tc
1727
1728 legalFEResultTyCon :: TyCon -> Validity
1729 legalFEResultTyCon tc
1730 | tc == unitTyCon = IsValid
1731 | otherwise = boxedMarshalableTyCon tc
1732
1733 legalOutgoingTyCon :: DynFlags -> Safety -> TyCon -> Validity
1734 -- Checks validity of types going from Haskell -> external world
1735 legalOutgoingTyCon dflags _ tc
1736 = marshalableTyCon dflags tc
1737
1738 legalFFITyCon :: TyCon -> Validity
1739 -- True for any TyCon that can possibly be an arg or result of an FFI call
1740 legalFFITyCon tc
1741 | isUnLiftedTyCon tc = IsValid
1742 | tc == unitTyCon = IsValid
1743 | otherwise = boxedMarshalableTyCon tc
1744
1745 marshalableTyCon :: DynFlags -> TyCon -> Validity
1746 marshalableTyCon dflags tc
1747 | isUnLiftedTyCon tc
1748 , not (isUnboxedTupleTyCon tc)
1749 , case tyConPrimRep tc of -- Note [Marshalling VoidRep]
1750 VoidRep -> False
1751 _ -> True
1752 = validIfUnliftedFFITypes dflags
1753 | otherwise
1754 = boxedMarshalableTyCon tc
1755
1756 boxedMarshalableTyCon :: TyCon -> Validity
1757 boxedMarshalableTyCon tc
1758 | getUnique tc `elem` [ intTyConKey, int8TyConKey, int16TyConKey
1759 , int32TyConKey, int64TyConKey
1760 , wordTyConKey, word8TyConKey, word16TyConKey
1761 , word32TyConKey, word64TyConKey
1762 , floatTyConKey, doubleTyConKey
1763 , ptrTyConKey, funPtrTyConKey
1764 , charTyConKey
1765 , stablePtrTyConKey
1766 , boolTyConKey
1767 ]
1768 = IsValid
1769
1770 | otherwise = NotValid empty
1771
1772 legalFIPrimArgTyCon :: DynFlags -> TyCon -> Validity
1773 -- Check args of 'foreign import prim', only allow simple unlifted types.
1774 -- Strictly speaking it is unnecessary to ban unboxed tuples here since
1775 -- currently they're of the wrong kind to use in function args anyway.
1776 legalFIPrimArgTyCon dflags tc
1777 | isUnLiftedTyCon tc
1778 , not (isUnboxedTupleTyCon tc)
1779 = validIfUnliftedFFITypes dflags
1780 | otherwise
1781 = NotValid unlifted_only
1782
1783 legalFIPrimResultTyCon :: DynFlags -> TyCon -> Validity
1784 -- Check result type of 'foreign import prim'. Allow simple unlifted
1785 -- types and also unboxed tuple result types '... -> (# , , #)'
1786 legalFIPrimResultTyCon dflags tc
1787 | isUnLiftedTyCon tc
1788 , (isUnboxedTupleTyCon tc
1789 || case tyConPrimRep tc of -- Note [Marshalling VoidRep]
1790 VoidRep -> False
1791 _ -> True)
1792 = validIfUnliftedFFITypes dflags
1793
1794 | otherwise
1795 = NotValid unlifted_only
1796
1797 unlifted_only :: MsgDoc
1798 unlifted_only = ptext (sLit "foreign import prim only accepts simple unlifted types")
1799
1800 validIfUnliftedFFITypes :: DynFlags -> Validity
1801 validIfUnliftedFFITypes dflags
1802 | xopt Opt_UnliftedFFITypes dflags = IsValid
1803 | otherwise = NotValid (ptext (sLit "To marshal unlifted types, use UnliftedFFITypes"))
1804
1805 {-
1806 Note [Marshalling VoidRep]
1807 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1808 We don't treat State# (whose PrimRep is VoidRep) as marshalable.
1809 In turn that means you can't write
1810 foreign import foo :: Int -> State# RealWorld
1811
1812 Reason: the back end falls over with panic "primRepHint:VoidRep";
1813 and there is no compelling reason to permit it
1814 -}
1815
1816 {-
1817 ************************************************************************
1818 * *
1819 The "Paterson size" of a type
1820 * *
1821 ************************************************************************
1822 -}
1823
1824 {-
1825 Note [Paterson conditions on PredTypes]
1826 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1827 We are considering whether *class* constraints terminate
1828 (see Note [Paterson conditions]). Precisely, the Paterson conditions
1829 would have us check that "the constraint has fewer constructors and variables
1830 (taken together and counting repetitions) than the head.".
1831
1832 However, we can be a bit more refined by looking at which kind of constraint
1833 this actually is. There are two main tricks:
1834
1835 1. It seems like it should be OK not to count the tuple type constructor
1836 for a PredType like (Show a, Eq a) :: Constraint, since we don't
1837 count the "implicit" tuple in the ThetaType itself.
1838
1839 In fact, the Paterson test just checks *each component* of the top level
1840 ThetaType against the size bound, one at a time. By analogy, it should be
1841 OK to return the size of the *largest* tuple component as the size of the
1842 whole tuple.
1843
1844 2. Once we get into an implicit parameter or equality we
1845 can't get back to a class constraint, so it's safe
1846 to say "size 0". See Trac #4200.
1847
1848 NB: we don't want to detect PredTypes in sizeType (and then call
1849 sizePred on them), or we might get an infinite loop if that PredType
1850 is irreducible. See Trac #5581.
1851 -}
1852
1853 type TypeSize = IntWithInf
1854
1855 sizeType, size_type :: Type -> TypeSize
1856 -- Size of a type: the number of variables and constructors
1857 -- Ignore kinds altogether
1858 sizeType ty | isKind ty = 0
1859 | otherwise = size_type ty
1860
1861 size_type ty | Just exp_ty <- tcView ty = size_type exp_ty
1862 size_type (TyVarTy {}) = 1
1863 size_type (TyConApp tc tys)
1864 | isTypeFamilyTyCon tc = infinity -- Type-family applications can
1865 -- expand to any arbitrary size
1866 | otherwise = sizeTypes tys + 1
1867 size_type (LitTy {}) = 1
1868 size_type (FunTy arg res) = size_type arg + size_type res + 1
1869 size_type (AppTy fun arg) = size_type fun + size_type arg
1870 size_type (ForAllTy _ ty) = size_type ty
1871
1872 sizeTypes :: [Type] -> TypeSize
1873 sizeTypes tys = sum (map sizeType tys)
1874