2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 \section[TcMonoType]{Typechecking user-specified @MonoTypes@}
7 module TcMonoType ( tcHsSigType, tcHsType, tcIfaceType, tcHsTheta,
11 kcHsTyVar, kcHsTyVars, mkTyClTyVars,
12 kcHsType, kcHsSigType, kcHsSigTypes,
13 kcHsLiftedSigType, kcHsContext,
14 tcAddScopedTyVars, tcHsTyVars, mkImmutTyVars,
16 TcSigInfo(..), tcTySig, mkTcSig, maybeSig
19 #include "HsVersions.h"
21 import HsSyn ( HsType(..), HsTyVarBndr(..),
22 Sig(..), HsPred(..), pprParendHsType, HsTupCon(..), hsTyVarNames )
23 import RnHsSyn ( RenamedHsType, RenamedHsPred, RenamedContext, RenamedSig, extractHsTyVars )
24 import TcHsSyn ( TcId )
27 import TcEnv ( tcExtendTyVarEnv, tcLookup, tcLookupGlobal,
29 TyThing(..), TcTyThing(..), tcExtendKindEnv
31 import TcMType ( newKindVar, tcInstSigTyVars, zonkKindEnv,
32 checkValidType, UserTypeCtxt(..), pprUserTypeCtxt
34 import TcUnify ( unifyKind, unifyOpenTypeKind )
35 import TcType ( Type, Kind, SourceType(..), ThetaType, TyVarDetails(..),
36 TcTyVar, TcKind, TcThetaType, TcTauType,
37 mkTyVarTy, mkTyVarTys, mkFunTy, mkSynTy,
38 tcSplitForAllTys, tcSplitRhoTy,
39 hoistForAllTys, zipFunTys,
40 mkSigmaTy, mkPredTy, mkTyConApp, mkAppTys,
41 liftedTypeKind, unliftedTypeKind, mkArrowKind,
42 mkArrowKinds, tcSplitFunTy_maybe
45 import Inst ( Inst, InstOrigin(..), newMethodWithGivenTy, instToId )
46 import Subst ( mkTopTyVarSubst, substTy )
47 import Id ( mkLocalId, idName, idType )
48 import Var ( TyVar, mkTyVar, tyVarKind )
49 import ErrUtils ( Message )
50 import TyCon ( TyCon, isSynTyCon, tyConKind )
51 import Class ( classTyCon )
54 import TysWiredIn ( mkListTy, mkTupleTy, genUnitTyCon )
55 import BasicTypes ( Boxity(..) )
56 import SrcLoc ( SrcLoc )
57 import Util ( lengthIs )
63 %************************************************************************
65 \subsection{Checking types}
67 %************************************************************************
69 Generally speaking we now type-check types in three phases
71 1. Kind check the HsType [kcHsType]
72 2. Convert from HsType to Type, and hoist the foralls [tcHsType]
73 3. Check the validity of the resulting type [checkValidType]
75 Often these steps are done one after the othe (tcHsSigType).
76 But in mutually recursive groups of type and class decls we do
77 1 kind-check the whole group
78 2 build TyCons/Classes in a knot-tied wa
79 3 check the validity of types in the now-unknotted TyCons/Classes
82 tcHsSigType :: UserTypeCtxt -> RenamedHsType -> TcM Type
83 -- Do kind checking, and hoist for-alls to the top
84 tcHsSigType ctxt ty = tcAddErrCtxt (checkTypeCtxt ctxt ty) (
85 kcTypeType ty `thenTc_`
88 checkValidType ctxt ty' `thenTc_`
92 = vcat [ptext SLIT("In the type:") <+> ppr ty,
93 ptext SLIT("While checking") <+> pprUserTypeCtxt ctxt ]
95 tcHsType :: RenamedHsType -> TcM Type
96 -- Don't do kind checking, nor validity checking,
97 -- but do hoist for-alls to the top
98 -- This is used in type and class decls, where kinding is
99 -- done in advance, and validity checking is done later
100 -- [Validity checking done later because of knot-tying issues.]
101 tcHsType ty = tc_type ty `thenTc` \ ty' ->
102 returnTc (hoistForAllTys ty')
104 tcHsTheta :: RenamedContext -> TcM ThetaType
105 -- Used when we are expecting a ClassContext (i.e. no implicit params)
106 -- Does not do validity checking, like tcHsType
107 tcHsTheta hs_theta = mapTc tc_pred hs_theta
109 -- In interface files the type is already kinded,
110 -- and we definitely don't want to hoist for-alls.
111 -- Otherwise we'll change
112 -- dmfail :: forall m:(*->*) Monad m => forall a:* => String -> m a
114 -- dmfail :: forall m:(*->*) a:* Monad m => String -> m a
115 -- which definitely isn't right!
116 tcIfaceType ty = tc_type ty
120 %************************************************************************
122 \subsection{Kind checking}
124 %************************************************************************
128 When we come across the binding site for some type variables, we
129 proceed in two stages
131 1. Figure out what kind each tyvar has
133 2. Create suitably-kinded tyvars,
135 and typecheck the body
137 To do step 1, we proceed thus:
139 1a. Bind each type variable to a kind variable
140 1b. Apply the kind checker
141 1c. Zonk the resulting kinds
143 The kind checker is passed to tcHsTyVars as an argument.
145 For example, when we find
146 (forall a m. m a -> m a)
147 we bind a,m to kind varibles and kind-check (m a -> m a). This
148 makes a get kind *, and m get kind *->*. Now we typecheck (m a -> m a)
149 in an environment that binds a and m suitably.
151 The kind checker passed to tcHsTyVars needs to look at enough to
152 establish the kind of the tyvar:
153 * For a group of type and class decls, it's just the group, not
154 the rest of the program
155 * For a tyvar bound in a pattern type signature, its the types
156 mentioned in the other type signatures in that bunch of patterns
157 * For a tyvar bound in a RULE, it's the type signatures on other
158 universally quantified variables in the rule
160 Note that this may occasionally give surprising results. For example:
162 data T a b = MkT (a b)
164 Here we deduce a::*->*, b::*.
165 But equally valid would be
166 a::(*->*)-> *, b::*->*
169 -- tcHsTyVars is used for type variables in type signatures
170 -- e.g. forall a. a->a
171 -- They are immutable, because they scope only over the signature
172 -- They may or may not be explicitly-kinded
173 tcHsTyVars :: [HsTyVarBndr Name]
174 -> TcM a -- The kind checker
175 -> ([TyVar] -> TcM b)
178 tcHsTyVars [] kind_check thing_inside = thing_inside []
179 -- A useful short cut for a common case!
181 tcHsTyVars tv_names kind_check thing_inside
182 = kcHsTyVars tv_names `thenNF_Tc` \ tv_names_w_kinds ->
183 tcExtendKindEnv tv_names_w_kinds kind_check `thenTc_`
184 zonkKindEnv tv_names_w_kinds `thenNF_Tc` \ tvs_w_kinds ->
186 tyvars = mkImmutTyVars tvs_w_kinds
188 tcExtendTyVarEnv tyvars (thing_inside tyvars)
192 tcAddScopedTyVars :: [RenamedHsType] -> TcM a -> TcM a
193 -- tcAddScopedTyVars is used for scoped type variables
194 -- added by pattern type signatures
195 -- e.g. \ (x::a) (y::a) -> x+y
196 -- They never have explicit kinds (because this is source-code only)
197 -- They are mutable (because they can get bound to a more specific type)
199 -- Find the not-already-in-scope signature type variables,
200 -- kind-check them, and bring them into scope
202 -- We no longer specify that these type variables must be univerally
203 -- quantified (lots of email on the subject). If you want to put that
204 -- back in, you need to
205 -- a) Do a checkSigTyVars after thing_inside
206 -- b) More insidiously, don't pass in expected_ty, else
207 -- we unify with it too early and checkSigTyVars barfs
208 -- Instead you have to pass in a fresh ty var, and unify
209 -- it with expected_ty afterwards
210 tcAddScopedTyVars [] thing_inside
211 = thing_inside -- Quick get-out for the empty case
213 tcAddScopedTyVars sig_tys thing_inside
214 = tcGetEnv `thenNF_Tc` \ env ->
216 all_sig_tvs = foldr (unionNameSets . extractHsTyVars) emptyNameSet sig_tys
217 sig_tvs = filter not_in_scope (nameSetToList all_sig_tvs)
218 not_in_scope tv = not (tcInLocalScope env tv)
220 mapNF_Tc newNamedKindVar sig_tvs `thenTc` \ kind_env ->
221 tcExtendKindEnv kind_env (kcHsSigTypes sig_tys) `thenTc_`
222 zonkKindEnv kind_env `thenNF_Tc` \ tvs_w_kinds ->
223 listTc [ tcNewMutTyVar name kind PatSigTv
224 | (name, kind) <- tvs_w_kinds] `thenNF_Tc` \ tyvars ->
225 tcExtendTyVarEnv tyvars thing_inside
230 kcHsTyVar :: HsTyVarBndr name -> NF_TcM (name, TcKind)
231 kcHsTyVars :: [HsTyVarBndr name] -> NF_TcM [(name, TcKind)]
233 kcHsTyVar (UserTyVar name) = newNamedKindVar name
234 kcHsTyVar (IfaceTyVar name kind) = returnNF_Tc (name, kind)
236 kcHsTyVars tvs = mapNF_Tc kcHsTyVar tvs
238 newNamedKindVar name = newKindVar `thenNF_Tc` \ kind ->
239 returnNF_Tc (name, kind)
241 ---------------------------
242 kcLiftedType :: RenamedHsType -> TcM ()
243 -- The type ty must be a *lifted* *type*
245 = kcHsType ty `thenTc` \ kind ->
246 tcAddErrCtxt (typeKindCtxt ty) $
247 unifyKind liftedTypeKind kind
249 ---------------------------
250 kcTypeType :: RenamedHsType -> TcM ()
251 -- The type ty must be a *type*, but it can be lifted or unlifted.
253 = kcHsType ty `thenTc` \ kind ->
254 tcAddErrCtxt (typeKindCtxt ty) $
255 unifyOpenTypeKind kind
257 ---------------------------
258 kcHsSigType, kcHsLiftedSigType :: RenamedHsType -> TcM ()
259 -- Used for type signatures
260 kcHsSigType = kcTypeType
261 kcHsSigTypes tys = mapTc_ kcHsSigType tys
262 kcHsLiftedSigType = kcLiftedType
264 ---------------------------
265 kcHsType :: RenamedHsType -> TcM TcKind
266 kcHsType (HsTyVar name) = kcTyVar name
268 kcHsType (HsListTy ty)
269 = kcLiftedType ty `thenTc` \ tau_ty ->
270 returnTc liftedTypeKind
272 kcHsType (HsTupleTy (HsTupCon _ boxity _) tys)
273 = mapTc kcTypeType tys `thenTc_`
274 returnTc (case boxity of
275 Boxed -> liftedTypeKind
276 Unboxed -> unliftedTypeKind)
278 kcHsType (HsFunTy ty1 ty2)
279 = kcTypeType ty1 `thenTc_`
280 kcTypeType ty2 `thenTc_`
281 returnTc liftedTypeKind
283 kcHsType (HsNumTy _) -- The unit type for generics
284 = returnTc liftedTypeKind
286 kcHsType ty@(HsOpTy ty1 op ty2)
287 = kcTyVar op `thenTc` \ op_kind ->
288 kcHsType ty1 `thenTc` \ ty1_kind ->
289 kcHsType ty2 `thenTc` \ ty2_kind ->
290 tcAddErrCtxt (appKindCtxt (ppr ty)) $
291 kcAppKind op_kind ty1_kind `thenTc` \ op_kind' ->
292 kcAppKind op_kind' ty2_kind
294 kcHsType (HsPredTy pred)
295 = kcHsPred pred `thenTc_`
296 returnTc liftedTypeKind
298 kcHsType ty@(HsAppTy ty1 ty2)
299 = kcHsType ty1 `thenTc` \ tc_kind ->
300 kcHsType ty2 `thenTc` \ arg_kind ->
301 tcAddErrCtxt (appKindCtxt (ppr ty)) $
302 kcAppKind tc_kind arg_kind
304 kcHsType (HsForAllTy (Just tv_names) context ty)
305 = kcHsTyVars tv_names `thenNF_Tc` \ kind_env ->
306 tcExtendKindEnv kind_env $
307 kcHsContext context `thenTc_`
308 kcHsType ty `thenTc_`
309 returnTc liftedTypeKind
311 ---------------------------
312 kcAppKind fun_kind arg_kind
313 = case tcSplitFunTy_maybe fun_kind of
314 Just (arg_kind', res_kind)
315 -> unifyKind arg_kind arg_kind' `thenTc_`
318 Nothing -> newKindVar `thenNF_Tc` \ res_kind ->
319 unifyKind fun_kind (mkArrowKind arg_kind res_kind) `thenTc_`
323 ---------------------------
324 kcHsContext ctxt = mapTc_ kcHsPred ctxt
326 kcHsPred :: RenamedHsPred -> TcM ()
327 kcHsPred pred@(HsIParam name ty)
328 = tcAddErrCtxt (appKindCtxt (ppr pred)) $
331 kcHsPred pred@(HsClassP cls tys)
332 = tcAddErrCtxt (appKindCtxt (ppr pred)) $
333 kcClass cls `thenTc` \ kind ->
334 mapTc kcHsType tys `thenTc` \ arg_kinds ->
335 unifyKind kind (mkArrowKinds arg_kinds liftedTypeKind)
337 ---------------------------
338 kcTyVar name -- Could be a tyvar or a tycon
339 = tcLookup name `thenTc` \ thing ->
341 AThing kind -> returnTc kind
342 ATyVar tv -> returnTc (tyVarKind tv)
343 AGlobal (ATyCon tc) -> returnTc (tyConKind tc)
344 other -> failWithTc (wrongThingErr "type" thing name)
346 kcClass cls -- Must be a class
347 = tcLookup cls `thenNF_Tc` \ thing ->
349 AThing kind -> returnTc kind
350 AGlobal (AClass cls) -> returnTc (tyConKind (classTyCon cls))
351 other -> failWithTc (wrongThingErr "class" thing cls)
354 %************************************************************************
358 %************************************************************************
360 tc_type, the main work horse
361 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
367 tc_type is used to typecheck the types in the RHS of data
368 constructors. In the case of recursive data types, that means that
369 the type constructors themselves are (partly) black holes. e.g.
371 data T a = MkT a [T a]
373 While typechecking the [T a] on the RHS, T itself is not yet fully
374 defined. That in turn places restrictions on what you can check in
375 tcHsType; if you poke on too much you get a black hole. I keep
376 forgetting this, hence this warning!
378 So tc_type does no validity-checking. Instead that's all done
379 by TcMType.checkValidType
381 --------------------------
382 *** END OF BIG WARNING ***
383 --------------------------
387 tc_type :: RenamedHsType -> TcM Type
389 tc_type ty@(HsTyVar name)
392 tc_type (HsListTy ty)
393 = tc_type ty `thenTc` \ tau_ty ->
394 returnTc (mkListTy tau_ty)
396 tc_type (HsTupleTy (HsTupCon _ boxity arity) tys)
397 = ASSERT( tys `lengthIs` arity )
398 tc_types tys `thenTc` \ tau_tys ->
399 returnTc (mkTupleTy boxity arity tau_tys)
401 tc_type (HsFunTy ty1 ty2)
402 = tc_type ty1 `thenTc` \ tau_ty1 ->
403 tc_type ty2 `thenTc` \ tau_ty2 ->
404 returnTc (mkFunTy tau_ty1 tau_ty2)
408 returnTc (mkTyConApp genUnitTyCon [])
410 tc_type (HsOpTy ty1 op ty2)
411 = tc_type ty1 `thenTc` \ tau_ty1 ->
412 tc_type ty2 `thenTc` \ tau_ty2 ->
413 tc_fun_type op [tau_ty1,tau_ty2]
415 tc_type (HsAppTy ty1 ty2) = tc_app ty1 [ty2]
417 tc_type (HsPredTy pred)
418 = tc_pred pred `thenTc` \ pred' ->
419 returnTc (mkPredTy pred')
421 tc_type full_ty@(HsForAllTy (Just tv_names) ctxt ty)
423 kind_check = kcHsContext ctxt `thenTc_` kcHsType ty
425 tcHsTyVars tv_names kind_check $ \ tyvars ->
426 mapTc tc_pred ctxt `thenTc` \ theta ->
427 tc_type ty `thenTc` \ tau ->
428 returnTc (mkSigmaTy tyvars theta tau)
430 tc_types arg_tys = mapTc tc_type arg_tys
433 Help functions for type applications
434 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
437 tc_app :: RenamedHsType -> [RenamedHsType] -> TcM Type
438 tc_app (HsAppTy ty1 ty2) tys
439 = tc_app ty1 (ty2:tys)
442 = tcAddErrCtxt (appKindCtxt pp_app) $
443 tc_types tys `thenTc` \ arg_tys ->
445 HsTyVar fun -> tc_fun_type fun arg_tys
446 other -> tc_type 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 -> returnTc (mkSynTy tc arg_tys)
462 | otherwise -> returnTc (mkTyConApp tc arg_tys)
464 other -> failWithTc (wrongThingErr "type constructor" thing name)
471 tc_pred assn@(HsClassP class_name tys)
472 = tcAddErrCtxt (appKindCtxt (ppr assn)) $
473 tc_types tys `thenTc` \ arg_tys ->
474 tcLookupGlobal class_name `thenTc` \ thing ->
476 AClass clas -> returnTc (ClassP clas arg_tys)
477 other -> failWithTc (wrongThingErr "class" (AGlobal thing) class_name)
479 tc_pred assn@(HsIParam name ty)
480 = tcAddErrCtxt (appKindCtxt (ppr assn)) $
481 tc_type ty `thenTc` \ arg_ty ->
482 returnTc (IParam name arg_ty)
487 %************************************************************************
489 \subsection{Type variables, with knot tying!}
491 %************************************************************************
494 mkImmutTyVars :: [(Name,Kind)] -> [TyVar]
495 mkImmutTyVars pairs = [mkTyVar name kind | (name, kind) <- pairs]
497 mkTyClTyVars :: Kind -- Kind of the tycon or class
498 -> [HsTyVarBndr Name]
500 mkTyClTyVars kind tyvar_names
501 = mkImmutTyVars tyvars_w_kinds
503 (tyvars_w_kinds, _) = zipFunTys (hsTyVarNames tyvar_names) kind
507 %************************************************************************
509 \subsection{Signatures}
511 %************************************************************************
513 @tcSigs@ checks the signatures for validity, and returns a list of
514 {\em freshly-instantiated} signatures. That is, the types are already
515 split up, and have fresh type variables installed. All non-type-signature
516 "RenamedSigs" are ignored.
518 The @TcSigInfo@ contains @TcTypes@ because they are unified with
519 the variable's type, and after that checked to see whether they've
525 Name -- N, the Name in corresponding binding
527 TcId -- *Polymorphic* binder for this value...
534 TcId -- *Monomorphic* binder for this value
535 -- Does *not* have name = N
538 [Inst] -- Empty if theta is null, or
539 -- (method mono_id) otherwise
541 SrcLoc -- Of the signature
543 instance Outputable TcSigInfo where
544 ppr (TySigInfo nm id tyvars theta tau _ inst loc) =
545 ppr nm <+> ptext SLIT("::") <+> ppr tyvars <+> ppr theta <+> ptext SLIT("=>") <+> ppr tau
547 maybeSig :: [TcSigInfo] -> Name -> Maybe (TcSigInfo)
548 -- Search for a particular signature
549 maybeSig [] name = Nothing
550 maybeSig (sig@(TySigInfo sig_name _ _ _ _ _ _ _) : sigs) name
551 | name == sig_name = Just sig
552 | otherwise = maybeSig sigs name
557 tcTySig :: RenamedSig -> TcM TcSigInfo
559 tcTySig (Sig v ty src_loc)
560 = tcAddSrcLoc src_loc $
561 tcHsSigType (FunSigCtxt v) ty `thenTc` \ sigma_tc_ty ->
562 mkTcSig (mkLocalId v sigma_tc_ty) src_loc `thenNF_Tc` \ sig ->
565 mkTcSig :: TcId -> SrcLoc -> NF_TcM TcSigInfo
566 mkTcSig poly_id src_loc
567 = -- Instantiate this type
568 -- It's important to do this even though in the error-free case
569 -- we could just split the sigma_tc_ty (since the tyvars don't
570 -- unified with anything). But in the case of an error, when
571 -- the tyvars *do* get unified with something, we want to carry on
572 -- typechecking the rest of the program with the function bound
573 -- to a pristine type, namely sigma_tc_ty
575 (tyvars, rho) = tcSplitForAllTys (idType poly_id)
577 tcInstSigTyVars SigTv tyvars `thenNF_Tc` \ tyvars' ->
578 -- Make *signature* type variables
581 tyvar_tys' = mkTyVarTys tyvars'
582 rho' = substTy (mkTopTyVarSubst tyvars tyvar_tys') rho
583 -- mkTopTyVarSubst because the tyvars' are fresh
585 (theta', tau') = tcSplitRhoTy rho'
586 -- This splitRhoTy tries hard to make sure that tau' is a type synonym
587 -- wherever possible, which can improve interface files.
589 newMethodWithGivenTy SignatureOrigin
592 theta' tau' `thenNF_Tc` \ inst ->
593 -- We make a Method even if it's not overloaded; no harm
595 returnNF_Tc (TySigInfo name poly_id tyvars' theta' tau' (instToId inst) [inst] src_loc)
597 name = idName poly_id
602 %************************************************************************
604 \subsection{Errors and contexts}
606 %************************************************************************
609 typeKindCtxt :: RenamedHsType -> Message
610 typeKindCtxt ty = sep [ptext SLIT("When checking that"),
611 nest 2 (quotes (ppr ty)),
612 ptext SLIT("is a type")]
614 appKindCtxt :: SDoc -> Message
615 appKindCtxt pp = ptext SLIT("When checking kinds in") <+> quotes pp
617 wrongThingErr expected thing name
618 = pp_thing thing <+> quotes (ppr name) <+> ptext SLIT("used as a") <+> text expected
620 pp_thing (AGlobal (ATyCon _)) = ptext SLIT("Type constructor")
621 pp_thing (AGlobal (AClass _)) = ptext SLIT("Class")
622 pp_thing (AGlobal (AnId _)) = ptext SLIT("Identifier")
623 pp_thing (ATyVar _) = ptext SLIT("Type variable")
624 pp_thing (ATcId _) = ptext SLIT("Local identifier")
625 pp_thing (AThing _) = ptext SLIT("Utterly bogus")