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,
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) $
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 WARN( not (immut_tv_ty `tcEqType` ty2), ppr tv $$ ppr immut_tv $$ ppr ty2 )
454 %************************************************************************
456 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
458 %* For internal use only! *
460 %************************************************************************
463 -- zonkType is used for Kinds as well
465 -- For unbound, mutable tyvars, zonkType uses the function given to it
466 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
467 -- type variable and zonks the kind too
469 zonkType :: (TcTyVar -> NF_TcM Type) -- What to do with unbound mutable type variables
470 -- see zonkTcType, and zonkTcTypeToType
473 zonkType unbound_var_fn ty
476 go (TyConApp tycon tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' ->
477 returnNF_Tc (TyConApp tycon tys')
479 go (NoteTy (SynNote ty1) ty2) = go ty1 `thenNF_Tc` \ ty1' ->
480 go ty2 `thenNF_Tc` \ ty2' ->
481 returnNF_Tc (NoteTy (SynNote ty1') ty2')
483 go (NoteTy (FTVNote _) ty2) = go ty2 -- Discard free-tyvar annotations
485 go (SourceTy p) = go_pred p `thenNF_Tc` \ p' ->
486 returnNF_Tc (SourceTy p')
488 go (FunTy arg res) = go arg `thenNF_Tc` \ arg' ->
489 go res `thenNF_Tc` \ res' ->
490 returnNF_Tc (FunTy arg' res')
492 go (AppTy fun arg) = go fun `thenNF_Tc` \ fun' ->
493 go arg `thenNF_Tc` \ arg' ->
494 returnNF_Tc (mkAppTy fun' arg')
495 -- NB the mkAppTy; we might have instantiated a
496 -- type variable to a type constructor, so we need
497 -- to pull the TyConApp to the top.
499 -- The two interesting cases!
500 go (TyVarTy tyvar) = zonkTyVar unbound_var_fn tyvar
502 go (ForAllTy tyvar ty) = zonkTcTyVarToTyVar tyvar `thenNF_Tc` \ tyvar' ->
503 go ty `thenNF_Tc` \ ty' ->
504 returnNF_Tc (ForAllTy tyvar' ty')
506 go_pred (ClassP c tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' ->
507 returnNF_Tc (ClassP c tys')
508 go_pred (NType tc tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' ->
509 returnNF_Tc (NType tc tys')
510 go_pred (IParam n ty) = go ty `thenNF_Tc` \ ty' ->
511 returnNF_Tc (IParam n ty')
513 zonkTyVar :: (TcTyVar -> NF_TcM Type) -- What to do for an unbound mutable variable
514 -> TcTyVar -> NF_TcM TcType
515 zonkTyVar unbound_var_fn tyvar
516 | not (isMutTyVar tyvar) -- Not a mutable tyvar. This can happen when
517 -- zonking a forall type, when the bound type variable
518 -- needn't be mutable
519 = ASSERT( isTyVar tyvar ) -- Should not be any immutable kind vars
520 returnNF_Tc (TyVarTy tyvar)
523 = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
525 Nothing -> unbound_var_fn tyvar -- Mutable and unbound
526 Just other_ty -> zonkType unbound_var_fn other_ty -- Bound
531 %************************************************************************
533 \subsection{Checking a user type}
535 %************************************************************************
537 When dealing with a user-written type, we first translate it from an HsType
538 to a Type, performing kind checking, and then check various things that should
539 be true about it. We don't want to perform these checks at the same time
540 as the initial translation because (a) they are unnecessary for interface-file
541 types and (b) when checking a mutually recursive group of type and class decls,
542 we can't "look" at the tycons/classes yet. Also, the checks are are rather
543 diverse, and used to really mess up the other code.
545 One thing we check for is 'rank'.
547 Rank 0: monotypes (no foralls)
548 Rank 1: foralls at the front only, Rank 0 inside
549 Rank 2: foralls at the front, Rank 1 on left of fn arrow,
551 basic ::= tyvar | T basic ... basic
553 r2 ::= forall tvs. cxt => r2a
554 r2a ::= r1 -> r2a | basic
555 r1 ::= forall tvs. cxt => r0
556 r0 ::= r0 -> r0 | basic
558 Another thing is to check that type synonyms are saturated.
559 This might not necessarily show up in kind checking.
561 data T k = MkT (k Int)
567 = FunSigCtxt Name -- Function type signature
568 | ExprSigCtxt -- Expression type signature
569 | ConArgCtxt Name -- Data constructor argument
570 | TySynCtxt Name -- RHS of a type synonym decl
571 | GenPatCtxt -- Pattern in generic decl
572 -- f{| a+b |} (Inl x) = ...
573 | PatSigCtxt -- Type sig in pattern
575 | ResSigCtxt -- Result type sig
577 | ForSigCtxt Name -- Foreign inport or export signature
578 | RuleSigCtxt Name -- Signature on a forall'd variable in a RULE
580 -- Notes re TySynCtxt
581 -- We allow type synonyms that aren't types; e.g. type List = []
583 -- If the RHS mentions tyvars that aren't in scope, we'll
584 -- quantify over them:
585 -- e.g. type T = a->a
586 -- will become type T = forall a. a->a
588 -- With gla-exts that's right, but for H98 we should complain.
591 pprUserTypeCtxt (FunSigCtxt n) = ptext SLIT("the type signature for") <+> quotes (ppr n)
592 pprUserTypeCtxt ExprSigCtxt = ptext SLIT("an expression type signature")
593 pprUserTypeCtxt (ConArgCtxt c) = ptext SLIT("the type of constructor") <+> quotes (ppr c)
594 pprUserTypeCtxt (TySynCtxt c) = ptext SLIT("the RHS of a type synonym declaration") <+> quotes (ppr c)
595 pprUserTypeCtxt GenPatCtxt = ptext SLIT("the type pattern of a generic definition")
596 pprUserTypeCtxt PatSigCtxt = ptext SLIT("a pattern type signature")
597 pprUserTypeCtxt ResSigCtxt = ptext SLIT("a result type signature")
598 pprUserTypeCtxt (ForSigCtxt n) = ptext SLIT("the foreign signature for") <+> quotes (ppr n)
599 pprUserTypeCtxt (RuleSigCtxt n) = ptext SLIT("the type signature on") <+> quotes (ppr n)
603 checkValidType :: UserTypeCtxt -> Type -> TcM ()
604 -- Checks that the type is valid for the given context
605 checkValidType ctxt ty
606 = doptsTc Opt_GlasgowExts `thenNF_Tc` \ gla_exts ->
608 rank | gla_exts = Arbitrary
610 = case ctxt of -- Haskell 98
614 TySynCtxt _ -> Rank 0
615 ExprSigCtxt -> Rank 1
616 FunSigCtxt _ -> Rank 1
617 ConArgCtxt _ -> Rank 1 -- We are given the type of the entire
618 -- constructor, hence rank 1
619 ForSigCtxt _ -> Rank 1
620 RuleSigCtxt _ -> Rank 1
622 actual_kind = typeKind ty
624 actual_kind_is_lifted = actual_kind `eqKind` liftedTypeKind
626 kind_ok = case ctxt of
627 TySynCtxt _ -> True -- Any kind will do
628 GenPatCtxt -> actual_kind_is_lifted
629 ForSigCtxt _ -> actual_kind_is_lifted
630 other -> isTypeKind actual_kind
632 ubx_tup | not gla_exts = UT_NotOk
633 | otherwise = case ctxt of
636 -- Unboxed tuples ok in function results,
637 -- but for type synonyms we allow them even at
640 tcAddErrCtxt (checkTypeCtxt ctxt ty) $
642 -- Check that the thing has kind Type, and is lifted if necessary
643 checkTc kind_ok (kindErr actual_kind) `thenTc_`
645 -- Check the internal validity of the type itself
646 check_poly_type rank ubx_tup ty
649 checkTypeCtxt ctxt ty
650 = vcat [ptext SLIT("In the type:") <+> ppr_ty ty,
651 ptext SLIT("While checking") <+> pprUserTypeCtxt ctxt ]
653 -- Hack alert. If there are no tyvars, (ppr sigma_ty) will print
654 -- something strange like {Eq k} -> k -> k, because there is no
655 -- ForAll at the top of the type. Since this is going to the user
656 -- we want it to look like a proper Haskell type even then; hence the hack
658 -- This shows up in the complaint about
660 -- op :: Eq a => a -> a
661 ppr_ty ty | null forall_tvs && notNull theta = pprTheta theta <+> ptext SLIT("=>") <+> ppr tau
664 (forall_tvs, theta, tau) = tcSplitSigmaTy ty
669 data Rank = Rank Int | Arbitrary
671 decRank :: Rank -> Rank
672 decRank Arbitrary = Arbitrary
673 decRank (Rank n) = Rank (n-1)
675 ----------------------------------------
676 data UbxTupFlag = UT_Ok | UT_NotOk
677 -- The "Ok" version means "ok if -fglasgow-exts is on"
679 ----------------------------------------
680 check_poly_type :: Rank -> UbxTupFlag -> Type -> TcM ()
681 check_poly_type (Rank 0) ubx_tup ty
682 = check_tau_type (Rank 0) ubx_tup ty
684 check_poly_type rank ubx_tup ty
686 (tvs, theta, tau) = tcSplitSigmaTy ty
688 check_valid_theta SigmaCtxt theta `thenTc_`
689 check_tau_type (decRank rank) ubx_tup tau `thenTc_`
690 checkFreeness tvs theta `thenTc_`
691 checkAmbiguity tvs theta (tyVarsOfType tau)
693 ----------------------------------------
694 check_arg_type :: Type -> TcM ()
695 -- The sort of type that can instantiate a type variable,
696 -- or be the argument of a type constructor.
697 -- Not an unboxed tuple, not a forall.
698 -- Other unboxed types are very occasionally allowed as type
699 -- arguments depending on the kind of the type constructor
701 -- For example, we want to reject things like:
703 -- instance Ord a => Ord (forall s. T s a)
705 -- g :: T s (forall b.b)
707 -- NB: unboxed tuples can have polymorphic or unboxed args.
708 -- This happens in the workers for functions returning
709 -- product types with polymorphic components.
710 -- But not in user code.
711 -- Anyway, they are dealt with by a special case in check_tau_type
714 = check_tau_type (Rank 0) UT_NotOk ty `thenTc_`
715 checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
717 ----------------------------------------
718 check_tau_type :: Rank -> UbxTupFlag -> Type -> TcM ()
719 -- Rank is allowed rank for function args
720 -- No foralls otherwise
722 check_tau_type rank ubx_tup ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty)
723 check_tau_type rank ubx_tup (SourceTy sty) = getDOptsTc `thenNF_Tc` \ dflags ->
724 check_source_ty dflags TypeCtxt sty
725 check_tau_type rank ubx_tup (TyVarTy _) = returnTc ()
726 check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
727 = check_poly_type rank UT_NotOk arg_ty `thenTc_`
728 check_tau_type rank UT_Ok res_ty
730 check_tau_type rank ubx_tup (AppTy ty1 ty2)
731 = check_arg_type ty1 `thenTc_` check_arg_type ty2
733 check_tau_type rank ubx_tup (NoteTy note ty)
734 = check_tau_type rank ubx_tup ty
735 -- Synonym notes are built only when the synonym is
736 -- saturated (see Type.mkSynTy)
737 -- Not checking the 'note' part allows us to instantiate a synonym
738 -- defn with a for-all type, or with a partially-applied type synonym,
739 -- but that seems OK too
741 check_tau_type rank ubx_tup ty@(TyConApp tc tys)
743 = -- NB: Type.mkSynTy builds a TyConApp (not a NoteTy) for an unsaturated
744 -- synonym application, leaving it to checkValidType (i.e. right here
746 checkTc syn_arity_ok arity_msg `thenTc_`
747 mapTc_ check_arg_type tys
749 | isUnboxedTupleTyCon tc
750 = doptsTc Opt_GlasgowExts `thenNF_Tc` \ gla_exts ->
751 checkTc (ubx_tup_ok gla_exts) ubx_tup_msg `thenTc_`
752 mapTc_ (check_tau_type (Rank 0) UT_Ok) tys
753 -- Args are allowed to be unlifted, or
754 -- more unboxed tuples, so can't use check_arg_ty
757 = mapTc_ check_arg_type tys
760 ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False }
762 syn_arity_ok = tc_arity <= n_args
763 -- It's OK to have an *over-applied* type synonym
764 -- data Tree a b = ...
765 -- type Foo a = Tree [a]
766 -- f :: Foo a b -> ...
768 tc_arity = tyConArity tc
770 arity_msg = arityErr "Type synonym" (tyConName tc) tc_arity n_args
771 ubx_tup_msg = ubxArgTyErr ty
773 ----------------------------------------
774 forAllTyErr ty = ptext SLIT("Illegal polymorphic type:") <+> ppr_ty ty
775 unliftedArgErr ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr_ty ty
776 ubxArgTyErr ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr_ty ty
777 kindErr kind = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
783 is ambiguous if P contains generic variables
784 (i.e. one of the Vs) that are not mentioned in tau
786 However, we need to take account of functional dependencies
787 when we speak of 'mentioned in tau'. Example:
788 class C a b | a -> b where ...
790 forall x y. (C x y) => x
791 is not ambiguous because x is mentioned and x determines y
793 NB; the ambiguity check is only used for *user* types, not for types
794 coming from inteface files. The latter can legitimately have
795 ambiguous types. Example
797 class S a where s :: a -> (Int,Int)
798 instance S Char where s _ = (1,1)
799 f:: S a => [a] -> Int -> (Int,Int)
800 f (_::[a]) x = (a*x,b)
801 where (a,b) = s (undefined::a)
803 Here the worker for f gets the type
804 fw :: forall a. S a => Int -> (# Int, Int #)
806 If the list of tv_names is empty, we have a monotype, and then we
807 don't need to check for ambiguity either, because the test can't fail
811 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
812 checkAmbiguity forall_tyvars theta tau_tyvars
813 = mapTc_ complain (filter is_ambig theta)
815 complain pred = addErrTc (ambigErr pred)
816 extended_tau_vars = grow theta tau_tyvars
817 is_ambig pred = any ambig_var (varSetElems (tyVarsOfPred pred))
819 ambig_var ct_var = (ct_var `elem` forall_tyvars) &&
820 not (ct_var `elemVarSet` extended_tau_vars)
822 is_free ct_var = not (ct_var `elem` forall_tyvars)
825 = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
826 nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
827 ptext SLIT("must be reachable from the type after the '=>'"))]
830 In addition, GHC insists that at least one type variable
831 in each constraint is in V. So we disallow a type like
832 forall a. Eq b => b -> b
833 even in a scope where b is in scope.
836 checkFreeness forall_tyvars theta
837 = mapTc_ complain (filter is_free theta)
839 is_free pred = not (isIPPred pred)
840 && not (any bound_var (varSetElems (tyVarsOfPred pred)))
841 bound_var ct_var = ct_var `elem` forall_tyvars
842 complain pred = addErrTc (freeErr pred)
845 = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
846 ptext SLIT("are already in scope"),
847 nest 4 (ptext SLIT("(at least one must be universally quantified here)"))
852 %************************************************************************
854 \subsection{Checking a theta or source type}
856 %************************************************************************
860 = ClassSCCtxt Name -- Superclasses of clas
861 | SigmaCtxt -- Context of a normal for-all type
862 | DataTyCtxt Name -- Context of a data decl
863 | TypeCtxt -- Source type in an ordinary type
864 | InstThetaCtxt -- Context of an instance decl
865 | InstHeadCtxt -- Head of an instance decl
867 pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
868 pprSourceTyCtxt SigmaCtxt = ptext SLIT("the context of a polymorphic type")
869 pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
870 pprSourceTyCtxt InstThetaCtxt = ptext SLIT("the context of an instance declaration")
871 pprSourceTyCtxt InstHeadCtxt = ptext SLIT("the head of an instance declaration")
872 pprSourceTyCtxt TypeCtxt = ptext SLIT("the context of a type")
876 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
877 checkValidTheta ctxt theta
878 = tcAddErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
880 -------------------------
881 check_valid_theta ctxt []
883 check_valid_theta ctxt theta
884 = getDOptsTc `thenNF_Tc` \ dflags ->
885 warnTc (notNull dups) (dupPredWarn dups) `thenNF_Tc_`
886 mapTc_ (check_source_ty dflags ctxt) theta
888 (_,dups) = removeDups tcCmpPred theta
890 -------------------------
891 check_source_ty dflags ctxt pred@(ClassP cls tys)
892 = -- Class predicates are valid in all contexts
893 mapTc_ check_arg_type tys `thenTc_`
894 checkTc (arity == n_tys) arity_err `thenTc_`
895 checkTc (all tyvar_head tys || arby_preds_ok)
896 (predTyVarErr pred $$ how_to_allow)
899 class_name = className cls
900 arity = classArity cls
902 arity_err = arityErr "Class" class_name arity n_tys
904 arby_preds_ok = case ctxt of
905 InstHeadCtxt -> True -- We check for instance-head formation
906 -- in checkValidInstHead
907 InstThetaCtxt -> dopt Opt_AllowUndecidableInstances dflags
908 other -> dopt Opt_GlasgowExts dflags
910 how_to_allow = case ctxt of
911 InstHeadCtxt -> empty -- Should not happen
912 InstThetaCtxt -> parens undecidableMsg
913 other -> parens (ptext SLIT("Use -fglasgow-exts to permit this"))
915 check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
916 -- Implicit parameters only allows in type
917 -- signatures; not in instance decls, superclasses etc
918 -- The reason for not allowing implicit params in instances is a bit subtle
919 -- If we allowed instance (?x::Int, Eq a) => Foo [a] where ...
920 -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
921 -- discharge all the potential usas of the ?x in e. For example, a
922 -- constraint Foo [Int] might come out of e,and applying the
923 -- instance decl would show up two uses of ?x.
925 check_source_ty dflags TypeCtxt (NType tc tys) = mapTc_ check_arg_type tys
928 check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
930 -------------------------
931 tyvar_head ty -- Haskell 98 allows predicates of form
932 | tcIsTyVarTy ty = True -- C (a ty1 .. tyn)
933 | otherwise -- where a is a type variable
934 = case tcSplitAppTy_maybe ty of
935 Just (ty, _) -> tyvar_head ty
940 badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprSourceType sty
941 predTyVarErr pred = ptext SLIT("Non-type variables in constraint:") <+> pprPred pred
942 dupPredWarn dups = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
944 checkThetaCtxt ctxt theta
945 = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
946 ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
950 %************************************************************************
952 \subsection{Validity check for TyCons}
954 %************************************************************************
956 checkValidTyCon is called once the mutually-recursive knot has been
957 tied, so we can look at things freely.
960 checkValidTyCon :: TyCon -> TcM ()
962 | isSynTyCon tc = checkValidType (TySynCtxt name) syn_rhs
964 = -- Check the context on the data decl
965 checkValidTheta (DataTyCtxt name) (tyConTheta tc) `thenTc_`
967 -- Check arg types of data constructors
968 mapTc_ checkValidDataCon data_cons `thenTc_`
970 -- Check that fields with the same name share a type
971 mapTc_ check_fields groups
975 (_, syn_rhs) = getSynTyConDefn tc
976 data_cons = tyConDataCons tc
978 fields = [field | con <- data_cons, field <- dataConFieldLabels con]
979 groups = equivClasses cmp_name fields
980 cmp_name field1 field2 = fieldLabelName field1 `compare` fieldLabelName field2
982 check_fields fields@(first_field_label : other_fields)
983 -- These fields all have the same name, but are from
984 -- different constructors in the data type
985 = -- Check that all the fields in the group have the same type
986 -- NB: this check assumes that all the constructors of a given
987 -- data type use the same type variables
988 checkTc (all (tcEqType field_ty) other_tys) (fieldTypeMisMatch field_name)
990 field_ty = fieldLabelType first_field_label
991 field_name = fieldLabelName first_field_label
992 other_tys = map fieldLabelType other_fields
994 checkValidDataCon :: DataCon -> TcM ()
995 checkValidDataCon con
996 = checkValidType ctxt (idType (dataConWrapId con)) `thenTc_`
997 -- This checks the argument types and
998 -- ambiguity of the existential context (if any)
999 tcAddErrCtxt (existentialCtxt con)
1000 (checkFreeness ex_tvs ex_theta)
1002 ctxt = ConArgCtxt (dataConName con)
1003 (_, _, ex_tvs, ex_theta, _, _) = dataConSig con
1006 fieldTypeMisMatch field_name
1007 = sep [ptext SLIT("Different constructors give different types for field"), quotes (ppr field_name)]
1009 existentialCtxt con = ptext SLIT("When checking the existential context of constructor")
1010 <+> quotes (ppr con)
1014 checkValidClass is called once the mutually-recursive knot has been
1015 tied, so we can look at things freely.
1018 checkValidClass :: Class -> TcM ()
1020 = -- CHECK ARITY 1 FOR HASKELL 1.4
1021 doptsTc Opt_GlasgowExts `thenTc` \ gla_exts ->
1023 -- Check that the class is unary, unless GlaExs
1024 checkTc (notNull tyvars) (nullaryClassErr cls) `thenTc_`
1025 checkTc (gla_exts || unary) (classArityErr cls) `thenTc_`
1027 -- Check the super-classes
1028 checkValidTheta (ClassSCCtxt (className cls)) theta `thenTc_`
1030 -- Check the class operations
1031 mapTc_ check_op op_stuff `thenTc_`
1033 -- Check that if the class has generic methods, then the
1034 -- class has only one parameter. We can't do generic
1035 -- multi-parameter type classes!
1036 checkTc (unary || no_generics) (genericMultiParamErr cls)
1039 (tyvars, theta, _, op_stuff) = classBigSig cls
1040 unary = isSingleton tyvars
1041 no_generics = null [() | (_, GenDefMeth) <- op_stuff]
1043 check_op (sel_id, dm)
1044 = checkValidTheta SigmaCtxt (tail theta) `thenTc_`
1045 -- The 'tail' removes the initial (C a) from the
1046 -- class itself, leaving just the method type
1048 checkValidType (FunSigCtxt op_name) tau `thenTc_`
1050 -- Check that for a generic method, the type of
1051 -- the method is sufficiently simple
1052 checkTc (dm /= GenDefMeth || validGenericMethodType op_ty)
1053 (badGenericMethodType op_name op_ty)
1055 op_name = idName sel_id
1056 op_ty = idType sel_id
1057 (_,theta,tau) = tcSplitSigmaTy op_ty
1060 = ptext SLIT("No parameters for class") <+> quotes (ppr cls)
1063 = vcat [ptext SLIT("Too many parameters for class") <+> quotes (ppr cls),
1064 parens (ptext SLIT("Use -fglasgow-exts to allow multi-parameter classes"))]
1066 genericMultiParamErr clas
1067 = ptext SLIT("The multi-parameter class") <+> quotes (ppr clas) <+>
1068 ptext SLIT("cannot have generic methods")
1070 badGenericMethodType op op_ty
1071 = hang (ptext SLIT("Generic method type is too complex"))
1072 4 (vcat [ppr op <+> dcolon <+> ppr op_ty,
1073 ptext SLIT("You can only use type variables, arrows, and tuples")])
1077 %************************************************************************
1079 \subsection{Checking for a decent instance head type}
1081 %************************************************************************
1083 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1084 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1086 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1087 flag is on, or (2)~the instance is imported (they must have been
1088 compiled elsewhere). In these cases, we let them go through anyway.
1090 We can also have instances for functions: @instance Foo (a -> b) ...@.
1093 checkValidInstHead :: Type -> TcM (Class, [TcType])
1095 checkValidInstHead ty -- Should be a source type
1096 = case tcSplitPredTy_maybe ty of {
1097 Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
1100 case getClassPredTys_maybe pred of {
1101 Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
1104 getDOptsTc `thenNF_Tc` \ dflags ->
1105 mapTc_ check_arg_type tys `thenTc_`
1106 check_inst_head dflags clas tys `thenTc_`
1107 returnTc (clas, tys)
1110 check_inst_head dflags clas tys
1112 -- A user declaration of a CCallable/CReturnable instance
1113 -- must be for a "boxed primitive" type.
1114 (clas `hasKey` cCallableClassKey
1115 && not (ccallable_type first_ty))
1116 || (clas `hasKey` cReturnableClassKey
1117 && not (creturnable_type first_ty))
1118 = failWithTc (nonBoxedPrimCCallErr clas first_ty)
1120 -- If GlasgowExts then check at least one isn't a type variable
1121 | dopt Opt_GlasgowExts dflags
1122 = check_tyvars dflags clas tys
1124 -- WITH HASKELL 1.4, MUST HAVE C (T a b c)
1126 Just (tycon, arg_tys) <- tcSplitTyConApp_maybe first_ty,
1127 not (isSynTyCon tycon), -- ...but not a synonym
1128 all tcIsTyVarTy arg_tys, -- Applied to type variables
1129 equalLength (varSetElems (tyVarsOfTypes arg_tys)) arg_tys
1130 -- This last condition checks that all the type variables are distinct
1134 = failWithTc (instTypeErr (pprClassPred clas tys) head_shape_msg)
1137 (first_ty : _) = tys
1139 ccallable_type ty = isFFIArgumentTy dflags PlayRisky ty
1140 creturnable_type ty = isFFIImportResultTy dflags ty
1142 head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
1143 text "where T is not a synonym, and a,b,c are distinct type variables")
1145 check_tyvars dflags clas tys
1146 -- Check that at least one isn't a type variable
1147 -- unless -fallow-undecideable-instances
1148 | dopt Opt_AllowUndecidableInstances dflags = returnTc ()
1149 | not (all tcIsTyVarTy tys) = returnTc ()
1150 | otherwise = failWithTc (instTypeErr (pprClassPred clas tys) msg)
1152 msg = parens (ptext SLIT("There must be at least one non-type-variable in the instance head")
1155 undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
1159 instTypeErr pp_ty msg
1160 = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,
1163 nonBoxedPrimCCallErr clas inst_ty
1164 = hang (ptext SLIT("Unacceptable instance type for ccall-ish class"))
1165 4 (pprClassPred clas [inst_ty])