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 TcMType ( newKindVar, tcInstSigVars,
34 zonkKindEnv, zonkTcType, zonkTcTyVars, zonkTcTyVar,
35 unifyKind, unifyOpenTypeKind
37 import TcType ( Type, Kind, SourceType(..), ThetaType, SigmaType, TauType,
38 mkTyVarTy, mkTyVarTys, mkFunTy, mkSynTy,
39 tcSplitForAllTys, tcSplitRhoTy,
40 hoistForAllTys, allDistinctTyVars,
42 mkSigmaTy, mkPredTy, mkTyConApp,
44 liftedTypeKind, unliftedTypeKind, mkArrowKind,
45 mkArrowKinds, tcGetTyVar_maybe, tcGetTyVar, tcSplitFunTy_maybe,
46 tidyOpenType, tidyOpenTypes, tidyTyVar, tidyTyVars,
47 tyVarsOfType, tyVarsOfPred, mkForAllTys,
48 isUnboxedTupleType, tcIsForAllTy, isIPPred
50 import Inst ( Inst, InstOrigin(..), newMethodWithGivenTy, instToId )
51 import FunDeps ( grow )
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 (HsNumTy _) -- The unit type for generics
216 = returnTc liftedTypeKind
218 kcHsType ty@(HsOpTy ty1 op ty2)
219 = kcTyVar op `thenTc` \ op_kind ->
220 kcHsType ty1 `thenTc` \ ty1_kind ->
221 kcHsType ty2 `thenTc` \ ty2_kind ->
222 tcAddErrCtxt (appKindCtxt (ppr ty)) $
223 kcAppKind op_kind ty1_kind `thenTc` \ op_kind' ->
224 kcAppKind op_kind' ty2_kind
226 kcHsType (HsPredTy pred)
227 = kcHsPred pred `thenTc_`
228 returnTc liftedTypeKind
230 kcHsType ty@(HsAppTy ty1 ty2)
231 = kcHsType ty1 `thenTc` \ tc_kind ->
232 kcHsType ty2 `thenTc` \ arg_kind ->
233 tcAddErrCtxt (appKindCtxt (ppr ty)) $
234 kcAppKind tc_kind arg_kind
236 kcHsType (HsForAllTy (Just tv_names) context ty)
237 = kcHsTyVars tv_names `thenNF_Tc` \ kind_env ->
238 tcExtendKindEnv kind_env $
239 kcHsContext context `thenTc_`
240 kcHsType ty `thenTc_`
241 returnTc liftedTypeKind
243 ---------------------------
244 kcAppKind fun_kind arg_kind
245 = case tcSplitFunTy_maybe fun_kind of
246 Just (arg_kind', res_kind)
247 -> unifyKind arg_kind arg_kind' `thenTc_`
250 Nothing -> newKindVar `thenNF_Tc` \ res_kind ->
251 unifyKind fun_kind (mkArrowKind arg_kind res_kind) `thenTc_`
255 ---------------------------
256 kcHsContext ctxt = mapTc_ kcHsPred ctxt
258 kcHsPred :: RenamedHsPred -> TcM ()
259 kcHsPred pred@(HsIParam name ty)
260 = tcAddErrCtxt (appKindCtxt (ppr pred)) $
263 kcHsPred pred@(HsClassP cls tys)
264 = tcAddErrCtxt (appKindCtxt (ppr pred)) $
265 kcClass cls `thenTc` \ kind ->
266 mapTc kcHsType tys `thenTc` \ arg_kinds ->
267 unifyKind kind (mkArrowKinds arg_kinds liftedTypeKind)
269 ---------------------------
270 kcTyVar name -- Could be a tyvar or a tycon
271 = tcLookup name `thenTc` \ thing ->
273 AThing kind -> returnTc kind
274 ATyVar tv -> returnTc (tyVarKind tv)
275 AGlobal (ATyCon tc) -> returnTc (tyConKind tc)
276 other -> failWithTc (wrongThingErr "type" thing name)
278 kcClass cls -- Must be a class
279 = tcLookup cls `thenNF_Tc` \ thing ->
281 AThing kind -> returnTc kind
282 AGlobal (AClass cls) -> returnTc (tyConKind (classTyCon cls))
283 other -> failWithTc (wrongThingErr "class" thing cls)
286 %************************************************************************
288 \subsection{Checking types}
290 %************************************************************************
292 tcHsSigType and tcHsLiftedSigType
293 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
295 tcHsSigType and tcHsLiftedSigType are used for type signatures written by the programmer
297 * We hoist any inner for-alls to the top
299 * Notice that we kind-check first, because the type-check assumes
300 that the kinds are already checked.
302 * They are only called when there are no kind vars in the environment
303 so the kind returned is indeed a Kind not a TcKind
306 tcHsSigType, tcHsLiftedSigType :: RenamedHsType -> TcM Type
307 -- Do kind checking, and hoist for-alls to the top
308 tcHsSigType ty = kcTypeType ty `thenTc_` tcHsType ty
309 tcHsLiftedSigType ty = kcLiftedType ty `thenTc_` tcHsType ty
311 tcHsType :: RenamedHsType -> TcM Type
312 tcHsRecType :: RecFlag -> RenamedHsType -> TcM Type
313 -- Don't do kind checking, but do hoist for-alls to the top
314 -- These are used in type and class decls, where kinding is
316 tcHsType ty = tc_type NonRecursive ty `thenTc` \ ty' -> returnTc (hoistForAllTys ty')
317 tcHsRecType wimp_out ty = tc_type wimp_out ty `thenTc` \ ty' -> returnTc (hoistForAllTys ty')
319 -- In interface files the type is already kinded,
320 -- and we definitely don't want to hoist for-alls.
321 -- Otherwise we'll change
322 -- dmfail :: forall m:(*->*) Monad m => forall a:* => String -> m a
324 -- dmfail :: forall m:(*->*) a:* Monad m => String -> m a
325 -- which definitely isn't right!
326 tcIfaceType ty = tc_type NonRecursive ty
330 %************************************************************************
334 %************************************************************************
336 tc_type, the main work horse
337 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
343 tc_type is used to typecheck the types in the RHS of data
344 constructors. In the case of recursive data types, that means that
345 the type constructors themselves are (partly) black holes. e.g.
347 data T a = MkT a [T a]
349 While typechecking the [T a] on the RHS, T itself is not yet fully
350 defined. That in turn places restrictions on what you can check in
351 tcHsType; if you poke on too much you get a black hole. I keep
352 forgetting this, hence this warning!
354 The wimp_out argument tells when we are in a mutually-recursive
355 group of type declarations, so omit various checks else we
356 get a black hole. They'll be done again later, in TcTyClDecls.tcGroup.
358 --------------------------
359 *** END OF BIG WARNING ***
360 --------------------------
364 tc_type :: RecFlag -> RenamedHsType -> TcM Type
366 tc_type wimp_out ty@(HsTyVar name)
367 = tc_app wimp_out ty []
369 tc_type wimp_out (HsListTy ty)
370 = tc_arg_type wimp_out ty `thenTc` \ tau_ty ->
371 returnTc (mkListTy tau_ty)
373 tc_type wimp_out (HsTupleTy (HsTupCon _ boxity arity) tys)
374 = ASSERT( arity == length tys )
375 mapTc tc_tup_arg tys `thenTc` \ tau_tys ->
376 returnTc (mkTupleTy boxity arity tau_tys)
378 tc_tup_arg = case boxity of
379 Boxed -> tc_arg_type wimp_out
380 Unboxed -> tc_type wimp_out
381 -- Unboxed tuples can have polymorphic or unboxed args.
382 -- This happens in the workers for functions returning
383 -- product types with polymorphic components
385 tc_type wimp_out (HsFunTy ty1 ty2)
386 = tc_type wimp_out ty1 `thenTc` \ tau_ty1 ->
387 -- Function argument can be polymorphic, but
388 -- must not be an unboxed tuple
390 -- In a recursive loop we can't ask whether the thing is
391 -- unboxed -- might be a synonym inside a synonym inside a group
392 checkTc (isRec wimp_out || not (isUnboxedTupleType tau_ty1))
393 (ubxArgTyErr ty1) `thenTc_`
394 tc_type wimp_out ty2 `thenTc` \ tau_ty2 ->
395 returnTc (mkFunTy tau_ty1 tau_ty2)
397 tc_type wimp_out (HsNumTy n)
399 returnTc (mkTyConApp genUnitTyCon [])
401 tc_type wimp_out (HsOpTy ty1 op ty2) =
402 tc_arg_type wimp_out ty1 `thenTc` \ tau_ty1 ->
403 tc_arg_type wimp_out ty2 `thenTc` \ tau_ty2 ->
404 tc_fun_type op [tau_ty1,tau_ty2]
406 tc_type wimp_out (HsAppTy ty1 ty2)
407 = tc_app wimp_out ty1 [ty2]
409 tc_type wimp_out (HsPredTy pred)
410 = tc_pred wimp_out pred `thenTc` \ pred' ->
411 returnTc (mkPredTy pred')
413 tc_type wimp_out full_ty@(HsForAllTy (Just tv_names) ctxt ty)
415 kind_check = kcHsContext ctxt `thenTc_` kcHsType ty
417 tcHsTyVars tv_names kind_check $ \ tyvars ->
418 tcRecTheta wimp_out ctxt `thenTc` \ theta ->
420 -- Context behaves like a function type
421 -- This matters. Return-unboxed-tuple analysis can
422 -- give overloaded functions like
423 -- f :: forall a. Num a => (# a->a, a->a #)
424 -- And we want these to get through the type checker
426 tc_arg_type wimp_out ty
431 checkAmbiguity wimp_out is_source tyvars theta tau
433 is_source = case tv_names of
434 (UserTyVar _ : _) -> True
438 -- tc_arg_type checks that the argument of a
439 -- type appplication isn't a for-all type or an unboxed tuple type
440 -- For example, we want to reject things like:
442 -- instance Ord a => Ord (forall s. T s a)
444 -- g :: T s (forall b.b)
446 -- Other unboxed types are very occasionally allowed as type
447 -- arguments depending on the kind of the type constructor
449 tc_arg_type wimp_out arg_ty
451 = tc_type wimp_out arg_ty
454 = tc_type wimp_out arg_ty `thenTc` \ arg_ty' ->
455 checkTc (isRec wimp_out || not (tcIsForAllTy arg_ty')) (polyArgTyErr arg_ty) `thenTc_`
456 checkTc (isRec wimp_out || not (isUnboxedTupleType arg_ty')) (ubxArgTyErr arg_ty) `thenTc_`
459 tc_arg_types wimp_out arg_tys = mapTc (tc_arg_type wimp_out) arg_tys
462 Help functions for type applications
463 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
466 tc_app :: RecFlag -> RenamedHsType -> [RenamedHsType] -> TcM Type
467 tc_app wimp_out (HsAppTy ty1 ty2) tys
468 = tc_app wimp_out ty1 (ty2:tys)
470 tc_app wimp_out ty tys
471 = tcAddErrCtxt (appKindCtxt pp_app) $
472 tc_arg_types wimp_out tys `thenTc` \ arg_tys ->
474 HsTyVar fun -> tc_fun_type fun arg_tys
475 other -> tc_type wimp_out ty `thenTc` \ fun_ty ->
476 returnNF_Tc (mkAppTys fun_ty arg_tys)
478 pp_app = ppr ty <+> sep (map pprParendHsType tys)
480 -- (tc_fun_type ty arg_tys) returns (mkAppTys ty arg_tys)
481 -- But not quite; for synonyms it checks the correct arity, and builds a SynTy
482 -- hence the rather strange functionality.
484 tc_fun_type name arg_tys
485 = tcLookup name `thenTc` \ thing ->
487 ATyVar tv -> returnTc (mkAppTys (mkTyVarTy tv) arg_tys)
490 | isSynTyCon tc -> checkTc arity_ok err_msg `thenTc_`
491 returnTc (mkAppTys (mkSynTy tc (take arity arg_tys))
492 (drop arity arg_tys))
494 | otherwise -> returnTc (mkTyConApp tc arg_tys)
497 arity_ok = arity <= n_args
498 arity = tyConArity tc
499 -- It's OK to have an *over-applied* type synonym
500 -- data Tree a b = ...
501 -- type Foo a = Tree [a]
502 -- f :: Foo a b -> ...
503 err_msg = arityErr "Type synonym" name arity n_args
504 n_args = length arg_tys
506 other -> failWithTc (wrongThingErr "type constructor" thing name)
513 tcRecTheta :: RecFlag -> RenamedContext -> TcM ThetaType
514 -- Used when we are expecting a ClassContext (i.e. no implicit params)
515 tcRecTheta wimp_out context = mapTc (tc_pred wimp_out) context
517 tc_pred wimp_out assn@(HsClassP class_name tys)
518 = tcAddErrCtxt (appKindCtxt (ppr assn)) $
519 tc_arg_types wimp_out tys `thenTc` \ arg_tys ->
520 tcLookupGlobal class_name `thenTc` \ thing ->
522 AClass clas -> checkTc (arity == n_tys) err `thenTc_`
523 returnTc (ClassP clas arg_tys)
525 arity = classArity clas
527 err = arityErr "Class" class_name arity n_tys
529 other -> failWithTc (wrongThingErr "class" (AGlobal thing) class_name)
531 tc_pred wimp_out assn@(HsIParam name ty)
532 = tcAddErrCtxt (appKindCtxt (ppr assn)) $
533 tc_arg_type wimp_out ty `thenTc` \ arg_ty ->
534 returnTc (IParam name arg_ty)
541 is ambiguous if P contains generic variables
542 (i.e. one of the Vs) that are not mentioned in tau
544 However, we need to take account of functional dependencies
545 when we speak of 'mentioned in tau'. Example:
546 class C a b | a -> b where ...
548 forall x y. (C x y) => x
549 is not ambiguous because x is mentioned and x determines y
551 NOTE: In addition, GHC insists that at least one type variable
552 in each constraint is in V. So we disallow a type like
553 forall a. Eq b => b -> b
554 even in a scope where b is in scope.
555 This is the is_free test below.
557 Notes on the 'is_source_polytype' test above
558 Check ambiguity only for source-program types, not
559 for types coming from inteface files. The latter can
560 legitimately have ambiguous types. Example
561 class S a where s :: a -> (Int,Int)
562 instance S Char where s _ = (1,1)
563 f:: S a => [a] -> Int -> (Int,Int)
564 f (_::[a]) x = (a*x,b)
565 where (a,b) = s (undefined::a)
566 Here the worker for f gets the type
567 fw :: forall a. S a => Int -> (# Int, Int #)
569 If the list of tv_names is empty, we have a monotype,
570 and then we don't need to check for ambiguity either,
571 because the test can't fail (see is_ambig).
574 checkAmbiguity :: RecFlag -> Bool
575 -> [TyVar] -> ThetaType -> TauType
577 checkAmbiguity wimp_out is_source_polytype forall_tyvars theta tau
578 | isRec wimp_out = returnTc sigma_ty
579 | otherwise = mapTc_ check_pred theta `thenTc_`
582 sigma_ty = mkSigmaTy forall_tyvars theta tau
583 tau_vars = tyVarsOfType tau
584 extended_tau_vars = grow theta tau_vars
586 -- Hack alert. If there are no tyvars, (ppr sigma_ty) will print
587 -- something strange like {Eq k} -> k -> k, because there is no
588 -- ForAll at the top of the type. Since this is going to the user
589 -- we want it to look like a proper Haskell type even then; hence the hack
591 -- This shows up in the complaint about
593 -- op :: Eq a => a -> a
594 ppr_sigma | null forall_tyvars = pprTheta theta <+> ptext SLIT("=>") <+> ppr tau
595 | otherwise = ppr sigma_ty
597 is_ambig ct_var = (ct_var `elem` forall_tyvars) &&
598 not (ct_var `elemVarSet` extended_tau_vars)
599 is_free ct_var = not (ct_var `elem` forall_tyvars)
601 check_pred pred = checkTc (not any_ambig) (ambigErr pred ppr_sigma) `thenTc_`
602 checkTc (isIPPred pred || not all_free) (freeErr pred ppr_sigma)
604 ct_vars = varSetElems (tyVarsOfPred pred)
605 all_free = all is_free ct_vars
606 any_ambig = is_source_polytype && any is_ambig ct_vars
609 %************************************************************************
611 \subsection{Type variables, with knot tying!}
613 %************************************************************************
616 mkImmutTyVars :: [(Name,Kind)] -> [TyVar]
617 mkImmutTyVars pairs = [mkTyVar name kind | (name, kind) <- pairs]
619 mkTyClTyVars :: Kind -- Kind of the tycon or class
620 -> [HsTyVarBndr Name]
622 mkTyClTyVars kind tyvar_names
623 = mkImmutTyVars tyvars_w_kinds
625 (tyvars_w_kinds, _) = zipFunTys (hsTyVarNames tyvar_names) kind
629 %************************************************************************
631 \subsection{Signatures}
633 %************************************************************************
635 @tcSigs@ checks the signatures for validity, and returns a list of
636 {\em freshly-instantiated} signatures. That is, the types are already
637 split up, and have fresh type variables installed. All non-type-signature
638 "RenamedSigs" are ignored.
640 The @TcSigInfo@ contains @TcTypes@ because they are unified with
641 the variable's type, and after that checked to see whether they've
647 Name -- N, the Name in corresponding binding
649 TcId -- *Polymorphic* binder for this value...
656 TcId -- *Monomorphic* binder for this value
657 -- Does *not* have name = N
660 [Inst] -- Empty if theta is null, or
661 -- (method mono_id) otherwise
663 SrcLoc -- Of the signature
665 instance Outputable TcSigInfo where
666 ppr (TySigInfo nm id tyvars theta tau _ inst loc) =
667 ppr nm <+> ptext SLIT("::") <+> ppr tyvars <+> ppr theta <+> ptext SLIT("=>") <+> ppr tau
669 maybeSig :: [TcSigInfo] -> Name -> Maybe (TcSigInfo)
670 -- Search for a particular signature
671 maybeSig [] name = Nothing
672 maybeSig (sig@(TySigInfo sig_name _ _ _ _ _ _ _) : sigs) name
673 | name == sig_name = Just sig
674 | otherwise = maybeSig sigs name
679 tcTySig :: RenamedSig -> TcM TcSigInfo
681 tcTySig (Sig v ty src_loc)
682 = tcAddSrcLoc src_loc $
683 tcAddErrCtxt (tcsigCtxt v) $
684 tcHsSigType ty `thenTc` \ sigma_tc_ty ->
685 mkTcSig (mkLocalId v sigma_tc_ty) src_loc `thenNF_Tc` \ sig ->
688 mkTcSig :: TcId -> SrcLoc -> NF_TcM TcSigInfo
689 mkTcSig poly_id src_loc
690 = -- Instantiate this type
691 -- It's important to do this even though in the error-free case
692 -- we could just split the sigma_tc_ty (since the tyvars don't
693 -- unified with anything). But in the case of an error, when
694 -- the tyvars *do* get unified with something, we want to carry on
695 -- typechecking the rest of the program with the function bound
696 -- to a pristine type, namely sigma_tc_ty
698 (tyvars, rho) = tcSplitForAllTys (idType poly_id)
700 tcInstSigVars tyvars `thenNF_Tc` \ tyvars' ->
701 -- Make *signature* type variables
704 tyvar_tys' = mkTyVarTys tyvars'
705 rho' = substTy (mkTopTyVarSubst tyvars tyvar_tys') rho
706 -- mkTopTyVarSubst because the tyvars' are fresh
708 (theta', tau') = tcSplitRhoTy rho'
709 -- This splitRhoTy tries hard to make sure that tau' is a type synonym
710 -- wherever possible, which can improve interface files.
712 newMethodWithGivenTy SignatureOrigin
715 theta' tau' `thenNF_Tc` \ inst ->
716 -- We make a Method even if it's not overloaded; no harm
718 returnNF_Tc (TySigInfo name poly_id tyvars' theta' tau' (instToId inst) [inst] src_loc)
720 name = idName poly_id
725 %************************************************************************
727 \subsection{Checking signature type variables}
729 %************************************************************************
731 @checkSigTyVars@ is used after the type in a type signature has been unified with
732 the actual type found. It then checks that the type variables of the type signature
734 (a) Still all type variables
735 eg matching signature [a] against inferred type [(p,q)]
736 [then a will be unified to a non-type variable]
738 (b) Still all distinct
739 eg matching signature [(a,b)] against inferred type [(p,p)]
740 [then a and b will be unified together]
742 (c) Not mentioned in the environment
743 eg the signature for f in this:
749 Here, f is forced to be monorphic by the free occurence of x.
751 (d) Not (unified with another type variable that is) in scope.
752 eg f x :: (r->r) = (\y->y) :: forall a. a->r
753 when checking the expression type signature, we find that
754 even though there is nothing in scope whose type mentions r,
755 nevertheless the type signature for the expression isn't right.
757 Another example is in a class or instance declaration:
759 op :: forall b. a -> b
761 Here, b gets unified with a
763 Before doing this, the substitution is applied to the signature type variable.
765 We used to have the notion of a "DontBind" type variable, which would
766 only be bound to itself or nothing. Then points (a) and (b) were
767 self-checking. But it gave rise to bogus consequential error messages.
770 f = (*) -- Monomorphic
775 Here, we get a complaint when checking the type signature for g,
776 that g isn't polymorphic enough; but then we get another one when
777 dealing with the (Num x) context arising from f's definition;
778 we try to unify x with Int (to default it), but find that x has already
779 been unified with the DontBind variable "a" from g's signature.
780 This is really a problem with side-effecting unification; we'd like to
781 undo g's effects when its type signature fails, but unification is done
782 by side effect, so we can't (easily).
784 So we revert to ordinary type variables for signatures, and try to
785 give a helpful message in checkSigTyVars.
788 checkSigTyVars :: [TcTyVar] -- Universally-quantified type variables in the signature
789 -> TcTyVarSet -- Tyvars that are free in the type signature
790 -- Not necessarily zonked
791 -- These should *already* be in the free-in-env set,
792 -- and are used here only to improve the error message
793 -> TcM [TcTyVar] -- Zonked signature type variables
795 checkSigTyVars [] free = returnTc []
796 checkSigTyVars sig_tyvars free_tyvars
797 = zonkTcTyVars sig_tyvars `thenNF_Tc` \ sig_tys ->
798 tcGetGlobalTyVars `thenNF_Tc` \ globals ->
800 checkTcM (allDistinctTyVars sig_tys globals)
801 (complain sig_tys globals) `thenTc_`
803 returnTc (map (tcGetTyVar "checkSigTyVars") sig_tys)
806 complain sig_tys globals
807 = -- For the in-scope ones, zonk them and construct a map
808 -- from the zonked tyvar to the in-scope one
809 -- If any of the in-scope tyvars zonk to a type, then ignore them;
810 -- that'll be caught later when we back up to their type sig
811 tcGetEnv `thenNF_Tc` \ env ->
813 in_scope_tvs = tcEnvTyVars env
815 zonkTcTyVars in_scope_tvs `thenNF_Tc` \ in_scope_tys ->
817 in_scope_assoc = [ (zonked_tv, in_scope_tv)
818 | (z_ty, in_scope_tv) <- in_scope_tys `zip` in_scope_tvs,
819 Just zonked_tv <- [tcGetTyVar_maybe z_ty]
821 in_scope_env = mkVarEnv in_scope_assoc
824 -- "check" checks each sig tyvar in turn
826 (env2, in_scope_env, [])
827 (tidy_tvs `zip` tidy_tys) `thenNF_Tc` \ (env3, _, msgs) ->
829 failWithTcM (env3, main_msg $$ nest 4 (vcat msgs))
831 (env1, tidy_tvs) = mapAccumL tidyTyVar emptyTidyEnv sig_tyvars
832 (env2, tidy_tys) = tidyOpenTypes env1 sig_tys
834 main_msg = ptext SLIT("Inferred type is less polymorphic than expected")
836 check (tidy_env, acc, msgs) (sig_tyvar,ty)
837 -- sig_tyvar is from the signature;
838 -- ty is what you get if you zonk sig_tyvar and then tidy it
840 -- acc maps a zonked type variable back to a signature type variable
841 = case tcGetTyVar_maybe ty of {
842 Nothing -> -- Error (a)!
843 returnNF_Tc (tidy_env, acc, unify_msg sig_tyvar (quotes (ppr ty)) : msgs) ;
847 case lookupVarEnv acc tv of {
848 Just sig_tyvar' -> -- Error (b) or (d)!
849 returnNF_Tc (tidy_env, acc, unify_msg sig_tyvar thing : msgs)
851 thing = ptext SLIT("another quantified type variable") <+> quotes (ppr sig_tyvar')
855 if tv `elemVarSet` globals -- Error (c)! Type variable escapes
856 -- The least comprehensible, so put it last
858 -- a) get the local TcIds from the environment,
859 -- and pass them to find_globals (they might have tv free)
860 -- b) similarly, find any free_tyvars that mention tv
861 then tcGetEnv `thenNF_Tc` \ ve ->
862 find_globals tv tidy_env [] (tcEnvTcIds ve) `thenNF_Tc` \ (tidy_env1, globs) ->
863 find_frees tv tidy_env1 [] (varSetElems free_tyvars) `thenNF_Tc` \ (tidy_env2, frees) ->
864 returnNF_Tc (tidy_env2, acc, escape_msg sig_tyvar tv globs frees : msgs)
867 returnNF_Tc (tidy_env, extendVarEnv acc tv sig_tyvar, msgs)
870 -- find_globals looks at the value environment and finds values
871 -- whose types mention the offending type variable. It has to be
872 -- careful to zonk the Id's type first, so it has to be in the monad.
873 -- We must be careful to pass it a zonked type variable, too.
879 -> NF_TcM (TidyEnv,[(Name,Type)])
881 find_globals tv tidy_env acc []
882 = returnNF_Tc (tidy_env, acc)
884 find_globals tv tidy_env acc (id:ids)
885 | isEmptyVarSet (idFreeTyVars id)
886 = find_globals tv tidy_env acc ids
889 = zonkTcType (idType id) `thenNF_Tc` \ id_ty ->
890 if tv `elemVarSet` tyVarsOfType id_ty then
892 (tidy_env', id_ty') = tidyOpenType tidy_env id_ty
893 acc' = (idName id, id_ty') : acc
895 find_globals tv tidy_env' acc' ids
897 find_globals tv tidy_env acc ids
899 find_frees tv tidy_env acc []
900 = returnNF_Tc (tidy_env, acc)
901 find_frees tv tidy_env acc (ftv:ftvs)
902 = zonkTcTyVar ftv `thenNF_Tc` \ ty ->
903 if tv `elemVarSet` tyVarsOfType ty then
905 (tidy_env', ftv') = tidyTyVar tidy_env ftv
907 find_frees tv tidy_env' (ftv':acc) ftvs
909 find_frees tv tidy_env acc ftvs
912 escape_msg sig_tv tv globs frees
913 = mk_msg sig_tv <+> ptext SLIT("escapes") $$
914 if not (null globs) then
915 vcat [pp_it <+> ptext SLIT("is mentioned in the environment"),
916 ptext SLIT("The following variables in the environment mention") <+> quotes (ppr tv),
917 nest 2 (vcat_first 10 [ppr name <+> dcolon <+> ppr ty | (name,ty) <- globs])
919 else if not (null frees) then
920 vcat [ptext SLIT("It is reachable from the type variable(s)") <+> pprQuotedList frees,
921 nest 2 (ptext SLIT("which") <+> is_are <+> ptext SLIT("free in the signature"))
924 empty -- Sigh. It's really hard to give a good error message
925 -- all the time. One bad case is an existential pattern match
927 is_are | isSingleton frees = ptext SLIT("is")
928 | otherwise = ptext SLIT("are")
929 pp_it | sig_tv /= tv = ptext SLIT("It unifies with") <+> quotes (ppr tv) <> comma <+> ptext SLIT("which")
930 | otherwise = ptext SLIT("It")
932 vcat_first :: Int -> [SDoc] -> SDoc
933 vcat_first n [] = empty
934 vcat_first 0 (x:xs) = text "...others omitted..."
935 vcat_first n (x:xs) = x $$ vcat_first (n-1) xs
937 unify_msg tv thing = mk_msg tv <+> ptext SLIT("is unified with") <+> thing
938 mk_msg tv = ptext SLIT("Quantified type variable") <+> quotes (ppr tv)
941 These two context are used with checkSigTyVars
944 sigCtxt :: Message -> [TcTyVar] -> TcThetaType -> TcTauType
945 -> TidyEnv -> NF_TcM (TidyEnv, Message)
946 sigCtxt when sig_tyvars sig_theta sig_tau tidy_env
947 = zonkTcType sig_tau `thenNF_Tc` \ actual_tau ->
949 (env1, tidy_sig_tyvars) = tidyTyVars tidy_env sig_tyvars
950 (env2, tidy_sig_rho) = tidyOpenType env1 (mkRhoTy sig_theta sig_tau)
951 (env3, tidy_actual_tau) = tidyOpenType env2 actual_tau
952 msg = vcat [ptext SLIT("Signature type: ") <+> pprType (mkForAllTys tidy_sig_tyvars tidy_sig_rho),
953 ptext SLIT("Type to generalise:") <+> pprType tidy_actual_tau,
957 returnNF_Tc (env3, msg)
959 sigPatCtxt bound_tvs bound_ids tidy_env
961 sep [ptext SLIT("When checking a pattern that binds"),
962 nest 4 (vcat (zipWith ppr_id show_ids tidy_tys))])
964 show_ids = filter is_interesting bound_ids
965 is_interesting id = any (`elemVarSet` idFreeTyVars id) bound_tvs
967 (env1, tidy_tys) = tidyOpenTypes tidy_env (map idType show_ids)
968 ppr_id id ty = ppr id <+> dcolon <+> ppr ty
969 -- Don't zonk the types so we get the separate, un-unified versions
973 %************************************************************************
975 \subsection{Errors and contexts}
977 %************************************************************************
980 tcsigCtxt v = ptext SLIT("In a type signature for") <+> quotes (ppr v)
982 typeKindCtxt :: RenamedHsType -> Message
983 typeKindCtxt ty = sep [ptext SLIT("When checking that"),
984 nest 2 (quotes (ppr ty)),
985 ptext SLIT("is a type")]
987 appKindCtxt :: SDoc -> Message
988 appKindCtxt pp = ptext SLIT("When checking kinds in") <+> quotes pp
990 wrongThingErr expected thing name
991 = pp_thing thing <+> quotes (ppr name) <+> ptext SLIT("used as a") <+> text expected
993 pp_thing (AGlobal (ATyCon _)) = ptext SLIT("Type constructor")
994 pp_thing (AGlobal (AClass _)) = ptext SLIT("Class")
995 pp_thing (AGlobal (AnId _)) = ptext SLIT("Identifier")
996 pp_thing (ATyVar _) = ptext SLIT("Type variable")
997 pp_thing (ATcId _) = ptext SLIT("Local identifier")
998 pp_thing (AThing _) = ptext SLIT("Utterly bogus")
1000 ambigErr pred ppr_ty
1001 = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
1002 nest 4 (ptext SLIT("for the type:") <+> ppr_ty),
1003 nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
1004 ptext SLIT("must be reachable from the type after the =>"))]
1007 = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
1008 ptext SLIT("are already in scope"),
1009 nest 4 (ptext SLIT("At least one must be universally quantified here")),
1010 ptext SLIT("In the type") <+> quotes ppr_ty
1013 polyArgTyErr ty = ptext SLIT("Illegal polymorphic type as argument:") <+> ppr ty
1014 ubxArgTyErr ty = ptext SLIT("Illegal unboxed tuple type as argument:") <+> ppr ty