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 checkValidInstHead, instTypeErr, checkAmbiguity,
32 --------------------------------
34 zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV,
35 zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
36 zonkTcPredType, zonkTcTypeToType, zonkTcTyVarToTyVar, zonkKindEnv,
40 #include "HsVersions.h"
44 import TypeRep ( Type(..), SourceType(..), TyNote(..), -- Friend; can see representation
47 import TcType ( TcType, TcThetaType, TcTauType, TcPredType,
48 TcTyVarSet, TcKind, TcTyVar, TyVarDetails(..),
50 tcSplitPhiTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe,
51 tcSplitTyConApp_maybe, tcSplitForAllTys,
52 tcIsTyVarTy, tcSplitSigmaTy,
53 isUnLiftedType, isIPPred, isHoleTyVar,
55 mkAppTy, mkTyVarTy, mkTyVarTys,
56 tyVarsOfPred, getClassPredTys_maybe,
58 liftedTypeKind, openTypeKind, defaultKind, superKind,
59 superBoxity, liftedBoxity, typeKind,
60 tyVarsOfType, tyVarsOfTypes,
61 eqKind, isTypeKind, isAnyTypeKind,
63 isFFIArgumentTy, isFFIImportResultTy
65 import qualified Type ( splitFunTys )
66 import Subst ( Subst, mkTopTyVarSubst, substTy )
67 import Class ( Class, classArity, className )
68 import TyCon ( TyCon, mkPrimTyCon, isSynTyCon, isUnboxedTupleTyCon,
69 tyConArity, tyConName, tyConKind )
70 import PrimRep ( PrimRep(VoidRep) )
71 import Var ( TyVar, tyVarKind, tyVarName, isTyVar, mkTyVar, isMutTyVar )
74 import TcMonad -- TcType, amongst others
75 import TysWiredIn ( voidTy, listTyCon, tupleTyCon )
76 import PrelNames ( cCallableClassKey, cReturnableClassKey, hasKey )
77 import ForeignCall ( Safety(..) )
78 import FunDeps ( grow )
79 import PprType ( pprPred, pprSourceType, pprTheta, pprClassPred )
80 import Name ( Name, NamedThing(..), setNameUnique, mkSystemName,
81 mkInternalName, mkDerivedTyConOcc
84 import BasicTypes ( Boxity(Boxed) )
85 import CmdLineOpts ( dopt, DynFlag(..) )
86 import Unique ( Uniquable(..) )
87 import SrcLoc ( noSrcLoc )
88 import Util ( nOfThem, isSingleton, equalLength )
89 import ListSetOps ( removeDups )
94 %************************************************************************
96 \subsection{New type variables}
98 %************************************************************************
101 newTyVar :: Kind -> NF_TcM TcTyVar
103 = tcGetUnique `thenNF_Tc` \ uniq ->
104 tcNewMutTyVar (mkSystemName uniq FSLIT("t")) kind VanillaTv
106 newTyVarTy :: Kind -> NF_TcM TcType
108 = newTyVar kind `thenNF_Tc` \ tc_tyvar ->
109 returnNF_Tc (TyVarTy tc_tyvar)
111 newTyVarTys :: Int -> Kind -> NF_TcM [TcType]
112 newTyVarTys n kind = mapNF_Tc newTyVarTy (nOfThem n kind)
114 newKindVar :: NF_TcM TcKind
116 = tcGetUnique `thenNF_Tc` \ uniq ->
117 tcNewMutTyVar (mkSystemName uniq FSLIT("k")) superKind VanillaTv `thenNF_Tc` \ kv ->
118 returnNF_Tc (TyVarTy kv)
120 newKindVars :: Int -> NF_TcM [TcKind]
121 newKindVars n = mapNF_Tc (\ _ -> newKindVar) (nOfThem n ())
123 newBoxityVar :: NF_TcM TcKind
125 = tcGetUnique `thenNF_Tc` \ uniq ->
126 tcNewMutTyVar (mkSystemName uniq FSLIT("bx")) superBoxity VanillaTv `thenNF_Tc` \ kv ->
127 returnNF_Tc (TyVarTy kv)
131 %************************************************************************
133 \subsection{'hole' type variables}
135 %************************************************************************
138 newHoleTyVarTy :: NF_TcM TcType
139 = tcGetUnique `thenNF_Tc` \ uniq ->
140 tcNewMutTyVar (mkSystemName uniq FSLIT("h")) openTypeKind HoleTv `thenNF_Tc` \ tv ->
141 returnNF_Tc (TyVarTy tv)
143 readHoleResult :: TcType -> NF_TcM TcType
144 -- Read the answer out of a hole, constructed by newHoleTyVarTy
145 readHoleResult (TyVarTy tv)
146 = ASSERT( isHoleTyVar tv )
147 getTcTyVar tv `thenNF_Tc` \ maybe_res ->
149 Just ty -> returnNF_Tc ty
150 Nothing -> pprPanic "readHoleResult: empty" (ppr tv)
151 readHoleResult ty = pprPanic "readHoleResult: not hole" (ppr ty)
153 zapToType :: TcType -> NF_TcM TcType
154 zapToType (TyVarTy tv)
156 = getTcTyVar tv `thenNF_Tc` \ maybe_res ->
158 Nothing -> newTyVarTy openTypeKind `thenNF_Tc` \ ty ->
159 putTcTyVar tv ty `thenNF_Tc_`
161 Just ty -> returnNF_Tc ty -- No need to loop; we never
162 -- have chains of holes
164 zapToType other_ty = returnNF_Tc other_ty
167 %************************************************************************
169 \subsection{Type instantiation}
171 %************************************************************************
173 Instantiating a bunch of type variables
176 tcInstTyVars :: TyVarDetails -> [TyVar]
177 -> NF_TcM ([TcTyVar], [TcType], Subst)
179 tcInstTyVars tv_details tyvars
180 = mapNF_Tc (tcInstTyVar tv_details) tyvars `thenNF_Tc` \ tc_tyvars ->
182 tys = mkTyVarTys tc_tyvars
184 returnNF_Tc (tc_tyvars, tys, mkTopTyVarSubst tyvars tys)
185 -- Since the tyvars are freshly made,
186 -- they cannot possibly be captured by
187 -- any existing for-alls. Hence mkTopTyVarSubst
189 tcInstTyVar tv_details tyvar
190 = tcGetUnique `thenNF_Tc` \ uniq ->
192 name = setNameUnique (tyVarName tyvar) uniq
193 -- Note that we don't change the print-name
194 -- This won't confuse the type checker but there's a chance
195 -- that two different tyvars will print the same way
196 -- in an error message. -dppr-debug will show up the difference
197 -- Better watch out for this. If worst comes to worst, just
200 tcNewMutTyVar name (tyVarKind tyvar) tv_details
202 tcInstType :: TyVarDetails -> TcType -> NF_TcM ([TcTyVar], TcThetaType, TcType)
203 -- tcInstType instantiates the outer-level for-alls of a TcType with
204 -- fresh (mutable) type variables, splits off the dictionary part,
205 -- and returns the pieces.
206 tcInstType tv_details ty
207 = case tcSplitForAllTys ty of
208 ([], rho) -> -- There may be overloading despite no type variables;
209 -- (?x :: Int) => Int -> Int
211 (theta, tau) = tcSplitPhiTy rho
213 returnNF_Tc ([], theta, tau)
215 (tyvars, rho) -> tcInstTyVars tv_details tyvars `thenNF_Tc` \ (tyvars', _, tenv) ->
217 (theta, tau) = tcSplitPhiTy (substTy tenv rho)
219 returnNF_Tc (tyvars', theta, tau)
223 %************************************************************************
225 \subsection{Putting and getting mutable type variables}
227 %************************************************************************
230 putTcTyVar :: TcTyVar -> TcType -> NF_TcM TcType
231 getTcTyVar :: TcTyVar -> NF_TcM (Maybe TcType)
238 | not (isMutTyVar tyvar)
239 = pprTrace "putTcTyVar" (ppr tyvar) $
243 = ASSERT( isMutTyVar tyvar )
244 tcWriteMutTyVar tyvar (Just ty) `thenNF_Tc_`
248 Getting is more interesting. The easy thing to do is just to read, thus:
251 getTcTyVar tyvar = tcReadMutTyVar tyvar
254 But it's more fun to short out indirections on the way: If this
255 version returns a TyVar, then that TyVar is unbound. If it returns
256 any other type, then there might be bound TyVars embedded inside it.
258 We return Nothing iff the original box was unbound.
262 | not (isMutTyVar tyvar)
263 = pprTrace "getTcTyVar" (ppr tyvar) $
264 returnNF_Tc (Just (mkTyVarTy tyvar))
267 = ASSERT2( isMutTyVar tyvar, ppr tyvar )
268 tcReadMutTyVar tyvar `thenNF_Tc` \ maybe_ty ->
270 Just ty -> short_out ty `thenNF_Tc` \ ty' ->
271 tcWriteMutTyVar tyvar (Just ty') `thenNF_Tc_`
272 returnNF_Tc (Just ty')
274 Nothing -> returnNF_Tc Nothing
276 short_out :: TcType -> NF_TcM TcType
277 short_out ty@(TyVarTy tyvar)
278 | not (isMutTyVar tyvar)
282 = tcReadMutTyVar tyvar `thenNF_Tc` \ maybe_ty ->
284 Just ty' -> short_out ty' `thenNF_Tc` \ ty' ->
285 tcWriteMutTyVar tyvar (Just ty') `thenNF_Tc_`
288 other -> returnNF_Tc ty
290 short_out other_ty = returnNF_Tc other_ty
294 %************************************************************************
296 \subsection{Zonking -- the exernal interfaces}
298 %************************************************************************
300 ----------------- Type variables
303 zonkTcTyVars :: [TcTyVar] -> NF_TcM [TcType]
304 zonkTcTyVars tyvars = mapNF_Tc zonkTcTyVar tyvars
306 zonkTcTyVarsAndFV :: [TcTyVar] -> NF_TcM TcTyVarSet
307 zonkTcTyVarsAndFV tyvars = mapNF_Tc zonkTcTyVar tyvars `thenNF_Tc` \ tys ->
308 returnNF_Tc (tyVarsOfTypes tys)
310 zonkTcTyVar :: TcTyVar -> NF_TcM TcType
311 zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnNF_Tc (TyVarTy tv)) tyvar
314 ----------------- Types
317 zonkTcType :: TcType -> NF_TcM TcType
318 zonkTcType ty = zonkType (\ tv -> returnNF_Tc (TyVarTy tv)) ty
320 zonkTcTypes :: [TcType] -> NF_TcM [TcType]
321 zonkTcTypes tys = mapNF_Tc zonkTcType tys
323 zonkTcClassConstraints cts = mapNF_Tc zonk cts
324 where zonk (clas, tys)
325 = zonkTcTypes tys `thenNF_Tc` \ new_tys ->
326 returnNF_Tc (clas, new_tys)
328 zonkTcThetaType :: TcThetaType -> NF_TcM TcThetaType
329 zonkTcThetaType theta = mapNF_Tc zonkTcPredType theta
331 zonkTcPredType :: TcPredType -> NF_TcM TcPredType
332 zonkTcPredType (ClassP c ts)
333 = zonkTcTypes ts `thenNF_Tc` \ new_ts ->
334 returnNF_Tc (ClassP c new_ts)
335 zonkTcPredType (IParam n t)
336 = zonkTcType t `thenNF_Tc` \ new_t ->
337 returnNF_Tc (IParam n new_t)
340 ------------------- These ...ToType, ...ToKind versions
341 are used at the end of type checking
344 zonkKindEnv :: [(Name, TcKind)] -> NF_TcM [(Name, Kind)]
346 = mapNF_Tc zonk_it pairs
348 zonk_it (name, tc_kind) = zonkType zonk_unbound_kind_var tc_kind `thenNF_Tc` \ kind ->
349 returnNF_Tc (name, kind)
351 -- When zonking a kind, we want to
352 -- zonk a *kind* variable to (Type *)
353 -- zonk a *boxity* variable to *
354 zonk_unbound_kind_var kv | tyVarKind kv `eqKind` superKind = putTcTyVar kv liftedTypeKind
355 | tyVarKind kv `eqKind` superBoxity = putTcTyVar kv liftedBoxity
356 | otherwise = pprPanic "zonkKindEnv" (ppr kv)
358 zonkTcTypeToType :: TcType -> NF_TcM Type
359 zonkTcTypeToType ty = zonkType zonk_unbound_tyvar ty
361 -- Zonk a mutable but unbound type variable to an arbitrary type
362 -- We know it's unbound even though we don't carry an environment,
363 -- because at the binding site for a type variable we bind the
364 -- mutable tyvar to a fresh immutable one. So the mutable store
365 -- plays the role of an environment. If we come across a mutable
366 -- type variable that isn't so bound, it must be completely free.
367 zonk_unbound_tyvar tv = putTcTyVar tv (mkArbitraryType tv)
370 -- When the type checker finds a type variable with no binding,
371 -- which means it can be instantiated with an arbitrary type, it
372 -- usually instantiates it to Void. Eg.
376 -- length Void (Nil Void)
378 -- But in really obscure programs, the type variable might have
379 -- a kind other than *, so we need to invent a suitably-kinded type.
383 -- List for kind *->*
384 -- Tuple for kind *->...*->*
386 -- which deals with most cases. (Previously, it only dealt with
389 -- In the other cases, it just makes up a TyCon with a suitable
390 -- kind. If this gets into an interface file, anyone reading that
391 -- file won't understand it. This is fixable (by making the client
392 -- of the interface file make up a TyCon too) but it is tiresome and
393 -- never happens, so I am leaving it
395 mkArbitraryType :: TcTyVar -> Type
396 -- Make up an arbitrary type whose kind is the same as the tyvar.
397 -- We'll use this to instantiate the (unbound) tyvar.
399 | isAnyTypeKind kind = voidTy -- The vastly common case
400 | otherwise = TyConApp tycon []
403 (args,res) = Type.splitFunTys kind -- Kinds are simple; use Type.splitFunTys
405 tycon | kind `eqKind` tyConKind listTyCon -- *->*
406 = listTyCon -- No tuples this size
408 | all isTypeKind args && isTypeKind res
409 = tupleTyCon Boxed (length args) -- *-> ... ->*->*
412 = pprTrace "Urk! Inventing strangely-kinded void TyCon" (ppr tc_name) $
413 mkPrimTyCon tc_name kind 0 [] VoidRep
414 -- Same name as the tyvar, apart from making it start with a colon (sigh)
415 -- I dread to think what will happen if this gets out into an
416 -- interface file. Catastrophe likely. Major sigh.
418 tc_name = mkInternalName (getUnique tv) (mkDerivedTyConOcc (getOccName tv)) noSrcLoc
420 -- zonkTcTyVarToTyVar is applied to the *binding* occurrence
421 -- of a type variable, at the *end* of type checking. It changes
422 -- the *mutable* type variable into an *immutable* one.
424 -- It does this by making an immutable version of tv and binds tv to it.
425 -- Now any bound occurences of the original type variable will get
426 -- zonked to the immutable version.
428 zonkTcTyVarToTyVar :: TcTyVar -> NF_TcM TyVar
429 zonkTcTyVarToTyVar tv
431 -- Make an immutable version, defaulting
432 -- the kind to lifted if necessary
433 immut_tv = mkTyVar (tyVarName tv) (defaultKind (tyVarKind tv))
434 immut_tv_ty = mkTyVarTy immut_tv
436 zap tv = putTcTyVar tv immut_tv_ty
437 -- Bind the mutable version to the immutable one
439 -- If the type variable is mutable, then bind it to immut_tv_ty
440 -- so that all other occurrences of the tyvar will get zapped too
441 zonkTyVar zap tv `thenNF_Tc` \ ty2 ->
443 WARN( not (immut_tv_ty `tcEqType` ty2), ppr tv $$ ppr immut_tv $$ ppr ty2 )
449 %************************************************************************
451 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
453 %* For internal use only! *
455 %************************************************************************
458 -- zonkType is used for Kinds as well
460 -- For unbound, mutable tyvars, zonkType uses the function given to it
461 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
462 -- type variable and zonks the kind too
464 zonkType :: (TcTyVar -> NF_TcM Type) -- What to do with unbound mutable type variables
465 -- see zonkTcType, and zonkTcTypeToType
468 zonkType unbound_var_fn ty
471 go (TyConApp tycon tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' ->
472 returnNF_Tc (TyConApp tycon tys')
474 go (NoteTy (SynNote ty1) ty2) = go ty1 `thenNF_Tc` \ ty1' ->
475 go ty2 `thenNF_Tc` \ ty2' ->
476 returnNF_Tc (NoteTy (SynNote ty1') ty2')
478 go (NoteTy (FTVNote _) ty2) = go ty2 -- Discard free-tyvar annotations
480 go (SourceTy p) = go_pred p `thenNF_Tc` \ p' ->
481 returnNF_Tc (SourceTy p')
483 go (FunTy arg res) = go arg `thenNF_Tc` \ arg' ->
484 go res `thenNF_Tc` \ res' ->
485 returnNF_Tc (FunTy arg' res')
487 go (AppTy fun arg) = go fun `thenNF_Tc` \ fun' ->
488 go arg `thenNF_Tc` \ arg' ->
489 returnNF_Tc (mkAppTy fun' arg')
490 -- NB the mkAppTy; we might have instantiated a
491 -- type variable to a type constructor, so we need
492 -- to pull the TyConApp to the top.
494 -- The two interesting cases!
495 go (TyVarTy tyvar) = zonkTyVar unbound_var_fn tyvar
497 go (ForAllTy tyvar ty) = zonkTcTyVarToTyVar tyvar `thenNF_Tc` \ tyvar' ->
498 go ty `thenNF_Tc` \ ty' ->
499 returnNF_Tc (ForAllTy tyvar' ty')
501 go_pred (ClassP c tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' ->
502 returnNF_Tc (ClassP c tys')
503 go_pred (NType tc tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' ->
504 returnNF_Tc (NType tc tys')
505 go_pred (IParam n ty) = go ty `thenNF_Tc` \ ty' ->
506 returnNF_Tc (IParam n ty')
508 zonkTyVar :: (TcTyVar -> NF_TcM Type) -- What to do for an unbound mutable variable
509 -> TcTyVar -> NF_TcM TcType
510 zonkTyVar unbound_var_fn tyvar
511 | not (isMutTyVar tyvar) -- Not a mutable tyvar. This can happen when
512 -- zonking a forall type, when the bound type variable
513 -- needn't be mutable
514 = ASSERT( isTyVar tyvar ) -- Should not be any immutable kind vars
515 returnNF_Tc (TyVarTy tyvar)
518 = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
520 Nothing -> unbound_var_fn tyvar -- Mutable and unbound
521 Just other_ty -> zonkType unbound_var_fn other_ty -- Bound
526 %************************************************************************
528 \subsection{Checking a user type}
530 %************************************************************************
532 When dealing with a user-written type, we first translate it from an HsType
533 to a Type, performing kind checking, and then check various things that should
534 be true about it. We don't want to perform these checks at the same time
535 as the initial translation because (a) they are unnecessary for interface-file
536 types and (b) when checking a mutually recursive group of type and class decls,
537 we can't "look" at the tycons/classes yet. Also, the checks are are rather
538 diverse, and used to really mess up the other code.
540 One thing we check for is 'rank'.
542 Rank 0: monotypes (no foralls)
543 Rank 1: foralls at the front only, Rank 0 inside
544 Rank 2: foralls at the front, Rank 1 on left of fn arrow,
546 basic ::= tyvar | T basic ... basic
548 r2 ::= forall tvs. cxt => r2a
549 r2a ::= r1 -> r2a | basic
550 r1 ::= forall tvs. cxt => r0
551 r0 ::= r0 -> r0 | basic
553 Another thing is to check that type synonyms are saturated.
554 This might not necessarily show up in kind checking.
556 data T k = MkT (k Int)
562 = FunSigCtxt Name -- Function type signature
563 | ExprSigCtxt -- Expression type signature
564 | ConArgCtxt Name -- Data constructor argument
565 | TySynCtxt Name -- RHS of a type synonym decl
566 | GenPatCtxt -- Pattern in generic decl
567 -- f{| a+b |} (Inl x) = ...
568 | PatSigCtxt -- Type sig in pattern
570 | ResSigCtxt -- Result type sig
572 | ForSigCtxt Name -- Foreign inport or export signature
573 | RuleSigCtxt Name -- Signature on a forall'd variable in a RULE
575 -- Notes re TySynCtxt
576 -- We allow type synonyms that aren't types; e.g. type List = []
578 -- If the RHS mentions tyvars that aren't in scope, we'll
579 -- quantify over them:
580 -- e.g. type T = a->a
581 -- will become type T = forall a. a->a
583 -- With gla-exts that's right, but for H98 we should complain.
586 pprUserTypeCtxt (FunSigCtxt n) = ptext SLIT("the type signature for") <+> quotes (ppr n)
587 pprUserTypeCtxt ExprSigCtxt = ptext SLIT("an expression type signature")
588 pprUserTypeCtxt (ConArgCtxt c) = ptext SLIT("the type of constructor") <+> quotes (ppr c)
589 pprUserTypeCtxt (TySynCtxt c) = ptext SLIT("the RHS of a type synonym declaration") <+> quotes (ppr c)
590 pprUserTypeCtxt GenPatCtxt = ptext SLIT("the type pattern of a generic definition")
591 pprUserTypeCtxt PatSigCtxt = ptext SLIT("a pattern type signature")
592 pprUserTypeCtxt ResSigCtxt = ptext SLIT("a result type signature")
593 pprUserTypeCtxt (ForSigCtxt n) = ptext SLIT("the foreign signature for") <+> quotes (ppr n)
594 pprUserTypeCtxt (RuleSigCtxt n) = ptext SLIT("the type signature on") <+> quotes (ppr n)
598 checkValidType :: UserTypeCtxt -> Type -> TcM ()
599 -- Checks that the type is valid for the given context
600 checkValidType ctxt ty
601 = doptsTc Opt_GlasgowExts `thenNF_Tc` \ gla_exts ->
603 rank | gla_exts = Arbitrary
605 = case ctxt of -- Haskell 98
609 TySynCtxt _ -> Rank 0
610 ExprSigCtxt -> Rank 1
611 FunSigCtxt _ -> Rank 1
612 ConArgCtxt _ -> Rank 1 -- We are given the type of the entire
613 -- constructor, hence rank 1
614 ForSigCtxt _ -> Rank 1
615 RuleSigCtxt _ -> Rank 1
617 actual_kind = typeKind ty
619 actual_kind_is_lifted = actual_kind `eqKind` liftedTypeKind
621 kind_ok = case ctxt of
622 TySynCtxt _ -> True -- Any kind will do
623 GenPatCtxt -> actual_kind_is_lifted
624 ForSigCtxt _ -> actual_kind_is_lifted
625 other -> isTypeKind actual_kind
627 ubx_tup | not gla_exts = UT_NotOk
628 | otherwise = case ctxt of
631 -- Unboxed tuples ok in function results,
632 -- but for type synonyms we allow them even at
635 tcAddErrCtxt (checkTypeCtxt ctxt ty) $
637 -- Check that the thing has kind Type, and is lifted if necessary
638 checkTc kind_ok (kindErr actual_kind) `thenTc_`
640 -- Check the internal validity of the type itself
641 check_poly_type rank ubx_tup ty
644 checkTypeCtxt ctxt ty
645 = vcat [ptext SLIT("In the type:") <+> ppr_ty ty,
646 ptext SLIT("While checking") <+> pprUserTypeCtxt ctxt ]
648 -- Hack alert. If there are no tyvars, (ppr sigma_ty) will print
649 -- something strange like {Eq k} -> k -> k, because there is no
650 -- ForAll at the top of the type. Since this is going to the user
651 -- we want it to look like a proper Haskell type even then; hence the hack
653 -- This shows up in the complaint about
655 -- op :: Eq a => a -> a
656 ppr_ty ty | null forall_tvs && not (null theta) = pprTheta theta <+> ptext SLIT("=>") <+> ppr tau
659 (forall_tvs, theta, tau) = tcSplitSigmaTy ty
664 data Rank = Rank Int | Arbitrary
666 decRank :: Rank -> Rank
667 decRank Arbitrary = Arbitrary
668 decRank (Rank n) = Rank (n-1)
670 ----------------------------------------
671 data UbxTupFlag = UT_Ok | UT_NotOk
672 -- The "Ok" version means "ok if -fglasgow-exts is on"
674 ----------------------------------------
675 check_poly_type :: Rank -> UbxTupFlag -> Type -> TcM ()
676 check_poly_type (Rank 0) ubx_tup ty
677 = check_tau_type (Rank 0) ubx_tup ty
679 check_poly_type rank ubx_tup ty
681 (tvs, theta, tau) = tcSplitSigmaTy ty
683 check_valid_theta SigmaCtxt theta `thenTc_`
684 check_tau_type (decRank rank) ubx_tup tau `thenTc_`
685 checkFreeness tvs theta `thenTc_`
686 checkAmbiguity tvs theta (tyVarsOfType tau)
688 ----------------------------------------
689 check_arg_type :: Type -> TcM ()
690 -- The sort of type that can instantiate a type variable,
691 -- or be the argument of a type constructor.
692 -- Not an unboxed tuple, not a forall.
693 -- Other unboxed types are very occasionally allowed as type
694 -- arguments depending on the kind of the type constructor
696 -- For example, we want to reject things like:
698 -- instance Ord a => Ord (forall s. T s a)
700 -- g :: T s (forall b.b)
702 -- NB: unboxed tuples can have polymorphic or unboxed args.
703 -- This happens in the workers for functions returning
704 -- product types with polymorphic components.
705 -- But not in user code.
706 -- Anyway, they are dealt with by a special case in check_tau_type
709 = check_tau_type (Rank 0) UT_NotOk ty `thenTc_`
710 checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
712 ----------------------------------------
713 check_tau_type :: Rank -> UbxTupFlag -> Type -> TcM ()
714 -- Rank is allowed rank for function args
715 -- No foralls otherwise
717 check_tau_type rank ubx_tup ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty)
718 check_tau_type rank ubx_tup (SourceTy sty) = getDOptsTc `thenNF_Tc` \ dflags ->
719 check_source_ty dflags TypeCtxt sty
720 check_tau_type rank ubx_tup (TyVarTy _) = returnTc ()
721 check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
722 = check_poly_type rank UT_NotOk arg_ty `thenTc_`
723 check_tau_type rank UT_Ok res_ty
725 check_tau_type rank ubx_tup (AppTy ty1 ty2)
726 = check_arg_type ty1 `thenTc_` check_arg_type ty2
728 check_tau_type rank ubx_tup (NoteTy note ty)
729 = check_tau_type rank ubx_tup ty
730 -- Synonym notes are built only when the synonym is
731 -- saturated (see Type.mkSynTy)
732 -- Not checking the 'note' part allows us to instantiate a synonym
733 -- defn with a for-all type, or with a partially-applied type synonym,
734 -- but that seems OK too
736 check_tau_type rank ubx_tup ty@(TyConApp tc tys)
738 = -- NB: Type.mkSynTy builds a TyConApp (not a NoteTy) for an unsaturated
739 -- synonym application, leaving it to checkValidType (i.e. right here
741 checkTc syn_arity_ok arity_msg `thenTc_`
742 mapTc_ check_arg_type tys
744 | isUnboxedTupleTyCon tc
745 = doptsTc Opt_GlasgowExts `thenNF_Tc` \ gla_exts ->
746 checkTc (ubx_tup_ok gla_exts) ubx_tup_msg `thenTc_`
747 mapTc_ (check_tau_type (Rank 0) UT_Ok) tys
748 -- Args are allowed to be unlifted, or
749 -- more unboxed tuples, so can't use check_arg_ty
752 = mapTc_ check_arg_type tys
755 ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False }
757 syn_arity_ok = tc_arity <= n_args
758 -- It's OK to have an *over-applied* type synonym
759 -- data Tree a b = ...
760 -- type Foo a = Tree [a]
761 -- f :: Foo a b -> ...
763 tc_arity = tyConArity tc
765 arity_msg = arityErr "Type synonym" (tyConName tc) tc_arity n_args
766 ubx_tup_msg = ubxArgTyErr ty
768 ----------------------------------------
769 forAllTyErr ty = ptext SLIT("Illegal polymorphic type:") <+> ppr_ty ty
770 unliftedArgErr ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr_ty ty
771 ubxArgTyErr ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr_ty ty
772 kindErr kind = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
778 is ambiguous if P contains generic variables
779 (i.e. one of the Vs) that are not mentioned in tau
781 However, we need to take account of functional dependencies
782 when we speak of 'mentioned in tau'. Example:
783 class C a b | a -> b where ...
785 forall x y. (C x y) => x
786 is not ambiguous because x is mentioned and x determines y
788 NB; the ambiguity check is only used for *user* types, not for types
789 coming from inteface files. The latter can legitimately have
790 ambiguous types. Example
792 class S a where s :: a -> (Int,Int)
793 instance S Char where s _ = (1,1)
794 f:: S a => [a] -> Int -> (Int,Int)
795 f (_::[a]) x = (a*x,b)
796 where (a,b) = s (undefined::a)
798 Here the worker for f gets the type
799 fw :: forall a. S a => Int -> (# Int, Int #)
801 If the list of tv_names is empty, we have a monotype, and then we
802 don't need to check for ambiguity either, because the test can't fail
806 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
807 checkAmbiguity forall_tyvars theta tau_tyvars
808 = mapTc_ complain (filter is_ambig theta)
810 complain pred = addErrTc (ambigErr pred)
811 extended_tau_vars = grow theta tau_tyvars
812 is_ambig pred = any ambig_var (varSetElems (tyVarsOfPred pred))
814 ambig_var ct_var = (ct_var `elem` forall_tyvars) &&
815 not (ct_var `elemVarSet` extended_tau_vars)
817 is_free ct_var = not (ct_var `elem` forall_tyvars)
820 = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
821 nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
822 ptext SLIT("must be reachable from the type after the '=>'"))]
825 In addition, GHC insists that at least one type variable
826 in each constraint is in V. So we disallow a type like
827 forall a. Eq b => b -> b
828 even in a scope where b is in scope.
831 checkFreeness forall_tyvars theta
832 = mapTc_ complain (filter is_free theta)
834 is_free pred = not (isIPPred pred)
835 && not (any bound_var (varSetElems (tyVarsOfPred pred)))
836 bound_var ct_var = ct_var `elem` forall_tyvars
837 complain pred = addErrTc (freeErr pred)
840 = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
841 ptext SLIT("are already in scope"),
842 nest 4 (ptext SLIT("At least one must be universally quantified here"))
847 %************************************************************************
849 \subsection{Checking a theta or source type}
851 %************************************************************************
855 = ClassSCCtxt Name -- Superclasses of clas
856 | SigmaCtxt -- Context of a normal for-all type
857 | DataTyCtxt Name -- Context of a data decl
858 | TypeCtxt -- Source type in an ordinary type
859 | InstThetaCtxt -- Context of an instance decl
860 | InstHeadCtxt -- Head of an instance decl
862 pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
863 pprSourceTyCtxt SigmaCtxt = ptext SLIT("the context of a polymorphic type")
864 pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
865 pprSourceTyCtxt InstThetaCtxt = ptext SLIT("the context of an instance declaration")
866 pprSourceTyCtxt InstHeadCtxt = ptext SLIT("the head of an instance declaration")
867 pprSourceTyCtxt TypeCtxt = ptext SLIT("the context of a type")
871 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
872 checkValidTheta ctxt theta
873 = tcAddErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
875 -------------------------
876 check_valid_theta ctxt []
878 check_valid_theta ctxt theta
879 = getDOptsTc `thenNF_Tc` \ dflags ->
880 warnTc (not (null dups)) (dupPredWarn dups) `thenNF_Tc_`
881 mapTc_ (check_source_ty dflags ctxt) theta
883 (_,dups) = removeDups tcCmpPred theta
885 -------------------------
886 check_source_ty dflags ctxt pred@(ClassP cls tys)
887 = -- Class predicates are valid in all contexts
888 mapTc_ check_arg_type tys `thenTc_`
889 checkTc (arity == n_tys) arity_err `thenTc_`
890 checkTc (all tyvar_head tys || arby_preds_ok)
891 (predTyVarErr pred $$ how_to_allow)
894 class_name = className cls
895 arity = classArity cls
897 arity_err = arityErr "Class" class_name arity n_tys
899 arby_preds_ok = case ctxt of
900 InstHeadCtxt -> True -- We check for instance-head formation
901 -- in checkValidInstHead
902 InstThetaCtxt -> dopt Opt_AllowUndecidableInstances dflags
903 other -> dopt Opt_GlasgowExts dflags
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) = mapTc_ check_arg_type tys
923 check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
925 -------------------------
926 tyvar_head ty -- Haskell 98 allows predicates of form
927 | tcIsTyVarTy ty = True -- C (a ty1 .. tyn)
928 | otherwise -- where a is a type variable
929 = case tcSplitAppTy_maybe ty of
930 Just (ty, _) -> tyvar_head ty
935 badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprSourceType sty
936 predTyVarErr pred = ptext SLIT("Non-type variables in constraint:") <+> pprPred pred
937 dupPredWarn dups = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
939 checkThetaCtxt ctxt theta
940 = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
941 ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
945 %************************************************************************
947 \subsection{Checking for a decent instance head type}
949 %************************************************************************
951 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
952 it must normally look like: @instance Foo (Tycon a b c ...) ...@
954 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
955 flag is on, or (2)~the instance is imported (they must have been
956 compiled elsewhere). In these cases, we let them go through anyway.
958 We can also have instances for functions: @instance Foo (a -> b) ...@.
961 checkValidInstHead :: Type -> TcM (Class, [TcType])
963 checkValidInstHead ty -- Should be a source type
964 = case tcSplitPredTy_maybe ty of {
965 Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
968 case getClassPredTys_maybe pred of {
969 Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
972 getDOptsTc `thenNF_Tc` \ dflags ->
973 mapTc_ check_arg_type tys `thenTc_`
974 check_inst_head dflags clas tys `thenTc_`
978 check_inst_head dflags clas tys
980 -- A user declaration of a CCallable/CReturnable instance
981 -- must be for a "boxed primitive" type.
982 (clas `hasKey` cCallableClassKey
983 && not (ccallable_type first_ty))
984 || (clas `hasKey` cReturnableClassKey
985 && not (creturnable_type first_ty))
986 = failWithTc (nonBoxedPrimCCallErr clas first_ty)
988 -- If GlasgowExts then check at least one isn't a type variable
989 | dopt Opt_GlasgowExts dflags
990 = check_tyvars dflags clas tys
992 -- WITH HASKELL 1.4, MUST HAVE C (T a b c)
994 Just (tycon, arg_tys) <- tcSplitTyConApp_maybe first_ty,
995 not (isSynTyCon tycon), -- ...but not a synonym
996 all tcIsTyVarTy arg_tys, -- Applied to type variables
997 equalLength (varSetElems (tyVarsOfTypes arg_tys)) arg_tys
998 -- This last condition checks that all the type variables are distinct
1002 = failWithTc (instTypeErr (pprClassPred clas tys) head_shape_msg)
1005 (first_ty : _) = tys
1007 ccallable_type ty = isFFIArgumentTy dflags PlayRisky ty
1008 creturnable_type ty = isFFIImportResultTy dflags ty
1010 head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
1011 text "where T is not a synonym, and a,b,c are distinct type variables")
1013 check_tyvars dflags clas tys
1014 -- Check that at least one isn't a type variable
1015 -- unless -fallow-undecideable-instances
1016 | dopt Opt_AllowUndecidableInstances dflags = returnTc ()
1017 | not (all tcIsTyVarTy tys) = returnTc ()
1018 | otherwise = failWithTc (instTypeErr (pprClassPred clas tys) msg)
1020 msg = parens (ptext SLIT("There must be at least one non-type-variable in the instance head")
1023 undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
1027 instTypeErr pp_ty msg
1028 = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,
1031 nonBoxedPrimCCallErr clas inst_ty
1032 = hang (ptext SLIT("Unacceptable instance type for ccall-ish class"))
1033 4 (pprClassPred clas [inst_ty])