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, tcInstSigType,
26 --------------------------------
27 -- Checking type validity
28 Rank, UserTypeCtxt(..), checkValidType, pprUserTypeCtxt,
29 SourceTyCtxt(..), checkValidTheta,
30 checkValidInstHead, instTypeErr, checkAmbiguity,
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 ( 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)
232 tcInstSigType :: TyVarDetails -> Type -> NF_TcM ([TcTyVar], TcThetaType, TcType)
233 -- Very similar to tcInstSigType, but uses signature type variables
234 -- Also, somewhat arbitrarily, don't deal with the monomorphic case so efficiently
235 tcInstSigType tv_details poly_ty
237 (tyvars, rho) = tcSplitForAllTys poly_ty
239 tcInstSigTyVars tv_details tyvars `thenNF_Tc` \ tyvars' ->
240 -- Make *signature* type variables
243 tyvar_tys' = mkTyVarTys tyvars'
244 rho' = substTy (mkTopTyVarSubst tyvars tyvar_tys') rho
245 -- mkTopTyVarSubst because the tyvars' are fresh
247 (theta', tau') = tcSplitRhoTy rho'
248 -- This splitRhoTy tries hard to make sure that tau' is a type synonym
249 -- wherever possible, which can improve interface files.
251 returnNF_Tc (tyvars', theta', tau')
256 %************************************************************************
258 \subsection{Putting and getting mutable type variables}
260 %************************************************************************
263 putTcTyVar :: TcTyVar -> TcType -> NF_TcM TcType
264 getTcTyVar :: TcTyVar -> NF_TcM (Maybe TcType)
271 | not (isMutTyVar tyvar)
272 = pprTrace "putTcTyVar" (ppr tyvar) $
276 = ASSERT( isMutTyVar tyvar )
277 UASSERT2( not (isUTy ty), ppr tyvar <+> ppr ty )
278 tcWriteMutTyVar tyvar (Just ty) `thenNF_Tc_`
282 Getting is more interesting. The easy thing to do is just to read, thus:
285 getTcTyVar tyvar = tcReadMutTyVar tyvar
288 But it's more fun to short out indirections on the way: If this
289 version returns a TyVar, then that TyVar is unbound. If it returns
290 any other type, then there might be bound TyVars embedded inside it.
292 We return Nothing iff the original box was unbound.
296 | not (isMutTyVar tyvar)
297 = pprTrace "getTcTyVar" (ppr tyvar) $
298 returnNF_Tc (Just (mkTyVarTy tyvar))
301 = ASSERT2( isMutTyVar tyvar, ppr tyvar )
302 tcReadMutTyVar tyvar `thenNF_Tc` \ maybe_ty ->
304 Just ty -> short_out ty `thenNF_Tc` \ ty' ->
305 tcWriteMutTyVar tyvar (Just ty') `thenNF_Tc_`
306 returnNF_Tc (Just ty')
308 Nothing -> returnNF_Tc Nothing
310 short_out :: TcType -> NF_TcM TcType
311 short_out ty@(TyVarTy tyvar)
312 | not (isMutTyVar tyvar)
316 = tcReadMutTyVar tyvar `thenNF_Tc` \ maybe_ty ->
318 Just ty' -> short_out ty' `thenNF_Tc` \ ty' ->
319 tcWriteMutTyVar tyvar (Just ty') `thenNF_Tc_`
322 other -> returnNF_Tc ty
324 short_out other_ty = returnNF_Tc other_ty
328 %************************************************************************
330 \subsection{Zonking -- the exernal interfaces}
332 %************************************************************************
334 ----------------- Type variables
337 zonkTcTyVars :: [TcTyVar] -> NF_TcM [TcType]
338 zonkTcTyVars tyvars = mapNF_Tc zonkTcTyVar tyvars
340 zonkTcTyVarsAndFV :: [TcTyVar] -> NF_TcM TcTyVarSet
341 zonkTcTyVarsAndFV tyvars = mapNF_Tc zonkTcTyVar tyvars `thenNF_Tc` \ tys ->
342 returnNF_Tc (tyVarsOfTypes tys)
344 zonkTcTyVar :: TcTyVar -> NF_TcM TcType
345 zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnNF_Tc (TyVarTy tv)) tyvar
347 zonkTcSigTyVars :: [TcTyVar] -> NF_TcM [TcTyVar]
348 -- This guy is to zonk the tyvars we're about to feed into tcSimplify
349 -- Usually this job is done by checkSigTyVars, but in a couple of places
350 -- that is overkill, so we use this simpler chap
351 zonkTcSigTyVars tyvars
352 = zonkTcTyVars tyvars `thenNF_Tc` \ tys ->
353 returnNF_Tc (map (tcGetTyVar "zonkTcSigTyVars") tys)
356 ----------------- Types
359 zonkTcType :: TcType -> NF_TcM TcType
360 zonkTcType ty = zonkType (\ tv -> returnNF_Tc (TyVarTy tv)) ty
362 zonkTcTypes :: [TcType] -> NF_TcM [TcType]
363 zonkTcTypes tys = mapNF_Tc zonkTcType tys
365 zonkTcClassConstraints cts = mapNF_Tc zonk cts
366 where zonk (clas, tys)
367 = zonkTcTypes tys `thenNF_Tc` \ new_tys ->
368 returnNF_Tc (clas, new_tys)
370 zonkTcThetaType :: TcThetaType -> NF_TcM TcThetaType
371 zonkTcThetaType theta = mapNF_Tc zonkTcPredType theta
373 zonkTcPredType :: TcPredType -> NF_TcM TcPredType
374 zonkTcPredType (ClassP c ts)
375 = zonkTcTypes ts `thenNF_Tc` \ new_ts ->
376 returnNF_Tc (ClassP c new_ts)
377 zonkTcPredType (IParam n t)
378 = zonkTcType t `thenNF_Tc` \ new_t ->
379 returnNF_Tc (IParam n new_t)
382 ------------------- These ...ToType, ...ToKind versions
383 are used at the end of type checking
386 zonkKindEnv :: [(Name, TcKind)] -> NF_TcM [(Name, Kind)]
388 = mapNF_Tc zonk_it pairs
390 zonk_it (name, tc_kind) = zonkType zonk_unbound_kind_var tc_kind `thenNF_Tc` \ kind ->
391 returnNF_Tc (name, kind)
393 -- When zonking a kind, we want to
394 -- zonk a *kind* variable to (Type *)
395 -- zonk a *boxity* variable to *
396 zonk_unbound_kind_var kv | tyVarKind kv `eqKind` superKind = putTcTyVar kv liftedTypeKind
397 | tyVarKind kv `eqKind` superBoxity = putTcTyVar kv liftedBoxity
398 | otherwise = pprPanic "zonkKindEnv" (ppr kv)
400 zonkTcTypeToType :: TcType -> NF_TcM Type
401 zonkTcTypeToType ty = zonkType zonk_unbound_tyvar ty
403 -- Zonk a mutable but unbound type variable to
404 -- Void if it has kind Lifted
406 -- We know it's unbound even though we don't carry an environment,
407 -- because at the binding site for a type variable we bind the
408 -- mutable tyvar to a fresh immutable one. So the mutable store
409 -- plays the role of an environment. If we come across a mutable
410 -- type variable that isn't so bound, it must be completely free.
411 zonk_unbound_tyvar tv
412 | kind `eqKind` liftedTypeKind || kind `eqKind` openTypeKind
413 = putTcTyVar tv voidTy -- Just to avoid creating a new tycon in
414 -- this vastly common case
416 = putTcTyVar tv (TyConApp (mk_void_tycon tv kind) [])
420 mk_void_tycon tv kind -- Make a new TyCon with the same kind as the
421 -- type variable tv. Same name too, apart from
422 -- making it start with a colon (sigh)
423 -- I dread to think what will happen if this gets out into an
424 -- interface file. Catastrophe likely. Major sigh.
425 = pprTrace "Urk! Inventing strangely-kinded void TyCon" (ppr tc_name) $
426 mkPrimTyCon tc_name kind 0 [] VoidRep
428 tc_name = mkLocalName (getUnique tv) (mkDerivedTyConOcc (getOccName tv)) noSrcLoc
430 -- zonkTcTyVarToTyVar is applied to the *binding* occurrence
431 -- of a type variable, at the *end* of type checking. It changes
432 -- the *mutable* type variable into an *immutable* one.
434 -- It does this by making an immutable version of tv and binds tv to it.
435 -- Now any bound occurences of the original type variable will get
436 -- zonked to the immutable version.
438 zonkTcTyVarToTyVar :: TcTyVar -> NF_TcM TyVar
439 zonkTcTyVarToTyVar tv
441 -- Make an immutable version, defaulting
442 -- the kind to lifted if necessary
443 immut_tv = mkTyVar (tyVarName tv) (defaultKind (tyVarKind tv))
444 immut_tv_ty = mkTyVarTy immut_tv
446 zap tv = putTcTyVar tv immut_tv_ty
447 -- Bind the mutable version to the immutable one
449 -- If the type variable is mutable, then bind it to immut_tv_ty
450 -- so that all other occurrences of the tyvar will get zapped too
451 zonkTyVar zap tv `thenNF_Tc` \ ty2 ->
453 WARN( not (immut_tv_ty `tcEqType` ty2), ppr tv $$ ppr immut_tv $$ ppr ty2 )
459 %************************************************************************
461 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
463 %* For internal use only! *
465 %************************************************************************
468 -- zonkType is used for Kinds as well
470 -- For unbound, mutable tyvars, zonkType uses the function given to it
471 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
472 -- type variable and zonks the kind too
474 zonkType :: (TcTyVar -> NF_TcM Type) -- What to do with unbound mutable type variables
475 -- see zonkTcType, and zonkTcTypeToType
478 zonkType unbound_var_fn ty
481 go (TyConApp tycon tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' ->
482 returnNF_Tc (TyConApp tycon tys')
484 go (NoteTy (SynNote ty1) ty2) = go ty1 `thenNF_Tc` \ ty1' ->
485 go ty2 `thenNF_Tc` \ ty2' ->
486 returnNF_Tc (NoteTy (SynNote ty1') ty2')
488 go (NoteTy (FTVNote _) ty2) = go ty2 -- Discard free-tyvar annotations
490 go (SourceTy p) = go_pred p `thenNF_Tc` \ p' ->
491 returnNF_Tc (SourceTy p')
493 go (FunTy arg res) = go arg `thenNF_Tc` \ arg' ->
494 go res `thenNF_Tc` \ res' ->
495 returnNF_Tc (FunTy arg' res')
497 go (AppTy fun arg) = go fun `thenNF_Tc` \ fun' ->
498 go arg `thenNF_Tc` \ arg' ->
499 returnNF_Tc (mkAppTy fun' arg')
501 go (UsageTy u ty) = go u `thenNF_Tc` \ u' ->
502 go ty `thenNF_Tc` \ ty' ->
503 returnNF_Tc (UsageTy u' ty')
505 -- The two interesting cases!
506 go (TyVarTy tyvar) = zonkTyVar unbound_var_fn tyvar
508 go (ForAllTy tyvar ty) = zonkTcTyVarToTyVar tyvar `thenNF_Tc` \ tyvar' ->
509 go ty `thenNF_Tc` \ ty' ->
510 returnNF_Tc (ForAllTy tyvar' ty')
512 go_pred (ClassP c tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' ->
513 returnNF_Tc (ClassP c tys')
514 go_pred (NType tc tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' ->
515 returnNF_Tc (NType tc tys')
516 go_pred (IParam n ty) = go ty `thenNF_Tc` \ ty' ->
517 returnNF_Tc (IParam n ty')
519 zonkTyVar :: (TcTyVar -> NF_TcM Type) -- What to do for an unbound mutable variable
520 -> TcTyVar -> NF_TcM TcType
521 zonkTyVar unbound_var_fn tyvar
522 | not (isMutTyVar tyvar) -- Not a mutable tyvar. This can happen when
523 -- zonking a forall type, when the bound type variable
524 -- needn't be mutable
525 = ASSERT( isTyVar tyvar ) -- Should not be any immutable kind vars
526 returnNF_Tc (TyVarTy tyvar)
529 = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
531 Nothing -> unbound_var_fn tyvar -- Mutable and unbound
532 Just other_ty -> zonkType unbound_var_fn other_ty -- Bound
537 %************************************************************************
539 \subsection{Checking a user type}
541 %************************************************************************
543 When dealing with a user-written type, we first translate it from an HsType
544 to a Type, performing kind checking, and then check various things that should
545 be true about it. We don't want to perform these checks at the same time
546 as the initial translation because (a) they are unnecessary for interface-file
547 types and (b) when checking a mutually recursive group of type and class decls,
548 we can't "look" at the tycons/classes yet. Also, the checks are are rather
549 diverse, and used to really mess up the other code.
551 One thing we check for is 'rank'.
553 Rank 0: monotypes (no foralls)
554 Rank 1: foralls at the front only, Rank 0 inside
555 Rank 2: foralls at the front, Rank 1 on left of fn arrow,
557 basic ::= tyvar | T basic ... basic
559 r2 ::= forall tvs. cxt => r2a
560 r2a ::= r1 -> r2a | basic
561 r1 ::= forall tvs. cxt => r0
562 r0 ::= r0 -> r0 | basic
564 Another thing is to check that type synonyms are saturated.
565 This might not necessarily show up in kind checking.
567 data T k = MkT (k Int)
573 = FunSigCtxt Name -- Function type signature
574 | ExprSigCtxt -- Expression type signature
575 | ConArgCtxt Name -- Data constructor argument
576 | TySynCtxt Name -- RHS of a type synonym decl
577 | GenPatCtxt -- Pattern in generic decl
578 -- f{| a+b |} (Inl x) = ...
579 | PatSigCtxt -- Type sig in pattern
581 | ResSigCtxt -- Result type sig
583 | ForSigCtxt Name -- Foreign inport or export signature
584 | RuleSigCtxt Name -- Signature on a forall'd variable in a RULE
586 -- Notes re TySynCtxt
587 -- We allow type synonyms that aren't types; e.g. type List = []
589 -- If the RHS mentions tyvars that aren't in scope, we'll
590 -- quantify over them:
591 -- e.g. type T = a->a
592 -- will become type T = forall a. a->a
594 -- With gla-exts that's right, but for H98 we should complain.
597 pprUserTypeCtxt (FunSigCtxt n) = ptext SLIT("the type signature for") <+> quotes (ppr n)
598 pprUserTypeCtxt ExprSigCtxt = ptext SLIT("an expression type signature")
599 pprUserTypeCtxt (ConArgCtxt c) = ptext SLIT("the type of constructor") <+> quotes (ppr c)
600 pprUserTypeCtxt (TySynCtxt c) = ptext SLIT("the RHS of a type synonym declaration") <+> quotes (ppr c)
601 pprUserTypeCtxt GenPatCtxt = ptext SLIT("the type pattern of a generic definition")
602 pprUserTypeCtxt PatSigCtxt = ptext SLIT("a pattern type signature")
603 pprUserTypeCtxt ResSigCtxt = ptext SLIT("a result type signature")
604 pprUserTypeCtxt (ForSigCtxt n) = ptext SLIT("the foreign signature for") <+> quotes (ppr n)
605 pprUserTypeCtxt (RuleSigCtxt n) = ptext SLIT("the type signature on") <+> quotes (ppr n)
609 checkValidType :: UserTypeCtxt -> Type -> TcM ()
610 -- Checks that the type is valid for the given context
611 checkValidType ctxt ty
612 = doptsTc Opt_GlasgowExts `thenNF_Tc` \ gla_exts ->
614 rank | gla_exts = Arbitrary
616 = case ctxt of -- Haskell 98
620 TySynCtxt _ -> Rank 0
621 ExprSigCtxt -> Rank 1
622 FunSigCtxt _ -> Rank 1
623 ConArgCtxt _ -> Rank 1 -- We are given the type of the entire
624 -- constructor, hence rank 1
625 ForSigCtxt _ -> Rank 1
626 RuleSigCtxt _ -> Rank 1
628 actual_kind = typeKind ty
630 actual_kind_is_lifted = actual_kind `eqKind` liftedTypeKind
632 kind_ok = case ctxt of
633 TySynCtxt _ -> True -- Any kind will do
634 GenPatCtxt -> actual_kind_is_lifted
635 ForSigCtxt _ -> actual_kind_is_lifted
636 other -> isTypeKind actual_kind
638 tcAddErrCtxt (checkTypeCtxt ctxt ty) $
640 -- Check that the thing has kind Type, and is lifted if necessary
641 checkTc kind_ok (kindErr actual_kind) `thenTc_`
643 -- Check the internal validity of the type itself
644 check_poly_type rank ty
647 checkTypeCtxt ctxt ty
648 = vcat [ptext SLIT("In the type:") <+> ppr_ty ty,
649 ptext SLIT("While checking") <+> pprUserTypeCtxt ctxt ]
651 -- Hack alert. If there are no tyvars, (ppr sigma_ty) will print
652 -- something strange like {Eq k} -> k -> k, because there is no
653 -- ForAll at the top of the type. Since this is going to the user
654 -- we want it to look like a proper Haskell type even then; hence the hack
656 -- This shows up in the complaint about
658 -- op :: Eq a => a -> a
659 ppr_ty ty | null forall_tvs && not (null theta) = pprTheta theta <+> ptext SLIT("=>") <+> ppr tau
662 (forall_tvs, theta, tau) = tcSplitSigmaTy ty
667 data Rank = Rank Int | Arbitrary
669 decRank :: Rank -> Rank
670 decRank Arbitrary = Arbitrary
671 decRank (Rank n) = Rank (n-1)
673 check_poly_type :: Rank -> Type -> TcM ()
674 check_poly_type (Rank 0) ty
675 = check_tau_type (Rank 0) False ty
677 check_poly_type rank ty
679 (tvs, theta, tau) = tcSplitSigmaTy ty
681 check_valid_theta SigmaCtxt theta `thenTc_`
682 check_tau_type (decRank rank) False tau `thenTc_`
683 checkFreeness tvs theta `thenTc_`
684 checkAmbiguity tvs theta (tyVarsOfType tau)
686 ----------------------------------------
687 check_arg_type :: Type -> TcM ()
688 -- The sort of type that can instantiate a type variable,
689 -- or be the argument of a type constructor.
690 -- Not an unboxed tuple, not a forall.
691 -- Other unboxed types are very occasionally allowed as type
692 -- arguments depending on the kind of the type constructor
694 -- For example, we want to reject things like:
696 -- instance Ord a => Ord (forall s. T s a)
698 -- g :: T s (forall b.b)
700 -- NB: unboxed tuples can have polymorphic or unboxed args.
701 -- This happens in the workers for functions returning
702 -- product types with polymorphic components.
703 -- But not in user code
705 -- Question: what about nested unboxed tuples?
706 -- Currently rejected.
708 = check_tau_type (Rank 0) False ty `thenTc_`
709 checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
711 ----------------------------------------
712 check_tau_type :: Rank -> Bool -> Type -> TcM ()
713 -- Rank is allowed rank for function args
714 -- No foralls otherwise
715 -- Bool is True iff unboxed tuple are allowed here
717 check_tau_type rank ubx_tup_ok ty@(UsageTy _ _) = failWithTc (usageTyErr ty)
718 check_tau_type rank ubx_tup_ok ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty)
719 check_tau_type rank ubx_tup_ok (SourceTy sty) = getDOptsTc `thenNF_Tc` \ dflags ->
720 check_source_ty dflags TypeCtxt sty
721 check_tau_type rank ubx_tup_ok (TyVarTy _) = returnTc ()
722 check_tau_type rank ubx_tup_ok ty@(FunTy arg_ty res_ty)
723 = check_poly_type rank arg_ty `thenTc_`
724 check_tau_type rank True res_ty
726 check_tau_type rank ubx_tup_ok (AppTy ty1 ty2)
727 = check_arg_type ty1 `thenTc_` check_arg_type ty2
729 check_tau_type rank ubx_tup_ok (NoteTy note ty)
730 = check_note note `thenTc_` check_tau_type rank ubx_tup_ok ty
732 check_tau_type rank ubx_tup_ok ty@(TyConApp tc tys)
734 = checkTc syn_arity_ok arity_msg `thenTc_`
735 mapTc_ check_arg_type tys
737 | isUnboxedTupleTyCon tc
738 = checkTc ubx_tup_ok ubx_tup_msg `thenTc_`
739 mapTc_ (check_tau_type (Rank 0) True) tys -- Args are allowed to be unlifted, or
740 -- more unboxed tuples, so can't use check_arg_ty
743 = mapTc_ check_arg_type tys
746 syn_arity_ok = tc_arity <= n_args
747 -- It's OK to have an *over-applied* type synonym
748 -- data Tree a b = ...
749 -- type Foo a = Tree [a]
750 -- f :: Foo a b -> ...
752 tc_arity = tyConArity tc
754 arity_msg = arityErr "Type synonym" (tyConName tc) tc_arity n_args
755 ubx_tup_msg = ubxArgTyErr ty
757 ----------------------------------------
758 check_note (FTVNote _) = returnTc ()
759 check_note (SynNote ty) = check_tau_type (Rank 0) False ty
761 ----------------------------------------
762 forAllTyErr ty = ptext SLIT("Illegal polymorphic type:") <+> ppr_ty ty
763 usageTyErr ty = ptext SLIT("Illegal usage type:") <+> ppr_ty ty
764 unliftedArgErr ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr_ty ty
765 ubxArgTyErr ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr_ty ty
766 kindErr kind = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
772 is ambiguous if P contains generic variables
773 (i.e. one of the Vs) that are not mentioned in tau
775 However, we need to take account of functional dependencies
776 when we speak of 'mentioned in tau'. Example:
777 class C a b | a -> b where ...
779 forall x y. (C x y) => x
780 is not ambiguous because x is mentioned and x determines y
782 NB; the ambiguity check is only used for *user* types, not for types
783 coming from inteface files. The latter can legitimately have
784 ambiguous types. Example
786 class S a where s :: a -> (Int,Int)
787 instance S Char where s _ = (1,1)
788 f:: S a => [a] -> Int -> (Int,Int)
789 f (_::[a]) x = (a*x,b)
790 where (a,b) = s (undefined::a)
792 Here the worker for f gets the type
793 fw :: forall a. S a => Int -> (# Int, Int #)
795 If the list of tv_names is empty, we have a monotype, and then we
796 don't need to check for ambiguity either, because the test can't fail
800 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
801 checkAmbiguity forall_tyvars theta tau_tyvars
802 = mapTc_ complain (filter is_ambig theta)
804 complain pred = addErrTc (ambigErr pred)
805 extended_tau_vars = grow theta tau_tyvars
806 is_ambig pred = any ambig_var (varSetElems (tyVarsOfPred pred))
808 ambig_var ct_var = (ct_var `elem` forall_tyvars) &&
809 not (ct_var `elemVarSet` extended_tau_vars)
811 is_free ct_var = not (ct_var `elem` forall_tyvars)
814 = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
815 nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
816 ptext SLIT("must be reachable from the type after the '=>'"))]
819 In addition, GHC insists that at least one type variable
820 in each constraint is in V. So we disallow a type like
821 forall a. Eq b => b -> b
822 even in a scope where b is in scope.
825 checkFreeness forall_tyvars theta
826 = mapTc_ complain (filter is_free theta)
828 is_free pred = not (isIPPred pred)
829 && not (any bound_var (varSetElems (tyVarsOfPred pred)))
830 bound_var ct_var = ct_var `elem` forall_tyvars
831 complain pred = addErrTc (freeErr pred)
834 = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
835 ptext SLIT("are already in scope"),
836 nest 4 (ptext SLIT("At least one must be universally quantified here"))
841 %************************************************************************
843 \subsection{Checking a theta or source type}
845 %************************************************************************
849 = ClassSCCtxt Name -- Superclasses of clas
850 | SigmaCtxt -- Context of a normal for-all type
851 | DataTyCtxt Name -- Context of a data decl
852 | TypeCtxt -- Source type in an ordinary type
853 | InstThetaCtxt -- Context of an instance decl
854 | InstHeadCtxt -- Head of an instance decl
856 pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
857 pprSourceTyCtxt SigmaCtxt = ptext SLIT("the context of a polymorphic type")
858 pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
859 pprSourceTyCtxt InstThetaCtxt = ptext SLIT("the context of an instance declaration")
860 pprSourceTyCtxt InstHeadCtxt = ptext SLIT("the head of an instance declaration")
861 pprSourceTyCtxt TypeCtxt = ptext SLIT("the context of a type")
865 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
866 checkValidTheta ctxt theta
867 = tcAddErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
869 -------------------------
870 check_valid_theta ctxt []
872 check_valid_theta ctxt theta
873 = getDOptsTc `thenNF_Tc` \ dflags ->
874 warnTc (not (null dups)) (dupPredWarn dups) `thenNF_Tc_`
875 mapTc_ (check_source_ty dflags ctxt) theta
877 (_,dups) = removeDups tcCmpPred theta
879 -------------------------
880 check_source_ty dflags ctxt pred@(ClassP cls tys)
881 = -- Class predicates are valid in all contexts
882 mapTc_ check_arg_type tys `thenTc_`
883 checkTc (arity == n_tys) arity_err `thenTc_`
884 checkTc (all tyvar_head tys || arby_preds_ok)
885 (predTyVarErr pred $$ how_to_allow)
888 class_name = className cls
889 arity = classArity cls
891 arity_err = arityErr "Class" class_name arity n_tys
893 arby_preds_ok = case ctxt of
894 InstHeadCtxt -> True -- We check for instance-head formation
895 -- in checkValidInstHead
896 InstThetaCtxt -> dopt Opt_AllowUndecidableInstances dflags
897 other -> dopt Opt_GlasgowExts dflags
899 how_to_allow = case ctxt of
900 InstHeadCtxt -> empty -- Should not happen
901 InstThetaCtxt -> parens undecidableMsg
902 other -> parens (ptext SLIT("Use -fglasgow-exts to permit this"))
904 check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
905 -- Implicit parameters only allows in type
906 -- signatures; not in instance decls, superclasses etc
907 -- The reason for not allowing implicit params in instances is a bit subtle
908 -- If we allowed instance (?x::Int, Eq a) => Foo [a] where ...
909 -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
910 -- discharge all the potential usas of the ?x in e. For example, a
911 -- constraint Foo [Int] might come out of e,and applying the
912 -- instance decl would show up two uses of ?x.
914 check_source_ty dflags TypeCtxt (NType tc tys) = mapTc_ check_arg_type tys
917 check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
919 -------------------------
920 tyvar_head ty -- Haskell 98 allows predicates of form
921 | tcIsTyVarTy ty = True -- C (a ty1 .. tyn)
922 | otherwise -- where a is a type variable
923 = case tcSplitAppTy_maybe ty of
924 Just (ty, _) -> tyvar_head ty
929 badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprSourceType sty
930 predTyVarErr pred = ptext SLIT("Non-type variables in constraint:") <+> pprPred pred
931 dupPredWarn dups = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
933 checkThetaCtxt ctxt theta
934 = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
935 ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
939 %************************************************************************
941 \subsection{Checking for a decent instance head type}
943 %************************************************************************
945 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
946 it must normally look like: @instance Foo (Tycon a b c ...) ...@
948 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
949 flag is on, or (2)~the instance is imported (they must have been
950 compiled elsewhere). In these cases, we let them go through anyway.
952 We can also have instances for functions: @instance Foo (a -> b) ...@.
955 checkValidInstHead :: Type -> TcM (Class, [TcType])
957 checkValidInstHead ty -- Should be a source type
958 = case tcSplitPredTy_maybe ty of {
959 Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
962 case getClassPredTys_maybe pred of {
963 Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
966 getDOptsTc `thenNF_Tc` \ dflags ->
967 mapTc_ check_arg_type tys `thenTc_`
968 check_inst_head dflags clas tys `thenTc_`
972 check_inst_head dflags clas tys
974 -- A user declaration of a CCallable/CReturnable instance
975 -- must be for a "boxed primitive" type.
976 (clas `hasKey` cCallableClassKey
977 && not (ccallable_type first_ty))
978 || (clas `hasKey` cReturnableClassKey
979 && not (creturnable_type first_ty))
980 = failWithTc (nonBoxedPrimCCallErr clas first_ty)
982 -- If GlasgowExts then check at least one isn't a type variable
983 | dopt Opt_GlasgowExts dflags
984 = check_tyvars dflags clas tys
986 -- WITH HASKELL 1.4, MUST HAVE C (T a b c)
988 Just (tycon, arg_tys) <- tcSplitTyConApp_maybe first_ty,
989 not (isSynTyCon tycon), -- ...but not a synonym
990 all tcIsTyVarTy arg_tys, -- Applied to type variables
991 equalLength (varSetElems (tyVarsOfTypes arg_tys)) arg_tys
992 -- This last condition checks that all the type variables are distinct
996 = failWithTc (instTypeErr (pprClassPred clas tys) head_shape_msg)
1001 ccallable_type ty = isFFIArgumentTy dflags PlayRisky ty
1002 creturnable_type ty = isFFIImportResultTy dflags ty
1004 head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
1005 text "where T is not a synonym, and a,b,c are distinct type variables")
1007 check_tyvars dflags clas tys
1008 -- Check that at least one isn't a type variable
1009 -- unless -fallow-undecideable-instances
1010 | dopt Opt_AllowUndecidableInstances dflags = returnTc ()
1011 | not (all tcIsTyVarTy tys) = returnTc ()
1012 | otherwise = failWithTc (instTypeErr (pprClassPred clas tys) msg)
1014 msg = parens (ptext SLIT("There must be at least one non-type-variable in the instance head")
1017 undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
1021 instTypeErr pp_ty msg
1022 = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,
1025 nonBoxedPrimCCallErr clas inst_ty
1026 = hang (ptext SLIT("Unacceptable instance type for ccall-ish class"))
1027 4 (pprClassPred clas [inst_ty])