2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 \section{Monadic type operations}
6 This module contains monadic operations over types that contain mutable type variables
10 TcTyVar, TcKind, TcType, TcTauType, TcThetaType, TcTyVarSet,
12 --------------------------------
13 -- Creating new mutable type variables
14 newTyVar, newHoleTyVarTy,
15 newTyVarTy, -- Kind -> NF_TcM TcType
16 newTyVarTys, -- Int -> Kind -> NF_TcM [TcType]
17 newKindVar, newKindVars, newBoxityVar,
18 putTcTyVar, getTcTyVar,
20 --------------------------------
22 tcInstTyVar, tcInstTyVars,
23 tcInstSigTyVars, tcInstType,
26 --------------------------------
27 -- Checking type validity
28 Rank, UserTypeCtxt(..), checkValidType, pprUserTypeCtxt,
29 SourceTyCtxt(..), checkValidTheta,
30 checkValidInstHead, instTypeErr,
32 --------------------------------
34 zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkTcSigTyVars,
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 tcSplitRhoTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe,
51 tcSplitTyConApp_maybe, tcSplitForAllTys,
52 tcGetTyVar, tcIsTyVarTy, tcSplitSigmaTy,
53 isUnLiftedType, isIPPred,
55 mkAppTy, mkTyVarTy, mkTyVarTys,
56 tyVarsOfPred, getClassPredTys_maybe,
58 liftedTypeKind, openTypeKind, defaultKind, superKind,
59 superBoxity, liftedBoxity, typeKind,
60 tyVarsOfType, tyVarsOfTypes,
63 isFFIArgumentTy, isFFIImportResultTy
65 import Subst ( Subst, mkTopTyVarSubst, substTy )
66 import Class ( classArity, className )
67 import TyCon ( TyCon, mkPrimTyCon, isSynTyCon, isUnboxedTupleTyCon,
68 tyConArity, tyConName )
69 import PrimRep ( PrimRep(VoidRep) )
70 import Var ( TyVar, tyVarKind, tyVarName, isTyVar, mkTyVar, isMutTyVar )
73 import TcMonad -- TcType, amongst others
74 import TysWiredIn ( voidTy )
75 import PrelNames ( cCallableClassKey, cReturnableClassKey, hasKey )
76 import ForeignCall ( Safety(..) )
77 import FunDeps ( grow )
78 import PprType ( pprPred, pprSourceType, pprTheta, pprClassPred )
79 import Name ( Name, NamedThing(..), setNameUnique, mkSysLocalName,
80 mkLocalName, mkDerivedTyConOcc
83 import CmdLineOpts ( dopt, DynFlag(..) )
84 import Unique ( Uniquable(..) )
85 import SrcLoc ( noSrcLoc )
86 import Util ( nOfThem, isSingleton, equalLength )
87 import ListSetOps ( removeDups )
92 %************************************************************************
94 \subsection{New type variables}
96 %************************************************************************
99 newTyVar :: Kind -> NF_TcM TcTyVar
101 = tcGetUnique `thenNF_Tc` \ uniq ->
102 tcNewMutTyVar (mkSysLocalName uniq SLIT("t")) kind VanillaTv
104 newTyVarTy :: Kind -> NF_TcM TcType
106 = newTyVar kind `thenNF_Tc` \ tc_tyvar ->
107 returnNF_Tc (TyVarTy tc_tyvar)
109 newHoleTyVarTy :: NF_TcM TcType
110 = tcGetUnique `thenNF_Tc` \ uniq ->
111 tcNewMutTyVar (mkSysLocalName uniq SLIT("h")) openTypeKind HoleTv `thenNF_Tc` \ tv ->
112 returnNF_Tc (TyVarTy tv)
114 newTyVarTys :: Int -> Kind -> NF_TcM [TcType]
115 newTyVarTys n kind = mapNF_Tc newTyVarTy (nOfThem n kind)
117 newKindVar :: NF_TcM TcKind
119 = tcGetUnique `thenNF_Tc` \ uniq ->
120 tcNewMutTyVar (mkSysLocalName uniq SLIT("k")) superKind VanillaTv `thenNF_Tc` \ kv ->
121 returnNF_Tc (TyVarTy kv)
123 newKindVars :: Int -> NF_TcM [TcKind]
124 newKindVars n = mapNF_Tc (\ _ -> newKindVar) (nOfThem n ())
126 newBoxityVar :: NF_TcM TcKind
128 = tcGetUnique `thenNF_Tc` \ uniq ->
129 tcNewMutTyVar (mkSysLocalName uniq SLIT("bx")) superBoxity VanillaTv `thenNF_Tc` \ kv ->
130 returnNF_Tc (TyVarTy kv)
134 %************************************************************************
136 \subsection{Type instantiation}
138 %************************************************************************
140 I don't understand why this is needed
141 An old comments says "No need for tcSplitForAllTyM because a type
142 variable can't be instantiated to a for-all type"
143 But the same is true of rho types!
146 tcSplitRhoTyM :: TcType -> NF_TcM (TcThetaType, TcType)
150 -- A type variable is never instantiated to a dictionary type,
151 -- so we don't need to do a tcReadVar on the "arg".
152 go syn_t (FunTy arg res) ts = case tcSplitPredTy_maybe arg of
153 Just pair -> go res res (pair:ts)
154 Nothing -> returnNF_Tc (reverse ts, syn_t)
155 go syn_t (NoteTy n t) ts = go syn_t t ts
156 go syn_t (TyVarTy tv) ts = getTcTyVar tv `thenNF_Tc` \ maybe_ty ->
158 Just ty | not (tcIsTyVarTy ty) -> go syn_t ty ts
159 other -> returnNF_Tc (reverse ts, syn_t)
160 go syn_t (UsageTy _ t) ts = go syn_t t ts
161 go syn_t t ts = returnNF_Tc (reverse ts, syn_t)
165 %************************************************************************
167 \subsection{Type instantiation}
169 %************************************************************************
171 Instantiating a bunch of type variables
174 tcInstTyVars :: [TyVar]
175 -> NF_TcM ([TcTyVar], [TcType], Subst)
178 = mapNF_Tc tcInstTyVar tyvars `thenNF_Tc` \ tc_tyvars ->
180 tys = mkTyVarTys tc_tyvars
182 returnNF_Tc (tc_tyvars, tys, mkTopTyVarSubst tyvars tys)
183 -- Since the tyvars are freshly made,
184 -- they cannot possibly be captured by
185 -- any existing for-alls. Hence mkTopTyVarSubst
188 = tcGetUnique `thenNF_Tc` \ uniq ->
190 name = setNameUnique (tyVarName tyvar) uniq
191 -- Note that we don't change the print-name
192 -- This won't confuse the type checker but there's a chance
193 -- that two different tyvars will print the same way
194 -- in an error message. -dppr-debug will show up the difference
195 -- Better watch out for this. If worst comes to worst, just
196 -- use mkSysLocalName.
198 tcNewMutTyVar name (tyVarKind tyvar) VanillaTv
200 tcInstSigTyVars :: TyVarDetails -> [TyVar] -> NF_TcM [TcTyVar]
201 tcInstSigTyVars details tyvars -- Very similar to tcInstTyVar
202 = tcGetUniques `thenNF_Tc` \ uniqs ->
203 listTc [ ASSERT( not (kind `eqKind` openTypeKind) ) -- Shouldn't happen
204 tcNewMutTyVar name kind details
205 | (tyvar, uniq) <- tyvars `zip` uniqs,
206 let name = setNameUnique (tyVarName tyvar) uniq,
207 let kind = tyVarKind tyvar
211 @tcInstType@ instantiates the outer-level for-alls of a TcType with
212 fresh type variables, splits off the dictionary part, and returns the results.
215 tcInstType :: TcType -> NF_TcM ([TcTyVar], TcThetaType, TcType)
217 = case tcSplitForAllTys ty of
218 ([], rho) -> -- There may be overloading but no type variables;
219 -- (?x :: Int) => Int -> Int
221 (theta, tau) = tcSplitRhoTy rho -- Used to be tcSplitRhoTyM
223 returnNF_Tc ([], theta, tau)
225 (tyvars, rho) -> tcInstTyVars tyvars `thenNF_Tc` \ (tyvars', _, tenv) ->
227 (theta, tau) = tcSplitRhoTy (substTy tenv rho) -- Used to be tcSplitRhoTyM
229 returnNF_Tc (tyvars', theta, tau)
234 %************************************************************************
236 \subsection{Putting and getting mutable type variables}
238 %************************************************************************
241 putTcTyVar :: TcTyVar -> TcType -> NF_TcM TcType
242 getTcTyVar :: TcTyVar -> NF_TcM (Maybe TcType)
249 | not (isMutTyVar tyvar)
250 = pprTrace "putTcTyVar" (ppr tyvar) $
254 = ASSERT( isMutTyVar tyvar )
255 UASSERT2( not (isUTy ty), ppr tyvar <+> ppr ty )
256 tcWriteMutTyVar tyvar (Just ty) `thenNF_Tc_`
260 Getting is more interesting. The easy thing to do is just to read, thus:
263 getTcTyVar tyvar = tcReadMutTyVar tyvar
266 But it's more fun to short out indirections on the way: If this
267 version returns a TyVar, then that TyVar is unbound. If it returns
268 any other type, then there might be bound TyVars embedded inside it.
270 We return Nothing iff the original box was unbound.
274 | not (isMutTyVar tyvar)
275 = pprTrace "getTcTyVar" (ppr tyvar) $
276 returnNF_Tc (Just (mkTyVarTy tyvar))
279 = ASSERT2( isMutTyVar tyvar, ppr tyvar )
280 tcReadMutTyVar tyvar `thenNF_Tc` \ maybe_ty ->
282 Just ty -> short_out ty `thenNF_Tc` \ ty' ->
283 tcWriteMutTyVar tyvar (Just ty') `thenNF_Tc_`
284 returnNF_Tc (Just ty')
286 Nothing -> returnNF_Tc Nothing
288 short_out :: TcType -> NF_TcM TcType
289 short_out ty@(TyVarTy tyvar)
290 | not (isMutTyVar tyvar)
294 = tcReadMutTyVar tyvar `thenNF_Tc` \ maybe_ty ->
296 Just ty' -> short_out ty' `thenNF_Tc` \ ty' ->
297 tcWriteMutTyVar tyvar (Just ty') `thenNF_Tc_`
300 other -> returnNF_Tc ty
302 short_out other_ty = returnNF_Tc other_ty
306 %************************************************************************
308 \subsection{Zonking -- the exernal interfaces}
310 %************************************************************************
312 ----------------- Type variables
315 zonkTcTyVars :: [TcTyVar] -> NF_TcM [TcType]
316 zonkTcTyVars tyvars = mapNF_Tc zonkTcTyVar tyvars
318 zonkTcTyVarsAndFV :: [TcTyVar] -> NF_TcM TcTyVarSet
319 zonkTcTyVarsAndFV tyvars = mapNF_Tc zonkTcTyVar tyvars `thenNF_Tc` \ tys ->
320 returnNF_Tc (tyVarsOfTypes tys)
322 zonkTcTyVar :: TcTyVar -> NF_TcM TcType
323 zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnNF_Tc (TyVarTy tv)) tyvar
325 zonkTcSigTyVars :: [TcTyVar] -> NF_TcM [TcTyVar]
326 -- This guy is to zonk the tyvars we're about to feed into tcSimplify
327 -- Usually this job is done by checkSigTyVars, but in a couple of places
328 -- that is overkill, so we use this simpler chap
329 zonkTcSigTyVars tyvars
330 = zonkTcTyVars tyvars `thenNF_Tc` \ tys ->
331 returnNF_Tc (map (tcGetTyVar "zonkTcSigTyVars") tys)
334 ----------------- Types
337 zonkTcType :: TcType -> NF_TcM TcType
338 zonkTcType ty = zonkType (\ tv -> returnNF_Tc (TyVarTy tv)) ty
340 zonkTcTypes :: [TcType] -> NF_TcM [TcType]
341 zonkTcTypes tys = mapNF_Tc zonkTcType tys
343 zonkTcClassConstraints cts = mapNF_Tc zonk cts
344 where zonk (clas, tys)
345 = zonkTcTypes tys `thenNF_Tc` \ new_tys ->
346 returnNF_Tc (clas, new_tys)
348 zonkTcThetaType :: TcThetaType -> NF_TcM TcThetaType
349 zonkTcThetaType theta = mapNF_Tc zonkTcPredType theta
351 zonkTcPredType :: TcPredType -> NF_TcM TcPredType
352 zonkTcPredType (ClassP c ts)
353 = zonkTcTypes ts `thenNF_Tc` \ new_ts ->
354 returnNF_Tc (ClassP c new_ts)
355 zonkTcPredType (IParam n t)
356 = zonkTcType t `thenNF_Tc` \ new_t ->
357 returnNF_Tc (IParam n new_t)
360 ------------------- These ...ToType, ...ToKind versions
361 are used at the end of type checking
364 zonkKindEnv :: [(Name, TcKind)] -> NF_TcM [(Name, Kind)]
366 = mapNF_Tc zonk_it pairs
368 zonk_it (name, tc_kind) = zonkType zonk_unbound_kind_var tc_kind `thenNF_Tc` \ kind ->
369 returnNF_Tc (name, 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 -> NF_TcM Type
379 zonkTcTypeToType ty = zonkType zonk_unbound_tyvar ty
381 -- Zonk a mutable but unbound type variable to
382 -- Void if it has kind Lifted
384 -- We know it's unbound even though we don't carry an environment,
385 -- because at the binding site for a type variable we bind the
386 -- mutable tyvar to a fresh immutable one. So the mutable store
387 -- plays the role of an environment. If we come across a mutable
388 -- type variable that isn't so bound, it must be completely free.
389 zonk_unbound_tyvar tv
390 | kind `eqKind` liftedTypeKind || kind `eqKind` openTypeKind
391 = putTcTyVar tv voidTy -- Just to avoid creating a new tycon in
392 -- this vastly common case
394 = putTcTyVar tv (TyConApp (mk_void_tycon tv kind) [])
398 mk_void_tycon tv kind -- Make a new TyCon with the same kind as the
399 -- type variable tv. Same name too, apart from
400 -- making it start with a colon (sigh)
401 -- I dread to think what will happen if this gets out into an
402 -- interface file. Catastrophe likely. Major sigh.
403 = pprTrace "Urk! Inventing strangely-kinded void TyCon" (ppr tc_name) $
404 mkPrimTyCon tc_name kind 0 [] VoidRep
406 tc_name = mkLocalName (getUnique tv) (mkDerivedTyConOcc (getOccName tv)) noSrcLoc
408 -- zonkTcTyVarToTyVar is applied to the *binding* occurrence
409 -- of a type variable, at the *end* of type checking. It changes
410 -- the *mutable* type variable into an *immutable* one.
412 -- It does this by making an immutable version of tv and binds tv to it.
413 -- Now any bound occurences of the original type variable will get
414 -- zonked to the immutable version.
416 zonkTcTyVarToTyVar :: TcTyVar -> NF_TcM TyVar
417 zonkTcTyVarToTyVar tv
419 -- Make an immutable version, defaulting
420 -- the kind to lifted if necessary
421 immut_tv = mkTyVar (tyVarName tv) (defaultKind (tyVarKind tv))
422 immut_tv_ty = mkTyVarTy immut_tv
424 zap tv = putTcTyVar tv immut_tv_ty
425 -- Bind the mutable version to the immutable one
427 -- If the type variable is mutable, then bind it to immut_tv_ty
428 -- so that all other occurrences of the tyvar will get zapped too
429 zonkTyVar zap tv `thenNF_Tc` \ ty2 ->
431 WARN( not (immut_tv_ty `tcEqType` ty2), ppr tv $$ ppr immut_tv $$ ppr ty2 )
437 %************************************************************************
439 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
441 %* For internal use only! *
443 %************************************************************************
446 -- zonkType is used for Kinds as well
448 -- For unbound, mutable tyvars, zonkType uses the function given to it
449 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
450 -- type variable and zonks the kind too
452 zonkType :: (TcTyVar -> NF_TcM Type) -- What to do with unbound mutable type variables
453 -- see zonkTcType, and zonkTcTypeToType
456 zonkType unbound_var_fn ty
459 go (TyConApp tycon tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' ->
460 returnNF_Tc (TyConApp tycon tys')
462 go (NoteTy (SynNote ty1) ty2) = go ty1 `thenNF_Tc` \ ty1' ->
463 go ty2 `thenNF_Tc` \ ty2' ->
464 returnNF_Tc (NoteTy (SynNote ty1') ty2')
466 go (NoteTy (FTVNote _) ty2) = go ty2 -- Discard free-tyvar annotations
468 go (SourceTy p) = go_pred p `thenNF_Tc` \ p' ->
469 returnNF_Tc (SourceTy p')
471 go (FunTy arg res) = go arg `thenNF_Tc` \ arg' ->
472 go res `thenNF_Tc` \ res' ->
473 returnNF_Tc (FunTy arg' res')
475 go (AppTy fun arg) = go fun `thenNF_Tc` \ fun' ->
476 go arg `thenNF_Tc` \ arg' ->
477 returnNF_Tc (mkAppTy fun' arg')
479 go (UsageTy u ty) = go u `thenNF_Tc` \ u' ->
480 go ty `thenNF_Tc` \ ty' ->
481 returnNF_Tc (UsageTy u' ty')
483 -- The two interesting cases!
484 go (TyVarTy tyvar) = zonkTyVar unbound_var_fn tyvar
486 go (ForAllTy tyvar ty) = zonkTcTyVarToTyVar tyvar `thenNF_Tc` \ tyvar' ->
487 go ty `thenNF_Tc` \ ty' ->
488 returnNF_Tc (ForAllTy tyvar' ty')
490 go_pred (ClassP c tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' ->
491 returnNF_Tc (ClassP c tys')
492 go_pred (NType tc tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' ->
493 returnNF_Tc (NType tc tys')
494 go_pred (IParam n ty) = go ty `thenNF_Tc` \ ty' ->
495 returnNF_Tc (IParam n ty')
497 zonkTyVar :: (TcTyVar -> NF_TcM Type) -- What to do for an unbound mutable variable
498 -> TcTyVar -> NF_TcM TcType
499 zonkTyVar unbound_var_fn tyvar
500 | not (isMutTyVar tyvar) -- Not a mutable tyvar. This can happen when
501 -- zonking a forall type, when the bound type variable
502 -- needn't be mutable
503 = ASSERT( isTyVar tyvar ) -- Should not be any immutable kind vars
504 returnNF_Tc (TyVarTy tyvar)
507 = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
509 Nothing -> unbound_var_fn tyvar -- Mutable and unbound
510 Just other_ty -> zonkType unbound_var_fn other_ty -- Bound
515 %************************************************************************
517 \subsection{Checking a user type}
519 %************************************************************************
521 When dealing with a user-written type, we first translate it from an HsType
522 to a Type, performing kind checking, and then check various things that should
523 be true about it. We don't want to perform these checks at the same time
524 as the initial translation because (a) they are unnecessary for interface-file
525 types and (b) when checking a mutually recursive group of type and class decls,
526 we can't "look" at the tycons/classes yet. Also, the checks are are rather
527 diverse, and used to really mess up the other code.
529 One thing we check for is 'rank'.
531 Rank 0: monotypes (no foralls)
532 Rank 1: foralls at the front only, Rank 0 inside
533 Rank 2: foralls at the front, Rank 1 on left of fn arrow,
535 basic ::= tyvar | T basic ... basic
537 r2 ::= forall tvs. cxt => r2a
538 r2a ::= r1 -> r2a | basic
539 r1 ::= forall tvs. cxt => r0
540 r0 ::= r0 -> r0 | basic
542 Another thing is to check that type synonyms are saturated.
543 This might not necessarily show up in kind checking.
545 data T k = MkT (k Int)
551 = FunSigCtxt Name -- Function type signature
552 | ExprSigCtxt -- Expression type signature
553 | ConArgCtxt Name -- Data constructor argument
554 | TySynCtxt Name -- RHS of a type synonym decl
555 | GenPatCtxt -- Pattern in generic decl
556 -- f{| a+b |} (Inl x) = ...
557 | PatSigCtxt -- Type sig in pattern
559 | ResSigCtxt -- Result type sig
561 | ForSigCtxt Name -- Foreign inport or export signature
562 | RuleSigCtxt Name -- Signature on a forall'd variable in a RULE
564 -- Notes re TySynCtxt
565 -- We allow type synonyms that aren't types; e.g. type List = []
567 -- If the RHS mentions tyvars that aren't in scope, we'll
568 -- quantify over them:
569 -- e.g. type T = a->a
570 -- will become type T = forall a. a->a
572 -- With gla-exts that's right, but for H98 we should complain.
575 pprUserTypeCtxt (FunSigCtxt n) = ptext SLIT("the type signature for") <+> quotes (ppr n)
576 pprUserTypeCtxt ExprSigCtxt = ptext SLIT("an expression type signature")
577 pprUserTypeCtxt (ConArgCtxt c) = ptext SLIT("the type of constructor") <+> quotes (ppr c)
578 pprUserTypeCtxt (TySynCtxt c) = ptext SLIT("the RHS of a type synonym declaration") <+> quotes (ppr c)
579 pprUserTypeCtxt GenPatCtxt = ptext SLIT("the type pattern of a generic definition")
580 pprUserTypeCtxt PatSigCtxt = ptext SLIT("a pattern type signature")
581 pprUserTypeCtxt ResSigCtxt = ptext SLIT("a result type signature")
582 pprUserTypeCtxt (ForSigCtxt n) = ptext SLIT("the foreign signature for") <+> quotes (ppr n)
583 pprUserTypeCtxt (RuleSigCtxt n) = ptext SLIT("the type signature on") <+> quotes (ppr n)
587 checkValidType :: UserTypeCtxt -> Type -> TcM ()
588 -- Checks that the type is valid for the given context
589 checkValidType ctxt ty
590 = doptsTc Opt_GlasgowExts `thenNF_Tc` \ gla_exts ->
592 rank | gla_exts = Arbitrary
594 = case ctxt of -- Haskell 98
598 TySynCtxt _ -> Rank 0
599 ExprSigCtxt -> Rank 1
600 FunSigCtxt _ -> Rank 1
601 ConArgCtxt _ -> Rank 1 -- We are given the type of the entire
602 -- constructor, hence rank 1
603 ForSigCtxt _ -> Rank 1
604 RuleSigCtxt _ -> Rank 1
606 actual_kind = typeKind ty
608 actual_kind_is_lifted = actual_kind `eqKind` liftedTypeKind
610 kind_ok = case ctxt of
611 TySynCtxt _ -> True -- Any kind will do
612 GenPatCtxt -> actual_kind_is_lifted
613 ForSigCtxt _ -> actual_kind_is_lifted
614 other -> isTypeKind actual_kind
616 tcAddErrCtxt (checkTypeCtxt ctxt ty) $
618 -- Check that the thing has kind Type, and is lifted if necessary
619 checkTc kind_ok (kindErr actual_kind) `thenTc_`
621 -- Check the internal validity of the type itself
622 check_poly_type rank ty
625 checkTypeCtxt ctxt ty
626 = vcat [ptext SLIT("In the type:") <+> ppr_ty ty,
627 ptext SLIT("While checking") <+> pprUserTypeCtxt ctxt ]
629 -- Hack alert. If there are no tyvars, (ppr sigma_ty) will print
630 -- something strange like {Eq k} -> k -> k, because there is no
631 -- ForAll at the top of the type. Since this is going to the user
632 -- we want it to look like a proper Haskell type even then; hence the hack
634 -- This shows up in the complaint about
636 -- op :: Eq a => a -> a
637 ppr_ty ty | null forall_tvs && not (null theta) = pprTheta theta <+> ptext SLIT("=>") <+> ppr tau
640 (forall_tvs, theta, tau) = tcSplitSigmaTy ty
645 data Rank = Rank Int | Arbitrary
647 decRank :: Rank -> Rank
648 decRank Arbitrary = Arbitrary
649 decRank (Rank n) = Rank (n-1)
651 check_poly_type :: Rank -> Type -> TcM ()
652 check_poly_type (Rank 0) ty
653 = check_tau_type (Rank 0) False ty
655 check_poly_type rank ty
657 (tvs, theta, tau) = tcSplitSigmaTy ty
659 check_valid_theta SigmaCtxt theta `thenTc_`
660 check_tau_type (decRank rank) False tau `thenTc_`
661 checkAmbiguity tvs theta tau
663 ----------------------------------------
664 check_arg_type :: Type -> TcM ()
665 -- The sort of type that can instantiate a type variable,
666 -- or be the argument of a type constructor.
667 -- Not an unboxed tuple, not a forall.
668 -- Other unboxed types are very occasionally allowed as type
669 -- arguments depending on the kind of the type constructor
671 -- For example, we want to reject things like:
673 -- instance Ord a => Ord (forall s. T s a)
675 -- g :: T s (forall b.b)
677 -- NB: unboxed tuples can have polymorphic or unboxed args.
678 -- This happens in the workers for functions returning
679 -- product types with polymorphic components.
680 -- But not in user code
682 -- Question: what about nested unboxed tuples?
683 -- Currently rejected.
685 = check_tau_type (Rank 0) False ty `thenTc_`
686 checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
688 ----------------------------------------
689 check_tau_type :: Rank -> Bool -> Type -> TcM ()
690 -- Rank is allowed rank for function args
691 -- No foralls otherwise
692 -- Bool is True iff unboxed tuple are allowed here
694 check_tau_type rank ubx_tup_ok ty@(UsageTy _ _) = failWithTc (usageTyErr ty)
695 check_tau_type rank ubx_tup_ok ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty)
696 check_tau_type rank ubx_tup_ok (SourceTy sty) = getDOptsTc `thenNF_Tc` \ dflags ->
697 check_source_ty dflags TypeCtxt sty
698 check_tau_type rank ubx_tup_ok (TyVarTy _) = returnTc ()
699 check_tau_type rank ubx_tup_ok ty@(FunTy arg_ty res_ty)
700 = check_poly_type rank arg_ty `thenTc_`
701 check_tau_type rank True res_ty
703 check_tau_type rank ubx_tup_ok (AppTy ty1 ty2)
704 = check_arg_type ty1 `thenTc_` check_arg_type ty2
706 check_tau_type rank ubx_tup_ok (NoteTy note ty)
707 = check_note note `thenTc_` check_tau_type rank ubx_tup_ok ty
709 check_tau_type rank ubx_tup_ok ty@(TyConApp tc tys)
711 = checkTc syn_arity_ok arity_msg `thenTc_`
712 mapTc_ check_arg_type tys
714 | isUnboxedTupleTyCon tc
715 = checkTc ubx_tup_ok ubx_tup_msg `thenTc_`
716 mapTc_ (check_tau_type (Rank 0) True) tys -- Args are allowed to be unlifted, or
717 -- more unboxed tuples, so can't use check_arg_ty
720 = mapTc_ check_arg_type tys
723 syn_arity_ok = tc_arity <= n_args
724 -- It's OK to have an *over-applied* type synonym
725 -- data Tree a b = ...
726 -- type Foo a = Tree [a]
727 -- f :: Foo a b -> ...
729 tc_arity = tyConArity tc
731 arity_msg = arityErr "Type synonym" (tyConName tc) tc_arity n_args
732 ubx_tup_msg = ubxArgTyErr ty
734 ----------------------------------------
735 check_note (FTVNote _) = returnTc ()
736 check_note (SynNote ty) = check_tau_type (Rank 0) False ty
742 is ambiguous if P contains generic variables
743 (i.e. one of the Vs) that are not mentioned in tau
745 However, we need to take account of functional dependencies
746 when we speak of 'mentioned in tau'. Example:
747 class C a b | a -> b where ...
749 forall x y. (C x y) => x
750 is not ambiguous because x is mentioned and x determines y
752 NOTE: In addition, GHC insists that at least one type variable
753 in each constraint is in V. So we disallow a type like
754 forall a. Eq b => b -> b
755 even in a scope where b is in scope.
756 This is the is_free test below.
758 NB; the ambiguity check is only used for *user* types, not for types
759 coming from inteface files. The latter can legitimately have
760 ambiguous types. Example
762 class S a where s :: a -> (Int,Int)
763 instance S Char where s _ = (1,1)
764 f:: S a => [a] -> Int -> (Int,Int)
765 f (_::[a]) x = (a*x,b)
766 where (a,b) = s (undefined::a)
768 Here the worker for f gets the type
769 fw :: forall a. S a => Int -> (# Int, Int #)
771 If the list of tv_names is empty, we have a monotype, and then we
772 don't need to check for ambiguity either, because the test can't fail
776 checkAmbiguity :: [TyVar] -> ThetaType -> Type -> TcM ()
777 checkAmbiguity forall_tyvars theta tau
778 = mapTc_ check_pred theta `thenTc_`
781 tau_vars = tyVarsOfType tau
782 extended_tau_vars = grow theta tau_vars
784 is_ambig ct_var = (ct_var `elem` forall_tyvars) &&
785 not (ct_var `elemVarSet` extended_tau_vars)
786 is_free ct_var = not (ct_var `elem` forall_tyvars)
788 check_pred pred = checkTc (not any_ambig) (ambigErr pred) `thenTc_`
789 checkTc (isIPPred pred || not all_free) (freeErr pred)
791 ct_vars = varSetElems (tyVarsOfPred pred)
792 all_free = all is_free ct_vars
793 any_ambig = any is_ambig ct_vars
798 = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
799 nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
800 ptext SLIT("must be reachable from the type after the '=>'"))]
804 = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
805 ptext SLIT("are already in scope"),
806 nest 4 (ptext SLIT("At least one must be universally quantified here"))
809 forAllTyErr ty = ptext SLIT("Illegal polymorphic type:") <+> ppr_ty ty
810 usageTyErr ty = ptext SLIT("Illegal usage type:") <+> ppr_ty ty
811 unliftedArgErr ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr_ty ty
812 ubxArgTyErr ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr_ty ty
813 kindErr kind = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
816 %************************************************************************
818 \subsection{Checking a theta or source type}
820 %************************************************************************
824 = ClassSCCtxt Name -- Superclasses of clas
825 | SigmaCtxt -- Context of a normal for-all type
826 | DataTyCtxt Name -- Context of a data decl
827 | TypeCtxt -- Source type in an ordinary type
828 | InstThetaCtxt -- Context of an instance decl
829 | InstHeadCtxt -- Head of an instance decl
831 pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
832 pprSourceTyCtxt SigmaCtxt = ptext SLIT("the context of a polymorphic type")
833 pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
834 pprSourceTyCtxt InstThetaCtxt = ptext SLIT("the context of an instance declaration")
835 pprSourceTyCtxt InstHeadCtxt = ptext SLIT("the head of an instance declaration")
836 pprSourceTyCtxt TypeCtxt = ptext SLIT("the context of a type")
840 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
841 checkValidTheta ctxt theta
842 = tcAddErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
844 -------------------------
845 check_valid_theta ctxt []
847 check_valid_theta ctxt theta
848 = getDOptsTc `thenNF_Tc` \ dflags ->
849 warnTc (not (null dups)) (dupPredWarn dups) `thenNF_Tc_`
850 mapTc_ (check_source_ty dflags ctxt) theta
852 (_,dups) = removeDups tcCmpPred theta
854 -------------------------
855 check_source_ty dflags ctxt pred@(ClassP cls tys)
856 = -- Class predicates are valid in all contexts
857 mapTc_ check_arg_type tys `thenTc_`
858 checkTc (arity == n_tys) arity_err `thenTc_`
859 checkTc (all tyvar_head tys || arby_preds_ok) (predTyVarErr pred)
862 class_name = className cls
863 arity = classArity cls
865 arity_err = arityErr "Class" class_name arity n_tys
867 arby_preds_ok = case ctxt of
868 InstHeadCtxt -> True -- We check for instance-head formation
869 -- in checkValidInstHead
870 InstThetaCtxt -> dopt Opt_AllowUndecidableInstances dflags
871 other -> dopt Opt_GlasgowExts dflags
873 check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
874 -- Implicit parameters only allows in type
875 -- signatures; not in instance decls, superclasses etc
876 -- The reason for not allowing implicit params in instances is a bit subtle
877 -- If we allowed instance (?x::Int, Eq a) => Foo [a] where ...
878 -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
879 -- discharge all the potential usas of the ?x in e. For example, a
880 -- constraint Foo [Int] might come out of e,and applying the
881 -- instance decl would show up two uses of ?x.
883 check_source_ty dflags TypeCtxt (NType tc tys) = mapTc_ check_arg_type tys
886 check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
888 -------------------------
889 tyvar_head ty -- Haskell 98 allows predicates of form
890 | tcIsTyVarTy ty = True -- C (a ty1 .. tyn)
891 | otherwise -- where a is a type variable
892 = case tcSplitAppTy_maybe ty of
893 Just (ty, _) -> tyvar_head ty
898 badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprSourceType sty
899 predTyVarErr pred = ptext SLIT("Non-type variables in constraint:") <+> pprPred pred
900 dupPredWarn dups = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
902 checkThetaCtxt ctxt theta
903 = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
904 ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
908 %************************************************************************
910 \subsection{Checking for a decent instance head type}
912 %************************************************************************
914 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
915 it must normally look like: @instance Foo (Tycon a b c ...) ...@
917 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
918 flag is on, or (2)~the instance is imported (they must have been
919 compiled elsewhere). In these cases, we let them go through anyway.
921 We can also have instances for functions: @instance Foo (a -> b) ...@.
924 checkValidInstHead :: Type -> TcM ()
926 checkValidInstHead ty -- Should be a source type
927 = case tcSplitPredTy_maybe ty of {
928 Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
931 case getClassPredTys_maybe pred of {
932 Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
935 getDOptsTc `thenNF_Tc` \ dflags ->
936 mapTc_ check_arg_type tys `thenTc_`
937 check_inst_head dflags clas tys
940 check_inst_head dflags clas tys
942 -- A user declaration of a CCallable/CReturnable instance
943 -- must be for a "boxed primitive" type.
944 (clas `hasKey` cCallableClassKey
945 && not (ccallable_type first_ty))
946 || (clas `hasKey` cReturnableClassKey
947 && not (creturnable_type first_ty))
948 = failWithTc (nonBoxedPrimCCallErr clas first_ty)
950 -- If GlasgowExts then check at least one isn't a type variable
951 | dopt Opt_GlasgowExts dflags
952 = check_tyvars dflags clas tys
954 -- WITH HASKELL 1.4, MUST HAVE C (T a b c)
956 Just (tycon, arg_tys) <- tcSplitTyConApp_maybe first_ty,
957 not (isSynTyCon tycon), -- ...but not a synonym
958 all tcIsTyVarTy arg_tys, -- Applied to type variables
959 equalLength (varSetElems (tyVarsOfTypes arg_tys)) arg_tys
960 -- This last condition checks that all the type variables are distinct
964 = failWithTc (instTypeErr (pprClassPred clas tys) head_shape_msg)
969 ccallable_type ty = isFFIArgumentTy dflags PlayRisky ty
970 creturnable_type ty = isFFIImportResultTy dflags ty
972 head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
973 text "where T is not a synonym, and a,b,c are distinct type variables")
975 check_tyvars dflags clas tys
976 -- Check that at least one isn't a type variable
977 -- unless -fallow-undecideable-instances
978 | dopt Opt_AllowUndecidableInstances dflags = returnTc ()
979 | not (all tcIsTyVarTy tys) = returnTc ()
980 | otherwise = failWithTc (instTypeErr (pprClassPred clas tys) msg)
982 msg = parens (ptext SLIT("There must be at least one non-type-variable in the instance head")
983 $$ ptext SLIT("Use -fallow-undecidable-instances to lift this restriction"))
987 instTypeErr pp_ty msg
988 = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,
991 nonBoxedPrimCCallErr clas inst_ty
992 = hang (ptext SLIT("Unacceptable instance type for ccall-ish class"))
993 4 (pprClassPred clas [inst_ty])