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