2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 \section[TcMonoType]{Typechecking user-specified @MonoTypes@}
7 module TcMonoType ( tcHsType, tcHsRecType,
8 tcHsSigType, tcHsLiftedSigType,
9 tcRecClassContext, checkAmbiguity,
12 kcHsTyVar, kcHsTyVars, mkTyClTyVars,
13 kcHsType, kcHsSigType, kcHsLiftedSigType, 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 ( oclose )
39 import TcUnify ( unifyKind, unifyOpenTypeKind )
40 import Type ( Type, Kind, PredType(..), ThetaType, SigmaType, TauType,
41 mkTyVarTy, mkTyVarTys, mkFunTy, mkSynTy,
42 zipFunTys, hoistForAllTys,
43 mkSigmaTy, mkPredTy, mkTyConApp,
44 mkAppTys, splitForAllTys, splitRhoTy, mkRhoTy,
45 liftedTypeKind, unliftedTypeKind, 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 kcLiftedType :: RenamedHsType -> TcM ()
165 -- The type ty must be a *lifted* *type*
167 = kcHsType ty `thenTc` \ kind ->
168 tcAddErrCtxt (typeKindCtxt ty) $
169 unifyKind liftedTypeKind kind
171 ---------------------------
172 kcTypeType :: RenamedHsType -> TcM ()
173 -- The type ty must be a *type*, but it can be lifted or unlifted.
175 = kcHsType ty `thenTc` \ kind ->
176 tcAddErrCtxt (typeKindCtxt ty) $
177 unifyOpenTypeKind kind
179 ---------------------------
180 kcHsSigType, kcHsLiftedSigType :: RenamedHsType -> TcM ()
181 -- Used for type signatures
182 kcHsSigType = kcTypeType
183 kcHsLiftedSigType = kcLiftedType
185 ---------------------------
186 kcHsType :: RenamedHsType -> TcM TcKind
187 kcHsType (HsTyVar name) = kcTyVar name
189 kcHsType (HsListTy ty)
190 = kcLiftedType ty `thenTc` \ tau_ty ->
191 returnTc liftedTypeKind
193 kcHsType (HsTupleTy (HsTupCon _ boxity _) tys)
194 = mapTc kcTypeType tys `thenTc_`
195 returnTc (case boxity of
196 Boxed -> liftedTypeKind
197 Unboxed -> unliftedTypeKind)
199 kcHsType (HsFunTy ty1 ty2)
200 = kcTypeType ty1 `thenTc_`
201 kcTypeType ty2 `thenTc_`
202 returnTc liftedTypeKind
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 liftedTypeKind
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 liftedTypeKind
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 liftedTypeKind)
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 tcHsLiftedSigType
279 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
281 tcHsSigType and tcHsLiftedSigType 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, tcHsLiftedSigType :: RenamedHsType -> TcM Type
293 -- Do kind checking, and hoist for-alls to the top
294 tcHsSigType ty = kcTypeType ty `thenTc_` tcHsType ty
295 tcHsLiftedSigType ty = kcLiftedType 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 arity) tys)
349 = ASSERT( arity == length tys )
350 mapTc tc_tup_arg tys `thenTc` \ tau_tys ->
351 returnTc (mkTupleTy boxity arity tau_tys)
353 tc_tup_arg = case boxity of
354 Boxed -> tc_arg_type wimp_out
355 Unboxed -> tc_type wimp_out
356 -- Unboxed tuples can have polymorphic or unboxed args.
357 -- This happens in the workers for functions returning
358 -- product types with polymorphic components
360 tc_type wimp_out (HsFunTy ty1 ty2)
361 = tc_type wimp_out ty1 `thenTc` \ tau_ty1 ->
362 -- Function argument can be polymorphic, but
363 -- must not be an unboxed tuple
364 checkTc (not (isUnboxedTupleType tau_ty1))
365 (ubxArgTyErr ty1) `thenTc_`
366 tc_type wimp_out ty2 `thenTc` \ tau_ty2 ->
367 returnTc (mkFunTy tau_ty1 tau_ty2)
369 tc_type wimp_out (HsNumTy n)
371 returnTc (mkTyConApp genUnitTyCon [])
373 tc_type wimp_out (HsOpTy ty1 op ty2) =
374 tc_arg_type wimp_out ty1 `thenTc` \ tau_ty1 ->
375 tc_arg_type wimp_out ty2 `thenTc` \ tau_ty2 ->
376 tc_fun_type op [tau_ty1,tau_ty2]
378 tc_type wimp_out (HsAppTy ty1 ty2)
379 = tc_app wimp_out ty1 [ty2]
381 tc_type wimp_out (HsPredTy pred)
382 = tc_pred wimp_out pred `thenTc` \ pred' ->
383 returnTc (mkPredTy pred')
385 tc_type wimp_out full_ty@(HsForAllTy (Just tv_names) ctxt ty)
387 kind_check = kcHsContext ctxt `thenTc_` kcHsType ty
389 tcHsTyVars tv_names kind_check $ \ tyvars ->
390 tc_context wimp_out ctxt `thenTc` \ theta ->
392 -- Context behaves like a function type
393 -- This matters. Return-unboxed-tuple analysis can
394 -- give overloaded functions like
395 -- f :: forall a. Num a => (# a->a, a->a #)
396 -- And we want these to get through the type checker
398 tc_arg_type wimp_out ty
403 checkAmbiguity wimp_out is_source tyvars theta tau
405 is_source = case tv_names of
406 (UserTyVar _ : _) -> True
410 -- tc_arg_type checks that the argument of a
411 -- type appplication isn't a for-all type or an unboxed tuple type
412 -- For example, we want to reject things like:
414 -- instance Ord a => Ord (forall s. T s a)
416 -- g :: T s (forall b.b)
418 -- Other unboxed types are very occasionally allowed as type
419 -- arguments depending on the kind of the type constructor
421 tc_arg_type wimp_out arg_ty
423 = tc_type wimp_out arg_ty
426 = tc_type wimp_out arg_ty `thenTc` \ arg_ty' ->
427 checkTc (not (isForAllTy arg_ty')) (polyArgTyErr arg_ty) `thenTc_`
428 checkTc (not (isUnboxedTupleType arg_ty')) (ubxArgTyErr arg_ty) `thenTc_`
431 tc_arg_types wimp_out arg_tys = mapTc (tc_arg_type wimp_out) arg_tys
434 Help functions for type applications
435 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
438 tc_app :: RecFlag -> RenamedHsType -> [RenamedHsType] -> TcM Type
439 tc_app wimp_out (HsAppTy ty1 ty2) tys
440 = tc_app wimp_out ty1 (ty2:tys)
442 tc_app wimp_out ty tys
443 = tcAddErrCtxt (appKindCtxt pp_app) $
444 tc_arg_types wimp_out tys `thenTc` \ arg_tys ->
446 HsTyVar fun -> tc_fun_type fun arg_tys
447 other -> tc_type wimp_out 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 = tcLookup name `thenTc` \ thing ->
459 ATyVar tv -> returnTc (mkAppTys (mkTyVarTy tv) arg_tys)
462 | isSynTyCon tc -> checkTc arity_ok err_msg `thenTc_`
463 returnTc (mkAppTys (mkSynTy tc (take arity arg_tys))
464 (drop arity arg_tys))
466 | otherwise -> returnTc (mkTyConApp tc arg_tys)
469 arity_ok = arity <= n_args
470 arity = tyConArity tc
471 -- It's OK to have an *over-applied* type synonym
472 -- data Tree a b = ...
473 -- type Foo a = Tree [a]
474 -- f :: Foo a b -> ...
475 err_msg = arityErr "Type synonym" name arity n_args
476 n_args = length arg_tys
478 other -> failWithTc (wrongThingErr "type constructor" thing name)
485 tcRecClassContext :: RecFlag -> RenamedContext -> TcM ClassContext
486 -- Used when we are expecting a ClassContext (i.e. no implicit params)
487 tcRecClassContext wimp_out context
488 = tc_context wimp_out context `thenTc` \ theta ->
489 returnTc (classesOfPreds theta)
491 tc_context :: RecFlag -> RenamedContext -> TcM ThetaType
492 tc_context wimp_out context = mapTc (tc_pred wimp_out) context
494 tc_pred wimp_out assn@(HsPClass class_name tys)
495 = tcAddErrCtxt (appKindCtxt (ppr assn)) $
496 tc_arg_types wimp_out tys `thenTc` \ arg_tys ->
497 tcLookupGlobal class_name `thenTc` \ thing ->
499 AClass clas -> checkTc (arity == n_tys) err `thenTc_`
500 returnTc (Class clas arg_tys)
502 arity = classArity clas
504 err = arityErr "Class" class_name arity n_tys
506 other -> failWithTc (wrongThingErr "class" (AGlobal thing) class_name)
508 tc_pred wimp_out assn@(HsPIParam name ty)
509 = tcAddErrCtxt (appKindCtxt (ppr assn)) $
510 tc_arg_type wimp_out ty `thenTc` \ arg_ty ->
511 returnTc (IParam name arg_ty)
518 is ambiguous if P contains generic variables
519 (i.e. one of the Vs) that are not mentioned in tau
521 However, we need to take account of functional dependencies
522 when we speak of 'mentioned in tau'. Example:
523 class C a b | a -> b where ...
525 forall x y. (C x y) => x
526 is not ambiguous because x is mentioned and x determines y
528 NOTE: In addition, GHC insists that at least one type variable
529 in each constraint is in V. So we disallow a type like
530 forall a. Eq b => b -> b
531 even in a scope where b is in scope.
532 This is the is_free test below.
534 Notes on the 'is_source_polytype' test above
535 Check ambiguity only for source-program types, not
536 for types coming from inteface files. The latter can
537 legitimately have ambiguous types. Example
538 class S a where s :: a -> (Int,Int)
539 instance S Char where s _ = (1,1)
540 f:: S a => [a] -> Int -> (Int,Int)
541 f (_::[a]) x = (a*x,b)
542 where (a,b) = s (undefined::a)
543 Here the worker for f gets the type
544 fw :: forall a. S a => Int -> (# Int, Int #)
546 If the list of tv_names is empty, we have a monotype,
547 and then we don't need to check for ambiguity either,
548 because the test can't fail (see is_ambig).
551 checkAmbiguity :: RecFlag -> Bool
552 -> [TyVar] -> ThetaType -> TauType
554 checkAmbiguity wimp_out is_source_polytype forall_tyvars theta tau
555 | isRec wimp_out = returnTc sigma_ty
556 | otherwise = mapTc_ check_pred theta `thenTc_`
559 sigma_ty = mkSigmaTy forall_tyvars theta tau
560 tau_vars = tyVarsOfType tau
561 fds = instFunDepsOfTheta theta
562 extended_tau_vars = oclose fds tau_vars
564 is_ambig ct_var = (ct_var `elem` forall_tyvars) &&
565 not (ct_var `elemUFM` extended_tau_vars)
566 is_free ct_var = not (ct_var `elem` forall_tyvars)
568 check_pred pred = checkTc (not any_ambig) (ambigErr pred sigma_ty) `thenTc_`
569 checkTc (is_ip pred || not all_free) (freeErr pred sigma_ty)
571 ct_vars = varSetElems (tyVarsOfPred pred)
572 all_free = all is_free ct_vars
573 any_ambig = is_source_polytype && any is_ambig ct_vars
574 is_ip (IParam _ _) = True
578 %************************************************************************
580 \subsection{Type variables, with knot tying!}
582 %************************************************************************
585 mkImmutTyVars :: [(Name,Kind)] -> [TyVar]
586 mkImmutTyVars pairs = [mkTyVar name kind | (name, kind) <- pairs]
588 mkTyClTyVars :: Kind -- Kind of the tycon or class
589 -> [HsTyVarBndr Name]
591 mkTyClTyVars kind tyvar_names
592 = mkImmutTyVars tyvars_w_kinds
594 (tyvars_w_kinds, _) = zipFunTys (hsTyVarNames tyvar_names) kind
598 %************************************************************************
600 \subsection{Signatures}
602 %************************************************************************
604 @tcSigs@ checks the signatures for validity, and returns a list of
605 {\em freshly-instantiated} signatures. That is, the types are already
606 split up, and have fresh type variables installed. All non-type-signature
607 "RenamedSigs" are ignored.
609 The @TcSigInfo@ contains @TcTypes@ because they are unified with
610 the variable's type, and after that checked to see whether they've
616 Name -- N, the Name in corresponding binding
618 TcId -- *Polymorphic* binder for this value...
625 TcId -- *Monomorphic* binder for this value
626 -- Does *not* have name = N
629 [Inst] -- Empty if theta is null, or
630 -- (method mono_id) otherwise
632 SrcLoc -- Of the signature
634 instance Outputable TcSigInfo where
635 ppr (TySigInfo nm id tyvars theta tau _ inst loc) =
636 ppr nm <+> ptext SLIT("::") <+> ppr tyvars <+> ppr theta <+> ptext SLIT("=>") <+> ppr tau
638 maybeSig :: [TcSigInfo] -> Name -> Maybe (TcSigInfo)
639 -- Search for a particular signature
640 maybeSig [] name = Nothing
641 maybeSig (sig@(TySigInfo sig_name _ _ _ _ _ _ _) : sigs) name
642 | name == sig_name = Just sig
643 | otherwise = maybeSig sigs name
648 tcTySig :: RenamedSig -> TcM TcSigInfo
650 tcTySig (Sig v ty src_loc)
651 = tcAddSrcLoc src_loc $
652 tcAddErrCtxt (tcsigCtxt v) $
653 tcHsSigType ty `thenTc` \ sigma_tc_ty ->
654 mkTcSig (mkVanillaId v sigma_tc_ty) src_loc `thenNF_Tc` \ sig ->
657 mkTcSig :: TcId -> SrcLoc -> NF_TcM TcSigInfo
658 mkTcSig poly_id src_loc
659 = -- Instantiate this type
660 -- It's important to do this even though in the error-free case
661 -- we could just split the sigma_tc_ty (since the tyvars don't
662 -- unified with anything). But in the case of an error, when
663 -- the tyvars *do* get unified with something, we want to carry on
664 -- typechecking the rest of the program with the function bound
665 -- to a pristine type, namely sigma_tc_ty
667 (tyvars, rho) = splitForAllTys (idType poly_id)
669 mapNF_Tc tcInstSigVar tyvars `thenNF_Tc` \ tyvars' ->
670 -- Make *signature* type variables
673 tyvar_tys' = mkTyVarTys tyvars'
674 rho' = substTy (mkTopTyVarSubst tyvars tyvar_tys') rho
675 -- mkTopTyVarSubst because the tyvars' are fresh
676 (theta', tau') = splitRhoTy rho'
677 -- This splitRhoTy tries hard to make sure that tau' is a type synonym
678 -- wherever possible, which can improve interface files.
680 newMethodWithGivenTy SignatureOrigin
683 theta' tau' `thenNF_Tc` \ inst ->
684 -- We make a Method even if it's not overloaded; no harm
685 instFunDeps SignatureOrigin theta' `thenNF_Tc` \ fds ->
687 returnNF_Tc (TySigInfo name poly_id tyvars' theta' tau' (instToIdBndr inst) (inst : fds) src_loc)
689 name = idName poly_id
694 %************************************************************************
696 \subsection{Checking signature type variables}
698 %************************************************************************
700 @checkSigTyVars@ is used after the type in a type signature has been unified with
701 the actual type found. It then checks that the type variables of the type signature
703 (a) Still all type variables
704 eg matching signature [a] against inferred type [(p,q)]
705 [then a will be unified to a non-type variable]
707 (b) Still all distinct
708 eg matching signature [(a,b)] against inferred type [(p,p)]
709 [then a and b will be unified together]
711 (c) Not mentioned in the environment
712 eg the signature for f in this:
718 Here, f is forced to be monorphic by the free occurence of x.
720 (d) Not (unified with another type variable that is) in scope.
721 eg f x :: (r->r) = (\y->y) :: forall a. a->r
722 when checking the expression type signature, we find that
723 even though there is nothing in scope whose type mentions r,
724 nevertheless the type signature for the expression isn't right.
726 Another example is in a class or instance declaration:
728 op :: forall b. a -> b
730 Here, b gets unified with a
732 Before doing this, the substitution is applied to the signature type variable.
734 We used to have the notion of a "DontBind" type variable, which would
735 only be bound to itself or nothing. Then points (a) and (b) were
736 self-checking. But it gave rise to bogus consequential error messages.
739 f = (*) -- Monomorphic
744 Here, we get a complaint when checking the type signature for g,
745 that g isn't polymorphic enough; but then we get another one when
746 dealing with the (Num x) context arising from f's definition;
747 we try to unify x with Int (to default it), but find that x has already
748 been unified with the DontBind variable "a" from g's signature.
749 This is really a problem with side-effecting unification; we'd like to
750 undo g's effects when its type signature fails, but unification is done
751 by side effect, so we can't (easily).
753 So we revert to ordinary type variables for signatures, and try to
754 give a helpful message in checkSigTyVars.
757 checkSigTyVars :: [TcTyVar] -- Universally-quantified type variables in the signature
758 -> TcTyVarSet -- Tyvars that are free in the type signature
759 -- These should *already* be in the global-var set, and are
760 -- used here only to improve the error message
761 -> TcM [TcTyVar] -- Zonked signature type variables
763 checkSigTyVars [] free = returnTc []
765 checkSigTyVars sig_tyvars free_tyvars
766 = zonkTcTyVars sig_tyvars `thenNF_Tc` \ sig_tys ->
767 tcGetGlobalTyVars `thenNF_Tc` \ globals ->
769 checkTcM (all_ok sig_tys globals)
770 (complain sig_tys globals) `thenTc_`
772 returnTc (map (getTyVar "checkSigTyVars") sig_tys)
776 all_ok (ty:tys) acc = case getTyVar_maybe ty of
777 Nothing -> False -- Point (a)
778 Just tv | tv `elemVarSet` acc -> False -- Point (b) or (c)
779 | otherwise -> all_ok tys (acc `extendVarSet` tv)
782 complain sig_tys globals
783 = -- For the in-scope ones, zonk them and construct a map
784 -- from the zonked tyvar to the in-scope one
785 -- If any of the in-scope tyvars zonk to a type, then ignore them;
786 -- that'll be caught later when we back up to their type sig
787 tcGetEnv `thenNF_Tc` \ env ->
789 in_scope_tvs = tcEnvTyVars env
791 zonkTcTyVars in_scope_tvs `thenNF_Tc` \ in_scope_tys ->
793 in_scope_assoc = [ (zonked_tv, in_scope_tv)
794 | (z_ty, in_scope_tv) <- in_scope_tys `zip` in_scope_tvs,
795 Just zonked_tv <- [getTyVar_maybe z_ty]
797 in_scope_env = mkVarEnv in_scope_assoc
800 -- "check" checks each sig tyvar in turn
802 (env2, in_scope_env, [])
803 (tidy_tvs `zip` tidy_tys) `thenNF_Tc` \ (env3, _, msgs) ->
805 failWithTcM (env3, main_msg $$ nest 4 (vcat msgs))
807 (env1, tidy_tvs) = mapAccumL tidyTyVar emptyTidyEnv sig_tyvars
808 (env2, tidy_tys) = tidyOpenTypes env1 sig_tys
810 main_msg = ptext SLIT("Inferred type is less polymorphic than expected")
812 check (tidy_env, acc, msgs) (sig_tyvar,ty)
813 -- sig_tyvar is from the signature;
814 -- ty is what you get if you zonk sig_tyvar and then tidy it
816 -- acc maps a zonked type variable back to a signature type variable
817 = case getTyVar_maybe ty of {
818 Nothing -> -- Error (a)!
819 returnNF_Tc (tidy_env, acc, unify_msg sig_tyvar (ppr ty) : msgs) ;
823 case lookupVarEnv acc tv of {
824 Just sig_tyvar' -> -- Error (b) or (d)!
825 returnNF_Tc (tidy_env, acc, unify_msg sig_tyvar (ppr sig_tyvar') : msgs) ;
829 if tv `elemVarSet` globals -- Error (c)! Type variable escapes
830 -- The least comprehensible, so put it last
832 -- a) get the local TcIds from the environment,
833 -- and pass them to find_globals (they might have tv free)
834 -- b) similarly, find any free_tyvars that mention tv
835 then tcGetEnv `thenNF_Tc` \ ve ->
836 find_globals tv tidy_env [] (tcEnvTcIds ve) `thenNF_Tc` \ (tidy_env1, globs) ->
837 find_frees tv tidy_env1 [] (varSetElems free_tyvars) `thenNF_Tc` \ (tidy_env2, frees) ->
838 returnNF_Tc (tidy_env2, acc, escape_msg sig_tyvar tv globs frees : msgs)
841 returnNF_Tc (tidy_env, extendVarEnv acc tv sig_tyvar, msgs)
844 -- find_globals looks at the value environment and finds values
845 -- whose types mention the offending type variable. It has to be
846 -- careful to zonk the Id's type first, so it has to be in the monad.
847 -- We must be careful to pass it a zonked type variable, too.
853 -> NF_TcM (TidyEnv,[(Name,Type)])
855 find_globals tv tidy_env acc []
856 = returnNF_Tc (tidy_env, acc)
858 find_globals tv tidy_env acc (id:ids)
859 | isEmptyVarSet (idFreeTyVars id)
860 = find_globals tv tidy_env acc ids
863 = zonkTcType (idType id) `thenNF_Tc` \ id_ty ->
864 if tv `elemVarSet` tyVarsOfType id_ty then
866 (tidy_env', id_ty') = tidyOpenType tidy_env id_ty
867 acc' = (idName id, id_ty') : acc
869 find_globals tv tidy_env' acc' ids
871 find_globals tv tidy_env acc ids
873 find_frees tv tidy_env acc []
874 = returnNF_Tc (tidy_env, acc)
875 find_frees tv tidy_env acc (ftv:ftvs)
876 = zonkTcTyVar ftv `thenNF_Tc` \ ty ->
877 if tv `elemVarSet` tyVarsOfType ty then
879 (tidy_env', ftv') = tidyTyVar tidy_env ftv
881 find_frees tv tidy_env' (ftv':acc) ftvs
883 find_frees tv tidy_env acc ftvs
886 escape_msg sig_tv tv globs frees
887 = mk_msg sig_tv <+> ptext SLIT("escapes") $$
888 if not (null globs) then
889 vcat [pp_it <+> ptext SLIT("is mentioned in the environment"),
890 ptext SLIT("The following variables in the environment mention") <+> quotes (ppr tv),
891 nest 2 (vcat_first 10 [ppr name <+> dcolon <+> ppr ty | (name,ty) <- globs])
893 else if not (null frees) then
894 vcat [ptext SLIT("It is reachable from the type variable(s)") <+> pprQuotedList frees,
895 nest 2 (ptext SLIT("which") <+> is_are <+> ptext SLIT("free in the signature"))
898 empty -- Sigh. It's really hard to give a good error message
899 -- all the time. One bad case is an existential pattern match
901 is_are | isSingleton frees = ptext SLIT("is")
902 | otherwise = ptext SLIT("are")
903 pp_it | sig_tv /= tv = ptext SLIT("It unifies with") <+> quotes (ppr tv) <> comma <+> ptext SLIT("which")
904 | otherwise = ptext SLIT("It")
906 vcat_first :: Int -> [SDoc] -> SDoc
907 vcat_first n [] = empty
908 vcat_first 0 (x:xs) = text "...others omitted..."
909 vcat_first n (x:xs) = x $$ vcat_first (n-1) xs
911 unify_msg tv thing = mk_msg tv <+> ptext SLIT("is unified with") <+> quotes thing
912 mk_msg tv = ptext SLIT("Quantified type variable") <+> quotes (ppr tv)
915 These two context are used with checkSigTyVars
918 sigCtxt :: Message -> [TcTyVar] -> TcThetaType -> TcTauType
919 -> TidyEnv -> NF_TcM (TidyEnv, Message)
920 sigCtxt when sig_tyvars sig_theta sig_tau tidy_env
921 = zonkTcType sig_tau `thenNF_Tc` \ actual_tau ->
923 (env1, tidy_sig_tyvars) = tidyTyVars tidy_env sig_tyvars
924 (env2, tidy_sig_rho) = tidyOpenType env1 (mkRhoTy sig_theta sig_tau)
925 (env3, tidy_actual_tau) = tidyOpenType env2 actual_tau
926 msg = vcat [ptext SLIT("Signature type: ") <+> pprType (mkForAllTys tidy_sig_tyvars tidy_sig_rho),
927 ptext SLIT("Type to generalise:") <+> pprType tidy_actual_tau,
931 returnNF_Tc (env3, msg)
933 sigPatCtxt bound_tvs bound_ids tidy_env
935 sep [ptext SLIT("When checking a pattern that binds"),
936 nest 4 (vcat (zipWith ppr_id show_ids tidy_tys))])
938 show_ids = filter is_interesting bound_ids
939 is_interesting id = any (`elemVarSet` idFreeTyVars id) bound_tvs
941 (env1, tidy_tys) = tidyOpenTypes tidy_env (map idType show_ids)
942 ppr_id id ty = ppr id <+> dcolon <+> ppr ty
943 -- Don't zonk the types so we get the separate, un-unified versions
947 %************************************************************************
949 \subsection{Errors and contexts}
951 %************************************************************************
954 tcsigCtxt v = ptext SLIT("In a type signature for") <+> quotes (ppr v)
956 typeKindCtxt :: RenamedHsType -> Message
957 typeKindCtxt ty = sep [ptext SLIT("When checking that"),
958 nest 2 (quotes (ppr ty)),
959 ptext SLIT("is a type")]
961 appKindCtxt :: SDoc -> Message
962 appKindCtxt pp = ptext SLIT("When checking kinds in") <+> quotes pp
964 wrongThingErr expected thing name
965 = pp_thing thing <+> quotes (ppr name) <+> ptext SLIT("used as a") <+> text expected
967 pp_thing (AGlobal (ATyCon _)) = ptext SLIT("Type constructor")
968 pp_thing (AGlobal (AClass _)) = ptext SLIT("Class")
969 pp_thing (AGlobal (AnId _)) = ptext SLIT("Identifier")
970 pp_thing (ATyVar _) = ptext SLIT("Type variable")
971 pp_thing (ATcId _) = ptext SLIT("Local identifier")
972 pp_thing (AThing _) = ptext SLIT("Utterly bogus")
975 = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
976 nest 4 (ptext SLIT("for the type:") <+> ppr ty),
977 nest 4 (ptext SLIT("Each forall'd type variable mentioned by the constraint must appear after the =>"))]
980 = sep [ptext SLIT("The constraint") <+> quotes (pprPred pred) <+>
981 ptext SLIT("does not mention any of the universally quantified type variables"),
982 nest 4 (ptext SLIT("in the type") <+> quotes (ppr ty))
985 polyArgTyErr ty = ptext SLIT("Illegal polymorphic type as argument:") <+> ppr ty
986 ubxArgTyErr ty = ptext SLIT("Illegal unboxed tuple type as argument:") <+> ppr ty