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,
86 mkInternalName, mkDerivedTyConOcc,
87 mkSystemTvNameEncoded,
90 import BasicTypes ( Boxity(Boxed) )
91 import CmdLineOpts ( dopt, DynFlag(..) )
92 import Unique ( Uniquable(..) )
93 import SrcLoc ( noSrcLoc )
94 import Util ( nOfThem, isSingleton, equalLength, notNull )
95 import ListSetOps ( equivClasses, removeDups )
100 %************************************************************************
102 \subsection{New type variables}
104 %************************************************************************
107 newTyVar :: Kind -> NF_TcM TcTyVar
109 = tcGetUnique `thenNF_Tc` \ uniq ->
110 tcNewMutTyVar (mkSystemTvNameEncoded uniq FSLIT("t")) kind VanillaTv
112 newTyVarTy :: Kind -> NF_TcM TcType
114 = newTyVar kind `thenNF_Tc` \ tc_tyvar ->
115 returnNF_Tc (TyVarTy tc_tyvar)
117 newTyVarTys :: Int -> Kind -> NF_TcM [TcType]
118 newTyVarTys n kind = mapNF_Tc newTyVarTy (nOfThem n kind)
120 newKindVar :: NF_TcM TcKind
122 = tcGetUnique `thenNF_Tc` \ uniq ->
123 tcNewMutTyVar (mkSystemTvNameEncoded uniq FSLIT("k")) superKind VanillaTv `thenNF_Tc` \ kv ->
124 returnNF_Tc (TyVarTy kv)
126 newKindVars :: Int -> NF_TcM [TcKind]
127 newKindVars n = mapNF_Tc (\ _ -> newKindVar) (nOfThem n ())
129 newBoxityVar :: NF_TcM TcKind
131 = tcGetUnique `thenNF_Tc` \ uniq ->
132 tcNewMutTyVar (mkSystemTvNameEncoded uniq FSLIT("bx")) superBoxity VanillaTv `thenNF_Tc` \ kv ->
133 returnNF_Tc (TyVarTy kv)
137 %************************************************************************
139 \subsection{'hole' type variables}
141 %************************************************************************
144 newHoleTyVarTy :: NF_TcM TcType
145 = tcGetUnique `thenNF_Tc` \ uniq ->
146 tcNewMutTyVar (mkSystemTvNameEncoded uniq FSLIT("h")) openTypeKind HoleTv `thenNF_Tc` \ tv ->
147 returnNF_Tc (TyVarTy tv)
149 readHoleResult :: TcType -> NF_TcM TcType
150 -- Read the answer out of a hole, constructed by newHoleTyVarTy
151 readHoleResult (TyVarTy tv)
152 = ASSERT( isHoleTyVar tv )
153 getTcTyVar tv `thenNF_Tc` \ maybe_res ->
155 Just ty -> returnNF_Tc ty
156 Nothing -> pprPanic "readHoleResult: empty" (ppr tv)
157 readHoleResult ty = pprPanic "readHoleResult: not hole" (ppr ty)
159 zapToType :: TcType -> NF_TcM TcType
160 zapToType (TyVarTy tv)
162 = getTcTyVar tv `thenNF_Tc` \ maybe_res ->
164 Nothing -> newTyVarTy openTypeKind `thenNF_Tc` \ ty ->
165 putTcTyVar tv ty `thenNF_Tc_`
167 Just ty -> returnNF_Tc ty -- No need to loop; we never
168 -- have chains of holes
170 zapToType other_ty = returnNF_Tc other_ty
173 %************************************************************************
175 \subsection{Type instantiation}
177 %************************************************************************
179 Instantiating a bunch of type variables
182 tcInstTyVars :: TyVarDetails -> [TyVar]
183 -> NF_TcM ([TcTyVar], [TcType], Subst)
185 tcInstTyVars tv_details tyvars
186 = mapNF_Tc (tcInstTyVar tv_details) tyvars `thenNF_Tc` \ tc_tyvars ->
188 tys = mkTyVarTys tc_tyvars
190 returnNF_Tc (tc_tyvars, tys, mkTopTyVarSubst tyvars tys)
191 -- Since the tyvars are freshly made,
192 -- they cannot possibly be captured by
193 -- any existing for-alls. Hence mkTopTyVarSubst
195 tcInstTyVar tv_details tyvar
196 = tcGetUnique `thenNF_Tc` \ uniq ->
198 name = setNameUnique (tyVarName tyvar) uniq
199 -- Note that we don't change the print-name
200 -- This won't confuse the type checker but there's a chance
201 -- that two different tyvars will print the same way
202 -- in an error message. -dppr-debug will show up the difference
203 -- Better watch out for this. If worst comes to worst, just
206 tcNewMutTyVar name (tyVarKind tyvar) tv_details
208 tcInstType :: TyVarDetails -> TcType -> NF_TcM ([TcTyVar], TcThetaType, TcType)
209 -- tcInstType instantiates the outer-level for-alls of a TcType with
210 -- fresh (mutable) type variables, splits off the dictionary part,
211 -- and returns the pieces.
212 tcInstType tv_details ty
213 = case tcSplitForAllTys ty of
214 ([], rho) -> -- There may be overloading despite no type variables;
215 -- (?x :: Int) => Int -> Int
217 (theta, tau) = tcSplitPhiTy rho
219 returnNF_Tc ([], theta, tau)
221 (tyvars, rho) -> tcInstTyVars tv_details tyvars `thenNF_Tc` \ (tyvars', _, tenv) ->
223 (theta, tau) = tcSplitPhiTy (substTy tenv rho)
225 returnNF_Tc (tyvars', theta, tau)
229 %************************************************************************
231 \subsection{Putting and getting mutable type variables}
233 %************************************************************************
236 putTcTyVar :: TcTyVar -> TcType -> NF_TcM TcType
237 getTcTyVar :: TcTyVar -> NF_TcM (Maybe TcType)
244 | not (isMutTyVar tyvar)
245 = pprTrace "putTcTyVar" (ppr tyvar) $
249 = ASSERT( isMutTyVar tyvar )
250 tcWriteMutTyVar tyvar (Just ty) `thenNF_Tc_`
254 Getting is more interesting. The easy thing to do is just to read, thus:
257 getTcTyVar tyvar = tcReadMutTyVar tyvar
260 But it's more fun to short out indirections on the way: If this
261 version returns a TyVar, then that TyVar is unbound. If it returns
262 any other type, then there might be bound TyVars embedded inside it.
264 We return Nothing iff the original box was unbound.
268 | not (isMutTyVar tyvar)
269 = pprTrace "getTcTyVar" (ppr tyvar) $
270 returnNF_Tc (Just (mkTyVarTy tyvar))
273 = ASSERT2( isMutTyVar tyvar, ppr tyvar )
274 tcReadMutTyVar tyvar `thenNF_Tc` \ maybe_ty ->
276 Just ty -> short_out ty `thenNF_Tc` \ ty' ->
277 tcWriteMutTyVar tyvar (Just ty') `thenNF_Tc_`
278 returnNF_Tc (Just ty')
280 Nothing -> returnNF_Tc Nothing
282 short_out :: TcType -> NF_TcM TcType
283 short_out ty@(TyVarTy tyvar)
284 | not (isMutTyVar tyvar)
288 = tcReadMutTyVar tyvar `thenNF_Tc` \ maybe_ty ->
290 Just ty' -> short_out ty' `thenNF_Tc` \ ty' ->
291 tcWriteMutTyVar tyvar (Just ty') `thenNF_Tc_`
294 other -> returnNF_Tc ty
296 short_out other_ty = returnNF_Tc other_ty
300 %************************************************************************
302 \subsection{Zonking -- the exernal interfaces}
304 %************************************************************************
306 ----------------- Type variables
309 zonkTcTyVars :: [TcTyVar] -> NF_TcM [TcType]
310 zonkTcTyVars tyvars = mapNF_Tc zonkTcTyVar tyvars
312 zonkTcTyVarsAndFV :: [TcTyVar] -> NF_TcM TcTyVarSet
313 zonkTcTyVarsAndFV tyvars = mapNF_Tc zonkTcTyVar tyvars `thenNF_Tc` \ tys ->
314 returnNF_Tc (tyVarsOfTypes tys)
316 zonkTcTyVar :: TcTyVar -> NF_TcM TcType
317 zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnNF_Tc (TyVarTy tv)) tyvar
320 ----------------- Types
323 zonkTcType :: TcType -> NF_TcM TcType
324 zonkTcType ty = zonkType (\ tv -> returnNF_Tc (TyVarTy tv)) ty
326 zonkTcTypes :: [TcType] -> NF_TcM [TcType]
327 zonkTcTypes tys = mapNF_Tc zonkTcType tys
329 zonkTcClassConstraints cts = mapNF_Tc zonk cts
330 where zonk (clas, tys)
331 = zonkTcTypes tys `thenNF_Tc` \ new_tys ->
332 returnNF_Tc (clas, new_tys)
334 zonkTcThetaType :: TcThetaType -> NF_TcM TcThetaType
335 zonkTcThetaType theta = mapNF_Tc zonkTcPredType theta
337 zonkTcPredType :: TcPredType -> NF_TcM TcPredType
338 zonkTcPredType (ClassP c ts)
339 = zonkTcTypes ts `thenNF_Tc` \ new_ts ->
340 returnNF_Tc (ClassP c new_ts)
341 zonkTcPredType (IParam n t)
342 = zonkTcType t `thenNF_Tc` \ new_t ->
343 returnNF_Tc (IParam n new_t)
346 ------------------- These ...ToType, ...ToKind versions
347 are used at the end of type checking
350 zonkKindEnv :: [(Name, TcKind)] -> NF_TcM [(Name, Kind)]
352 = mapNF_Tc zonk_it pairs
354 zonk_it (name, tc_kind) = zonkType zonk_unbound_kind_var tc_kind `thenNF_Tc` \ kind ->
355 returnNF_Tc (name, kind)
357 -- When zonking a kind, we want to
358 -- zonk a *kind* variable to (Type *)
359 -- zonk a *boxity* variable to *
360 zonk_unbound_kind_var kv | tyVarKind kv `eqKind` superKind = putTcTyVar kv liftedTypeKind
361 | tyVarKind kv `eqKind` superBoxity = putTcTyVar kv liftedBoxity
362 | otherwise = pprPanic "zonkKindEnv" (ppr kv)
364 zonkTcTypeToType :: TcType -> NF_TcM Type
365 zonkTcTypeToType ty = zonkType zonk_unbound_tyvar ty
367 -- Zonk a mutable but unbound type variable to an arbitrary type
368 -- We know it's unbound even though we don't carry an environment,
369 -- because at the binding site for a type variable we bind the
370 -- mutable tyvar to a fresh immutable one. So the mutable store
371 -- plays the role of an environment. If we come across a mutable
372 -- type variable that isn't so bound, it must be completely free.
373 zonk_unbound_tyvar tv = putTcTyVar tv (mkArbitraryType tv)
376 -- When the type checker finds a type variable with no binding,
377 -- which means it can be instantiated with an arbitrary type, it
378 -- usually instantiates it to Void. Eg.
382 -- length Void (Nil Void)
384 -- But in really obscure programs, the type variable might have
385 -- a kind other than *, so we need to invent a suitably-kinded type.
389 -- List for kind *->*
390 -- Tuple for kind *->...*->*
392 -- which deals with most cases. (Previously, it only dealt with
395 -- In the other cases, it just makes up a TyCon with a suitable
396 -- kind. If this gets into an interface file, anyone reading that
397 -- file won't understand it. This is fixable (by making the client
398 -- of the interface file make up a TyCon too) but it is tiresome and
399 -- never happens, so I am leaving it
401 mkArbitraryType :: TcTyVar -> Type
402 -- Make up an arbitrary type whose kind is the same as the tyvar.
403 -- We'll use this to instantiate the (unbound) tyvar.
405 | isAnyTypeKind kind = voidTy -- The vastly common case
406 | otherwise = TyConApp tycon []
409 (args,res) = Type.splitFunTys kind -- Kinds are simple; use Type.splitFunTys
411 tycon | kind `eqKind` tyConKind listTyCon -- *->*
412 = listTyCon -- No tuples this size
414 | all isTypeKind args && isTypeKind res
415 = tupleTyCon Boxed (length args) -- *-> ... ->*->*
418 = pprTrace "Urk! Inventing strangely-kinded void TyCon:" (ppr tc_name $$ ppr kind) $
419 mkPrimTyCon tc_name kind 0 [] VoidRep
420 -- Same name as the tyvar, apart from making it start with a colon (sigh)
421 -- I dread to think what will happen if this gets out into an
422 -- interface file. Catastrophe likely. Major sigh.
424 tc_name = mkInternalName (getUnique tv) (mkDerivedTyConOcc (getOccName tv)) noSrcLoc
426 -- zonkTcTyVarToTyVar is applied to the *binding* occurrence
427 -- of a type variable, at the *end* of type checking. It changes
428 -- the *mutable* type variable into an *immutable* one.
430 -- It does this by making an immutable version of tv and binds tv to it.
431 -- Now any bound occurences of the original type variable will get
432 -- zonked to the immutable version.
434 zonkTcTyVarToTyVar :: TcTyVar -> NF_TcM TyVar
435 zonkTcTyVarToTyVar tv
437 -- Make an immutable version, defaulting
438 -- the kind to lifted if necessary
439 immut_tv = mkTyVar (tyVarName tv) (defaultKind (tyVarKind tv))
440 immut_tv_ty = mkTyVarTy immut_tv
442 zap tv = putTcTyVar tv immut_tv_ty
443 -- Bind the mutable version to the immutable one
445 -- If the type variable is mutable, then bind it to immut_tv_ty
446 -- so that all other occurrences of the tyvar will get zapped too
447 zonkTyVar zap tv `thenNF_Tc` \ ty2 ->
449 -- This warning shows up if the allegedly-unbound tyvar is
450 -- already bound to something. It can actually happen, and
451 -- in a harmless way (see [Silly Type Synonyms] below) so
452 -- it's only a warning
453 WARN( not (immut_tv_ty `tcEqType` ty2), ppr tv $$ ppr immut_tv $$ ppr ty2 )
458 [Silly Type Synonyms]
461 type C u a = u -- Note 'a' unused
463 foo :: (forall a. C u a -> C u a) -> u
467 bar = foo (\t -> t + t)
469 * From the (\t -> t+t) we get type {Num d} => d -> d
472 * Now unify with type of foo's arg, and we get:
473 {Num (C d a)} => C d a -> C d a
476 * Now abstract over the 'a', but float out the Num (C d a) constraint
477 because it does not 'really' mention a. (see Type.tyVarsOfType)
478 The arg to foo becomes
481 * So we get a dict binding for Num (C d a), which is zonked to give
484 * Then the /\a abstraction has a zonked 'a' in it.
486 All very silly. I think its harmless to ignore the problem.
489 %************************************************************************
491 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
493 %* For internal use only! *
495 %************************************************************************
498 -- zonkType is used for Kinds as well
500 -- For unbound, mutable tyvars, zonkType uses the function given to it
501 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
502 -- type variable and zonks the kind too
504 zonkType :: (TcTyVar -> NF_TcM Type) -- What to do with unbound mutable type variables
505 -- see zonkTcType, and zonkTcTypeToType
508 zonkType unbound_var_fn ty
511 go (TyConApp tycon tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' ->
512 returnNF_Tc (TyConApp tycon tys')
514 go (NoteTy (SynNote ty1) ty2) = go ty1 `thenNF_Tc` \ ty1' ->
515 go ty2 `thenNF_Tc` \ ty2' ->
516 returnNF_Tc (NoteTy (SynNote ty1') ty2')
518 go (NoteTy (FTVNote _) ty2) = go ty2 -- Discard free-tyvar annotations
520 go (SourceTy p) = go_pred p `thenNF_Tc` \ p' ->
521 returnNF_Tc (SourceTy p')
523 go (FunTy arg res) = go arg `thenNF_Tc` \ arg' ->
524 go res `thenNF_Tc` \ res' ->
525 returnNF_Tc (FunTy arg' res')
527 go (AppTy fun arg) = go fun `thenNF_Tc` \ fun' ->
528 go arg `thenNF_Tc` \ arg' ->
529 returnNF_Tc (mkAppTy fun' arg')
530 -- NB the mkAppTy; we might have instantiated a
531 -- type variable to a type constructor, so we need
532 -- to pull the TyConApp to the top.
534 -- The two interesting cases!
535 go (TyVarTy tyvar) = zonkTyVar unbound_var_fn tyvar
537 go (ForAllTy tyvar ty) = zonkTcTyVarToTyVar tyvar `thenNF_Tc` \ tyvar' ->
538 go ty `thenNF_Tc` \ ty' ->
539 returnNF_Tc (ForAllTy tyvar' ty')
541 go_pred (ClassP c tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' ->
542 returnNF_Tc (ClassP c tys')
543 go_pred (NType tc tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' ->
544 returnNF_Tc (NType tc tys')
545 go_pred (IParam n ty) = go ty `thenNF_Tc` \ ty' ->
546 returnNF_Tc (IParam n ty')
548 zonkTyVar :: (TcTyVar -> NF_TcM Type) -- What to do for an unbound mutable variable
549 -> TcTyVar -> NF_TcM TcType
550 zonkTyVar unbound_var_fn tyvar
551 | not (isMutTyVar tyvar) -- Not a mutable tyvar. This can happen when
552 -- zonking a forall type, when the bound type variable
553 -- needn't be mutable
554 = ASSERT( isTyVar tyvar ) -- Should not be any immutable kind vars
555 returnNF_Tc (TyVarTy tyvar)
558 = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
560 Nothing -> unbound_var_fn tyvar -- Mutable and unbound
561 Just other_ty -> zonkType unbound_var_fn other_ty -- Bound
566 %************************************************************************
568 \subsection{Checking a user type}
570 %************************************************************************
572 When dealing with a user-written type, we first translate it from an HsType
573 to a Type, performing kind checking, and then check various things that should
574 be true about it. We don't want to perform these checks at the same time
575 as the initial translation because (a) they are unnecessary for interface-file
576 types and (b) when checking a mutually recursive group of type and class decls,
577 we can't "look" at the tycons/classes yet. Also, the checks are are rather
578 diverse, and used to really mess up the other code.
580 One thing we check for is 'rank'.
582 Rank 0: monotypes (no foralls)
583 Rank 1: foralls at the front only, Rank 0 inside
584 Rank 2: foralls at the front, Rank 1 on left of fn arrow,
586 basic ::= tyvar | T basic ... basic
588 r2 ::= forall tvs. cxt => r2a
589 r2a ::= r1 -> r2a | basic
590 r1 ::= forall tvs. cxt => r0
591 r0 ::= r0 -> r0 | basic
593 Another thing is to check that type synonyms are saturated.
594 This might not necessarily show up in kind checking.
596 data T k = MkT (k Int)
602 = FunSigCtxt Name -- Function type signature
603 | ExprSigCtxt -- Expression type signature
604 | ConArgCtxt Name -- Data constructor argument
605 | TySynCtxt Name -- RHS of a type synonym decl
606 | GenPatCtxt -- Pattern in generic decl
607 -- f{| a+b |} (Inl x) = ...
608 | PatSigCtxt -- Type sig in pattern
610 | ResSigCtxt -- Result type sig
612 | ForSigCtxt Name -- Foreign inport or export signature
613 | RuleSigCtxt Name -- Signature on a forall'd variable in a RULE
615 -- Notes re TySynCtxt
616 -- We allow type synonyms that aren't types; e.g. type List = []
618 -- If the RHS mentions tyvars that aren't in scope, we'll
619 -- quantify over them:
620 -- e.g. type T = a->a
621 -- will become type T = forall a. a->a
623 -- With gla-exts that's right, but for H98 we should complain.
626 pprUserTypeCtxt (FunSigCtxt n) = ptext SLIT("the type signature for") <+> quotes (ppr n)
627 pprUserTypeCtxt ExprSigCtxt = ptext SLIT("an expression type signature")
628 pprUserTypeCtxt (ConArgCtxt c) = ptext SLIT("the type of constructor") <+> quotes (ppr c)
629 pprUserTypeCtxt (TySynCtxt c) = ptext SLIT("the RHS of a type synonym declaration") <+> quotes (ppr c)
630 pprUserTypeCtxt GenPatCtxt = ptext SLIT("the type pattern of a generic definition")
631 pprUserTypeCtxt PatSigCtxt = ptext SLIT("a pattern type signature")
632 pprUserTypeCtxt ResSigCtxt = ptext SLIT("a result type signature")
633 pprUserTypeCtxt (ForSigCtxt n) = ptext SLIT("the foreign signature for") <+> quotes (ppr n)
634 pprUserTypeCtxt (RuleSigCtxt n) = ptext SLIT("the type signature on") <+> quotes (ppr n)
638 checkValidType :: UserTypeCtxt -> Type -> TcM ()
639 -- Checks that the type is valid for the given context
640 checkValidType ctxt ty
641 = doptsTc Opt_GlasgowExts `thenNF_Tc` \ gla_exts ->
643 rank | gla_exts = Arbitrary
645 = case ctxt of -- Haskell 98
649 TySynCtxt _ -> Rank 0
650 ExprSigCtxt -> Rank 1
651 FunSigCtxt _ -> Rank 1
652 ConArgCtxt _ -> Rank 1 -- We are given the type of the entire
653 -- constructor, hence rank 1
654 ForSigCtxt _ -> Rank 1
655 RuleSigCtxt _ -> Rank 1
657 actual_kind = typeKind ty
659 actual_kind_is_lifted = actual_kind `eqKind` liftedTypeKind
661 kind_ok = case ctxt of
662 TySynCtxt _ -> True -- Any kind will do
663 GenPatCtxt -> actual_kind_is_lifted
664 ForSigCtxt _ -> actual_kind_is_lifted
665 other -> isTypeKind actual_kind
667 ubx_tup | not gla_exts = UT_NotOk
668 | otherwise = case ctxt of
671 -- Unboxed tuples ok in function results,
672 -- but for type synonyms we allow them even at
675 tcAddErrCtxt (checkTypeCtxt ctxt ty) $
677 -- Check that the thing has kind Type, and is lifted if necessary
678 checkTc kind_ok (kindErr actual_kind) `thenTc_`
680 -- Check the internal validity of the type itself
681 check_poly_type rank ubx_tup ty
684 checkTypeCtxt ctxt ty
685 = vcat [ptext SLIT("In the type:") <+> ppr_ty ty,
686 ptext SLIT("While checking") <+> pprUserTypeCtxt ctxt ]
688 -- Hack alert. If there are no tyvars, (ppr sigma_ty) will print
689 -- something strange like {Eq k} -> k -> k, because there is no
690 -- ForAll at the top of the type. Since this is going to the user
691 -- we want it to look like a proper Haskell type even then; hence the hack
693 -- This shows up in the complaint about
695 -- op :: Eq a => a -> a
696 ppr_ty ty | null forall_tvs && notNull theta = pprTheta theta <+> ptext SLIT("=>") <+> ppr tau
699 (forall_tvs, theta, tau) = tcSplitSigmaTy ty
704 data Rank = Rank Int | Arbitrary
706 decRank :: Rank -> Rank
707 decRank Arbitrary = Arbitrary
708 decRank (Rank n) = Rank (n-1)
710 ----------------------------------------
711 data UbxTupFlag = UT_Ok | UT_NotOk
712 -- The "Ok" version means "ok if -fglasgow-exts is on"
714 ----------------------------------------
715 check_poly_type :: Rank -> UbxTupFlag -> Type -> TcM ()
716 check_poly_type (Rank 0) ubx_tup ty
717 = check_tau_type (Rank 0) ubx_tup ty
719 check_poly_type rank ubx_tup ty
721 (tvs, theta, tau) = tcSplitSigmaTy ty
723 check_valid_theta SigmaCtxt theta `thenTc_`
724 check_tau_type (decRank rank) ubx_tup tau `thenTc_`
725 checkFreeness tvs theta `thenTc_`
726 checkAmbiguity tvs theta (tyVarsOfType tau)
728 ----------------------------------------
729 check_arg_type :: Type -> TcM ()
730 -- The sort of type that can instantiate a type variable,
731 -- or be the argument of a type constructor.
732 -- Not an unboxed tuple, not a forall.
733 -- Other unboxed types are very occasionally allowed as type
734 -- arguments depending on the kind of the type constructor
736 -- For example, we want to reject things like:
738 -- instance Ord a => Ord (forall s. T s a)
740 -- g :: T s (forall b.b)
742 -- NB: unboxed tuples can have polymorphic or unboxed args.
743 -- This happens in the workers for functions returning
744 -- product types with polymorphic components.
745 -- But not in user code.
746 -- Anyway, they are dealt with by a special case in check_tau_type
749 = check_tau_type (Rank 0) UT_NotOk ty `thenTc_`
750 checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
752 ----------------------------------------
753 check_tau_type :: Rank -> UbxTupFlag -> Type -> TcM ()
754 -- Rank is allowed rank for function args
755 -- No foralls otherwise
757 check_tau_type rank ubx_tup ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty)
758 check_tau_type rank ubx_tup (SourceTy sty) = getDOptsTc `thenNF_Tc` \ dflags ->
759 check_source_ty dflags TypeCtxt sty
760 check_tau_type rank ubx_tup (TyVarTy _) = returnTc ()
761 check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
762 = check_poly_type rank UT_NotOk arg_ty `thenTc_`
763 check_tau_type rank UT_Ok res_ty
765 check_tau_type rank ubx_tup (AppTy ty1 ty2)
766 = check_arg_type ty1 `thenTc_` check_arg_type ty2
768 check_tau_type rank ubx_tup (NoteTy (SynNote syn) ty)
769 -- Synonym notes are built only when the synonym is
770 -- saturated (see Type.mkSynTy)
771 = doptsTc Opt_GlasgowExts `thenNF_Tc` \ gla_exts ->
773 -- If -fglasgow-exts then don't check the 'note' part.
774 -- This allows us to instantiate a synonym defn with a
775 -- for-all type, or with a partially-applied type synonym.
776 -- e.g. type T a b = a
779 -- Here, T is partially applied, so it's illegal in H98.
780 -- But if you expand S first, then T we get just
785 -- For H98, do check the un-expanded part
786 check_tau_type rank ubx_tup syn
789 check_tau_type rank ubx_tup ty
791 check_tau_type rank ubx_tup (NoteTy other_note ty)
792 = check_tau_type rank ubx_tup ty
794 check_tau_type rank ubx_tup ty@(TyConApp tc tys)
796 = -- NB: Type.mkSynTy builds a TyConApp (not a NoteTy) for an unsaturated
797 -- synonym application, leaving it to checkValidType (i.e. right here)
799 checkTc syn_arity_ok arity_msg `thenTc_`
800 mapTc_ check_arg_type tys
802 | isUnboxedTupleTyCon tc
803 = doptsTc Opt_GlasgowExts `thenNF_Tc` \ gla_exts ->
804 checkTc (ubx_tup_ok gla_exts) ubx_tup_msg `thenTc_`
805 mapTc_ (check_tau_type (Rank 0) UT_Ok) tys
806 -- Args are allowed to be unlifted, or
807 -- more unboxed tuples, so can't use check_arg_ty
810 = mapTc_ check_arg_type tys
813 ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False }
815 syn_arity_ok = tc_arity <= n_args
816 -- It's OK to have an *over-applied* type synonym
817 -- data Tree a b = ...
818 -- type Foo a = Tree [a]
819 -- f :: Foo a b -> ...
821 tc_arity = tyConArity tc
823 arity_msg = arityErr "Type synonym" (tyConName tc) tc_arity n_args
824 ubx_tup_msg = ubxArgTyErr ty
826 ----------------------------------------
827 forAllTyErr ty = ptext SLIT("Illegal polymorphic type:") <+> ppr_ty ty
828 unliftedArgErr ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr_ty ty
829 ubxArgTyErr ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr_ty ty
830 kindErr kind = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
836 is ambiguous if P contains generic variables
837 (i.e. one of the Vs) that are not mentioned in tau
839 However, we need to take account of functional dependencies
840 when we speak of 'mentioned in tau'. Example:
841 class C a b | a -> b where ...
843 forall x y. (C x y) => x
844 is not ambiguous because x is mentioned and x determines y
846 NB; the ambiguity check is only used for *user* types, not for types
847 coming from inteface files. The latter can legitimately have
848 ambiguous types. Example
850 class S a where s :: a -> (Int,Int)
851 instance S Char where s _ = (1,1)
852 f:: S a => [a] -> Int -> (Int,Int)
853 f (_::[a]) x = (a*x,b)
854 where (a,b) = s (undefined::a)
856 Here the worker for f gets the type
857 fw :: forall a. S a => Int -> (# Int, Int #)
859 If the list of tv_names is empty, we have a monotype, and then we
860 don't need to check for ambiguity either, because the test can't fail
864 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
865 checkAmbiguity forall_tyvars theta tau_tyvars
866 = mapTc_ complain (filter is_ambig theta)
868 complain pred = addErrTc (ambigErr pred)
869 extended_tau_vars = grow theta tau_tyvars
870 is_ambig pred = any ambig_var (varSetElems (tyVarsOfPred pred))
872 ambig_var ct_var = (ct_var `elem` forall_tyvars) &&
873 not (ct_var `elemVarSet` extended_tau_vars)
875 is_free ct_var = not (ct_var `elem` forall_tyvars)
878 = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
879 nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
880 ptext SLIT("must be reachable from the type after the '=>'"))]
883 In addition, GHC insists that at least one type variable
884 in each constraint is in V. So we disallow a type like
885 forall a. Eq b => b -> b
886 even in a scope where b is in scope.
889 checkFreeness forall_tyvars theta
890 = mapTc_ complain (filter is_free theta)
892 is_free pred = not (isIPPred pred)
893 && not (any bound_var (varSetElems (tyVarsOfPred pred)))
894 bound_var ct_var = ct_var `elem` forall_tyvars
895 complain pred = addErrTc (freeErr pred)
898 = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
899 ptext SLIT("are already in scope"),
900 nest 4 (ptext SLIT("(at least one must be universally quantified here)"))
905 %************************************************************************
907 \subsection{Checking a theta or source type}
909 %************************************************************************
913 = ClassSCCtxt Name -- Superclasses of clas
914 | SigmaCtxt -- Context of a normal for-all type
915 | DataTyCtxt Name -- Context of a data decl
916 | TypeCtxt -- Source type in an ordinary type
917 | InstThetaCtxt -- Context of an instance decl
918 | InstHeadCtxt -- Head of an instance decl
920 pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
921 pprSourceTyCtxt SigmaCtxt = ptext SLIT("the context of a polymorphic type")
922 pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
923 pprSourceTyCtxt InstThetaCtxt = ptext SLIT("the context of an instance declaration")
924 pprSourceTyCtxt InstHeadCtxt = ptext SLIT("the head of an instance declaration")
925 pprSourceTyCtxt TypeCtxt = ptext SLIT("the context of a type")
929 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
930 checkValidTheta ctxt theta
931 = tcAddErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
933 -------------------------
934 check_valid_theta ctxt []
936 check_valid_theta ctxt theta
937 = getDOptsTc `thenNF_Tc` \ dflags ->
938 warnTc (notNull dups) (dupPredWarn dups) `thenNF_Tc_`
939 mapTc_ (check_source_ty dflags ctxt) theta
941 (_,dups) = removeDups tcCmpPred theta
943 -------------------------
944 check_source_ty dflags ctxt pred@(ClassP cls tys)
945 = -- Class predicates are valid in all contexts
946 mapTc_ check_arg_type tys `thenTc_`
947 checkTc (arity == n_tys) arity_err `thenTc_`
948 checkTc (check_class_pred_tys dflags ctxt tys)
949 (predTyVarErr pred $$ how_to_allow)
952 class_name = className cls
953 arity = classArity cls
955 arity_err = arityErr "Class" class_name arity n_tys
957 how_to_allow = case ctxt of
958 InstHeadCtxt -> empty -- Should not happen
959 InstThetaCtxt -> parens undecidableMsg
960 other -> parens (ptext SLIT("Use -fglasgow-exts to permit this"))
962 check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
963 -- Implicit parameters only allows in type
964 -- signatures; not in instance decls, superclasses etc
965 -- The reason for not allowing implicit params in instances is a bit subtle
966 -- If we allowed instance (?x::Int, Eq a) => Foo [a] where ...
967 -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
968 -- discharge all the potential usas of the ?x in e. For example, a
969 -- constraint Foo [Int] might come out of e,and applying the
970 -- instance decl would show up two uses of ?x.
972 check_source_ty dflags TypeCtxt (NType tc tys) = mapTc_ check_arg_type tys
975 check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
977 -------------------------
978 check_class_pred_tys dflags ctxt tys
980 InstHeadCtxt -> True -- We check for instance-head
981 -- formation in checkValidInstHead
982 InstThetaCtxt -> undecidable_ok || all isTyVarTy tys
983 other -> gla_exts || all tyvar_head tys
985 undecidable_ok = dopt Opt_AllowUndecidableInstances dflags
986 gla_exts = dopt Opt_GlasgowExts dflags
988 -------------------------
989 tyvar_head ty -- Haskell 98 allows predicates of form
990 | tcIsTyVarTy ty = True -- C (a ty1 .. tyn)
991 | otherwise -- where a is a type variable
992 = case tcSplitAppTy_maybe ty of
993 Just (ty, _) -> tyvar_head ty
998 badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprSourceType sty
999 predTyVarErr pred = ptext SLIT("Non-type variables in constraint:") <+> pprPred pred
1000 dupPredWarn dups = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
1002 checkThetaCtxt ctxt theta
1003 = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
1004 ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
1008 %************************************************************************
1010 \subsection{Validity check for TyCons}
1012 %************************************************************************
1014 checkValidTyCon is called once the mutually-recursive knot has been
1015 tied, so we can look at things freely.
1018 checkValidTyCon :: TyCon -> TcM ()
1020 | isSynTyCon tc = checkValidType (TySynCtxt name) syn_rhs
1022 = -- Check the context on the data decl
1023 checkValidTheta (DataTyCtxt name) (tyConTheta tc) `thenTc_`
1025 -- Check arg types of data constructors
1026 mapTc_ checkValidDataCon data_cons `thenTc_`
1028 -- Check that fields with the same name share a type
1029 mapTc_ check_fields groups
1033 (_, syn_rhs) = getSynTyConDefn tc
1034 data_cons = tyConDataCons tc
1036 fields = [field | con <- data_cons, field <- dataConFieldLabels con]
1037 groups = equivClasses cmp_name fields
1038 cmp_name field1 field2 = fieldLabelName field1 `compare` fieldLabelName field2
1040 check_fields fields@(first_field_label : other_fields)
1041 -- These fields all have the same name, but are from
1042 -- different constructors in the data type
1043 = -- Check that all the fields in the group have the same type
1044 -- NB: this check assumes that all the constructors of a given
1045 -- data type use the same type variables
1046 checkTc (all (tcEqType field_ty) other_tys) (fieldTypeMisMatch field_name)
1048 field_ty = fieldLabelType first_field_label
1049 field_name = fieldLabelName first_field_label
1050 other_tys = map fieldLabelType other_fields
1052 checkValidDataCon :: DataCon -> TcM ()
1053 checkValidDataCon con
1054 = checkValidType ctxt (idType (dataConWrapId con)) `thenTc_`
1055 -- This checks the argument types and
1056 -- ambiguity of the existential context (if any)
1057 tcAddErrCtxt (existentialCtxt con)
1058 (checkFreeness ex_tvs ex_theta)
1060 ctxt = ConArgCtxt (dataConName con)
1061 (_, _, ex_tvs, ex_theta, _, _) = dataConSig con
1064 fieldTypeMisMatch field_name
1065 = sep [ptext SLIT("Different constructors give different types for field"), quotes (ppr field_name)]
1067 existentialCtxt con = ptext SLIT("When checking the existential context of constructor")
1068 <+> quotes (ppr con)
1072 checkValidClass is called once the mutually-recursive knot has been
1073 tied, so we can look at things freely.
1076 checkValidClass :: Class -> TcM ()
1078 = -- CHECK ARITY 1 FOR HASKELL 1.4
1079 doptsTc Opt_GlasgowExts `thenTc` \ gla_exts ->
1081 -- Check that the class is unary, unless GlaExs
1082 checkTc (notNull tyvars) (nullaryClassErr cls) `thenTc_`
1083 checkTc (gla_exts || unary) (classArityErr cls) `thenTc_`
1085 -- Check the super-classes
1086 checkValidTheta (ClassSCCtxt (className cls)) theta `thenTc_`
1088 -- Check the class operations
1089 mapTc_ check_op op_stuff `thenTc_`
1091 -- Check that if the class has generic methods, then the
1092 -- class has only one parameter. We can't do generic
1093 -- multi-parameter type classes!
1094 checkTc (unary || no_generics) (genericMultiParamErr cls)
1097 (tyvars, theta, _, op_stuff) = classBigSig cls
1098 unary = isSingleton tyvars
1099 no_generics = null [() | (_, GenDefMeth) <- op_stuff]
1101 check_op (sel_id, dm)
1102 = checkValidTheta SigmaCtxt (tail theta) `thenTc_`
1103 -- The 'tail' removes the initial (C a) from the
1104 -- class itself, leaving just the method type
1106 checkValidType (FunSigCtxt op_name) tau `thenTc_`
1108 -- Check that for a generic method, the type of
1109 -- the method is sufficiently simple
1110 checkTc (dm /= GenDefMeth || validGenericMethodType op_ty)
1111 (badGenericMethodType op_name op_ty)
1113 op_name = idName sel_id
1114 op_ty = idType sel_id
1115 (_,theta,tau) = tcSplitSigmaTy op_ty
1118 = ptext SLIT("No parameters for class") <+> quotes (ppr cls)
1121 = vcat [ptext SLIT("Too many parameters for class") <+> quotes (ppr cls),
1122 parens (ptext SLIT("Use -fglasgow-exts to allow multi-parameter classes"))]
1124 genericMultiParamErr clas
1125 = ptext SLIT("The multi-parameter class") <+> quotes (ppr clas) <+>
1126 ptext SLIT("cannot have generic methods")
1128 badGenericMethodType op op_ty
1129 = hang (ptext SLIT("Generic method type is too complex"))
1130 4 (vcat [ppr op <+> dcolon <+> ppr op_ty,
1131 ptext SLIT("You can only use type variables, arrows, and tuples")])
1135 %************************************************************************
1137 \subsection{Checking for a decent instance head type}
1139 %************************************************************************
1141 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1142 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1144 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1145 flag is on, or (2)~the instance is imported (they must have been
1146 compiled elsewhere). In these cases, we let them go through anyway.
1148 We can also have instances for functions: @instance Foo (a -> b) ...@.
1151 checkValidInstHead :: Type -> TcM (Class, [TcType])
1153 checkValidInstHead ty -- Should be a source type
1154 = case tcSplitPredTy_maybe ty of {
1155 Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
1158 case getClassPredTys_maybe pred of {
1159 Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
1162 getDOptsTc `thenNF_Tc` \ dflags ->
1163 mapTc_ check_arg_type tys `thenTc_`
1164 check_inst_head dflags clas tys `thenTc_`
1165 returnTc (clas, tys)
1168 check_inst_head dflags clas tys
1170 -- A user declaration of a CCallable/CReturnable instance
1171 -- must be for a "boxed primitive" type.
1172 (clas `hasKey` cCallableClassKey
1173 && not (ccallable_type first_ty))
1174 || (clas `hasKey` cReturnableClassKey
1175 && not (creturnable_type first_ty))
1176 = failWithTc (nonBoxedPrimCCallErr clas first_ty)
1178 -- If GlasgowExts then check at least one isn't a type variable
1179 | dopt Opt_GlasgowExts dflags
1180 = check_tyvars dflags clas tys
1182 -- WITH HASKELL 1.4, MUST HAVE C (T a b c)
1184 Just (tycon, arg_tys) <- tcSplitTyConApp_maybe first_ty,
1185 not (isSynTyCon tycon), -- ...but not a synonym
1186 all tcIsTyVarTy arg_tys, -- Applied to type variables
1187 equalLength (varSetElems (tyVarsOfTypes arg_tys)) arg_tys
1188 -- This last condition checks that all the type variables are distinct
1192 = failWithTc (instTypeErr (pprClassPred clas tys) head_shape_msg)
1195 (first_ty : _) = tys
1197 ccallable_type ty = isFFIArgumentTy dflags PlayRisky ty
1198 creturnable_type ty = isFFIImportResultTy dflags ty
1200 head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
1201 text "where T is not a synonym, and a,b,c are distinct type variables")
1203 check_tyvars dflags clas tys
1204 -- Check that at least one isn't a type variable
1205 -- unless -fallow-undecideable-instances
1206 | dopt Opt_AllowUndecidableInstances dflags = returnTc ()
1207 | not (all tcIsTyVarTy tys) = returnTc ()
1208 | otherwise = failWithTc (instTypeErr (pprClassPred clas tys) msg)
1210 msg = parens (ptext SLIT("There must be at least one non-type-variable in the instance head")
1213 undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
1217 instTypeErr pp_ty msg
1218 = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,
1221 nonBoxedPrimCCallErr clas inst_ty
1222 = hang (ptext SLIT("Unacceptable instance type for ccall-ish class"))
1223 4 (pprClassPred clas [inst_ty])