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, newOpenTypeKind, tcInstType, newMutTyVar,
36 zonkTcType, zonkTcKindToKind,
37 checkValidType, UserTypeCtxt(..), pprHsSigCtxt
39 import TcUnify ( unifyKind, unifyFunKind )
40 import TcType ( Type, PredType(..), ThetaType, TyVarDetails(..),
41 TcTyVar, TcKind, TcThetaType, TcTauType,
42 mkTyVarTy, mkTyVarTys, mkFunTy, isTypeKind,
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
213 -- Be sure to use checkExpectedKind, rather than simply unifying
214 -- with (Type bx), because it gives better error messages
216 = kcHsType ty `thenM` \ (ty', kind) ->
217 if isTypeKind kind then
220 newOpenTypeKind `thenM` \ type_kind ->
221 checkExpectedKind (ppr ty) kind type_kind `thenM_`
224 ---------------------------
225 kcCheckHsType :: HsType Name -> TcKind -> TcM (HsType Name)
226 -- Check that the type has the specified kind
227 kcCheckHsType ty exp_kind
228 = kcHsType ty `thenM` \ (ty', act_kind) ->
229 checkExpectedKind (ppr ty) act_kind exp_kind `thenM_`
233 Here comes the main function
236 kcHsType :: HsType Name -> TcM (HsType Name, TcKind)
237 -- kcHsType *returns* the kind of the type, rather than taking an expected
238 -- kind as argument as tcExpr does.
240 -- (a) the kind of (->) is
241 -- forall bx1 bx2. Type bx1 -> Type bx2 -> Type Boxed
242 -- so we'd need to generate huge numbers of bx variables.
243 -- (b) kinds are so simple that the error messages are fine
245 -- The translated type has explicitly-kinded type-variable binders
247 kcHsType (HsParTy ty)
248 = kcHsType ty `thenM` \ (ty', kind) ->
249 returnM (HsParTy ty', kind)
251 kcHsType (HsTyVar name)
252 = kcTyVar name `thenM` \ kind ->
253 returnM (HsTyVar name, kind)
255 kcHsType (HsListTy ty)
256 = kcLiftedType ty `thenM` \ ty' ->
257 returnM (HsListTy ty', liftedTypeKind)
259 kcHsType (HsPArrTy ty)
260 = kcLiftedType ty `thenM` \ ty' ->
261 returnM (HsPArrTy ty', liftedTypeKind)
264 = returnM (HsNumTy n, liftedTypeKind)
266 kcHsType (HsKindSig ty k)
267 = kcCheckHsType ty k `thenM` \ ty' ->
268 returnM (HsKindSig ty' k, k)
270 kcHsType (HsTupleTy Boxed tys)
271 = mappM kcLiftedType tys `thenM` \ tys' ->
272 returnM (HsTupleTy Boxed tys', liftedTypeKind)
274 kcHsType (HsTupleTy Unboxed tys)
275 = mappM kcTypeType tys `thenM` \ tys' ->
276 returnM (HsTupleTy Unboxed tys', unliftedTypeKind)
278 kcHsType (HsFunTy ty1 ty2)
279 = kcTypeType ty1 `thenM` \ ty1' ->
280 kcTypeType ty2 `thenM` \ ty2' ->
281 returnM (HsFunTy ty1' ty2', liftedTypeKind)
283 kcHsType ty@(HsOpTy ty1 op ty2)
284 = kcTyVar op `thenM` \ op_kind ->
285 kcApps op_kind (ppr op) [ty1,ty2] `thenM` \ ([ty1',ty2'], res_kind) ->
286 returnM (HsOpTy ty1' op ty2', res_kind)
288 kcHsType ty@(HsAppTy ty1 ty2)
289 = kcHsType fun_ty `thenM` \ (fun_ty', fun_kind) ->
290 kcApps fun_kind (ppr fun_ty) arg_tys `thenM` \ (arg_tys', res_kind) ->
291 returnM (foldl HsAppTy fun_ty' arg_tys', res_kind)
293 (fun_ty, arg_tys) = split ty1 [ty2]
294 split (HsAppTy f a) as = split f (a:as)
297 kcHsType (HsPredTy pred)
298 = kcHsPred pred `thenM` \ pred' ->
299 returnM (HsPredTy pred', liftedTypeKind)
301 kcHsType (HsForAllTy exp tv_names context ty)
302 = kcHsTyVars tv_names $ \ tv_names' ->
303 kcHsContext context `thenM` \ ctxt' ->
304 kcLiftedType ty `thenM` \ ty' ->
305 -- The body of a forall must be of kind *
306 -- In principle, I suppose, we could allow unlifted types,
307 -- but it seems simpler to stick to lifted types for now.
308 returnM (HsForAllTy exp tv_names' ctxt' ty', liftedTypeKind)
310 ---------------------------
311 kcApps :: TcKind -- Function kind
313 -> [HsType Name] -- Arg types
314 -> TcM ([HsType Name], TcKind) -- Kind-checked args
315 kcApps fun_kind ppr_fun args
316 = split_fk fun_kind (length args) `thenM` \ (arg_kinds, res_kind) ->
317 mappM kc_arg (args `zip` arg_kinds) `thenM` \ args' ->
318 returnM (args', res_kind)
320 split_fk fk 0 = returnM ([], fk)
321 split_fk fk n = unifyFunKind fk `thenM` \ mb_fk ->
323 Nothing -> failWithTc too_many_args
324 Just (ak,fk') -> split_fk fk' (n-1) `thenM` \ (aks, rk) ->
327 kc_arg (arg, arg_kind) = kcCheckHsType arg arg_kind
329 too_many_args = ptext SLIT("Kind error:") <+> quotes ppr_fun <+>
330 ptext SLIT("is applied to too many type arguments")
332 ---------------------------
333 kcHsContext :: HsContext Name -> TcM (HsContext Name)
334 kcHsContext ctxt = mappM kcHsPred ctxt
336 kcHsPred pred -- Checks that the result is of kind liftedType
337 = kc_pred pred `thenM` \ (pred', kind) ->
338 checkExpectedKind (ppr pred) kind liftedTypeKind `thenM_`
341 ---------------------------
342 kc_pred :: HsPred Name -> TcM (HsPred Name, TcKind)
343 -- Does *not* check for a saturated
344 -- application (reason: used from TcDeriv)
345 kc_pred pred@(HsIParam name ty)
346 = kcHsType ty `thenM` \ (ty', kind) ->
347 returnM (HsIParam name ty', kind)
349 kc_pred pred@(HsClassP cls tys)
350 = kcClass cls `thenM` \ kind ->
351 kcApps kind (ppr cls) tys `thenM` \ (tys', res_kind) ->
352 returnM (HsClassP cls tys', res_kind)
354 ---------------------------
355 kcTyVar :: Name -> TcM TcKind
356 kcTyVar name -- Could be a tyvar or a tycon
357 = tcLookup name `thenM` \ thing ->
359 ATyVar tv -> returnM (tyVarKind tv)
360 ARecTyCon kind -> returnM kind
361 AGlobal (ATyCon tc) -> returnM (tyConKind tc)
362 other -> failWithTc (wrongThingErr "type" thing name)
364 kcClass :: Name -> TcM TcKind
365 kcClass cls -- Must be a class
366 = tcLookup cls `thenM` \ thing ->
368 ARecClass kind -> returnM kind
369 AGlobal (AClass cls) -> returnM (tyConKind (classTyCon cls))
370 other -> failWithTc (wrongThingErr "class" thing cls)
377 ---------------------------
378 -- We would like to get a decent error message from
379 -- (a) Under-applied type constructors
380 -- f :: (Maybe, Maybe)
381 -- (b) Over-applied type constructors
382 -- f :: Int x -> Int x
386 checkExpectedKind :: SDoc -> TcKind -> TcKind -> TcM TcKind
387 -- A fancy wrapper for 'unifyKind', which tries to give
388 -- decent error messages.
389 -- Returns the same kind that it is passed, exp_kind
390 checkExpectedKind pp_ty act_kind exp_kind
391 | act_kind `eqKind` exp_kind -- Short cut for a very common case
394 = tryTc (unifyKind exp_kind act_kind) `thenM` \ (errs, mb_r) ->
396 Just _ -> returnM exp_kind ; -- Unification succeeded
399 -- So there's definitely an error
400 -- Now to find out what sort
401 zonkTcType exp_kind `thenM` \ exp_kind ->
402 zonkTcType act_kind `thenM` \ act_kind ->
404 let (exp_as, _) = Type.splitFunTys exp_kind
405 (act_as, _) = Type.splitFunTys act_kind
406 -- Use the Type versions for kinds
407 n_exp_as = length exp_as
408 n_act_as = length act_as
410 err | n_exp_as < n_act_as -- E.g. [Maybe]
411 = quotes pp_ty <+> ptext SLIT("is not applied to enough type arguments")
413 -- Now n_exp_as >= n_act_as. In the next two cases,
414 -- n_exp_as == 0, and hence so is n_act_as
415 | exp_kind `eqKind` liftedTypeKind && act_kind `eqKind` unliftedTypeKind
416 = ptext SLIT("Expecting a lifted type, but") <+> quotes pp_ty
417 <+> ptext SLIT("is unlifted")
419 | exp_kind `eqKind` unliftedTypeKind && act_kind `eqKind` liftedTypeKind
420 = ptext SLIT("Expecting an unlifted type, but") <+> quotes pp_ty
421 <+> ptext SLIT("is lifted")
423 | otherwise -- E.g. Monad [Int]
424 = sep [ ptext SLIT("Expecting kind") <+> quotes (pprKind exp_kind) <> comma,
425 ptext SLIT("but") <+> quotes pp_ty <+>
426 ptext SLIT("has kind") <+> quotes (pprKind act_kind)]
428 failWithTc (ptext SLIT("Kind error:") <+> err)
432 %************************************************************************
436 %************************************************************************
440 * Transforms from HsType to Type
443 It cannot fail, and does no validity checking
446 dsHsType :: HsType Name -- All HsTyVarBndrs are kind-annotated
449 dsHsType ty@(HsTyVar name)
452 dsHsType (HsParTy ty) -- Remove the parentheses markers
455 dsHsType (HsKindSig ty k)
456 = dsHsType ty -- Kind checking done already
458 dsHsType (HsListTy ty)
459 = dsHsType ty `thenM` \ tau_ty ->
460 returnM (mkListTy tau_ty)
462 dsHsType (HsPArrTy ty)
463 = dsHsType ty `thenM` \ tau_ty ->
464 returnM (mkPArrTy tau_ty)
466 dsHsType (HsTupleTy boxity tys)
467 = dsHsTypes tys `thenM` \ tau_tys ->
468 returnM (mkTupleTy boxity (length tys) tau_tys)
470 dsHsType (HsFunTy ty1 ty2)
471 = dsHsType ty1 `thenM` \ tau_ty1 ->
472 dsHsType ty2 `thenM` \ tau_ty2 ->
473 returnM (mkFunTy tau_ty1 tau_ty2)
475 dsHsType (HsOpTy ty1 op ty2)
476 = dsHsType ty1 `thenM` \ tau_ty1 ->
477 dsHsType ty2 `thenM` \ tau_ty2 ->
478 ds_var_app op [tau_ty1,tau_ty2]
482 tcLookupTyCon genUnitTyConName `thenM` \ tc ->
483 returnM (mkTyConApp tc [])
485 dsHsType ty@(HsAppTy ty1 ty2)
488 dsHsType (HsPredTy pred)
489 = dsHsPred pred `thenM` \ pred' ->
490 returnM (mkPredTy pred')
492 dsHsType full_ty@(HsForAllTy exp tv_names ctxt ty)
493 = tcTyVarBndrs tv_names $ \ tyvars ->
494 mappM dsHsPred ctxt `thenM` \ theta ->
495 dsHsType ty `thenM` \ tau ->
496 returnM (mkSigmaTy tyvars theta tau)
498 dsHsTypes arg_tys = mappM dsHsType arg_tys
501 Help functions for type applications
502 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
505 ds_app :: HsType Name -> [HsType Name] -> TcM Type
506 ds_app (HsAppTy ty1 ty2) tys
507 = ds_app ty1 (ty2:tys)
510 = dsHsTypes tys `thenM` \ arg_tys ->
512 HsTyVar fun -> ds_var_app fun arg_tys
513 other -> dsHsType ty `thenM` \ fun_ty ->
514 returnM (mkAppTys fun_ty arg_tys)
516 ds_var_app :: Name -> [Type] -> TcM Type
517 ds_var_app name arg_tys
518 = tcLookup name `thenM` \ thing ->
520 ATyVar tv -> returnM (mkAppTys (mkTyVarTy tv) arg_tys)
521 AGlobal (ATyCon tc) -> returnM (mkGenTyConApp tc arg_tys)
522 ARecTyCon _ -> tcLookupTyCon name `thenM` \ tc ->
523 returnM (mkGenTyConApp tc arg_tys)
524 other -> pprPanic "ds_app_type" (ppr name <+> ppr arg_tys)
531 dsHsPred :: HsPred Name -> TcM PredType
532 dsHsPred pred@(HsClassP class_name tys)
533 = dsHsTypes tys `thenM` \ arg_tys ->
534 tcLookupClass class_name `thenM` \ clas ->
535 returnM (ClassP clas arg_tys)
537 dsHsPred (HsIParam name ty)
538 = dsHsType ty `thenM` \ arg_ty ->
539 returnM (IParam name arg_ty)
543 %************************************************************************
545 Type-variable binders
547 %************************************************************************
551 kcHsTyVars :: [HsTyVarBndr Name]
552 -> ([HsTyVarBndr Name] -> TcM r) -- These binders are kind-annotated
553 -- They scope over the thing inside
555 kcHsTyVars tvs thing_inside
556 = mappM kcHsTyVar tvs `thenM` \ bndrs ->
557 tcExtendTyVarKindEnv bndrs $
560 kcHsTyVar :: HsTyVarBndr Name -> TcM (HsTyVarBndr Name)
561 -- Return a *kind-annotated* binder, and a tyvar with a mutable kind in it
562 kcHsTyVar (UserTyVar name) = newKindVar `thenM` \ kind ->
563 returnM (KindedTyVar name kind)
564 kcHsTyVar (KindedTyVar name kind) = returnM (KindedTyVar name kind)
567 tcTyVarBndrs :: [HsTyVarBndr Name] -- Kind-annotated binders, which need kind-zonking
568 -> ([TyVar] -> TcM r)
570 -- Used when type-checking types/classes/type-decls
571 -- Brings into scope immutable TyVars, not mutable ones that require later zonking
572 tcTyVarBndrs bndrs thing_inside
573 = mapM zonk bndrs `thenM` \ tyvars ->
574 tcExtendTyVarEnv tyvars (thing_inside tyvars)
576 zonk (KindedTyVar name kind) = zonkTcKindToKind kind `thenM` \ kind' ->
577 returnM (mkTyVar name kind')
578 zonk (UserTyVar name) = pprTrace "BAD: Un-kinded tyvar" (ppr name) $
579 returnM (mkTyVar name liftedTypeKind)
583 %************************************************************************
585 Scoped type variables
587 %************************************************************************
590 tcAddScopedTyVars is used for scoped type variables added by pattern
592 e.g. \ ((x::a), (y::a)) -> x+y
593 They never have explicit kinds (because this is source-code only)
594 They are mutable (because they can get bound to a more specific type).
596 Usually we kind-infer and expand type splices, and then
597 tupecheck/desugar the type. That doesn't work well for scoped type
598 variables, because they scope left-right in patterns. (e.g. in the
599 example above, the 'a' in (y::a) is bound by the 'a' in (x::a).
601 The current not-very-good plan is to
602 * find all the types in the patterns
603 * find their free tyvars
605 * bring the kinded type vars into scope
606 * BUT throw away the kind-checked type
607 (we'll kind-check it again when we type-check the pattern)
609 This is bad because throwing away the kind checked type throws away
610 its splices. But too bad for now. [July 03]
613 We no longer specify that these type variables must be univerally
614 quantified (lots of email on the subject). If you want to put that
616 a) Do a checkSigTyVars after thing_inside
617 b) More insidiously, don't pass in expected_ty, else
618 we unify with it too early and checkSigTyVars barfs
619 Instead you have to pass in a fresh ty var, and unify
620 it with expected_ty afterwards
623 tcAddScopedTyVars :: [RenamedHsType] -> TcM a -> TcM a
624 tcAddScopedTyVars [] thing_inside
625 = thing_inside -- Quick get-out for the empty case
627 tcAddScopedTyVars sig_tys thing_inside
628 = getInLocalScope `thenM` \ in_scope ->
630 sig_tvs = [ UserTyVar n | ty <- sig_tys,
631 n <- nameSetToList (extractHsTyVars ty),
633 -- The tyvars we want are the free type variables of
634 -- the type that are not already in scope
636 -- Behave like kcHsType on a ForAll type
637 -- i.e. make kinded tyvars with mutable kinds,
638 -- and kind-check the enclosed types
639 kcHsTyVars sig_tvs (\ kinded_tvs -> do
640 { mappM kcTypeType sig_tys
641 ; return kinded_tvs }) `thenM` \ kinded_tvs ->
643 -- Zonk the mutable kinds and bring the tyvars into scope
644 -- Rather like tcTyVarBndrs, except that it brings *mutable*
645 -- tyvars into scope, not immutable ones
647 -- Furthermore, the tyvars are PatSigTvs, which means that we get better
648 -- error messages when type variables escape:
649 -- Inferred type is less polymorphic than expected
650 -- Quantified type variable `t' escapes
651 -- It is mentioned in the environment:
652 -- t is bound by the pattern type signature at tcfail103.hs:6
653 mapM zonk kinded_tvs `thenM` \ tyvars ->
654 tcExtendTyVarEnv tyvars thing_inside
657 zonk (KindedTyVar name kind) = zonkTcKindToKind kind `thenM` \ kind' ->
658 newMutTyVar name kind' PatSigTv
659 zonk (UserTyVar name) = pprTrace "BAD: Un-kinded tyvar" (ppr name) $
660 returnM (mkTyVar name liftedTypeKind)
664 %************************************************************************
666 \subsection{Signatures}
668 %************************************************************************
670 @tcSigs@ checks the signatures for validity, and returns a list of
671 {\em freshly-instantiated} signatures. That is, the types are already
672 split up, and have fresh type variables installed. All non-type-signature
673 "RenamedSigs" are ignored.
675 The @TcSigInfo@ contains @TcTypes@ because they are unified with
676 the variable's type, and after that checked to see whether they've
682 TcId -- *Polymorphic* binder for this value...
689 TcId -- *Monomorphic* binder for this value
690 -- Does *not* have name = N
693 [Inst] -- Empty if theta is null, or
694 -- (method mono_id) otherwise
696 SrcLoc -- Of the signature
698 instance Outputable TcSigInfo where
699 ppr (TySigInfo id tyvars theta tau _ inst loc) =
700 ppr id <+> ptext SLIT("::") <+> ppr tyvars <+> ppr theta <+> ptext SLIT("=>") <+> ppr tau
702 tcSigPolyId :: TcSigInfo -> TcId
703 tcSigPolyId (TySigInfo id _ _ _ _ _ _) = id
705 tcSigMonoId :: TcSigInfo -> TcId
706 tcSigMonoId (TySigInfo _ _ _ _ id _ _) = id
708 maybeSig :: [TcSigInfo] -> Name -> Maybe (TcSigInfo)
709 -- Search for a particular signature
710 maybeSig [] name = Nothing
711 maybeSig (sig@(TySigInfo sig_id _ _ _ _ _ _) : sigs) name
712 | name == idName sig_id = Just sig
713 | otherwise = maybeSig sigs name
718 tcTySig :: RenamedSig -> TcM TcSigInfo
720 tcTySig (Sig v ty src_loc)
721 = addSrcLoc src_loc $
722 tcHsSigType (FunSigCtxt v) ty `thenM` \ sigma_tc_ty ->
723 mkTcSig (mkLocalId v sigma_tc_ty) `thenM` \ sig ->
726 mkTcSig :: TcId -> TcM TcSigInfo
728 = -- Instantiate this type
729 -- It's important to do this even though in the error-free case
730 -- we could just split the sigma_tc_ty (since the tyvars don't
731 -- unified with anything). But in the case of an error, when
732 -- the tyvars *do* get unified with something, we want to carry on
733 -- typechecking the rest of the program with the function bound
734 -- to a pristine type, namely sigma_tc_ty
735 tcInstType SigTv (idType poly_id) `thenM` \ (tyvars', theta', tau') ->
737 getInstLoc SignatureOrigin `thenM` \ inst_loc ->
738 newMethod inst_loc poly_id
740 theta' tau' `thenM` \ inst ->
741 -- We make a Method even if it's not overloaded; no harm
742 -- But do not extend the LIE! We're just making an Id.
744 getSrcLocM `thenM` \ src_loc ->
745 returnM (TySigInfo poly_id tyvars' theta' tau'
746 (instToId inst) [inst] src_loc)
750 %************************************************************************
752 \subsection{Errors and contexts}
754 %************************************************************************
758 hoistForAllTys :: Type -> Type
759 -- Used for user-written type signatures only
760 -- Move all the foralls and constraints to the top
761 -- e.g. T -> forall a. a ==> forall a. T -> a
762 -- T -> (?x::Int) -> Int ==> (?x::Int) -> T -> Int
764 -- Also: eliminate duplicate constraints. These can show up
765 -- when hoisting constraints, notably implicit parameters.
767 -- We want to 'look through' type synonyms when doing this
768 -- so it's better done on the Type than the HsType
772 no_shadow_ty = deShadowTy ty
773 -- Running over ty with an empty substitution gives it the
774 -- no-shadowing property. This is important. For example:
775 -- type Foo r = forall a. a -> r
776 -- foo :: Foo (Foo ())
777 -- Here the hoisting should give
778 -- foo :: forall a a1. a -> a1 -> ()
780 -- What about type vars that are lexically in scope in the envt?
781 -- We simply rely on them having a different unique to any
782 -- binder in 'ty'. Otherwise we'd have to slurp the in-scope-tyvars
783 -- out of the envt, which is boring and (I think) not necessary.
785 case hoist no_shadow_ty of
786 (tvs, theta, body) -> mkForAllTys tvs (mkFunTys (nubBy tcEqType theta) body)
787 -- The 'nubBy' eliminates duplicate constraints,
788 -- notably implicit parameters
791 | (tvs1, body_ty) <- tcSplitForAllTys ty,
793 = case hoist body_ty of
794 (tvs2,theta,tau) -> (tvs1 ++ tvs2, theta, tau)
796 | Just (arg, res) <- tcSplitFunTy_maybe ty
798 arg' = hoistForAllTys arg -- Don't forget to apply hoist recursively
799 in -- to the argument type
800 if (isPredTy arg') then
802 (tvs,theta,tau) -> (tvs, arg':theta, tau)
805 (tvs,theta,tau) -> (tvs, theta, mkFunTy arg' tau)
807 | otherwise = ([], [], ty)
811 %************************************************************************
813 \subsection{Errors and contexts}
815 %************************************************************************
818 wrongThingErr expected thing name
819 = pp_thing thing <+> quotes (ppr name) <+> ptext SLIT("used as a") <+> text expected
821 pp_thing (AGlobal (ATyCon _)) = ptext SLIT("Type constructor")
822 pp_thing (AGlobal (AClass _)) = ptext SLIT("Class")
823 pp_thing (AGlobal (AnId _)) = ptext SLIT("Identifier")
824 pp_thing (AGlobal (ADataCon _)) = ptext SLIT("Data constructor")
825 pp_thing (ATyVar _) = ptext SLIT("Type variable")
826 pp_thing (ATcId _ _ _) = ptext SLIT("Local identifier")
827 pp_thing (ARecTyCon _) = ptext SLIT("Rec tycon")
828 pp_thing (ARecClass _) = ptext SLIT("Rec class")