2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 \section[TcMonoType]{Typechecking user-specified @MonoTypes@}
12 kcHsTyVars, kcHsSigType, kcHsLiftedSigType,
13 kcCheckHsType, kcHsContext,
15 -- Typechecking kinded types
16 tcHsKindedContext, tcHsKindedType, tcTyVarBndrs, dsHsType,
20 TcSigInfo(..), tcTySig, mkTcSig, maybeSig, tcSigPolyId, tcSigMonoId
23 #include "HsVersions.h"
25 import HsSyn ( HsType(..), HsTyVarBndr(..), HsContext, Sig(..), HsPred(..) )
26 import RnHsSyn ( RenamedHsType, RenamedContext, RenamedSig, extractHsTyVars )
27 import TcHsSyn ( TcId )
30 import TcEnv ( tcExtendTyVarEnv, tcExtendTyVarKindEnv,
31 tcLookup, tcLookupClass, tcLookupTyCon,
32 TyThing(..), TcTyThing(..),
35 import TcMType ( newKindVar, tcInstType, newMutTyVar,
36 zonkTcType, zonkTcKindToKind,
37 checkValidType, UserTypeCtxt(..), pprHsSigCtxt
39 import TcUnify ( unifyKind, unifyFunKind, unifyTypeKind )
40 import TcType ( Type, PredType(..), ThetaType, TyVarDetails(..),
41 TcTyVar, TcKind, TcThetaType, TcTauType,
42 mkTyVarTy, mkTyVarTys, mkFunTy,
43 mkForAllTys, mkFunTys, tcEqType, isPredTy,
44 mkSigmaTy, mkPredTy, mkGenTyConApp, mkTyConApp, mkAppTys,
45 liftedTypeKind, unliftedTypeKind, eqKind,
46 tcSplitFunTy_maybe, tcSplitForAllTys, tcSplitSigmaTy
48 import PprType ( pprKind, pprThetaArrow )
49 import qualified Type ( splitFunTys )
50 import Inst ( Inst, InstOrigin(..), newMethod, instToId )
52 import Id ( mkLocalId, idName, idType )
53 import Var ( TyVar, mkTyVar, tyVarKind )
54 import ErrUtils ( Message )
55 import TyCon ( TyCon, tyConKind )
56 import Class ( classTyCon )
59 import PrelNames ( genUnitTyConName )
60 import Subst ( deShadowTy )
61 import TysWiredIn ( mkListTy, mkPArrTy, mkTupleTy )
62 import BasicTypes ( Boxity(..) )
63 import SrcLoc ( SrcLoc )
69 ----------------------------
71 ----------------------------
73 Generally speaking we now type-check types in three phases
75 1. kcHsType: kind check the HsType
76 *includes* performing any TH type splices;
77 so it returns a translated, and kind-annotated, type
79 2. dsHsType: convert from HsType to Type:
81 expand type synonyms [mkGenTyApps]
82 hoist the foralls [tcHsType]
84 3. checkValidType: check the validity of the resulting type
86 Often these steps are done one after the other (tcHsSigType).
87 But in mutually recursive groups of type and class decls we do
88 1 kind-check the whole group
89 2 build TyCons/Classes in a knot-tied way
90 3 check the validity of types in the now-unknotted TyCons/Classes
92 For example, when we find
93 (forall a m. m a -> m a)
94 we bind a,m to kind varibles and kind-check (m a -> m a). This makes
95 a get kind *, and m get kind *->*. Now we typecheck (m a -> m a) in
96 an environment that binds a and m suitably.
98 The kind checker passed to tcHsTyVars needs to look at enough to
99 establish the kind of the tyvar:
100 * For a group of type and class decls, it's just the group, not
101 the rest of the program
102 * For a tyvar bound in a pattern type signature, its the types
103 mentioned in the other type signatures in that bunch of patterns
104 * For a tyvar bound in a RULE, it's the type signatures on other
105 universally quantified variables in the rule
107 Note that this may occasionally give surprising results. For example:
109 data T a b = MkT (a b)
111 Here we deduce a::*->*, b::*
112 But equally valid would be a::(*->*)-> *, b::*->*
117 Some of the validity check could in principle be done by the kind checker,
120 - During desugaring, we normalise by expanding type synonyms. Only
121 after this step can we check things like type-synonym saturation
122 e.g. type T k = k Int
124 Then (T S) is ok, because T is saturated; (T S) expands to (S Int);
125 and then S is saturated. This is a GHC extension.
127 - Similarly, also a GHC extension, we look through synonyms before complaining
128 about the form of a class or instance declaration
130 - Ambiguity checks involve functional dependencies, and it's easier to wait
131 until knots have been resolved before poking into them
133 Also, in a mutually recursive group of types, we can't look at the TyCon until we've
134 finished building the loop. So to keep things simple, we postpone most validity
135 checking until step (3).
139 During step (1) we might fault in a TyCon defined in another module, and it might
140 (via a loop) refer back to a TyCon defined in this module. So when we tie a big
141 knot around type declarations with ARecThing, so that the fault-in code can get
142 the TyCon being defined.
145 %************************************************************************
147 \subsection{Checking types}
149 %************************************************************************
152 tcHsSigType :: UserTypeCtxt -> RenamedHsType -> TcM Type
153 -- Do kind checking, and hoist for-alls to the top
154 tcHsSigType ctxt hs_ty
155 = addErrCtxt (pprHsSigCtxt ctxt hs_ty) $
156 do { kinded_ty <- kcTypeType hs_ty
157 ; ty <- tcHsKindedType kinded_ty
158 ; checkValidType ctxt ty
161 -- tcHsPred is happy with a partial application, e.g. (ST s)
164 = do { (kinded_pred,_) <- kc_pred pred -- kc_pred rather than kcHsPred
165 -- to avoid the partial application check
166 ; dsHsPred kinded_pred }
169 These functions are used during knot-tying in
170 type and class declarations, when we have to
171 separate kind-checking, desugaring, and validity checking
174 kcHsSigType, kcHsLiftedSigType :: HsType Name -> TcM (HsType Name)
175 -- Used for type signatures
176 kcHsSigType ty = kcTypeType ty
177 kcHsLiftedSigType ty = kcLiftedType ty
179 tcHsKindedType :: RenamedHsType -> TcM Type
180 -- Don't do kind checking, nor validity checking,
181 -- but do hoist for-alls to the top
182 -- This is used in type and class decls, where kinding is
183 -- done in advance, and validity checking is done later
184 -- [Validity checking done later because of knot-tying issues.]
186 = do { ty <- dsHsType hs_ty
187 ; return (hoistForAllTys ty) }
189 tcHsKindedContext :: RenamedContext -> TcM ThetaType
190 -- Used when we are expecting a ClassContext (i.e. no implicit params)
191 -- Does not do validity checking, like tcHsKindedType
192 tcHsKindedContext hs_theta = mappM dsHsPred hs_theta
196 %************************************************************************
198 The main kind checker: kcHsType
200 %************************************************************************
202 First a couple of simple wrappers for kcHsType
205 ---------------------------
206 kcLiftedType :: HsType Name -> TcM (HsType Name)
207 -- The type ty must be a *lifted* *type*
208 kcLiftedType ty = kcCheckHsType ty liftedTypeKind
210 ---------------------------
211 kcTypeType :: HsType Name -> TcM (HsType Name)
212 -- The type ty must be a *type*, but it can be lifted or unlifted
214 = kcHsType ty `thenM` \ (ty', kind) ->
215 unifyTypeKind kind `thenM_`
218 ---------------------------
219 kcCheckHsType :: HsType Name -> TcKind -> TcM (HsType Name)
220 -- Check that the type has the specified kind
221 kcCheckHsType ty exp_kind
222 = kcHsType ty `thenM` \ (ty', act_kind) ->
223 checkExpectedKind (ppr ty) act_kind exp_kind `thenM_`
227 Here comes the main function
230 kcHsType :: HsType Name -> TcM (HsType Name, TcKind)
231 -- kcHsType *returns* the kind of the type, rather than taking an expected
232 -- kind as argument as tcExpr does.
234 -- (a) the kind of (->) is
235 -- forall bx1 bx2. Type bx1 -> Type bx2 -> Type Boxed
236 -- so we'd need to generate huge numbers of bx variables.
237 -- (b) kinds are so simple that the error messages are fine
239 -- The translated type has explicitly-kinded type-variable binders
241 kcHsType (HsParTy ty)
242 = kcHsType ty `thenM` \ (ty', kind) ->
243 returnM (HsParTy ty', kind)
245 kcHsType (HsTyVar name)
246 = kcTyVar name `thenM` \ kind ->
247 returnM (HsTyVar name, kind)
249 kcHsType (HsListTy ty)
250 = kcLiftedType ty `thenM` \ ty' ->
251 returnM (HsListTy ty', liftedTypeKind)
253 kcHsType (HsPArrTy ty)
254 = kcLiftedType ty `thenM` \ ty' ->
255 returnM (HsPArrTy ty', liftedTypeKind)
258 = returnM (HsNumTy n, liftedTypeKind)
260 kcHsType (HsKindSig ty k)
261 = kcCheckHsType ty k `thenM` \ ty' ->
262 returnM (HsKindSig ty' k, k)
264 kcHsType (HsTupleTy Boxed tys)
265 = mappM kcLiftedType tys `thenM` \ tys' ->
266 returnM (HsTupleTy Boxed tys', liftedTypeKind)
268 kcHsType (HsTupleTy Unboxed tys)
269 = mappM kcTypeType tys `thenM` \ tys' ->
270 returnM (HsTupleTy Unboxed tys', unliftedTypeKind)
272 kcHsType (HsFunTy ty1 ty2)
273 = kcTypeType ty1 `thenM` \ ty1' ->
274 kcTypeType ty2 `thenM` \ ty2' ->
275 returnM (HsFunTy ty1' ty2', liftedTypeKind)
277 kcHsType ty@(HsOpTy ty1 op ty2)
278 = kcTyVar op `thenM` \ op_kind ->
279 kcApps op_kind (ppr op) [ty1,ty2] `thenM` \ ([ty1',ty2'], res_kind) ->
280 returnM (HsOpTy ty1' op ty2', res_kind)
282 kcHsType ty@(HsAppTy ty1 ty2)
283 = kcHsType fun_ty `thenM` \ (fun_ty', fun_kind) ->
284 kcApps fun_kind (ppr fun_ty) arg_tys `thenM` \ (arg_tys', res_kind) ->
285 returnM (foldl HsAppTy fun_ty' arg_tys', res_kind)
287 (fun_ty, arg_tys) = split ty1 [ty2]
288 split (HsAppTy f a) as = split f (a:as)
291 kcHsType (HsPredTy pred)
292 = kcHsPred pred `thenM` \ pred' ->
293 returnM (HsPredTy pred', liftedTypeKind)
295 kcHsType (HsForAllTy (Just tv_names) context ty)
296 = kcHsTyVars tv_names $ \ tv_names' ->
297 kcHsContext context `thenM` \ ctxt' ->
298 kcLiftedType ty `thenM` \ ty' ->
299 -- The body of a forall must be of kind *
300 -- In principle, I suppose, we could allow unlifted types,
301 -- but it seems simpler to stick to lifted types for now.
302 returnM (HsForAllTy (Just tv_names') ctxt' ty', liftedTypeKind)
304 ---------------------------
305 kcApps :: TcKind -- Function kind
307 -> [HsType Name] -- Arg types
308 -> TcM ([HsType Name], TcKind) -- Kind-checked args
309 kcApps fun_kind ppr_fun args
310 = split_fk fun_kind (length args) `thenM` \ (arg_kinds, res_kind) ->
311 mappM kc_arg (args `zip` arg_kinds) `thenM` \ args' ->
312 returnM (args', res_kind)
314 split_fk fk 0 = returnM ([], fk)
315 split_fk fk n = unifyFunKind fk `thenM` \ mb_fk ->
317 Nothing -> failWithTc too_many_args
318 Just (ak,fk') -> split_fk fk' (n-1) `thenM` \ (aks, rk) ->
321 kc_arg (arg, arg_kind) = kcCheckHsType arg arg_kind
323 too_many_args = ptext SLIT("Kind error:") <+> quotes ppr_fun <+>
324 ptext SLIT("is applied to too many type arguments")
326 ---------------------------
327 kcHsContext :: HsContext Name -> TcM (HsContext Name)
328 kcHsContext ctxt = mappM kcHsPred ctxt
330 kcHsPred pred -- Checks that the result is of kind liftedType
331 = kc_pred pred `thenM` \ (pred', kind) ->
332 checkExpectedKind (ppr pred) kind liftedTypeKind `thenM_`
335 ---------------------------
336 kc_pred :: HsPred Name -> TcM (HsPred Name, TcKind)
337 -- Does *not* check for a saturated
338 -- application (reason: used from TcDeriv)
339 kc_pred pred@(HsIParam name ty)
340 = kcHsType ty `thenM` \ (ty', kind) ->
341 returnM (HsIParam name ty', kind)
343 kc_pred pred@(HsClassP cls tys)
344 = kcClass cls `thenM` \ kind ->
345 kcApps kind (ppr cls) tys `thenM` \ (tys', res_kind) ->
346 returnM (HsClassP cls tys', res_kind)
348 ---------------------------
349 kcTyVar :: Name -> TcM TcKind
350 kcTyVar name -- Could be a tyvar or a tycon
351 = tcLookup name `thenM` \ thing ->
353 ATyVar tv -> returnM (tyVarKind tv)
354 ARecTyCon kind -> returnM kind
355 AGlobal (ATyCon tc) -> returnM (tyConKind tc)
356 other -> failWithTc (wrongThingErr "type" thing name)
358 kcClass :: Name -> TcM TcKind
359 kcClass cls -- Must be a class
360 = tcLookup cls `thenM` \ thing ->
362 ARecClass kind -> returnM kind
363 AGlobal (AClass cls) -> returnM (tyConKind (classTyCon cls))
364 other -> failWithTc (wrongThingErr "class" thing cls)
371 ---------------------------
372 -- We would like to get a decent error message from
373 -- (a) Under-applied type constructors
374 -- f :: (Maybe, Maybe)
375 -- (b) Over-applied type constructors
376 -- f :: Int x -> Int x
380 checkExpectedKind :: SDoc -> TcKind -> TcKind -> TcM TcKind
381 -- A fancy wrapper for 'unifyKind', which tries to give
382 -- decent error messages.
383 -- Returns the same kind that it is passed, exp_kind
384 checkExpectedKind pp_ty act_kind exp_kind
385 | act_kind `eqKind` exp_kind -- Short cut for a very common case
388 = tryTc (unifyKind exp_kind act_kind) `thenM` \ (errs, mb_r) ->
390 Just _ -> returnM exp_kind ; -- Unification succeeded
393 -- So there's definitely an error
394 -- Now to find out what sort
395 zonkTcType exp_kind `thenM` \ exp_kind ->
396 zonkTcType act_kind `thenM` \ act_kind ->
398 let (exp_as, _) = Type.splitFunTys exp_kind
399 (act_as, _) = Type.splitFunTys act_kind
400 -- Use the Type versions for kinds
401 n_exp_as = length exp_as
402 n_act_as = length act_as
404 err | n_exp_as < n_act_as -- E.g. [Maybe]
405 = quotes pp_ty <+> ptext SLIT("is not applied to enough type arguments")
407 -- Now n_exp_as >= n_act_as. In the next two cases,
408 -- n_exp_as == 0, and hence so is n_act_as
409 | exp_kind `eqKind` liftedTypeKind && act_kind `eqKind` unliftedTypeKind
410 = ptext SLIT("Expecting a lifted type, but") <+> quotes pp_ty
411 <+> ptext SLIT("is unlifted")
413 | exp_kind `eqKind` unliftedTypeKind && act_kind `eqKind` liftedTypeKind
414 = ptext SLIT("Expecting an unlifted type, but") <+> quotes pp_ty
415 <+> ptext SLIT("is lifted")
417 | otherwise -- E.g. Monad [Int]
418 = sep [ ptext SLIT("Expecting kind") <+> quotes (pprKind exp_kind) <> comma,
419 ptext SLIT("but") <+> quotes pp_ty <+>
420 ptext SLIT("has kind") <+> quotes (pprKind act_kind)]
422 failWithTc (ptext SLIT("Kind error:") <+> err)
426 %************************************************************************
430 %************************************************************************
434 * Transforms from HsType to Type
437 It cannot fail, and does no validity checking
440 dsHsType :: HsType Name -- All HsTyVarBndrs are kind-annotated
443 dsHsType ty@(HsTyVar name)
446 dsHsType (HsParTy ty) -- Remove the parentheses markers
449 dsHsType (HsKindSig ty k)
450 = dsHsType ty -- Kind checking done already
452 dsHsType (HsListTy ty)
453 = dsHsType ty `thenM` \ tau_ty ->
454 returnM (mkListTy tau_ty)
456 dsHsType (HsPArrTy ty)
457 = dsHsType ty `thenM` \ tau_ty ->
458 returnM (mkPArrTy tau_ty)
460 dsHsType (HsTupleTy boxity tys)
461 = dsHsTypes tys `thenM` \ tau_tys ->
462 returnM (mkTupleTy boxity (length tys) tau_tys)
464 dsHsType (HsFunTy ty1 ty2)
465 = dsHsType ty1 `thenM` \ tau_ty1 ->
466 dsHsType ty2 `thenM` \ tau_ty2 ->
467 returnM (mkFunTy tau_ty1 tau_ty2)
469 dsHsType (HsOpTy ty1 op ty2)
470 = dsHsType ty1 `thenM` \ tau_ty1 ->
471 dsHsType ty2 `thenM` \ tau_ty2 ->
472 ds_var_app op [tau_ty1,tau_ty2]
476 tcLookupTyCon genUnitTyConName `thenM` \ tc ->
477 returnM (mkTyConApp tc [])
479 dsHsType ty@(HsAppTy ty1 ty2)
482 dsHsType (HsPredTy pred)
483 = dsHsPred pred `thenM` \ pred' ->
484 returnM (mkPredTy pred')
486 dsHsType full_ty@(HsForAllTy (Just tv_names) ctxt ty)
487 = tcTyVarBndrs tv_names $ \ tyvars ->
488 mappM dsHsPred ctxt `thenM` \ theta ->
489 dsHsType ty `thenM` \ tau ->
490 returnM (mkSigmaTy tyvars theta tau)
492 dsHsTypes arg_tys = mappM dsHsType arg_tys
495 Help functions for type applications
496 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
499 ds_app :: HsType Name -> [HsType Name] -> TcM Type
500 ds_app (HsAppTy ty1 ty2) tys
501 = ds_app ty1 (ty2:tys)
504 = dsHsTypes tys `thenM` \ arg_tys ->
506 HsTyVar fun -> ds_var_app fun arg_tys
507 other -> dsHsType ty `thenM` \ fun_ty ->
508 returnM (mkAppTys fun_ty arg_tys)
510 ds_var_app :: Name -> [Type] -> TcM Type
511 ds_var_app name arg_tys
512 = tcLookup name `thenM` \ thing ->
514 ATyVar tv -> returnM (mkAppTys (mkTyVarTy tv) arg_tys)
515 AGlobal (ATyCon tc) -> returnM (mkGenTyConApp tc arg_tys)
516 ARecTyCon _ -> tcLookupTyCon name `thenM` \ tc ->
517 returnM (mkGenTyConApp tc arg_tys)
518 other -> pprPanic "ds_app_type" (ppr name <+> ppr arg_tys)
525 dsHsPred :: HsPred Name -> TcM PredType
526 dsHsPred pred@(HsClassP class_name tys)
527 = dsHsTypes tys `thenM` \ arg_tys ->
528 tcLookupClass class_name `thenM` \ clas ->
529 returnM (ClassP clas arg_tys)
531 dsHsPred (HsIParam name ty)
532 = dsHsType ty `thenM` \ arg_ty ->
533 returnM (IParam name arg_ty)
537 %************************************************************************
539 Type-variable binders
541 %************************************************************************
545 kcHsTyVars :: [HsTyVarBndr Name]
546 -> ([HsTyVarBndr Name] -> TcM r) -- These binders are kind-annotated
547 -- They scope over the thing inside
549 kcHsTyVars tvs thing_inside
550 = mappM kcHsTyVar tvs `thenM` \ bndrs ->
551 tcExtendTyVarKindEnv bndrs $
554 kcHsTyVar :: HsTyVarBndr Name -> TcM (HsTyVarBndr Name)
555 -- Return a *kind-annotated* binder, and a tyvar with a mutable kind in it
556 kcHsTyVar (UserTyVar name) = newKindVar `thenM` \ kind ->
557 returnM (KindedTyVar name kind)
558 kcHsTyVar (KindedTyVar name kind) = returnM (KindedTyVar name kind)
561 tcTyVarBndrs :: [HsTyVarBndr Name] -- Kind-annotated binders, which need kind-zonking
562 -> ([TyVar] -> TcM r)
564 -- Used when type-checking types/classes/type-decls
565 -- Brings into scope immutable TyVars, not mutable ones that require later zonking
566 tcTyVarBndrs bndrs thing_inside
567 = mapM zonk bndrs `thenM` \ tyvars ->
568 tcExtendTyVarEnv tyvars (thing_inside tyvars)
570 zonk (KindedTyVar name kind) = zonkTcKindToKind kind `thenM` \ kind' ->
571 returnM (mkTyVar name kind')
572 zonk (UserTyVar name) = pprTrace "BAD: Un-kinded tyvar" (ppr name) $
573 returnM (mkTyVar name liftedTypeKind)
577 %************************************************************************
579 Scoped type variables
581 %************************************************************************
584 tcAddScopedTyVars is used for scoped type variables added by pattern
586 e.g. \ ((x::a), (y::a)) -> x+y
587 They never have explicit kinds (because this is source-code only)
588 They are mutable (because they can get bound to a more specific type).
590 Usually we kind-infer and expand type splices, and then
591 tupecheck/desugar the type. That doesn't work well for scoped type
592 variables, because they scope left-right in patterns. (e.g. in the
593 example above, the 'a' in (y::a) is bound by the 'a' in (x::a).
595 The current not-very-good plan is to
596 * find all the types in the patterns
597 * find their free tyvars
599 * bring the kinded type vars into scope
600 * BUT throw away the kind-checked type
601 (we'll kind-check it again when we type-check the pattern)
603 This is bad because throwing away the kind checked type throws away
604 its splices. But too bad for now. [July 03]
607 We no longer specify that these type variables must be univerally
608 quantified (lots of email on the subject). If you want to put that
610 a) Do a checkSigTyVars after thing_inside
611 b) More insidiously, don't pass in expected_ty, else
612 we unify with it too early and checkSigTyVars barfs
613 Instead you have to pass in a fresh ty var, and unify
614 it with expected_ty afterwards
617 tcAddScopedTyVars :: [RenamedHsType] -> TcM a -> TcM a
618 tcAddScopedTyVars [] thing_inside
619 = thing_inside -- Quick get-out for the empty case
621 tcAddScopedTyVars sig_tys thing_inside
622 = getInLocalScope `thenM` \ in_scope ->
624 sig_tvs = [ UserTyVar n | ty <- sig_tys,
625 n <- nameSetToList (extractHsTyVars ty),
627 -- The tyvars we want are the free type variables of
628 -- the type that are not already in scope
630 -- Behave like kcHsType on a ForAll type
631 -- i.e. make kinded tyvars with mutable kinds,
632 -- and kind-check the enclosed types
633 kcHsTyVars sig_tvs (\ kinded_tvs -> do
634 { mappM kcTypeType sig_tys
635 ; return kinded_tvs }) `thenM` \ kinded_tvs ->
637 -- Zonk the mutable kinds and bring the tyvars into scope
638 -- Rather like tcTyVarBndrs, except that it brings *mutable*
639 -- tyvars into scope, not immutable ones
641 -- Furthermore, the tyvars are PatSigTvs, which means that we get better
642 -- error messages when type variables escape:
643 -- Inferred type is less polymorphic than expected
644 -- Quantified type variable `t' escapes
645 -- It is mentioned in the environment:
646 -- t is bound by the pattern type signature at tcfail103.hs:6
647 mapM zonk kinded_tvs `thenM` \ tyvars ->
648 tcExtendTyVarEnv tyvars thing_inside
651 zonk (KindedTyVar name kind) = zonkTcKindToKind kind `thenM` \ kind' ->
652 newMutTyVar name kind' PatSigTv
653 zonk (UserTyVar name) = pprTrace "BAD: Un-kinded tyvar" (ppr name) $
654 returnM (mkTyVar name liftedTypeKind)
658 %************************************************************************
660 \subsection{Signatures}
662 %************************************************************************
664 @tcSigs@ checks the signatures for validity, and returns a list of
665 {\em freshly-instantiated} signatures. That is, the types are already
666 split up, and have fresh type variables installed. All non-type-signature
667 "RenamedSigs" are ignored.
669 The @TcSigInfo@ contains @TcTypes@ because they are unified with
670 the variable's type, and after that checked to see whether they've
676 TcId -- *Polymorphic* binder for this value...
683 TcId -- *Monomorphic* binder for this value
684 -- Does *not* have name = N
687 [Inst] -- Empty if theta is null, or
688 -- (method mono_id) otherwise
690 SrcLoc -- Of the signature
692 instance Outputable TcSigInfo where
693 ppr (TySigInfo id tyvars theta tau _ inst loc) =
694 ppr id <+> ptext SLIT("::") <+> ppr tyvars <+> ppr theta <+> ptext SLIT("=>") <+> ppr tau
696 tcSigPolyId :: TcSigInfo -> TcId
697 tcSigPolyId (TySigInfo id _ _ _ _ _ _) = id
699 tcSigMonoId :: TcSigInfo -> TcId
700 tcSigMonoId (TySigInfo _ _ _ _ id _ _) = id
702 maybeSig :: [TcSigInfo] -> Name -> Maybe (TcSigInfo)
703 -- Search for a particular signature
704 maybeSig [] name = Nothing
705 maybeSig (sig@(TySigInfo sig_id _ _ _ _ _ _) : sigs) name
706 | name == idName sig_id = Just sig
707 | otherwise = maybeSig sigs name
712 tcTySig :: RenamedSig -> TcM TcSigInfo
714 tcTySig (Sig v ty src_loc)
715 = addSrcLoc src_loc $
716 tcHsSigType (FunSigCtxt v) ty `thenM` \ sigma_tc_ty ->
717 mkTcSig (mkLocalId v sigma_tc_ty) `thenM` \ sig ->
720 mkTcSig :: TcId -> TcM TcSigInfo
722 = -- Instantiate this type
723 -- It's important to do this even though in the error-free case
724 -- we could just split the sigma_tc_ty (since the tyvars don't
725 -- unified with anything). But in the case of an error, when
726 -- the tyvars *do* get unified with something, we want to carry on
727 -- typechecking the rest of the program with the function bound
728 -- to a pristine type, namely sigma_tc_ty
729 tcInstType SigTv (idType poly_id) `thenM` \ (tyvars', theta', tau') ->
731 getInstLoc SignatureOrigin `thenM` \ inst_loc ->
732 newMethod inst_loc poly_id
734 theta' tau' `thenM` \ inst ->
735 -- We make a Method even if it's not overloaded; no harm
736 -- But do not extend the LIE! We're just making an Id.
738 getSrcLocM `thenM` \ src_loc ->
739 returnM (TySigInfo poly_id tyvars' theta' tau'
740 (instToId inst) [inst] src_loc)
744 %************************************************************************
746 \subsection{Errors and contexts}
748 %************************************************************************
752 hoistForAllTys :: Type -> Type
753 -- Used for user-written type signatures only
754 -- Move all the foralls and constraints to the top
755 -- e.g. T -> forall a. a ==> forall a. T -> a
756 -- T -> (?x::Int) -> Int ==> (?x::Int) -> T -> Int
758 -- Also: eliminate duplicate constraints. These can show up
759 -- when hoisting constraints, notably implicit parameters.
761 -- We want to 'look through' type synonyms when doing this
762 -- so it's better done on the Type than the HsType
766 no_shadow_ty = deShadowTy ty
767 -- Running over ty with an empty substitution gives it the
768 -- no-shadowing property. This is important. For example:
769 -- type Foo r = forall a. a -> r
770 -- foo :: Foo (Foo ())
771 -- Here the hoisting should give
772 -- foo :: forall a a1. a -> a1 -> ()
774 -- What about type vars that are lexically in scope in the envt?
775 -- We simply rely on them having a different unique to any
776 -- binder in 'ty'. Otherwise we'd have to slurp the in-scope-tyvars
777 -- out of the envt, which is boring and (I think) not necessary.
779 case hoist no_shadow_ty of
780 (tvs, theta, body) -> mkForAllTys tvs (mkFunTys (nubBy tcEqType theta) body)
781 -- The 'nubBy' eliminates duplicate constraints,
782 -- notably implicit parameters
785 | (tvs1, body_ty) <- tcSplitForAllTys ty,
787 = case hoist body_ty of
788 (tvs2,theta,tau) -> (tvs1 ++ tvs2, theta, tau)
790 | Just (arg, res) <- tcSplitFunTy_maybe ty
792 arg' = hoistForAllTys arg -- Don't forget to apply hoist recursively
793 in -- to the argument type
794 if (isPredTy arg') then
796 (tvs,theta,tau) -> (tvs, arg':theta, tau)
799 (tvs,theta,tau) -> (tvs, theta, mkFunTy arg' tau)
801 | otherwise = ([], [], ty)
805 %************************************************************************
807 \subsection{Errors and contexts}
809 %************************************************************************
812 wrongThingErr expected thing name
813 = pp_thing thing <+> quotes (ppr name) <+> ptext SLIT("used as a") <+> text expected
815 pp_thing (AGlobal (ATyCon _)) = ptext SLIT("Type constructor")
816 pp_thing (AGlobal (AClass _)) = ptext SLIT("Class")
817 pp_thing (AGlobal (AnId _)) = ptext SLIT("Identifier")
818 pp_thing (AGlobal (ADataCon _)) = ptext SLIT("Data constructor")
819 pp_thing (ATyVar _) = ptext SLIT("Type variable")
820 pp_thing (ATcId _ _ _) = ptext SLIT("Local identifier")
821 pp_thing (ARecTyCon _) = ptext SLIT("Rec tycon")
822 pp_thing (ARecClass _) = ptext SLIT("Rec class")