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 -> TcM TcType
16 newTyVarTys, -- Int -> Kind -> TcM [TcType]
17 newKindVar, newKindVars, newBoxityVar,
18 putTcTyVar, getTcTyVar,
19 newMutTyVar, readMutTyVar, writeMutTyVar,
21 newHoleTyVarTy, readHoleResult, zapToType,
23 --------------------------------
25 tcInstTyVar, tcInstTyVars, tcInstType,
27 --------------------------------
28 -- Checking type validity
29 Rank, UserTypeCtxt(..), checkValidType, pprUserTypeCtxt,
30 SourceTyCtxt(..), checkValidTheta,
31 checkValidTyCon, checkValidClass,
32 checkValidInstHead, instTypeErr, checkAmbiguity,
35 --------------------------------
37 zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV,
38 zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
39 zonkTcPredType, zonkTcTypeToType, zonkTcTyVarToTyVar, zonkKindEnv,
43 #include "HsVersions.h"
47 import TypeRep ( Type(..), SourceType(..), TyNote(..), -- Friend; can see representation
50 import TcType ( TcType, TcThetaType, TcTauType, TcPredType,
51 TcTyVarSet, TcKind, TcTyVar, TyVarDetails(..),
53 tcSplitPhiTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe,
54 tcSplitTyConApp_maybe, tcSplitForAllTys,
55 tcIsTyVarTy, tcSplitSigmaTy,
56 isUnLiftedType, isIPPred, isHoleTyVar, isTyVarTy,
58 mkAppTy, mkTyVarTy, mkTyVarTys,
59 tyVarsOfPred, getClassPredTys_maybe,
61 liftedTypeKind, openTypeKind, defaultKind, superKind,
62 superBoxity, liftedBoxity, typeKind,
63 tyVarsOfType, tyVarsOfTypes,
64 eqKind, isTypeKind, isAnyTypeKind,
66 isFFIArgumentTy, isFFIImportResultTy
68 import qualified Type ( splitFunTys )
69 import Subst ( Subst, mkTopTyVarSubst, substTy )
70 import Class ( Class, DefMeth(..), classArity, className, classBigSig )
71 import TyCon ( TyCon, mkPrimTyCon, isSynTyCon, isUnboxedTupleTyCon,
72 tyConArity, tyConName, tyConKind, tyConTheta,
73 getSynTyConDefn, tyConDataCons )
74 import DataCon ( DataCon, dataConWrapId, dataConName, dataConSig, dataConFieldLabels )
75 import FieldLabel ( fieldLabelName, fieldLabelType )
76 import PrimRep ( PrimRep(VoidRep) )
77 import Var ( TyVar, idType, idName, tyVarKind, tyVarName, isTyVar,
78 mkTyVar, mkMutTyVar, isMutTyVar, mutTyVarRef )
81 import Generics ( validGenericMethodType )
82 import TcRnMonad -- TcType, amongst others
83 import TysWiredIn ( voidTy, listTyCon, tupleTyCon )
84 import PrelNames ( cCallableClassKey, cReturnableClassKey, hasKey )
85 import ForeignCall ( Safety(..) )
86 import FunDeps ( grow )
87 import PprType ( pprPred, pprSourceType, pprTheta, pprClassPred )
88 import Name ( Name, NamedThing(..), setNameUnique,
89 mkInternalName, mkDerivedTyConOcc,
90 mkSystemTvNameEncoded,
93 import BasicTypes ( Boxity(Boxed) )
94 import CmdLineOpts ( dopt, DynFlag(..) )
95 import Unique ( Uniquable(..) )
96 import SrcLoc ( noSrcLoc )
97 import Util ( nOfThem, isSingleton, equalLength, notNull )
98 import ListSetOps ( equivClasses, removeDups )
103 %************************************************************************
105 \subsection{New type variables}
107 %************************************************************************
110 newMutTyVar :: Name -> Kind -> TyVarDetails -> TcM TyVar
111 newMutTyVar name kind details
112 = do { ref <- newMutVar Nothing ;
113 return (mkMutTyVar name kind details ref) }
115 readMutTyVar :: TyVar -> TcM (Maybe Type)
116 readMutTyVar tyvar = readMutVar (mutTyVarRef tyvar)
118 writeMutTyVar :: TyVar -> Maybe Type -> TcM ()
119 writeMutTyVar tyvar val = writeMutVar (mutTyVarRef tyvar) val
121 newTyVar :: Kind -> TcM TcTyVar
123 = newUnique `thenM` \ uniq ->
124 newMutTyVar (mkSystemTvNameEncoded uniq FSLIT("t")) kind VanillaTv
126 newTyVarTy :: Kind -> TcM TcType
128 = newTyVar kind `thenM` \ tc_tyvar ->
129 returnM (TyVarTy tc_tyvar)
131 newTyVarTys :: Int -> Kind -> TcM [TcType]
132 newTyVarTys n kind = mappM newTyVarTy (nOfThem n kind)
134 newKindVar :: TcM TcKind
136 = newUnique `thenM` \ uniq ->
137 newMutTyVar (mkSystemTvNameEncoded uniq FSLIT("k")) superKind VanillaTv `thenM` \ kv ->
140 newKindVars :: Int -> TcM [TcKind]
141 newKindVars n = mappM (\ _ -> newKindVar) (nOfThem n ())
143 newBoxityVar :: TcM TcKind
145 = newUnique `thenM` \ uniq ->
146 newMutTyVar (mkSystemTvNameEncoded uniq FSLIT("bx")) superBoxity VanillaTv `thenM` \ kv ->
151 %************************************************************************
153 \subsection{'hole' type variables}
155 %************************************************************************
158 newHoleTyVarTy :: TcM TcType
159 = newUnique `thenM` \ uniq ->
160 newMutTyVar (mkSystemTvNameEncoded uniq FSLIT("h")) openTypeKind HoleTv `thenM` \ tv ->
163 readHoleResult :: TcType -> TcM TcType
164 -- Read the answer out of a hole, constructed by newHoleTyVarTy
165 readHoleResult (TyVarTy tv)
166 = ASSERT( isHoleTyVar tv )
167 getTcTyVar tv `thenM` \ maybe_res ->
169 Just ty -> returnM ty
170 Nothing -> pprPanic "readHoleResult: empty" (ppr tv)
171 readHoleResult ty = pprPanic "readHoleResult: not hole" (ppr ty)
173 zapToType :: TcType -> TcM TcType
174 zapToType (TyVarTy tv)
176 = getTcTyVar tv `thenM` \ maybe_res ->
178 Nothing -> newTyVarTy openTypeKind `thenM` \ ty ->
179 putTcTyVar tv ty `thenM_`
181 Just ty -> returnM ty -- No need to loop; we never
182 -- have chains of holes
184 zapToType other_ty = returnM other_ty
187 %************************************************************************
189 \subsection{Type instantiation}
191 %************************************************************************
193 Instantiating a bunch of type variables
196 tcInstTyVars :: TyVarDetails -> [TyVar]
197 -> TcM ([TcTyVar], [TcType], Subst)
199 tcInstTyVars tv_details tyvars
200 = mappM (tcInstTyVar tv_details) tyvars `thenM` \ tc_tyvars ->
202 tys = mkTyVarTys tc_tyvars
204 returnM (tc_tyvars, tys, mkTopTyVarSubst tyvars tys)
205 -- Since the tyvars are freshly made,
206 -- they cannot possibly be captured by
207 -- any existing for-alls. Hence mkTopTyVarSubst
209 tcInstTyVar tv_details tyvar
210 = newUnique `thenM` \ uniq ->
212 name = setNameUnique (tyVarName tyvar) uniq
213 -- Note that we don't change the print-name
214 -- This won't confuse the type checker but there's a chance
215 -- that two different tyvars will print the same way
216 -- in an error message. -dppr-debug will show up the difference
217 -- Better watch out for this. If worst comes to worst, just
220 newMutTyVar name (tyVarKind tyvar) tv_details
222 tcInstType :: TyVarDetails -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
223 -- tcInstType instantiates the outer-level for-alls of a TcType with
224 -- fresh (mutable) type variables, splits off the dictionary part,
225 -- and returns the pieces.
226 tcInstType tv_details ty
227 = case tcSplitForAllTys ty of
228 ([], rho) -> -- There may be overloading despite no type variables;
229 -- (?x :: Int) => Int -> Int
231 (theta, tau) = tcSplitPhiTy rho
233 returnM ([], theta, tau)
235 (tyvars, rho) -> tcInstTyVars tv_details tyvars `thenM` \ (tyvars', _, tenv) ->
237 (theta, tau) = tcSplitPhiTy (substTy tenv rho)
239 returnM (tyvars', theta, tau)
243 %************************************************************************
245 \subsection{Putting and getting mutable type variables}
247 %************************************************************************
250 putTcTyVar :: TcTyVar -> TcType -> TcM TcType
251 getTcTyVar :: TcTyVar -> TcM (Maybe TcType)
258 | not (isMutTyVar tyvar)
259 = pprTrace "putTcTyVar" (ppr tyvar) $
263 = ASSERT( isMutTyVar tyvar )
264 writeMutTyVar tyvar (Just ty) `thenM_`
268 Getting is more interesting. The easy thing to do is just to read, thus:
271 getTcTyVar tyvar = readMutTyVar tyvar
274 But it's more fun to short out indirections on the way: If this
275 version returns a TyVar, then that TyVar is unbound. If it returns
276 any other type, then there might be bound TyVars embedded inside it.
278 We return Nothing iff the original box was unbound.
282 | not (isMutTyVar tyvar)
283 = pprTrace "getTcTyVar" (ppr tyvar) $
284 returnM (Just (mkTyVarTy tyvar))
287 = ASSERT2( isMutTyVar tyvar, ppr tyvar )
288 readMutTyVar tyvar `thenM` \ maybe_ty ->
290 Just ty -> short_out ty `thenM` \ ty' ->
291 writeMutTyVar tyvar (Just ty') `thenM_`
294 Nothing -> returnM Nothing
296 short_out :: TcType -> TcM TcType
297 short_out ty@(TyVarTy tyvar)
298 | not (isMutTyVar tyvar)
302 = readMutTyVar tyvar `thenM` \ maybe_ty ->
304 Just ty' -> short_out ty' `thenM` \ ty' ->
305 writeMutTyVar tyvar (Just ty') `thenM_`
310 short_out other_ty = returnM other_ty
314 %************************************************************************
316 \subsection{Zonking -- the exernal interfaces}
318 %************************************************************************
320 ----------------- Type variables
323 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
324 zonkTcTyVars tyvars = mappM zonkTcTyVar tyvars
326 zonkTcTyVarsAndFV :: [TcTyVar] -> TcM TcTyVarSet
327 zonkTcTyVarsAndFV tyvars = mappM zonkTcTyVar tyvars `thenM` \ tys ->
328 returnM (tyVarsOfTypes tys)
330 zonkTcTyVar :: TcTyVar -> TcM TcType
331 zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnM (TyVarTy tv)) tyvar
334 ----------------- Types
337 zonkTcType :: TcType -> TcM TcType
338 zonkTcType ty = zonkType (\ tv -> returnM (TyVarTy tv)) ty
340 zonkTcTypes :: [TcType] -> TcM [TcType]
341 zonkTcTypes tys = mappM zonkTcType tys
343 zonkTcClassConstraints cts = mappM zonk cts
344 where zonk (clas, tys)
345 = zonkTcTypes tys `thenM` \ new_tys ->
346 returnM (clas, new_tys)
348 zonkTcThetaType :: TcThetaType -> TcM TcThetaType
349 zonkTcThetaType theta = mappM zonkTcPredType theta
351 zonkTcPredType :: TcPredType -> TcM TcPredType
352 zonkTcPredType (ClassP c ts)
353 = zonkTcTypes ts `thenM` \ new_ts ->
354 returnM (ClassP c new_ts)
355 zonkTcPredType (IParam n t)
356 = zonkTcType t `thenM` \ new_t ->
357 returnM (IParam n new_t)
360 ------------------- These ...ToType, ...ToKind versions
361 are used at the end of type checking
364 zonkKindEnv :: [(Name, TcKind)] -> TcM [(Name, Kind)]
366 = mappM zonk_it pairs
368 zonk_it (name, tc_kind) = zonkType zonk_unbound_kind_var tc_kind `thenM` \ kind ->
371 -- When zonking a kind, we want to
372 -- zonk a *kind* variable to (Type *)
373 -- zonk a *boxity* variable to *
374 zonk_unbound_kind_var kv | tyVarKind kv `eqKind` superKind = putTcTyVar kv liftedTypeKind
375 | tyVarKind kv `eqKind` superBoxity = putTcTyVar kv liftedBoxity
376 | otherwise = pprPanic "zonkKindEnv" (ppr kv)
378 zonkTcTypeToType :: TcType -> TcM Type
379 zonkTcTypeToType ty = zonkType zonk_unbound_tyvar ty
381 -- Zonk a mutable but unbound type variable to an arbitrary type
382 -- We know it's unbound even though we don't carry an environment,
383 -- because at the binding site for a type variable we bind the
384 -- mutable tyvar to a fresh immutable one. So the mutable store
385 -- plays the role of an environment. If we come across a mutable
386 -- type variable that isn't so bound, it must be completely free.
387 zonk_unbound_tyvar tv = putTcTyVar tv (mkArbitraryType tv)
390 -- When the type checker finds a type variable with no binding,
391 -- which means it can be instantiated with an arbitrary type, it
392 -- usually instantiates it to Void. Eg.
396 -- length Void (Nil Void)
398 -- But in really obscure programs, the type variable might have
399 -- a kind other than *, so we need to invent a suitably-kinded type.
403 -- List for kind *->*
404 -- Tuple for kind *->...*->*
406 -- which deals with most cases. (Previously, it only dealt with
409 -- In the other cases, it just makes up a TyCon with a suitable
410 -- kind. If this gets into an interface file, anyone reading that
411 -- file won't understand it. This is fixable (by making the client
412 -- of the interface file make up a TyCon too) but it is tiresome and
413 -- never happens, so I am leaving it
415 mkArbitraryType :: TcTyVar -> Type
416 -- Make up an arbitrary type whose kind is the same as the tyvar.
417 -- We'll use this to instantiate the (unbound) tyvar.
419 | isAnyTypeKind kind = voidTy -- The vastly common case
420 | otherwise = TyConApp tycon []
423 (args,res) = Type.splitFunTys kind -- Kinds are simple; use Type.splitFunTys
425 tycon | kind `eqKind` tyConKind listTyCon -- *->*
426 = listTyCon -- No tuples this size
428 | all isTypeKind args && isTypeKind res
429 = tupleTyCon Boxed (length args) -- *-> ... ->*->*
432 = pprTrace "Urk! Inventing strangely-kinded void TyCon:" (ppr tc_name $$ ppr kind) $
433 mkPrimTyCon tc_name kind 0 [] VoidRep
434 -- Same name as the tyvar, apart from making it start with a colon (sigh)
435 -- I dread to think what will happen if this gets out into an
436 -- interface file. Catastrophe likely. Major sigh.
438 tc_name = mkInternalName (getUnique tv) (mkDerivedTyConOcc (getOccName tv)) noSrcLoc
440 -- zonkTcTyVarToTyVar is applied to the *binding* occurrence
441 -- of a type variable, at the *end* of type checking. It changes
442 -- the *mutable* type variable into an *immutable* one.
444 -- It does this by making an immutable version of tv and binds tv to it.
445 -- Now any bound occurences of the original type variable will get
446 -- zonked to the immutable version.
448 zonkTcTyVarToTyVar :: TcTyVar -> TcM TyVar
449 zonkTcTyVarToTyVar tv
451 -- Make an immutable version, defaulting
452 -- the kind to lifted if necessary
453 immut_tv = mkTyVar (tyVarName tv) (defaultKind (tyVarKind tv))
454 immut_tv_ty = mkTyVarTy immut_tv
456 zap tv = putTcTyVar tv immut_tv_ty
457 -- Bind the mutable version to the immutable one
459 -- If the type variable is mutable, then bind it to immut_tv_ty
460 -- so that all other occurrences of the tyvar will get zapped too
461 zonkTyVar zap tv `thenM` \ ty2 ->
463 -- This warning shows up if the allegedly-unbound tyvar is
464 -- already bound to something. It can actually happen, and
465 -- in a harmless way (see [Silly Type Synonyms] below) so
466 -- it's only a warning
467 WARN( not (immut_tv_ty `tcEqType` ty2), ppr tv $$ ppr immut_tv $$ ppr ty2 )
472 [Silly Type Synonyms]
475 type C u a = u -- Note 'a' unused
477 foo :: (forall a. C u a -> C u a) -> u
481 bar = foo (\t -> t + t)
483 * From the (\t -> t+t) we get type {Num d} => d -> d
486 * Now unify with type of foo's arg, and we get:
487 {Num (C d a)} => C d a -> C d a
490 * Now abstract over the 'a', but float out the Num (C d a) constraint
491 because it does not 'really' mention a. (see Type.tyVarsOfType)
492 The arg to foo becomes
495 * So we get a dict binding for Num (C d a), which is zonked to give
498 * Then the /\a abstraction has a zonked 'a' in it.
500 All very silly. I think its harmless to ignore the problem.
503 %************************************************************************
505 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
507 %* For internal use only! *
509 %************************************************************************
512 -- zonkType is used for Kinds as well
514 -- For unbound, mutable tyvars, zonkType uses the function given to it
515 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
516 -- type variable and zonks the kind too
518 zonkType :: (TcTyVar -> TcM Type) -- What to do with unbound mutable type variables
519 -- see zonkTcType, and zonkTcTypeToType
522 zonkType unbound_var_fn ty
525 go (TyConApp tycon tys) = mappM go tys `thenM` \ tys' ->
526 returnM (TyConApp tycon tys')
528 go (NoteTy (SynNote ty1) ty2) = go ty1 `thenM` \ ty1' ->
529 go ty2 `thenM` \ ty2' ->
530 returnM (NoteTy (SynNote ty1') ty2')
532 go (NoteTy (FTVNote _) ty2) = go ty2 -- Discard free-tyvar annotations
534 go (SourceTy p) = go_pred p `thenM` \ p' ->
535 returnM (SourceTy p')
537 go (FunTy arg res) = go arg `thenM` \ arg' ->
538 go res `thenM` \ res' ->
539 returnM (FunTy arg' res')
541 go (AppTy fun arg) = go fun `thenM` \ fun' ->
542 go arg `thenM` \ arg' ->
543 returnM (mkAppTy fun' arg')
544 -- NB the mkAppTy; we might have instantiated a
545 -- type variable to a type constructor, so we need
546 -- to pull the TyConApp to the top.
548 -- The two interesting cases!
549 go (TyVarTy tyvar) = zonkTyVar unbound_var_fn tyvar
551 go (ForAllTy tyvar ty) = zonkTcTyVarToTyVar tyvar `thenM` \ tyvar' ->
552 go ty `thenM` \ ty' ->
553 returnM (ForAllTy tyvar' ty')
555 go_pred (ClassP c tys) = mappM go tys `thenM` \ tys' ->
556 returnM (ClassP c tys')
557 go_pred (NType tc tys) = mappM go tys `thenM` \ tys' ->
558 returnM (NType tc tys')
559 go_pred (IParam n ty) = go ty `thenM` \ ty' ->
560 returnM (IParam n ty')
562 zonkTyVar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable variable
563 -> TcTyVar -> TcM TcType
564 zonkTyVar unbound_var_fn tyvar
565 | not (isMutTyVar tyvar) -- Not a mutable tyvar. This can happen when
566 -- zonking a forall type, when the bound type variable
567 -- needn't be mutable
568 = ASSERT( isTyVar tyvar ) -- Should not be any immutable kind vars
569 returnM (TyVarTy tyvar)
572 = getTcTyVar tyvar `thenM` \ maybe_ty ->
574 Nothing -> unbound_var_fn tyvar -- Mutable and unbound
575 Just other_ty -> zonkType unbound_var_fn other_ty -- Bound
580 %************************************************************************
582 \subsection{Checking a user type}
584 %************************************************************************
586 When dealing with a user-written type, we first translate it from an HsType
587 to a Type, performing kind checking, and then check various things that should
588 be true about it. We don't want to perform these checks at the same time
589 as the initial translation because (a) they are unnecessary for interface-file
590 types and (b) when checking a mutually recursive group of type and class decls,
591 we can't "look" at the tycons/classes yet. Also, the checks are are rather
592 diverse, and used to really mess up the other code.
594 One thing we check for is 'rank'.
596 Rank 0: monotypes (no foralls)
597 Rank 1: foralls at the front only, Rank 0 inside
598 Rank 2: foralls at the front, Rank 1 on left of fn arrow,
600 basic ::= tyvar | T basic ... basic
602 r2 ::= forall tvs. cxt => r2a
603 r2a ::= r1 -> r2a | basic
604 r1 ::= forall tvs. cxt => r0
605 r0 ::= r0 -> r0 | basic
607 Another thing is to check that type synonyms are saturated.
608 This might not necessarily show up in kind checking.
610 data T k = MkT (k Int)
616 = FunSigCtxt Name -- Function type signature
617 | ExprSigCtxt -- Expression type signature
618 | ConArgCtxt Name -- Data constructor argument
619 | TySynCtxt Name -- RHS of a type synonym decl
620 | GenPatCtxt -- Pattern in generic decl
621 -- f{| a+b |} (Inl x) = ...
622 | PatSigCtxt -- Type sig in pattern
624 | ResSigCtxt -- Result type sig
626 | ForSigCtxt Name -- Foreign inport or export signature
627 | RuleSigCtxt Name -- Signature on a forall'd variable in a RULE
629 -- Notes re TySynCtxt
630 -- We allow type synonyms that aren't types; e.g. type List = []
632 -- If the RHS mentions tyvars that aren't in scope, we'll
633 -- quantify over them:
634 -- e.g. type T = a->a
635 -- will become type T = forall a. a->a
637 -- With gla-exts that's right, but for H98 we should complain.
640 pprUserTypeCtxt (FunSigCtxt n) = ptext SLIT("the type signature for") <+> quotes (ppr n)
641 pprUserTypeCtxt ExprSigCtxt = ptext SLIT("an expression type signature")
642 pprUserTypeCtxt (ConArgCtxt c) = ptext SLIT("the type of constructor") <+> quotes (ppr c)
643 pprUserTypeCtxt (TySynCtxt c) = ptext SLIT("the RHS of a type synonym declaration") <+> quotes (ppr c)
644 pprUserTypeCtxt GenPatCtxt = ptext SLIT("the type pattern of a generic definition")
645 pprUserTypeCtxt PatSigCtxt = ptext SLIT("a pattern type signature")
646 pprUserTypeCtxt ResSigCtxt = ptext SLIT("a result type signature")
647 pprUserTypeCtxt (ForSigCtxt n) = ptext SLIT("the foreign signature for") <+> quotes (ppr n)
648 pprUserTypeCtxt (RuleSigCtxt n) = ptext SLIT("the type signature on") <+> quotes (ppr n)
652 checkValidType :: UserTypeCtxt -> Type -> TcM ()
653 -- Checks that the type is valid for the given context
654 checkValidType ctxt ty
655 = doptM Opt_GlasgowExts `thenM` \ gla_exts ->
657 rank | gla_exts = Arbitrary
659 = case ctxt of -- Haskell 98
663 TySynCtxt _ -> Rank 0
664 ExprSigCtxt -> Rank 1
665 FunSigCtxt _ -> Rank 1
666 ConArgCtxt _ -> Rank 1 -- We are given the type of the entire
667 -- constructor, hence rank 1
668 ForSigCtxt _ -> Rank 1
669 RuleSigCtxt _ -> Rank 1
671 actual_kind = typeKind ty
673 actual_kind_is_lifted = actual_kind `eqKind` liftedTypeKind
675 kind_ok = case ctxt of
676 TySynCtxt _ -> True -- Any kind will do
677 GenPatCtxt -> actual_kind_is_lifted
678 ForSigCtxt _ -> actual_kind_is_lifted
679 other -> isTypeKind actual_kind
681 ubx_tup | not gla_exts = UT_NotOk
682 | otherwise = case ctxt of
685 -- Unboxed tuples ok in function results,
686 -- but for type synonyms we allow them even at
689 addErrCtxt (checkTypeCtxt ctxt ty) $
691 -- Check that the thing has kind Type, and is lifted if necessary
692 checkTc kind_ok (kindErr actual_kind) `thenM_`
694 -- Check the internal validity of the type itself
695 check_poly_type rank ubx_tup ty
698 checkTypeCtxt ctxt ty
699 = vcat [ptext SLIT("In the type:") <+> ppr_ty ty,
700 ptext SLIT("While checking") <+> pprUserTypeCtxt ctxt ]
702 -- Hack alert. If there are no tyvars, (ppr sigma_ty) will print
703 -- something strange like {Eq k} -> k -> k, because there is no
704 -- ForAll at the top of the type. Since this is going to the user
705 -- we want it to look like a proper Haskell type even then; hence the hack
707 -- This shows up in the complaint about
709 -- op :: Eq a => a -> a
710 ppr_ty ty | null forall_tvs && notNull theta = pprTheta theta <+> ptext SLIT("=>") <+> ppr tau
713 (forall_tvs, theta, tau) = tcSplitSigmaTy ty
718 data Rank = Rank Int | Arbitrary
720 decRank :: Rank -> Rank
721 decRank Arbitrary = Arbitrary
722 decRank (Rank n) = Rank (n-1)
724 ----------------------------------------
725 data UbxTupFlag = UT_Ok | UT_NotOk
726 -- The "Ok" version means "ok if -fglasgow-exts is on"
728 ----------------------------------------
729 check_poly_type :: Rank -> UbxTupFlag -> Type -> TcM ()
730 check_poly_type (Rank 0) ubx_tup ty
731 = check_tau_type (Rank 0) ubx_tup ty
733 check_poly_type rank ubx_tup ty
735 (tvs, theta, tau) = tcSplitSigmaTy ty
737 check_valid_theta SigmaCtxt theta `thenM_`
738 check_tau_type (decRank rank) ubx_tup tau `thenM_`
739 checkFreeness tvs theta `thenM_`
740 checkAmbiguity tvs theta (tyVarsOfType tau)
742 ----------------------------------------
743 check_arg_type :: Type -> TcM ()
744 -- The sort of type that can instantiate a type variable,
745 -- or be the argument of a type constructor.
746 -- Not an unboxed tuple, not a forall.
747 -- Other unboxed types are very occasionally allowed as type
748 -- arguments depending on the kind of the type constructor
750 -- For example, we want to reject things like:
752 -- instance Ord a => Ord (forall s. T s a)
754 -- g :: T s (forall b.b)
756 -- NB: unboxed tuples can have polymorphic or unboxed args.
757 -- This happens in the workers for functions returning
758 -- product types with polymorphic components.
759 -- But not in user code.
760 -- Anyway, they are dealt with by a special case in check_tau_type
763 = check_tau_type (Rank 0) UT_NotOk ty `thenM_`
764 checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
766 ----------------------------------------
767 check_tau_type :: Rank -> UbxTupFlag -> Type -> TcM ()
768 -- Rank is allowed rank for function args
769 -- No foralls otherwise
771 check_tau_type rank ubx_tup ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty)
772 check_tau_type rank ubx_tup (SourceTy sty) = getDOpts `thenM` \ dflags ->
773 check_source_ty dflags TypeCtxt sty
774 check_tau_type rank ubx_tup (TyVarTy _) = returnM ()
775 check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
776 = check_poly_type rank UT_NotOk arg_ty `thenM_`
777 check_tau_type rank UT_Ok res_ty
779 check_tau_type rank ubx_tup (AppTy ty1 ty2)
780 = check_arg_type ty1 `thenM_` check_arg_type ty2
782 check_tau_type rank ubx_tup (NoteTy (SynNote syn) ty)
783 -- Synonym notes are built only when the synonym is
784 -- saturated (see Type.mkSynTy)
785 = doptM Opt_GlasgowExts `thenM` \ gla_exts ->
787 -- If -fglasgow-exts then don't check the 'note' part.
788 -- This allows us to instantiate a synonym defn with a
789 -- for-all type, or with a partially-applied type synonym.
790 -- e.g. type T a b = a
793 -- Here, T is partially applied, so it's illegal in H98.
794 -- But if you expand S first, then T we get just
799 -- For H98, do check the un-expanded part
800 check_tau_type rank ubx_tup syn
803 check_tau_type rank ubx_tup ty
805 check_tau_type rank ubx_tup (NoteTy other_note ty)
806 = check_tau_type rank ubx_tup ty
808 check_tau_type rank ubx_tup ty@(TyConApp tc tys)
810 = -- NB: Type.mkSynTy builds a TyConApp (not a NoteTy) for an unsaturated
811 -- synonym application, leaving it to checkValidType (i.e. right here)
813 checkTc syn_arity_ok arity_msg `thenM_`
814 mappM_ check_arg_type tys
816 | isUnboxedTupleTyCon tc
817 = doptM Opt_GlasgowExts `thenM` \ gla_exts ->
818 checkTc (ubx_tup_ok gla_exts) ubx_tup_msg `thenM_`
819 mappM_ (check_tau_type (Rank 0) UT_Ok) tys
820 -- Args are allowed to be unlifted, or
821 -- more unboxed tuples, so can't use check_arg_ty
824 = mappM_ check_arg_type tys
827 ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False }
829 syn_arity_ok = tc_arity <= n_args
830 -- It's OK to have an *over-applied* type synonym
831 -- data Tree a b = ...
832 -- type Foo a = Tree [a]
833 -- f :: Foo a b -> ...
835 tc_arity = tyConArity tc
837 arity_msg = arityErr "Type synonym" (tyConName tc) tc_arity n_args
838 ubx_tup_msg = ubxArgTyErr ty
840 ----------------------------------------
841 forAllTyErr ty = ptext SLIT("Illegal polymorphic type:") <+> ppr_ty ty
842 unliftedArgErr ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr_ty ty
843 ubxArgTyErr ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr_ty ty
844 kindErr kind = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
849 %************************************************************************
851 \subsection{Checking a theta or source type}
853 %************************************************************************
857 = ClassSCCtxt Name -- Superclasses of clas
858 | SigmaCtxt -- Context of a normal for-all type
859 | DataTyCtxt Name -- Context of a data decl
860 | TypeCtxt -- Source type in an ordinary type
861 | InstThetaCtxt -- Context of an instance decl
862 | InstHeadCtxt -- Head of an instance decl
864 pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
865 pprSourceTyCtxt SigmaCtxt = ptext SLIT("the context of a polymorphic type")
866 pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
867 pprSourceTyCtxt InstThetaCtxt = ptext SLIT("the context of an instance declaration")
868 pprSourceTyCtxt InstHeadCtxt = ptext SLIT("the head of an instance declaration")
869 pprSourceTyCtxt TypeCtxt = ptext SLIT("the context of a type")
873 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
874 checkValidTheta ctxt theta
875 = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
877 -------------------------
878 check_valid_theta ctxt []
880 check_valid_theta ctxt theta
881 = getDOpts `thenM` \ dflags ->
882 warnTc (notNull dups) (dupPredWarn dups) `thenM_`
883 -- Actually, in instance decls and type signatures,
884 -- duplicate constraints are eliminated by TcMonoType.hoistForAllTys,
885 -- so this error can only fire for the context of a class or
887 mappM_ (check_source_ty dflags ctxt) theta
889 (_,dups) = removeDups tcCmpPred theta
891 -------------------------
892 check_source_ty dflags ctxt pred@(ClassP cls tys)
893 = -- Class predicates are valid in all contexts
894 mappM_ check_arg_type tys `thenM_`
895 checkTc (arity == n_tys) arity_err `thenM_`
896 checkTc (check_class_pred_tys dflags ctxt tys)
897 (predTyVarErr pred $$ how_to_allow)
900 class_name = className cls
901 arity = classArity cls
903 arity_err = arityErr "Class" class_name arity n_tys
905 how_to_allow = case ctxt of
906 InstHeadCtxt -> empty -- Should not happen
907 InstThetaCtxt -> parens undecidableMsg
908 other -> parens (ptext SLIT("Use -fglasgow-exts to permit this"))
910 check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
911 -- Implicit parameters only allows in type
912 -- signatures; not in instance decls, superclasses etc
913 -- The reason for not allowing implicit params in instances is a bit subtle
914 -- If we allowed instance (?x::Int, Eq a) => Foo [a] where ...
915 -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
916 -- discharge all the potential usas of the ?x in e. For example, a
917 -- constraint Foo [Int] might come out of e,and applying the
918 -- instance decl would show up two uses of ?x.
920 check_source_ty dflags TypeCtxt (NType tc tys) = mappM_ check_arg_type tys
923 check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
925 -------------------------
926 check_class_pred_tys dflags ctxt tys
928 InstHeadCtxt -> True -- We check for instance-head
929 -- formation in checkValidInstHead
930 InstThetaCtxt -> undecidable_ok || all isTyVarTy tys
931 other -> gla_exts || all tyvar_head tys
933 undecidable_ok = dopt Opt_AllowUndecidableInstances dflags
934 gla_exts = dopt Opt_GlasgowExts dflags
936 -------------------------
937 tyvar_head ty -- Haskell 98 allows predicates of form
938 | tcIsTyVarTy ty = True -- C (a ty1 .. tyn)
939 | otherwise -- where a is a type variable
940 = case tcSplitAppTy_maybe ty of
941 Just (ty, _) -> tyvar_head ty
948 is ambiguous if P contains generic variables
949 (i.e. one of the Vs) that are not mentioned in tau
951 However, we need to take account of functional dependencies
952 when we speak of 'mentioned in tau'. Example:
953 class C a b | a -> b where ...
955 forall x y. (C x y) => x
956 is not ambiguous because x is mentioned and x determines y
958 NB; the ambiguity check is only used for *user* types, not for types
959 coming from inteface files. The latter can legitimately have
960 ambiguous types. Example
962 class S a where s :: a -> (Int,Int)
963 instance S Char where s _ = (1,1)
964 f:: S a => [a] -> Int -> (Int,Int)
965 f (_::[a]) x = (a*x,b)
966 where (a,b) = s (undefined::a)
968 Here the worker for f gets the type
969 fw :: forall a. S a => Int -> (# Int, Int #)
971 If the list of tv_names is empty, we have a monotype, and then we
972 don't need to check for ambiguity either, because the test can't fail
976 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
977 checkAmbiguity forall_tyvars theta tau_tyvars
978 = mappM_ complain (filter is_ambig theta)
980 complain pred = addErrTc (ambigErr pred)
981 extended_tau_vars = grow theta tau_tyvars
982 is_ambig pred = any ambig_var (varSetElems (tyVarsOfPred pred))
984 ambig_var ct_var = (ct_var `elem` forall_tyvars) &&
985 not (ct_var `elemVarSet` extended_tau_vars)
987 is_free ct_var = not (ct_var `elem` forall_tyvars)
990 = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
991 nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
992 ptext SLIT("must be reachable from the type after the '=>'"))]
995 In addition, GHC insists that at least one type variable
996 in each constraint is in V. So we disallow a type like
997 forall a. Eq b => b -> b
998 even in a scope where b is in scope.
1001 checkFreeness forall_tyvars theta
1002 = mappM_ complain (filter is_free theta)
1004 is_free pred = not (isIPPred pred)
1005 && not (any bound_var (varSetElems (tyVarsOfPred pred)))
1006 bound_var ct_var = ct_var `elem` forall_tyvars
1007 complain pred = addErrTc (freeErr pred)
1010 = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
1011 ptext SLIT("are already in scope"),
1012 nest 4 (ptext SLIT("(at least one must be universally quantified here)"))
1017 checkThetaCtxt ctxt theta
1018 = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
1019 ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
1021 badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprSourceType sty
1022 predTyVarErr pred = ptext SLIT("Non-type variables in constraint:") <+> pprPred pred
1023 dupPredWarn dups = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
1025 arityErr kind name n m
1026 = hsep [ text kind, quotes (ppr name), ptext SLIT("should have"),
1027 n_arguments <> comma, text "but has been given", int m]
1029 n_arguments | n == 0 = ptext SLIT("no arguments")
1030 | n == 1 = ptext SLIT("1 argument")
1031 | True = hsep [int n, ptext SLIT("arguments")]
1035 %************************************************************************
1037 \subsection{Validity check for TyCons}
1039 %************************************************************************
1041 checkValidTyCon is called once the mutually-recursive knot has been
1042 tied, so we can look at things freely.
1045 checkValidTyCon :: TyCon -> TcM ()
1047 | isSynTyCon tc = checkValidType (TySynCtxt name) syn_rhs
1049 = -- Check the context on the data decl
1050 checkValidTheta (DataTyCtxt name) (tyConTheta tc) `thenM_`
1052 -- Check arg types of data constructors
1053 mappM_ checkValidDataCon data_cons `thenM_`
1055 -- Check that fields with the same name share a type
1056 mappM_ check_fields groups
1060 (_, syn_rhs) = getSynTyConDefn tc
1061 data_cons = tyConDataCons tc
1063 fields = [field | con <- data_cons, field <- dataConFieldLabels con]
1064 groups = equivClasses cmp_name fields
1065 cmp_name field1 field2 = fieldLabelName field1 `compare` fieldLabelName field2
1067 check_fields fields@(first_field_label : other_fields)
1068 -- These fields all have the same name, but are from
1069 -- different constructors in the data type
1070 = -- Check that all the fields in the group have the same type
1071 -- NB: this check assumes that all the constructors of a given
1072 -- data type use the same type variables
1073 checkTc (all (tcEqType field_ty) other_tys) (fieldTypeMisMatch field_name)
1075 field_ty = fieldLabelType first_field_label
1076 field_name = fieldLabelName first_field_label
1077 other_tys = map fieldLabelType other_fields
1079 checkValidDataCon :: DataCon -> TcM ()
1080 checkValidDataCon con
1081 = checkValidType ctxt (idType (dataConWrapId con)) `thenM_`
1082 -- This checks the argument types and
1083 -- ambiguity of the existential context (if any)
1084 addErrCtxt (existentialCtxt con)
1085 (checkFreeness ex_tvs ex_theta)
1087 ctxt = ConArgCtxt (dataConName con)
1088 (_, _, ex_tvs, ex_theta, _, _) = dataConSig con
1091 fieldTypeMisMatch field_name
1092 = sep [ptext SLIT("Different constructors give different types for field"), quotes (ppr field_name)]
1094 existentialCtxt con = ptext SLIT("When checking the existential context of constructor")
1095 <+> quotes (ppr con)
1099 checkValidClass is called once the mutually-recursive knot has been
1100 tied, so we can look at things freely.
1103 checkValidClass :: Class -> TcM ()
1105 = -- CHECK ARITY 1 FOR HASKELL 1.4
1106 doptM Opt_GlasgowExts `thenM` \ gla_exts ->
1108 -- Check that the class is unary, unless GlaExs
1109 checkTc (notNull tyvars) (nullaryClassErr cls) `thenM_`
1110 checkTc (gla_exts || unary) (classArityErr cls) `thenM_`
1112 -- Check the super-classes
1113 checkValidTheta (ClassSCCtxt (className cls)) theta `thenM_`
1115 -- Check the class operations
1116 mappM_ check_op op_stuff `thenM_`
1118 -- Check that if the class has generic methods, then the
1119 -- class has only one parameter. We can't do generic
1120 -- multi-parameter type classes!
1121 checkTc (unary || no_generics) (genericMultiParamErr cls)
1124 (tyvars, theta, _, op_stuff) = classBigSig cls
1125 unary = isSingleton tyvars
1126 no_generics = null [() | (_, GenDefMeth) <- op_stuff]
1128 check_op (sel_id, dm)
1129 = checkValidTheta SigmaCtxt (tail theta) `thenM_`
1130 -- The 'tail' removes the initial (C a) from the
1131 -- class itself, leaving just the method type
1133 checkValidType (FunSigCtxt op_name) tau `thenM_`
1135 -- Check that for a generic method, the type of
1136 -- the method is sufficiently simple
1137 checkTc (dm /= GenDefMeth || validGenericMethodType op_ty)
1138 (badGenericMethodType op_name op_ty)
1140 op_name = idName sel_id
1141 op_ty = idType sel_id
1142 (_,theta,tau) = tcSplitSigmaTy op_ty
1145 = ptext SLIT("No parameters for class") <+> quotes (ppr cls)
1148 = vcat [ptext SLIT("Too many parameters for class") <+> quotes (ppr cls),
1149 parens (ptext SLIT("Use -fglasgow-exts to allow multi-parameter classes"))]
1151 genericMultiParamErr clas
1152 = ptext SLIT("The multi-parameter class") <+> quotes (ppr clas) <+>
1153 ptext SLIT("cannot have generic methods")
1155 badGenericMethodType op op_ty
1156 = hang (ptext SLIT("Generic method type is too complex"))
1157 4 (vcat [ppr op <+> dcolon <+> ppr op_ty,
1158 ptext SLIT("You can only use type variables, arrows, and tuples")])
1162 %************************************************************************
1164 \subsection{Checking for a decent instance head type}
1166 %************************************************************************
1168 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1169 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1171 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1172 flag is on, or (2)~the instance is imported (they must have been
1173 compiled elsewhere). In these cases, we let them go through anyway.
1175 We can also have instances for functions: @instance Foo (a -> b) ...@.
1178 checkValidInstHead :: Type -> TcM (Class, [TcType])
1180 checkValidInstHead ty -- Should be a source type
1181 = case tcSplitPredTy_maybe ty of {
1182 Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
1185 case getClassPredTys_maybe pred of {
1186 Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
1189 getDOpts `thenM` \ dflags ->
1190 mappM_ check_arg_type tys `thenM_`
1191 check_inst_head dflags clas tys `thenM_`
1195 check_inst_head dflags clas tys
1197 -- A user declaration of a CCallable/CReturnable instance
1198 -- must be for a "boxed primitive" type.
1199 (clas `hasKey` cCallableClassKey
1200 && not (ccallable_type first_ty))
1201 || (clas `hasKey` cReturnableClassKey
1202 && not (creturnable_type first_ty))
1203 = failWithTc (nonBoxedPrimCCallErr clas first_ty)
1205 -- If GlasgowExts then check at least one isn't a type variable
1206 | dopt Opt_GlasgowExts dflags
1207 = check_tyvars dflags clas tys
1209 -- WITH HASKELL 1.4, MUST HAVE C (T a b c)
1211 Just (tycon, arg_tys) <- tcSplitTyConApp_maybe first_ty,
1212 not (isSynTyCon tycon), -- ...but not a synonym
1213 all tcIsTyVarTy arg_tys, -- Applied to type variables
1214 equalLength (varSetElems (tyVarsOfTypes arg_tys)) arg_tys
1215 -- This last condition checks that all the type variables are distinct
1219 = failWithTc (instTypeErr (pprClassPred clas tys) head_shape_msg)
1222 (first_ty : _) = tys
1224 ccallable_type ty = isFFIArgumentTy dflags PlayRisky ty
1225 creturnable_type ty = isFFIImportResultTy dflags ty
1227 head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
1228 text "where T is not a synonym, and a,b,c are distinct type variables")
1230 check_tyvars dflags clas tys
1231 -- Check that at least one isn't a type variable
1232 -- unless -fallow-undecideable-instances
1233 | dopt Opt_AllowUndecidableInstances dflags = returnM ()
1234 | not (all tcIsTyVarTy tys) = returnM ()
1235 | otherwise = failWithTc (instTypeErr (pprClassPred clas tys) msg)
1237 msg = parens (ptext SLIT("There must be at least one non-type-variable in the instance head")
1240 undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
1244 instTypeErr pp_ty msg
1245 = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,
1248 nonBoxedPrimCCallErr clas inst_ty
1249 = hang (ptext SLIT("Unacceptable instance type for ccall-ish class"))
1250 4 (pprClassPred clas [inst_ty])