2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 \section{Monadic type operations}
6 This module contains monadic operations over types that contain mutable type variables
10 TcTyVar, TcKind, TcType, TcTauType, TcThetaType, TcTyVarSet,
12 --------------------------------
13 -- Creating new mutable type variables
15 newTyVarTy, -- Kind -> NF_TcM TcType
16 newTyVarTys, -- Int -> Kind -> NF_TcM [TcType]
17 newKindVar, newKindVars, newBoxityVar,
18 putTcTyVar, getTcTyVar,
20 newHoleTyVarTy, readHoleResult, zapToType,
22 --------------------------------
24 tcInstTyVar, tcInstTyVars, tcInstType,
26 --------------------------------
27 -- Checking type validity
28 Rank, UserTypeCtxt(..), checkValidType, pprUserTypeCtxt,
29 SourceTyCtxt(..), checkValidTheta,
30 checkValidTyCon, checkValidClass,
31 checkValidInstHead, instTypeErr, checkAmbiguity,
33 --------------------------------
35 zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV,
36 zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
37 zonkTcPredType, zonkTcTypeToType, zonkTcTyVarToTyVar, zonkKindEnv,
41 #include "HsVersions.h"
45 import TypeRep ( Type(..), SourceType(..), TyNote(..), -- Friend; can see representation
48 import TcType ( TcType, TcThetaType, TcTauType, TcPredType,
49 TcTyVarSet, TcKind, TcTyVar, TyVarDetails(..),
51 tcSplitPhiTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe,
52 tcSplitTyConApp_maybe, tcSplitForAllTys,
53 tcIsTyVarTy, tcSplitSigmaTy,
54 isUnLiftedType, isIPPred, isHoleTyVar, isTyVarTy,
56 mkAppTy, mkTyVarTy, mkTyVarTys,
57 tyVarsOfPred, getClassPredTys_maybe,
59 liftedTypeKind, openTypeKind, defaultKind, superKind,
60 superBoxity, liftedBoxity, typeKind,
61 tyVarsOfType, tyVarsOfTypes,
62 eqKind, isTypeKind, isAnyTypeKind,
64 isFFIArgumentTy, isFFIImportResultTy
66 import qualified Type ( splitFunTys )
67 import Subst ( Subst, mkTopTyVarSubst, substTy )
68 import Class ( Class, DefMeth(..), classArity, className, classBigSig )
69 import TyCon ( TyCon, mkPrimTyCon, isSynTyCon, isUnboxedTupleTyCon,
70 tyConArity, tyConName, tyConKind, tyConTheta,
71 getSynTyConDefn, tyConDataCons )
72 import DataCon ( DataCon, dataConWrapId, dataConName, dataConSig, dataConFieldLabels )
73 import FieldLabel ( fieldLabelName, fieldLabelType )
74 import PrimRep ( PrimRep(VoidRep) )
75 import Var ( TyVar, idType, idName, tyVarKind, tyVarName, isTyVar, mkTyVar, isMutTyVar )
78 import Generics ( validGenericMethodType )
79 import TcMonad -- TcType, amongst others
80 import TysWiredIn ( voidTy, listTyCon, tupleTyCon )
81 import PrelNames ( cCallableClassKey, cReturnableClassKey, hasKey )
82 import ForeignCall ( Safety(..) )
83 import FunDeps ( grow )
84 import PprType ( pprPred, pprSourceType, pprTheta, pprClassPred )
85 import Name ( Name, NamedThing(..), setNameUnique, mkSystemName,
86 mkInternalName, mkDerivedTyConOcc
89 import BasicTypes ( Boxity(Boxed) )
90 import CmdLineOpts ( dopt, DynFlag(..) )
91 import Unique ( Uniquable(..) )
92 import SrcLoc ( noSrcLoc )
93 import Util ( nOfThem, isSingleton, equalLength, notNull )
94 import ListSetOps ( equivClasses, removeDups )
99 %************************************************************************
101 \subsection{New type variables}
103 %************************************************************************
106 newTyVar :: Kind -> NF_TcM TcTyVar
108 = tcGetUnique `thenNF_Tc` \ uniq ->
109 tcNewMutTyVar (mkSystemName uniq FSLIT("t")) kind VanillaTv
111 newTyVarTy :: Kind -> NF_TcM TcType
113 = newTyVar kind `thenNF_Tc` \ tc_tyvar ->
114 returnNF_Tc (TyVarTy tc_tyvar)
116 newTyVarTys :: Int -> Kind -> NF_TcM [TcType]
117 newTyVarTys n kind = mapNF_Tc newTyVarTy (nOfThem n kind)
119 newKindVar :: NF_TcM TcKind
121 = tcGetUnique `thenNF_Tc` \ uniq ->
122 tcNewMutTyVar (mkSystemName uniq FSLIT("k")) superKind VanillaTv `thenNF_Tc` \ kv ->
123 returnNF_Tc (TyVarTy kv)
125 newKindVars :: Int -> NF_TcM [TcKind]
126 newKindVars n = mapNF_Tc (\ _ -> newKindVar) (nOfThem n ())
128 newBoxityVar :: NF_TcM TcKind
130 = tcGetUnique `thenNF_Tc` \ uniq ->
131 tcNewMutTyVar (mkSystemName uniq FSLIT("bx")) superBoxity VanillaTv `thenNF_Tc` \ kv ->
132 returnNF_Tc (TyVarTy kv)
136 %************************************************************************
138 \subsection{'hole' type variables}
140 %************************************************************************
143 newHoleTyVarTy :: NF_TcM TcType
144 = tcGetUnique `thenNF_Tc` \ uniq ->
145 tcNewMutTyVar (mkSystemName uniq FSLIT("h")) openTypeKind HoleTv `thenNF_Tc` \ tv ->
146 returnNF_Tc (TyVarTy tv)
148 readHoleResult :: TcType -> NF_TcM TcType
149 -- Read the answer out of a hole, constructed by newHoleTyVarTy
150 readHoleResult (TyVarTy tv)
151 = ASSERT( isHoleTyVar tv )
152 getTcTyVar tv `thenNF_Tc` \ maybe_res ->
154 Just ty -> returnNF_Tc ty
155 Nothing -> pprPanic "readHoleResult: empty" (ppr tv)
156 readHoleResult ty = pprPanic "readHoleResult: not hole" (ppr ty)
158 zapToType :: TcType -> NF_TcM TcType
159 zapToType (TyVarTy tv)
161 = getTcTyVar tv `thenNF_Tc` \ maybe_res ->
163 Nothing -> newTyVarTy openTypeKind `thenNF_Tc` \ ty ->
164 putTcTyVar tv ty `thenNF_Tc_`
166 Just ty -> returnNF_Tc ty -- No need to loop; we never
167 -- have chains of holes
169 zapToType other_ty = returnNF_Tc other_ty
172 %************************************************************************
174 \subsection{Type instantiation}
176 %************************************************************************
178 Instantiating a bunch of type variables
181 tcInstTyVars :: TyVarDetails -> [TyVar]
182 -> NF_TcM ([TcTyVar], [TcType], Subst)
184 tcInstTyVars tv_details tyvars
185 = mapNF_Tc (tcInstTyVar tv_details) tyvars `thenNF_Tc` \ tc_tyvars ->
187 tys = mkTyVarTys tc_tyvars
189 returnNF_Tc (tc_tyvars, tys, mkTopTyVarSubst tyvars tys)
190 -- Since the tyvars are freshly made,
191 -- they cannot possibly be captured by
192 -- any existing for-alls. Hence mkTopTyVarSubst
194 tcInstTyVar tv_details tyvar
195 = tcGetUnique `thenNF_Tc` \ uniq ->
197 name = setNameUnique (tyVarName tyvar) uniq
198 -- Note that we don't change the print-name
199 -- This won't confuse the type checker but there's a chance
200 -- that two different tyvars will print the same way
201 -- in an error message. -dppr-debug will show up the difference
202 -- Better watch out for this. If worst comes to worst, just
205 tcNewMutTyVar name (tyVarKind tyvar) tv_details
207 tcInstType :: TyVarDetails -> TcType -> NF_TcM ([TcTyVar], TcThetaType, TcType)
208 -- tcInstType instantiates the outer-level for-alls of a TcType with
209 -- fresh (mutable) type variables, splits off the dictionary part,
210 -- and returns the pieces.
211 tcInstType tv_details ty
212 = case tcSplitForAllTys ty of
213 ([], rho) -> -- There may be overloading despite no type variables;
214 -- (?x :: Int) => Int -> Int
216 (theta, tau) = tcSplitPhiTy rho
218 returnNF_Tc ([], theta, tau)
220 (tyvars, rho) -> tcInstTyVars tv_details tyvars `thenNF_Tc` \ (tyvars', _, tenv) ->
222 (theta, tau) = tcSplitPhiTy (substTy tenv rho)
224 returnNF_Tc (tyvars', theta, tau)
228 %************************************************************************
230 \subsection{Putting and getting mutable type variables}
232 %************************************************************************
235 putTcTyVar :: TcTyVar -> TcType -> NF_TcM TcType
236 getTcTyVar :: TcTyVar -> NF_TcM (Maybe TcType)
243 | not (isMutTyVar tyvar)
244 = pprTrace "putTcTyVar" (ppr tyvar) $
248 = ASSERT( isMutTyVar tyvar )
249 tcWriteMutTyVar tyvar (Just ty) `thenNF_Tc_`
253 Getting is more interesting. The easy thing to do is just to read, thus:
256 getTcTyVar tyvar = tcReadMutTyVar tyvar
259 But it's more fun to short out indirections on the way: If this
260 version returns a TyVar, then that TyVar is unbound. If it returns
261 any other type, then there might be bound TyVars embedded inside it.
263 We return Nothing iff the original box was unbound.
267 | not (isMutTyVar tyvar)
268 = pprTrace "getTcTyVar" (ppr tyvar) $
269 returnNF_Tc (Just (mkTyVarTy tyvar))
272 = ASSERT2( isMutTyVar tyvar, ppr tyvar )
273 tcReadMutTyVar tyvar `thenNF_Tc` \ maybe_ty ->
275 Just ty -> short_out ty `thenNF_Tc` \ ty' ->
276 tcWriteMutTyVar tyvar (Just ty') `thenNF_Tc_`
277 returnNF_Tc (Just ty')
279 Nothing -> returnNF_Tc Nothing
281 short_out :: TcType -> NF_TcM TcType
282 short_out ty@(TyVarTy tyvar)
283 | not (isMutTyVar tyvar)
287 = tcReadMutTyVar tyvar `thenNF_Tc` \ maybe_ty ->
289 Just ty' -> short_out ty' `thenNF_Tc` \ ty' ->
290 tcWriteMutTyVar tyvar (Just ty') `thenNF_Tc_`
293 other -> returnNF_Tc ty
295 short_out other_ty = returnNF_Tc other_ty
299 %************************************************************************
301 \subsection{Zonking -- the exernal interfaces}
303 %************************************************************************
305 ----------------- Type variables
308 zonkTcTyVars :: [TcTyVar] -> NF_TcM [TcType]
309 zonkTcTyVars tyvars = mapNF_Tc zonkTcTyVar tyvars
311 zonkTcTyVarsAndFV :: [TcTyVar] -> NF_TcM TcTyVarSet
312 zonkTcTyVarsAndFV tyvars = mapNF_Tc zonkTcTyVar tyvars `thenNF_Tc` \ tys ->
313 returnNF_Tc (tyVarsOfTypes tys)
315 zonkTcTyVar :: TcTyVar -> NF_TcM TcType
316 zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnNF_Tc (TyVarTy tv)) tyvar
319 ----------------- Types
322 zonkTcType :: TcType -> NF_TcM TcType
323 zonkTcType ty = zonkType (\ tv -> returnNF_Tc (TyVarTy tv)) ty
325 zonkTcTypes :: [TcType] -> NF_TcM [TcType]
326 zonkTcTypes tys = mapNF_Tc zonkTcType tys
328 zonkTcClassConstraints cts = mapNF_Tc zonk cts
329 where zonk (clas, tys)
330 = zonkTcTypes tys `thenNF_Tc` \ new_tys ->
331 returnNF_Tc (clas, new_tys)
333 zonkTcThetaType :: TcThetaType -> NF_TcM TcThetaType
334 zonkTcThetaType theta = mapNF_Tc zonkTcPredType theta
336 zonkTcPredType :: TcPredType -> NF_TcM TcPredType
337 zonkTcPredType (ClassP c ts)
338 = zonkTcTypes ts `thenNF_Tc` \ new_ts ->
339 returnNF_Tc (ClassP c new_ts)
340 zonkTcPredType (IParam n t)
341 = zonkTcType t `thenNF_Tc` \ new_t ->
342 returnNF_Tc (IParam n new_t)
345 ------------------- These ...ToType, ...ToKind versions
346 are used at the end of type checking
349 zonkKindEnv :: [(Name, TcKind)] -> NF_TcM [(Name, Kind)]
351 = mapNF_Tc zonk_it pairs
353 zonk_it (name, tc_kind) = zonkType zonk_unbound_kind_var tc_kind `thenNF_Tc` \ kind ->
354 returnNF_Tc (name, kind)
356 -- When zonking a kind, we want to
357 -- zonk a *kind* variable to (Type *)
358 -- zonk a *boxity* variable to *
359 zonk_unbound_kind_var kv | tyVarKind kv `eqKind` superKind = putTcTyVar kv liftedTypeKind
360 | tyVarKind kv `eqKind` superBoxity = putTcTyVar kv liftedBoxity
361 | otherwise = pprPanic "zonkKindEnv" (ppr kv)
363 zonkTcTypeToType :: TcType -> NF_TcM Type
364 zonkTcTypeToType ty = zonkType zonk_unbound_tyvar ty
366 -- Zonk a mutable but unbound type variable to an arbitrary type
367 -- We know it's unbound even though we don't carry an environment,
368 -- because at the binding site for a type variable we bind the
369 -- mutable tyvar to a fresh immutable one. So the mutable store
370 -- plays the role of an environment. If we come across a mutable
371 -- type variable that isn't so bound, it must be completely free.
372 zonk_unbound_tyvar tv = putTcTyVar tv (mkArbitraryType tv)
375 -- When the type checker finds a type variable with no binding,
376 -- which means it can be instantiated with an arbitrary type, it
377 -- usually instantiates it to Void. Eg.
381 -- length Void (Nil Void)
383 -- But in really obscure programs, the type variable might have
384 -- a kind other than *, so we need to invent a suitably-kinded type.
388 -- List for kind *->*
389 -- Tuple for kind *->...*->*
391 -- which deals with most cases. (Previously, it only dealt with
394 -- In the other cases, it just makes up a TyCon with a suitable
395 -- kind. If this gets into an interface file, anyone reading that
396 -- file won't understand it. This is fixable (by making the client
397 -- of the interface file make up a TyCon too) but it is tiresome and
398 -- never happens, so I am leaving it
400 mkArbitraryType :: TcTyVar -> Type
401 -- Make up an arbitrary type whose kind is the same as the tyvar.
402 -- We'll use this to instantiate the (unbound) tyvar.
404 | isAnyTypeKind kind = voidTy -- The vastly common case
405 | otherwise = TyConApp tycon []
408 (args,res) = Type.splitFunTys kind -- Kinds are simple; use Type.splitFunTys
410 tycon | kind `eqKind` tyConKind listTyCon -- *->*
411 = listTyCon -- No tuples this size
413 | all isTypeKind args && isTypeKind res
414 = tupleTyCon Boxed (length args) -- *-> ... ->*->*
417 = pprTrace "Urk! Inventing strangely-kinded void TyCon:" (ppr tc_name $$ ppr kind) $
418 mkPrimTyCon tc_name kind 0 [] VoidRep
419 -- Same name as the tyvar, apart from making it start with a colon (sigh)
420 -- I dread to think what will happen if this gets out into an
421 -- interface file. Catastrophe likely. Major sigh.
423 tc_name = mkInternalName (getUnique tv) (mkDerivedTyConOcc (getOccName tv)) noSrcLoc
425 -- zonkTcTyVarToTyVar is applied to the *binding* occurrence
426 -- of a type variable, at the *end* of type checking. It changes
427 -- the *mutable* type variable into an *immutable* one.
429 -- It does this by making an immutable version of tv and binds tv to it.
430 -- Now any bound occurences of the original type variable will get
431 -- zonked to the immutable version.
433 zonkTcTyVarToTyVar :: TcTyVar -> NF_TcM TyVar
434 zonkTcTyVarToTyVar tv
436 -- Make an immutable version, defaulting
437 -- the kind to lifted if necessary
438 immut_tv = mkTyVar (tyVarName tv) (defaultKind (tyVarKind tv))
439 immut_tv_ty = mkTyVarTy immut_tv
441 zap tv = putTcTyVar tv immut_tv_ty
442 -- Bind the mutable version to the immutable one
444 -- If the type variable is mutable, then bind it to immut_tv_ty
445 -- so that all other occurrences of the tyvar will get zapped too
446 zonkTyVar zap tv `thenNF_Tc` \ ty2 ->
448 -- This warning shows up if the allegedly-unbound tyvar is
449 -- already bound to something. It can actually happen, and
450 -- in a harmless way (see [Silly Type Synonyms] below) so
451 -- it's only a warning
452 WARN( not (immut_tv_ty `tcEqType` ty2), ppr tv $$ ppr immut_tv $$ ppr ty2 )
457 [Silly Type Synonyms]
460 type C u a = u -- Note 'a' unused
462 foo :: (forall a. C u a -> C u a) -> u
466 bar = foo (\t -> t + t)
468 * From the (\t -> t+t) we get type {Num d} => d -> d
471 * Now unify with type of foo's arg, and we get:
472 {Num (C d a)} => C d a -> C d a
475 * Now abstract over the 'a', but float out the Num (C d a) constraint
476 because it does not 'really' mention a. (see Type.tyVarsOfType)
477 The arg to foo becomes
480 * So we get a dict binding for Num (C d a), which is zonked to give
483 * Then the /\a abstraction has a zonked 'a' in it.
485 All very silly. I think its harmless to ignore the problem.
488 %************************************************************************
490 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
492 %* For internal use only! *
494 %************************************************************************
497 -- zonkType is used for Kinds as well
499 -- For unbound, mutable tyvars, zonkType uses the function given to it
500 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
501 -- type variable and zonks the kind too
503 zonkType :: (TcTyVar -> NF_TcM Type) -- What to do with unbound mutable type variables
504 -- see zonkTcType, and zonkTcTypeToType
507 zonkType unbound_var_fn ty
510 go (TyConApp tycon tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' ->
511 returnNF_Tc (TyConApp tycon tys')
513 go (NoteTy (SynNote ty1) ty2) = go ty1 `thenNF_Tc` \ ty1' ->
514 go ty2 `thenNF_Tc` \ ty2' ->
515 returnNF_Tc (NoteTy (SynNote ty1') ty2')
517 go (NoteTy (FTVNote _) ty2) = go ty2 -- Discard free-tyvar annotations
519 go (SourceTy p) = go_pred p `thenNF_Tc` \ p' ->
520 returnNF_Tc (SourceTy p')
522 go (FunTy arg res) = go arg `thenNF_Tc` \ arg' ->
523 go res `thenNF_Tc` \ res' ->
524 returnNF_Tc (FunTy arg' res')
526 go (AppTy fun arg) = go fun `thenNF_Tc` \ fun' ->
527 go arg `thenNF_Tc` \ arg' ->
528 returnNF_Tc (mkAppTy fun' arg')
529 -- NB the mkAppTy; we might have instantiated a
530 -- type variable to a type constructor, so we need
531 -- to pull the TyConApp to the top.
533 -- The two interesting cases!
534 go (TyVarTy tyvar) = zonkTyVar unbound_var_fn tyvar
536 go (ForAllTy tyvar ty) = zonkTcTyVarToTyVar tyvar `thenNF_Tc` \ tyvar' ->
537 go ty `thenNF_Tc` \ ty' ->
538 returnNF_Tc (ForAllTy tyvar' ty')
540 go_pred (ClassP c tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' ->
541 returnNF_Tc (ClassP c tys')
542 go_pred (NType tc tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' ->
543 returnNF_Tc (NType tc tys')
544 go_pred (IParam n ty) = go ty `thenNF_Tc` \ ty' ->
545 returnNF_Tc (IParam n ty')
547 zonkTyVar :: (TcTyVar -> NF_TcM Type) -- What to do for an unbound mutable variable
548 -> TcTyVar -> NF_TcM TcType
549 zonkTyVar unbound_var_fn tyvar
550 | not (isMutTyVar tyvar) -- Not a mutable tyvar. This can happen when
551 -- zonking a forall type, when the bound type variable
552 -- needn't be mutable
553 = ASSERT( isTyVar tyvar ) -- Should not be any immutable kind vars
554 returnNF_Tc (TyVarTy tyvar)
557 = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
559 Nothing -> unbound_var_fn tyvar -- Mutable and unbound
560 Just other_ty -> zonkType unbound_var_fn other_ty -- Bound
565 %************************************************************************
567 \subsection{Checking a user type}
569 %************************************************************************
571 When dealing with a user-written type, we first translate it from an HsType
572 to a Type, performing kind checking, and then check various things that should
573 be true about it. We don't want to perform these checks at the same time
574 as the initial translation because (a) they are unnecessary for interface-file
575 types and (b) when checking a mutually recursive group of type and class decls,
576 we can't "look" at the tycons/classes yet. Also, the checks are are rather
577 diverse, and used to really mess up the other code.
579 One thing we check for is 'rank'.
581 Rank 0: monotypes (no foralls)
582 Rank 1: foralls at the front only, Rank 0 inside
583 Rank 2: foralls at the front, Rank 1 on left of fn arrow,
585 basic ::= tyvar | T basic ... basic
587 r2 ::= forall tvs. cxt => r2a
588 r2a ::= r1 -> r2a | basic
589 r1 ::= forall tvs. cxt => r0
590 r0 ::= r0 -> r0 | basic
592 Another thing is to check that type synonyms are saturated.
593 This might not necessarily show up in kind checking.
595 data T k = MkT (k Int)
601 = FunSigCtxt Name -- Function type signature
602 | ExprSigCtxt -- Expression type signature
603 | ConArgCtxt Name -- Data constructor argument
604 | TySynCtxt Name -- RHS of a type synonym decl
605 | GenPatCtxt -- Pattern in generic decl
606 -- f{| a+b |} (Inl x) = ...
607 | PatSigCtxt -- Type sig in pattern
609 | ResSigCtxt -- Result type sig
611 | ForSigCtxt Name -- Foreign inport or export signature
612 | RuleSigCtxt Name -- Signature on a forall'd variable in a RULE
614 -- Notes re TySynCtxt
615 -- We allow type synonyms that aren't types; e.g. type List = []
617 -- If the RHS mentions tyvars that aren't in scope, we'll
618 -- quantify over them:
619 -- e.g. type T = a->a
620 -- will become type T = forall a. a->a
622 -- With gla-exts that's right, but for H98 we should complain.
625 pprUserTypeCtxt (FunSigCtxt n) = ptext SLIT("the type signature for") <+> quotes (ppr n)
626 pprUserTypeCtxt ExprSigCtxt = ptext SLIT("an expression type signature")
627 pprUserTypeCtxt (ConArgCtxt c) = ptext SLIT("the type of constructor") <+> quotes (ppr c)
628 pprUserTypeCtxt (TySynCtxt c) = ptext SLIT("the RHS of a type synonym declaration") <+> quotes (ppr c)
629 pprUserTypeCtxt GenPatCtxt = ptext SLIT("the type pattern of a generic definition")
630 pprUserTypeCtxt PatSigCtxt = ptext SLIT("a pattern type signature")
631 pprUserTypeCtxt ResSigCtxt = ptext SLIT("a result type signature")
632 pprUserTypeCtxt (ForSigCtxt n) = ptext SLIT("the foreign signature for") <+> quotes (ppr n)
633 pprUserTypeCtxt (RuleSigCtxt n) = ptext SLIT("the type signature on") <+> quotes (ppr n)
637 checkValidType :: UserTypeCtxt -> Type -> TcM ()
638 -- Checks that the type is valid for the given context
639 checkValidType ctxt ty
640 = doptsTc Opt_GlasgowExts `thenNF_Tc` \ gla_exts ->
642 rank | gla_exts = Arbitrary
644 = case ctxt of -- Haskell 98
648 TySynCtxt _ -> Rank 0
649 ExprSigCtxt -> Rank 1
650 FunSigCtxt _ -> Rank 1
651 ConArgCtxt _ -> Rank 1 -- We are given the type of the entire
652 -- constructor, hence rank 1
653 ForSigCtxt _ -> Rank 1
654 RuleSigCtxt _ -> Rank 1
656 actual_kind = typeKind ty
658 actual_kind_is_lifted = actual_kind `eqKind` liftedTypeKind
660 kind_ok = case ctxt of
661 TySynCtxt _ -> True -- Any kind will do
662 GenPatCtxt -> actual_kind_is_lifted
663 ForSigCtxt _ -> actual_kind_is_lifted
664 other -> isTypeKind actual_kind
666 ubx_tup | not gla_exts = UT_NotOk
667 | otherwise = case ctxt of
670 -- Unboxed tuples ok in function results,
671 -- but for type synonyms we allow them even at
674 tcAddErrCtxt (checkTypeCtxt ctxt ty) $
676 -- Check that the thing has kind Type, and is lifted if necessary
677 checkTc kind_ok (kindErr actual_kind) `thenTc_`
679 -- Check the internal validity of the type itself
680 check_poly_type rank ubx_tup ty
683 checkTypeCtxt ctxt ty
684 = vcat [ptext SLIT("In the type:") <+> ppr_ty ty,
685 ptext SLIT("While checking") <+> pprUserTypeCtxt ctxt ]
687 -- Hack alert. If there are no tyvars, (ppr sigma_ty) will print
688 -- something strange like {Eq k} -> k -> k, because there is no
689 -- ForAll at the top of the type. Since this is going to the user
690 -- we want it to look like a proper Haskell type even then; hence the hack
692 -- This shows up in the complaint about
694 -- op :: Eq a => a -> a
695 ppr_ty ty | null forall_tvs && notNull theta = pprTheta theta <+> ptext SLIT("=>") <+> ppr tau
698 (forall_tvs, theta, tau) = tcSplitSigmaTy ty
703 data Rank = Rank Int | Arbitrary
705 decRank :: Rank -> Rank
706 decRank Arbitrary = Arbitrary
707 decRank (Rank n) = Rank (n-1)
709 ----------------------------------------
710 data UbxTupFlag = UT_Ok | UT_NotOk
711 -- The "Ok" version means "ok if -fglasgow-exts is on"
713 ----------------------------------------
714 check_poly_type :: Rank -> UbxTupFlag -> Type -> TcM ()
715 check_poly_type (Rank 0) ubx_tup ty
716 = check_tau_type (Rank 0) ubx_tup ty
718 check_poly_type rank ubx_tup ty
720 (tvs, theta, tau) = tcSplitSigmaTy ty
722 check_valid_theta SigmaCtxt theta `thenTc_`
723 check_tau_type (decRank rank) ubx_tup tau `thenTc_`
724 checkFreeness tvs theta `thenTc_`
725 checkAmbiguity tvs theta (tyVarsOfType tau)
727 ----------------------------------------
728 check_arg_type :: Type -> TcM ()
729 -- The sort of type that can instantiate a type variable,
730 -- or be the argument of a type constructor.
731 -- Not an unboxed tuple, not a forall.
732 -- Other unboxed types are very occasionally allowed as type
733 -- arguments depending on the kind of the type constructor
735 -- For example, we want to reject things like:
737 -- instance Ord a => Ord (forall s. T s a)
739 -- g :: T s (forall b.b)
741 -- NB: unboxed tuples can have polymorphic or unboxed args.
742 -- This happens in the workers for functions returning
743 -- product types with polymorphic components.
744 -- But not in user code.
745 -- Anyway, they are dealt with by a special case in check_tau_type
748 = check_tau_type (Rank 0) UT_NotOk ty `thenTc_`
749 checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
751 ----------------------------------------
752 check_tau_type :: Rank -> UbxTupFlag -> Type -> TcM ()
753 -- Rank is allowed rank for function args
754 -- No foralls otherwise
756 check_tau_type rank ubx_tup ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty)
757 check_tau_type rank ubx_tup (SourceTy sty) = getDOptsTc `thenNF_Tc` \ dflags ->
758 check_source_ty dflags TypeCtxt sty
759 check_tau_type rank ubx_tup (TyVarTy _) = returnTc ()
760 check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
761 = check_poly_type rank UT_NotOk arg_ty `thenTc_`
762 check_tau_type rank UT_Ok res_ty
764 check_tau_type rank ubx_tup (AppTy ty1 ty2)
765 = check_arg_type ty1 `thenTc_` check_arg_type ty2
767 check_tau_type rank ubx_tup (NoteTy (SynNote syn) ty)
768 -- Synonym notes are built only when the synonym is
769 -- saturated (see Type.mkSynTy)
770 = doptsTc Opt_GlasgowExts `thenNF_Tc` \ gla_exts ->
772 -- If -fglasgow-exts then don't check the 'note' part.
773 -- This allows us to instantiate a synonym defn with a
774 -- for-all type, or with a partially-applied type synonym.
775 -- e.g. type T a b = a
778 -- Here, T is partially applied, so it's illegal in H98.
779 -- But if you expand S first, then T we get just
784 -- For H98, do check the un-expanded part
785 check_tau_type rank ubx_tup syn
788 check_tau_type rank ubx_tup ty
790 check_tau_type rank ubx_tup (NoteTy other_note ty)
791 = check_tau_type rank ubx_tup ty
793 check_tau_type rank ubx_tup ty@(TyConApp tc tys)
795 = -- NB: Type.mkSynTy builds a TyConApp (not a NoteTy) for an unsaturated
796 -- synonym application, leaving it to checkValidType (i.e. right here)
798 checkTc syn_arity_ok arity_msg `thenTc_`
799 mapTc_ check_arg_type tys
801 | isUnboxedTupleTyCon tc
802 = doptsTc Opt_GlasgowExts `thenNF_Tc` \ gla_exts ->
803 checkTc (ubx_tup_ok gla_exts) ubx_tup_msg `thenTc_`
804 mapTc_ (check_tau_type (Rank 0) UT_Ok) tys
805 -- Args are allowed to be unlifted, or
806 -- more unboxed tuples, so can't use check_arg_ty
809 = mapTc_ check_arg_type tys
812 ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False }
814 syn_arity_ok = tc_arity <= n_args
815 -- It's OK to have an *over-applied* type synonym
816 -- data Tree a b = ...
817 -- type Foo a = Tree [a]
818 -- f :: Foo a b -> ...
820 tc_arity = tyConArity tc
822 arity_msg = arityErr "Type synonym" (tyConName tc) tc_arity n_args
823 ubx_tup_msg = ubxArgTyErr ty
825 ----------------------------------------
826 forAllTyErr ty = ptext SLIT("Illegal polymorphic type:") <+> ppr_ty ty
827 unliftedArgErr ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr_ty ty
828 ubxArgTyErr ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr_ty ty
829 kindErr kind = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
835 is ambiguous if P contains generic variables
836 (i.e. one of the Vs) that are not mentioned in tau
838 However, we need to take account of functional dependencies
839 when we speak of 'mentioned in tau'. Example:
840 class C a b | a -> b where ...
842 forall x y. (C x y) => x
843 is not ambiguous because x is mentioned and x determines y
845 NB; the ambiguity check is only used for *user* types, not for types
846 coming from inteface files. The latter can legitimately have
847 ambiguous types. Example
849 class S a where s :: a -> (Int,Int)
850 instance S Char where s _ = (1,1)
851 f:: S a => [a] -> Int -> (Int,Int)
852 f (_::[a]) x = (a*x,b)
853 where (a,b) = s (undefined::a)
855 Here the worker for f gets the type
856 fw :: forall a. S a => Int -> (# Int, Int #)
858 If the list of tv_names is empty, we have a monotype, and then we
859 don't need to check for ambiguity either, because the test can't fail
863 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
864 checkAmbiguity forall_tyvars theta tau_tyvars
865 = mapTc_ complain (filter is_ambig theta)
867 complain pred = addErrTc (ambigErr pred)
868 extended_tau_vars = grow theta tau_tyvars
869 is_ambig pred = any ambig_var (varSetElems (tyVarsOfPred pred))
871 ambig_var ct_var = (ct_var `elem` forall_tyvars) &&
872 not (ct_var `elemVarSet` extended_tau_vars)
874 is_free ct_var = not (ct_var `elem` forall_tyvars)
877 = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
878 nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
879 ptext SLIT("must be reachable from the type after the '=>'"))]
882 In addition, GHC insists that at least one type variable
883 in each constraint is in V. So we disallow a type like
884 forall a. Eq b => b -> b
885 even in a scope where b is in scope.
888 checkFreeness forall_tyvars theta
889 = mapTc_ complain (filter is_free theta)
891 is_free pred = not (isIPPred pred)
892 && not (any bound_var (varSetElems (tyVarsOfPred pred)))
893 bound_var ct_var = ct_var `elem` forall_tyvars
894 complain pred = addErrTc (freeErr pred)
897 = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
898 ptext SLIT("are already in scope"),
899 nest 4 (ptext SLIT("(at least one must be universally quantified here)"))
904 %************************************************************************
906 \subsection{Checking a theta or source type}
908 %************************************************************************
912 = ClassSCCtxt Name -- Superclasses of clas
913 | SigmaCtxt -- Context of a normal for-all type
914 | DataTyCtxt Name -- Context of a data decl
915 | TypeCtxt -- Source type in an ordinary type
916 | InstThetaCtxt -- Context of an instance decl
917 | InstHeadCtxt -- Head of an instance decl
919 pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
920 pprSourceTyCtxt SigmaCtxt = ptext SLIT("the context of a polymorphic type")
921 pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
922 pprSourceTyCtxt InstThetaCtxt = ptext SLIT("the context of an instance declaration")
923 pprSourceTyCtxt InstHeadCtxt = ptext SLIT("the head of an instance declaration")
924 pprSourceTyCtxt TypeCtxt = ptext SLIT("the context of a type")
928 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
929 checkValidTheta ctxt theta
930 = tcAddErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
932 -------------------------
933 check_valid_theta ctxt []
935 check_valid_theta ctxt theta
936 = getDOptsTc `thenNF_Tc` \ dflags ->
937 warnTc (notNull dups) (dupPredWarn dups) `thenNF_Tc_`
938 mapTc_ (check_source_ty dflags ctxt) theta
940 (_,dups) = removeDups tcCmpPred theta
942 -------------------------
943 check_source_ty dflags ctxt pred@(ClassP cls tys)
944 = -- Class predicates are valid in all contexts
945 mapTc_ check_arg_type tys `thenTc_`
946 checkTc (arity == n_tys) arity_err `thenTc_`
947 checkTc (check_class_pred_tys dflags ctxt tys)
948 (predTyVarErr pred $$ how_to_allow)
951 class_name = className cls
952 arity = classArity cls
954 arity_err = arityErr "Class" class_name arity n_tys
956 how_to_allow = case ctxt of
957 InstHeadCtxt -> empty -- Should not happen
958 InstThetaCtxt -> parens undecidableMsg
959 other -> parens (ptext SLIT("Use -fglasgow-exts to permit this"))
961 check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
962 -- Implicit parameters only allows in type
963 -- signatures; not in instance decls, superclasses etc
964 -- The reason for not allowing implicit params in instances is a bit subtle
965 -- If we allowed instance (?x::Int, Eq a) => Foo [a] where ...
966 -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
967 -- discharge all the potential usas of the ?x in e. For example, a
968 -- constraint Foo [Int] might come out of e,and applying the
969 -- instance decl would show up two uses of ?x.
971 check_source_ty dflags TypeCtxt (NType tc tys) = mapTc_ check_arg_type tys
974 check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
976 -------------------------
977 check_class_pred_tys dflags ctxt tys
979 InstHeadCtxt -> True -- We check for instance-head
980 -- formation in checkValidInstHead
981 InstThetaCtxt -> undecidable_ok || all isTyVarTy tys
982 other -> gla_exts || all tyvar_head tys
984 undecidable_ok = dopt Opt_AllowUndecidableInstances dflags
985 gla_exts = dopt Opt_GlasgowExts dflags
987 -------------------------
988 tyvar_head ty -- Haskell 98 allows predicates of form
989 | tcIsTyVarTy ty = True -- C (a ty1 .. tyn)
990 | otherwise -- where a is a type variable
991 = case tcSplitAppTy_maybe ty of
992 Just (ty, _) -> tyvar_head ty
997 badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprSourceType sty
998 predTyVarErr pred = ptext SLIT("Non-type variables in constraint:") <+> pprPred pred
999 dupPredWarn dups = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
1001 checkThetaCtxt ctxt theta
1002 = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
1003 ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
1007 %************************************************************************
1009 \subsection{Validity check for TyCons}
1011 %************************************************************************
1013 checkValidTyCon is called once the mutually-recursive knot has been
1014 tied, so we can look at things freely.
1017 checkValidTyCon :: TyCon -> TcM ()
1019 | isSynTyCon tc = checkValidType (TySynCtxt name) syn_rhs
1021 = -- Check the context on the data decl
1022 checkValidTheta (DataTyCtxt name) (tyConTheta tc) `thenTc_`
1024 -- Check arg types of data constructors
1025 mapTc_ checkValidDataCon data_cons `thenTc_`
1027 -- Check that fields with the same name share a type
1028 mapTc_ check_fields groups
1032 (_, syn_rhs) = getSynTyConDefn tc
1033 data_cons = tyConDataCons tc
1035 fields = [field | con <- data_cons, field <- dataConFieldLabels con]
1036 groups = equivClasses cmp_name fields
1037 cmp_name field1 field2 = fieldLabelName field1 `compare` fieldLabelName field2
1039 check_fields fields@(first_field_label : other_fields)
1040 -- These fields all have the same name, but are from
1041 -- different constructors in the data type
1042 = -- Check that all the fields in the group have the same type
1043 -- NB: this check assumes that all the constructors of a given
1044 -- data type use the same type variables
1045 checkTc (all (tcEqType field_ty) other_tys) (fieldTypeMisMatch field_name)
1047 field_ty = fieldLabelType first_field_label
1048 field_name = fieldLabelName first_field_label
1049 other_tys = map fieldLabelType other_fields
1051 checkValidDataCon :: DataCon -> TcM ()
1052 checkValidDataCon con
1053 = checkValidType ctxt (idType (dataConWrapId con)) `thenTc_`
1054 -- This checks the argument types and
1055 -- ambiguity of the existential context (if any)
1056 tcAddErrCtxt (existentialCtxt con)
1057 (checkFreeness ex_tvs ex_theta)
1059 ctxt = ConArgCtxt (dataConName con)
1060 (_, _, ex_tvs, ex_theta, _, _) = dataConSig con
1063 fieldTypeMisMatch field_name
1064 = sep [ptext SLIT("Different constructors give different types for field"), quotes (ppr field_name)]
1066 existentialCtxt con = ptext SLIT("When checking the existential context of constructor")
1067 <+> quotes (ppr con)
1071 checkValidClass is called once the mutually-recursive knot has been
1072 tied, so we can look at things freely.
1075 checkValidClass :: Class -> TcM ()
1077 = -- CHECK ARITY 1 FOR HASKELL 1.4
1078 doptsTc Opt_GlasgowExts `thenTc` \ gla_exts ->
1080 -- Check that the class is unary, unless GlaExs
1081 checkTc (notNull tyvars) (nullaryClassErr cls) `thenTc_`
1082 checkTc (gla_exts || unary) (classArityErr cls) `thenTc_`
1084 -- Check the super-classes
1085 checkValidTheta (ClassSCCtxt (className cls)) theta `thenTc_`
1087 -- Check the class operations
1088 mapTc_ check_op op_stuff `thenTc_`
1090 -- Check that if the class has generic methods, then the
1091 -- class has only one parameter. We can't do generic
1092 -- multi-parameter type classes!
1093 checkTc (unary || no_generics) (genericMultiParamErr cls)
1096 (tyvars, theta, _, op_stuff) = classBigSig cls
1097 unary = isSingleton tyvars
1098 no_generics = null [() | (_, GenDefMeth) <- op_stuff]
1100 check_op (sel_id, dm)
1101 = checkValidTheta SigmaCtxt (tail theta) `thenTc_`
1102 -- The 'tail' removes the initial (C a) from the
1103 -- class itself, leaving just the method type
1105 checkValidType (FunSigCtxt op_name) tau `thenTc_`
1107 -- Check that for a generic method, the type of
1108 -- the method is sufficiently simple
1109 checkTc (dm /= GenDefMeth || validGenericMethodType op_ty)
1110 (badGenericMethodType op_name op_ty)
1112 op_name = idName sel_id
1113 op_ty = idType sel_id
1114 (_,theta,tau) = tcSplitSigmaTy op_ty
1117 = ptext SLIT("No parameters for class") <+> quotes (ppr cls)
1120 = vcat [ptext SLIT("Too many parameters for class") <+> quotes (ppr cls),
1121 parens (ptext SLIT("Use -fglasgow-exts to allow multi-parameter classes"))]
1123 genericMultiParamErr clas
1124 = ptext SLIT("The multi-parameter class") <+> quotes (ppr clas) <+>
1125 ptext SLIT("cannot have generic methods")
1127 badGenericMethodType op op_ty
1128 = hang (ptext SLIT("Generic method type is too complex"))
1129 4 (vcat [ppr op <+> dcolon <+> ppr op_ty,
1130 ptext SLIT("You can only use type variables, arrows, and tuples")])
1134 %************************************************************************
1136 \subsection{Checking for a decent instance head type}
1138 %************************************************************************
1140 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1141 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1143 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1144 flag is on, or (2)~the instance is imported (they must have been
1145 compiled elsewhere). In these cases, we let them go through anyway.
1147 We can also have instances for functions: @instance Foo (a -> b) ...@.
1150 checkValidInstHead :: Type -> TcM (Class, [TcType])
1152 checkValidInstHead ty -- Should be a source type
1153 = case tcSplitPredTy_maybe ty of {
1154 Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
1157 case getClassPredTys_maybe pred of {
1158 Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
1161 getDOptsTc `thenNF_Tc` \ dflags ->
1162 mapTc_ check_arg_type tys `thenTc_`
1163 check_inst_head dflags clas tys `thenTc_`
1164 returnTc (clas, tys)
1167 check_inst_head dflags clas tys
1169 -- A user declaration of a CCallable/CReturnable instance
1170 -- must be for a "boxed primitive" type.
1171 (clas `hasKey` cCallableClassKey
1172 && not (ccallable_type first_ty))
1173 || (clas `hasKey` cReturnableClassKey
1174 && not (creturnable_type first_ty))
1175 = failWithTc (nonBoxedPrimCCallErr clas first_ty)
1177 -- If GlasgowExts then check at least one isn't a type variable
1178 | dopt Opt_GlasgowExts dflags
1179 = check_tyvars dflags clas tys
1181 -- WITH HASKELL 1.4, MUST HAVE C (T a b c)
1183 Just (tycon, arg_tys) <- tcSplitTyConApp_maybe first_ty,
1184 not (isSynTyCon tycon), -- ...but not a synonym
1185 all tcIsTyVarTy arg_tys, -- Applied to type variables
1186 equalLength (varSetElems (tyVarsOfTypes arg_tys)) arg_tys
1187 -- This last condition checks that all the type variables are distinct
1191 = failWithTc (instTypeErr (pprClassPred clas tys) head_shape_msg)
1194 (first_ty : _) = tys
1196 ccallable_type ty = isFFIArgumentTy dflags PlayRisky ty
1197 creturnable_type ty = isFFIImportResultTy dflags ty
1199 head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
1200 text "where T is not a synonym, and a,b,c are distinct type variables")
1202 check_tyvars dflags clas tys
1203 -- Check that at least one isn't a type variable
1204 -- unless -fallow-undecideable-instances
1205 | dopt Opt_AllowUndecidableInstances dflags = returnTc ()
1206 | not (all tcIsTyVarTy tys) = returnTc ()
1207 | otherwise = failWithTc (instTypeErr (pprClassPred clas tys) msg)
1209 msg = parens (ptext SLIT("There must be at least one non-type-variable in the instance head")
1212 undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
1216 instTypeErr pp_ty msg
1217 = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,
1220 nonBoxedPrimCCallErr clas inst_ty
1221 = hang (ptext SLIT("Unacceptable instance type for ccall-ish class"))
1222 4 (pprClassPred clas [inst_ty])