2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 \section[TcMonoType]{Typechecking user-specified @MonoTypes@}
7 module TcMonoType ( tcHsType, tcHsRecType,
8 tcHsSigType, tcHsBoxedSigType,
9 tcRecClassContext, checkAmbiguity,
12 kcHsTyVar, kcHsTyVars, mkTyClTyVars,
13 kcHsType, kcHsSigType, kcHsBoxedSigType, kcHsContext,
14 tcTyVars, tcHsTyVars, mkImmutTyVars,
16 TcSigInfo(..), tcTySig, mkTcSig, maybeSig,
17 checkSigTyVars, sigCtxt, sigPatCtxt
20 #include "HsVersions.h"
22 import HsSyn ( HsType(..), HsTyVarBndr(..),
23 Sig(..), HsPred(..), pprParendHsType, HsTupCon(..), hsTyVarNames )
24 import RnHsSyn ( RenamedHsType, RenamedHsPred, RenamedContext, RenamedSig )
25 import TcHsSyn ( TcId )
28 import TcEnv ( tcExtendTyVarEnv, tcLookup, tcLookupGlobal,
29 tcGetGlobalTyVars, tcEnvTcIds, tcEnvTyVars,
30 TyThing(..), TcTyThing(..), tcExtendKindEnv
32 import 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,
41 mkTyVarTy, mkTyVarTys, mkFunTy, mkSynTy,
42 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, isForAllTy
51 import PprType ( pprType, pprPred )
52 import Subst ( mkTopTyVarSubst, substTy )
53 import CoreFVs ( idFreeTyVars )
54 import Id ( mkVanillaId, idName, idType )
55 import Var ( Id, Var, TyVar, mkTyVar, tyVarKind )
58 import ErrUtils ( Message )
59 import TyCon ( TyCon, isSynTyCon, tyConArity, tyConKind )
60 import Class ( ClassContext, classArity, classTyCon )
62 import TysWiredIn ( mkListTy, mkTupleTy, genUnitTyCon )
63 import UniqFM ( elemUFM )
64 import BasicTypes ( Boxity(..), RecFlag(..), isRec )
65 import SrcLoc ( SrcLoc )
66 import Util ( mapAccumL, isSingleton )
72 %************************************************************************
74 \subsection{Kind checking}
76 %************************************************************************
80 When we come across the binding site for some type variables, we
83 1. Figure out what kind each tyvar has
85 2. Create suitably-kinded tyvars,
87 and typecheck the body
89 To do step 1, we proceed thus:
91 1a. Bind each type variable to a kind variable
92 1b. Apply the kind checker
93 1c. Zonk the resulting kinds
95 The kind checker is passed to tcHsTyVars as an argument.
97 For example, when we find
98 (forall a m. m a -> m a)
99 we bind a,m to kind varibles and kind-check (m a -> m a). This
100 makes a get kind *, and m get kind *->*. Now we typecheck (m a -> m a)
101 in an environment that binds a and m suitably.
103 The kind checker passed to tcHsTyVars needs to look at enough to
104 establish the kind of the tyvar:
105 * For a group of type and class decls, it's just the group, not
106 the rest of the program
107 * For a tyvar bound in a pattern type signature, its the types
108 mentioned in the other type signatures in that bunch of patterns
109 * For a tyvar bound in a RULE, it's the type signatures on other
110 universally quantified variables in the rule
112 Note that this may occasionally give surprising results. For example:
114 data T a b = MkT (a b)
116 Here we deduce a::*->*, b::*.
117 But equally valid would be
118 a::(*->*)-> *, b::*->*
121 tcHsTyVars :: [HsTyVarBndr Name]
122 -> TcM a -- The kind checker
123 -> ([TyVar] -> TcM b)
126 tcHsTyVars [] kind_check thing_inside = thing_inside []
127 -- A useful short cut for a common case!
129 tcHsTyVars tv_names kind_check thing_inside
130 = kcHsTyVars tv_names `thenNF_Tc` \ tv_names_w_kinds ->
131 tcExtendKindEnv tv_names_w_kinds kind_check `thenTc_`
132 zonkKindEnv tv_names_w_kinds `thenNF_Tc` \ tvs_w_kinds ->
134 tyvars = mkImmutTyVars tvs_w_kinds
136 tcExtendTyVarEnv tyvars (thing_inside tyvars)
139 -> TcM a -- The kind checker
141 tcTyVars [] kind_check = returnTc []
143 tcTyVars tv_names kind_check
144 = mapNF_Tc newNamedKindVar tv_names `thenTc` \ kind_env ->
145 tcExtendKindEnv kind_env kind_check `thenTc_`
146 zonkKindEnv kind_env `thenNF_Tc` \ tvs_w_kinds ->
147 listNF_Tc [tcNewSigTyVar name kind | (name,kind) <- tvs_w_kinds]
152 kcHsTyVar :: HsTyVarBndr name -> NF_TcM (name, TcKind)
153 kcHsTyVars :: [HsTyVarBndr name] -> NF_TcM [(name, TcKind)]
155 kcHsTyVar (UserTyVar name) = newNamedKindVar name
156 kcHsTyVar (IfaceTyVar name kind) = returnNF_Tc (name, kind)
158 kcHsTyVars tvs = mapNF_Tc kcHsTyVar tvs
160 newNamedKindVar name = newKindVar `thenNF_Tc` \ kind ->
161 returnNF_Tc (name, kind)
163 ---------------------------
164 kcBoxedType :: RenamedHsType -> TcM ()
165 -- The type ty must be a *boxed* *type*
167 = kcHsType ty `thenTc` \ kind ->
168 tcAddErrCtxt (typeKindCtxt ty) $
169 unifyKind boxedTypeKind kind
171 ---------------------------
172 kcTypeType :: RenamedHsType -> TcM ()
173 -- The type ty must be a *type*, but it can be boxed or unboxed.
175 = kcHsType ty `thenTc` \ kind ->
176 tcAddErrCtxt (typeKindCtxt ty) $
177 unifyOpenTypeKind kind
179 ---------------------------
180 kcHsSigType, kcHsBoxedSigType :: RenamedHsType -> TcM ()
181 -- Used for type signatures
182 kcHsSigType = kcTypeType
183 kcHsBoxedSigType = kcBoxedType
185 ---------------------------
186 kcHsType :: RenamedHsType -> TcM TcKind
187 kcHsType (HsTyVar name) = kcTyVar name
189 kcHsType (HsListTy ty)
190 = kcBoxedType ty `thenTc` \ tau_ty ->
191 returnTc boxedTypeKind
193 kcHsType (HsTupleTy (HsTupCon _ boxity) tys)
194 = mapTc kcTypeType tys `thenTc_`
195 returnTc (case boxity of
196 Boxed -> boxedTypeKind
197 Unboxed -> unboxedTypeKind)
199 kcHsType (HsFunTy ty1 ty2)
200 = kcTypeType ty1 `thenTc_`
201 kcTypeType ty2 `thenTc_`
202 returnTc boxedTypeKind
204 kcHsType ty@(HsOpTy ty1 op ty2)
205 = kcTyVar op `thenTc` \ op_kind ->
206 kcHsType ty1 `thenTc` \ ty1_kind ->
207 kcHsType ty2 `thenTc` \ ty2_kind ->
208 tcAddErrCtxt (appKindCtxt (ppr ty)) $
209 kcAppKind op_kind ty1_kind `thenTc` \ op_kind' ->
210 kcAppKind op_kind' ty2_kind
212 kcHsType (HsPredTy pred)
213 = kcHsPred pred `thenTc_`
214 returnTc boxedTypeKind
216 kcHsType ty@(HsAppTy ty1 ty2)
217 = kcHsType ty1 `thenTc` \ tc_kind ->
218 kcHsType ty2 `thenTc` \ arg_kind ->
219 tcAddErrCtxt (appKindCtxt (ppr ty)) $
220 kcAppKind tc_kind arg_kind
222 kcHsType (HsForAllTy (Just tv_names) context ty)
223 = kcHsTyVars tv_names `thenNF_Tc` \ kind_env ->
224 tcExtendKindEnv kind_env $
225 kcHsContext context `thenTc_`
226 kcHsType ty `thenTc_`
227 returnTc boxedTypeKind
229 ---------------------------
230 kcAppKind fun_kind arg_kind
231 = case splitFunTy_maybe fun_kind of
232 Just (arg_kind', res_kind)
233 -> unifyKind arg_kind arg_kind' `thenTc_`
236 Nothing -> newKindVar `thenNF_Tc` \ res_kind ->
237 unifyKind fun_kind (mkArrowKind arg_kind res_kind) `thenTc_`
241 ---------------------------
242 kcHsContext ctxt = mapTc_ kcHsPred ctxt
244 kcHsPred :: RenamedHsPred -> TcM ()
245 kcHsPred pred@(HsPIParam name ty)
246 = tcAddErrCtxt (appKindCtxt (ppr pred)) $
249 kcHsPred pred@(HsPClass cls tys)
250 = tcAddErrCtxt (appKindCtxt (ppr pred)) $
251 kcClass cls `thenTc` \ kind ->
252 mapTc kcHsType tys `thenTc` \ arg_kinds ->
253 unifyKind kind (mkArrowKinds arg_kinds boxedTypeKind)
255 ---------------------------
256 kcTyVar name -- Could be a tyvar or a tycon
257 = tcLookup name `thenTc` \ thing ->
259 AThing kind -> returnTc kind
260 ATyVar tv -> returnTc (tyVarKind tv)
261 AGlobal (ATyCon tc) -> returnTc (tyConKind tc)
262 other -> failWithTc (wrongThingErr "type" thing name)
264 kcClass cls -- Must be a class
265 = tcLookup cls `thenNF_Tc` \ thing ->
267 AThing kind -> returnTc kind
268 AGlobal (AClass cls) -> returnTc (tyConKind (classTyCon cls))
269 other -> failWithTc (wrongThingErr "class" thing cls)
272 %************************************************************************
274 \subsection{Checking types}
276 %************************************************************************
278 tcHsSigType and tcHsBoxedSigType
279 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
281 tcHsSigType and tcHsBoxedSigType are used for type signatures written by the programmer
283 * We hoist any inner for-alls to the top
285 * Notice that we kind-check first, because the type-check assumes
286 that the kinds are already checked.
288 * They are only called when there are no kind vars in the environment
289 so the kind returned is indeed a Kind not a TcKind
292 tcHsSigType, tcHsBoxedSigType :: RenamedHsType -> TcM Type
293 -- Do kind checking, and hoist for-alls to the top
294 tcHsSigType ty = kcTypeType ty `thenTc_` tcHsType ty
295 tcHsBoxedSigType ty = kcBoxedType ty `thenTc_` tcHsType ty
297 tcHsType :: RenamedHsType -> TcM Type
298 tcHsRecType :: RecFlag -> RenamedHsType -> TcM Type
299 -- Don't do kind checking, but do hoist for-alls to the top
300 tcHsType ty = tc_type NonRecursive ty `thenTc` \ ty' -> returnTc (hoistForAllTys ty')
301 tcHsRecType wimp_out ty = tc_type wimp_out ty `thenTc` \ ty' -> returnTc (hoistForAllTys ty')
305 %************************************************************************
309 %************************************************************************
311 tc_type, the main work horse
312 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
318 tc_type is used to typecheck the types in the RHS of data
319 constructors. In the case of recursive data types, that means that
320 the type constructors themselves are (partly) black holes. e.g.
322 data T a = MkT a [T a]
324 While typechecking the [T a] on the RHS, T itself is not yet fully
325 defined. That in turn places restrictions on what you can check in
326 tcHsType; if you poke on too much you get a black hole. I keep
327 forgetting this, hence this warning!
329 The wimp_out argument tells when we are in a mutually-recursive
330 group of type declarations, so omit various checks else we
331 get a black hole. They'll be done again later, in TcTyClDecls.tcGroup.
333 --------------------------
334 *** END OF BIG WARNING ***
335 --------------------------
339 tc_type :: RecFlag -> RenamedHsType -> TcM Type
341 tc_type wimp_out ty@(HsTyVar name)
342 = tc_app wimp_out ty []
344 tc_type wimp_out (HsListTy ty)
345 = tc_arg_type wimp_out ty `thenTc` \ tau_ty ->
346 returnTc (mkListTy tau_ty)
348 tc_type wimp_out (HsTupleTy (HsTupCon _ boxity) tys)
349 = mapTc tc_tup_arg tys `thenTc` \ tau_tys ->
350 returnTc (mkTupleTy boxity (length tys) tau_tys)
352 tc_tup_arg = case boxity of
353 Boxed -> tc_arg_type wimp_out
354 Unboxed -> tc_type wimp_out
355 -- Unboxed tuples can have polymorphic or unboxed args.
356 -- This happens in the workers for functions returning
357 -- product types with polymorphic components
359 tc_type wimp_out (HsFunTy ty1 ty2)
360 = tc_type wimp_out ty1 `thenTc` \ tau_ty1 ->
361 -- Function argument can be polymorphic, but
362 -- must not be an unboxed tuple
363 checkTc (not (isUnboxedTupleType tau_ty1))
364 (ubxArgTyErr ty1) `thenTc_`
365 tc_type wimp_out ty2 `thenTc` \ tau_ty2 ->
366 returnTc (mkFunTy tau_ty1 tau_ty2)
368 tc_type wimp_out (HsNumTy n)
370 returnTc (mkTyConApp genUnitTyCon [])
372 tc_type wimp_out (HsOpTy ty1 op ty2) =
373 tc_arg_type wimp_out ty1 `thenTc` \ tau_ty1 ->
374 tc_arg_type wimp_out ty2 `thenTc` \ tau_ty2 ->
375 tc_fun_type op [tau_ty1,tau_ty2]
377 tc_type wimp_out (HsAppTy ty1 ty2)
378 = tc_app wimp_out ty1 [ty2]
380 tc_type wimp_out (HsPredTy pred)
381 = tc_pred wimp_out pred `thenTc` \ pred' ->
382 returnTc (mkPredTy pred')
384 tc_type wimp_out full_ty@(HsForAllTy (Just tv_names) ctxt ty)
386 kind_check = kcHsContext ctxt `thenTc_` kcHsType ty
388 tcHsTyVars tv_names kind_check $ \ tyvars ->
389 tc_context wimp_out ctxt `thenTc` \ theta ->
391 -- Context behaves like a function type
392 -- This matters. Return-unboxed-tuple analysis can
393 -- give overloaded functions like
394 -- f :: forall a. Num a => (# a->a, a->a #)
395 -- And we want these to get through the type checker
397 tc_arg_type wimp_out ty
402 checkAmbiguity wimp_out is_source tyvars theta tau
404 is_source = case tv_names of
405 (UserTyVar _ : _) -> True
409 -- tc_arg_type checks that the argument of a
410 -- type appplication isn't a for-all type or an unboxed tuple type
411 -- For example, we want to reject things like:
413 -- instance Ord a => Ord (forall s. T s a)
415 -- g :: T s (forall b.b)
417 -- Other unboxed types are very occasionally allowed as type
418 -- arguments depending on the kind of the type constructor
420 tc_arg_type wimp_out arg_ty
422 = tc_type wimp_out arg_ty
425 = tc_type wimp_out arg_ty `thenTc` \ arg_ty' ->
426 checkTc (not (isForAllTy arg_ty')) (polyArgTyErr arg_ty) `thenTc_`
427 checkTc (not (isUnboxedTupleType arg_ty')) (ubxArgTyErr arg_ty) `thenTc_`
430 tc_arg_types wimp_out arg_tys = mapTc (tc_arg_type wimp_out) arg_tys
433 Help functions for type applications
434 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
437 tc_app :: RecFlag -> RenamedHsType -> [RenamedHsType] -> TcM Type
438 tc_app wimp_out (HsAppTy ty1 ty2) tys
439 = tc_app wimp_out ty1 (ty2:tys)
441 tc_app wimp_out ty tys
442 = tcAddErrCtxt (appKindCtxt pp_app) $
443 tc_arg_types wimp_out tys `thenTc` \ arg_tys ->
445 HsTyVar fun -> tc_fun_type fun arg_tys
446 other -> tc_type wimp_out ty `thenTc` \ fun_ty ->
447 returnNF_Tc (mkAppTys fun_ty arg_tys)
449 pp_app = ppr ty <+> sep (map pprParendHsType tys)
451 -- (tc_fun_type ty arg_tys) returns (mkAppTys ty arg_tys)
452 -- But not quite; for synonyms it checks the correct arity, and builds a SynTy
453 -- hence the rather strange functionality.
455 tc_fun_type name arg_tys
456 = tcLookup name `thenTc` \ thing ->
458 ATyVar tv -> returnTc (mkAppTys (mkTyVarTy tv) arg_tys)
461 | 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" thing name)
484 tcRecClassContext :: RecFlag -> RenamedContext -> TcM ClassContext
485 -- Used when we are expecting a ClassContext (i.e. no implicit params)
486 tcRecClassContext wimp_out context
487 = tc_context wimp_out context `thenTc` \ theta ->
488 returnTc (classesOfPreds theta)
490 tc_context :: RecFlag -> RenamedContext -> TcM ThetaType
491 tc_context wimp_out context = mapTc (tc_pred wimp_out) context
493 tc_pred wimp_out assn@(HsPClass class_name tys)
494 = tcAddErrCtxt (appKindCtxt (ppr assn)) $
495 tc_arg_types wimp_out tys `thenTc` \ arg_tys ->
496 tcLookupGlobal 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" (AGlobal thing) class_name)
507 tc_pred wimp_out assn@(HsPIParam name ty)
508 = tcAddErrCtxt (appKindCtxt (ppr assn)) $
509 tc_arg_type wimp_out ty `thenTc` \ arg_ty ->
510 returnTc (IParam name arg_ty)
517 is ambiguous if P contains generic variables
518 (i.e. one of the Vs) that are not mentioned in tau
520 However, we need to take account of functional dependencies
521 when we speak of 'mentioned in tau'. Example:
522 class C a b | a -> b where ...
524 forall x y. (C x y) => x
525 is not ambiguous because x is mentioned and x determines y
527 NOTE: In addition, GHC insists that at least one type variable
528 in each constraint is in V. So we disallow a type like
529 forall a. Eq b => b -> b
530 even in a scope where b is in scope.
531 This is the is_free test below.
533 Notes on the 'is_source_polytype' test above
534 Check ambiguity only for source-program types, not
535 for types coming from inteface files. The latter can
536 legitimately have ambiguous types. Example
537 class S a where s :: a -> (Int,Int)
538 instance S Char where s _ = (1,1)
539 f:: S a => [a] -> Int -> (Int,Int)
540 f (_::[a]) x = (a*x,b)
541 where (a,b) = s (undefined::a)
542 Here the worker for f gets the type
543 fw :: forall a. S a => Int -> (# Int, Int #)
545 If the list of tv_names is empty, we have a monotype,
546 and then we don't need to check for ambiguity either,
547 because the test can't fail (see is_ambig).
550 checkAmbiguity wimp_out is_source_polytype forall_tyvars theta tau
551 | isRec wimp_out = returnTc sigma_ty
552 | otherwise = mapTc_ check_pred theta `thenTc_`
555 sigma_ty = mkSigmaTy forall_tyvars theta tau
556 tau_vars = tyVarsOfType tau
557 fds = instFunDepsOfTheta theta
558 tvFundep = tyVarFunDep fds
559 extended_tau_vars = oclose tvFundep tau_vars
561 is_ambig ct_var = (ct_var `elem` forall_tyvars) &&
562 not (ct_var `elemUFM` extended_tau_vars)
563 is_free ct_var = not (ct_var `elem` forall_tyvars)
565 check_pred pred = checkTc (not any_ambig) (ambigErr pred sigma_ty) `thenTc_`
566 checkTc (is_ip pred || not all_free) (freeErr pred sigma_ty)
568 ct_vars = varSetElems (tyVarsOfPred pred)
569 all_free = all is_free ct_vars
570 any_ambig = is_source_polytype && any is_ambig ct_vars
571 is_ip (IParam _ _) = True
575 %************************************************************************
577 \subsection{Type variables, with knot tying!}
579 %************************************************************************
582 mkImmutTyVars :: [(Name,Kind)] -> [TyVar]
583 mkImmutTyVars pairs = [mkTyVar name kind | (name, kind) <- pairs]
585 mkTyClTyVars :: Kind -- Kind of the tycon or class
586 -> [HsTyVarBndr Name]
588 mkTyClTyVars kind tyvar_names
589 = mkImmutTyVars tyvars_w_kinds
591 (tyvars_w_kinds, _) = zipFunTys (hsTyVarNames tyvar_names) kind
595 %************************************************************************
597 \subsection{Signatures}
599 %************************************************************************
601 @tcSigs@ checks the signatures for validity, and returns a list of
602 {\em freshly-instantiated} signatures. That is, the types are already
603 split up, and have fresh type variables installed. All non-type-signature
604 "RenamedSigs" are ignored.
606 The @TcSigInfo@ contains @TcTypes@ because they are unified with
607 the variable's type, and after that checked to see whether they've
613 Name -- N, the Name in corresponding binding
615 TcId -- *Polymorphic* binder for this value...
622 TcId -- *Monomorphic* binder for this value
623 -- Does *not* have name = N
626 [Inst] -- Empty if theta is null, or
627 -- (method mono_id) otherwise
629 SrcLoc -- Of the signature
631 instance Outputable TcSigInfo where
632 ppr (TySigInfo nm id tyvars theta tau _ inst loc) =
633 ppr nm <+> ptext SLIT("::") <+> ppr tyvars <+> ppr theta <+> ptext SLIT("=>") <+> ppr tau
635 maybeSig :: [TcSigInfo] -> Name -> Maybe (TcSigInfo)
636 -- Search for a particular signature
637 maybeSig [] name = Nothing
638 maybeSig (sig@(TySigInfo sig_name _ _ _ _ _ _ _) : sigs) name
639 | name == sig_name = Just sig
640 | otherwise = maybeSig sigs name
645 tcTySig :: RenamedSig -> TcM TcSigInfo
647 tcTySig (Sig v ty src_loc)
648 = tcAddSrcLoc src_loc $
649 tcAddErrCtxt (tcsigCtxt v) $
650 tcHsSigType ty `thenTc` \ sigma_tc_ty ->
651 mkTcSig (mkVanillaId v sigma_tc_ty) src_loc `thenNF_Tc` \ sig ->
654 mkTcSig :: TcId -> SrcLoc -> NF_TcM TcSigInfo
655 mkTcSig poly_id src_loc
656 = -- Instantiate this type
657 -- It's important to do this even though in the error-free case
658 -- we could just split the sigma_tc_ty (since the tyvars don't
659 -- unified with anything). But in the case of an error, when
660 -- the tyvars *do* get unified with something, we want to carry on
661 -- typechecking the rest of the program with the function bound
662 -- to a pristine type, namely sigma_tc_ty
664 (tyvars, rho) = splitForAllTys (idType poly_id)
666 mapNF_Tc tcInstSigVar tyvars `thenNF_Tc` \ tyvars' ->
667 -- Make *signature* type variables
670 tyvar_tys' = mkTyVarTys tyvars'
671 rho' = substTy (mkTopTyVarSubst tyvars tyvar_tys') rho
672 -- mkTopTyVarSubst because the tyvars' are fresh
673 (theta', tau') = splitRhoTy rho'
674 -- This splitRhoTy tries hard to make sure that tau' is a type synonym
675 -- wherever possible, which can improve interface files.
677 newMethodWithGivenTy SignatureOrigin
680 theta' tau' `thenNF_Tc` \ inst ->
681 -- We make a Method even if it's not overloaded; no harm
682 instFunDeps SignatureOrigin theta' `thenNF_Tc` \ fds ->
684 returnNF_Tc (TySigInfo name poly_id tyvars' theta' tau' (instToIdBndr inst) (inst : fds) src_loc)
686 name = idName poly_id
691 %************************************************************************
693 \subsection{Checking signature type variables}
695 %************************************************************************
697 @checkSigTyVars@ is used after the type in a type signature has been unified with
698 the actual type found. It then checks that the type variables of the type signature
700 (a) Still all type variables
701 eg matching signature [a] against inferred type [(p,q)]
702 [then a will be unified to a non-type variable]
704 (b) Still all distinct
705 eg matching signature [(a,b)] against inferred type [(p,p)]
706 [then a and b will be unified together]
708 (c) Not mentioned in the environment
709 eg the signature for f in this:
715 Here, f is forced to be monorphic by the free occurence of x.
717 (d) Not (unified with another type variable that is) in scope.
718 eg f x :: (r->r) = (\y->y) :: forall a. a->r
719 when checking the expression type signature, we find that
720 even though there is nothing in scope whose type mentions r,
721 nevertheless the type signature for the expression isn't right.
723 Another example is in a class or instance declaration:
725 op :: forall b. a -> b
727 Here, b gets unified with a
729 Before doing this, the substitution is applied to the signature type variable.
731 We used to have the notion of a "DontBind" type variable, which would
732 only be bound to itself or nothing. Then points (a) and (b) were
733 self-checking. But it gave rise to bogus consequential error messages.
736 f = (*) -- Monomorphic
741 Here, we get a complaint when checking the type signature for g,
742 that g isn't polymorphic enough; but then we get another one when
743 dealing with the (Num x) context arising from f's definition;
744 we try to unify x with Int (to default it), but find that x has already
745 been unified with the DontBind variable "a" from g's signature.
746 This is really a problem with side-effecting unification; we'd like to
747 undo g's effects when its type signature fails, but unification is done
748 by side effect, so we can't (easily).
750 So we revert to ordinary type variables for signatures, and try to
751 give a helpful message in checkSigTyVars.
754 checkSigTyVars :: [TcTyVar] -- Universally-quantified type variables in the signature
755 -> TcTyVarSet -- Tyvars that are free in the type signature
756 -- These should *already* be in the global-var set, and are
757 -- used here only to improve the error message
758 -> TcM [TcTyVar] -- Zonked signature type variables
760 checkSigTyVars [] free = returnTc []
762 checkSigTyVars sig_tyvars free_tyvars
763 = zonkTcTyVars sig_tyvars `thenNF_Tc` \ sig_tys ->
764 tcGetGlobalTyVars `thenNF_Tc` \ globals ->
766 checkTcM (all_ok sig_tys globals)
767 (complain sig_tys globals) `thenTc_`
769 returnTc (map (getTyVar "checkSigTyVars") sig_tys)
773 all_ok (ty:tys) acc = case getTyVar_maybe ty of
774 Nothing -> False -- Point (a)
775 Just tv | tv `elemVarSet` acc -> False -- Point (b) or (c)
776 | otherwise -> all_ok tys (acc `extendVarSet` tv)
779 complain sig_tys globals
780 = -- For the in-scope ones, zonk them and construct a map
781 -- from the zonked tyvar to the in-scope one
782 -- If any of the in-scope tyvars zonk to a type, then ignore them;
783 -- that'll be caught later when we back up to their type sig
784 tcGetEnv `thenNF_Tc` \ env ->
786 in_scope_tvs = tcEnvTyVars env
788 zonkTcTyVars in_scope_tvs `thenNF_Tc` \ in_scope_tys ->
790 in_scope_assoc = [ (zonked_tv, in_scope_tv)
791 | (z_ty, in_scope_tv) <- in_scope_tys `zip` in_scope_tvs,
792 Just zonked_tv <- [getTyVar_maybe z_ty]
794 in_scope_env = mkVarEnv in_scope_assoc
797 -- "check" checks each sig tyvar in turn
799 (env2, in_scope_env, [])
800 (tidy_tvs `zip` tidy_tys) `thenNF_Tc` \ (env3, _, msgs) ->
802 failWithTcM (env3, main_msg $$ nest 4 (vcat msgs))
804 (env1, tidy_tvs) = mapAccumL tidyTyVar emptyTidyEnv sig_tyvars
805 (env2, tidy_tys) = tidyOpenTypes env1 sig_tys
807 main_msg = ptext SLIT("Inferred type is less polymorphic than expected")
809 check (tidy_env, acc, msgs) (sig_tyvar,ty)
810 -- sig_tyvar is from the signature;
811 -- ty is what you get if you zonk sig_tyvar and then tidy it
813 -- acc maps a zonked type variable back to a signature type variable
814 = case getTyVar_maybe ty of {
815 Nothing -> -- Error (a)!
816 returnNF_Tc (tidy_env, acc, unify_msg sig_tyvar (ppr ty) : msgs) ;
820 case lookupVarEnv acc tv of {
821 Just sig_tyvar' -> -- Error (b) or (d)!
822 returnNF_Tc (tidy_env, acc, unify_msg sig_tyvar (ppr sig_tyvar') : msgs) ;
826 if tv `elemVarSet` globals -- Error (c)! Type variable escapes
827 -- The least comprehensible, so put it last
829 -- a) get the local TcIds from the environment,
830 -- and pass them to find_globals (they might have tv free)
831 -- b) similarly, find any free_tyvars that mention tv
832 then tcGetEnv `thenNF_Tc` \ ve ->
833 find_globals tv tidy_env [] (tcEnvTcIds ve) `thenNF_Tc` \ (tidy_env1, globs) ->
834 find_frees tv tidy_env1 [] (varSetElems free_tyvars) `thenNF_Tc` \ (tidy_env2, frees) ->
835 returnNF_Tc (tidy_env2, acc, escape_msg sig_tyvar tv globs frees : msgs)
838 returnNF_Tc (tidy_env, extendVarEnv acc tv sig_tyvar, msgs)
841 -- find_globals looks at the value environment and finds values
842 -- whose types mention the offending type variable. It has to be
843 -- careful to zonk the Id's type first, so it has to be in the monad.
844 -- We must be careful to pass it a zonked type variable, too.
850 -> NF_TcM (TidyEnv,[(Name,Type)])
852 find_globals tv tidy_env acc []
853 = returnNF_Tc (tidy_env, acc)
855 find_globals tv tidy_env acc (id:ids)
856 | isEmptyVarSet (idFreeTyVars id)
857 = find_globals tv tidy_env acc ids
860 = zonkTcType (idType id) `thenNF_Tc` \ id_ty ->
861 if tv `elemVarSet` tyVarsOfType id_ty then
863 (tidy_env', id_ty') = tidyOpenType tidy_env id_ty
864 acc' = (idName id, id_ty') : acc
866 find_globals tv tidy_env' acc' ids
868 find_globals tv tidy_env acc ids
870 find_frees tv tidy_env acc []
871 = returnNF_Tc (tidy_env, acc)
872 find_frees tv tidy_env acc (ftv:ftvs)
873 = zonkTcTyVar ftv `thenNF_Tc` \ ty ->
874 if tv `elemVarSet` tyVarsOfType ty then
876 (tidy_env', ftv') = tidyTyVar tidy_env ftv
878 find_frees tv tidy_env' (ftv':acc) ftvs
880 find_frees tv tidy_env acc ftvs
883 escape_msg sig_tv tv globs frees
884 = mk_msg sig_tv <+> ptext SLIT("escapes") $$
885 if not (null globs) then
886 vcat [pp_it <+> ptext SLIT("is mentioned in the environment"),
887 ptext SLIT("The following variables in the environment mention") <+> quotes (ppr tv),
888 nest 2 (vcat_first 10 [ppr name <+> dcolon <+> ppr ty | (name,ty) <- globs])
890 else if not (null frees) then
891 vcat [ptext SLIT("It is reachable from the type variable(s)") <+> pprQuotedList frees,
892 nest 2 (ptext SLIT("which") <+> is_are <+> ptext SLIT("free in the signature"))
895 empty -- Sigh. It's really hard to give a good error message
896 -- all the time. One bad case is an existential pattern match
898 is_are | isSingleton frees = ptext SLIT("is")
899 | otherwise = ptext SLIT("are")
900 pp_it | sig_tv /= tv = ptext SLIT("It unifies with") <+> quotes (ppr tv) <> comma <+> ptext SLIT("which")
901 | otherwise = ptext SLIT("It")
903 vcat_first :: Int -> [SDoc] -> SDoc
904 vcat_first n [] = empty
905 vcat_first 0 (x:xs) = text "...others omitted..."
906 vcat_first n (x:xs) = x $$ vcat_first (n-1) xs
908 unify_msg tv thing = mk_msg tv <+> ptext SLIT("is unified with") <+> quotes thing
909 mk_msg tv = ptext SLIT("Quantified type variable") <+> quotes (ppr tv)
912 These two context are used with checkSigTyVars
915 sigCtxt :: Message -> [TcTyVar] -> TcThetaType -> TcTauType
916 -> TidyEnv -> NF_TcM (TidyEnv, Message)
917 sigCtxt when sig_tyvars sig_theta sig_tau tidy_env
918 = zonkTcType sig_tau `thenNF_Tc` \ actual_tau ->
920 (env1, tidy_sig_tyvars) = tidyTyVars tidy_env sig_tyvars
921 (env2, tidy_sig_rho) = tidyOpenType env1 (mkRhoTy sig_theta sig_tau)
922 (env3, tidy_actual_tau) = tidyOpenType env2 actual_tau
923 msg = vcat [ptext SLIT("Signature type: ") <+> pprType (mkForAllTys tidy_sig_tyvars tidy_sig_rho),
924 ptext SLIT("Type to generalise:") <+> pprType tidy_actual_tau,
928 returnNF_Tc (env3, msg)
930 sigPatCtxt bound_tvs bound_ids tidy_env
932 sep [ptext SLIT("When checking a pattern that binds"),
933 nest 4 (vcat (zipWith ppr_id show_ids tidy_tys))])
935 show_ids = filter is_interesting bound_ids
936 is_interesting id = any (`elemVarSet` idFreeTyVars id) bound_tvs
938 (env1, tidy_tys) = tidyOpenTypes tidy_env (map idType show_ids)
939 ppr_id id ty = ppr id <+> dcolon <+> ppr ty
940 -- Don't zonk the types so we get the separate, un-unified versions
944 %************************************************************************
946 \subsection{Errors and contexts}
948 %************************************************************************
951 tcsigCtxt v = ptext SLIT("In a type signature for") <+> quotes (ppr v)
953 typeKindCtxt :: RenamedHsType -> Message
954 typeKindCtxt ty = sep [ptext SLIT("When checking that"),
955 nest 2 (quotes (ppr ty)),
956 ptext SLIT("is a type")]
958 appKindCtxt :: SDoc -> Message
959 appKindCtxt pp = ptext SLIT("When checking kinds in") <+> quotes pp
961 wrongThingErr expected thing name
962 = pp_thing thing <+> quotes (ppr name) <+> ptext SLIT("used as a") <+> text expected
964 pp_thing (AGlobal (ATyCon _)) = ptext SLIT("Type constructor")
965 pp_thing (AGlobal (AClass _)) = ptext SLIT("Class")
966 pp_thing (AGlobal (AnId _)) = ptext SLIT("Identifier")
967 pp_thing (ATyVar _) = ptext SLIT("Type variable")
968 pp_thing (ATcId _) = ptext SLIT("Local identifier")
969 pp_thing (AThing _) = ptext SLIT("Utterly bogus")
972 = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
973 nest 4 (ptext SLIT("for the type:") <+> ppr ty),
974 nest 4 (ptext SLIT("Each forall'd type variable mentioned by the constraint must appear after the =>"))]
977 = sep [ptext SLIT("The constraint") <+> quotes (pprPred pred) <+>
978 ptext SLIT("does not mention any of the universally quantified type variables"),
979 nest 4 (ptext SLIT("in the type") <+> quotes (ppr ty))
982 polyArgTyErr ty = ptext SLIT("Illegal polymorphic type as argument:") <+> ppr ty
983 ubxArgTyErr ty = ptext SLIT("Illegal unboxed tuple type as argument:") <+> ppr ty