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
14 newTyVar, newSigTyVar,
15 newTyVarTy, -- Kind -> TcM TcType
16 newTyVarTys, -- Int -> Kind -> TcM [TcType]
17 newKindVar, newKindVars, newOpenTypeKind,
18 putTcTyVar, getTcTyVar,
19 newMutTyVar, readMutTyVar, writeMutTyVar,
21 --------------------------------
23 tcInstTyVar, tcInstTyVars, tcInstType,
25 --------------------------------
26 -- Checking type validity
27 Rank, UserTypeCtxt(..), checkValidType, pprUserTypeCtxt,
28 SourceTyCtxt(..), checkValidTheta,
29 checkValidTyCon, checkValidClass,
30 checkValidInstHead, instTypeErr, checkAmbiguity,
33 --------------------------------
36 zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV,
37 zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
38 zonkTcPredType, zonkTcTyVarToTyVar, zonkKindEnv,
42 #include "HsVersions.h"
46 import TypeRep ( Type(..), SourceType(..), TyNote(..), -- Friend; can see representation
47 Kind, ThetaType, typeCon
49 import TcType ( TcType, TcThetaType, TcTauType, TcPredType,
50 TcTyVarSet, TcKind, TcTyVar, TyVarDetails(..),
51 tcEqType, tcCmpPred, isClassPred,
52 tcSplitPhiTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe,
53 tcSplitTyConApp_maybe, tcSplitForAllTys,
54 tcIsTyVarTy, tcSplitSigmaTy, mkTyConApp,
55 isUnLiftedType, isIPPred, isTyVarTy,
57 mkAppTy, mkTyVarTy, mkTyVarTys,
58 tyVarsOfPred, getClassPredTys_maybe,
60 liftedTypeKind, openTypeKind, defaultKind, superKind,
61 superBoxity, liftedBoxity, typeKind,
62 tyVarsOfType, tyVarsOfTypes,
64 isFFIArgumentTy, isFFIImportResultTy
66 import Subst ( Subst, mkTopTyVarSubst, substTy )
67 import Class ( Class, DefMeth(..), classArity, className, classBigSig )
68 import TyCon ( TyCon, isSynTyCon, isUnboxedTupleTyCon,
69 tyConArity, tyConName, tyConTheta,
70 getSynTyConDefn, tyConDataCons )
71 import DataCon ( DataCon, dataConWrapId, dataConName, dataConSig, dataConFieldLabels )
72 import FieldLabel ( fieldLabelName, fieldLabelType )
73 import Var ( TyVar, idType, idName, tyVarKind, tyVarName, isTyVar,
74 mkTyVar, mkMutTyVar, isMutTyVar, mutTyVarRef )
77 import Generics ( validGenericMethodType )
78 import TcRnMonad -- TcType, amongst others
79 import PrelNames ( cCallableClassKey, cReturnableClassKey, hasKey )
80 import ForeignCall ( Safety(..) )
81 import FunDeps ( grow )
82 import PprType ( pprPred, pprSourceType, pprTheta, pprClassPred )
83 import Name ( Name, setNameUnique, mkSystemTvNameEncoded )
85 import CmdLineOpts ( dopt, DynFlag(..) )
86 import Util ( nOfThem, isSingleton, equalLength, notNull, lengthExceeds )
87 import ListSetOps ( equivClasses, removeDups )
92 %************************************************************************
94 \subsection{New type variables}
96 %************************************************************************
99 newMutTyVar :: Name -> Kind -> TyVarDetails -> TcM TyVar
100 newMutTyVar name kind details
101 = do { ref <- newMutVar Nothing ;
102 return (mkMutTyVar name kind details ref) }
104 readMutTyVar :: TyVar -> TcM (Maybe Type)
105 readMutTyVar tyvar = readMutVar (mutTyVarRef tyvar)
107 writeMutTyVar :: TyVar -> Maybe Type -> TcM ()
108 writeMutTyVar tyvar val = writeMutVar (mutTyVarRef tyvar) val
110 newTyVar :: Kind -> TcM TcTyVar
112 = newUnique `thenM` \ uniq ->
113 newMutTyVar (mkSystemTvNameEncoded uniq FSLIT("t")) kind VanillaTv
115 newSigTyVar :: Kind -> TcM TcTyVar
117 = newUnique `thenM` \ uniq ->
118 newMutTyVar (mkSystemTvNameEncoded uniq FSLIT("s")) kind SigTv
120 newTyVarTy :: Kind -> TcM TcType
122 = newTyVar kind `thenM` \ tc_tyvar ->
123 returnM (TyVarTy tc_tyvar)
125 newTyVarTys :: Int -> Kind -> TcM [TcType]
126 newTyVarTys n kind = mappM newTyVarTy (nOfThem n kind)
128 newKindVar :: TcM TcKind
130 = newUnique `thenM` \ uniq ->
131 newMutTyVar (mkSystemTvNameEncoded uniq FSLIT("k")) superKind VanillaTv `thenM` \ kv ->
134 newKindVars :: Int -> TcM [TcKind]
135 newKindVars n = mappM (\ _ -> newKindVar) (nOfThem n ())
137 newOpenTypeKind :: TcM TcKind -- Returns the kind (Type bx), where bx is fresh
139 = newUnique `thenM` \ uniq ->
140 newMutTyVar (mkSystemTvNameEncoded uniq FSLIT("bx")) superBoxity VanillaTv `thenM` \ kv ->
141 returnM (mkTyConApp typeCon [TyVarTy kv])
145 %************************************************************************
147 \subsection{Type instantiation}
149 %************************************************************************
151 Instantiating a bunch of type variables
154 tcInstTyVars :: TyVarDetails -> [TyVar]
155 -> TcM ([TcTyVar], [TcType], Subst)
157 tcInstTyVars tv_details tyvars
158 = mappM (tcInstTyVar tv_details) tyvars `thenM` \ tc_tyvars ->
160 tys = mkTyVarTys tc_tyvars
162 returnM (tc_tyvars, tys, mkTopTyVarSubst tyvars tys)
163 -- Since the tyvars are freshly made,
164 -- they cannot possibly be captured by
165 -- any existing for-alls. Hence mkTopTyVarSubst
167 tcInstTyVar tv_details tyvar
168 = newUnique `thenM` \ uniq ->
170 name = setNameUnique (tyVarName tyvar) uniq
171 -- Note that we don't change the print-name
172 -- This won't confuse the type checker but there's a chance
173 -- that two different tyvars will print the same way
174 -- in an error message. -dppr-debug will show up the difference
175 -- Better watch out for this. If worst comes to worst, just
178 newMutTyVar name (tyVarKind tyvar) tv_details
180 tcInstType :: TyVarDetails -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
181 -- tcInstType instantiates the outer-level for-alls of a TcType with
182 -- fresh (mutable) type variables, splits off the dictionary part,
183 -- and returns the pieces.
184 tcInstType tv_details ty
185 = case tcSplitForAllTys ty of
186 ([], rho) -> -- There may be overloading despite no type variables;
187 -- (?x :: Int) => Int -> Int
189 (theta, tau) = tcSplitPhiTy rho
191 returnM ([], theta, tau)
193 (tyvars, rho) -> tcInstTyVars tv_details tyvars `thenM` \ (tyvars', _, tenv) ->
195 (theta, tau) = tcSplitPhiTy (substTy tenv rho)
197 returnM (tyvars', theta, tau)
201 %************************************************************************
203 \subsection{Putting and getting mutable type variables}
205 %************************************************************************
208 putTcTyVar :: TcTyVar -> TcType -> TcM TcType
209 getTcTyVar :: TcTyVar -> TcM (Maybe TcType)
216 | not (isMutTyVar tyvar)
217 = pprTrace "putTcTyVar" (ppr tyvar) $
221 = ASSERT( isMutTyVar tyvar )
222 writeMutTyVar tyvar (Just ty) `thenM_`
226 Getting is more interesting. The easy thing to do is just to read, thus:
229 getTcTyVar tyvar = readMutTyVar tyvar
232 But it's more fun to short out indirections on the way: If this
233 version returns a TyVar, then that TyVar is unbound. If it returns
234 any other type, then there might be bound TyVars embedded inside it.
236 We return Nothing iff the original box was unbound.
240 | not (isMutTyVar tyvar)
241 = pprTrace "getTcTyVar" (ppr tyvar) $
242 returnM (Just (mkTyVarTy tyvar))
245 = ASSERT2( isMutTyVar tyvar, ppr tyvar )
246 readMutTyVar tyvar `thenM` \ maybe_ty ->
248 Just ty -> short_out ty `thenM` \ ty' ->
249 writeMutTyVar tyvar (Just ty') `thenM_`
252 Nothing -> returnM Nothing
254 short_out :: TcType -> TcM TcType
255 short_out ty@(TyVarTy tyvar)
256 | not (isMutTyVar tyvar)
260 = readMutTyVar tyvar `thenM` \ maybe_ty ->
262 Just ty' -> short_out ty' `thenM` \ ty' ->
263 writeMutTyVar tyvar (Just ty') `thenM_`
268 short_out other_ty = returnM other_ty
272 %************************************************************************
274 \subsection{Zonking -- the exernal interfaces}
276 %************************************************************************
278 ----------------- Type variables
281 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
282 zonkTcTyVars tyvars = mappM zonkTcTyVar tyvars
284 zonkTcTyVarsAndFV :: [TcTyVar] -> TcM TcTyVarSet
285 zonkTcTyVarsAndFV tyvars = mappM zonkTcTyVar tyvars `thenM` \ tys ->
286 returnM (tyVarsOfTypes tys)
288 zonkTcTyVar :: TcTyVar -> TcM TcType
289 zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnM (TyVarTy tv)) tyvar
292 ----------------- Types
295 zonkTcType :: TcType -> TcM TcType
296 zonkTcType ty = zonkType (\ tv -> returnM (TyVarTy tv)) ty
298 zonkTcTypes :: [TcType] -> TcM [TcType]
299 zonkTcTypes tys = mappM zonkTcType tys
301 zonkTcClassConstraints cts = mappM zonk cts
302 where zonk (clas, tys)
303 = zonkTcTypes tys `thenM` \ new_tys ->
304 returnM (clas, new_tys)
306 zonkTcThetaType :: TcThetaType -> TcM TcThetaType
307 zonkTcThetaType theta = mappM zonkTcPredType theta
309 zonkTcPredType :: TcPredType -> TcM TcPredType
310 zonkTcPredType (ClassP c ts)
311 = zonkTcTypes ts `thenM` \ new_ts ->
312 returnM (ClassP c new_ts)
313 zonkTcPredType (IParam n t)
314 = zonkTcType t `thenM` \ new_t ->
315 returnM (IParam n new_t)
318 ------------------- These ...ToType, ...ToKind versions
319 are used at the end of type checking
322 zonkKindEnv :: [(Name, TcKind)] -> TcM [(Name, Kind)]
324 = mappM zonk_it pairs
326 zonk_it (name, tc_kind) = zonkType zonk_unbound_kind_var tc_kind `thenM` \ kind ->
329 -- When zonking a kind, we want to
330 -- zonk a *kind* variable to (Type *)
331 -- zonk a *boxity* variable to *
332 zonk_unbound_kind_var kv | tyVarKind kv `eqKind` superKind = putTcTyVar kv liftedTypeKind
333 | tyVarKind kv `eqKind` superBoxity = putTcTyVar kv liftedBoxity
334 | otherwise = pprPanic "zonkKindEnv" (ppr kv)
336 -- zonkTcTyVarToTyVar is applied to the *binding* occurrence
337 -- of a type variable, at the *end* of type checking. It changes
338 -- the *mutable* type variable into an *immutable* one.
340 -- It does this by making an immutable version of tv and binds tv to it.
341 -- Now any bound occurences of the original type variable will get
342 -- zonked to the immutable version.
344 zonkTcTyVarToTyVar :: TcTyVar -> TcM TyVar
345 zonkTcTyVarToTyVar tv
347 -- Make an immutable version, defaulting
348 -- the kind to lifted if necessary
349 immut_tv = mkTyVar (tyVarName tv) (defaultKind (tyVarKind tv))
350 immut_tv_ty = mkTyVarTy immut_tv
352 zap tv = putTcTyVar tv immut_tv_ty
353 -- Bind the mutable version to the immutable one
355 -- If the type variable is mutable, then bind it to immut_tv_ty
356 -- so that all other occurrences of the tyvar will get zapped too
357 zonkTyVar zap tv `thenM` \ ty2 ->
359 -- This warning shows up if the allegedly-unbound tyvar is
360 -- already bound to something. It can actually happen, and
361 -- in a harmless way (see [Silly Type Synonyms] below) so
362 -- it's only a warning
363 WARN( not (immut_tv_ty `tcEqType` ty2), ppr tv $$ ppr immut_tv $$ ppr ty2 )
368 [Silly Type Synonyms]
371 type C u a = u -- Note 'a' unused
373 foo :: (forall a. C u a -> C u a) -> u
377 bar = foo (\t -> t + t)
379 * From the (\t -> t+t) we get type {Num d} => d -> d
382 * Now unify with type of foo's arg, and we get:
383 {Num (C d a)} => C d a -> C d a
386 * Now abstract over the 'a', but float out the Num (C d a) constraint
387 because it does not 'really' mention a. (see Type.tyVarsOfType)
388 The arg to foo becomes
391 * So we get a dict binding for Num (C d a), which is zonked to give
394 * Then the /\a abstraction has a zonked 'a' in it.
396 All very silly. I think its harmless to ignore the problem.
399 %************************************************************************
401 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
403 %* For internal use only! *
405 %************************************************************************
408 -- zonkType is used for Kinds as well
410 -- For unbound, mutable tyvars, zonkType uses the function given to it
411 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
412 -- type variable and zonks the kind too
414 zonkType :: (TcTyVar -> TcM Type) -- What to do with unbound mutable type variables
415 -- see zonkTcType, and zonkTcTypeToType
418 zonkType unbound_var_fn ty
421 go (TyConApp tycon tys) = mappM go tys `thenM` \ tys' ->
422 returnM (TyConApp tycon tys')
424 go (NoteTy (SynNote ty1) ty2) = go ty1 `thenM` \ ty1' ->
425 go ty2 `thenM` \ ty2' ->
426 returnM (NoteTy (SynNote ty1') ty2')
428 go (NoteTy (FTVNote _) ty2) = go ty2 -- Discard free-tyvar annotations
430 go (SourceTy p) = go_pred p `thenM` \ p' ->
431 returnM (SourceTy p')
433 go (FunTy arg res) = go arg `thenM` \ arg' ->
434 go res `thenM` \ res' ->
435 returnM (FunTy arg' res')
437 go (AppTy fun arg) = go fun `thenM` \ fun' ->
438 go arg `thenM` \ arg' ->
439 returnM (mkAppTy fun' arg')
440 -- NB the mkAppTy; we might have instantiated a
441 -- type variable to a type constructor, so we need
442 -- to pull the TyConApp to the top.
444 -- The two interesting cases!
445 go (TyVarTy tyvar) = zonkTyVar unbound_var_fn tyvar
447 go (ForAllTy tyvar ty) = zonkTcTyVarToTyVar tyvar `thenM` \ tyvar' ->
448 go ty `thenM` \ ty' ->
449 returnM (ForAllTy tyvar' ty')
451 go_pred (ClassP c tys) = mappM go tys `thenM` \ tys' ->
452 returnM (ClassP c tys')
453 go_pred (NType tc tys) = mappM go tys `thenM` \ tys' ->
454 returnM (NType tc tys')
455 go_pred (IParam n ty) = go ty `thenM` \ ty' ->
456 returnM (IParam n ty')
458 zonkTyVar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable variable
459 -> TcTyVar -> TcM TcType
460 zonkTyVar unbound_var_fn tyvar
461 | not (isMutTyVar tyvar) -- Not a mutable tyvar. This can happen when
462 -- zonking a forall type, when the bound type variable
463 -- needn't be mutable
464 = ASSERT( isTyVar tyvar ) -- Should not be any immutable kind vars
465 returnM (TyVarTy tyvar)
468 = getTcTyVar tyvar `thenM` \ maybe_ty ->
470 Nothing -> unbound_var_fn tyvar -- Mutable and unbound
471 Just other_ty -> zonkType unbound_var_fn other_ty -- Bound
476 %************************************************************************
478 \subsection{Checking a user type}
480 %************************************************************************
482 When dealing with a user-written type, we first translate it from an HsType
483 to a Type, performing kind checking, and then check various things that should
484 be true about it. We don't want to perform these checks at the same time
485 as the initial translation because (a) they are unnecessary for interface-file
486 types and (b) when checking a mutually recursive group of type and class decls,
487 we can't "look" at the tycons/classes yet. Also, the checks are are rather
488 diverse, and used to really mess up the other code.
490 One thing we check for is 'rank'.
492 Rank 0: monotypes (no foralls)
493 Rank 1: foralls at the front only, Rank 0 inside
494 Rank 2: foralls at the front, Rank 1 on left of fn arrow,
496 basic ::= tyvar | T basic ... basic
498 r2 ::= forall tvs. cxt => r2a
499 r2a ::= r1 -> r2a | basic
500 r1 ::= forall tvs. cxt => r0
501 r0 ::= r0 -> r0 | basic
503 Another thing is to check that type synonyms are saturated.
504 This might not necessarily show up in kind checking.
506 data T k = MkT (k Int)
512 = FunSigCtxt Name -- Function type signature
513 | ExprSigCtxt -- Expression type signature
514 | ConArgCtxt Name -- Data constructor argument
515 | TySynCtxt Name -- RHS of a type synonym decl
516 | GenPatCtxt -- Pattern in generic decl
517 -- f{| a+b |} (Inl x) = ...
518 | PatSigCtxt -- Type sig in pattern
520 | ResSigCtxt -- Result type sig
522 | ForSigCtxt Name -- Foreign inport or export signature
523 | RuleSigCtxt Name -- Signature on a forall'd variable in a RULE
525 -- Notes re TySynCtxt
526 -- We allow type synonyms that aren't types; e.g. type List = []
528 -- If the RHS mentions tyvars that aren't in scope, we'll
529 -- quantify over them:
530 -- e.g. type T = a->a
531 -- will become type T = forall a. a->a
533 -- With gla-exts that's right, but for H98 we should complain.
536 pprUserTypeCtxt (FunSigCtxt n) = ptext SLIT("the type signature for") <+> quotes (ppr n)
537 pprUserTypeCtxt ExprSigCtxt = ptext SLIT("an expression type signature")
538 pprUserTypeCtxt (ConArgCtxt c) = ptext SLIT("the type of constructor") <+> quotes (ppr c)
539 pprUserTypeCtxt (TySynCtxt c) = ptext SLIT("the RHS of a type synonym declaration") <+> quotes (ppr c)
540 pprUserTypeCtxt GenPatCtxt = ptext SLIT("the type pattern of a generic definition")
541 pprUserTypeCtxt PatSigCtxt = ptext SLIT("a pattern type signature")
542 pprUserTypeCtxt ResSigCtxt = ptext SLIT("a result type signature")
543 pprUserTypeCtxt (ForSigCtxt n) = ptext SLIT("the foreign signature for") <+> quotes (ppr n)
544 pprUserTypeCtxt (RuleSigCtxt n) = ptext SLIT("the type signature on") <+> quotes (ppr n)
548 checkValidType :: UserTypeCtxt -> Type -> TcM ()
549 -- Checks that the type is valid for the given context
550 checkValidType ctxt ty
551 = doptM Opt_GlasgowExts `thenM` \ gla_exts ->
553 rank | gla_exts = Arbitrary
555 = case ctxt of -- Haskell 98
559 TySynCtxt _ -> Rank 0
560 ExprSigCtxt -> Rank 1
561 FunSigCtxt _ -> Rank 1
562 ConArgCtxt _ -> Rank 1 -- We are given the type of the entire
563 -- constructor, hence rank 1
564 ForSigCtxt _ -> Rank 1
565 RuleSigCtxt _ -> Rank 1
567 actual_kind = typeKind ty
569 actual_kind_is_lifted = actual_kind `eqKind` liftedTypeKind
571 kind_ok = case ctxt of
572 TySynCtxt _ -> True -- Any kind will do
573 GenPatCtxt -> actual_kind_is_lifted
574 ForSigCtxt _ -> actual_kind_is_lifted
575 other -> isTypeKind actual_kind
577 ubx_tup | not gla_exts = UT_NotOk
578 | otherwise = case ctxt of
581 -- Unboxed tuples ok in function results,
582 -- but for type synonyms we allow them even at
585 addErrCtxt (checkTypeCtxt ctxt ty) $
587 -- Check that the thing has kind Type, and is lifted if necessary
588 checkTc kind_ok (kindErr actual_kind) `thenM_`
590 -- Check the internal validity of the type itself
591 check_poly_type rank ubx_tup ty
594 checkTypeCtxt ctxt ty
595 = vcat [ptext SLIT("In the type:") <+> ppr_ty ty,
596 ptext SLIT("While checking") <+> pprUserTypeCtxt ctxt ]
598 -- Hack alert. If there are no tyvars, (ppr sigma_ty) will print
599 -- something strange like {Eq k} -> k -> k, because there is no
600 -- ForAll at the top of the type. Since this is going to the user
601 -- we want it to look like a proper Haskell type even then; hence the hack
603 -- This shows up in the complaint about
605 -- op :: Eq a => a -> a
606 ppr_ty ty | null forall_tvs && notNull theta = pprTheta theta <+> ptext SLIT("=>") <+> ppr tau
609 (forall_tvs, theta, tau) = tcSplitSigmaTy ty
614 data Rank = Rank Int | Arbitrary
616 decRank :: Rank -> Rank
617 decRank Arbitrary = Arbitrary
618 decRank (Rank n) = Rank (n-1)
620 ----------------------------------------
621 data UbxTupFlag = UT_Ok | UT_NotOk
622 -- The "Ok" version means "ok if -fglasgow-exts is on"
624 ----------------------------------------
625 check_poly_type :: Rank -> UbxTupFlag -> Type -> TcM ()
626 check_poly_type (Rank 0) ubx_tup ty
627 = check_tau_type (Rank 0) ubx_tup ty
629 check_poly_type rank ubx_tup ty
631 (tvs, theta, tau) = tcSplitSigmaTy ty
633 check_valid_theta SigmaCtxt theta `thenM_`
634 check_tau_type (decRank rank) ubx_tup tau `thenM_`
635 checkFreeness tvs theta `thenM_`
636 checkAmbiguity tvs theta (tyVarsOfType tau)
638 ----------------------------------------
639 check_arg_type :: Type -> TcM ()
640 -- The sort of type that can instantiate a type variable,
641 -- or be the argument of a type constructor.
642 -- Not an unboxed tuple, not a forall.
643 -- Other unboxed types are very occasionally allowed as type
644 -- arguments depending on the kind of the type constructor
646 -- For example, we want to reject things like:
648 -- instance Ord a => Ord (forall s. T s a)
650 -- g :: T s (forall b.b)
652 -- NB: unboxed tuples can have polymorphic or unboxed args.
653 -- This happens in the workers for functions returning
654 -- product types with polymorphic components.
655 -- But not in user code.
656 -- Anyway, they are dealt with by a special case in check_tau_type
659 = check_tau_type (Rank 0) UT_NotOk ty `thenM_`
660 checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
662 ----------------------------------------
663 check_tau_type :: Rank -> UbxTupFlag -> Type -> TcM ()
664 -- Rank is allowed rank for function args
665 -- No foralls otherwise
667 check_tau_type rank ubx_tup ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty)
668 check_tau_type rank ubx_tup (SourceTy sty) = getDOpts `thenM` \ dflags ->
669 check_source_ty dflags TypeCtxt sty
670 check_tau_type rank ubx_tup (TyVarTy _) = returnM ()
671 check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
672 = check_poly_type rank UT_NotOk arg_ty `thenM_`
673 check_tau_type rank UT_Ok res_ty
675 check_tau_type rank ubx_tup (AppTy ty1 ty2)
676 = check_arg_type ty1 `thenM_` check_arg_type ty2
678 check_tau_type rank ubx_tup (NoteTy (SynNote syn) ty)
679 -- Synonym notes are built only when the synonym is
680 -- saturated (see Type.mkSynTy)
681 = doptM Opt_GlasgowExts `thenM` \ gla_exts ->
683 -- If -fglasgow-exts then don't check the 'note' part.
684 -- This allows us to instantiate a synonym defn with a
685 -- for-all type, or with a partially-applied type synonym.
686 -- e.g. type T a b = a
689 -- Here, T is partially applied, so it's illegal in H98.
690 -- But if you expand S first, then T we get just
695 -- For H98, do check the un-expanded part
696 check_tau_type rank ubx_tup syn
699 check_tau_type rank ubx_tup ty
701 check_tau_type rank ubx_tup (NoteTy other_note ty)
702 = check_tau_type rank ubx_tup ty
704 check_tau_type rank ubx_tup ty@(TyConApp tc tys)
706 = -- NB: Type.mkSynTy builds a TyConApp (not a NoteTy) for an unsaturated
707 -- synonym application, leaving it to checkValidType (i.e. right here)
709 checkTc syn_arity_ok arity_msg `thenM_`
710 mappM_ check_arg_type tys
712 | isUnboxedTupleTyCon tc
713 = doptM Opt_GlasgowExts `thenM` \ gla_exts ->
714 checkTc (ubx_tup_ok gla_exts) ubx_tup_msg `thenM_`
715 mappM_ (check_tau_type (Rank 0) UT_Ok) tys
716 -- Args are allowed to be unlifted, or
717 -- more unboxed tuples, so can't use check_arg_ty
720 = mappM_ check_arg_type tys
723 ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False }
725 syn_arity_ok = tc_arity <= n_args
726 -- It's OK to have an *over-applied* type synonym
727 -- data Tree a b = ...
728 -- type Foo a = Tree [a]
729 -- f :: Foo a b -> ...
731 tc_arity = tyConArity tc
733 arity_msg = arityErr "Type synonym" (tyConName tc) tc_arity n_args
734 ubx_tup_msg = ubxArgTyErr ty
736 ----------------------------------------
737 forAllTyErr ty = ptext SLIT("Illegal polymorphic type:") <+> ppr_ty ty
738 unliftedArgErr ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr_ty ty
739 ubxArgTyErr ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr_ty ty
740 kindErr kind = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
745 %************************************************************************
747 \subsection{Checking a theta or source type}
749 %************************************************************************
752 -- Enumerate the contexts in which a "source type", <S>, can occur
756 -- or (N a) where N is a newtype
759 = ClassSCCtxt Name -- Superclasses of clas
760 -- class <S> => C a where ...
761 | SigmaCtxt -- Theta part of a normal for-all type
762 -- f :: <S> => a -> a
763 | DataTyCtxt Name -- Theta part of a data decl
764 -- data <S> => T a = MkT a
765 | TypeCtxt -- Source type in an ordinary type
767 | InstThetaCtxt -- Context of an instance decl
768 -- instance <S> => C [a] where ...
769 | InstHeadCtxt -- Head of an instance decl
770 -- instance ... => Eq a where ...
772 pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
773 pprSourceTyCtxt SigmaCtxt = ptext SLIT("the context of a polymorphic type")
774 pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
775 pprSourceTyCtxt InstThetaCtxt = ptext SLIT("the context of an instance declaration")
776 pprSourceTyCtxt InstHeadCtxt = ptext SLIT("the head of an instance declaration")
777 pprSourceTyCtxt TypeCtxt = ptext SLIT("the context of a type")
781 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
782 checkValidTheta ctxt theta
783 = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
785 -------------------------
786 check_valid_theta ctxt []
788 check_valid_theta ctxt theta
789 = getDOpts `thenM` \ dflags ->
790 warnTc (notNull dups) (dupPredWarn dups) `thenM_`
791 -- Actually, in instance decls and type signatures,
792 -- duplicate constraints are eliminated by TcMonoType.hoistForAllTys,
793 -- so this error can only fire for the context of a class or
795 mappM_ (check_source_ty dflags ctxt) theta
797 (_,dups) = removeDups tcCmpPred theta
799 -------------------------
800 check_source_ty dflags ctxt pred@(ClassP cls tys)
801 = -- Class predicates are valid in all contexts
802 mappM_ check_arg_type tys `thenM_`
803 checkTc (arity == n_tys) arity_err `thenM_`
804 checkTc (check_class_pred_tys dflags ctxt tys)
805 (predTyVarErr pred $$ how_to_allow)
808 class_name = className cls
809 arity = classArity cls
811 arity_err = arityErr "Class" class_name arity n_tys
813 how_to_allow = case ctxt of
814 InstHeadCtxt -> empty -- Should not happen
815 InstThetaCtxt -> parens undecidableMsg
816 other -> parens (ptext SLIT("Use -fglasgow-exts to permit this"))
818 check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
819 -- Implicit parameters only allows in type
820 -- signatures; not in instance decls, superclasses etc
821 -- The reason for not allowing implicit params in instances is a bit subtle
822 -- If we allowed instance (?x::Int, Eq a) => Foo [a] where ...
823 -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
824 -- discharge all the potential usas of the ?x in e. For example, a
825 -- constraint Foo [Int] might come out of e,and applying the
826 -- instance decl would show up two uses of ?x.
828 check_source_ty dflags TypeCtxt (NType tc tys) = mappM_ check_arg_type tys
831 check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
833 -------------------------
834 check_class_pred_tys dflags ctxt tys
836 InstHeadCtxt -> True -- We check for instance-head
837 -- formation in checkValidInstHead
838 InstThetaCtxt -> undecidable_ok || all isTyVarTy tys
839 other -> gla_exts || all tyvar_head tys
841 undecidable_ok = dopt Opt_AllowUndecidableInstances dflags
842 gla_exts = dopt Opt_GlasgowExts dflags
844 -------------------------
845 tyvar_head ty -- Haskell 98 allows predicates of form
846 | tcIsTyVarTy ty = True -- C (a ty1 .. tyn)
847 | otherwise -- where a is a type variable
848 = case tcSplitAppTy_maybe ty of
849 Just (ty, _) -> tyvar_head ty
856 is ambiguous if P contains generic variables
857 (i.e. one of the Vs) that are not mentioned in tau
859 However, we need to take account of functional dependencies
860 when we speak of 'mentioned in tau'. Example:
861 class C a b | a -> b where ...
863 forall x y. (C x y) => x
864 is not ambiguous because x is mentioned and x determines y
866 NB; the ambiguity check is only used for *user* types, not for types
867 coming from inteface files. The latter can legitimately have
868 ambiguous types. Example
870 class S a where s :: a -> (Int,Int)
871 instance S Char where s _ = (1,1)
872 f:: S a => [a] -> Int -> (Int,Int)
873 f (_::[a]) x = (a*x,b)
874 where (a,b) = s (undefined::a)
876 Here the worker for f gets the type
877 fw :: forall a. S a => Int -> (# Int, Int #)
879 If the list of tv_names is empty, we have a monotype, and then we
880 don't need to check for ambiguity either, because the test can't fail
884 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
885 checkAmbiguity forall_tyvars theta tau_tyvars
886 = mappM_ complain (filter is_ambig theta)
888 complain pred = addErrTc (ambigErr pred)
889 extended_tau_vars = grow theta tau_tyvars
891 -- Only a *class* predicate can give rise to ambiguity
892 -- An *implicit parameter* cannot. For example:
893 -- foo :: (?x :: [a]) => Int
895 -- is fine. The call site will suppply a particular 'x'
896 is_ambig pred = isClassPred pred &&
897 any ambig_var (varSetElems (tyVarsOfPred pred))
899 ambig_var ct_var = (ct_var `elem` forall_tyvars) &&
900 not (ct_var `elemVarSet` extended_tau_vars)
903 = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
904 nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
905 ptext SLIT("must be reachable from the type after the '=>'"))]
908 In addition, GHC insists that at least one type variable
909 in each constraint is in V. So we disallow a type like
910 forall a. Eq b => b -> b
911 even in a scope where b is in scope.
914 checkFreeness forall_tyvars theta
915 = mappM_ complain (filter is_free theta)
917 is_free pred = not (isIPPred pred)
918 && not (any bound_var (varSetElems (tyVarsOfPred pred)))
919 bound_var ct_var = ct_var `elem` forall_tyvars
920 complain pred = addErrTc (freeErr pred)
923 = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
924 ptext SLIT("are already in scope"),
925 nest 4 (ptext SLIT("(at least one must be universally quantified here)"))
930 checkThetaCtxt ctxt theta
931 = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
932 ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
934 badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprSourceType sty
935 predTyVarErr pred = ptext SLIT("Non-type variables in constraint:") <+> pprPred pred
936 dupPredWarn dups = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
938 arityErr kind name n m
939 = hsep [ text kind, quotes (ppr name), ptext SLIT("should have"),
940 n_arguments <> comma, text "but has been given", int m]
942 n_arguments | n == 0 = ptext SLIT("no arguments")
943 | n == 1 = ptext SLIT("1 argument")
944 | True = hsep [int n, ptext SLIT("arguments")]
948 %************************************************************************
950 \subsection{Validity check for TyCons}
952 %************************************************************************
954 checkValidTyCon is called once the mutually-recursive knot has been
955 tied, so we can look at things freely.
958 checkValidTyCon :: TyCon -> TcM ()
960 | isSynTyCon tc = checkValidType (TySynCtxt name) syn_rhs
962 = -- Check the context on the data decl
963 checkValidTheta (DataTyCtxt name) (tyConTheta tc) `thenM_`
965 -- Check arg types of data constructors
966 mappM_ checkValidDataCon data_cons `thenM_`
968 -- Check that fields with the same name share a type
969 mappM_ check_fields groups
973 (_, syn_rhs) = getSynTyConDefn tc
974 data_cons = tyConDataCons tc
976 fields = [field | con <- data_cons, field <- dataConFieldLabels con]
977 groups = equivClasses cmp_name fields
978 cmp_name field1 field2 = fieldLabelName field1 `compare` fieldLabelName field2
980 check_fields fields@(first_field_label : other_fields)
981 -- These fields all have the same name, but are from
982 -- different constructors in the data type
983 = -- Check that all the fields in the group have the same type
984 -- NB: this check assumes that all the constructors of a given
985 -- data type use the same type variables
986 checkTc (all (tcEqType field_ty) other_tys) (fieldTypeMisMatch field_name)
988 field_ty = fieldLabelType first_field_label
989 field_name = fieldLabelName first_field_label
990 other_tys = map fieldLabelType other_fields
992 checkValidDataCon :: DataCon -> TcM ()
993 checkValidDataCon con
994 = checkValidType ctxt (idType (dataConWrapId con)) `thenM_`
995 -- This checks the argument types and
996 -- ambiguity of the existential context (if any)
997 addErrCtxt (existentialCtxt con)
998 (checkFreeness ex_tvs ex_theta)
1000 ctxt = ConArgCtxt (dataConName con)
1001 (_, _, ex_tvs, ex_theta, _, _) = dataConSig con
1004 fieldTypeMisMatch field_name
1005 = sep [ptext SLIT("Different constructors give different types for field"), quotes (ppr field_name)]
1007 existentialCtxt con = ptext SLIT("When checking the existential context of constructor")
1008 <+> quotes (ppr con)
1012 checkValidClass is called once the mutually-recursive knot has been
1013 tied, so we can look at things freely.
1016 checkValidClass :: Class -> TcM ()
1018 = -- CHECK ARITY 1 FOR HASKELL 1.4
1019 doptM Opt_GlasgowExts `thenM` \ gla_exts ->
1021 -- Check that the class is unary, unless GlaExs
1022 checkTc (notNull tyvars) (nullaryClassErr cls) `thenM_`
1023 checkTc (gla_exts || unary) (classArityErr cls) `thenM_`
1025 -- Check the super-classes
1026 checkValidTheta (ClassSCCtxt (className cls)) theta `thenM_`
1028 -- Check the class operations
1029 mappM_ check_op op_stuff `thenM_`
1031 -- Check that if the class has generic methods, then the
1032 -- class has only one parameter. We can't do generic
1033 -- multi-parameter type classes!
1034 checkTc (unary || no_generics) (genericMultiParamErr cls)
1037 (tyvars, theta, _, op_stuff) = classBigSig cls
1038 unary = isSingleton tyvars
1039 no_generics = null [() | (_, GenDefMeth) <- op_stuff]
1041 check_op (sel_id, dm)
1042 = checkValidTheta SigmaCtxt (tail theta) `thenM_`
1043 -- The 'tail' removes the initial (C a) from the
1044 -- class itself, leaving just the method type
1046 checkValidType (FunSigCtxt op_name) tau `thenM_`
1048 -- Check that for a generic method, the type of
1049 -- the method is sufficiently simple
1050 checkTc (dm /= GenDefMeth || validGenericMethodType op_ty)
1051 (badGenericMethodType op_name op_ty)
1053 op_name = idName sel_id
1054 op_ty = idType sel_id
1055 (_,theta,tau) = tcSplitSigmaTy op_ty
1058 = ptext SLIT("No parameters for class") <+> quotes (ppr cls)
1061 = vcat [ptext SLIT("Too many parameters for class") <+> quotes (ppr cls),
1062 parens (ptext SLIT("Use -fglasgow-exts to allow multi-parameter classes"))]
1064 genericMultiParamErr clas
1065 = ptext SLIT("The multi-parameter class") <+> quotes (ppr clas) <+>
1066 ptext SLIT("cannot have generic methods")
1068 badGenericMethodType op op_ty
1069 = hang (ptext SLIT("Generic method type is too complex"))
1070 4 (vcat [ppr op <+> dcolon <+> ppr op_ty,
1071 ptext SLIT("You can only use type variables, arrows, and tuples")])
1075 %************************************************************************
1077 \subsection{Checking for a decent instance head type}
1079 %************************************************************************
1081 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1082 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1084 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1085 flag is on, or (2)~the instance is imported (they must have been
1086 compiled elsewhere). In these cases, we let them go through anyway.
1088 We can also have instances for functions: @instance Foo (a -> b) ...@.
1091 checkValidInstHead :: Type -> TcM (Class, [TcType])
1093 checkValidInstHead ty -- Should be a source type
1094 = case tcSplitPredTy_maybe ty of {
1095 Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
1098 case getClassPredTys_maybe pred of {
1099 Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
1102 getDOpts `thenM` \ dflags ->
1103 mappM_ check_arg_type tys `thenM_`
1104 check_inst_head dflags clas tys `thenM_`
1108 check_inst_head dflags clas tys
1110 -- A user declaration of a CCallable/CReturnable instance
1111 -- must be for a "boxed primitive" type.
1112 (clas `hasKey` cCallableClassKey
1113 && not (ccallable_type first_ty))
1114 || (clas `hasKey` cReturnableClassKey
1115 && not (creturnable_type first_ty))
1116 = failWithTc (nonBoxedPrimCCallErr clas first_ty)
1118 -- If GlasgowExts then check at least one isn't a type variable
1119 | dopt Opt_GlasgowExts dflags
1120 = check_tyvars dflags clas tys
1122 -- WITH HASKELL 1.4, MUST HAVE C (T a b c)
1124 Just (tycon, arg_tys) <- tcSplitTyConApp_maybe first_ty,
1125 not (isSynTyCon tycon), -- ...but not a synonym
1126 all tcIsTyVarTy arg_tys, -- Applied to type variables
1127 equalLength (varSetElems (tyVarsOfTypes arg_tys)) arg_tys
1128 -- This last condition checks that all the type variables are distinct
1132 = failWithTc (instTypeErr (pprClassPred clas tys) head_shape_msg)
1135 (first_ty : _) = tys
1137 ccallable_type ty = isFFIArgumentTy dflags PlayRisky ty
1138 creturnable_type ty = isFFIImportResultTy dflags ty
1140 head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
1141 text "where T is not a synonym, and a,b,c are distinct type variables")
1143 check_tyvars dflags clas tys
1144 -- Check that at least one isn't a type variable
1145 -- unless -fallow-undecideable-instances
1146 | dopt Opt_AllowUndecidableInstances dflags = returnM ()
1147 | not (all tcIsTyVarTy tys) = returnM ()
1148 | otherwise = failWithTc (instTypeErr (pprClassPred clas tys) msg)
1150 msg = parens (ptext SLIT("There must be at least one non-type-variable in the instance head")
1153 undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
1157 instTypeErr pp_ty msg
1158 = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,
1161 nonBoxedPrimCCallErr clas inst_ty
1162 = hang (ptext SLIT("Unacceptable instance type for ccall-ish class"))
1163 4 (pprClassPred clas [inst_ty])