2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 \section[TcMonoType]{Typechecking user-specified @MonoTypes@}
7 module TcMonoType ( tcHsType, tcHsTcType, tcHsTypeKind, tcContext,
9 TcSigInfo(..), tcTySig, mkTcSig, noSigs, maybeSig,
10 checkSigTyVars, sigCtxt, existentialPatCtxt
13 #include "HsVersions.h"
15 import HsSyn ( HsType(..), HsTyVar(..), Sig(..), pprContext )
16 import RnHsSyn ( RenamedHsType, RenamedContext, RenamedSig )
17 import TcHsSyn ( TcIdBndr, TcIdOcc(..) )
20 import TcEnv ( tcLookupTyVar, tcLookupClass, tcLookupTyCon, tcExtendTyVarEnv,
21 tcGetGlobalTyVars, tidyTypes, tidyTyVar
23 import TcType ( TcType, TcKind, TcTyVar, TcThetaType, TcTauType,
24 typeToTcType, tcInstTcType, kindToTcKind,
26 zonkTcKindToKind, zonkTcTyVars, zonkTcType
28 import Inst ( Inst, InstOrigin(..), newMethodWithGivenTy, instToIdBndr )
29 import TcUnify ( unifyKind, unifyKinds )
30 import Type ( Type, ThetaType,
31 mkTyVarTy, mkTyVarTys, mkFunTy, mkSynTy,
32 mkSigmaTy, mkDictTy, mkTyConApp, mkAppTys, splitRhoTy,
33 boxedTypeKind, unboxedTypeKind, openTypeKind,
34 mkArrowKind, getTyVar_maybe, getTyVar
36 import Id ( mkUserId, idName, idType, idFreeTyVars )
37 import Var ( TyVar, mkTyVar )
40 import Bag ( bagToList )
41 import PrelInfo ( cCallishClassKeys )
42 import TyCon ( TyCon )
43 import Name ( Name, OccName, isTvOcc, getOccName )
44 import TysWiredIn ( mkListTy, mkTupleTy, mkUnboxedTupleTy )
45 import SrcLoc ( SrcLoc )
46 import Unique ( Unique, Uniquable(..) )
47 import Util ( zipWithEqual, zipLazy, mapAccumL )
52 %************************************************************************
54 \subsection{Checking types}
56 %************************************************************************
58 tcHsType and tcHsTypeKind
59 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
61 tcHsType checks that the type really is of kind Type!
64 tcHsType :: RenamedHsType -> TcM s Type
66 = tcAddErrCtxt (typeCtxt ty) $
69 -- Version for when we need a TcType returned
70 tcHsTcType :: RenamedHsType -> TcM s (TcType s)
72 = tcHsType ty `thenTc` \ ty' ->
73 returnTc (typeToTcType ty')
76 = tc_hs_type_kind ty `thenTc` \ (kind,ty) ->
77 -- Check that it really is a type
78 unifyKind openTypeKind kind `thenTc_`
82 tcHsTypeKind does the real work. It returns a kind and a type.
85 tcHsTypeKind :: RenamedHsType -> TcM s (TcKind s, Type)
88 = tcAddErrCtxt (typeCtxt ty) $
92 -- This equation isn't needed (the next one would handle it fine)
93 -- but it's rather a common case, so we handle it directly
94 tc_hs_type_kind (MonoTyVar name)
95 | isTvOcc (getOccName name)
96 = tcLookupTyVar name `thenNF_Tc` \ (kind,tyvar) ->
97 returnTc (kind, mkTyVarTy tyvar)
99 tc_hs_type_kind ty@(MonoTyVar name)
102 tc_hs_type_kind (MonoListTy ty)
103 = tc_hs_type ty `thenTc` \ tau_ty ->
104 returnTc (boxedTypeKind, mkListTy tau_ty)
106 tc_hs_type_kind (MonoTupleTy tys True{-boxed-})
107 = mapTc tc_hs_type tys `thenTc` \ tau_tys ->
108 returnTc (boxedTypeKind, mkTupleTy (length tys) tau_tys)
110 tc_hs_type_kind (MonoTupleTy tys False{-unboxed-})
111 = mapTc tc_hs_type tys `thenTc` \ tau_tys ->
112 returnTc (unboxedTypeKind, mkUnboxedTupleTy (length tys) tau_tys)
114 tc_hs_type_kind (MonoFunTy ty1 ty2)
115 = tc_hs_type ty1 `thenTc` \ tau_ty1 ->
116 tc_hs_type ty2 `thenTc` \ tau_ty2 ->
117 returnTc (boxedTypeKind, mkFunTy tau_ty1 tau_ty2)
119 tc_hs_type_kind (MonoTyApp ty1 ty2)
122 tc_hs_type_kind (HsForAllTy tv_names context ty)
123 = tcTyVarScope tv_names $ \ tyvars ->
124 tcContext context `thenTc` \ theta ->
125 tc_hs_type ty `thenTc` \ tau ->
126 -- For-all's are of kind type!
127 returnTc (boxedTypeKind, mkSigmaTy tyvars theta tau)
129 -- for unfoldings, and instance decls, only:
130 tc_hs_type_kind (MonoDictTy class_name tys)
131 = tcClassAssertion (class_name, tys) `thenTc` \ (clas, arg_tys) ->
132 returnTc (boxedTypeKind, mkDictTy clas arg_tys)
135 Help functions for type applications
136 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
138 tcTyApp (MonoTyApp ty1 ty2) tys
139 = tcTyApp ty1 (ty2:tys)
146 = mapAndUnzipTc tc_hs_type_kind tys `thenTc` \ (arg_kinds, arg_tys) ->
147 tcFunType ty arg_tys `thenTc` \ (fun_kind, result_ty) ->
149 -- Check argument compatibility
150 newKindVar `thenNF_Tc` \ result_kind ->
151 unifyKind fun_kind (foldr mkArrowKind result_kind arg_kinds)
153 returnTc (result_kind, result_ty)
155 -- (tcFunType ty arg_tys) returns (kind-of ty, mkAppTys ty arg_tys)
156 -- But not quite; for synonyms it checks the correct arity, and builds a SynTy
157 -- hence the rather strange functionality.
159 tcFunType (MonoTyVar name) arg_tys
160 | isTvOcc (getOccName name) -- Must be a type variable
161 = tcLookupTyVar name `thenNF_Tc` \ (kind,tyvar) ->
162 returnTc (kind, mkAppTys (mkTyVarTy tyvar) arg_tys)
164 | otherwise -- Must be a type constructor
165 = tcLookupTyCon name `thenTc` \ (tycon_kind,maybe_arity, tycon) ->
167 Nothing -> -- Data type or newtype
168 returnTc (tycon_kind, mkTyConApp tycon arg_tys)
170 Just arity -> -- Type synonym
171 checkTc (arity <= n_args) err_msg `thenTc_`
172 returnTc (tycon_kind, result_ty)
174 -- It's OK to have an *over-applied* type synonym
175 -- data Tree a b = ...
176 -- type Foo a = Tree [a]
177 -- f :: Foo a b -> ...
178 result_ty = mkAppTys (mkSynTy tycon (take arity arg_tys))
180 err_msg = arityErr "Type synonym constructor" name arity n_args
181 n_args = length arg_tys
184 = tc_hs_type_kind ty `thenTc` \ (fun_kind, fun_ty) ->
185 returnTc (fun_kind, mkAppTys fun_ty arg_tys)
193 tcContext :: RenamedContext -> TcM s ThetaType
195 = tcAddErrCtxt (thetaCtxt context) $
197 --Someone discovered that @CCallable@ and @CReturnable@
198 -- could be used in contexts such as:
199 -- foo :: CCallable a => a -> PrimIO Int
200 -- Doing this utterly wrecks the whole point of introducing these
201 -- classes so we specifically check that this isn't being done.
203 -- We *don't* do this check in tcClassAssertion, because that's
204 -- called when checking a HsDictTy, and we don't want to reject
205 -- instance CCallable Int
207 mapTc check_naughty context `thenTc_`
209 mapTc tcClassAssertion context
212 check_naughty (class_name, _)
213 = checkTc (not (getUnique class_name `elem` cCallishClassKeys))
214 (naughtyCCallContextErr class_name)
216 tcClassAssertion (class_name, tys)
217 = tcLookupClass class_name `thenTc` \ (class_kinds, clas) ->
218 mapAndUnzipTc tc_hs_type_kind tys `thenTc` \ (ty_kinds, tc_tys) ->
220 -- Check with kind mis-match
222 arity = length class_kinds
223 n_tys = length ty_kinds
224 err = arityErr "Class" class_name arity n_tys
226 checkTc (arity == n_tys) err `thenTc_`
227 unifyKinds class_kinds ty_kinds `thenTc_`
229 returnTc (clas, tc_tys)
233 %************************************************************************
235 \subsection{Type variables, with knot tying!}
237 %************************************************************************
241 :: [HsTyVar Name] -- Names of some type variables
242 -> ([TyVar] -> TcM s a) -- Thing to type check in their scope
245 tcTyVarScope tyvar_names thing_inside
246 = mapAndUnzipNF_Tc tcHsTyVar tyvar_names `thenNF_Tc` \ (names, kinds) ->
248 fixTc (\ ~(rec_tyvars, _) ->
249 -- Ok to look at names, kinds, but not tyvars!
251 tcExtendTyVarEnv names (kinds `zipLazy` rec_tyvars)
252 (thing_inside rec_tyvars) `thenTc` \ result ->
254 -- Get the tyvar's Kinds from their TcKinds
255 mapNF_Tc zonkTcKindToKind kinds `thenNF_Tc` \ kinds' ->
257 -- Construct the real TyVars
259 tyvars = zipWithEqual "tcTyVarScope" mkTyVar names kinds'
261 returnTc (tyvars, result)
262 ) `thenTc` \ (_,result) ->
265 tcHsTyVar (UserTyVar name)
266 = newKindVar `thenNF_Tc` \ tc_kind ->
267 returnNF_Tc (name, tc_kind)
268 tcHsTyVar (IfaceTyVar name kind)
269 = returnNF_Tc (name, kindToTcKind kind)
273 %************************************************************************
275 \subsection{Signatures}
277 %************************************************************************
279 @tcSigs@ checks the signatures for validity, and returns a list of
280 {\em freshly-instantiated} signatures. That is, the types are already
281 split up, and have fresh type variables installed. All non-type-signature
282 "RenamedSigs" are ignored.
284 The @TcSigInfo@ contains @TcTypes@ because they are unified with
285 the variable's type, and after that checked to see whether they've
291 Name -- N, the Name in corresponding binding
293 (TcIdBndr s) -- *Polymorphic* binder for this value...
296 [TcTyVar s] -- tyvars
297 (TcThetaType s) -- theta
300 (TcIdBndr s) -- *Monomorphic* binder for this value
301 -- Does *not* have name = N
304 (Inst s) -- Empty if theta is null, or
305 -- (method mono_id) otherwise
307 SrcLoc -- Of the signature
310 maybeSig :: [TcSigInfo s] -> Name -> Maybe (TcSigInfo s)
311 -- Search for a particular signature
312 maybeSig [] name = Nothing
313 maybeSig (sig@(TySigInfo sig_name _ _ _ _ _ _ _) : sigs) name
314 | name == sig_name = Just sig
315 | otherwise = maybeSig sigs name
317 -- This little helper is useful to pass to tcPat
318 noSigs :: Name -> Maybe (TcIdBndr s)
319 noSigs name = Nothing
324 tcTySig :: RenamedSig
325 -> TcM s (TcSigInfo s)
327 tcTySig (Sig v ty src_loc)
328 = tcAddSrcLoc src_loc $
329 tcHsTcType ty `thenTc` \ sigma_tc_ty ->
330 mkTcSig (mkUserId v sigma_tc_ty) src_loc `thenNF_Tc` \ sig ->
333 mkTcSig :: TcIdBndr s -> SrcLoc -> NF_TcM s (TcSigInfo s)
334 mkTcSig poly_id src_loc
335 = -- Instantiate this type
336 -- It's important to do this even though in the error-free case
337 -- we could just split the sigma_tc_ty (since the tyvars don't
338 -- unified with anything). But in the case of an error, when
339 -- the tyvars *do* get unified with something, we want to carry on
340 -- typechecking the rest of the program with the function bound
341 -- to a pristine type, namely sigma_tc_ty
342 tcInstTcType (idType poly_id) `thenNF_Tc` \ (tyvars, rho) ->
344 (theta, tau) = splitRhoTy rho
345 -- This splitSigmaTy tries hard to make sure that tau' is a type synonym
346 -- wherever possible, which can improve interface files.
348 newMethodWithGivenTy SignatureOrigin
351 theta tau `thenNF_Tc` \ inst ->
352 -- We make a Method even if it's not overloaded; no harm
354 returnNF_Tc (TySigInfo name poly_id tyvars theta tau (instToIdBndr inst) inst src_loc)
356 name = idName poly_id
361 %************************************************************************
363 \subsection{Checking signature type variables}
365 %************************************************************************
367 @checkSigTyVars@ is used after the type in a type signature has been unified with
368 the actual type found. It then checks that the type variables of the type signature
370 (a) still all type variables
371 eg matching signature [a] against inferred type [(p,q)]
372 [then a will be unified to a non-type variable]
374 (b) still all distinct
375 eg matching signature [(a,b)] against inferred type [(p,p)]
376 [then a and b will be unified together]
378 (c) not mentioned in the environment
379 eg the signature for f in this:
385 Here, f is forced to be monorphic by the free occurence of x.
387 Before doing this, the substitution is applied to the signature type variable.
389 We used to have the notion of a "DontBind" type variable, which would
390 only be bound to itself or nothing. Then points (a) and (b) were
391 self-checking. But it gave rise to bogus consequential error messages.
394 f = (*) -- Monomorphic
399 Here, we get a complaint when checking the type signature for g,
400 that g isn't polymorphic enough; but then we get another one when
401 dealing with the (Num x) context arising from f's definition;
402 we try to unify x with Int (to default it), but find that x has already
403 been unified with the DontBind variable "a" from g's signature.
404 This is really a problem with side-effecting unification; we'd like to
405 undo g's effects when its type signature fails, but unification is done
406 by side effect, so we can't (easily).
408 So we revert to ordinary type variables for signatures, and try to
409 give a helpful message in checkSigTyVars.
412 checkSigTyVars :: [TcTyVar s] -- The original signature type variables
413 -> TcM s [TcTyVar s] -- Zonked signature type variables
415 checkSigTyVars [] = returnTc []
417 checkSigTyVars sig_tyvars
418 = zonkTcTyVars sig_tyvars `thenNF_Tc` \ sig_tys ->
419 tcGetGlobalTyVars `thenNF_Tc` \ globals ->
420 checkTcM (all_ok sig_tys globals)
421 (complain sig_tys globals) `thenTc_`
423 returnTc (map (getTyVar "checkSigTyVars") sig_tys)
427 all_ok (ty:tys) acc = case getTyVar_maybe ty of
428 Nothing -> False -- Point (a)
429 Just tv | tv `elemVarSet` acc -> False -- Point (b) or (c)
430 | otherwise -> all_ok tys (acc `extendVarSet` tv)
433 complain sig_tys globals
434 = failWithTcM (env2, main_msg)
436 (env1, tidy_tys) = tidyTypes emptyTidyEnv sig_tys
437 (env2, tidy_tvs) = mapAccumL tidyTyVar env1 sig_tyvars
439 msgs = check (tidy_tvs `zip` tidy_tys) emptyVarEnv
441 main_msg = ptext SLIT("Inferred type is less polymorphic than expected")
446 check ((sig_tyvar,ty):prs) acc
447 = case getTyVar_maybe ty of
448 Nothing -- Error (a)!
449 -> unify_msg sig_tyvar (ppr ty) : check prs acc
452 | tv `elemVarSet` globals -- Error (c)! Type variable escapes
453 -> escape_msg tv : check prs acc
456 -> case lookupVarEnv acc tv of
458 -> check prs (extendVarEnv acc tv sig_tyvar) -- All OK
459 Just sig_tyvar' -- Error (b)!
460 -> unify_msg sig_tyvar (ppr sig_tyvar') : check prs acc
463 escape_msg tv = mk_msg tv <+> ptext SLIT("escapes; i.e. unifies with something more global")
464 unify_msg tv thing = mk_msg tv <+> ptext SLIT("is unified with") <+> quotes thing
465 mk_msg tv = ptext SLIT("Quantified type variable") <+> quotes (ppr tv)
468 These two context are used with checkSigTyVars
471 sigCtxt thing sig_tau tidy_env
472 = zonkTcType sig_tau `thenNF_Tc` \ zonked_sig_tau ->
474 (env1, [tidy_tau, tidy_zonked_tau]) = tidyTypes tidy_env [sig_tau, zonked_sig_tau]
476 msg = vcat [ptext SLIT("When checking the type signature for") <+> thing,
477 nest 4 (ptext SLIT("Signature:") <+> ppr tidy_tau),
478 nest 4 (ptext SLIT("Inferred: ") <+> ppr tidy_zonked_tau)]
480 returnNF_Tc (env1, msg)
482 existentialPatCtxt bound_tvs bound_ids tidy_env
484 sep [ptext SLIT("When checking an existential pattern that binds"),
485 nest 4 (vcat (zipWith ppr_id show_ids tidy_tys))])
487 tv_list = bagToList bound_tvs
488 show_ids = filter is_interesting (map snd (bagToList bound_ids))
489 is_interesting id = any (`elemVarSet` idFreeTyVars id) tv_list
491 (env1, tidy_tys) = tidyTypes tidy_env (map idType show_ids)
492 ppr_id id ty = ppr id <+> ptext SLIT("::") <+> ppr ty
493 -- Don't zonk the types so we get the separate, un-unified versions
497 %************************************************************************
499 \subsection{Errors and contexts}
501 %************************************************************************
504 naughtyCCallContextErr clas_name
505 = sep [ptext SLIT("Can't use class"), quotes (ppr clas_name), ptext SLIT("in a context")]
507 typeCtxt ty = ptext SLIT("In the type") <+> quotes (ppr ty)
509 thetaCtxt theta = ptext SLIT("In the context") <+> quotes (pprContext theta)