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, tcExtendKindEnv,
32 tcLookup, tcLookupClass, tcLookupTyCon,
33 TyThing(..), TcTyThing(..),
34 getInLocalScope, wrongThingErr
36 import TcMType ( newKindVar, tcInstType, newMutTyVar,
38 checkValidType, UserTypeCtxt(..), pprHsSigCtxt
40 import TcUnify ( unifyFunKind, checkExpectedKind )
41 import TcType ( Type, PredType(..), ThetaType, TyVarDetails(..),
42 TcTyVar, TcKind, TcThetaType, TcTauType,
43 mkTyVarTy, mkTyVarTys, mkFunTy,
44 mkForAllTys, mkFunTys, tcEqType, isPredTy,
45 mkSigmaTy, mkPredTy, mkGenTyConApp, mkTyConApp, mkAppTys,
46 tcSplitFunTy_maybe, tcSplitForAllTys )
47 import Kind ( liftedTypeKind, ubxTupleKind, openTypeKind, argTypeKind )
48 import Inst ( Inst, InstOrigin(..), newMethod, instToId )
50 import Id ( mkLocalId, idName, idType )
51 import Var ( TyVar, mkTyVar, tyVarKind )
52 import TyCon ( TyCon, tyConKind )
53 import Class ( classTyCon )
56 import PrelNames ( genUnitTyConName )
57 import Subst ( deShadowTy )
58 import TysWiredIn ( mkListTy, mkPArrTy, mkTupleTy )
59 import BasicTypes ( Boxity(..) )
60 import SrcLoc ( SrcSpan, Located(..), unLoc, noLoc )
66 ----------------------------
68 ----------------------------
70 Generally speaking we now type-check types in three phases
72 1. kcHsType: kind check the HsType
73 *includes* performing any TH type splices;
74 so it returns a translated, and kind-annotated, type
76 2. dsHsType: convert from HsType to Type:
78 expand type synonyms [mkGenTyApps]
79 hoist the foralls [tcHsType]
81 3. checkValidType: check the validity of the resulting type
83 Often these steps are done one after the other (tcHsSigType).
84 But in mutually recursive groups of type and class decls we do
85 1 kind-check the whole group
86 2 build TyCons/Classes in a knot-tied way
87 3 check the validity of types in the now-unknotted TyCons/Classes
89 For example, when we find
90 (forall a m. m a -> m a)
91 we bind a,m to kind varibles and kind-check (m a -> m a). This makes
92 a get kind *, and m get kind *->*. Now we typecheck (m a -> m a) in
93 an environment that binds a and m suitably.
95 The kind checker passed to tcHsTyVars needs to look at enough to
96 establish the kind of the tyvar:
97 * For a group of type and class decls, it's just the group, not
98 the rest of the program
99 * For a tyvar bound in a pattern type signature, its the types
100 mentioned in the other type signatures in that bunch of patterns
101 * For a tyvar bound in a RULE, it's the type signatures on other
102 universally quantified variables in the rule
104 Note that this may occasionally give surprising results. For example:
106 data T a b = MkT (a b)
108 Here we deduce a::*->*, b::*
109 But equally valid would be a::(*->*)-> *, b::*->*
114 Some of the validity check could in principle be done by the kind checker,
117 - During desugaring, we normalise by expanding type synonyms. Only
118 after this step can we check things like type-synonym saturation
119 e.g. type T k = k Int
121 Then (T S) is ok, because T is saturated; (T S) expands to (S Int);
122 and then S is saturated. This is a GHC extension.
124 - Similarly, also a GHC extension, we look through synonyms before complaining
125 about the form of a class or instance declaration
127 - Ambiguity checks involve functional dependencies, and it's easier to wait
128 until knots have been resolved before poking into them
130 Also, in a mutually recursive group of types, we can't look at the TyCon until we've
131 finished building the loop. So to keep things simple, we postpone most validity
132 checking until step (3).
136 During step (1) we might fault in a TyCon defined in another module, and it might
137 (via a loop) refer back to a TyCon defined in this module. So when we tie a big
138 knot around type declarations with ARecThing, so that the fault-in code can get
139 the TyCon being defined.
142 %************************************************************************
144 \subsection{Checking types}
146 %************************************************************************
149 tcHsSigType :: UserTypeCtxt -> LHsType Name -> TcM Type
150 -- Do kind checking, and hoist for-alls to the top
151 tcHsSigType ctxt hs_ty
152 = addErrCtxt (pprHsSigCtxt ctxt hs_ty) $
153 do { kinded_ty <- kcTypeType hs_ty
154 ; ty <- tcHsKindedType kinded_ty
155 ; checkValidType ctxt ty
158 -- tcHsPred is happy with a partial application, e.g. (ST s)
161 = do { (kinded_pred,_) <- wrapLocFstM kc_pred pred -- kc_pred rather than kcHsPred
162 -- to avoid the partial application check
163 ; dsHsPred kinded_pred }
166 These functions are used during knot-tying in
167 type and class declarations, when we have to
168 separate kind-checking, desugaring, and validity checking
171 kcHsSigType, kcHsLiftedSigType :: LHsType Name -> TcM (LHsType Name)
172 -- Used for type signatures
173 kcHsSigType ty = kcTypeType ty
174 kcHsLiftedSigType ty = kcLiftedType ty
176 tcHsKindedType :: LHsType Name -> TcM Type
177 -- Don't do kind checking, nor validity checking,
178 -- but do hoist for-alls to the top
179 -- This is used in type and class decls, where kinding is
180 -- done in advance, and validity checking is done later
181 -- [Validity checking done later because of knot-tying issues.]
183 = do { ty <- dsHsType hs_ty
184 ; return (hoistForAllTys ty) }
186 tcHsKindedContext :: LHsContext Name -> TcM ThetaType
187 -- Used when we are expecting a ClassContext (i.e. no implicit params)
188 -- Does not do validity checking, like tcHsKindedType
189 tcHsKindedContext hs_theta = addLocM (mappM dsHsPred) hs_theta
193 %************************************************************************
195 The main kind checker: kcHsType
197 %************************************************************************
199 First a couple of simple wrappers for kcHsType
202 ---------------------------
203 kcLiftedType :: LHsType Name -> TcM (LHsType Name)
204 -- The type ty must be a *lifted* *type*
205 kcLiftedType ty = kcCheckHsType ty liftedTypeKind
207 ---------------------------
208 kcTypeType :: LHsType Name -> TcM (LHsType Name)
209 -- The type ty must be a *type*, but it can be lifted or
210 -- unlifted or an unboxed tuple.
211 kcTypeType ty = kcCheckHsType ty openTypeKind
213 ---------------------------
214 kcCheckHsType :: LHsType Name -> TcKind -> TcM (LHsType Name)
215 -- Check that the type has the specified kind
216 -- Be sure to use checkExpectedKind, rather than simply unifying
217 -- with OpenTypeKind, because it gives better error messages
218 kcCheckHsType (L span ty) exp_kind
220 kc_hs_type ty `thenM` \ (ty', act_kind) ->
221 checkExpectedKind ty act_kind exp_kind `thenM_`
225 Here comes the main function
228 kcHsType :: LHsType Name -> TcM (LHsType Name, TcKind)
229 kcHsType ty = wrapLocFstM kc_hs_type ty
230 -- kcHsType *returns* the kind of the type, rather than taking an expected
231 -- kind as argument as tcExpr does.
233 -- (a) the kind of (->) is
234 -- forall bx1 bx2. Type bx1 -> Type bx2 -> Type Boxed
235 -- so we'd need to generate huge numbers of bx variables.
236 -- (b) kinds are so simple that the error messages are fine
238 -- The translated type has explicitly-kinded type-variable binders
240 kc_hs_type (HsParTy ty)
241 = kcHsType ty `thenM` \ (ty', kind) ->
242 returnM (HsParTy ty', kind)
244 -- kcHsType (HsSpliceTy s)
247 kc_hs_type (HsTyVar name)
248 = kcTyVar name `thenM` \ kind ->
249 returnM (HsTyVar name, kind)
251 kc_hs_type (HsListTy ty)
252 = kcLiftedType ty `thenM` \ ty' ->
253 returnM (HsListTy ty', liftedTypeKind)
255 kc_hs_type (HsPArrTy ty)
256 = kcLiftedType ty `thenM` \ ty' ->
257 returnM (HsPArrTy ty', liftedTypeKind)
259 kc_hs_type (HsNumTy n)
260 = returnM (HsNumTy n, liftedTypeKind)
262 kc_hs_type (HsKindSig ty k)
263 = kcCheckHsType ty k `thenM` \ ty' ->
264 returnM (HsKindSig ty' k, k)
266 kc_hs_type (HsTupleTy Boxed tys)
267 = mappM kcLiftedType tys `thenM` \ tys' ->
268 returnM (HsTupleTy Boxed tys', liftedTypeKind)
270 kc_hs_type (HsTupleTy Unboxed tys)
271 = mappM kcTypeType tys `thenM` \ tys' ->
272 returnM (HsTupleTy Unboxed tys', ubxTupleKind)
274 kc_hs_type (HsFunTy ty1 ty2)
275 = kcCheckHsType ty1 argTypeKind `thenM` \ ty1' ->
276 kcTypeType ty2 `thenM` \ ty2' ->
277 returnM (HsFunTy ty1' ty2', liftedTypeKind)
279 kc_hs_type ty@(HsOpTy ty1 op ty2)
280 = addLocM kcTyVar op `thenM` \ op_kind ->
281 kcApps op_kind (ppr op) [ty1,ty2] `thenM` \ ([ty1',ty2'], res_kind) ->
282 returnM (HsOpTy ty1' op ty2', res_kind)
284 kc_hs_type ty@(HsAppTy ty1 ty2)
285 = kcHsType fun_ty `thenM` \ (fun_ty', fun_kind) ->
286 kcApps fun_kind (ppr fun_ty) arg_tys `thenM` \ ((arg_ty':arg_tys'), res_kind) ->
287 returnM (foldl mk_app (HsAppTy fun_ty' arg_ty') arg_tys', res_kind)
289 (fun_ty, arg_tys) = split ty1 [ty2]
290 split (L _ (HsAppTy f a)) as = split f (a:as)
292 mk_app fun arg = HsAppTy (noLoc fun) arg -- Add noLocs for inner nodes of
293 -- the application; they are never used
295 kc_hs_type (HsPredTy pred)
296 = kcHsPred pred `thenM` \ pred' ->
297 returnM (HsPredTy pred', liftedTypeKind)
299 kc_hs_type (HsForAllTy exp tv_names context ty)
300 = kcHsTyVars tv_names $ \ tv_names' ->
301 kcHsContext context `thenM` \ ctxt' ->
302 kcLiftedType ty `thenM` \ ty' ->
303 -- The body of a forall must be a type, but in principle
304 -- there's no reason to prohibit *unlifted* types.
305 -- In fact, GHC can itself construct a function with an
306 -- unboxed tuple inside a for-all (via CPR analyis; see
307 -- typecheck/should_compile/tc170)
309 -- Still, that's only for internal interfaces, which aren't
310 -- kind-checked, and it's a bit inconvenient to use kcTypeType
311 -- here (because it doesn't return the result kind), so I'm
312 -- leaving it as lifted types for now.
313 returnM (HsForAllTy exp tv_names' ctxt' ty', liftedTypeKind)
315 ---------------------------
316 kcApps :: TcKind -- Function kind
318 -> [LHsType Name] -- Arg types
319 -> TcM ([LHsType Name], TcKind) -- Kind-checked args
320 kcApps fun_kind ppr_fun args
321 = split_fk fun_kind (length args) `thenM` \ (arg_kinds, res_kind) ->
322 zipWithM kc_arg args arg_kinds `thenM` \ args' ->
323 returnM (args', res_kind)
325 split_fk fk 0 = returnM ([], fk)
326 split_fk fk n = unifyFunKind fk `thenM` \ mb_fk ->
328 Nothing -> failWithTc too_many_args
329 Just (ak,fk') -> split_fk fk' (n-1) `thenM` \ (aks, rk) ->
332 kc_arg arg arg_kind = kcCheckHsType arg arg_kind
334 too_many_args = ptext SLIT("Kind error:") <+> quotes ppr_fun <+>
335 ptext SLIT("is applied to too many type arguments")
337 ---------------------------
338 kcHsContext :: LHsContext Name -> TcM (LHsContext Name)
339 kcHsContext ctxt = wrapLocM (mappM kcHsPred) ctxt
341 kcHsPred (L span pred) -- Checks that the result is of kind liftedType
343 kc_pred pred `thenM` \ (pred', kind) ->
344 checkExpectedKind pred kind liftedTypeKind `thenM_`
345 returnM (L span pred')
347 ---------------------------
348 kc_pred :: HsPred Name -> TcM (HsPred Name, TcKind)
349 -- Does *not* check for a saturated
350 -- application (reason: used from TcDeriv)
351 kc_pred pred@(HsIParam name ty)
352 = kcHsType ty `thenM` \ (ty', kind) ->
353 returnM (HsIParam name ty', kind)
355 kc_pred pred@(HsClassP cls tys)
356 = kcClass cls `thenM` \ kind ->
357 kcApps kind (ppr cls) tys `thenM` \ (tys', res_kind) ->
358 returnM (HsClassP cls tys', res_kind)
360 ---------------------------
361 kcTyVar :: Name -> TcM TcKind
362 kcTyVar name -- Could be a tyvar or a tycon
363 = traceTc (text "lk1" <+> ppr name) `thenM_`
364 tcLookup name `thenM` \ thing ->
365 traceTc (text "lk2" <+> ppr name <+> ppr thing) `thenM_`
367 ATyVar tv -> returnM (tyVarKind tv)
368 AThing kind -> returnM kind
369 AGlobal (ATyCon tc) -> returnM (tyConKind tc)
370 other -> wrongThingErr "type" thing name
372 kcClass :: Name -> TcM TcKind
373 kcClass cls -- Must be a class
374 = tcLookup cls `thenM` \ thing ->
376 AThing kind -> returnM kind
377 AGlobal (AClass cls) -> returnM (tyConKind (classTyCon cls))
378 other -> wrongThingErr "class" thing cls
382 %************************************************************************
386 %************************************************************************
390 * Transforms from HsType to Type
393 It cannot fail, and does no validity checking
396 dsHsType :: LHsType Name -> TcM Type
397 -- All HsTyVarBndrs in the intput type are kind-annotated
398 dsHsType ty = ds_type (unLoc ty)
400 ds_type ty@(HsTyVar name)
403 ds_type (HsParTy ty) -- Remove the parentheses markers
406 ds_type (HsKindSig ty k)
407 = dsHsType ty -- Kind checking done already
409 ds_type (HsListTy ty)
410 = dsHsType ty `thenM` \ tau_ty ->
411 returnM (mkListTy tau_ty)
413 ds_type (HsPArrTy ty)
414 = dsHsType ty `thenM` \ tau_ty ->
415 returnM (mkPArrTy tau_ty)
417 ds_type (HsTupleTy boxity tys)
418 = dsHsTypes tys `thenM` \ tau_tys ->
419 returnM (mkTupleTy boxity (length tys) tau_tys)
421 ds_type (HsFunTy ty1 ty2)
422 = dsHsType ty1 `thenM` \ tau_ty1 ->
423 dsHsType ty2 `thenM` \ tau_ty2 ->
424 returnM (mkFunTy tau_ty1 tau_ty2)
426 ds_type (HsOpTy ty1 (L span op) ty2)
427 = dsHsType ty1 `thenM` \ tau_ty1 ->
428 dsHsType ty2 `thenM` \ tau_ty2 ->
429 addSrcSpan span (ds_var_app op [tau_ty1,tau_ty2])
433 tcLookupTyCon genUnitTyConName `thenM` \ tc ->
434 returnM (mkTyConApp tc [])
436 ds_type ty@(HsAppTy _ _)
439 ds_type (HsPredTy pred)
440 = dsHsPred pred `thenM` \ pred' ->
441 returnM (mkPredTy pred')
443 ds_type full_ty@(HsForAllTy exp tv_names ctxt ty)
444 = tcTyVarBndrs tv_names $ \ tyvars ->
445 mappM dsHsPred (unLoc ctxt) `thenM` \ theta ->
446 dsHsType ty `thenM` \ tau ->
447 returnM (mkSigmaTy tyvars theta tau)
449 dsHsTypes arg_tys = mappM dsHsType arg_tys
452 Help functions for type applications
453 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
456 ds_app :: HsType Name -> [LHsType Name] -> TcM Type
457 ds_app (HsAppTy ty1 ty2) tys
458 = ds_app (unLoc ty1) (ty2:tys)
461 = dsHsTypes tys `thenM` \ arg_tys ->
463 HsTyVar fun -> ds_var_app fun arg_tys
464 other -> ds_type ty `thenM` \ fun_ty ->
465 returnM (mkAppTys fun_ty arg_tys)
467 ds_var_app :: Name -> [Type] -> TcM Type
468 ds_var_app name arg_tys
469 = tcLookup name `thenM` \ thing ->
471 ATyVar tv -> returnM (mkAppTys (mkTyVarTy tv) arg_tys)
472 AGlobal (ATyCon tc) -> returnM (mkGenTyConApp tc arg_tys)
473 AThing _ -> tcLookupTyCon name `thenM` \ tc ->
474 returnM (mkGenTyConApp tc arg_tys)
475 other -> pprPanic "ds_app_type" (ppr name <+> ppr arg_tys)
482 dsHsPred :: LHsPred Name -> TcM PredType
483 dsHsPred pred = ds_pred (unLoc pred)
485 ds_pred pred@(HsClassP class_name tys)
486 = dsHsTypes tys `thenM` \ arg_tys ->
487 tcLookupClass class_name `thenM` \ clas ->
488 returnM (ClassP clas arg_tys)
490 ds_pred (HsIParam name ty)
491 = dsHsType ty `thenM` \ arg_ty ->
492 returnM (IParam name arg_ty)
496 %************************************************************************
498 Type-variable binders
500 %************************************************************************
504 kcHsTyVars :: [LHsTyVarBndr Name]
505 -> ([LHsTyVarBndr Name] -> TcM r) -- These binders are kind-annotated
506 -- They scope over the thing inside
508 kcHsTyVars tvs thing_inside
509 = mappM (wrapLocM kcHsTyVar) tvs `thenM` \ bndrs ->
510 tcExtendKindEnv [(n,k) | L _ (KindedTyVar n k) <- bndrs]
513 kcHsTyVar :: HsTyVarBndr Name -> TcM (HsTyVarBndr Name)
514 -- Return a *kind-annotated* binder, and a tyvar with a mutable kind in it
515 kcHsTyVar (UserTyVar name) = newKindVar `thenM` \ kind ->
516 returnM (KindedTyVar name kind)
517 kcHsTyVar (KindedTyVar name kind) = returnM (KindedTyVar name kind)
520 tcTyVarBndrs :: [LHsTyVarBndr Name] -- Kind-annotated binders, which need kind-zonking
521 -> ([TyVar] -> TcM r)
523 -- Used when type-checking types/classes/type-decls
524 -- Brings into scope immutable TyVars, not mutable ones that require later zonking
525 tcTyVarBndrs bndrs thing_inside
526 = mapM (zonk . unLoc) bndrs `thenM` \ tyvars ->
527 tcExtendTyVarEnv tyvars (thing_inside tyvars)
529 zonk (KindedTyVar name kind) = zonkTcKindToKind kind `thenM` \ kind' ->
530 returnM (mkTyVar name kind')
531 zonk (UserTyVar name) = pprTrace "BAD: Un-kinded tyvar" (ppr name) $
532 returnM (mkTyVar name liftedTypeKind)
536 %************************************************************************
538 Scoped type variables
540 %************************************************************************
543 tcAddScopedTyVars is used for scoped type variables added by pattern
545 e.g. \ ((x::a), (y::a)) -> x+y
546 They never have explicit kinds (because this is source-code only)
547 They are mutable (because they can get bound to a more specific type).
549 Usually we kind-infer and expand type splices, and then
550 tupecheck/desugar the type. That doesn't work well for scoped type
551 variables, because they scope left-right in patterns. (e.g. in the
552 example above, the 'a' in (y::a) is bound by the 'a' in (x::a).
554 The current not-very-good plan is to
555 * find all the types in the patterns
556 * find their free tyvars
558 * bring the kinded type vars into scope
559 * BUT throw away the kind-checked type
560 (we'll kind-check it again when we type-check the pattern)
562 This is bad because throwing away the kind checked type throws away
563 its splices. But too bad for now. [July 03]
566 We no longer specify that these type variables must be univerally
567 quantified (lots of email on the subject). If you want to put that
569 a) Do a checkSigTyVars after thing_inside
570 b) More insidiously, don't pass in expected_ty, else
571 we unify with it too early and checkSigTyVars barfs
572 Instead you have to pass in a fresh ty var, and unify
573 it with expected_ty afterwards
576 tcAddScopedTyVars :: [LHsType Name] -> TcM a -> TcM a
577 tcAddScopedTyVars [] thing_inside
578 = thing_inside -- Quick get-out for the empty case
580 tcAddScopedTyVars sig_tys thing_inside
581 = getInLocalScope `thenM` \ in_scope ->
582 getSrcSpanM `thenM` \ span ->
584 sig_tvs = [ L span (UserTyVar n)
586 n <- nameSetToList (extractHsTyVars ty),
588 -- The tyvars we want are the free type variables of
589 -- the type that are not already in scope
591 -- Behave like kcHsType on a ForAll type
592 -- i.e. make kinded tyvars with mutable kinds,
593 -- and kind-check the enclosed types
594 kcHsTyVars sig_tvs (\ kinded_tvs -> do
595 { mappM kcTypeType sig_tys
596 ; return kinded_tvs }) `thenM` \ kinded_tvs ->
598 -- Zonk the mutable kinds and bring the tyvars into scope
599 -- Rather like tcTyVarBndrs, except that it brings *mutable*
600 -- tyvars into scope, not immutable ones
602 -- Furthermore, the tyvars are PatSigTvs, which means that we get better
603 -- error messages when type variables escape:
604 -- Inferred type is less polymorphic than expected
605 -- Quantified type variable `t' escapes
606 -- It is mentioned in the environment:
607 -- t is bound by the pattern type signature at tcfail103.hs:6
608 mapM (zonk . unLoc) kinded_tvs `thenM` \ tyvars ->
609 tcExtendTyVarEnv tyvars thing_inside
612 zonk (KindedTyVar name kind) = zonkTcKindToKind kind `thenM` \ kind' ->
613 newMutTyVar name kind' PatSigTv
614 zonk (UserTyVar name) = pprTrace "BAD: Un-kinded tyvar" (ppr name) $
615 returnM (mkTyVar name liftedTypeKind)
619 %************************************************************************
621 \subsection{Signatures}
623 %************************************************************************
625 @tcSigs@ checks the signatures for validity, and returns a list of
626 {\em freshly-instantiated} signatures. That is, the types are already
627 split up, and have fresh type variables installed. All non-type-signature
628 "RenamedSigs" are ignored.
630 The @TcSigInfo@ contains @TcTypes@ because they are unified with
631 the variable's type, and after that checked to see whether they've
637 sig_poly_id :: TcId, -- *Polymorphic* binder for this value...
640 sig_tvs :: [TcTyVar], -- tyvars
641 sig_theta :: TcThetaType, -- theta
642 sig_tau :: TcTauType, -- tau
644 sig_mono_id :: TcId, -- *Monomorphic* binder for this value
645 -- Does *not* have name = N
648 sig_insts :: [Inst], -- Empty if theta is null, or
649 -- (method mono_id) otherwise
651 sig_loc :: SrcSpan -- The location of the signature
655 instance Outputable TcSigInfo where
656 ppr (TySigInfo id tyvars theta tau _ inst _) =
657 ppr id <+> ptext SLIT("::") <+> ppr tyvars <+> ppr theta <+> ptext SLIT("=>") <+> ppr tau
659 maybeSig :: [TcSigInfo] -> Name -> Maybe (TcSigInfo)
660 -- Search for a particular signature
661 maybeSig [] name = Nothing
662 maybeSig (sig@(TySigInfo sig_id _ _ _ _ _ _) : sigs) name
663 | name == idName sig_id = Just sig
664 | otherwise = maybeSig sigs name
669 tcTySig :: LSig Name -> TcM TcSigInfo
671 tcTySig (L span (Sig (L _ v) ty))
673 tcHsSigType (FunSigCtxt v) ty `thenM` \ sigma_tc_ty ->
674 mkTcSig (mkLocalId v sigma_tc_ty) `thenM` \ sig ->
677 mkTcSig :: TcId -> TcM TcSigInfo
679 = -- Instantiate this type
680 -- It's important to do this even though in the error-free case
681 -- we could just split the sigma_tc_ty (since the tyvars don't
682 -- unified with anything). But in the case of an error, when
683 -- the tyvars *do* get unified with something, we want to carry on
684 -- typechecking the rest of the program with the function bound
685 -- to a pristine type, namely sigma_tc_ty
686 tcInstType SigTv (idType poly_id) `thenM` \ (tyvars', theta', tau') ->
688 getInstLoc SignatureOrigin `thenM` \ inst_loc ->
689 newMethod inst_loc poly_id
691 theta' tau' `thenM` \ inst ->
692 -- We make a Method even if it's not overloaded; no harm
693 -- But do not extend the LIE! We're just making an Id.
695 getSrcSpanM `thenM` \ src_loc ->
696 returnM (TySigInfo { sig_poly_id = poly_id, sig_tvs = tyvars',
697 sig_theta = theta', sig_tau = tau',
698 sig_mono_id = instToId inst,
699 sig_insts = [inst], sig_loc = src_loc })
703 %************************************************************************
705 \subsection{Errors and contexts}
707 %************************************************************************
711 hoistForAllTys :: Type -> Type
712 -- Used for user-written type signatures only
713 -- Move all the foralls and constraints to the top
714 -- e.g. T -> forall a. a ==> forall a. T -> a
715 -- T -> (?x::Int) -> Int ==> (?x::Int) -> T -> Int
717 -- Also: eliminate duplicate constraints. These can show up
718 -- when hoisting constraints, notably implicit parameters.
720 -- We want to 'look through' type synonyms when doing this
721 -- so it's better done on the Type than the HsType
725 no_shadow_ty = deShadowTy ty
726 -- Running over ty with an empty substitution gives it the
727 -- no-shadowing property. This is important. For example:
728 -- type Foo r = forall a. a -> r
729 -- foo :: Foo (Foo ())
730 -- Here the hoisting should give
731 -- foo :: forall a a1. a -> a1 -> ()
733 -- What about type vars that are lexically in scope in the envt?
734 -- We simply rely on them having a different unique to any
735 -- binder in 'ty'. Otherwise we'd have to slurp the in-scope-tyvars
736 -- out of the envt, which is boring and (I think) not necessary.
738 case hoist no_shadow_ty of
739 (tvs, theta, body) -> mkForAllTys tvs (mkFunTys (nubBy tcEqType theta) body)
740 -- The 'nubBy' eliminates duplicate constraints,
741 -- notably implicit parameters
744 | (tvs1, body_ty) <- tcSplitForAllTys ty,
746 = case hoist body_ty of
747 (tvs2,theta,tau) -> (tvs1 ++ tvs2, theta, tau)
749 | Just (arg, res) <- tcSplitFunTy_maybe ty
751 arg' = hoistForAllTys arg -- Don't forget to apply hoist recursively
752 in -- to the argument type
753 if (isPredTy arg') then
755 (tvs,theta,tau) -> (tvs, arg':theta, tau)
758 (tvs,theta,tau) -> (tvs, theta, mkFunTy arg' tau)
760 | otherwise = ([], [], ty)