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