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
23 #include "HsVersions.h"
25 import HsSyn ( HsType(..), LHsType, HsTyVarBndr(..), LHsTyVarBndr,
26 LHsContext, Sig(..), LSig, HsPred(..), LHsPred )
27 import RnHsSyn ( extractHsTyVars )
28 import TcHsSyn ( TcId )
31 import TcEnv ( tcExtendTyVarEnv, tcExtendTyVarKindEnv,
32 tcLookup, tcLookupClass, tcLookupTyCon,
33 TyThing(..), TcTyThing(..),
36 import TcMType ( newKindVar, newOpenTypeKind, tcInstType, newMutTyVar,
37 zonkTcType, zonkTcKindToKind,
38 checkValidType, UserTypeCtxt(..), pprHsSigCtxt
40 import TcUnify ( unifyKind, unifyFunKind )
41 import TcType ( Type, PredType(..), ThetaType, TyVarDetails(..),
42 TcTyVar, TcKind, TcThetaType, TcTauType,
43 mkTyVarTy, mkTyVarTys, mkFunTy, isTypeKind,
44 mkForAllTys, mkFunTys, tcEqType, isPredTy,
45 mkSigmaTy, mkPredTy, mkGenTyConApp, mkTyConApp, mkAppTys,
46 liftedTypeKind, unliftedTypeKind, eqKind,
47 tcSplitFunTy_maybe, tcSplitForAllTys, pprKind )
48 import qualified Type ( splitFunTys )
49 import Inst ( Inst, InstOrigin(..), newMethod, instToId )
51 import Id ( mkLocalId, idName, idType )
52 import Var ( TyVar, mkTyVar, tyVarKind )
53 import TyCon ( TyCon, tyConKind )
54 import Class ( classTyCon )
57 import PrelNames ( genUnitTyConName )
58 import Subst ( deShadowTy )
59 import TysWiredIn ( mkListTy, mkPArrTy, mkTupleTy )
60 import BasicTypes ( Boxity(..) )
61 import SrcLoc ( SrcSpan, Located(..), unLoc, noLoc )
67 ----------------------------
69 ----------------------------
71 Generally speaking we now type-check types in three phases
73 1. kcHsType: kind check the HsType
74 *includes* performing any TH type splices;
75 so it returns a translated, and kind-annotated, type
77 2. dsHsType: convert from HsType to Type:
79 expand type synonyms [mkGenTyApps]
80 hoist the foralls [tcHsType]
82 3. checkValidType: check the validity of the resulting type
84 Often these steps are done one after the other (tcHsSigType).
85 But in mutually recursive groups of type and class decls we do
86 1 kind-check the whole group
87 2 build TyCons/Classes in a knot-tied way
88 3 check the validity of types in the now-unknotted TyCons/Classes
90 For example, when we find
91 (forall a m. m a -> m a)
92 we bind a,m to kind varibles and kind-check (m a -> m a). This makes
93 a get kind *, and m get kind *->*. Now we typecheck (m a -> m a) in
94 an environment that binds a and m suitably.
96 The kind checker passed to tcHsTyVars needs to look at enough to
97 establish the kind of the tyvar:
98 * For a group of type and class decls, it's just the group, not
99 the rest of the program
100 * For a tyvar bound in a pattern type signature, its the types
101 mentioned in the other type signatures in that bunch of patterns
102 * For a tyvar bound in a RULE, it's the type signatures on other
103 universally quantified variables in the rule
105 Note that this may occasionally give surprising results. For example:
107 data T a b = MkT (a b)
109 Here we deduce a::*->*, b::*
110 But equally valid would be a::(*->*)-> *, b::*->*
115 Some of the validity check could in principle be done by the kind checker,
118 - During desugaring, we normalise by expanding type synonyms. Only
119 after this step can we check things like type-synonym saturation
120 e.g. type T k = k Int
122 Then (T S) is ok, because T is saturated; (T S) expands to (S Int);
123 and then S is saturated. This is a GHC extension.
125 - Similarly, also a GHC extension, we look through synonyms before complaining
126 about the form of a class or instance declaration
128 - Ambiguity checks involve functional dependencies, and it's easier to wait
129 until knots have been resolved before poking into them
131 Also, in a mutually recursive group of types, we can't look at the TyCon until we've
132 finished building the loop. So to keep things simple, we postpone most validity
133 checking until step (3).
137 During step (1) we might fault in a TyCon defined in another module, and it might
138 (via a loop) refer back to a TyCon defined in this module. So when we tie a big
139 knot around type declarations with ARecThing, so that the fault-in code can get
140 the TyCon being defined.
143 %************************************************************************
145 \subsection{Checking types}
147 %************************************************************************
150 tcHsSigType :: UserTypeCtxt -> LHsType Name -> TcM Type
151 -- Do kind checking, and hoist for-alls to the top
152 tcHsSigType ctxt hs_ty
153 = addErrCtxt (pprHsSigCtxt ctxt hs_ty) $
154 do { kinded_ty <- kcTypeType hs_ty
155 ; ty <- tcHsKindedType kinded_ty
156 ; checkValidType ctxt ty
159 -- tcHsPred is happy with a partial application, e.g. (ST s)
162 = do { (kinded_pred,_) <- wrapLocFstM kc_pred pred -- kc_pred rather than kcHsPred
163 -- to avoid the partial application check
164 ; dsHsPred kinded_pred }
167 These functions are used during knot-tying in
168 type and class declarations, when we have to
169 separate kind-checking, desugaring, and validity checking
172 kcHsSigType, kcHsLiftedSigType :: LHsType Name -> TcM (LHsType Name)
173 -- Used for type signatures
174 kcHsSigType ty = kcTypeType ty
175 kcHsLiftedSigType ty = kcLiftedType ty
177 tcHsKindedType :: LHsType Name -> TcM Type
178 -- Don't do kind checking, nor validity checking,
179 -- but do hoist for-alls to the top
180 -- This is used in type and class decls, where kinding is
181 -- done in advance, and validity checking is done later
182 -- [Validity checking done later because of knot-tying issues.]
184 = do { ty <- dsHsType hs_ty
185 ; return (hoistForAllTys ty) }
187 tcHsKindedContext :: LHsContext Name -> TcM ThetaType
188 -- Used when we are expecting a ClassContext (i.e. no implicit params)
189 -- Does not do validity checking, like tcHsKindedType
190 tcHsKindedContext hs_theta = addLocM (mappM dsHsPred) hs_theta
194 %************************************************************************
196 The main kind checker: kcHsType
198 %************************************************************************
200 First a couple of simple wrappers for kcHsType
203 ---------------------------
204 kcLiftedType :: LHsType Name -> TcM (LHsType Name)
205 -- The type ty must be a *lifted* *type*
206 kcLiftedType ty = kcCheckHsType ty liftedTypeKind
208 ---------------------------
209 kcTypeType :: LHsType Name -> TcM (LHsType Name)
210 -- The type ty must be a *type*, but it can be lifted or unlifted
211 -- Be sure to use checkExpectedKind, rather than simply unifying
212 -- with (Type bx), because it gives better error messages
214 = kcHsType ty `thenM` \ (ty', kind) ->
215 if isTypeKind kind then
218 newOpenTypeKind `thenM` \ type_kind ->
219 traceTc (text "kcTypeType" $$ nest 2 (ppr ty $$ ppr ty' $$ ppr kind $$ ppr type_kind)) `thenM_`
220 checkExpectedKind ty kind type_kind `thenM_`
223 ---------------------------
224 kcCheckHsType :: LHsType Name -> TcKind -> TcM (LHsType Name)
225 -- Check that the type has the specified kind
226 kcCheckHsType ty exp_kind
227 = kcHsType ty `thenM` \ (ty', act_kind) ->
228 checkExpectedKind ty act_kind exp_kind `thenM_`
232 Here comes the main function
235 kcHsType :: LHsType Name -> TcM (LHsType Name, TcKind)
236 kcHsType ty = wrapLocFstM kc_hs_type ty
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 kc_hs_type (HsParTy ty)
248 = kcHsType ty `thenM` \ (ty', kind) ->
249 returnM (HsParTy ty', kind)
251 kc_hs_type (HsTyVar name)
252 = kcTyVar name `thenM` \ kind ->
253 returnM (HsTyVar name, kind)
255 kc_hs_type (HsListTy ty)
256 = kcLiftedType ty `thenM` \ ty' ->
257 returnM (HsListTy ty', liftedTypeKind)
259 kc_hs_type (HsPArrTy ty)
260 = kcLiftedType ty `thenM` \ ty' ->
261 returnM (HsPArrTy ty', liftedTypeKind)
263 kc_hs_type (HsNumTy n)
264 = returnM (HsNumTy n, liftedTypeKind)
266 kc_hs_type (HsKindSig ty k)
267 = kcCheckHsType ty k `thenM` \ ty' ->
268 returnM (HsKindSig ty' k, k)
270 kc_hs_type (HsTupleTy Boxed tys)
271 = mappM kcLiftedType tys `thenM` \ tys' ->
272 returnM (HsTupleTy Boxed tys', liftedTypeKind)
274 kc_hs_type (HsTupleTy Unboxed tys)
275 = mappM kcTypeType tys `thenM` \ tys' ->
276 returnM (HsTupleTy Unboxed tys', unliftedTypeKind)
278 kc_hs_type (HsFunTy ty1 ty2)
279 = kcTypeType ty1 `thenM` \ ty1' ->
280 kcTypeType ty2 `thenM` \ ty2' ->
281 returnM (HsFunTy ty1' ty2', liftedTypeKind)
283 kc_hs_type ty@(HsOpTy ty1 op ty2)
284 = addLocM 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 kc_hs_type ty@(HsAppTy ty1 ty2)
289 = kcHsType fun_ty `thenM` \ (fun_ty', fun_kind) ->
290 kcApps fun_kind (ppr fun_ty) arg_tys `thenM` \ ((arg_ty':arg_tys'), res_kind) ->
291 returnM (foldl mk_app (HsAppTy fun_ty' arg_ty') arg_tys', res_kind)
293 (fun_ty, arg_tys) = split ty1 [ty2]
294 split (L _ (HsAppTy f a)) as = split f (a:as)
296 mk_app fun arg = HsAppTy (noLoc fun) arg -- Add noLocs for inner nodes of
297 -- the application; they are never used
299 kc_hs_type (HsPredTy pred)
300 = kcHsPred pred `thenM` \ pred' ->
301 returnM (HsPredTy pred', liftedTypeKind)
303 kc_hs_type (HsForAllTy exp tv_names context ty)
304 = kcHsTyVars tv_names $ \ tv_names' ->
305 kcHsContext context `thenM` \ ctxt' ->
306 kcLiftedType ty `thenM` \ ty' ->
307 -- The body of a forall must be a type, but in principle
308 -- there's no reason to prohibit *unlifted* types.
309 -- In fact, GHC can itself construct a function with an
310 -- unboxed tuple inside a for-all (via CPR analyis; see
311 -- typecheck/should_compile/tc170)
313 -- Still, that's only for internal interfaces, which aren't
314 -- kind-checked, and it's a bit inconvenient to use kcTypeType
315 -- here (because it doesn't return the result kind), so I'm
316 -- leaving it as lifted types for now.
317 returnM (HsForAllTy exp tv_names' ctxt' ty', liftedTypeKind)
319 ---------------------------
320 kcApps :: TcKind -- Function kind
322 -> [LHsType Name] -- Arg types
323 -> TcM ([LHsType Name], TcKind) -- Kind-checked args
324 kcApps fun_kind ppr_fun args
325 = split_fk fun_kind (length args) `thenM` \ (arg_kinds, res_kind) ->
326 mappM kc_arg (args `zip` arg_kinds) `thenM` \ args' ->
327 returnM (args', res_kind)
329 split_fk fk 0 = returnM ([], fk)
330 split_fk fk n = unifyFunKind fk `thenM` \ mb_fk ->
332 Nothing -> failWithTc too_many_args
333 Just (ak,fk') -> split_fk fk' (n-1) `thenM` \ (aks, rk) ->
336 kc_arg (arg, arg_kind) = kcCheckHsType arg arg_kind
338 too_many_args = ptext SLIT("Kind error:") <+> quotes ppr_fun <+>
339 ptext SLIT("is applied to too many type arguments")
341 ---------------------------
342 kcHsContext :: LHsContext Name -> TcM (LHsContext Name)
343 kcHsContext ctxt = wrapLocM (mappM kcHsPred) ctxt
345 kcHsPred pred -- Checks that the result is of kind liftedType
346 = wrapLocFstM kc_pred pred `thenM` \ (pred', kind) ->
347 checkExpectedKind pred kind liftedTypeKind `thenM_`
350 ---------------------------
351 kc_pred :: HsPred Name -> TcM (HsPred Name, TcKind)
352 -- Does *not* check for a saturated
353 -- application (reason: used from TcDeriv)
354 kc_pred pred@(HsIParam name ty)
355 = kcHsType ty `thenM` \ (ty', kind) ->
356 returnM (HsIParam name ty', kind)
358 kc_pred pred@(HsClassP cls tys)
359 = kcClass cls `thenM` \ kind ->
360 kcApps kind (ppr cls) tys `thenM` \ (tys', res_kind) ->
361 returnM (HsClassP cls tys', res_kind)
363 ---------------------------
364 kcTyVar :: Name -> TcM TcKind
365 kcTyVar name -- Could be a tyvar or a tycon
366 = tcLookup name `thenM` \ thing ->
368 ATyVar tv -> returnM (tyVarKind tv)
369 ARecTyCon kind -> returnM kind
370 AGlobal (ATyCon tc) -> returnM (tyConKind tc)
371 other -> failWithTc (wrongThingErr "type" thing name)
373 kcClass :: Name -> TcM TcKind
374 kcClass cls -- Must be a class
375 = tcLookup cls `thenM` \ thing ->
377 ARecClass kind -> returnM kind
378 AGlobal (AClass cls) -> returnM (tyConKind (classTyCon cls))
379 other -> failWithTc (wrongThingErr "class" thing cls)
386 ---------------------------
387 -- We would like to get a decent error message from
388 -- (a) Under-applied type constructors
389 -- f :: (Maybe, Maybe)
390 -- (b) Over-applied type constructors
391 -- f :: Int x -> Int x
395 checkExpectedKind :: Outputable a => Located a -> TcKind -> TcKind -> TcM TcKind
396 -- A fancy wrapper for 'unifyKind', which tries to give
397 -- decent error messages.
398 -- Returns the same kind that it is passed, exp_kind
399 checkExpectedKind (L span ty) act_kind exp_kind
400 | act_kind `eqKind` exp_kind -- Short cut for a very common case
403 = tryTc (unifyKind exp_kind act_kind) `thenM` \ (errs, mb_r) ->
405 Just _ -> returnM exp_kind ; -- Unification succeeded
408 -- So there's definitely an error
409 -- Now to find out what sort
411 zonkTcType exp_kind `thenM` \ exp_kind ->
412 zonkTcType act_kind `thenM` \ act_kind ->
414 let (exp_as, _) = Type.splitFunTys exp_kind
415 (act_as, _) = Type.splitFunTys act_kind
416 -- Use the Type versions for kinds
417 n_exp_as = length exp_as
418 n_act_as = length act_as
420 err | n_exp_as < n_act_as -- E.g. [Maybe]
421 = quotes (ppr ty) <+> ptext SLIT("is not applied to enough type arguments")
423 -- Now n_exp_as >= n_act_as. In the next two cases,
424 -- n_exp_as == 0, and hence so is n_act_as
425 | exp_kind `eqKind` liftedTypeKind && act_kind `eqKind` unliftedTypeKind
426 = ptext SLIT("Expecting a lifted type, but") <+> quotes (ppr ty)
427 <+> ptext SLIT("is unlifted")
429 | exp_kind `eqKind` unliftedTypeKind && act_kind `eqKind` liftedTypeKind
430 = ptext SLIT("Expecting an unlifted type, but") <+> quotes (ppr ty)
431 <+> ptext SLIT("is lifted")
433 | otherwise -- E.g. Monad [Int]
434 = sep [ ptext SLIT("Expecting kind") <+> quotes (pprKind exp_kind) <> comma,
435 ptext SLIT("but") <+> quotes (ppr ty) <+>
436 ptext SLIT("has kind") <+> quotes (pprKind act_kind)]
438 failWithTc (ptext SLIT("Kind error:") <+> err)
442 %************************************************************************
446 %************************************************************************
450 * Transforms from HsType to Type
453 It cannot fail, and does no validity checking
456 dsHsType :: LHsType Name -> TcM Type
457 -- All HsTyVarBndrs in the intput type are kind-annotated
458 dsHsType ty = ds_type (unLoc ty)
460 ds_type ty@(HsTyVar name)
463 ds_type (HsParTy ty) -- Remove the parentheses markers
466 ds_type (HsKindSig ty k)
467 = dsHsType ty -- Kind checking done already
469 ds_type (HsListTy ty)
470 = dsHsType ty `thenM` \ tau_ty ->
471 returnM (mkListTy tau_ty)
473 ds_type (HsPArrTy ty)
474 = dsHsType ty `thenM` \ tau_ty ->
475 returnM (mkPArrTy tau_ty)
477 ds_type (HsTupleTy boxity tys)
478 = dsHsTypes tys `thenM` \ tau_tys ->
479 returnM (mkTupleTy boxity (length tys) tau_tys)
481 ds_type (HsFunTy ty1 ty2)
482 = dsHsType ty1 `thenM` \ tau_ty1 ->
483 dsHsType ty2 `thenM` \ tau_ty2 ->
484 returnM (mkFunTy tau_ty1 tau_ty2)
486 ds_type (HsOpTy ty1 (L span op) ty2)
487 = dsHsType ty1 `thenM` \ tau_ty1 ->
488 dsHsType ty2 `thenM` \ tau_ty2 ->
489 addSrcSpan span (ds_var_app op [tau_ty1,tau_ty2])
493 tcLookupTyCon genUnitTyConName `thenM` \ tc ->
494 returnM (mkTyConApp tc [])
496 ds_type ty@(HsAppTy _ _)
499 ds_type (HsPredTy pred)
500 = dsHsPred pred `thenM` \ pred' ->
501 returnM (mkPredTy pred')
503 ds_type full_ty@(HsForAllTy exp tv_names ctxt ty)
504 = tcTyVarBndrs tv_names $ \ tyvars ->
505 mappM dsHsPred (unLoc ctxt) `thenM` \ theta ->
506 dsHsType ty `thenM` \ tau ->
507 returnM (mkSigmaTy tyvars theta tau)
509 dsHsTypes arg_tys = mappM dsHsType arg_tys
512 Help functions for type applications
513 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
516 ds_app :: HsType Name -> [LHsType Name] -> TcM Type
517 ds_app (HsAppTy ty1 ty2) tys
518 = ds_app (unLoc ty1) (ty2:tys)
521 = dsHsTypes tys `thenM` \ arg_tys ->
523 HsTyVar fun -> ds_var_app fun arg_tys
524 other -> ds_type ty `thenM` \ fun_ty ->
525 returnM (mkAppTys fun_ty arg_tys)
527 ds_var_app :: Name -> [Type] -> TcM Type
528 ds_var_app name arg_tys
529 = tcLookup name `thenM` \ thing ->
531 ATyVar tv -> returnM (mkAppTys (mkTyVarTy tv) arg_tys)
532 AGlobal (ATyCon tc) -> returnM (mkGenTyConApp tc arg_tys)
533 ARecTyCon _ -> tcLookupTyCon name `thenM` \ tc ->
534 returnM (mkGenTyConApp tc arg_tys)
535 other -> pprPanic "ds_app_type" (ppr name <+> ppr arg_tys)
542 dsHsPred :: LHsPred Name -> TcM PredType
543 dsHsPred pred = ds_pred (unLoc pred)
545 ds_pred pred@(HsClassP class_name tys)
546 = dsHsTypes tys `thenM` \ arg_tys ->
547 tcLookupClass class_name `thenM` \ clas ->
548 returnM (ClassP clas arg_tys)
550 ds_pred (HsIParam name ty)
551 = dsHsType ty `thenM` \ arg_ty ->
552 returnM (IParam name arg_ty)
556 %************************************************************************
558 Type-variable binders
560 %************************************************************************
564 kcHsTyVars :: [LHsTyVarBndr Name]
565 -> ([LHsTyVarBndr Name] -> TcM r) -- These binders are kind-annotated
566 -- They scope over the thing inside
568 kcHsTyVars tvs thing_inside
569 = mappM (wrapLocM kcHsTyVar) tvs `thenM` \ bndrs ->
570 tcExtendTyVarKindEnv bndrs $
573 kcHsTyVar :: HsTyVarBndr Name -> TcM (HsTyVarBndr Name)
574 -- Return a *kind-annotated* binder, and a tyvar with a mutable kind in it
575 kcHsTyVar (UserTyVar name) = newKindVar `thenM` \ kind ->
576 returnM (KindedTyVar name kind)
577 kcHsTyVar (KindedTyVar name kind) = returnM (KindedTyVar name kind)
580 tcTyVarBndrs :: [LHsTyVarBndr Name] -- Kind-annotated binders, which need kind-zonking
581 -> ([TyVar] -> TcM r)
583 -- Used when type-checking types/classes/type-decls
584 -- Brings into scope immutable TyVars, not mutable ones that require later zonking
585 tcTyVarBndrs bndrs thing_inside
586 = mapM (zonk . unLoc) bndrs `thenM` \ tyvars ->
587 tcExtendTyVarEnv tyvars (thing_inside tyvars)
589 zonk (KindedTyVar name kind) = zonkTcKindToKind kind `thenM` \ kind' ->
590 returnM (mkTyVar name kind')
591 zonk (UserTyVar name) = pprTrace "BAD: Un-kinded tyvar" (ppr name) $
592 returnM (mkTyVar name liftedTypeKind)
596 %************************************************************************
598 Scoped type variables
600 %************************************************************************
603 tcAddScopedTyVars is used for scoped type variables added by pattern
605 e.g. \ ((x::a), (y::a)) -> x+y
606 They never have explicit kinds (because this is source-code only)
607 They are mutable (because they can get bound to a more specific type).
609 Usually we kind-infer and expand type splices, and then
610 tupecheck/desugar the type. That doesn't work well for scoped type
611 variables, because they scope left-right in patterns. (e.g. in the
612 example above, the 'a' in (y::a) is bound by the 'a' in (x::a).
614 The current not-very-good plan is to
615 * find all the types in the patterns
616 * find their free tyvars
618 * bring the kinded type vars into scope
619 * BUT throw away the kind-checked type
620 (we'll kind-check it again when we type-check the pattern)
622 This is bad because throwing away the kind checked type throws away
623 its splices. But too bad for now. [July 03]
626 We no longer specify that these type variables must be univerally
627 quantified (lots of email on the subject). If you want to put that
629 a) Do a checkSigTyVars after thing_inside
630 b) More insidiously, don't pass in expected_ty, else
631 we unify with it too early and checkSigTyVars barfs
632 Instead you have to pass in a fresh ty var, and unify
633 it with expected_ty afterwards
636 tcAddScopedTyVars :: [LHsType Name] -> TcM a -> TcM a
637 tcAddScopedTyVars [] thing_inside
638 = thing_inside -- Quick get-out for the empty case
640 tcAddScopedTyVars sig_tys thing_inside
641 = getInLocalScope `thenM` \ in_scope ->
642 getSrcSpanM `thenM` \ span ->
644 sig_tvs = [ L span (UserTyVar n)
646 n <- nameSetToList (extractHsTyVars ty),
648 -- The tyvars we want are the free type variables of
649 -- the type that are not already in scope
651 -- Behave like kcHsType on a ForAll type
652 -- i.e. make kinded tyvars with mutable kinds,
653 -- and kind-check the enclosed types
654 kcHsTyVars sig_tvs (\ kinded_tvs -> do
655 { mappM kcTypeType sig_tys
656 ; return kinded_tvs }) `thenM` \ kinded_tvs ->
658 -- Zonk the mutable kinds and bring the tyvars into scope
659 -- Rather like tcTyVarBndrs, except that it brings *mutable*
660 -- tyvars into scope, not immutable ones
662 -- Furthermore, the tyvars are PatSigTvs, which means that we get better
663 -- error messages when type variables escape:
664 -- Inferred type is less polymorphic than expected
665 -- Quantified type variable `t' escapes
666 -- It is mentioned in the environment:
667 -- t is bound by the pattern type signature at tcfail103.hs:6
668 mapM (zonk . unLoc) kinded_tvs `thenM` \ tyvars ->
669 tcExtendTyVarEnv tyvars thing_inside
672 zonk (KindedTyVar name kind) = zonkTcKindToKind kind `thenM` \ kind' ->
673 newMutTyVar name kind' PatSigTv
674 zonk (UserTyVar name) = pprTrace "BAD: Un-kinded tyvar" (ppr name) $
675 returnM (mkTyVar name liftedTypeKind)
679 %************************************************************************
681 \subsection{Signatures}
683 %************************************************************************
685 @tcSigs@ checks the signatures for validity, and returns a list of
686 {\em freshly-instantiated} signatures. That is, the types are already
687 split up, and have fresh type variables installed. All non-type-signature
688 "RenamedSigs" are ignored.
690 The @TcSigInfo@ contains @TcTypes@ because they are unified with
691 the variable's type, and after that checked to see whether they've
697 sig_poly_id :: TcId, -- *Polymorphic* binder for this value...
700 sig_tvs :: [TcTyVar], -- tyvars
701 sig_theta :: TcThetaType, -- theta
702 sig_tau :: TcTauType, -- tau
704 sig_mono_id :: TcId, -- *Monomorphic* binder for this value
705 -- Does *not* have name = N
708 sig_insts :: [Inst], -- Empty if theta is null, or
709 -- (method mono_id) otherwise
711 sig_loc :: SrcSpan -- The location of the signature
715 instance Outputable TcSigInfo where
716 ppr (TySigInfo id tyvars theta tau _ inst _) =
717 ppr id <+> ptext SLIT("::") <+> ppr tyvars <+> ppr theta <+> ptext SLIT("=>") <+> ppr tau
719 maybeSig :: [TcSigInfo] -> Name -> Maybe (TcSigInfo)
720 -- Search for a particular signature
721 maybeSig [] name = Nothing
722 maybeSig (sig@(TySigInfo sig_id _ _ _ _ _ _) : sigs) name
723 | name == idName sig_id = Just sig
724 | otherwise = maybeSig sigs name
729 tcTySig :: LSig Name -> TcM TcSigInfo
731 tcTySig (L span (Sig (L _ v) ty))
733 tcHsSigType (FunSigCtxt v) ty `thenM` \ sigma_tc_ty ->
734 mkTcSig (mkLocalId v sigma_tc_ty) `thenM` \ sig ->
737 mkTcSig :: TcId -> TcM TcSigInfo
739 = -- Instantiate this type
740 -- It's important to do this even though in the error-free case
741 -- we could just split the sigma_tc_ty (since the tyvars don't
742 -- unified with anything). But in the case of an error, when
743 -- the tyvars *do* get unified with something, we want to carry on
744 -- typechecking the rest of the program with the function bound
745 -- to a pristine type, namely sigma_tc_ty
746 tcInstType SigTv (idType poly_id) `thenM` \ (tyvars', theta', tau') ->
748 getInstLoc SignatureOrigin `thenM` \ inst_loc ->
749 newMethod inst_loc poly_id
751 theta' tau' `thenM` \ inst ->
752 -- We make a Method even if it's not overloaded; no harm
753 -- But do not extend the LIE! We're just making an Id.
755 getSrcSpanM `thenM` \ src_loc ->
756 returnM (TySigInfo { sig_poly_id = poly_id, sig_tvs = tyvars',
757 sig_theta = theta', sig_tau = tau',
758 sig_mono_id = instToId inst,
759 sig_insts = [inst], sig_loc = src_loc })
763 %************************************************************************
765 \subsection{Errors and contexts}
767 %************************************************************************
771 hoistForAllTys :: Type -> Type
772 -- Used for user-written type signatures only
773 -- Move all the foralls and constraints to the top
774 -- e.g. T -> forall a. a ==> forall a. T -> a
775 -- T -> (?x::Int) -> Int ==> (?x::Int) -> T -> Int
777 -- Also: eliminate duplicate constraints. These can show up
778 -- when hoisting constraints, notably implicit parameters.
780 -- We want to 'look through' type synonyms when doing this
781 -- so it's better done on the Type than the HsType
785 no_shadow_ty = deShadowTy ty
786 -- Running over ty with an empty substitution gives it the
787 -- no-shadowing property. This is important. For example:
788 -- type Foo r = forall a. a -> r
789 -- foo :: Foo (Foo ())
790 -- Here the hoisting should give
791 -- foo :: forall a a1. a -> a1 -> ()
793 -- What about type vars that are lexically in scope in the envt?
794 -- We simply rely on them having a different unique to any
795 -- binder in 'ty'. Otherwise we'd have to slurp the in-scope-tyvars
796 -- out of the envt, which is boring and (I think) not necessary.
798 case hoist no_shadow_ty of
799 (tvs, theta, body) -> mkForAllTys tvs (mkFunTys (nubBy tcEqType theta) body)
800 -- The 'nubBy' eliminates duplicate constraints,
801 -- notably implicit parameters
804 | (tvs1, body_ty) <- tcSplitForAllTys ty,
806 = case hoist body_ty of
807 (tvs2,theta,tau) -> (tvs1 ++ tvs2, theta, tau)
809 | Just (arg, res) <- tcSplitFunTy_maybe ty
811 arg' = hoistForAllTys arg -- Don't forget to apply hoist recursively
812 in -- to the argument type
813 if (isPredTy arg') then
815 (tvs,theta,tau) -> (tvs, arg':theta, tau)
818 (tvs,theta,tau) -> (tvs, theta, mkFunTy arg' tau)
820 | otherwise = ([], [], ty)
824 %************************************************************************
826 \subsection{Errors and contexts}
828 %************************************************************************
831 wrongThingErr expected thing name
832 = pp_thing thing <+> quotes (ppr name) <+> ptext SLIT("used as a") <+> text expected
834 pp_thing (AGlobal (ATyCon _)) = ptext SLIT("Type constructor")
835 pp_thing (AGlobal (AClass _)) = ptext SLIT("Class")
836 pp_thing (AGlobal (AnId _)) = ptext SLIT("Identifier")
837 pp_thing (AGlobal (ADataCon _)) = ptext SLIT("Data constructor")
838 pp_thing (ATyVar _) = ptext SLIT("Type variable")
839 pp_thing (ATcId _ _ _) = ptext SLIT("Local identifier")
840 pp_thing (ARecTyCon _) = ptext SLIT("Rec tycon")
841 pp_thing (ARecClass _) = ptext SLIT("Rec class")