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