2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 \section[TcMonoType]{Typechecking user-specified @MonoTypes@}
7 module TcMonoType ( tcHsType, tcHsSigType, tcHsBoxedSigType,
8 tcContext, tcClassContext,
11 kcHsTyVar, kcHsTyVars, mkTyClTyVars,
12 kcHsType, kcHsSigType, kcHsBoxedSigType, kcHsContext,
13 kcTyVarScope, newSigTyVars, mkImmutTyVars,
15 TcSigInfo(..), tcTySig, mkTcSig, maybeSig,
16 checkSigTyVars, sigCtxt, sigPatCtxt
19 #include "HsVersions.h"
21 import HsSyn ( HsType(..), HsTyVarBndr(..), HsUsageAnn(..),
22 Sig(..), HsPred(..), pprParendHsType, HsTupCon(..), hsTyVarNames )
23 import RnHsSyn ( RenamedHsType, RenamedHsPred, RenamedContext, RenamedSig )
24 import TcHsSyn ( TcId )
27 import TcEnv ( tcExtendTyVarEnv, tcLookupTy, tcGetValueEnv, tcGetInScopeTyVars,
28 tcExtendUVarEnv, tcLookupUVar,
29 tcGetGlobalTyVars, valueEnvIds,
30 TyThing(..), tcExtendKindEnv
32 import TcType ( TcType, TcKind, TcTyVar, TcThetaType, TcTauType,
33 newKindVar, tcInstSigVar,
34 zonkKindEnv, zonkTcType, zonkTcTyVars, zonkTcTyVar
36 import Inst ( Inst, InstOrigin(..), newMethodWithGivenTy, instToIdBndr,
37 instFunDeps, instFunDepsOfTheta )
38 import FunDeps ( tyVarFunDep, oclose )
39 import TcUnify ( unifyKind, unifyOpenTypeKind )
40 import Type ( Type, Kind, PredType(..), ThetaType, UsageAnn(..),
41 mkTyVarTy, mkTyVarTys, mkFunTy, mkSynTy, mkUsgTy,
42 mkUsForAllTy, zipFunTys, hoistForAllTys,
43 mkSigmaTy, mkPredTy, mkTyConApp,
44 mkAppTys, splitForAllTys, splitRhoTy, mkRhoTy,
45 boxedTypeKind, unboxedTypeKind, mkArrowKind,
46 mkArrowKinds, getTyVar_maybe, getTyVar, splitFunTy_maybe,
47 tidyOpenType, tidyOpenTypes, tidyTyVar, tidyTyVars,
48 tyVarsOfType, tyVarsOfPred, mkForAllTys,
49 classesOfPreds, isUnboxedTupleType
51 import PprType ( pprType, pprPred )
52 import Subst ( mkTopTyVarSubst, substTy )
53 import Id ( mkVanillaId, idName, idType, idFreeTyVars )
54 import Var ( TyVar, mkTyVar, tyVarKind, mkNamedUVar )
57 import ErrUtils ( Message )
58 import TyCon ( TyCon, isSynTyCon, tyConArity, tyConKind )
59 import Class ( ClassContext, classArity, classTyCon )
60 import Name ( Name, isLocallyDefined )
61 import TysWiredIn ( mkListTy, mkTupleTy )
62 import UniqFM ( elemUFM )
63 import BasicTypes ( Boxity(..) )
64 import SrcLoc ( SrcLoc )
65 import Util ( mapAccumL, isSingleton )
70 %************************************************************************
72 \subsection{Kind checking}
74 %************************************************************************
78 When we come across the binding site for some type variables, we
81 1. Figure out what kind each tyvar has
83 2. Create suitably-kinded tyvars,
85 and typecheck the body
87 To do step 1, we proceed thus:
89 1a. Bind each type variable to a kind variable
90 1b. Apply the kind checker
91 1c. Zonk the resulting kinds
93 The kind checker is passed to kcTyVarScope as an argument.
95 For example, when we find
96 (forall a m. m a -> m a)
97 we bind a,m to kind varibles and kind-check (m a -> m a). This
98 makes a get kind *, and m get kind *->*. Now we typecheck (m a -> m a)
99 in an environment that binds a and m suitably.
101 The kind checker passed to kcTyVarScope needs to look at enough to
102 establish the kind of the tyvar:
103 * For a group of type and class decls, it's just the group, not
104 the rest of the program
105 * For a tyvar bound in a pattern type signature, its the types
106 mentioned in the other type signatures in that bunch of patterns
107 * For a tyvar bound in a RULE, it's the type signatures on other
108 universally quantified variables in the rule
110 Note that this may occasionally give surprising results. For example:
112 data T a b = MkT (a b)
114 Here we deduce a::*->*, b::*.
115 But equally valid would be
116 a::(*->*)-> *, b::*->*
119 kcTyVarScope :: [HsTyVarBndr Name]
120 -> TcM s a -- The kind checker
121 -> TcM s [(Name,Kind)]
122 -- Do a kind check to find out the kinds of the type variables
123 -- Then return a bunch of name-kind pairs, from which to
124 -- construct the type variables. We don't return the tyvars
125 -- themselves because sometimes we want mutable ones and
126 -- sometimes we want immutable ones.
128 kcTyVarScope [] kind_check = returnTc []
129 -- A useful short cut for a common case!
131 kcTyVarScope tv_names kind_check
132 = kcHsTyVars tv_names `thenNF_Tc` \ tv_names_w_kinds ->
133 tcExtendKindEnv tv_names_w_kinds kind_check `thenTc_`
134 zonkKindEnv tv_names_w_kinds
139 kcHsTyVar :: HsTyVarBndr name -> NF_TcM s (name, TcKind)
140 kcHsTyVars :: [HsTyVarBndr name] -> NF_TcM s [(name, TcKind)]
142 kcHsTyVar (UserTyVar name) = newKindVar `thenNF_Tc` \ kind ->
143 returnNF_Tc (name, kind)
144 kcHsTyVar (IfaceTyVar name kind) = returnNF_Tc (name, kind)
146 kcHsTyVars tvs = mapNF_Tc kcHsTyVar tvs
148 ---------------------------
149 kcBoxedType :: RenamedHsType -> TcM s ()
150 -- The type ty must be a *boxed* *type*
152 = kcHsType ty `thenTc` \ kind ->
153 tcAddErrCtxt (typeKindCtxt ty) $
154 unifyKind boxedTypeKind kind
156 ---------------------------
157 kcTypeType :: RenamedHsType -> TcM s ()
158 -- The type ty must be a *type*, but it can be boxed or unboxed.
160 = kcHsType ty `thenTc` \ kind ->
161 tcAddErrCtxt (typeKindCtxt ty) $
162 unifyOpenTypeKind kind
164 ---------------------------
165 kcHsSigType, kcHsBoxedSigType :: RenamedHsType -> TcM s ()
166 -- Used for type signatures
167 kcHsSigType = kcTypeType
168 kcHsBoxedSigType = kcBoxedType
170 ---------------------------
171 kcHsType :: RenamedHsType -> TcM s TcKind
172 kcHsType (HsTyVar name)
173 = tcLookupTy name `thenTc` \ thing ->
175 ATyVar tv -> returnTc (tyVarKind tv)
176 ATyCon tc -> returnTc (tyConKind tc)
177 AThing k -> returnTc k
178 other -> failWithTc (wrongThingErr "type" thing name)
180 kcHsType (HsUsgTy _ ty) = kcHsType ty
181 kcHsType (HsUsgForAllTy _ ty) = kcHsType ty
183 kcHsType (HsListTy ty)
184 = kcBoxedType ty `thenTc` \ tau_ty ->
185 returnTc boxedTypeKind
187 kcHsType (HsTupleTy (HsTupCon _ Boxed) tys)
188 = mapTc kcBoxedType tys `thenTc_`
189 returnTc boxedTypeKind
191 kcHsType ty@(HsTupleTy (HsTupCon _ Unboxed) tys)
192 = failWithTc (unboxedTupleErr ty)
193 -- Unboxed tuples are illegal everywhere except
194 -- just after a function arrow (see kcFunResType)
196 kcHsType (HsFunTy ty1 ty2)
197 = kcTypeType ty1 `thenTc_`
198 kcFunResType ty2 `thenTc_`
199 returnTc boxedTypeKind
201 kcHsType (HsPredTy pred)
202 = kcHsPred pred `thenTc_`
203 returnTc boxedTypeKind
205 kcHsType ty@(HsAppTy ty1 ty2)
206 = kcHsType ty1 `thenTc` \ tc_kind ->
207 kcHsType ty2 `thenTc` \ arg_kind ->
209 tcAddErrCtxt (appKindCtxt (ppr ty)) $
210 case splitFunTy_maybe tc_kind of
211 Just (arg_kind', res_kind)
212 -> unifyKind arg_kind arg_kind' `thenTc_`
215 Nothing -> newKindVar `thenNF_Tc` \ res_kind ->
216 unifyKind tc_kind (mkArrowKind arg_kind res_kind) `thenTc_`
219 kcHsType (HsForAllTy (Just tv_names) context ty)
220 = kcHsTyVars tv_names `thenNF_Tc` \ kind_env ->
221 tcExtendKindEnv kind_env $
222 kcHsContext context `thenTc_`
224 -- Context behaves like a function type
225 -- This matters. Return-unboxed-tuple analysis can
226 -- give overloaded functions like
227 -- f :: forall a. Num a => (# a->a, a->a #)
228 -- And we want these to get through the type checker
232 kcFunResType ty `thenTc_`
233 returnTc boxedTypeKind
235 kcFunResType :: RenamedHsType -> TcM s TcKind
236 -- The only place an unboxed tuple type is allowed
237 -- is at the right hand end of an arrow
238 kcFunResType (HsTupleTy (HsTupCon _ Unboxed) tys)
239 = mapTc kcTypeType tys `thenTc_`
240 returnTc unboxedTypeKind
242 kcFunResType ty = kcHsType ty
245 ---------------------------
246 kcHsContext ctxt = mapTc_ kcHsPred ctxt
248 kcHsPred :: RenamedHsPred -> TcM s ()
249 kcHsPred pred@(HsPIParam name ty)
250 = tcAddErrCtxt (appKindCtxt (ppr pred)) $
253 kcHsPred pred@(HsPClass cls tys)
254 = tcAddErrCtxt (appKindCtxt (ppr pred)) $
255 tcLookupTy cls `thenNF_Tc` \ thing ->
257 AClass cls -> returnTc (tyConKind (classTyCon cls))
258 AThing kind -> returnTc kind
259 other -> failWithTc (wrongThingErr "class" thing cls)) `thenTc` \ kind ->
260 mapTc kcHsType tys `thenTc` \ arg_kinds ->
261 unifyKind kind (mkArrowKinds arg_kinds boxedTypeKind)
264 %************************************************************************
266 \subsection{Checking types}
268 %************************************************************************
270 tcHsSigType and tcHsBoxedSigType
271 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
273 tcHsSigType and tcHsBoxedSigType are used for type signatures written by the programmer
275 * We hoist any inner for-alls to the top
277 * Notice that we kind-check first, because the type-check assumes
278 that the kinds are already checked.
280 * They are only called when there are no kind vars in the environment
281 so the kind returned is indeed a Kind not a TcKind
284 tcHsSigType :: RenamedHsType -> TcM s TcType
286 = kcTypeType ty `thenTc_`
287 tcHsType ty `thenTc` \ ty' ->
288 returnTc (hoistForAllTys ty')
290 tcHsBoxedSigType :: RenamedHsType -> TcM s Type
292 = kcBoxedType ty `thenTc_`
293 tcHsType ty `thenTc` \ ty' ->
294 returnTc (hoistForAllTys ty')
298 tcHsType, the main work horse
299 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
302 tcHsType :: RenamedHsType -> TcM s Type
303 tcHsType ty@(HsTyVar name)
306 tcHsType (HsListTy ty)
307 = tcHsType ty `thenTc` \ tau_ty ->
308 returnTc (mkListTy tau_ty)
310 tcHsType (HsTupleTy (HsTupCon _ boxity) tys)
311 = mapTc tcHsType tys `thenTc` \ tau_tys ->
312 returnTc (mkTupleTy boxity (length tys) tau_tys)
314 tcHsType (HsFunTy ty1 ty2)
315 = tcHsType ty1 `thenTc` \ tau_ty1 ->
316 tcHsType ty2 `thenTc` \ tau_ty2 ->
317 returnTc (mkFunTy tau_ty1 tau_ty2)
319 tcHsType (HsAppTy ty1 ty2)
322 tcHsType (HsPredTy pred)
323 = tcClassAssertion True pred `thenTc` \ pred' ->
324 returnTc (mkPredTy pred')
326 tcHsType (HsUsgTy usg ty)
327 = newUsg usg `thenTc` \ usg' ->
328 tcHsType ty `thenTc` \ tc_ty ->
329 returnTc (mkUsgTy usg' tc_ty)
331 newUsg usg = case usg of
332 HsUsOnce -> returnTc UsOnce
333 HsUsMany -> returnTc UsMany
334 HsUsVar uv_name -> tcLookupUVar uv_name `thenTc` \ uv ->
337 tcHsType (HsUsgForAllTy uv_name ty)
339 uv = mkNamedUVar uv_name
341 tcExtendUVarEnv uv_name uv $
342 tcHsType ty `thenTc` \ tc_ty ->
343 returnTc (mkUsForAllTy uv tc_ty)
345 tcHsType full_ty@(HsForAllTy (Just tv_names) ctxt ty)
346 = kcTyVarScope tv_names
347 (kcHsContext ctxt `thenTc_` kcFunResType ty) `thenTc` \ tv_kinds ->
349 forall_tyvars = mkImmutTyVars tv_kinds
351 tcExtendTyVarEnv forall_tyvars $
352 tcContext ctxt `thenTc` \ theta ->
353 tcHsType ty `thenTc` \ tau ->
355 -- Check for ambiguity
356 -- forall V. P => tau
357 -- is ambiguous if P contains generic variables
358 -- (i.e. one of the Vs) that are not mentioned in tau
360 -- However, we need to take account of functional dependencies
361 -- when we speak of 'mentioned in tau'. Example:
362 -- class C a b | a -> b where ...
364 -- forall x y. (C x y) => x
365 -- is not ambiguous because x is mentioned and x determines y
367 -- NOTE: In addition, GHC insists that at least one type variable
368 -- in each constraint is in V. So we disallow a type like
369 -- forall a. Eq b => b -> b
370 -- even in a scope where b is in scope.
371 -- This is the is_free test below.
373 tau_vars = tyVarsOfType tau
374 fds = instFunDepsOfTheta theta
375 tvFundep = tyVarFunDep fds
376 extended_tau_vars = oclose tvFundep tau_vars
377 is_ambig ct_var = (ct_var `elem` forall_tyvars) &&
378 not (ct_var `elemUFM` extended_tau_vars)
379 is_free ct_var = not (ct_var `elem` forall_tyvars)
381 check_pred pred = checkTc (not any_ambig) (ambigErr pred full_ty) `thenTc_`
382 checkTc (not all_free) (freeErr pred full_ty)
384 ct_vars = varSetElems (tyVarsOfPred pred)
385 any_ambig = is_source_polytype && any is_ambig ct_vars
386 all_free = all is_free ct_vars
388 -- Check ambiguity only for source-program types, not
389 -- for types coming from inteface files. The latter can
390 -- legitimately have ambiguous types. Example
391 -- class S a where s :: a -> (Int,Int)
392 -- instance S Char where s _ = (1,1)
393 -- f:: S a => [a] -> Int -> (Int,Int)
394 -- f (_::[a]) x = (a*x,b)
395 -- where (a,b) = s (undefined::a)
396 -- Here the worker for f gets the type
397 -- fw :: forall a. S a => Int -> (# Int, Int #)
399 -- If the list of tv_names is empty, we have a monotype,
400 -- and then we don't need to check for ambiguity either,
401 -- because the test can't fail (see is_ambig).
402 is_source_polytype = case tv_names of
403 (UserTyVar _ : _) -> True
406 mapTc check_pred theta `thenTc_`
407 returnTc (mkSigmaTy forall_tyvars theta tau)
410 Help functions for type applications
411 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
414 tc_app (HsAppTy ty1 ty2) tys
415 = tc_app ty1 (ty2:tys)
418 = tcAddErrCtxt (appKindCtxt pp_app) $
419 mapTc tcHsType tys `thenTc` \ arg_tys ->
420 tc_fun_type ty arg_tys
422 pp_app = ppr ty <+> sep (map pprParendHsType tys)
424 -- (tc_fun_type ty arg_tys) returns (mkAppTys ty arg_tys)
425 -- But not quite; for synonyms it checks the correct arity, and builds a SynTy
426 -- hence the rather strange functionality.
428 tc_fun_type (HsTyVar name) arg_tys
429 = tcLookupTy name `thenTc` \ thing ->
431 ATyVar tv -> returnTc (mkAppTys (mkTyVarTy tv) arg_tys)
433 ATyCon tc | isSynTyCon tc -> checkTc arity_ok err_msg `thenTc_`
434 returnTc (mkAppTys (mkSynTy tc (take arity arg_tys))
435 (drop arity arg_tys))
437 | otherwise -> returnTc (mkTyConApp tc arg_tys)
440 arity_ok = arity <= n_args
441 arity = tyConArity tc
442 -- It's OK to have an *over-applied* type synonym
443 -- data Tree a b = ...
444 -- type Foo a = Tree [a]
445 -- f :: Foo a b -> ...
446 err_msg = arityErr "Type synonym" name arity n_args
447 n_args = length arg_tys
449 other -> failWithTc (wrongThingErr "type constructor" thing name)
451 tc_fun_type ty arg_tys
452 = tcHsType ty `thenTc` \ fun_ty ->
453 returnNF_Tc (mkAppTys fun_ty arg_tys)
460 tcClassContext :: RenamedContext -> TcM s ClassContext
461 -- Used when we are expecting a ClassContext (i.e. no implicit params)
462 tcClassContext context
463 = tcContext context `thenTc` \ theta ->
464 returnTc (classesOfPreds theta)
466 tcContext :: RenamedContext -> TcM s ThetaType
467 tcContext context = mapTc (tcClassAssertion False) context
469 tcClassAssertion ccall_ok assn@(HsPClass class_name tys)
470 = tcAddErrCtxt (appKindCtxt (ppr assn)) $
471 mapTc tcHsType tys `thenTc` \ arg_tys ->
472 tcLookupTy class_name `thenTc` \ thing ->
474 AClass clas -> checkTc (arity == n_tys) err `thenTc_`
475 returnTc (Class clas arg_tys)
477 arity = classArity clas
479 err = arityErr "Class" class_name arity n_tys
481 other -> failWithTc (wrongThingErr "class" thing class_name)
483 tcClassAssertion ccall_ok assn@(HsPIParam name ty)
484 = tcAddErrCtxt (appKindCtxt (ppr assn)) $
485 tcHsType ty `thenTc` \ arg_ty ->
486 returnTc (IParam name arg_ty)
490 %************************************************************************
492 \subsection{Type variables, with knot tying!}
494 %************************************************************************
497 mkImmutTyVars :: [(Name,Kind)] -> [TyVar]
498 newSigTyVars :: [(Name,Kind)] -> NF_TcM s [TcTyVar]
500 mkImmutTyVars pairs = [mkTyVar name kind | (name, kind) <- pairs]
501 newSigTyVars pairs = listNF_Tc [tcNewSigTyVar name kind | (name,kind) <- pairs]
503 mkTyClTyVars :: Kind -- Kind of the tycon or class
504 -> [HsTyVarBndr Name]
506 mkTyClTyVars kind tyvar_names
507 = mkImmutTyVars tyvars_w_kinds
509 (tyvars_w_kinds, _) = zipFunTys (hsTyVarNames tyvar_names) kind
513 %************************************************************************
515 \subsection{Signatures}
517 %************************************************************************
519 @tcSigs@ checks the signatures for validity, and returns a list of
520 {\em freshly-instantiated} signatures. That is, the types are already
521 split up, and have fresh type variables installed. All non-type-signature
522 "RenamedSigs" are ignored.
524 The @TcSigInfo@ contains @TcTypes@ because they are unified with
525 the variable's type, and after that checked to see whether they've
531 Name -- N, the Name in corresponding binding
533 TcId -- *Polymorphic* binder for this value...
540 TcId -- *Monomorphic* binder for this value
541 -- Does *not* have name = N
544 [Inst] -- Empty if theta is null, or
545 -- (method mono_id) otherwise
547 SrcLoc -- Of the signature
549 instance Outputable TcSigInfo where
550 ppr (TySigInfo nm id tyvars theta tau _ inst loc) =
551 ppr nm <+> ptext SLIT("::") <+> ppr tyvars <+> ppr theta <+> ptext SLIT("=>") <+> ppr tau
553 maybeSig :: [TcSigInfo] -> Name -> Maybe (TcSigInfo)
554 -- Search for a particular signature
555 maybeSig [] name = Nothing
556 maybeSig (sig@(TySigInfo sig_name _ _ _ _ _ _ _) : sigs) name
557 | name == sig_name = Just sig
558 | otherwise = maybeSig sigs name
563 tcTySig :: RenamedSig -> TcM s TcSigInfo
565 tcTySig (Sig v ty src_loc)
566 = tcAddSrcLoc src_loc $
567 tcAddErrCtxt (tcsigCtxt v) $
568 tcHsSigType ty `thenTc` \ sigma_tc_ty ->
569 mkTcSig (mkVanillaId v sigma_tc_ty) src_loc `thenNF_Tc` \ sig ->
572 mkTcSig :: TcId -> SrcLoc -> NF_TcM s TcSigInfo
573 mkTcSig poly_id src_loc
574 = -- Instantiate this type
575 -- It's important to do this even though in the error-free case
576 -- we could just split the sigma_tc_ty (since the tyvars don't
577 -- unified with anything). But in the case of an error, when
578 -- the tyvars *do* get unified with something, we want to carry on
579 -- typechecking the rest of the program with the function bound
580 -- to a pristine type, namely sigma_tc_ty
582 (tyvars, rho) = splitForAllTys (idType poly_id)
584 mapNF_Tc tcInstSigVar tyvars `thenNF_Tc` \ tyvars' ->
585 -- Make *signature* type variables
588 tyvar_tys' = mkTyVarTys tyvars'
589 rho' = substTy (mkTopTyVarSubst tyvars tyvar_tys') rho
590 -- mkTopTyVarSubst because the tyvars' are fresh
591 (theta', tau') = splitRhoTy rho'
592 -- This splitRhoTy tries hard to make sure that tau' is a type synonym
593 -- wherever possible, which can improve interface files.
595 newMethodWithGivenTy SignatureOrigin
598 theta' tau' `thenNF_Tc` \ inst ->
599 -- We make a Method even if it's not overloaded; no harm
600 instFunDeps SignatureOrigin theta' `thenNF_Tc` \ fds ->
602 returnNF_Tc (TySigInfo name poly_id tyvars' theta' tau' (instToIdBndr inst) (inst : fds) src_loc)
604 name = idName poly_id
609 %************************************************************************
611 \subsection{Checking signature type variables}
613 %************************************************************************
615 @checkSigTyVars@ is used after the type in a type signature has been unified with
616 the actual type found. It then checks that the type variables of the type signature
618 (a) Still all type variables
619 eg matching signature [a] against inferred type [(p,q)]
620 [then a will be unified to a non-type variable]
622 (b) Still all distinct
623 eg matching signature [(a,b)] against inferred type [(p,p)]
624 [then a and b will be unified together]
626 (c) Not mentioned in the environment
627 eg the signature for f in this:
633 Here, f is forced to be monorphic by the free occurence of x.
635 (d) Not (unified with another type variable that is) in scope.
636 eg f x :: (r->r) = (\y->y) :: forall a. a->r
637 when checking the expression type signature, we find that
638 even though there is nothing in scope whose type mentions r,
639 nevertheless the type signature for the expression isn't right.
641 Another example is in a class or instance declaration:
643 op :: forall b. a -> b
645 Here, b gets unified with a
647 Before doing this, the substitution is applied to the signature type variable.
649 We used to have the notion of a "DontBind" type variable, which would
650 only be bound to itself or nothing. Then points (a) and (b) were
651 self-checking. But it gave rise to bogus consequential error messages.
654 f = (*) -- Monomorphic
659 Here, we get a complaint when checking the type signature for g,
660 that g isn't polymorphic enough; but then we get another one when
661 dealing with the (Num x) context arising from f's definition;
662 we try to unify x with Int (to default it), but find that x has already
663 been unified with the DontBind variable "a" from g's signature.
664 This is really a problem with side-effecting unification; we'd like to
665 undo g's effects when its type signature fails, but unification is done
666 by side effect, so we can't (easily).
668 So we revert to ordinary type variables for signatures, and try to
669 give a helpful message in checkSigTyVars.
672 checkSigTyVars :: [TcTyVar] -- Universally-quantified type variables in the signature
673 -> TcTyVarSet -- Tyvars that are free in the type signature
674 -- These should *already* be in the global-var set, and are
675 -- used here only to improve the error message
676 -> TcM s [TcTyVar] -- Zonked signature type variables
678 checkSigTyVars [] free = returnTc []
680 checkSigTyVars sig_tyvars free_tyvars
681 = zonkTcTyVars sig_tyvars `thenNF_Tc` \ sig_tys ->
682 tcGetGlobalTyVars `thenNF_Tc` \ globals ->
684 checkTcM (all_ok sig_tys globals)
685 (complain sig_tys globals) `thenTc_`
687 returnTc (map (getTyVar "checkSigTyVars") sig_tys)
691 all_ok (ty:tys) acc = case getTyVar_maybe ty of
692 Nothing -> False -- Point (a)
693 Just tv | tv `elemVarSet` acc -> False -- Point (b) or (c)
694 | otherwise -> all_ok tys (acc `extendVarSet` tv)
697 complain sig_tys globals
698 = -- For the in-scope ones, zonk them and construct a map
699 -- from the zonked tyvar to the in-scope one
700 -- If any of the in-scope tyvars zonk to a type, then ignore them;
701 -- that'll be caught later when we back up to their type sig
702 tcGetInScopeTyVars `thenNF_Tc` \ in_scope_tvs ->
703 zonkTcTyVars in_scope_tvs `thenNF_Tc` \ in_scope_tys ->
705 in_scope_assoc = [ (zonked_tv, in_scope_tv)
706 | (z_ty, in_scope_tv) <- in_scope_tys `zip` in_scope_tvs,
707 Just zonked_tv <- [getTyVar_maybe z_ty]
709 in_scope_env = mkVarEnv in_scope_assoc
712 -- "check" checks each sig tyvar in turn
714 (env2, in_scope_env, [])
715 (tidy_tvs `zip` tidy_tys) `thenNF_Tc` \ (env3, _, msgs) ->
717 failWithTcM (env3, main_msg $$ nest 4 (vcat msgs))
719 (env1, tidy_tvs) = mapAccumL tidyTyVar emptyTidyEnv sig_tyvars
720 (env2, tidy_tys) = tidyOpenTypes env1 sig_tys
722 main_msg = ptext SLIT("Inferred type is less polymorphic than expected")
724 check (env, acc, msgs) (sig_tyvar,ty)
725 -- sig_tyvar is from the signature;
726 -- ty is what you get if you zonk sig_tyvar and then tidy it
728 -- acc maps a zonked type variable back to a signature type variable
729 = case getTyVar_maybe ty of {
730 Nothing -> -- Error (a)!
731 returnNF_Tc (env, acc, unify_msg sig_tyvar (ppr ty) : msgs) ;
735 case lookupVarEnv acc tv of {
736 Just sig_tyvar' -> -- Error (b) or (d)!
737 returnNF_Tc (env, acc, unify_msg sig_tyvar (ppr sig_tyvar') : msgs) ;
741 if tv `elemVarSet` globals -- Error (c)! Type variable escapes
742 -- The least comprehensible, so put it last
743 then tcGetValueEnv `thenNF_Tc` \ ve ->
744 find_globals tv env [] (valueEnvIds ve) `thenNF_Tc` \ (env1, globs) ->
745 find_frees tv env1 [] (varSetElems free_tyvars) `thenNF_Tc` \ (env2, frees) ->
746 returnNF_Tc (env2, acc, escape_msg sig_tyvar tv globs frees : msgs)
749 returnNF_Tc (env, extendVarEnv acc tv sig_tyvar, msgs)
752 -- find_globals looks at the value environment and finds values
753 -- whose types mention the offending type variable. It has to be
754 -- careful to zonk the Id's type first, so it has to be in the monad.
755 -- We must be careful to pass it a zonked type variable, too.
756 find_globals tv tidy_env acc []
757 = returnNF_Tc (tidy_env, acc)
759 find_globals tv tidy_env acc (id:ids)
760 | not (isLocallyDefined id) ||
761 isEmptyVarSet (idFreeTyVars id)
762 = find_globals tv tidy_env acc ids
765 = zonkTcType (idType id) `thenNF_Tc` \ id_ty ->
766 if tv `elemVarSet` tyVarsOfType id_ty then
768 (tidy_env', id_ty') = tidyOpenType tidy_env id_ty
769 acc' = (idName id, id_ty') : acc
771 find_globals tv tidy_env' acc' ids
773 find_globals tv tidy_env acc ids
775 find_frees tv tidy_env acc []
776 = returnNF_Tc (tidy_env, acc)
777 find_frees tv tidy_env acc (ftv:ftvs)
778 = zonkTcTyVar ftv `thenNF_Tc` \ ty ->
779 if tv `elemVarSet` tyVarsOfType ty then
781 (tidy_env', ftv') = tidyTyVar tidy_env ftv
783 find_frees tv tidy_env' (ftv':acc) ftvs
785 find_frees tv tidy_env acc ftvs
788 escape_msg sig_tv tv globs frees
789 = mk_msg sig_tv <+> ptext SLIT("escapes") $$
790 if not (null globs) then
791 vcat [pp_it <+> ptext SLIT("is mentioned in the environment"),
792 ptext SLIT("The following variables in the environment mention") <+> quotes (ppr tv),
793 nest 2 (vcat_first 10 [ppr name <+> dcolon <+> ppr ty | (name,ty) <- globs])
795 else if not (null frees) then
796 vcat [ptext SLIT("It is reachable from the type variable(s)") <+> pprQuotedList frees,
797 nest 2 (ptext SLIT("which") <+> is_are <+> ptext SLIT("free in the signature"))
800 empty -- Sigh. It's really hard to give a good error message
801 -- all the time. One bad case is an existential pattern match
803 is_are | isSingleton frees = ptext SLIT("is")
804 | otherwise = ptext SLIT("are")
805 pp_it | sig_tv /= tv = ptext SLIT("It unifies with") <+> quotes (ppr tv) <> comma <+> ptext SLIT("which")
806 | otherwise = ptext SLIT("It")
808 vcat_first :: Int -> [SDoc] -> SDoc
809 vcat_first n [] = empty
810 vcat_first 0 (x:xs) = text "...others omitted..."
811 vcat_first n (x:xs) = x $$ vcat_first (n-1) xs
813 unify_msg tv thing = mk_msg tv <+> ptext SLIT("is unified with") <+> quotes thing
814 mk_msg tv = ptext SLIT("Quantified type variable") <+> quotes (ppr tv)
817 These two context are used with checkSigTyVars
820 sigCtxt :: Message -> [TcTyVar] -> TcThetaType -> TcTauType
821 -> TidyEnv -> NF_TcM s (TidyEnv, Message)
822 sigCtxt when sig_tyvars sig_theta sig_tau tidy_env
823 = zonkTcType sig_tau `thenNF_Tc` \ actual_tau ->
825 (env1, tidy_sig_tyvars) = tidyTyVars tidy_env sig_tyvars
826 (env2, tidy_sig_rho) = tidyOpenType env1 (mkRhoTy sig_theta sig_tau)
827 (env3, tidy_actual_tau) = tidyOpenType env2 actual_tau
828 msg = vcat [ptext SLIT("Signature type: ") <+> pprType (mkForAllTys tidy_sig_tyvars tidy_sig_rho),
829 ptext SLIT("Type to generalise:") <+> pprType tidy_actual_tau,
833 returnNF_Tc (env3, msg)
835 sigPatCtxt bound_tvs bound_ids tidy_env
837 sep [ptext SLIT("When checking a pattern that binds"),
838 nest 4 (vcat (zipWith ppr_id show_ids tidy_tys))])
840 show_ids = filter is_interesting bound_ids
841 is_interesting id = any (`elemVarSet` idFreeTyVars id) bound_tvs
843 (env1, tidy_tys) = tidyOpenTypes tidy_env (map idType show_ids)
844 ppr_id id ty = ppr id <+> dcolon <+> ppr ty
845 -- Don't zonk the types so we get the separate, un-unified versions
849 %************************************************************************
851 \subsection{Errors and contexts}
853 %************************************************************************
856 tcsigCtxt v = ptext SLIT("In a type signature for") <+> quotes (ppr v)
858 typeKindCtxt :: RenamedHsType -> Message
859 typeKindCtxt ty = sep [ptext SLIT("When checking that"),
860 nest 2 (quotes (ppr ty)),
861 ptext SLIT("is a type")]
863 appKindCtxt :: SDoc -> Message
864 appKindCtxt pp = ptext SLIT("When checking kinds in") <+> quotes pp
866 wrongThingErr expected actual name
867 = pp_actual actual <+> quotes (ppr name) <+> ptext SLIT("used as a") <+> text expected
869 pp_actual (ATyCon _) = ptext SLIT("Type constructor")
870 pp_actual (AClass _) = ptext SLIT("Class")
871 pp_actual (ATyVar _) = ptext SLIT("Type variable")
872 pp_actual (AThing _) = ptext SLIT("Utterly bogus")
875 = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
876 nest 4 (ptext SLIT("for the type:") <+> ppr ty),
877 nest 4 (ptext SLIT("Each forall'd type variable mentioned by the constraint must appear after the =>"))]
880 = sep [ptext SLIT("The constraint") <+> quotes (pprPred pred) <+>
881 ptext SLIT("does not mention any of the universally quantified type variables"),
882 nest 4 (ptext SLIT("in the type") <+> quotes (ppr ty))
886 = sep [ptext (SLIT("Illegal unboxed tuple as a function or contructor argument:")), nest 4 (ppr ty)]