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,
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, mkSysLocalName,
81 mkLocalName, 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 (mkSysLocalName uniq SLIT("t")) kind VanillaTv
106 newTyVarTy :: Kind -> NF_TcM TcType
108 = newTyVar kind `thenNF_Tc` \ tc_tyvar ->
109 returnNF_Tc (TyVarTy tc_tyvar)
111 newHoleTyVarTy :: NF_TcM TcType
112 = tcGetUnique `thenNF_Tc` \ uniq ->
113 tcNewMutTyVar (mkSysLocalName uniq SLIT("h")) openTypeKind HoleTv `thenNF_Tc` \ tv ->
114 returnNF_Tc (TyVarTy tv)
116 newTyVarTys :: Int -> Kind -> NF_TcM [TcType]
117 newTyVarTys n kind = mapNF_Tc newTyVarTy (nOfThem n kind)
119 newKindVar :: NF_TcM TcKind
121 = tcGetUnique `thenNF_Tc` \ uniq ->
122 tcNewMutTyVar (mkSysLocalName uniq SLIT("k")) superKind VanillaTv `thenNF_Tc` \ kv ->
123 returnNF_Tc (TyVarTy kv)
125 newKindVars :: Int -> NF_TcM [TcKind]
126 newKindVars n = mapNF_Tc (\ _ -> newKindVar) (nOfThem n ())
128 newBoxityVar :: NF_TcM TcKind
130 = tcGetUnique `thenNF_Tc` \ uniq ->
131 tcNewMutTyVar (mkSysLocalName uniq SLIT("bx")) superBoxity VanillaTv `thenNF_Tc` \ kv ->
132 returnNF_Tc (TyVarTy kv)
136 %************************************************************************
138 \subsection{Type instantiation}
140 %************************************************************************
142 I don't understand why this is needed
143 An old comments says "No need for tcSplitForAllTyM because a type
144 variable can't be instantiated to a for-all type"
145 But the same is true of rho types!
148 tcSplitRhoTyM :: TcType -> NF_TcM (TcThetaType, TcType)
152 -- A type variable is never instantiated to a dictionary type,
153 -- so we don't need to do a tcReadVar on the "arg".
154 go syn_t (FunTy arg res) ts = case tcSplitPredTy_maybe arg of
155 Just pair -> go res res (pair:ts)
156 Nothing -> returnNF_Tc (reverse ts, syn_t)
157 go syn_t (NoteTy n t) ts = go syn_t t ts
158 go syn_t (TyVarTy tv) ts = getTcTyVar tv `thenNF_Tc` \ maybe_ty ->
160 Just ty | not (tcIsTyVarTy ty) -> go syn_t ty ts
161 other -> returnNF_Tc (reverse ts, syn_t)
162 go syn_t t ts = returnNF_Tc (reverse ts, syn_t)
166 %************************************************************************
168 \subsection{Type instantiation}
170 %************************************************************************
172 Instantiating a bunch of type variables
175 tcInstTyVars :: [TyVar]
176 -> NF_TcM ([TcTyVar], [TcType], Subst)
179 = mapNF_Tc tcInstTyVar tyvars `thenNF_Tc` \ tc_tyvars ->
181 tys = mkTyVarTys tc_tyvars
183 returnNF_Tc (tc_tyvars, tys, mkTopTyVarSubst tyvars tys)
184 -- Since the tyvars are freshly made,
185 -- they cannot possibly be captured by
186 -- any existing for-alls. Hence mkTopTyVarSubst
189 = tcGetUnique `thenNF_Tc` \ uniq ->
191 name = setNameUnique (tyVarName tyvar) uniq
192 -- Note that we don't change the print-name
193 -- This won't confuse the type checker but there's a chance
194 -- that two different tyvars will print the same way
195 -- in an error message. -dppr-debug will show up the difference
196 -- Better watch out for this. If worst comes to worst, just
197 -- use mkSysLocalName.
199 tcNewMutTyVar name (tyVarKind tyvar) VanillaTv
201 tcInstSigTyVars :: TyVarDetails -> [TyVar] -> NF_TcM [TcTyVar]
202 tcInstSigTyVars details tyvars -- Very similar to tcInstTyVar
203 = tcGetUniques `thenNF_Tc` \ uniqs ->
204 listTc [ ASSERT( not (kind `eqKind` openTypeKind) ) -- Shouldn't happen
205 tcNewMutTyVar name kind details
206 | (tyvar, uniq) <- tyvars `zip` uniqs,
207 let name = setNameUnique (tyVarName tyvar) uniq,
208 let kind = tyVarKind tyvar
212 @tcInstType@ instantiates the outer-level for-alls of a TcType with
213 fresh type variables, splits off the dictionary part, and returns the results.
216 tcInstType :: TcType -> NF_TcM ([TcTyVar], TcThetaType, TcType)
218 = case tcSplitForAllTys ty of
219 ([], rho) -> -- There may be overloading but no type variables;
220 -- (?x :: Int) => Int -> Int
222 (theta, tau) = tcSplitRhoTy rho -- Used to be tcSplitRhoTyM
224 returnNF_Tc ([], theta, tau)
226 (tyvars, rho) -> tcInstTyVars tyvars `thenNF_Tc` \ (tyvars', _, tenv) ->
228 (theta, tau) = tcSplitRhoTy (substTy tenv rho) -- Used to be tcSplitRhoTyM
230 returnNF_Tc (tyvars', theta, tau)
233 tcInstSigType :: TyVarDetails -> Type -> NF_TcM ([TcTyVar], TcThetaType, TcType)
234 -- Very similar to tcInstSigType, but uses signature type variables
235 -- Also, somewhat arbitrarily, don't deal with the monomorphic case so efficiently
236 tcInstSigType tv_details poly_ty
238 (tyvars, rho) = tcSplitForAllTys poly_ty
240 tcInstSigTyVars tv_details tyvars `thenNF_Tc` \ tyvars' ->
241 -- Make *signature* type variables
244 tyvar_tys' = mkTyVarTys tyvars'
245 rho' = substTy (mkTopTyVarSubst tyvars tyvar_tys') rho
246 -- mkTopTyVarSubst because the tyvars' are fresh
248 (theta', tau') = tcSplitRhoTy rho'
249 -- This splitRhoTy tries hard to make sure that tau' is a type synonym
250 -- wherever possible, which can improve interface files.
252 returnNF_Tc (tyvars', theta', tau')
257 %************************************************************************
259 \subsection{Putting and getting mutable type variables}
261 %************************************************************************
264 putTcTyVar :: TcTyVar -> TcType -> NF_TcM TcType
265 getTcTyVar :: TcTyVar -> NF_TcM (Maybe TcType)
272 | not (isMutTyVar tyvar)
273 = pprTrace "putTcTyVar" (ppr tyvar) $
277 = ASSERT( isMutTyVar tyvar )
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 an arbitrary type
404 -- We know it's unbound even though we don't carry an environment,
405 -- because at the binding site for a type variable we bind the
406 -- mutable tyvar to a fresh immutable one. So the mutable store
407 -- plays the role of an environment. If we come across a mutable
408 -- type variable that isn't so bound, it must be completely free.
409 zonk_unbound_tyvar tv = putTcTyVar tv (mkArbitraryType tv)
412 -- When the type checker finds a type variable with no binding,
413 -- which means it can be instantiated with an arbitrary type, it
414 -- usually instantiates it to Void. Eg.
418 -- length Void (Nil Void)
420 -- But in really obscure programs, the type variable might have
421 -- a kind other than *, so we need to invent a suitably-kinded type.
425 -- List for kind *->*
426 -- Tuple for kind *->...*->*
428 -- which deals with most cases. (Previously, it only dealt with
431 -- In the other cases, it just makes up a TyCon with a suitable
432 -- kind. If this gets into an interface file, anyone reading that
433 -- file won't understand it. This is fixable (by making the client
434 -- of the interface file make up a TyCon too) but it is tiresome and
435 -- never happens, so I am leaving it
437 mkArbitraryType :: TcTyVar -> Type
438 -- Make up an arbitrary type whose kind is the same as the tyvar.
439 -- We'll use this to instantiate the (unbound) tyvar.
441 | isAnyTypeKind kind = voidTy -- The vastly common case
442 | otherwise = TyConApp tycon []
445 (args,res) = Type.splitFunTys kind -- Kinds are simple; use Type.splitFunTys
447 tycon | kind `eqKind` tyConKind listTyCon -- *->*
448 = listTyCon -- No tuples this size
450 | all isTypeKind args && isTypeKind res
451 = tupleTyCon Boxed (length args) -- *-> ... ->*->*
454 = pprTrace "Urk! Inventing strangely-kinded void TyCon" (ppr tc_name) $
455 mkPrimTyCon tc_name kind 0 [] VoidRep
456 -- Same name as the tyvar, apart from making it start with a colon (sigh)
457 -- I dread to think what will happen if this gets out into an
458 -- interface file. Catastrophe likely. Major sigh.
460 tc_name = mkLocalName (getUnique tv) (mkDerivedTyConOcc (getOccName tv)) noSrcLoc
462 -- zonkTcTyVarToTyVar is applied to the *binding* occurrence
463 -- of a type variable, at the *end* of type checking. It changes
464 -- the *mutable* type variable into an *immutable* one.
466 -- It does this by making an immutable version of tv and binds tv to it.
467 -- Now any bound occurences of the original type variable will get
468 -- zonked to the immutable version.
470 zonkTcTyVarToTyVar :: TcTyVar -> NF_TcM TyVar
471 zonkTcTyVarToTyVar tv
473 -- Make an immutable version, defaulting
474 -- the kind to lifted if necessary
475 immut_tv = mkTyVar (tyVarName tv) (defaultKind (tyVarKind tv))
476 immut_tv_ty = mkTyVarTy immut_tv
478 zap tv = putTcTyVar tv immut_tv_ty
479 -- Bind the mutable version to the immutable one
481 -- If the type variable is mutable, then bind it to immut_tv_ty
482 -- so that all other occurrences of the tyvar will get zapped too
483 zonkTyVar zap tv `thenNF_Tc` \ ty2 ->
485 WARN( not (immut_tv_ty `tcEqType` ty2), ppr tv $$ ppr immut_tv $$ ppr ty2 )
491 %************************************************************************
493 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
495 %* For internal use only! *
497 %************************************************************************
500 -- zonkType is used for Kinds as well
502 -- For unbound, mutable tyvars, zonkType uses the function given to it
503 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
504 -- type variable and zonks the kind too
506 zonkType :: (TcTyVar -> NF_TcM Type) -- What to do with unbound mutable type variables
507 -- see zonkTcType, and zonkTcTypeToType
510 zonkType unbound_var_fn ty
513 go (TyConApp tycon tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' ->
514 returnNF_Tc (TyConApp tycon tys')
516 go (NoteTy (SynNote ty1) ty2) = go ty1 `thenNF_Tc` \ ty1' ->
517 go ty2 `thenNF_Tc` \ ty2' ->
518 returnNF_Tc (NoteTy (SynNote ty1') ty2')
520 go (NoteTy (FTVNote _) ty2) = go ty2 -- Discard free-tyvar annotations
522 go (SourceTy p) = go_pred p `thenNF_Tc` \ p' ->
523 returnNF_Tc (SourceTy p')
525 go (FunTy arg res) = go arg `thenNF_Tc` \ arg' ->
526 go res `thenNF_Tc` \ res' ->
527 returnNF_Tc (FunTy arg' res')
529 go (AppTy fun arg) = go fun `thenNF_Tc` \ fun' ->
530 go arg `thenNF_Tc` \ arg' ->
531 returnNF_Tc (mkAppTy fun' arg')
533 -- The two interesting cases!
534 go (TyVarTy tyvar) = zonkTyVar unbound_var_fn tyvar
536 go (ForAllTy tyvar ty) = zonkTcTyVarToTyVar tyvar `thenNF_Tc` \ tyvar' ->
537 go ty `thenNF_Tc` \ ty' ->
538 returnNF_Tc (ForAllTy tyvar' ty')
540 go_pred (ClassP c tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' ->
541 returnNF_Tc (ClassP c tys')
542 go_pred (NType tc tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' ->
543 returnNF_Tc (NType tc tys')
544 go_pred (IParam n ty) = go ty `thenNF_Tc` \ ty' ->
545 returnNF_Tc (IParam n ty')
547 zonkTyVar :: (TcTyVar -> NF_TcM Type) -- What to do for an unbound mutable variable
548 -> TcTyVar -> NF_TcM TcType
549 zonkTyVar unbound_var_fn tyvar
550 | not (isMutTyVar tyvar) -- Not a mutable tyvar. This can happen when
551 -- zonking a forall type, when the bound type variable
552 -- needn't be mutable
553 = ASSERT( isTyVar tyvar ) -- Should not be any immutable kind vars
554 returnNF_Tc (TyVarTy tyvar)
557 = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
559 Nothing -> unbound_var_fn tyvar -- Mutable and unbound
560 Just other_ty -> zonkType unbound_var_fn other_ty -- Bound
565 %************************************************************************
567 \subsection{Checking a user type}
569 %************************************************************************
571 When dealing with a user-written type, we first translate it from an HsType
572 to a Type, performing kind checking, and then check various things that should
573 be true about it. We don't want to perform these checks at the same time
574 as the initial translation because (a) they are unnecessary for interface-file
575 types and (b) when checking a mutually recursive group of type and class decls,
576 we can't "look" at the tycons/classes yet. Also, the checks are are rather
577 diverse, and used to really mess up the other code.
579 One thing we check for is 'rank'.
581 Rank 0: monotypes (no foralls)
582 Rank 1: foralls at the front only, Rank 0 inside
583 Rank 2: foralls at the front, Rank 1 on left of fn arrow,
585 basic ::= tyvar | T basic ... basic
587 r2 ::= forall tvs. cxt => r2a
588 r2a ::= r1 -> r2a | basic
589 r1 ::= forall tvs. cxt => r0
590 r0 ::= r0 -> r0 | basic
592 Another thing is to check that type synonyms are saturated.
593 This might not necessarily show up in kind checking.
595 data T k = MkT (k Int)
601 = FunSigCtxt Name -- Function type signature
602 | ExprSigCtxt -- Expression type signature
603 | ConArgCtxt Name -- Data constructor argument
604 | TySynCtxt Name -- RHS of a type synonym decl
605 | GenPatCtxt -- Pattern in generic decl
606 -- f{| a+b |} (Inl x) = ...
607 | PatSigCtxt -- Type sig in pattern
609 | ResSigCtxt -- Result type sig
611 | ForSigCtxt Name -- Foreign inport or export signature
612 | RuleSigCtxt Name -- Signature on a forall'd variable in a RULE
614 -- Notes re TySynCtxt
615 -- We allow type synonyms that aren't types; e.g. type List = []
617 -- If the RHS mentions tyvars that aren't in scope, we'll
618 -- quantify over them:
619 -- e.g. type T = a->a
620 -- will become type T = forall a. a->a
622 -- With gla-exts that's right, but for H98 we should complain.
625 pprUserTypeCtxt (FunSigCtxt n) = ptext SLIT("the type signature for") <+> quotes (ppr n)
626 pprUserTypeCtxt ExprSigCtxt = ptext SLIT("an expression type signature")
627 pprUserTypeCtxt (ConArgCtxt c) = ptext SLIT("the type of constructor") <+> quotes (ppr c)
628 pprUserTypeCtxt (TySynCtxt c) = ptext SLIT("the RHS of a type synonym declaration") <+> quotes (ppr c)
629 pprUserTypeCtxt GenPatCtxt = ptext SLIT("the type pattern of a generic definition")
630 pprUserTypeCtxt PatSigCtxt = ptext SLIT("a pattern type signature")
631 pprUserTypeCtxt ResSigCtxt = ptext SLIT("a result type signature")
632 pprUserTypeCtxt (ForSigCtxt n) = ptext SLIT("the foreign signature for") <+> quotes (ppr n)
633 pprUserTypeCtxt (RuleSigCtxt n) = ptext SLIT("the type signature on") <+> quotes (ppr n)
637 checkValidType :: UserTypeCtxt -> Type -> TcM ()
638 -- Checks that the type is valid for the given context
639 checkValidType ctxt ty
640 = doptsTc Opt_GlasgowExts `thenNF_Tc` \ gla_exts ->
642 rank | gla_exts = Arbitrary
644 = case ctxt of -- Haskell 98
648 TySynCtxt _ -> Rank 0
649 ExprSigCtxt -> Rank 1
650 FunSigCtxt _ -> Rank 1
651 ConArgCtxt _ -> Rank 1 -- We are given the type of the entire
652 -- constructor, hence rank 1
653 ForSigCtxt _ -> Rank 1
654 RuleSigCtxt _ -> Rank 1
656 actual_kind = typeKind ty
658 actual_kind_is_lifted = actual_kind `eqKind` liftedTypeKind
660 kind_ok = case ctxt of
661 TySynCtxt _ -> True -- Any kind will do
662 GenPatCtxt -> actual_kind_is_lifted
663 ForSigCtxt _ -> actual_kind_is_lifted
664 other -> isTypeKind actual_kind
666 ubx_tup | not gla_exts = UT_NotOk
667 | otherwise = case ctxt of
670 -- Unboxed tuples ok in function results,
671 -- but for type synonyms we allow them even at
674 tcAddErrCtxt (checkTypeCtxt ctxt ty) $
676 -- Check that the thing has kind Type, and is lifted if necessary
677 checkTc kind_ok (kindErr actual_kind) `thenTc_`
679 -- Check the internal validity of the type itself
680 check_poly_type rank ubx_tup ty
683 checkTypeCtxt ctxt ty
684 = vcat [ptext SLIT("In the type:") <+> ppr_ty ty,
685 ptext SLIT("While checking") <+> pprUserTypeCtxt ctxt ]
687 -- Hack alert. If there are no tyvars, (ppr sigma_ty) will print
688 -- something strange like {Eq k} -> k -> k, because there is no
689 -- ForAll at the top of the type. Since this is going to the user
690 -- we want it to look like a proper Haskell type even then; hence the hack
692 -- This shows up in the complaint about
694 -- op :: Eq a => a -> a
695 ppr_ty ty | null forall_tvs && not (null theta) = pprTheta theta <+> ptext SLIT("=>") <+> ppr tau
698 (forall_tvs, theta, tau) = tcSplitSigmaTy ty
703 data Rank = Rank Int | Arbitrary
705 decRank :: Rank -> Rank
706 decRank Arbitrary = Arbitrary
707 decRank (Rank n) = Rank (n-1)
709 ----------------------------------------
710 data UbxTupFlag = UT_Ok | UT_NotOk
711 -- The "Ok" version means "ok if -fglasgow-exts is on"
713 ----------------------------------------
714 check_poly_type :: Rank -> UbxTupFlag -> Type -> TcM ()
715 check_poly_type (Rank 0) ubx_tup ty
716 = check_tau_type (Rank 0) ubx_tup ty
718 check_poly_type rank ubx_tup ty
720 (tvs, theta, tau) = tcSplitSigmaTy ty
722 check_valid_theta SigmaCtxt theta `thenTc_`
723 check_tau_type (decRank rank) ubx_tup tau `thenTc_`
724 checkFreeness tvs theta `thenTc_`
725 checkAmbiguity tvs theta (tyVarsOfType tau)
727 ----------------------------------------
728 check_arg_type :: Type -> TcM ()
729 -- The sort of type that can instantiate a type variable,
730 -- or be the argument of a type constructor.
731 -- Not an unboxed tuple, not a forall.
732 -- Other unboxed types are very occasionally allowed as type
733 -- arguments depending on the kind of the type constructor
735 -- For example, we want to reject things like:
737 -- instance Ord a => Ord (forall s. T s a)
739 -- g :: T s (forall b.b)
741 -- NB: unboxed tuples can have polymorphic or unboxed args.
742 -- This happens in the workers for functions returning
743 -- product types with polymorphic components.
744 -- But not in user code.
745 -- Anyway, they are dealt with by a special case in check_tau_type
748 = check_tau_type (Rank 0) UT_NotOk ty `thenTc_`
749 checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
751 ----------------------------------------
752 check_tau_type :: Rank -> UbxTupFlag -> Type -> TcM ()
753 -- Rank is allowed rank for function args
754 -- No foralls otherwise
756 check_tau_type rank ubx_tup ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty)
757 check_tau_type rank ubx_tup (SourceTy sty) = getDOptsTc `thenNF_Tc` \ dflags ->
758 check_source_ty dflags TypeCtxt sty
759 check_tau_type rank ubx_tup (TyVarTy _) = returnTc ()
760 check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
761 = check_poly_type rank UT_NotOk arg_ty `thenTc_`
762 check_tau_type rank UT_Ok res_ty
764 check_tau_type rank ubx_tup (AppTy ty1 ty2)
765 = check_arg_type ty1 `thenTc_` check_arg_type ty2
767 check_tau_type rank ubx_tup (NoteTy note ty)
768 = check_tau_type rank ubx_tup ty
769 -- Synonym notes are built only when the synonym is
770 -- saturated (see Type.mkSynTy)
771 -- Not checking the 'note' part allows us to instantiate a synonym
772 -- defn with a for-all type, but that seems OK too
774 check_tau_type rank ubx_tup ty@(TyConApp tc tys)
776 = -- NB: Type.mkSynTy builds a TyConApp (not a NoteTy) for an unsaturated
777 -- synonym application, leaving it to checkValidType (i.e. right here
779 checkTc syn_arity_ok arity_msg `thenTc_`
780 mapTc_ check_arg_type tys
782 | isUnboxedTupleTyCon tc
783 = doptsTc Opt_GlasgowExts `thenNF_Tc` \ gla_exts ->
784 checkTc (ubx_tup_ok gla_exts) ubx_tup_msg `thenTc_`
785 mapTc_ (check_tau_type (Rank 0) UT_Ok) tys
786 -- Args are allowed to be unlifted, or
787 -- more unboxed tuples, so can't use check_arg_ty
790 = mapTc_ check_arg_type tys
793 ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False }
795 syn_arity_ok = tc_arity <= n_args
796 -- It's OK to have an *over-applied* type synonym
797 -- data Tree a b = ...
798 -- type Foo a = Tree [a]
799 -- f :: Foo a b -> ...
801 tc_arity = tyConArity tc
803 arity_msg = arityErr "Type synonym" (tyConName tc) tc_arity n_args
804 ubx_tup_msg = ubxArgTyErr ty
806 ----------------------------------------
807 forAllTyErr ty = ptext SLIT("Illegal polymorphic type:") <+> ppr_ty ty
808 unliftedArgErr ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr_ty ty
809 ubxArgTyErr ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr_ty ty
810 kindErr kind = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
816 is ambiguous if P contains generic variables
817 (i.e. one of the Vs) that are not mentioned in tau
819 However, we need to take account of functional dependencies
820 when we speak of 'mentioned in tau'. Example:
821 class C a b | a -> b where ...
823 forall x y. (C x y) => x
824 is not ambiguous because x is mentioned and x determines y
826 NB; the ambiguity check is only used for *user* types, not for types
827 coming from inteface files. The latter can legitimately have
828 ambiguous types. Example
830 class S a where s :: a -> (Int,Int)
831 instance S Char where s _ = (1,1)
832 f:: S a => [a] -> Int -> (Int,Int)
833 f (_::[a]) x = (a*x,b)
834 where (a,b) = s (undefined::a)
836 Here the worker for f gets the type
837 fw :: forall a. S a => Int -> (# Int, Int #)
839 If the list of tv_names is empty, we have a monotype, and then we
840 don't need to check for ambiguity either, because the test can't fail
844 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
845 checkAmbiguity forall_tyvars theta tau_tyvars
846 = mapTc_ complain (filter is_ambig theta)
848 complain pred = addErrTc (ambigErr pred)
849 extended_tau_vars = grow theta tau_tyvars
850 is_ambig pred = any ambig_var (varSetElems (tyVarsOfPred pred))
852 ambig_var ct_var = (ct_var `elem` forall_tyvars) &&
853 not (ct_var `elemVarSet` extended_tau_vars)
855 is_free ct_var = not (ct_var `elem` forall_tyvars)
858 = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
859 nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
860 ptext SLIT("must be reachable from the type after the '=>'"))]
863 In addition, GHC insists that at least one type variable
864 in each constraint is in V. So we disallow a type like
865 forall a. Eq b => b -> b
866 even in a scope where b is in scope.
869 checkFreeness forall_tyvars theta
870 = mapTc_ complain (filter is_free theta)
872 is_free pred = not (isIPPred pred)
873 && not (any bound_var (varSetElems (tyVarsOfPred pred)))
874 bound_var ct_var = ct_var `elem` forall_tyvars
875 complain pred = addErrTc (freeErr pred)
878 = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
879 ptext SLIT("are already in scope"),
880 nest 4 (ptext SLIT("At least one must be universally quantified here"))
885 %************************************************************************
887 \subsection{Checking a theta or source type}
889 %************************************************************************
893 = ClassSCCtxt Name -- Superclasses of clas
894 | SigmaCtxt -- Context of a normal for-all type
895 | DataTyCtxt Name -- Context of a data decl
896 | TypeCtxt -- Source type in an ordinary type
897 | InstThetaCtxt -- Context of an instance decl
898 | InstHeadCtxt -- Head of an instance decl
900 pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
901 pprSourceTyCtxt SigmaCtxt = ptext SLIT("the context of a polymorphic type")
902 pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
903 pprSourceTyCtxt InstThetaCtxt = ptext SLIT("the context of an instance declaration")
904 pprSourceTyCtxt InstHeadCtxt = ptext SLIT("the head of an instance declaration")
905 pprSourceTyCtxt TypeCtxt = ptext SLIT("the context of a type")
909 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
910 checkValidTheta ctxt theta
911 = tcAddErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
913 -------------------------
914 check_valid_theta ctxt []
916 check_valid_theta ctxt theta
917 = getDOptsTc `thenNF_Tc` \ dflags ->
918 warnTc (not (null dups)) (dupPredWarn dups) `thenNF_Tc_`
919 mapTc_ (check_source_ty dflags ctxt) theta
921 (_,dups) = removeDups tcCmpPred theta
923 -------------------------
924 check_source_ty dflags ctxt pred@(ClassP cls tys)
925 = -- Class predicates are valid in all contexts
926 mapTc_ check_arg_type tys `thenTc_`
927 checkTc (arity == n_tys) arity_err `thenTc_`
928 checkTc (all tyvar_head tys || arby_preds_ok)
929 (predTyVarErr pred $$ how_to_allow)
932 class_name = className cls
933 arity = classArity cls
935 arity_err = arityErr "Class" class_name arity n_tys
937 arby_preds_ok = case ctxt of
938 InstHeadCtxt -> True -- We check for instance-head formation
939 -- in checkValidInstHead
940 InstThetaCtxt -> dopt Opt_AllowUndecidableInstances dflags
941 other -> dopt Opt_GlasgowExts dflags
943 how_to_allow = case ctxt of
944 InstHeadCtxt -> empty -- Should not happen
945 InstThetaCtxt -> parens undecidableMsg
946 other -> parens (ptext SLIT("Use -fglasgow-exts to permit this"))
948 check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
949 -- Implicit parameters only allows in type
950 -- signatures; not in instance decls, superclasses etc
951 -- The reason for not allowing implicit params in instances is a bit subtle
952 -- If we allowed instance (?x::Int, Eq a) => Foo [a] where ...
953 -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
954 -- discharge all the potential usas of the ?x in e. For example, a
955 -- constraint Foo [Int] might come out of e,and applying the
956 -- instance decl would show up two uses of ?x.
958 check_source_ty dflags TypeCtxt (NType tc tys) = mapTc_ check_arg_type tys
961 check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
963 -------------------------
964 tyvar_head ty -- Haskell 98 allows predicates of form
965 | tcIsTyVarTy ty = True -- C (a ty1 .. tyn)
966 | otherwise -- where a is a type variable
967 = case tcSplitAppTy_maybe ty of
968 Just (ty, _) -> tyvar_head ty
973 badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprSourceType sty
974 predTyVarErr pred = ptext SLIT("Non-type variables in constraint:") <+> pprPred pred
975 dupPredWarn dups = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
977 checkThetaCtxt ctxt theta
978 = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
979 ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
983 %************************************************************************
985 \subsection{Checking for a decent instance head type}
987 %************************************************************************
989 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
990 it must normally look like: @instance Foo (Tycon a b c ...) ...@
992 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
993 flag is on, or (2)~the instance is imported (they must have been
994 compiled elsewhere). In these cases, we let them go through anyway.
996 We can also have instances for functions: @instance Foo (a -> b) ...@.
999 checkValidInstHead :: Type -> TcM (Class, [TcType])
1001 checkValidInstHead ty -- Should be a source type
1002 = case tcSplitPredTy_maybe ty of {
1003 Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
1006 case getClassPredTys_maybe pred of {
1007 Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
1010 getDOptsTc `thenNF_Tc` \ dflags ->
1011 mapTc_ check_arg_type tys `thenTc_`
1012 check_inst_head dflags clas tys `thenTc_`
1013 returnTc (clas, tys)
1016 check_inst_head dflags clas tys
1018 -- A user declaration of a CCallable/CReturnable instance
1019 -- must be for a "boxed primitive" type.
1020 (clas `hasKey` cCallableClassKey
1021 && not (ccallable_type first_ty))
1022 || (clas `hasKey` cReturnableClassKey
1023 && not (creturnable_type first_ty))
1024 = failWithTc (nonBoxedPrimCCallErr clas first_ty)
1026 -- If GlasgowExts then check at least one isn't a type variable
1027 | dopt Opt_GlasgowExts dflags
1028 = check_tyvars dflags clas tys
1030 -- WITH HASKELL 1.4, MUST HAVE C (T a b c)
1032 Just (tycon, arg_tys) <- tcSplitTyConApp_maybe first_ty,
1033 not (isSynTyCon tycon), -- ...but not a synonym
1034 all tcIsTyVarTy arg_tys, -- Applied to type variables
1035 equalLength (varSetElems (tyVarsOfTypes arg_tys)) arg_tys
1036 -- This last condition checks that all the type variables are distinct
1040 = failWithTc (instTypeErr (pprClassPred clas tys) head_shape_msg)
1043 (first_ty : _) = tys
1045 ccallable_type ty = isFFIArgumentTy dflags PlayRisky ty
1046 creturnable_type ty = isFFIImportResultTy dflags ty
1048 head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
1049 text "where T is not a synonym, and a,b,c are distinct type variables")
1051 check_tyvars dflags clas tys
1052 -- Check that at least one isn't a type variable
1053 -- unless -fallow-undecideable-instances
1054 | dopt Opt_AllowUndecidableInstances dflags = returnTc ()
1055 | not (all tcIsTyVarTy tys) = returnTc ()
1056 | otherwise = failWithTc (instTypeErr (pprClassPred clas tys) msg)
1058 msg = parens (ptext SLIT("There must be at least one non-type-variable in the instance head")
1061 undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
1065 instTypeErr pp_ty msg
1066 = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,
1069 nonBoxedPrimCCallErr clas inst_ty
1070 = hang (ptext SLIT("Unacceptable instance type for ccall-ish class"))
1071 4 (pprClassPred clas [inst_ty])