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