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 tcTyVars, tcHsTyVars, 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, tcExtendKindEnv, tcLookupTy,
28 tcGetEnv, tcEnvTyVars, tcEnvTcIds,
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 )
57 import ErrUtils ( Message )
58 import TyCon ( TyCon, isSynTyCon, tyConArity, tyConKind, tyConName )
59 import Class ( ClassContext, classArity, classTyCon )
60 import Name ( Name, isLocallyDefined )
61 import TysWiredIn ( mkListTy, mkTupleTy, genUnitTyCon )
62 import UniqFM ( elemUFM )
63 import BasicTypes ( Boxity(..) )
64 import SrcLoc ( SrcLoc )
65 import Util ( mapAccumL, isSingleton )
71 %************************************************************************
73 \subsection{Kind checking}
75 %************************************************************************
79 When we come across the binding site for some type variables, we
82 1. Figure out what kind each tyvar has
84 2. Create suitably-kinded tyvars,
86 and typecheck the body
88 To do step 1, we proceed thus:
90 1a. Bind each type variable to a kind variable
91 1b. Apply the kind checker
92 1c. Zonk the resulting kinds
94 The kind checker is passed to tcHsTyVars as an argument.
96 For example, when we find
97 (forall a m. m a -> m a)
98 we bind a,m to kind varibles and kind-check (m a -> m a). This
99 makes a get kind *, and m get kind *->*. Now we typecheck (m a -> m a)
100 in an environment that binds a and m suitably.
102 The kind checker passed to tcHsTyVars needs to look at enough to
103 establish the kind of the tyvar:
104 * For a group of type and class decls, it's just the group, not
105 the rest of the program
106 * For a tyvar bound in a pattern type signature, its the types
107 mentioned in the other type signatures in that bunch of patterns
108 * For a tyvar bound in a RULE, it's the type signatures on other
109 universally quantified variables in the rule
111 Note that this may occasionally give surprising results. For example:
113 data T a b = MkT (a b)
115 Here we deduce a::*->*, b::*.
116 But equally valid would be
117 a::(*->*)-> *, b::*->*
120 tcHsTyVars :: [HsTyVarBndr Name]
121 -> TcM a -- The kind checker
122 -> ([TyVar] -> TcM b)
125 tcHsTyVars [] kind_check thing_inside = thing_inside []
126 -- A useful short cut for a common case!
128 tcHsTyVars tv_names kind_check thing_inside
129 = kcHsTyVars tv_names `thenNF_Tc` \ tv_names_w_kinds ->
130 tcExtendKindEnv tv_names_w_kinds kind_check `thenTc_`
131 zonkKindEnv tv_names_w_kinds `thenNF_Tc` \ tvs_w_kinds ->
133 tyvars = mkImmutTyVars tvs_w_kinds
135 tcExtendTyVarEnv tyvars (thing_inside tyvars)
138 -> TcM a -- The kind checker
140 tcTyVars [] kind_check = returnTc []
142 tcTyVars tv_names kind_check
143 = mapNF_Tc newNamedKindVar tv_names `thenTc` \ kind_env ->
144 tcExtendKindEnv kind_env kind_check `thenTc_`
145 zonkKindEnv kind_env `thenNF_Tc` \ tvs_w_kinds ->
146 listNF_Tc [tcNewSigTyVar name kind | (name,kind) <- tvs_w_kinds]
151 kcHsTyVar :: HsTyVarBndr name -> NF_TcM (name, TcKind)
152 kcHsTyVars :: [HsTyVarBndr name] -> NF_TcM [(name, TcKind)]
154 kcHsTyVar (UserTyVar name) = newNamedKindVar name
155 kcHsTyVar (IfaceTyVar name kind) = returnNF_Tc (name, kind)
157 kcHsTyVars tvs = mapNF_Tc kcHsTyVar tvs
159 newNamedKindVar name = newKindVar `thenNF_Tc` \ kind ->
160 returnNF_Tc (name, kind)
162 ---------------------------
163 kcBoxedType :: RenamedHsType -> TcM ()
164 -- The type ty must be a *boxed* *type*
166 = kcHsType ty `thenTc` \ kind ->
167 tcAddErrCtxt (typeKindCtxt ty) $
168 unifyKind boxedTypeKind kind
170 ---------------------------
171 kcTypeType :: RenamedHsType -> TcM ()
172 -- The type ty must be a *type*, but it can be boxed or unboxed.
174 = kcHsType ty `thenTc` \ kind ->
175 tcAddErrCtxt (typeKindCtxt ty) $
176 unifyOpenTypeKind kind
178 ---------------------------
179 kcHsSigType, kcHsBoxedSigType :: RenamedHsType -> TcM ()
180 -- Used for type signatures
181 kcHsSigType = kcTypeType
182 kcHsBoxedSigType = kcBoxedType
184 ---------------------------
185 kcHsType :: RenamedHsType -> TcM TcKind
186 kcHsType (HsTyVar name) = kcTyVar name
187 kcHsType (HsUsgTy _ ty) = kcHsType ty
188 kcHsType (HsUsgForAllTy _ ty) = kcHsType ty
190 kcHsType (HsListTy ty)
191 = kcBoxedType ty `thenTc` \ tau_ty ->
192 returnTc boxedTypeKind
194 kcHsType (HsTupleTy (HsTupCon _ Boxed) tys)
195 = mapTc kcBoxedType tys `thenTc_`
196 returnTc boxedTypeKind
198 kcHsType ty@(HsTupleTy (HsTupCon _ Unboxed) tys)
199 = failWithTc (unboxedTupleErr ty)
200 -- Unboxed tuples are illegal everywhere except
201 -- just after a function arrow (see kcFunResType)
203 kcHsType (HsFunTy ty1 ty2)
204 = kcTypeType ty1 `thenTc_`
205 kcFunResType ty2 `thenTc_`
206 returnTc boxedTypeKind
208 kcHsType ty@(HsOpTy ty1 op ty2)
209 = kcTyVar op `thenTc` \ op_kind ->
210 kcHsType ty1 `thenTc` \ ty1_kind ->
211 kcHsType ty2 `thenTc` \ ty2_kind ->
212 tcAddErrCtxt (appKindCtxt (ppr ty)) $
213 kcAppKind op_kind ty1_kind `thenTc` \ op_kind' ->
214 kcAppKind op_kind' ty2_kind
216 kcHsType (HsPredTy pred)
217 = kcHsPred pred `thenTc_`
218 returnTc boxedTypeKind
220 kcHsType ty@(HsAppTy ty1 ty2)
221 = kcHsType ty1 `thenTc` \ tc_kind ->
222 kcHsType ty2 `thenTc` \ arg_kind ->
223 tcAddErrCtxt (appKindCtxt (ppr ty)) $
224 kcAppKind tc_kind arg_kind
226 kcHsType (HsForAllTy (Just tv_names) context ty)
227 = kcHsTyVars tv_names `thenNF_Tc` \ kind_env ->
228 tcExtendKindEnv kind_env $
229 kcHsContext context `thenTc_`
231 -- Context behaves like a function type
232 -- This matters. Return-unboxed-tuple analysis can
233 -- give overloaded functions like
234 -- f :: forall a. Num a => (# a->a, a->a #)
235 -- And we want these to get through the type checker
239 kcFunResType ty `thenTc_`
240 returnTc boxedTypeKind
242 ---------------------------
243 kcTyVar name -- Could be a tyvar or a tycon
244 = tcLookup name `thenTc` \ thing ->
246 ATyVar tv -> returnTc (tyVarKind tv) ;
247 AThing k -> returnTc k ;
248 AGlobal (ATyCon tc) -> returnTc (tyConKind tc) ;
251 failWithTc (wrongThingErr "type" thing name)
254 ---------------------------
255 kcFunResType :: RenamedHsType -> TcM TcKind
256 -- The only place an unboxed tuple type is allowed
257 -- is at the right hand end of an arrow
258 kcFunResType (HsTupleTy (HsTupCon _ Unboxed) tys)
259 = mapTc kcTypeType tys `thenTc_`
260 returnTc unboxedTypeKind
262 kcFunResType ty = kcHsType ty
264 ---------------------------
265 kcAppKind fun_kind arg_kind
266 = case splitFunTy_maybe fun_kind of
267 Just (arg_kind', res_kind)
268 -> unifyKind arg_kind arg_kind' `thenTc_`
271 Nothing -> newKindVar `thenNF_Tc` \ res_kind ->
272 unifyKind fun_kind (mkArrowKind arg_kind res_kind) `thenTc_`
276 ---------------------------
277 kcHsContext ctxt = mapTc_ kcHsPred ctxt
279 kcHsPred :: RenamedHsPred -> TcM ()
280 kcHsPred pred@(HsPIParam name ty)
281 = tcAddErrCtxt (appKindCtxt (ppr pred)) $
284 kcHsPred pred@(HsPClass cls tys)
285 = tcAddErrCtxt (appKindCtxt (ppr pred)) $
286 tcLookupTy cls `thenNF_Tc` \ thing ->
288 AClass cls -> returnTc (tyConKind (classTyCon cls))
289 AThing kind -> returnTc kind
290 other -> failWithTc (wrongThingErr "class" (pp_thing thing) cls)) `thenTc` \ kind ->
291 mapTc kcHsType tys `thenTc` \ arg_kinds ->
292 unifyKind kind (mkArrowKinds arg_kinds boxedTypeKind)
295 %************************************************************************
297 \subsection{Checking types}
299 %************************************************************************
301 tcHsSigType and tcHsBoxedSigType
302 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
304 tcHsSigType and tcHsBoxedSigType are used for type signatures written by the programmer
306 * We hoist any inner for-alls to the top
308 * Notice that we kind-check first, because the type-check assumes
309 that the kinds are already checked.
311 * They are only called when there are no kind vars in the environment
312 so the kind returned is indeed a Kind not a TcKind
315 tcHsSigType :: RenamedHsType -> TcM TcType
317 = kcTypeType ty `thenTc_`
318 tcHsType ty `thenTc` \ ty' ->
319 returnTc (hoistForAllTys ty')
321 tcHsBoxedSigType :: RenamedHsType -> TcM Type
323 = kcBoxedType ty `thenTc_`
324 tcHsType ty `thenTc` \ ty' ->
325 returnTc (hoistForAllTys ty')
329 tcHsType, the main work horse
330 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
333 tcHsType :: RenamedHsType -> TcM Type
334 tcHsType ty@(HsTyVar name)
337 tcHsType (HsListTy ty)
338 = tcHsType ty `thenTc` \ tau_ty ->
339 returnTc (mkListTy tau_ty)
341 tcHsType (HsTupleTy (HsTupCon _ boxity) tys)
342 = mapTc tcHsType tys `thenTc` \ tau_tys ->
343 returnTc (mkTupleTy boxity (length tys) tau_tys)
345 tcHsType (HsFunTy ty1 ty2)
346 = tcHsType ty1 `thenTc` \ tau_ty1 ->
347 tcHsType ty2 `thenTc` \ tau_ty2 ->
348 returnTc (mkFunTy tau_ty1 tau_ty2)
352 returnTc (mkTyConApp genUnitTyCon [])
354 tcHsType (HsOpTy ty1 op ty2) =
355 tcHsType ty1 `thenTc` \ tau_ty1 ->
356 tcHsType ty2 `thenTc` \ tau_ty2 ->
357 tc_fun_type op [tau_ty1,tau_ty2]
359 tcHsType (HsAppTy ty1 ty2)
362 tcHsType (HsPredTy pred)
363 = tcClassAssertion True pred `thenTc` \ pred' ->
364 returnTc (mkPredTy pred')
366 tcHsType full_ty@(HsForAllTy (Just tv_names) ctxt ty)
368 kind_check = kcHsContext ctxt `thenTc_` kcFunResType ty
370 tcHsTyVars tv_names kind_check $ \ tyvars ->
371 tcContext ctxt `thenTc` \ theta ->
372 tcHsType ty `thenTc` \ tau ->
373 checkAmbiguity full_ty tyvars theta tau `thenTc_`
374 returnTc (mkSigmaTy tyvars theta tau)
376 -- Check for ambiguity
377 -- forall V. P => tau
378 -- is ambiguous if P contains generic variables
379 -- (i.e. one of the Vs) that are not mentioned in tau
381 -- However, we need to take account of functional dependencies
382 -- when we speak of 'mentioned in tau'. Example:
383 -- class C a b | a -> b where ...
385 -- forall x y. (C x y) => x
386 -- is not ambiguous because x is mentioned and x determines y
388 -- NOTE: In addition, GHC insists that at least one type variable
389 -- in each constraint is in V. So we disallow a type like
390 -- forall a. Eq b => b -> b
391 -- even in a scope where b is in scope.
392 -- This is the is_free test below.
394 checkAmbiguity full_ty forall_tyvars theta tau
395 = mapTc check_pred theta
397 tau_vars = tyVarsOfType tau
398 fds = instFunDepsOfTheta theta
399 tvFundep = tyVarFunDep fds
400 extended_tau_vars = oclose tvFundep tau_vars
402 is_ambig ct_var = (ct_var `elem` forall_tyvars) &&
403 not (ct_var `elemUFM` extended_tau_vars)
404 is_free ct_var = not (ct_var `elem` forall_tyvars)
406 check_pred pred = checkTc (not any_ambig) (ambigErr pred full_ty) `thenTc_`
407 checkTc (not all_free) (freeErr pred full_ty)
409 ct_vars = varSetElems (tyVarsOfPred pred)
410 all_free = all is_free ct_vars
411 any_ambig = is_source_polytype && any is_ambig ct_vars
413 -- Notes on the 'is_source_polytype' test above
414 -- Check ambiguity only for source-program types, not
415 -- for types coming from inteface files. The latter can
416 -- legitimately have ambiguous types. Example
417 -- class S a where s :: a -> (Int,Int)
418 -- instance S Char where s _ = (1,1)
419 -- f:: S a => [a] -> Int -> (Int,Int)
420 -- f (_::[a]) x = (a*x,b)
421 -- where (a,b) = s (undefined::a)
422 -- Here the worker for f gets the type
423 -- fw :: forall a. S a => Int -> (# Int, Int #)
425 -- If the list of tv_names is empty, we have a monotype,
426 -- and then we don't need to check for ambiguity either,
427 -- because the test can't fail (see is_ambig).
430 HsForAllTy (Just (UserTyVar _ : _)) _ _ -> True
434 Help functions for type applications
435 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
438 tc_app :: RenamedHsType -> [RenamedHsType] -> TcM Type
439 tc_app (HsAppTy ty1 ty2) tys
440 = tc_app ty1 (ty2:tys)
443 = tcAddErrCtxt (appKindCtxt pp_app) $
444 mapTc tcHsType tys `thenTc` \ arg_tys ->
446 HsTyVar fun -> tc_fun_type fun arg_tys
447 other -> tcHsType ty `thenTc` \ fun_ty ->
448 returnNF_Tc (mkAppTys fun_ty arg_tys)
450 pp_app = ppr ty <+> sep (map pprParendHsType tys)
452 -- (tc_fun_type ty arg_tys) returns (mkAppTys ty arg_tys)
453 -- But not quite; for synonyms it checks the correct arity, and builds a SynTy
454 -- hence the rather strange functionality.
456 tc_fun_type name arg_tys
457 = tcLookupGlobal name `thenTc` \ thing ->
459 ATyVar tv -> returnTc (mkAppTys (mkTyVarTy tv) arg_tys)
461 ATyCon tc | isSynTyCon tc -> checkTc arity_ok err_msg `thenTc_`
462 returnTc (mkAppTys (mkSynTy tc (take arity arg_tys))
463 (drop arity arg_tys))
465 | otherwise -> returnTc (mkTyConApp tc arg_tys)
468 arity_ok = arity <= n_args
469 arity = tyConArity tc
470 -- It's OK to have an *over-applied* type synonym
471 -- data Tree a b = ...
472 -- type Foo a = Tree [a]
473 -- f :: Foo a b -> ...
474 err_msg = arityErr "Type synonym" name arity n_args
475 n_args = length arg_tys
477 other -> failWithTc (wrongThingErr "type constructor" (pp_thing thing) name)
484 tcClassContext :: RenamedContext -> TcM ClassContext
485 -- Used when we are expecting a ClassContext (i.e. no implicit params)
486 tcClassContext context
487 = tcContext context `thenTc` \ theta ->
488 returnTc (classesOfPreds theta)
490 tcContext :: RenamedContext -> TcM ThetaType
491 tcContext context = mapTc (tcClassAssertion False) context
493 tcClassAssertion ccall_ok assn@(HsPClass class_name tys)
494 = tcAddErrCtxt (appKindCtxt (ppr assn)) $
495 mapTc tcHsType tys `thenTc` \ arg_tys ->
496 tcLookupTy class_name `thenTc` \ thing ->
498 AClass clas -> checkTc (arity == n_tys) err `thenTc_`
499 returnTc (Class clas arg_tys)
501 arity = classArity clas
503 err = arityErr "Class" class_name arity n_tys
505 other -> failWithTc (wrongThingErr "class" (ppr_thing thing) class_name)
507 tcClassAssertion ccall_ok assn@(HsPIParam name ty)
508 = tcAddErrCtxt (appKindCtxt (ppr assn)) $
509 tcHsType ty `thenTc` \ arg_ty ->
510 returnTc (IParam name arg_ty)
514 %************************************************************************
516 \subsection{Type variables, with knot tying!}
518 %************************************************************************
521 mkImmutTyVars :: [(Name,Kind)] -> [TyVar]
522 mkImmutTyVars pairs = [mkTyVar name kind | (name, kind) <- pairs]
524 mkTyClTyVars :: Kind -- Kind of the tycon or class
525 -> [HsTyVarBndr Name]
527 mkTyClTyVars kind tyvar_names
528 = mkImmutTyVars tyvars_w_kinds
530 (tyvars_w_kinds, _) = zipFunTys (hsTyVarNames tyvar_names) kind
534 %************************************************************************
536 \subsection{Signatures}
538 %************************************************************************
540 @tcSigs@ checks the signatures for validity, and returns a list of
541 {\em freshly-instantiated} signatures. That is, the types are already
542 split up, and have fresh type variables installed. All non-type-signature
543 "RenamedSigs" are ignored.
545 The @TcSigInfo@ contains @TcTypes@ because they are unified with
546 the variable's type, and after that checked to see whether they've
552 Name -- N, the Name in corresponding binding
554 TcId -- *Polymorphic* binder for this value...
561 TcId -- *Monomorphic* binder for this value
562 -- Does *not* have name = N
565 [Inst] -- Empty if theta is null, or
566 -- (method mono_id) otherwise
568 SrcLoc -- Of the signature
570 instance Outputable TcSigInfo where
571 ppr (TySigInfo nm id tyvars theta tau _ inst loc) =
572 ppr nm <+> ptext SLIT("::") <+> ppr tyvars <+> ppr theta <+> ptext SLIT("=>") <+> ppr tau
574 maybeSig :: [TcSigInfo] -> Name -> Maybe (TcSigInfo)
575 -- Search for a particular signature
576 maybeSig [] name = Nothing
577 maybeSig (sig@(TySigInfo sig_name _ _ _ _ _ _ _) : sigs) name
578 | name == sig_name = Just sig
579 | otherwise = maybeSig sigs name
584 tcTySig :: RenamedSig -> TcM TcSigInfo
586 tcTySig (Sig v ty src_loc)
587 = tcAddSrcLoc src_loc $
588 tcAddErrCtxt (tcsigCtxt v) $
589 tcHsSigType ty `thenTc` \ sigma_tc_ty ->
590 mkTcSig (mkVanillaId v sigma_tc_ty) src_loc `thenNF_Tc` \ sig ->
593 mkTcSig :: TcId -> SrcLoc -> NF_TcM TcSigInfo
594 mkTcSig poly_id src_loc
595 = -- Instantiate this type
596 -- It's important to do this even though in the error-free case
597 -- we could just split the sigma_tc_ty (since the tyvars don't
598 -- unified with anything). But in the case of an error, when
599 -- the tyvars *do* get unified with something, we want to carry on
600 -- typechecking the rest of the program with the function bound
601 -- to a pristine type, namely sigma_tc_ty
603 (tyvars, rho) = splitForAllTys (idType poly_id)
605 mapNF_Tc tcInstSigVar tyvars `thenNF_Tc` \ tyvars' ->
606 -- Make *signature* type variables
609 tyvar_tys' = mkTyVarTys tyvars'
610 rho' = substTy (mkTopTyVarSubst tyvars tyvar_tys') rho
611 -- mkTopTyVarSubst because the tyvars' are fresh
612 (theta', tau') = splitRhoTy rho'
613 -- This splitRhoTy tries hard to make sure that tau' is a type synonym
614 -- wherever possible, which can improve interface files.
616 newMethodWithGivenTy SignatureOrigin
619 theta' tau' `thenNF_Tc` \ inst ->
620 -- We make a Method even if it's not overloaded; no harm
621 instFunDeps SignatureOrigin theta' `thenNF_Tc` \ fds ->
623 returnNF_Tc (TySigInfo name poly_id tyvars' theta' tau' (instToIdBndr inst) (inst : fds) src_loc)
625 name = idName poly_id
630 %************************************************************************
632 \subsection{Checking signature type variables}
634 %************************************************************************
636 @checkSigTyVars@ is used after the type in a type signature has been unified with
637 the actual type found. It then checks that the type variables of the type signature
639 (a) Still all type variables
640 eg matching signature [a] against inferred type [(p,q)]
641 [then a will be unified to a non-type variable]
643 (b) Still all distinct
644 eg matching signature [(a,b)] against inferred type [(p,p)]
645 [then a and b will be unified together]
647 (c) Not mentioned in the environment
648 eg the signature for f in this:
654 Here, f is forced to be monorphic by the free occurence of x.
656 (d) Not (unified with another type variable that is) in scope.
657 eg f x :: (r->r) = (\y->y) :: forall a. a->r
658 when checking the expression type signature, we find that
659 even though there is nothing in scope whose type mentions r,
660 nevertheless the type signature for the expression isn't right.
662 Another example is in a class or instance declaration:
664 op :: forall b. a -> b
666 Here, b gets unified with a
668 Before doing this, the substitution is applied to the signature type variable.
670 We used to have the notion of a "DontBind" type variable, which would
671 only be bound to itself or nothing. Then points (a) and (b) were
672 self-checking. But it gave rise to bogus consequential error messages.
675 f = (*) -- Monomorphic
680 Here, we get a complaint when checking the type signature for g,
681 that g isn't polymorphic enough; but then we get another one when
682 dealing with the (Num x) context arising from f's definition;
683 we try to unify x with Int (to default it), but find that x has already
684 been unified with the DontBind variable "a" from g's signature.
685 This is really a problem with side-effecting unification; we'd like to
686 undo g's effects when its type signature fails, but unification is done
687 by side effect, so we can't (easily).
689 So we revert to ordinary type variables for signatures, and try to
690 give a helpful message in checkSigTyVars.
693 checkSigTyVars :: [TcTyVar] -- Universally-quantified type variables in the signature
694 -> TcTyVarSet -- Tyvars that are free in the type signature
695 -- These should *already* be in the global-var set, and are
696 -- used here only to improve the error message
697 -> TcM [TcTyVar] -- Zonked signature type variables
699 checkSigTyVars [] free = returnTc []
701 checkSigTyVars sig_tyvars free_tyvars
702 = zonkTcTyVars sig_tyvars `thenNF_Tc` \ sig_tys ->
703 tcGetGlobalTyVars `thenNF_Tc` \ globals ->
705 checkTcM (all_ok sig_tys globals)
706 (complain sig_tys globals) `thenTc_`
708 returnTc (map (getTyVar "checkSigTyVars") sig_tys)
712 all_ok (ty:tys) acc = case getTyVar_maybe ty of
713 Nothing -> False -- Point (a)
714 Just tv | tv `elemVarSet` acc -> False -- Point (b) or (c)
715 | otherwise -> all_ok tys (acc `extendVarSet` tv)
718 complain sig_tys globals
719 = -- For the in-scope ones, zonk them and construct a map
720 -- from the zonked tyvar to the in-scope one
721 -- If any of the in-scope tyvars zonk to a type, then ignore them;
722 -- that'll be caught later when we back up to their type sig
723 tcGetEnv `thenNF_Tc` \ env ->
725 in_scope_tvs = tcEnvTyVars env
727 zonkTcTyVars in_scope_tvs `thenNF_Tc` \ in_scope_tys ->
729 in_scope_assoc = [ (zonked_tv, in_scope_tv)
730 | (z_ty, in_scope_tv) <- in_scope_tys `zip` in_scope_tvs,
731 Just zonked_tv <- [getTyVar_maybe z_ty]
733 in_scope_env = mkVarEnv in_scope_assoc
736 -- "check" checks each sig tyvar in turn
738 (env2, in_scope_env, [])
739 (tidy_tvs `zip` tidy_tys) `thenNF_Tc` \ (env3, _, msgs) ->
741 failWithTcM (env3, main_msg $$ nest 4 (vcat msgs))
743 (env1, tidy_tvs) = mapAccumL tidyTyVar emptyTidyEnv sig_tyvars
744 (env2, tidy_tys) = tidyOpenTypes env1 sig_tys
746 main_msg = ptext SLIT("Inferred type is less polymorphic than expected")
748 check (env, acc, msgs) (sig_tyvar,ty)
749 -- sig_tyvar is from the signature;
750 -- ty is what you get if you zonk sig_tyvar and then tidy it
752 -- acc maps a zonked type variable back to a signature type variable
753 = case getTyVar_maybe ty of {
754 Nothing -> -- Error (a)!
755 returnNF_Tc (env, acc, unify_msg sig_tyvar (ppr ty) : msgs) ;
759 case lookupVarEnv acc tv of {
760 Just sig_tyvar' -> -- Error (b) or (d)!
761 returnNF_Tc (env, acc, unify_msg sig_tyvar (ppr sig_tyvar') : msgs) ;
765 if tv `elemVarSet` globals -- Error (c)! Type variable escapes
766 -- The least comprehensible, so put it last
767 then tcGetEnv `thenNF_Tc` \ env ->
768 find_globals tv env [] (tcEnvTcIds) `thenNF_Tc` \ (env1, globs) ->
769 find_frees tv env1 [] (varSetElems free_tyvars) `thenNF_Tc` \ (env2, frees) ->
770 returnNF_Tc (env2, acc, escape_msg sig_tyvar tv globs frees : msgs)
773 returnNF_Tc (env, extendVarEnv acc tv sig_tyvar, msgs)
776 -- find_globals looks at the value environment and finds values
777 -- whose types mention the offending type variable. It has to be
778 -- careful to zonk the Id's type first, so it has to be in the monad.
779 -- We must be careful to pass it a zonked type variable, too.
780 find_globals tv tidy_env acc []
781 = returnNF_Tc (tidy_env, acc)
783 find_globals tv tidy_env acc (id:ids)
784 | not (isLocallyDefined id) ||
785 isEmptyVarSet (idFreeTyVars id)
786 = find_globals tv tidy_env acc ids
789 = zonkTcType (idType id) `thenNF_Tc` \ id_ty ->
790 if tv `elemVarSet` tyVarsOfType id_ty then
792 (tidy_env', id_ty') = tidyOpenType tidy_env id_ty
793 acc' = (idName id, id_ty') : acc
795 find_globals tv tidy_env' acc' ids
797 find_globals tv tidy_env acc ids
799 find_frees tv tidy_env acc []
800 = returnNF_Tc (tidy_env, acc)
801 find_frees tv tidy_env acc (ftv:ftvs)
802 = zonkTcTyVar ftv `thenNF_Tc` \ ty ->
803 if tv `elemVarSet` tyVarsOfType ty then
805 (tidy_env', ftv') = tidyTyVar tidy_env ftv
807 find_frees tv tidy_env' (ftv':acc) ftvs
809 find_frees tv tidy_env acc ftvs
812 escape_msg sig_tv tv globs frees
813 = mk_msg sig_tv <+> ptext SLIT("escapes") $$
814 if not (null globs) then
815 vcat [pp_it <+> ptext SLIT("is mentioned in the environment"),
816 ptext SLIT("The following variables in the environment mention") <+> quotes (ppr tv),
817 nest 2 (vcat_first 10 [ppr name <+> dcolon <+> ppr ty | (name,ty) <- globs])
819 else if not (null frees) then
820 vcat [ptext SLIT("It is reachable from the type variable(s)") <+> pprQuotedList frees,
821 nest 2 (ptext SLIT("which") <+> is_are <+> ptext SLIT("free in the signature"))
824 empty -- Sigh. It's really hard to give a good error message
825 -- all the time. One bad case is an existential pattern match
827 is_are | isSingleton frees = ptext SLIT("is")
828 | otherwise = ptext SLIT("are")
829 pp_it | sig_tv /= tv = ptext SLIT("It unifies with") <+> quotes (ppr tv) <> comma <+> ptext SLIT("which")
830 | otherwise = ptext SLIT("It")
832 vcat_first :: Int -> [SDoc] -> SDoc
833 vcat_first n [] = empty
834 vcat_first 0 (x:xs) = text "...others omitted..."
835 vcat_first n (x:xs) = x $$ vcat_first (n-1) xs
837 unify_msg tv thing = mk_msg tv <+> ptext SLIT("is unified with") <+> quotes thing
838 mk_msg tv = ptext SLIT("Quantified type variable") <+> quotes (ppr tv)
841 These two context are used with checkSigTyVars
844 sigCtxt :: Message -> [TcTyVar] -> TcThetaType -> TcTauType
845 -> TidyEnv -> NF_TcM (TidyEnv, Message)
846 sigCtxt when sig_tyvars sig_theta sig_tau tidy_env
847 = zonkTcType sig_tau `thenNF_Tc` \ actual_tau ->
849 (env1, tidy_sig_tyvars) = tidyTyVars tidy_env sig_tyvars
850 (env2, tidy_sig_rho) = tidyOpenType env1 (mkRhoTy sig_theta sig_tau)
851 (env3, tidy_actual_tau) = tidyOpenType env2 actual_tau
852 msg = vcat [ptext SLIT("Signature type: ") <+> pprType (mkForAllTys tidy_sig_tyvars tidy_sig_rho),
853 ptext SLIT("Type to generalise:") <+> pprType tidy_actual_tau,
857 returnNF_Tc (env3, msg)
859 sigPatCtxt bound_tvs bound_ids tidy_env
861 sep [ptext SLIT("When checking a pattern that binds"),
862 nest 4 (vcat (zipWith ppr_id show_ids tidy_tys))])
864 show_ids = filter is_interesting bound_ids
865 is_interesting id = any (`elemVarSet` idFreeTyVars id) bound_tvs
867 (env1, tidy_tys) = tidyOpenTypes tidy_env (map idType show_ids)
868 ppr_id id ty = ppr id <+> dcolon <+> ppr ty
869 -- Don't zonk the types so we get the separate, un-unified versions
873 %************************************************************************
875 \subsection{Errors and contexts}
877 %************************************************************************
880 tcsigCtxt v = ptext SLIT("In a type signature for") <+> quotes (ppr v)
882 typeKindCtxt :: RenamedHsType -> Message
883 typeKindCtxt ty = sep [ptext SLIT("When checking that"),
884 nest 2 (quotes (ppr ty)),
885 ptext SLIT("is a type")]
887 appKindCtxt :: SDoc -> Message
888 appKindCtxt pp = ptext SLIT("When checking kinds in") <+> quotes pp
890 wrongThingErr expected thing name
891 = thing <+> quotes (ppr name) <+> ptext SLIT("used as a") <+> text expected
893 pp_ty_thing (ATyCon _) = ptext SLIT("Type constructor")
894 pp_ty_thing (AClass _) = ptext SLIT("Class")
895 pp_ty_thing (AnId _) = ptext SLIT("Identifier")
897 pp_tc_ty_thing (ATyVar _) = ptext SLIT("Type variable")
898 pp_tc_ty_thing (ATcId _) = ptext SLIT("Local identifier")
899 pp_tc_ty_thing (AThing _) = ptext SLIT("Utterly bogus")
902 = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
903 nest 4 (ptext SLIT("for the type:") <+> ppr ty),
904 nest 4 (ptext SLIT("Each forall'd type variable mentioned by the constraint must appear after the =>"))]
907 = sep [ptext SLIT("The constraint") <+> quotes (pprPred pred) <+>
908 ptext SLIT("does not mention any of the universally quantified type variables"),
909 nest 4 (ptext SLIT("in the type") <+> quotes (ppr ty))
913 = sep [ptext (SLIT("Illegal unboxed tuple as a function or contructor argument:")), nest 4 (ppr ty)]