2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 \section[TcMonoType]{Typechecking user-specified @MonoTypes@}
7 module TcMonoType ( tcHsType, tcHsRecType, tcIfaceType,
8 tcHsSigType, tcHsLiftedSigType,
9 tcRecTheta, checkAmbiguity,
12 kcHsTyVar, kcHsTyVars, mkTyClTyVars,
13 kcHsType, kcHsSigType, kcHsSigTypes,
14 kcHsLiftedSigType, kcHsContext,
15 tcScopedTyVars, tcHsTyVars, mkImmutTyVars,
17 TcSigInfo(..), tcTySig, mkTcSig, maybeSig,
18 checkSigTyVars, sigCtxt, sigPatCtxt
21 #include "HsVersions.h"
23 import HsSyn ( HsType(..), HsTyVarBndr(..),
24 Sig(..), HsPred(..), pprParendHsType, HsTupCon(..), hsTyVarNames )
25 import RnHsSyn ( RenamedHsType, RenamedHsPred, RenamedContext, RenamedSig )
26 import TcHsSyn ( TcId )
29 import TcEnv ( tcExtendTyVarEnv, tcLookup, tcLookupGlobal,
30 tcGetGlobalTyVars, tcEnvTcIds, tcEnvTyVars,
31 TyThing(..), TcTyThing(..), tcExtendKindEnv
33 import TcType ( TcKind, TcTyVar, TcThetaType, TcTauType,
34 newKindVar, tcInstSigVars,
35 zonkKindEnv, zonkTcType, zonkTcTyVars, zonkTcTyVar
37 import Inst ( Inst, InstOrigin(..), newMethodWithGivenTy, instToId )
38 import FunDeps ( grow )
39 import TcUnify ( unifyKind, unifyOpenTypeKind )
40 import Unify ( allDistinctTyVars )
41 import Type ( Type, Kind, PredType(..), ThetaType, SigmaType, TauType,
42 mkTyVarTy, mkTyVarTys, mkFunTy, mkSynTy,
43 zipFunTys, hoistForAllTys,
44 mkSigmaTy, mkPredTy, mkTyConApp,
45 mkAppTys, splitForAllTys, splitRhoTy, mkRhoTy,
46 liftedTypeKind, unliftedTypeKind, mkArrowKind,
47 mkArrowKinds, getTyVar_maybe, getTyVar, splitFunTy_maybe,
48 tidyOpenType, tidyOpenTypes, tidyTyVar, tidyTyVars,
49 tyVarsOfType, tyVarsOfPred, mkForAllTys,
50 isUnboxedTupleType, isForAllTy, isIPPred
52 import PprType ( pprType, pprTheta, pprPred )
53 import Subst ( mkTopTyVarSubst, substTy )
54 import CoreFVs ( idFreeTyVars )
55 import Id ( mkLocalId, idName, idType )
56 import Var ( Id, Var, TyVar, mkTyVar, tyVarKind )
59 import ErrUtils ( Message )
60 import TyCon ( TyCon, isSynTyCon, tyConArity, tyConKind )
61 import Class ( classArity, classTyCon )
63 import TysWiredIn ( mkListTy, mkTupleTy, genUnitTyCon )
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 is used for type variables in type signatures
122 -- e.g. forall a. a->a
123 -- They are immutable, because they scope only over the signature
124 -- They may or may not be explicitly-kinded
125 tcHsTyVars :: [HsTyVarBndr Name]
126 -> TcM a -- The kind checker
127 -> ([TyVar] -> TcM b)
130 tcHsTyVars [] kind_check thing_inside = thing_inside []
131 -- A useful short cut for a common case!
133 tcHsTyVars tv_names kind_check thing_inside
134 = kcHsTyVars tv_names `thenNF_Tc` \ tv_names_w_kinds ->
135 tcExtendKindEnv tv_names_w_kinds kind_check `thenTc_`
136 zonkKindEnv tv_names_w_kinds `thenNF_Tc` \ tvs_w_kinds ->
138 tyvars = mkImmutTyVars tvs_w_kinds
140 tcExtendTyVarEnv tyvars (thing_inside tyvars)
142 -- tcScopedTyVars is used for scoped type variables
143 -- e.g. \ (x::a) (y::a) -> x+y
144 -- They never have explicit kinds (because this is source-code only)
145 -- They are mutable (because they can get bound to a more specific type)
146 tcScopedTyVars :: [Name]
147 -> TcM a -- The kind checker
150 tcScopedTyVars [] kind_check thing_inside = thing_inside
152 tcScopedTyVars tv_names kind_check thing_inside
153 = mapNF_Tc newNamedKindVar tv_names `thenTc` \ kind_env ->
154 tcExtendKindEnv kind_env kind_check `thenTc_`
155 zonkKindEnv kind_env `thenNF_Tc` \ tvs_w_kinds ->
156 listTc [tcNewMutTyVar name kind | (name, kind) <- tvs_w_kinds] `thenNF_Tc` \ tyvars ->
157 tcExtendTyVarEnv tyvars thing_inside
162 kcHsTyVar :: HsTyVarBndr name -> NF_TcM (name, TcKind)
163 kcHsTyVars :: [HsTyVarBndr name] -> NF_TcM [(name, TcKind)]
165 kcHsTyVar (UserTyVar name) = newNamedKindVar name
166 kcHsTyVar (IfaceTyVar name kind) = returnNF_Tc (name, kind)
168 kcHsTyVars tvs = mapNF_Tc kcHsTyVar tvs
170 newNamedKindVar name = newKindVar `thenNF_Tc` \ kind ->
171 returnNF_Tc (name, kind)
173 ---------------------------
174 kcLiftedType :: RenamedHsType -> TcM ()
175 -- The type ty must be a *lifted* *type*
177 = kcHsType ty `thenTc` \ kind ->
178 tcAddErrCtxt (typeKindCtxt ty) $
179 unifyKind liftedTypeKind kind
181 ---------------------------
182 kcTypeType :: RenamedHsType -> TcM ()
183 -- The type ty must be a *type*, but it can be lifted or unlifted.
185 = kcHsType ty `thenTc` \ kind ->
186 tcAddErrCtxt (typeKindCtxt ty) $
187 unifyOpenTypeKind kind
189 ---------------------------
190 kcHsSigType, kcHsLiftedSigType :: RenamedHsType -> TcM ()
191 -- Used for type signatures
192 kcHsSigType = kcTypeType
193 kcHsSigTypes tys = mapTc_ kcHsSigType tys
194 kcHsLiftedSigType = kcLiftedType
196 ---------------------------
197 kcHsType :: RenamedHsType -> TcM TcKind
198 kcHsType (HsTyVar name) = kcTyVar name
200 kcHsType (HsListTy ty)
201 = kcLiftedType ty `thenTc` \ tau_ty ->
202 returnTc liftedTypeKind
204 kcHsType (HsTupleTy (HsTupCon _ boxity _) tys)
205 = mapTc kcTypeType tys `thenTc_`
206 returnTc (case boxity of
207 Boxed -> liftedTypeKind
208 Unboxed -> unliftedTypeKind)
210 kcHsType (HsFunTy ty1 ty2)
211 = kcTypeType ty1 `thenTc_`
212 kcTypeType ty2 `thenTc_`
213 returnTc liftedTypeKind
215 kcHsType ty@(HsOpTy ty1 op ty2)
216 = kcTyVar op `thenTc` \ op_kind ->
217 kcHsType ty1 `thenTc` \ ty1_kind ->
218 kcHsType ty2 `thenTc` \ ty2_kind ->
219 tcAddErrCtxt (appKindCtxt (ppr ty)) $
220 kcAppKind op_kind ty1_kind `thenTc` \ op_kind' ->
221 kcAppKind op_kind' ty2_kind
223 kcHsType (HsPredTy pred)
224 = kcHsPred pred `thenTc_`
225 returnTc liftedTypeKind
227 kcHsType ty@(HsAppTy ty1 ty2)
228 = kcHsType ty1 `thenTc` \ tc_kind ->
229 kcHsType ty2 `thenTc` \ arg_kind ->
230 tcAddErrCtxt (appKindCtxt (ppr ty)) $
231 kcAppKind tc_kind arg_kind
233 kcHsType (HsForAllTy (Just tv_names) context ty)
234 = kcHsTyVars tv_names `thenNF_Tc` \ kind_env ->
235 tcExtendKindEnv kind_env $
236 kcHsContext context `thenTc_`
237 kcHsType ty `thenTc_`
238 returnTc liftedTypeKind
240 ---------------------------
241 kcAppKind fun_kind arg_kind
242 = case splitFunTy_maybe fun_kind of
243 Just (arg_kind', res_kind)
244 -> unifyKind arg_kind arg_kind' `thenTc_`
247 Nothing -> newKindVar `thenNF_Tc` \ res_kind ->
248 unifyKind fun_kind (mkArrowKind arg_kind res_kind) `thenTc_`
252 ---------------------------
253 kcHsContext ctxt = mapTc_ kcHsPred ctxt
255 kcHsPred :: RenamedHsPred -> TcM ()
256 kcHsPred pred@(HsIParam name ty)
257 = tcAddErrCtxt (appKindCtxt (ppr pred)) $
260 kcHsPred pred@(HsClassP cls tys)
261 = tcAddErrCtxt (appKindCtxt (ppr pred)) $
262 kcClass cls `thenTc` \ kind ->
263 mapTc kcHsType tys `thenTc` \ arg_kinds ->
264 unifyKind kind (mkArrowKinds arg_kinds liftedTypeKind)
266 ---------------------------
267 kcTyVar name -- Could be a tyvar or a tycon
268 = tcLookup name `thenTc` \ thing ->
270 AThing kind -> returnTc kind
271 ATyVar tv -> returnTc (tyVarKind tv)
272 AGlobal (ATyCon tc) -> returnTc (tyConKind tc)
273 other -> failWithTc (wrongThingErr "type" thing name)
275 kcClass cls -- Must be a class
276 = tcLookup cls `thenNF_Tc` \ thing ->
278 AThing kind -> returnTc kind
279 AGlobal (AClass cls) -> returnTc (tyConKind (classTyCon cls))
280 other -> failWithTc (wrongThingErr "class" thing cls)
283 %************************************************************************
285 \subsection{Checking types}
287 %************************************************************************
289 tcHsSigType and tcHsLiftedSigType
290 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
292 tcHsSigType and tcHsLiftedSigType are used for type signatures written by the programmer
294 * We hoist any inner for-alls to the top
296 * Notice that we kind-check first, because the type-check assumes
297 that the kinds are already checked.
299 * They are only called when there are no kind vars in the environment
300 so the kind returned is indeed a Kind not a TcKind
303 tcHsSigType, tcHsLiftedSigType :: RenamedHsType -> TcM Type
304 -- Do kind checking, and hoist for-alls to the top
305 tcHsSigType ty = kcTypeType ty `thenTc_` tcHsType ty
306 tcHsLiftedSigType ty = kcLiftedType ty `thenTc_` tcHsType ty
308 tcHsType :: RenamedHsType -> TcM Type
309 tcHsRecType :: RecFlag -> RenamedHsType -> TcM Type
310 -- Don't do kind checking, but do hoist for-alls to the top
311 -- These are used in type and class decls, where kinding is
313 tcHsType ty = tc_type NonRecursive ty `thenTc` \ ty' -> returnTc (hoistForAllTys ty')
314 tcHsRecType wimp_out ty = tc_type wimp_out ty `thenTc` \ ty' -> returnTc (hoistForAllTys ty')
316 -- In interface files the type is already kinded,
317 -- and we definitely don't want to hoist for-alls.
318 -- Otherwise we'll change
319 -- dmfail :: forall m:(*->*) Monad m => forall a:* => String -> m a
321 -- dmfail :: forall m:(*->*) a:* Monad m => String -> m a
322 -- which definitely isn't right!
323 tcIfaceType ty = tc_type NonRecursive ty
327 %************************************************************************
331 %************************************************************************
333 tc_type, the main work horse
334 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
340 tc_type is used to typecheck the types in the RHS of data
341 constructors. In the case of recursive data types, that means that
342 the type constructors themselves are (partly) black holes. e.g.
344 data T a = MkT a [T a]
346 While typechecking the [T a] on the RHS, T itself is not yet fully
347 defined. That in turn places restrictions on what you can check in
348 tcHsType; if you poke on too much you get a black hole. I keep
349 forgetting this, hence this warning!
351 The wimp_out argument tells when we are in a mutually-recursive
352 group of type declarations, so omit various checks else we
353 get a black hole. They'll be done again later, in TcTyClDecls.tcGroup.
355 --------------------------
356 *** END OF BIG WARNING ***
357 --------------------------
361 tc_type :: RecFlag -> RenamedHsType -> TcM Type
363 tc_type wimp_out ty@(HsTyVar name)
364 = tc_app wimp_out ty []
366 tc_type wimp_out (HsListTy ty)
367 = tc_arg_type wimp_out ty `thenTc` \ tau_ty ->
368 returnTc (mkListTy tau_ty)
370 tc_type wimp_out (HsTupleTy (HsTupCon _ boxity arity) tys)
371 = ASSERT( arity == length tys )
372 mapTc tc_tup_arg tys `thenTc` \ tau_tys ->
373 returnTc (mkTupleTy boxity arity tau_tys)
375 tc_tup_arg = case boxity of
376 Boxed -> tc_arg_type wimp_out
377 Unboxed -> tc_type wimp_out
378 -- Unboxed tuples can have polymorphic or unboxed args.
379 -- This happens in the workers for functions returning
380 -- product types with polymorphic components
382 tc_type wimp_out (HsFunTy ty1 ty2)
383 = tc_type wimp_out ty1 `thenTc` \ tau_ty1 ->
384 -- Function argument can be polymorphic, but
385 -- must not be an unboxed tuple
387 -- In a recursive loop we can't ask whether the thing is
388 -- unboxed -- might be a synonym inside a synonym inside a group
389 checkTc (isRec wimp_out || not (isUnboxedTupleType tau_ty1))
390 (ubxArgTyErr ty1) `thenTc_`
391 tc_type wimp_out ty2 `thenTc` \ tau_ty2 ->
392 returnTc (mkFunTy tau_ty1 tau_ty2)
394 tc_type wimp_out (HsNumTy n)
396 returnTc (mkTyConApp genUnitTyCon [])
398 tc_type wimp_out (HsOpTy ty1 op ty2) =
399 tc_arg_type wimp_out ty1 `thenTc` \ tau_ty1 ->
400 tc_arg_type wimp_out ty2 `thenTc` \ tau_ty2 ->
401 tc_fun_type op [tau_ty1,tau_ty2]
403 tc_type wimp_out (HsAppTy ty1 ty2)
404 = tc_app wimp_out ty1 [ty2]
406 tc_type wimp_out (HsPredTy pred)
407 = tc_pred wimp_out pred `thenTc` \ pred' ->
408 returnTc (mkPredTy pred')
410 tc_type wimp_out full_ty@(HsForAllTy (Just tv_names) ctxt ty)
412 kind_check = kcHsContext ctxt `thenTc_` kcHsType ty
414 tcHsTyVars tv_names kind_check $ \ tyvars ->
415 tcRecTheta wimp_out ctxt `thenTc` \ theta ->
417 -- Context behaves like a function type
418 -- This matters. Return-unboxed-tuple analysis can
419 -- give overloaded functions like
420 -- f :: forall a. Num a => (# a->a, a->a #)
421 -- And we want these to get through the type checker
423 tc_arg_type wimp_out ty
428 checkAmbiguity wimp_out is_source tyvars theta tau
430 is_source = case tv_names of
431 (UserTyVar _ : _) -> True
435 -- tc_arg_type checks that the argument of a
436 -- type appplication isn't a for-all type or an unboxed tuple type
437 -- For example, we want to reject things like:
439 -- instance Ord a => Ord (forall s. T s a)
441 -- g :: T s (forall b.b)
443 -- Other unboxed types are very occasionally allowed as type
444 -- arguments depending on the kind of the type constructor
446 tc_arg_type wimp_out arg_ty
448 = tc_type wimp_out arg_ty
451 = tc_type wimp_out arg_ty `thenTc` \ arg_ty' ->
452 checkTc (isRec wimp_out || not (isForAllTy arg_ty')) (polyArgTyErr arg_ty) `thenTc_`
453 checkTc (isRec wimp_out || not (isUnboxedTupleType arg_ty')) (ubxArgTyErr arg_ty) `thenTc_`
456 tc_arg_types wimp_out arg_tys = mapTc (tc_arg_type wimp_out) arg_tys
459 Help functions for type applications
460 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
463 tc_app :: RecFlag -> RenamedHsType -> [RenamedHsType] -> TcM Type
464 tc_app wimp_out (HsAppTy ty1 ty2) tys
465 = tc_app wimp_out ty1 (ty2:tys)
467 tc_app wimp_out ty tys
468 = tcAddErrCtxt (appKindCtxt pp_app) $
469 tc_arg_types wimp_out tys `thenTc` \ arg_tys ->
471 HsTyVar fun -> tc_fun_type fun arg_tys
472 other -> tc_type wimp_out ty `thenTc` \ fun_ty ->
473 returnNF_Tc (mkAppTys fun_ty arg_tys)
475 pp_app = ppr ty <+> sep (map pprParendHsType tys)
477 -- (tc_fun_type ty arg_tys) returns (mkAppTys ty arg_tys)
478 -- But not quite; for synonyms it checks the correct arity, and builds a SynTy
479 -- hence the rather strange functionality.
481 tc_fun_type name arg_tys
482 = tcLookup name `thenTc` \ thing ->
484 ATyVar tv -> returnTc (mkAppTys (mkTyVarTy tv) arg_tys)
487 | isSynTyCon tc -> checkTc arity_ok err_msg `thenTc_`
488 returnTc (mkAppTys (mkSynTy tc (take arity arg_tys))
489 (drop arity arg_tys))
491 | otherwise -> returnTc (mkTyConApp tc arg_tys)
494 arity_ok = arity <= n_args
495 arity = tyConArity tc
496 -- It's OK to have an *over-applied* type synonym
497 -- data Tree a b = ...
498 -- type Foo a = Tree [a]
499 -- f :: Foo a b -> ...
500 err_msg = arityErr "Type synonym" name arity n_args
501 n_args = length arg_tys
503 other -> failWithTc (wrongThingErr "type constructor" thing name)
510 tcRecTheta :: RecFlag -> RenamedContext -> TcM ThetaType
511 -- Used when we are expecting a ClassContext (i.e. no implicit params)
512 tcRecTheta wimp_out context = mapTc (tc_pred wimp_out) context
514 tc_pred wimp_out assn@(HsClassP class_name tys)
515 = tcAddErrCtxt (appKindCtxt (ppr assn)) $
516 tc_arg_types wimp_out tys `thenTc` \ arg_tys ->
517 tcLookupGlobal class_name `thenTc` \ thing ->
519 AClass clas -> checkTc (arity == n_tys) err `thenTc_`
520 returnTc (ClassP clas arg_tys)
522 arity = classArity clas
524 err = arityErr "Class" class_name arity n_tys
526 other -> failWithTc (wrongThingErr "class" (AGlobal thing) class_name)
528 tc_pred wimp_out assn@(HsIParam name ty)
529 = tcAddErrCtxt (appKindCtxt (ppr assn)) $
530 tc_arg_type wimp_out ty `thenTc` \ arg_ty ->
531 returnTc (IParam name arg_ty)
538 is ambiguous if P contains generic variables
539 (i.e. one of the Vs) that are not mentioned in tau
541 However, we need to take account of functional dependencies
542 when we speak of 'mentioned in tau'. Example:
543 class C a b | a -> b where ...
545 forall x y. (C x y) => x
546 is not ambiguous because x is mentioned and x determines y
548 NOTE: In addition, GHC insists that at least one type variable
549 in each constraint is in V. So we disallow a type like
550 forall a. Eq b => b -> b
551 even in a scope where b is in scope.
552 This is the is_free test below.
554 Notes on the 'is_source_polytype' test above
555 Check ambiguity only for source-program types, not
556 for types coming from inteface files. The latter can
557 legitimately have ambiguous types. Example
558 class S a where s :: a -> (Int,Int)
559 instance S Char where s _ = (1,1)
560 f:: S a => [a] -> Int -> (Int,Int)
561 f (_::[a]) x = (a*x,b)
562 where (a,b) = s (undefined::a)
563 Here the worker for f gets the type
564 fw :: forall a. S a => Int -> (# Int, Int #)
566 If the list of tv_names is empty, we have a monotype,
567 and then we don't need to check for ambiguity either,
568 because the test can't fail (see is_ambig).
571 checkAmbiguity :: RecFlag -> Bool
572 -> [TyVar] -> ThetaType -> TauType
574 checkAmbiguity wimp_out is_source_polytype forall_tyvars theta tau
575 | isRec wimp_out = returnTc sigma_ty
576 | otherwise = mapTc_ check_pred theta `thenTc_`
579 sigma_ty = mkSigmaTy forall_tyvars theta tau
580 tau_vars = tyVarsOfType tau
581 extended_tau_vars = grow theta tau_vars
583 -- Hack alert. If there are no tyvars, (ppr sigma_ty) will print
584 -- something strange like {Eq k} -> k -> k, because there is no
585 -- ForAll at the top of the type. Since this is going to the user
586 -- we want it to look like a proper Haskell type even then; hence the hack
588 -- This shows up in the complaint about
590 -- op :: Eq a => a -> a
591 ppr_sigma | null forall_tyvars = pprTheta theta <+> ptext SLIT("=>") <+> ppr tau
592 | otherwise = ppr sigma_ty
594 is_ambig ct_var = (ct_var `elem` forall_tyvars) &&
595 not (ct_var `elemVarSet` extended_tau_vars)
596 is_free ct_var = not (ct_var `elem` forall_tyvars)
598 check_pred pred = checkTc (not any_ambig) (ambigErr pred ppr_sigma) `thenTc_`
599 checkTc (isIPPred pred || not all_free) (freeErr pred ppr_sigma)
601 ct_vars = varSetElems (tyVarsOfPred pred)
602 all_free = all is_free ct_vars
603 any_ambig = is_source_polytype && any is_ambig ct_vars
606 %************************************************************************
608 \subsection{Type variables, with knot tying!}
610 %************************************************************************
613 mkImmutTyVars :: [(Name,Kind)] -> [TyVar]
614 mkImmutTyVars pairs = [mkTyVar name kind | (name, kind) <- pairs]
616 mkTyClTyVars :: Kind -- Kind of the tycon or class
617 -> [HsTyVarBndr Name]
619 mkTyClTyVars kind tyvar_names
620 = mkImmutTyVars tyvars_w_kinds
622 (tyvars_w_kinds, _) = zipFunTys (hsTyVarNames tyvar_names) kind
626 %************************************************************************
628 \subsection{Signatures}
630 %************************************************************************
632 @tcSigs@ checks the signatures for validity, and returns a list of
633 {\em freshly-instantiated} signatures. That is, the types are already
634 split up, and have fresh type variables installed. All non-type-signature
635 "RenamedSigs" are ignored.
637 The @TcSigInfo@ contains @TcTypes@ because they are unified with
638 the variable's type, and after that checked to see whether they've
644 Name -- N, the Name in corresponding binding
646 TcId -- *Polymorphic* binder for this value...
653 TcId -- *Monomorphic* binder for this value
654 -- Does *not* have name = N
657 [Inst] -- Empty if theta is null, or
658 -- (method mono_id) otherwise
660 SrcLoc -- Of the signature
662 instance Outputable TcSigInfo where
663 ppr (TySigInfo nm id tyvars theta tau _ inst loc) =
664 ppr nm <+> ptext SLIT("::") <+> ppr tyvars <+> ppr theta <+> ptext SLIT("=>") <+> ppr tau
666 maybeSig :: [TcSigInfo] -> Name -> Maybe (TcSigInfo)
667 -- Search for a particular signature
668 maybeSig [] name = Nothing
669 maybeSig (sig@(TySigInfo sig_name _ _ _ _ _ _ _) : sigs) name
670 | name == sig_name = Just sig
671 | otherwise = maybeSig sigs name
676 tcTySig :: RenamedSig -> TcM TcSigInfo
678 tcTySig (Sig v ty src_loc)
679 = tcAddSrcLoc src_loc $
680 tcAddErrCtxt (tcsigCtxt v) $
681 tcHsSigType ty `thenTc` \ sigma_tc_ty ->
682 mkTcSig (mkLocalId v sigma_tc_ty) src_loc `thenNF_Tc` \ sig ->
685 mkTcSig :: TcId -> SrcLoc -> NF_TcM TcSigInfo
686 mkTcSig poly_id src_loc
687 = -- Instantiate this type
688 -- It's important to do this even though in the error-free case
689 -- we could just split the sigma_tc_ty (since the tyvars don't
690 -- unified with anything). But in the case of an error, when
691 -- the tyvars *do* get unified with something, we want to carry on
692 -- typechecking the rest of the program with the function bound
693 -- to a pristine type, namely sigma_tc_ty
695 (tyvars, rho) = splitForAllTys (idType poly_id)
697 tcInstSigVars tyvars `thenNF_Tc` \ tyvars' ->
698 -- Make *signature* type variables
701 tyvar_tys' = mkTyVarTys tyvars'
702 rho' = substTy (mkTopTyVarSubst tyvars tyvar_tys') rho
703 -- mkTopTyVarSubst because the tyvars' are fresh
704 (theta', tau') = splitRhoTy rho'
705 -- This splitRhoTy tries hard to make sure that tau' is a type synonym
706 -- wherever possible, which can improve interface files.
708 newMethodWithGivenTy SignatureOrigin
711 theta' tau' `thenNF_Tc` \ inst ->
712 -- We make a Method even if it's not overloaded; no harm
714 returnNF_Tc (TySigInfo name poly_id tyvars' theta' tau' (instToId inst) [inst] src_loc)
716 name = idName poly_id
721 %************************************************************************
723 \subsection{Checking signature type variables}
725 %************************************************************************
727 @checkSigTyVars@ is used after the type in a type signature has been unified with
728 the actual type found. It then checks that the type variables of the type signature
730 (a) Still all type variables
731 eg matching signature [a] against inferred type [(p,q)]
732 [then a will be unified to a non-type variable]
734 (b) Still all distinct
735 eg matching signature [(a,b)] against inferred type [(p,p)]
736 [then a and b will be unified together]
738 (c) Not mentioned in the environment
739 eg the signature for f in this:
745 Here, f is forced to be monorphic by the free occurence of x.
747 (d) Not (unified with another type variable that is) in scope.
748 eg f x :: (r->r) = (\y->y) :: forall a. a->r
749 when checking the expression type signature, we find that
750 even though there is nothing in scope whose type mentions r,
751 nevertheless the type signature for the expression isn't right.
753 Another example is in a class or instance declaration:
755 op :: forall b. a -> b
757 Here, b gets unified with a
759 Before doing this, the substitution is applied to the signature type variable.
761 We used to have the notion of a "DontBind" type variable, which would
762 only be bound to itself or nothing. Then points (a) and (b) were
763 self-checking. But it gave rise to bogus consequential error messages.
766 f = (*) -- Monomorphic
771 Here, we get a complaint when checking the type signature for g,
772 that g isn't polymorphic enough; but then we get another one when
773 dealing with the (Num x) context arising from f's definition;
774 we try to unify x with Int (to default it), but find that x has already
775 been unified with the DontBind variable "a" from g's signature.
776 This is really a problem with side-effecting unification; we'd like to
777 undo g's effects when its type signature fails, but unification is done
778 by side effect, so we can't (easily).
780 So we revert to ordinary type variables for signatures, and try to
781 give a helpful message in checkSigTyVars.
784 checkSigTyVars :: [TcTyVar] -- Universally-quantified type variables in the signature
785 -> TcTyVarSet -- Tyvars that are free in the type signature
786 -- Not necessarily zonked
787 -- These should *already* be in the free-in-env set,
788 -- and are used here only to improve the error message
789 -> TcM [TcTyVar] -- Zonked signature type variables
791 checkSigTyVars [] free = returnTc []
792 checkSigTyVars sig_tyvars free_tyvars
793 = zonkTcTyVars sig_tyvars `thenNF_Tc` \ sig_tys ->
794 tcGetGlobalTyVars `thenNF_Tc` \ globals ->
796 checkTcM (allDistinctTyVars sig_tys globals)
797 (complain sig_tys globals) `thenTc_`
799 returnTc (map (getTyVar "checkSigTyVars") sig_tys)
802 complain sig_tys globals
803 = -- For the in-scope ones, zonk them and construct a map
804 -- from the zonked tyvar to the in-scope one
805 -- If any of the in-scope tyvars zonk to a type, then ignore them;
806 -- that'll be caught later when we back up to their type sig
807 tcGetEnv `thenNF_Tc` \ env ->
809 in_scope_tvs = tcEnvTyVars env
811 zonkTcTyVars in_scope_tvs `thenNF_Tc` \ in_scope_tys ->
813 in_scope_assoc = [ (zonked_tv, in_scope_tv)
814 | (z_ty, in_scope_tv) <- in_scope_tys `zip` in_scope_tvs,
815 Just zonked_tv <- [getTyVar_maybe z_ty]
817 in_scope_env = mkVarEnv in_scope_assoc
820 -- "check" checks each sig tyvar in turn
822 (env2, in_scope_env, [])
823 (tidy_tvs `zip` tidy_tys) `thenNF_Tc` \ (env3, _, msgs) ->
825 failWithTcM (env3, main_msg $$ nest 4 (vcat msgs))
827 (env1, tidy_tvs) = mapAccumL tidyTyVar emptyTidyEnv sig_tyvars
828 (env2, tidy_tys) = tidyOpenTypes env1 sig_tys
830 main_msg = ptext SLIT("Inferred type is less polymorphic than expected")
832 check (tidy_env, acc, msgs) (sig_tyvar,ty)
833 -- sig_tyvar is from the signature;
834 -- ty is what you get if you zonk sig_tyvar and then tidy it
836 -- acc maps a zonked type variable back to a signature type variable
837 = case getTyVar_maybe ty of {
838 Nothing -> -- Error (a)!
839 returnNF_Tc (tidy_env, acc, unify_msg sig_tyvar (quotes (ppr ty)) : msgs) ;
843 case lookupVarEnv acc tv of {
844 Just sig_tyvar' -> -- Error (b) or (d)!
845 returnNF_Tc (tidy_env, acc, unify_msg sig_tyvar thing : msgs)
847 thing = ptext SLIT("another quantified type variable") <+> quotes (ppr sig_tyvar')
851 if tv `elemVarSet` globals -- Error (c)! Type variable escapes
852 -- The least comprehensible, so put it last
854 -- a) get the local TcIds from the environment,
855 -- and pass them to find_globals (they might have tv free)
856 -- b) similarly, find any free_tyvars that mention tv
857 then tcGetEnv `thenNF_Tc` \ ve ->
858 find_globals tv tidy_env [] (tcEnvTcIds ve) `thenNF_Tc` \ (tidy_env1, globs) ->
859 find_frees tv tidy_env1 [] (varSetElems free_tyvars) `thenNF_Tc` \ (tidy_env2, frees) ->
860 returnNF_Tc (tidy_env2, acc, escape_msg sig_tyvar tv globs frees : msgs)
863 returnNF_Tc (tidy_env, extendVarEnv acc tv sig_tyvar, msgs)
866 -- find_globals looks at the value environment and finds values
867 -- whose types mention the offending type variable. It has to be
868 -- careful to zonk the Id's type first, so it has to be in the monad.
869 -- We must be careful to pass it a zonked type variable, too.
875 -> NF_TcM (TidyEnv,[(Name,Type)])
877 find_globals tv tidy_env acc []
878 = returnNF_Tc (tidy_env, acc)
880 find_globals tv tidy_env acc (id:ids)
881 | isEmptyVarSet (idFreeTyVars id)
882 = find_globals tv tidy_env acc ids
885 = zonkTcType (idType id) `thenNF_Tc` \ id_ty ->
886 if tv `elemVarSet` tyVarsOfType id_ty then
888 (tidy_env', id_ty') = tidyOpenType tidy_env id_ty
889 acc' = (idName id, id_ty') : acc
891 find_globals tv tidy_env' acc' ids
893 find_globals tv tidy_env acc ids
895 find_frees tv tidy_env acc []
896 = returnNF_Tc (tidy_env, acc)
897 find_frees tv tidy_env acc (ftv:ftvs)
898 = zonkTcTyVar ftv `thenNF_Tc` \ ty ->
899 if tv `elemVarSet` tyVarsOfType ty then
901 (tidy_env', ftv') = tidyTyVar tidy_env ftv
903 find_frees tv tidy_env' (ftv':acc) ftvs
905 find_frees tv tidy_env acc ftvs
908 escape_msg sig_tv tv globs frees
909 = mk_msg sig_tv <+> ptext SLIT("escapes") $$
910 if not (null globs) then
911 vcat [pp_it <+> ptext SLIT("is mentioned in the environment"),
912 ptext SLIT("The following variables in the environment mention") <+> quotes (ppr tv),
913 nest 2 (vcat_first 10 [ppr name <+> dcolon <+> ppr ty | (name,ty) <- globs])
915 else if not (null frees) then
916 vcat [ptext SLIT("It is reachable from the type variable(s)") <+> pprQuotedList frees,
917 nest 2 (ptext SLIT("which") <+> is_are <+> ptext SLIT("free in the signature"))
920 empty -- Sigh. It's really hard to give a good error message
921 -- all the time. One bad case is an existential pattern match
923 is_are | isSingleton frees = ptext SLIT("is")
924 | otherwise = ptext SLIT("are")
925 pp_it | sig_tv /= tv = ptext SLIT("It unifies with") <+> quotes (ppr tv) <> comma <+> ptext SLIT("which")
926 | otherwise = ptext SLIT("It")
928 vcat_first :: Int -> [SDoc] -> SDoc
929 vcat_first n [] = empty
930 vcat_first 0 (x:xs) = text "...others omitted..."
931 vcat_first n (x:xs) = x $$ vcat_first (n-1) xs
933 unify_msg tv thing = mk_msg tv <+> ptext SLIT("is unified with") <+> thing
934 mk_msg tv = ptext SLIT("Quantified type variable") <+> quotes (ppr tv)
937 These two context are used with checkSigTyVars
940 sigCtxt :: Message -> [TcTyVar] -> TcThetaType -> TcTauType
941 -> TidyEnv -> NF_TcM (TidyEnv, Message)
942 sigCtxt when sig_tyvars sig_theta sig_tau tidy_env
943 = zonkTcType sig_tau `thenNF_Tc` \ actual_tau ->
945 (env1, tidy_sig_tyvars) = tidyTyVars tidy_env sig_tyvars
946 (env2, tidy_sig_rho) = tidyOpenType env1 (mkRhoTy sig_theta sig_tau)
947 (env3, tidy_actual_tau) = tidyOpenType env2 actual_tau
948 msg = vcat [ptext SLIT("Signature type: ") <+> pprType (mkForAllTys tidy_sig_tyvars tidy_sig_rho),
949 ptext SLIT("Type to generalise:") <+> pprType tidy_actual_tau,
953 returnNF_Tc (env3, msg)
955 sigPatCtxt bound_tvs bound_ids tidy_env
957 sep [ptext SLIT("When checking a pattern that binds"),
958 nest 4 (vcat (zipWith ppr_id show_ids tidy_tys))])
960 show_ids = filter is_interesting bound_ids
961 is_interesting id = any (`elemVarSet` idFreeTyVars id) bound_tvs
963 (env1, tidy_tys) = tidyOpenTypes tidy_env (map idType show_ids)
964 ppr_id id ty = ppr id <+> dcolon <+> ppr ty
965 -- Don't zonk the types so we get the separate, un-unified versions
969 %************************************************************************
971 \subsection{Errors and contexts}
973 %************************************************************************
976 tcsigCtxt v = ptext SLIT("In a type signature for") <+> quotes (ppr v)
978 typeKindCtxt :: RenamedHsType -> Message
979 typeKindCtxt ty = sep [ptext SLIT("When checking that"),
980 nest 2 (quotes (ppr ty)),
981 ptext SLIT("is a type")]
983 appKindCtxt :: SDoc -> Message
984 appKindCtxt pp = ptext SLIT("When checking kinds in") <+> quotes pp
986 wrongThingErr expected thing name
987 = pp_thing thing <+> quotes (ppr name) <+> ptext SLIT("used as a") <+> text expected
989 pp_thing (AGlobal (ATyCon _)) = ptext SLIT("Type constructor")
990 pp_thing (AGlobal (AClass _)) = ptext SLIT("Class")
991 pp_thing (AGlobal (AnId _)) = ptext SLIT("Identifier")
992 pp_thing (ATyVar _) = ptext SLIT("Type variable")
993 pp_thing (ATcId _) = ptext SLIT("Local identifier")
994 pp_thing (AThing _) = ptext SLIT("Utterly bogus")
997 = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
998 nest 4 (ptext SLIT("for the type:") <+> ppr_ty),
999 nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
1000 ptext SLIT("must be reachable from the type after the =>"))]
1003 = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
1004 ptext SLIT("are already in scope"),
1005 nest 4 (ptext SLIT("At least one must be universally quantified here")),
1006 ptext SLIT("In the type") <+> quotes ppr_ty
1009 polyArgTyErr ty = ptext SLIT("Illegal polymorphic type as argument:") <+> ppr ty
1010 ubxArgTyErr ty = ptext SLIT("Illegal unboxed tuple type as argument:") <+> ppr ty