2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 \section[TcMonoType]{Typechecking user-specified @MonoTypes@}
12 kcHsTyVars, kcHsSigType, kcHsLiftedSigType,
13 kcCheckHsType, kcHsContext, kcHsType,
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 -- kcHsType (HsSpliceTy s)
254 kc_hs_type (HsTyVar name)
255 = kcTyVar name `thenM` \ kind ->
256 returnM (HsTyVar name, kind)
258 kc_hs_type (HsListTy ty)
259 = kcLiftedType ty `thenM` \ ty' ->
260 returnM (HsListTy ty', liftedTypeKind)
262 kc_hs_type (HsPArrTy ty)
263 = kcLiftedType ty `thenM` \ ty' ->
264 returnM (HsPArrTy ty', liftedTypeKind)
266 kc_hs_type (HsNumTy n)
267 = returnM (HsNumTy n, liftedTypeKind)
269 kc_hs_type (HsKindSig ty k)
270 = kcCheckHsType ty k `thenM` \ ty' ->
271 returnM (HsKindSig ty' k, k)
273 kc_hs_type (HsTupleTy Boxed tys)
274 = mappM kcLiftedType tys `thenM` \ tys' ->
275 returnM (HsTupleTy Boxed tys', liftedTypeKind)
277 kc_hs_type (HsTupleTy Unboxed tys)
278 = mappM kcTypeType tys `thenM` \ tys' ->
279 returnM (HsTupleTy Unboxed tys', unliftedTypeKind)
281 kc_hs_type (HsFunTy ty1 ty2)
282 = kcTypeType ty1 `thenM` \ ty1' ->
283 kcTypeType ty2 `thenM` \ ty2' ->
284 returnM (HsFunTy ty1' ty2', liftedTypeKind)
286 kc_hs_type ty@(HsOpTy ty1 op ty2)
287 = addLocM kcTyVar op `thenM` \ op_kind ->
288 kcApps op_kind (ppr op) [ty1,ty2] `thenM` \ ([ty1',ty2'], res_kind) ->
289 returnM (HsOpTy ty1' op ty2', res_kind)
291 kc_hs_type ty@(HsAppTy ty1 ty2)
292 = kcHsType fun_ty `thenM` \ (fun_ty', fun_kind) ->
293 kcApps fun_kind (ppr fun_ty) arg_tys `thenM` \ ((arg_ty':arg_tys'), res_kind) ->
294 returnM (foldl mk_app (HsAppTy fun_ty' arg_ty') arg_tys', res_kind)
296 (fun_ty, arg_tys) = split ty1 [ty2]
297 split (L _ (HsAppTy f a)) as = split f (a:as)
299 mk_app fun arg = HsAppTy (noLoc fun) arg -- Add noLocs for inner nodes of
300 -- the application; they are never used
302 kc_hs_type (HsPredTy pred)
303 = kcHsPred pred `thenM` \ pred' ->
304 returnM (HsPredTy pred', liftedTypeKind)
306 kc_hs_type (HsForAllTy exp tv_names context ty)
307 = kcHsTyVars tv_names $ \ tv_names' ->
308 kcHsContext context `thenM` \ ctxt' ->
309 kcLiftedType ty `thenM` \ ty' ->
310 -- The body of a forall must be a type, but in principle
311 -- there's no reason to prohibit *unlifted* types.
312 -- In fact, GHC can itself construct a function with an
313 -- unboxed tuple inside a for-all (via CPR analyis; see
314 -- typecheck/should_compile/tc170)
316 -- Still, that's only for internal interfaces, which aren't
317 -- kind-checked, and it's a bit inconvenient to use kcTypeType
318 -- here (because it doesn't return the result kind), so I'm
319 -- leaving it as lifted types for now.
320 returnM (HsForAllTy exp tv_names' ctxt' ty', liftedTypeKind)
322 ---------------------------
323 kcApps :: TcKind -- Function kind
325 -> [LHsType Name] -- Arg types
326 -> TcM ([LHsType Name], TcKind) -- Kind-checked args
327 kcApps fun_kind ppr_fun args
328 = split_fk fun_kind (length args) `thenM` \ (arg_kinds, res_kind) ->
329 mappM kc_arg (args `zip` arg_kinds) `thenM` \ args' ->
330 returnM (args', res_kind)
332 split_fk fk 0 = returnM ([], fk)
333 split_fk fk n = unifyFunKind fk `thenM` \ mb_fk ->
335 Nothing -> failWithTc too_many_args
336 Just (ak,fk') -> split_fk fk' (n-1) `thenM` \ (aks, rk) ->
339 kc_arg (arg, arg_kind) = kcCheckHsType arg arg_kind
341 too_many_args = ptext SLIT("Kind error:") <+> quotes ppr_fun <+>
342 ptext SLIT("is applied to too many type arguments")
344 ---------------------------
345 kcHsContext :: LHsContext Name -> TcM (LHsContext Name)
346 kcHsContext ctxt = wrapLocM (mappM kcHsPred) ctxt
348 kcHsPred pred -- Checks that the result is of kind liftedType
349 = wrapLocFstM kc_pred pred `thenM` \ (pred', kind) ->
350 checkExpectedKind pred kind liftedTypeKind `thenM_`
353 ---------------------------
354 kc_pred :: HsPred Name -> TcM (HsPred Name, TcKind)
355 -- Does *not* check for a saturated
356 -- application (reason: used from TcDeriv)
357 kc_pred pred@(HsIParam name ty)
358 = kcHsType ty `thenM` \ (ty', kind) ->
359 returnM (HsIParam name ty', kind)
361 kc_pred pred@(HsClassP cls tys)
362 = kcClass cls `thenM` \ kind ->
363 kcApps kind (ppr cls) tys `thenM` \ (tys', res_kind) ->
364 returnM (HsClassP cls tys', res_kind)
366 ---------------------------
367 kcTyVar :: Name -> TcM TcKind
368 kcTyVar name -- Could be a tyvar or a tycon
369 = tcLookup name `thenM` \ thing ->
371 ATyVar tv -> returnM (tyVarKind tv)
372 ARecTyCon kind -> returnM kind
373 AGlobal (ATyCon tc) -> returnM (tyConKind tc)
374 other -> failWithTc (wrongThingErr "type" thing name)
376 kcClass :: Name -> TcM TcKind
377 kcClass cls -- Must be a class
378 = tcLookup cls `thenM` \ thing ->
380 ARecClass kind -> returnM kind
381 AGlobal (AClass cls) -> returnM (tyConKind (classTyCon cls))
382 other -> failWithTc (wrongThingErr "class" thing cls)
389 ---------------------------
390 -- We would like to get a decent error message from
391 -- (a) Under-applied type constructors
392 -- f :: (Maybe, Maybe)
393 -- (b) Over-applied type constructors
394 -- f :: Int x -> Int x
398 checkExpectedKind :: Outputable a => Located a -> TcKind -> TcKind -> TcM TcKind
399 -- A fancy wrapper for 'unifyKind', which tries to give
400 -- decent error messages.
401 -- Returns the same kind that it is passed, exp_kind
402 checkExpectedKind (L span ty) act_kind exp_kind
403 | act_kind `eqKind` exp_kind -- Short cut for a very common case
406 = tryTc (unifyKind exp_kind act_kind) `thenM` \ (errs, mb_r) ->
408 Just _ -> returnM exp_kind ; -- Unification succeeded
411 -- So there's definitely an error
412 -- Now to find out what sort
414 zonkTcType exp_kind `thenM` \ exp_kind ->
415 zonkTcType act_kind `thenM` \ act_kind ->
417 let (exp_as, _) = Type.splitFunTys exp_kind
418 (act_as, _) = Type.splitFunTys act_kind
419 -- Use the Type versions for kinds
420 n_exp_as = length exp_as
421 n_act_as = length act_as
423 err | n_exp_as < n_act_as -- E.g. [Maybe]
424 = quotes (ppr ty) <+> ptext SLIT("is not applied to enough type arguments")
426 -- Now n_exp_as >= n_act_as. In the next two cases,
427 -- n_exp_as == 0, and hence so is n_act_as
428 | exp_kind `eqKind` liftedTypeKind && act_kind `eqKind` unliftedTypeKind
429 = ptext SLIT("Expecting a lifted type, but") <+> quotes (ppr ty)
430 <+> ptext SLIT("is unlifted")
432 | exp_kind `eqKind` unliftedTypeKind && act_kind `eqKind` liftedTypeKind
433 = ptext SLIT("Expecting an unlifted type, but") <+> quotes (ppr ty)
434 <+> ptext SLIT("is lifted")
436 | otherwise -- E.g. Monad [Int]
437 = sep [ ptext SLIT("Expecting kind") <+> quotes (pprKind exp_kind) <> comma,
438 ptext SLIT("but") <+> quotes (ppr ty) <+>
439 ptext SLIT("has kind") <+> quotes (pprKind act_kind)]
441 failWithTc (ptext SLIT("Kind error:") <+> err)
445 %************************************************************************
449 %************************************************************************
453 * Transforms from HsType to Type
456 It cannot fail, and does no validity checking
459 dsHsType :: LHsType Name -> TcM Type
460 -- All HsTyVarBndrs in the intput type are kind-annotated
461 dsHsType ty = ds_type (unLoc ty)
463 ds_type ty@(HsTyVar name)
466 ds_type (HsParTy ty) -- Remove the parentheses markers
469 ds_type (HsKindSig ty k)
470 = dsHsType ty -- Kind checking done already
472 ds_type (HsListTy ty)
473 = dsHsType ty `thenM` \ tau_ty ->
474 returnM (mkListTy tau_ty)
476 ds_type (HsPArrTy ty)
477 = dsHsType ty `thenM` \ tau_ty ->
478 returnM (mkPArrTy tau_ty)
480 ds_type (HsTupleTy boxity tys)
481 = dsHsTypes tys `thenM` \ tau_tys ->
482 returnM (mkTupleTy boxity (length tys) tau_tys)
484 ds_type (HsFunTy ty1 ty2)
485 = dsHsType ty1 `thenM` \ tau_ty1 ->
486 dsHsType ty2 `thenM` \ tau_ty2 ->
487 returnM (mkFunTy tau_ty1 tau_ty2)
489 ds_type (HsOpTy ty1 (L span op) ty2)
490 = dsHsType ty1 `thenM` \ tau_ty1 ->
491 dsHsType ty2 `thenM` \ tau_ty2 ->
492 addSrcSpan span (ds_var_app op [tau_ty1,tau_ty2])
496 tcLookupTyCon genUnitTyConName `thenM` \ tc ->
497 returnM (mkTyConApp tc [])
499 ds_type ty@(HsAppTy _ _)
502 ds_type (HsPredTy pred)
503 = dsHsPred pred `thenM` \ pred' ->
504 returnM (mkPredTy pred')
506 ds_type full_ty@(HsForAllTy exp tv_names ctxt ty)
507 = tcTyVarBndrs tv_names $ \ tyvars ->
508 mappM dsHsPred (unLoc ctxt) `thenM` \ theta ->
509 dsHsType ty `thenM` \ tau ->
510 returnM (mkSigmaTy tyvars theta tau)
512 dsHsTypes arg_tys = mappM dsHsType arg_tys
515 Help functions for type applications
516 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
519 ds_app :: HsType Name -> [LHsType Name] -> TcM Type
520 ds_app (HsAppTy ty1 ty2) tys
521 = ds_app (unLoc ty1) (ty2:tys)
524 = dsHsTypes tys `thenM` \ arg_tys ->
526 HsTyVar fun -> ds_var_app fun arg_tys
527 other -> ds_type ty `thenM` \ fun_ty ->
528 returnM (mkAppTys fun_ty arg_tys)
530 ds_var_app :: Name -> [Type] -> TcM Type
531 ds_var_app name arg_tys
532 = tcLookup name `thenM` \ thing ->
534 ATyVar tv -> returnM (mkAppTys (mkTyVarTy tv) arg_tys)
535 AGlobal (ATyCon tc) -> returnM (mkGenTyConApp tc arg_tys)
536 ARecTyCon _ -> tcLookupTyCon name `thenM` \ tc ->
537 returnM (mkGenTyConApp tc arg_tys)
538 other -> pprPanic "ds_app_type" (ppr name <+> ppr arg_tys)
545 dsHsPred :: LHsPred Name -> TcM PredType
546 dsHsPred pred = ds_pred (unLoc pred)
548 ds_pred pred@(HsClassP class_name tys)
549 = dsHsTypes tys `thenM` \ arg_tys ->
550 tcLookupClass class_name `thenM` \ clas ->
551 returnM (ClassP clas arg_tys)
553 ds_pred (HsIParam name ty)
554 = dsHsType ty `thenM` \ arg_ty ->
555 returnM (IParam name arg_ty)
559 %************************************************************************
561 Type-variable binders
563 %************************************************************************
567 kcHsTyVars :: [LHsTyVarBndr Name]
568 -> ([LHsTyVarBndr Name] -> TcM r) -- These binders are kind-annotated
569 -- They scope over the thing inside
571 kcHsTyVars tvs thing_inside
572 = mappM (wrapLocM kcHsTyVar) tvs `thenM` \ bndrs ->
573 tcExtendTyVarKindEnv bndrs $
576 kcHsTyVar :: HsTyVarBndr Name -> TcM (HsTyVarBndr Name)
577 -- Return a *kind-annotated* binder, and a tyvar with a mutable kind in it
578 kcHsTyVar (UserTyVar name) = newKindVar `thenM` \ kind ->
579 returnM (KindedTyVar name kind)
580 kcHsTyVar (KindedTyVar name kind) = returnM (KindedTyVar name kind)
583 tcTyVarBndrs :: [LHsTyVarBndr Name] -- Kind-annotated binders, which need kind-zonking
584 -> ([TyVar] -> TcM r)
586 -- Used when type-checking types/classes/type-decls
587 -- Brings into scope immutable TyVars, not mutable ones that require later zonking
588 tcTyVarBndrs bndrs thing_inside
589 = mapM (zonk . unLoc) bndrs `thenM` \ tyvars ->
590 tcExtendTyVarEnv tyvars (thing_inside tyvars)
592 zonk (KindedTyVar name kind) = zonkTcKindToKind kind `thenM` \ kind' ->
593 returnM (mkTyVar name kind')
594 zonk (UserTyVar name) = pprTrace "BAD: Un-kinded tyvar" (ppr name) $
595 returnM (mkTyVar name liftedTypeKind)
599 %************************************************************************
601 Scoped type variables
603 %************************************************************************
606 tcAddScopedTyVars is used for scoped type variables added by pattern
608 e.g. \ ((x::a), (y::a)) -> x+y
609 They never have explicit kinds (because this is source-code only)
610 They are mutable (because they can get bound to a more specific type).
612 Usually we kind-infer and expand type splices, and then
613 tupecheck/desugar the type. That doesn't work well for scoped type
614 variables, because they scope left-right in patterns. (e.g. in the
615 example above, the 'a' in (y::a) is bound by the 'a' in (x::a).
617 The current not-very-good plan is to
618 * find all the types in the patterns
619 * find their free tyvars
621 * bring the kinded type vars into scope
622 * BUT throw away the kind-checked type
623 (we'll kind-check it again when we type-check the pattern)
625 This is bad because throwing away the kind checked type throws away
626 its splices. But too bad for now. [July 03]
629 We no longer specify that these type variables must be univerally
630 quantified (lots of email on the subject). If you want to put that
632 a) Do a checkSigTyVars after thing_inside
633 b) More insidiously, don't pass in expected_ty, else
634 we unify with it too early and checkSigTyVars barfs
635 Instead you have to pass in a fresh ty var, and unify
636 it with expected_ty afterwards
639 tcAddScopedTyVars :: [LHsType Name] -> TcM a -> TcM a
640 tcAddScopedTyVars [] thing_inside
641 = thing_inside -- Quick get-out for the empty case
643 tcAddScopedTyVars sig_tys thing_inside
644 = getInLocalScope `thenM` \ in_scope ->
645 getSrcSpanM `thenM` \ span ->
647 sig_tvs = [ L span (UserTyVar n)
649 n <- nameSetToList (extractHsTyVars ty),
651 -- The tyvars we want are the free type variables of
652 -- the type that are not already in scope
654 -- Behave like kcHsType on a ForAll type
655 -- i.e. make kinded tyvars with mutable kinds,
656 -- and kind-check the enclosed types
657 kcHsTyVars sig_tvs (\ kinded_tvs -> do
658 { mappM kcTypeType sig_tys
659 ; return kinded_tvs }) `thenM` \ kinded_tvs ->
661 -- Zonk the mutable kinds and bring the tyvars into scope
662 -- Rather like tcTyVarBndrs, except that it brings *mutable*
663 -- tyvars into scope, not immutable ones
665 -- Furthermore, the tyvars are PatSigTvs, which means that we get better
666 -- error messages when type variables escape:
667 -- Inferred type is less polymorphic than expected
668 -- Quantified type variable `t' escapes
669 -- It is mentioned in the environment:
670 -- t is bound by the pattern type signature at tcfail103.hs:6
671 mapM (zonk . unLoc) kinded_tvs `thenM` \ tyvars ->
672 tcExtendTyVarEnv tyvars thing_inside
675 zonk (KindedTyVar name kind) = zonkTcKindToKind kind `thenM` \ kind' ->
676 newMutTyVar name kind' PatSigTv
677 zonk (UserTyVar name) = pprTrace "BAD: Un-kinded tyvar" (ppr name) $
678 returnM (mkTyVar name liftedTypeKind)
682 %************************************************************************
684 \subsection{Signatures}
686 %************************************************************************
688 @tcSigs@ checks the signatures for validity, and returns a list of
689 {\em freshly-instantiated} signatures. That is, the types are already
690 split up, and have fresh type variables installed. All non-type-signature
691 "RenamedSigs" are ignored.
693 The @TcSigInfo@ contains @TcTypes@ because they are unified with
694 the variable's type, and after that checked to see whether they've
700 sig_poly_id :: TcId, -- *Polymorphic* binder for this value...
703 sig_tvs :: [TcTyVar], -- tyvars
704 sig_theta :: TcThetaType, -- theta
705 sig_tau :: TcTauType, -- tau
707 sig_mono_id :: TcId, -- *Monomorphic* binder for this value
708 -- Does *not* have name = N
711 sig_insts :: [Inst], -- Empty if theta is null, or
712 -- (method mono_id) otherwise
714 sig_loc :: SrcSpan -- The location of the signature
718 instance Outputable TcSigInfo where
719 ppr (TySigInfo id tyvars theta tau _ inst _) =
720 ppr id <+> ptext SLIT("::") <+> ppr tyvars <+> ppr theta <+> ptext SLIT("=>") <+> ppr tau
722 maybeSig :: [TcSigInfo] -> Name -> Maybe (TcSigInfo)
723 -- Search for a particular signature
724 maybeSig [] name = Nothing
725 maybeSig (sig@(TySigInfo sig_id _ _ _ _ _ _) : sigs) name
726 | name == idName sig_id = Just sig
727 | otherwise = maybeSig sigs name
732 tcTySig :: LSig Name -> TcM TcSigInfo
734 tcTySig (L span (Sig (L _ v) ty))
736 tcHsSigType (FunSigCtxt v) ty `thenM` \ sigma_tc_ty ->
737 mkTcSig (mkLocalId v sigma_tc_ty) `thenM` \ sig ->
740 mkTcSig :: TcId -> TcM TcSigInfo
742 = -- Instantiate this type
743 -- It's important to do this even though in the error-free case
744 -- we could just split the sigma_tc_ty (since the tyvars don't
745 -- unified with anything). But in the case of an error, when
746 -- the tyvars *do* get unified with something, we want to carry on
747 -- typechecking the rest of the program with the function bound
748 -- to a pristine type, namely sigma_tc_ty
749 tcInstType SigTv (idType poly_id) `thenM` \ (tyvars', theta', tau') ->
751 getInstLoc SignatureOrigin `thenM` \ inst_loc ->
752 newMethod inst_loc poly_id
754 theta' tau' `thenM` \ inst ->
755 -- We make a Method even if it's not overloaded; no harm
756 -- But do not extend the LIE! We're just making an Id.
758 getSrcSpanM `thenM` \ src_loc ->
759 returnM (TySigInfo { sig_poly_id = poly_id, sig_tvs = tyvars',
760 sig_theta = theta', sig_tau = tau',
761 sig_mono_id = instToId inst,
762 sig_insts = [inst], sig_loc = src_loc })
766 %************************************************************************
768 \subsection{Errors and contexts}
770 %************************************************************************
774 hoistForAllTys :: Type -> Type
775 -- Used for user-written type signatures only
776 -- Move all the foralls and constraints to the top
777 -- e.g. T -> forall a. a ==> forall a. T -> a
778 -- T -> (?x::Int) -> Int ==> (?x::Int) -> T -> Int
780 -- Also: eliminate duplicate constraints. These can show up
781 -- when hoisting constraints, notably implicit parameters.
783 -- We want to 'look through' type synonyms when doing this
784 -- so it's better done on the Type than the HsType
788 no_shadow_ty = deShadowTy ty
789 -- Running over ty with an empty substitution gives it the
790 -- no-shadowing property. This is important. For example:
791 -- type Foo r = forall a. a -> r
792 -- foo :: Foo (Foo ())
793 -- Here the hoisting should give
794 -- foo :: forall a a1. a -> a1 -> ()
796 -- What about type vars that are lexically in scope in the envt?
797 -- We simply rely on them having a different unique to any
798 -- binder in 'ty'. Otherwise we'd have to slurp the in-scope-tyvars
799 -- out of the envt, which is boring and (I think) not necessary.
801 case hoist no_shadow_ty of
802 (tvs, theta, body) -> mkForAllTys tvs (mkFunTys (nubBy tcEqType theta) body)
803 -- The 'nubBy' eliminates duplicate constraints,
804 -- notably implicit parameters
807 | (tvs1, body_ty) <- tcSplitForAllTys ty,
809 = case hoist body_ty of
810 (tvs2,theta,tau) -> (tvs1 ++ tvs2, theta, tau)
812 | Just (arg, res) <- tcSplitFunTy_maybe ty
814 arg' = hoistForAllTys arg -- Don't forget to apply hoist recursively
815 in -- to the argument type
816 if (isPredTy arg') then
818 (tvs,theta,tau) -> (tvs, arg':theta, tau)
821 (tvs,theta,tau) -> (tvs, theta, mkFunTy arg' tau)
823 | otherwise = ([], [], ty)
827 %************************************************************************
829 \subsection{Errors and contexts}
831 %************************************************************************
834 wrongThingErr expected thing name
835 = pp_thing thing <+> quotes (ppr name) <+> ptext SLIT("used as a") <+> text expected
837 pp_thing (AGlobal (ATyCon _)) = ptext SLIT("Type constructor")
838 pp_thing (AGlobal (AClass _)) = ptext SLIT("Class")
839 pp_thing (AGlobal (AnId _)) = ptext SLIT("Identifier")
840 pp_thing (AGlobal (ADataCon _)) = ptext SLIT("Data constructor")
841 pp_thing (ATyVar _) = ptext SLIT("Type variable")
842 pp_thing (ATcId _ _ _) = ptext SLIT("Local identifier")
843 pp_thing (ARecTyCon _) = ptext SLIT("Rec tycon")
844 pp_thing (ARecClass _) = ptext SLIT("Rec class")