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