[project @ 2001-03-13 14:58:25 by simonpj]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcMonoType.lhs
1 %
2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
3 %
4 \section[TcMonoType]{Typechecking user-specified @MonoTypes@}
5
6 \begin{code}
7 module TcMonoType ( tcHsType, tcHsRecType, tcIfaceType,
8                     tcHsSigType, tcHsLiftedSigType, 
9                     tcRecTheta, checkAmbiguity,
10
11                         -- Kind checking
12                     kcHsTyVar, kcHsTyVars, mkTyClTyVars,
13                     kcHsType, kcHsSigType, kcHsLiftedSigType, kcHsContext,
14                     tcTyVars, tcHsTyVars, mkImmutTyVars,
15
16                     TcSigInfo(..), tcTySig, mkTcSig, maybeSig,
17                     checkSigTyVars, sigCtxt, sigPatCtxt
18                   ) where
19
20 #include "HsVersions.h"
21
22 import HsSyn            ( HsType(..), HsTyVarBndr(..),
23                           Sig(..), HsPred(..), pprParendHsType, HsTupCon(..), hsTyVarNames )
24 import RnHsSyn          ( RenamedHsType, RenamedHsPred, RenamedContext, RenamedSig )
25 import TcHsSyn          ( TcId )
26
27 import TcMonad
28 import TcEnv            ( tcExtendTyVarEnv, tcLookup, tcLookupGlobal,
29                           tcGetGlobalTyVars, tcEnvTcIds, tcEnvTyVars,
30                           TyThing(..), TcTyThing(..), tcExtendKindEnv
31                         )
32 import TcType           ( TcKind, TcTyVar, TcThetaType, TcTauType,
33                           newKindVar, tcInstSigVar,
34                           zonkKindEnv, zonkTcType, zonkTcTyVars, zonkTcTyVar
35                         )
36 import Inst             ( Inst, InstOrigin(..), newMethodWithGivenTy, instToId )
37 import FunDeps          ( grow )
38 import TcUnify          ( unifyKind, unifyOpenTypeKind )
39 import Unify            ( allDistinctTyVars )
40 import Type             ( Type, Kind, PredType(..), ThetaType, SigmaType, TauType,
41                           mkTyVarTy, mkTyVarTys, mkFunTy, mkSynTy,
42                           zipFunTys, hoistForAllTys,
43                           mkSigmaTy, mkPredTy, mkTyConApp,
44                           mkAppTys, splitForAllTys, splitRhoTy, mkRhoTy,
45                           liftedTypeKind, unliftedTypeKind, mkArrowKind,
46                           mkArrowKinds, getTyVar_maybe, getTyVar, splitFunTy_maybe,
47                           tidyOpenType, tidyOpenTypes, tidyTyVar, tidyTyVars,
48                           tyVarsOfType, tyVarsOfPred, mkForAllTys,
49                           isUnboxedTupleType, isForAllTy, isIPPred
50                         )
51 import PprType          ( pprType, pprPred )
52 import Subst            ( mkTopTyVarSubst, substTy )
53 import CoreFVs          ( idFreeTyVars )
54 import Id               ( mkLocalId, idName, idType )
55 import Var              ( Id, Var, TyVar, mkTyVar, tyVarKind )
56 import VarEnv
57 import VarSet
58 import ErrUtils         ( Message )
59 import TyCon            ( TyCon, isSynTyCon, tyConArity, tyConKind )
60 import Class            ( classArity, classTyCon )
61 import Name             ( Name )
62 import TysWiredIn       ( mkListTy, mkTupleTy, genUnitTyCon )
63 import BasicTypes       ( Boxity(..), RecFlag(..), isRec )
64 import SrcLoc           ( SrcLoc )
65 import Util             ( mapAccumL, isSingleton )
66 import Outputable
67
68 \end{code}
69
70
71 %************************************************************************
72 %*                                                                      *
73 \subsection{Kind checking}
74 %*                                                                      *
75 %************************************************************************
76
77 Kind checking
78 ~~~~~~~~~~~~~
79 When we come across the binding site for some type variables, we
80 proceed in two stages
81
82 1. Figure out what kind each tyvar has
83
84 2. Create suitably-kinded tyvars, 
85    extend the envt, 
86    and typecheck the body
87
88 To do step 1, we proceed thus:
89
90 1a. Bind each type variable to a kind variable
91 1b. Apply the kind checker
92 1c. Zonk the resulting kinds
93
94 The kind checker is passed to tcHsTyVars as an argument.  
95
96 For example, when we find
97         (forall a m. m a -> m a)
98 we bind a,m to kind varibles and kind-check (m a -> m a).  This
99 makes a get kind *, and m get kind *->*.  Now we typecheck (m a -> m a)
100 in an environment that binds a and m suitably.
101
102 The kind checker passed to tcHsTyVars needs to look at enough to
103 establish the kind of the tyvar:
104   * For a group of type and class decls, it's just the group, not
105         the rest of the program
106   * For a tyvar bound in a pattern type signature, its the types
107         mentioned in the other type signatures in that bunch of patterns
108   * For a tyvar bound in a RULE, it's the type signatures on other
109         universally quantified variables in the rule
110
111 Note that this may occasionally give surprising results.  For example:
112
113         data T a b = MkT (a b)
114
115 Here we deduce                  a::*->*, b::*.
116 But equally valid would be
117                                 a::(*->*)-> *, b::*->*
118
119 \begin{code}
120 tcHsTyVars :: [HsTyVarBndr Name] 
121            -> TcM a                             -- The kind checker
122            -> ([TyVar] -> TcM b)
123            -> TcM b
124
125 tcHsTyVars [] kind_check thing_inside = thing_inside []
126         -- A useful short cut for a common case!
127   
128 tcHsTyVars tv_names kind_check thing_inside
129   = kcHsTyVars tv_names                                 `thenNF_Tc` \ tv_names_w_kinds ->
130     tcExtendKindEnv tv_names_w_kinds kind_check         `thenTc_`
131     zonkKindEnv tv_names_w_kinds                        `thenNF_Tc` \ tvs_w_kinds ->
132     let
133         tyvars = mkImmutTyVars tvs_w_kinds
134     in
135     tcExtendTyVarEnv tyvars (thing_inside tyvars)
136
137 tcTyVars :: [Name] 
138              -> TcM a                           -- The kind checker
139              -> TcM [TyVar]
140 tcTyVars [] kind_check = returnTc []
141
142 tcTyVars tv_names kind_check
143   = mapNF_Tc newNamedKindVar tv_names           `thenTc` \ kind_env ->
144     tcExtendKindEnv kind_env kind_check         `thenTc_`
145     zonkKindEnv kind_env                        `thenNF_Tc` \ tvs_w_kinds ->
146     listNF_Tc [tcNewSigTyVar name kind | (name,kind) <- tvs_w_kinds]
147 \end{code}
148     
149
150 \begin{code}
151 kcHsTyVar  :: HsTyVarBndr name   -> NF_TcM (name, TcKind)
152 kcHsTyVars :: [HsTyVarBndr name] -> NF_TcM [(name, TcKind)]
153
154 kcHsTyVar (UserTyVar name)       = newNamedKindVar name
155 kcHsTyVar (IfaceTyVar name kind) = returnNF_Tc (name, kind)
156
157 kcHsTyVars tvs = mapNF_Tc kcHsTyVar tvs
158
159 newNamedKindVar name = newKindVar       `thenNF_Tc` \ kind ->
160                        returnNF_Tc (name, kind)
161
162 ---------------------------
163 kcLiftedType :: RenamedHsType -> TcM ()
164         -- The type ty must be a *lifted* *type*
165 kcLiftedType ty
166   = kcHsType ty                         `thenTc` \ kind ->
167     tcAddErrCtxt (typeKindCtxt ty)      $
168     unifyKind liftedTypeKind kind
169     
170 ---------------------------
171 kcTypeType :: RenamedHsType -> TcM ()
172         -- The type ty must be a *type*, but it can be lifted or unlifted.
173 kcTypeType ty
174   = kcHsType ty                         `thenTc` \ kind ->
175     tcAddErrCtxt (typeKindCtxt ty)      $
176     unifyOpenTypeKind kind
177
178 ---------------------------
179 kcHsSigType, kcHsLiftedSigType :: RenamedHsType -> TcM ()
180         -- Used for type signatures
181 kcHsSigType      = kcTypeType
182 kcHsLiftedSigType = kcLiftedType
183
184 ---------------------------
185 kcHsType :: RenamedHsType -> TcM TcKind
186 kcHsType (HsTyVar name)       = kcTyVar name
187
188 kcHsType (HsListTy ty)
189   = kcLiftedType ty             `thenTc` \ tau_ty ->
190     returnTc liftedTypeKind
191
192 kcHsType (HsTupleTy (HsTupCon _ boxity _) tys)
193   = mapTc kcTypeType tys        `thenTc_`
194     returnTc (case boxity of
195                   Boxed   -> liftedTypeKind
196                   Unboxed -> unliftedTypeKind)
197
198 kcHsType (HsFunTy ty1 ty2)
199   = kcTypeType ty1      `thenTc_`
200     kcTypeType ty2      `thenTc_`
201     returnTc liftedTypeKind
202
203 kcHsType ty@(HsOpTy ty1 op ty2)
204   = kcTyVar op                          `thenTc` \ op_kind ->
205     kcHsType ty1                        `thenTc` \ ty1_kind ->
206     kcHsType ty2                        `thenTc` \ ty2_kind ->
207     tcAddErrCtxt (appKindCtxt (ppr ty)) $
208     kcAppKind op_kind  ty1_kind         `thenTc` \ op_kind' ->
209     kcAppKind op_kind' ty2_kind
210    
211 kcHsType (HsPredTy pred)
212   = kcHsPred pred               `thenTc_`
213     returnTc liftedTypeKind
214
215 kcHsType ty@(HsAppTy ty1 ty2)
216   = kcHsType ty1                        `thenTc` \ tc_kind ->
217     kcHsType ty2                        `thenTc` \ arg_kind ->
218     tcAddErrCtxt (appKindCtxt (ppr ty)) $
219     kcAppKind tc_kind arg_kind
220
221 kcHsType (HsForAllTy (Just tv_names) context ty)
222   = kcHsTyVars tv_names         `thenNF_Tc` \ kind_env ->
223     tcExtendKindEnv kind_env    $
224     kcHsContext context         `thenTc_`
225     kcHsType ty                 `thenTc_`
226     returnTc liftedTypeKind
227
228 ---------------------------
229 kcAppKind fun_kind arg_kind
230   = case splitFunTy_maybe fun_kind of 
231         Just (arg_kind', res_kind)
232                 -> unifyKind arg_kind arg_kind' `thenTc_`
233                    returnTc res_kind
234
235         Nothing -> newKindVar                                           `thenNF_Tc` \ res_kind ->
236                    unifyKind fun_kind (mkArrowKind arg_kind res_kind)   `thenTc_`
237                    returnTc res_kind
238
239
240 ---------------------------
241 kcHsContext ctxt = mapTc_ kcHsPred ctxt
242
243 kcHsPred :: RenamedHsPred -> TcM ()
244 kcHsPred pred@(HsIParam name ty)
245   = tcAddErrCtxt (appKindCtxt (ppr pred))       $
246     kcLiftedType ty
247
248 kcHsPred pred@(HsClassP cls tys)
249   = tcAddErrCtxt (appKindCtxt (ppr pred))       $
250     kcClass cls                                 `thenTc` \ kind ->
251     mapTc kcHsType tys                          `thenTc` \ arg_kinds ->
252     unifyKind kind (mkArrowKinds arg_kinds liftedTypeKind)
253
254  ---------------------------
255 kcTyVar name    -- Could be a tyvar or a tycon
256   = tcLookup name       `thenTc` \ thing ->
257     case thing of 
258         AThing kind         -> returnTc kind
259         ATyVar tv           -> returnTc (tyVarKind tv)
260         AGlobal (ATyCon tc) -> returnTc (tyConKind tc) 
261         other               -> failWithTc (wrongThingErr "type" thing name)
262
263 kcClass cls     -- Must be a class
264   = tcLookup cls                                `thenNF_Tc` \ thing -> 
265     case thing of
266         AThing kind           -> returnTc kind
267         AGlobal (AClass cls)  -> returnTc (tyConKind (classTyCon cls))
268         other                 -> failWithTc (wrongThingErr "class" thing cls)
269 \end{code}
270
271 %************************************************************************
272 %*                                                                      *
273 \subsection{Checking types}
274 %*                                                                      *
275 %************************************************************************
276
277 tcHsSigType and tcHsLiftedSigType
278 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
279
280 tcHsSigType and tcHsLiftedSigType are used for type signatures written by the programmer
281
282   * We hoist any inner for-alls to the top
283
284   * Notice that we kind-check first, because the type-check assumes
285         that the kinds are already checked.
286
287   * They are only called when there are no kind vars in the environment
288         so the kind returned is indeed a Kind not a TcKind
289
290 \begin{code}
291 tcHsSigType, tcHsLiftedSigType :: RenamedHsType -> TcM Type
292   -- Do kind checking, and hoist for-alls to the top
293 tcHsSigType       ty = kcTypeType   ty `thenTc_` tcHsType ty    
294 tcHsLiftedSigType ty = kcLiftedType ty `thenTc_` tcHsType ty
295
296 tcHsType    ::            RenamedHsType -> TcM Type
297 tcHsRecType :: RecFlag -> RenamedHsType -> TcM Type
298   -- Don't do kind checking, but do hoist for-alls to the top
299   -- These are used in type and class decls, where kinding is
300   -- done in advance
301 tcHsType             ty = tc_type NonRecursive ty  `thenTc` \ ty' ->  returnTc (hoistForAllTys ty')
302 tcHsRecType wimp_out ty = tc_type wimp_out     ty  `thenTc` \ ty' ->  returnTc (hoistForAllTys ty')
303
304 -- In interface files the type is already kinded,
305 -- and we definitely don't want to hoist for-alls.
306 -- Otherwise we'll change
307 --      dmfail :: forall m:(*->*) Monad m => forall a:* => String -> m a
308 -- into 
309 --      dmfail :: forall m:(*->*) a:* Monad m => String -> m a
310 -- which definitely isn't right!
311 tcIfaceType ty = tc_type NonRecursive ty
312 \end{code}
313
314
315 %************************************************************************
316 %*                                                                      *
317 \subsection{tc_type}
318 %*                                                                      *
319 %************************************************************************
320
321 tc_type, the main work horse
322 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
323
324         -------------------
325         *** BIG WARNING ***
326         -------------------
327
328 tc_type is used to typecheck the types in the RHS of data
329 constructors.  In the case of recursive data types, that means that
330 the type constructors themselves are (partly) black holes.  e.g.
331
332         data T a = MkT a [T a]
333
334 While typechecking the [T a] on the RHS, T itself is not yet fully
335 defined.  That in turn places restrictions on what you can check in
336 tcHsType; if you poke on too much you get a black hole.  I keep
337 forgetting this, hence this warning!
338
339 The wimp_out argument tells when we are in a mutually-recursive
340 group of type declarations, so omit various checks else we
341 get a black hole.  They'll be done again later, in TcTyClDecls.tcGroup.
342
343         --------------------------
344         *** END OF BIG WARNING ***
345         --------------------------
346
347
348 \begin{code}
349 tc_type :: RecFlag -> RenamedHsType -> TcM Type
350
351 tc_type wimp_out ty@(HsTyVar name)
352   = tc_app wimp_out ty []
353
354 tc_type wimp_out (HsListTy ty)
355   = tc_arg_type wimp_out ty     `thenTc` \ tau_ty ->
356     returnTc (mkListTy tau_ty)
357
358 tc_type wimp_out (HsTupleTy (HsTupCon _ boxity arity) tys)
359   = ASSERT( arity == length tys )
360     mapTc tc_tup_arg tys        `thenTc` \ tau_tys ->
361     returnTc (mkTupleTy boxity arity tau_tys)
362   where
363     tc_tup_arg = case boxity of
364                    Boxed   -> tc_arg_type wimp_out
365                    Unboxed -> tc_type     wimp_out 
366         -- Unboxed tuples can have polymorphic or unboxed args.
367         -- This happens in the workers for functions returning
368         -- product types with polymorphic components
369
370 tc_type wimp_out (HsFunTy ty1 ty2)
371   = tc_type wimp_out ty1                        `thenTc` \ tau_ty1 ->
372         -- Function argument can be polymorphic, but
373         -- must not be an unboxed tuple
374     checkTc (not (isUnboxedTupleType tau_ty1))
375             (ubxArgTyErr ty1)                   `thenTc_`
376     tc_type wimp_out ty2                        `thenTc` \ tau_ty2 ->
377     returnTc (mkFunTy tau_ty1 tau_ty2)
378
379 tc_type wimp_out (HsNumTy n)
380   = ASSERT(n== 1)
381     returnTc (mkTyConApp genUnitTyCon [])
382
383 tc_type wimp_out (HsOpTy ty1 op ty2) =
384   tc_arg_type wimp_out ty1 `thenTc` \ tau_ty1 ->
385   tc_arg_type wimp_out ty2 `thenTc` \ tau_ty2 ->
386   tc_fun_type op [tau_ty1,tau_ty2]
387
388 tc_type wimp_out (HsAppTy ty1 ty2)
389   = tc_app wimp_out ty1 [ty2]
390
391 tc_type wimp_out (HsPredTy pred)
392   = tc_pred wimp_out pred       `thenTc` \ pred' ->
393     returnTc (mkPredTy pred')
394
395 tc_type wimp_out full_ty@(HsForAllTy (Just tv_names) ctxt ty)
396   = let
397         kind_check = kcHsContext ctxt `thenTc_` kcHsType ty
398     in
399     tcHsTyVars tv_names kind_check                      $ \ tyvars ->
400     tcRecTheta wimp_out ctxt                            `thenTc` \ theta ->
401
402         -- Context behaves like a function type
403         -- This matters.  Return-unboxed-tuple analysis can
404         -- give overloaded functions like
405         --      f :: forall a. Num a => (# a->a, a->a #)
406         -- And we want these to get through the type checker
407     (if null theta then
408         tc_arg_type wimp_out ty
409      else
410         tc_type wimp_out ty
411     )                                                   `thenTc` \ tau ->
412
413     checkAmbiguity wimp_out is_source tyvars theta tau
414   where
415     is_source = case tv_names of
416                    (UserTyVar _ : _) -> True
417                    other             -> False
418
419
420   -- tc_arg_type checks that the argument of a 
421   -- type appplication isn't a for-all type or an unboxed tuple type
422   -- For example, we want to reject things like:
423   --
424   --    instance Ord a => Ord (forall s. T s a)
425   -- and
426   --    g :: T s (forall b.b)
427   --
428   -- Other unboxed types are very occasionally allowed as type
429   -- arguments depending on the kind of the type constructor
430
431 tc_arg_type wimp_out arg_ty     
432   | isRec wimp_out
433   = tc_type wimp_out arg_ty
434
435   | otherwise
436   = tc_type wimp_out arg_ty                                             `thenTc` \ arg_ty' ->
437     checkTc (not (isForAllTy arg_ty'))         (polyArgTyErr arg_ty)    `thenTc_`
438     checkTc (not (isUnboxedTupleType arg_ty')) (ubxArgTyErr arg_ty)     `thenTc_`
439     returnTc arg_ty'
440
441 tc_arg_types wimp_out arg_tys = mapTc (tc_arg_type wimp_out) arg_tys
442 \end{code}
443
444 Help functions for type applications
445 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
446
447 \begin{code}
448 tc_app :: RecFlag -> RenamedHsType -> [RenamedHsType] -> TcM Type
449 tc_app wimp_out (HsAppTy ty1 ty2) tys
450   = tc_app wimp_out ty1 (ty2:tys)
451
452 tc_app wimp_out ty tys
453   = tcAddErrCtxt (appKindCtxt pp_app)   $
454     tc_arg_types wimp_out tys           `thenTc` \ arg_tys ->
455     case ty of
456         HsTyVar fun -> tc_fun_type fun arg_tys
457         other       -> tc_type wimp_out ty              `thenTc` \ fun_ty ->
458                        returnNF_Tc (mkAppTys fun_ty arg_tys)
459   where
460     pp_app = ppr ty <+> sep (map pprParendHsType tys)
461
462 -- (tc_fun_type ty arg_tys) returns (mkAppTys ty arg_tys)
463 -- But not quite; for synonyms it checks the correct arity, and builds a SynTy
464 --      hence the rather strange functionality.
465
466 tc_fun_type name arg_tys
467   = tcLookup name                       `thenTc` \ thing ->
468     case thing of
469         ATyVar tv -> returnTc (mkAppTys (mkTyVarTy tv) arg_tys)
470
471         AGlobal (ATyCon tc)
472                 | isSynTyCon tc ->  checkTc arity_ok err_msg    `thenTc_`
473                                     returnTc (mkAppTys (mkSynTy tc (take arity arg_tys))
474                                                        (drop arity arg_tys))
475
476                 | otherwise       ->  returnTc (mkTyConApp tc arg_tys)
477                 where
478
479                     arity_ok = arity <= n_args 
480                     arity = tyConArity tc
481                         -- It's OK to have an *over-applied* type synonym
482                         --      data Tree a b = ...
483                         --      type Foo a = Tree [a]
484                         --      f :: Foo a b -> ...
485                     err_msg = arityErr "Type synonym" name arity n_args
486                     n_args  = length arg_tys
487
488         other -> failWithTc (wrongThingErr "type constructor" thing name)
489 \end{code}
490
491
492 Contexts
493 ~~~~~~~~
494 \begin{code}
495 tcRecTheta :: RecFlag -> RenamedContext -> TcM ThetaType
496         -- Used when we are expecting a ClassContext (i.e. no implicit params)
497 tcRecTheta wimp_out context = mapTc (tc_pred wimp_out) context
498
499 tc_pred wimp_out assn@(HsClassP class_name tys)
500   = tcAddErrCtxt (appKindCtxt (ppr assn))       $
501     tc_arg_types wimp_out tys                   `thenTc` \ arg_tys ->
502     tcLookupGlobal class_name                   `thenTc` \ thing ->
503     case thing of
504         AClass clas -> checkTc (arity == n_tys) err     `thenTc_`
505                        returnTc (ClassP clas arg_tys)
506             where
507                 arity = classArity clas
508                 n_tys = length tys
509                 err   = arityErr "Class" class_name arity n_tys
510
511         other -> failWithTc (wrongThingErr "class" (AGlobal thing) class_name)
512
513 tc_pred wimp_out assn@(HsIParam name ty)
514   = tcAddErrCtxt (appKindCtxt (ppr assn))       $
515     tc_arg_type wimp_out ty                     `thenTc` \ arg_ty ->
516     returnTc (IParam name arg_ty)
517 \end{code}
518
519
520 Check for ambiguity
521 ~~~~~~~~~~~~~~~~~~~
522           forall V. P => tau
523 is ambiguous if P contains generic variables
524 (i.e. one of the Vs) that are not mentioned in tau
525
526 However, we need to take account of functional dependencies
527 when we speak of 'mentioned in tau'.  Example:
528         class C a b | a -> b where ...
529 Then the type
530         forall x y. (C x y) => x
531 is not ambiguous because x is mentioned and x determines y
532
533 NOTE: In addition, GHC insists that at least one type variable
534 in each constraint is in V.  So we disallow a type like
535         forall a. Eq b => b -> b
536 even in a scope where b is in scope.
537 This is the is_free test below.
538
539 Notes on the 'is_source_polytype' test above
540 Check ambiguity only for source-program types, not
541 for types coming from inteface files.  The latter can
542 legitimately have ambiguous types. Example
543    class S a where s :: a -> (Int,Int)
544    instance S Char where s _ = (1,1)
545    f:: S a => [a] -> Int -> (Int,Int)
546    f (_::[a]) x = (a*x,b)
547         where (a,b) = s (undefined::a)
548 Here the worker for f gets the type
549         fw :: forall a. S a => Int -> (# Int, Int #)
550
551 If the list of tv_names is empty, we have a monotype,
552 and then we don't need to check for ambiguity either,
553 because the test can't fail (see is_ambig).
554
555 \begin{code}
556 checkAmbiguity :: RecFlag -> Bool
557                -> [TyVar] -> ThetaType -> TauType
558                -> TcM SigmaType
559 checkAmbiguity wimp_out is_source_polytype forall_tyvars theta tau
560   | isRec wimp_out = returnTc sigma_ty
561   | otherwise      = mapTc_ check_pred theta    `thenTc_`
562                      returnTc sigma_ty
563   where
564     sigma_ty          = mkSigmaTy forall_tyvars theta tau
565     tau_vars          = tyVarsOfType tau
566     extended_tau_vars = grow theta tau_vars
567
568     is_ambig ct_var   = (ct_var `elem` forall_tyvars) &&
569                         not (ct_var `elemVarSet` extended_tau_vars)
570     is_free ct_var    = not (ct_var `elem` forall_tyvars)
571     
572     check_pred pred = checkTc (not any_ambig)                 (ambigErr pred sigma_ty) `thenTc_`
573                       checkTc (isIPPred pred || not all_free) (freeErr  pred sigma_ty)
574              where 
575                 ct_vars   = varSetElems (tyVarsOfPred pred)
576                 all_free  = all is_free ct_vars
577                 any_ambig = is_source_polytype && any is_ambig ct_vars
578 \end{code}
579
580 %************************************************************************
581 %*                                                                      *
582 \subsection{Type variables, with knot tying!}
583 %*                                                                      *
584 %************************************************************************
585
586 \begin{code}
587 mkImmutTyVars :: [(Name,Kind)] -> [TyVar]
588 mkImmutTyVars pairs = [mkTyVar name kind | (name, kind) <- pairs]
589
590 mkTyClTyVars :: Kind                    -- Kind of the tycon or class
591              -> [HsTyVarBndr Name]
592              -> [TyVar]
593 mkTyClTyVars kind tyvar_names
594   = mkImmutTyVars tyvars_w_kinds
595   where
596     (tyvars_w_kinds, _) = zipFunTys (hsTyVarNames tyvar_names) kind
597 \end{code}
598
599
600 %************************************************************************
601 %*                                                                      *
602 \subsection{Signatures}
603 %*                                                                      *
604 %************************************************************************
605
606 @tcSigs@ checks the signatures for validity, and returns a list of
607 {\em freshly-instantiated} signatures.  That is, the types are already
608 split up, and have fresh type variables installed.  All non-type-signature
609 "RenamedSigs" are ignored.
610
611 The @TcSigInfo@ contains @TcTypes@ because they are unified with
612 the variable's type, and after that checked to see whether they've
613 been instantiated.
614
615 \begin{code}
616 data TcSigInfo
617   = TySigInfo       
618         Name                    -- N, the Name in corresponding binding
619
620         TcId                    -- *Polymorphic* binder for this value...
621                                 -- Has name = N
622
623         [TcTyVar]               -- tyvars
624         TcThetaType             -- theta
625         TcTauType               -- tau
626
627         TcId                    -- *Monomorphic* binder for this value
628                                 -- Does *not* have name = N
629                                 -- Has type tau
630
631         [Inst]                  -- Empty if theta is null, or
632                                 -- (method mono_id) otherwise
633
634         SrcLoc                  -- Of the signature
635
636 instance Outputable TcSigInfo where
637     ppr (TySigInfo nm id tyvars theta tau _ inst loc) =
638         ppr nm <+> ptext SLIT("::") <+> ppr tyvars <+> ppr theta <+> ptext SLIT("=>") <+> ppr tau
639
640 maybeSig :: [TcSigInfo] -> Name -> Maybe (TcSigInfo)
641         -- Search for a particular signature
642 maybeSig [] name = Nothing
643 maybeSig (sig@(TySigInfo sig_name _ _ _ _ _ _ _) : sigs) name
644   | name == sig_name = Just sig
645   | otherwise        = maybeSig sigs name
646 \end{code}
647
648
649 \begin{code}
650 tcTySig :: RenamedSig -> TcM TcSigInfo
651
652 tcTySig (Sig v ty src_loc)
653  = tcAddSrcLoc src_loc                          $ 
654    tcAddErrCtxt (tcsigCtxt v)                   $
655    tcHsSigType ty                               `thenTc` \ sigma_tc_ty ->
656    mkTcSig (mkLocalId v sigma_tc_ty) src_loc    `thenNF_Tc` \ sig -> 
657    returnTc sig
658
659 mkTcSig :: TcId -> SrcLoc -> NF_TcM TcSigInfo
660 mkTcSig poly_id src_loc
661   =     -- Instantiate this type
662         -- It's important to do this even though in the error-free case
663         -- we could just split the sigma_tc_ty (since the tyvars don't
664         -- unified with anything).  But in the case of an error, when
665         -- the tyvars *do* get unified with something, we want to carry on
666         -- typechecking the rest of the program with the function bound
667         -- to a pristine type, namely sigma_tc_ty
668    let
669         (tyvars, rho) = splitForAllTys (idType poly_id)
670    in
671    mapNF_Tc tcInstSigVar tyvars         `thenNF_Tc` \ tyvars' ->
672         -- Make *signature* type variables
673
674    let
675      tyvar_tys' = mkTyVarTys tyvars'
676      rho' = substTy (mkTopTyVarSubst tyvars tyvar_tys') rho
677         -- mkTopTyVarSubst because the tyvars' are fresh
678      (theta', tau') = splitRhoTy rho'
679         -- This splitRhoTy tries hard to make sure that tau' is a type synonym
680         -- wherever possible, which can improve interface files.
681    in
682    newMethodWithGivenTy SignatureOrigin 
683                 poly_id
684                 tyvar_tys'
685                 theta' tau'                     `thenNF_Tc` \ inst ->
686         -- We make a Method even if it's not overloaded; no harm
687         
688    returnNF_Tc (TySigInfo name poly_id tyvars' theta' tau' (instToId inst) [inst] src_loc)
689   where
690     name = idName poly_id
691 \end{code}
692
693
694
695 %************************************************************************
696 %*                                                                      *
697 \subsection{Checking signature type variables}
698 %*                                                                      *
699 %************************************************************************
700
701 @checkSigTyVars@ is used after the type in a type signature has been unified with
702 the actual type found.  It then checks that the type variables of the type signature
703 are
704         (a) Still all type variables
705                 eg matching signature [a] against inferred type [(p,q)]
706                 [then a will be unified to a non-type variable]
707
708         (b) Still all distinct
709                 eg matching signature [(a,b)] against inferred type [(p,p)]
710                 [then a and b will be unified together]
711
712         (c) Not mentioned in the environment
713                 eg the signature for f in this:
714
715                         g x = ... where
716                                         f :: a->[a]
717                                         f y = [x,y]
718
719                 Here, f is forced to be monorphic by the free occurence of x.
720
721         (d) Not (unified with another type variable that is) in scope.
722                 eg f x :: (r->r) = (\y->y) :: forall a. a->r
723             when checking the expression type signature, we find that
724             even though there is nothing in scope whose type mentions r,
725             nevertheless the type signature for the expression isn't right.
726
727             Another example is in a class or instance declaration:
728                 class C a where
729                    op :: forall b. a -> b
730                    op x = x
731             Here, b gets unified with a
732
733 Before doing this, the substitution is applied to the signature type variable.
734
735 We used to have the notion of a "DontBind" type variable, which would
736 only be bound to itself or nothing.  Then points (a) and (b) were 
737 self-checking.  But it gave rise to bogus consequential error messages.
738 For example:
739
740    f = (*)      -- Monomorphic
741
742    g :: Num a => a -> a
743    g x = f x x
744
745 Here, we get a complaint when checking the type signature for g,
746 that g isn't polymorphic enough; but then we get another one when
747 dealing with the (Num x) context arising from f's definition;
748 we try to unify x with Int (to default it), but find that x has already
749 been unified with the DontBind variable "a" from g's signature.
750 This is really a problem with side-effecting unification; we'd like to
751 undo g's effects when its type signature fails, but unification is done
752 by side effect, so we can't (easily).
753
754 So we revert to ordinary type variables for signatures, and try to
755 give a helpful message in checkSigTyVars.
756
757 \begin{code}
758 checkSigTyVars :: [TcTyVar]             -- Universally-quantified type variables in the signature
759                -> TcTyVarSet            -- Tyvars that are free in the type signature
760                                         --      Not necessarily zonked
761                                         --      These should *already* be in the free-in-env set, 
762                                         --      and are used here only to improve the error message
763                -> TcM [TcTyVar]         -- Zonked signature type variables
764
765 checkSigTyVars [] free = returnTc []
766 checkSigTyVars sig_tyvars free_tyvars
767   = zonkTcTyVars sig_tyvars             `thenNF_Tc` \ sig_tys ->
768     tcGetGlobalTyVars                   `thenNF_Tc` \ globals ->
769
770     checkTcM (allDistinctTyVars sig_tys globals)
771              (complain sig_tys globals) `thenTc_`
772
773     returnTc (map (getTyVar "checkSigTyVars") sig_tys)
774
775   where
776     complain sig_tys globals
777       = -- For the in-scope ones, zonk them and construct a map
778         -- from the zonked tyvar to the in-scope one
779         -- If any of the in-scope tyvars zonk to a type, then ignore them;
780         -- that'll be caught later when we back up to their type sig
781         tcGetEnv                                `thenNF_Tc` \ env ->
782         let
783            in_scope_tvs = tcEnvTyVars env
784         in
785         zonkTcTyVars in_scope_tvs               `thenNF_Tc` \ in_scope_tys ->
786         let
787             in_scope_assoc = [ (zonked_tv, in_scope_tv) 
788                              | (z_ty, in_scope_tv) <- in_scope_tys `zip` in_scope_tvs,
789                                Just zonked_tv <- [getTyVar_maybe z_ty]
790                              ]
791             in_scope_env = mkVarEnv in_scope_assoc
792         in
793
794         -- "check" checks each sig tyvar in turn
795         foldlNF_Tc check
796                    (env2, in_scope_env, [])
797                    (tidy_tvs `zip` tidy_tys)    `thenNF_Tc` \ (env3, _, msgs) ->
798
799         failWithTcM (env3, main_msg $$ nest 4 (vcat msgs))
800       where
801         (env1, tidy_tvs) = mapAccumL tidyTyVar emptyTidyEnv sig_tyvars
802         (env2, tidy_tys) = tidyOpenTypes env1 sig_tys
803
804         main_msg = ptext SLIT("Inferred type is less polymorphic than expected")
805
806         check (tidy_env, acc, msgs) (sig_tyvar,ty)
807                 -- sig_tyvar is from the signature;
808                 -- ty is what you get if you zonk sig_tyvar and then tidy it
809                 --
810                 -- acc maps a zonked type variable back to a signature type variable
811           = case getTyVar_maybe ty of {
812               Nothing ->                        -- Error (a)!
813                         returnNF_Tc (tidy_env, acc, unify_msg sig_tyvar (ppr ty) : msgs) ;
814
815               Just tv ->
816
817             case lookupVarEnv acc tv of {
818                 Just sig_tyvar' ->      -- Error (b) or (d)!
819                         returnNF_Tc (tidy_env, acc, unify_msg sig_tyvar (ppr sig_tyvar') : msgs) ;
820
821                 Nothing ->
822
823             if tv `elemVarSet` globals  -- Error (c)! Type variable escapes
824                                         -- The least comprehensible, so put it last
825                         -- Game plan: 
826                         --    a) get the local TcIds from the environment,
827                         --       and pass them to find_globals (they might have tv free)
828                         --    b) similarly, find any free_tyvars that mention tv
829             then   tcGetEnv                                                     `thenNF_Tc` \ ve ->
830                    find_globals tv tidy_env  [] (tcEnvTcIds ve)                 `thenNF_Tc` \ (tidy_env1, globs) ->
831                    find_frees   tv tidy_env1 [] (varSetElems free_tyvars)       `thenNF_Tc` \ (tidy_env2, frees) ->
832                    returnNF_Tc (tidy_env2, acc, escape_msg sig_tyvar tv globs frees : msgs)
833
834             else        -- All OK
835             returnNF_Tc (tidy_env, extendVarEnv acc tv sig_tyvar, msgs)
836             }}
837
838 -- find_globals looks at the value environment and finds values
839 -- whose types mention the offending type variable.  It has to be 
840 -- careful to zonk the Id's type first, so it has to be in the monad.
841 -- We must be careful to pass it a zonked type variable, too.
842
843 find_globals :: Var 
844              -> TidyEnv 
845              -> [(Name,Type)] 
846              -> [Id] 
847              -> NF_TcM (TidyEnv,[(Name,Type)])
848
849 find_globals tv tidy_env acc []
850   = returnNF_Tc (tidy_env, acc)
851
852 find_globals tv tidy_env acc (id:ids) 
853   | isEmptyVarSet (idFreeTyVars id)
854   = find_globals tv tidy_env acc ids
855
856   | otherwise
857   = zonkTcType (idType id)      `thenNF_Tc` \ id_ty ->
858     if tv `elemVarSet` tyVarsOfType id_ty then
859         let 
860            (tidy_env', id_ty') = tidyOpenType tidy_env id_ty
861            acc'                = (idName id, id_ty') : acc
862         in
863         find_globals tv tidy_env' acc' ids
864     else
865         find_globals tv tidy_env  acc  ids
866
867 find_frees tv tidy_env acc []
868   = returnNF_Tc (tidy_env, acc)
869 find_frees tv tidy_env acc (ftv:ftvs)
870   = zonkTcTyVar ftv     `thenNF_Tc` \ ty ->
871     if tv `elemVarSet` tyVarsOfType ty then
872         let
873             (tidy_env', ftv') = tidyTyVar tidy_env ftv
874         in
875         find_frees tv tidy_env' (ftv':acc) ftvs
876     else
877         find_frees tv tidy_env  acc        ftvs
878
879
880 escape_msg sig_tv tv globs frees
881   = mk_msg sig_tv <+> ptext SLIT("escapes") $$
882     if not (null globs) then
883         vcat [pp_it <+> ptext SLIT("is mentioned in the environment"),
884               ptext SLIT("The following variables in the environment mention") <+> quotes (ppr tv),
885               nest 2 (vcat_first 10 [ppr name <+> dcolon <+> ppr ty | (name,ty) <- globs])
886         ]
887      else if not (null frees) then
888         vcat [ptext SLIT("It is reachable from the type variable(s)") <+> pprQuotedList frees,
889               nest 2 (ptext SLIT("which") <+> is_are <+> ptext SLIT("free in the signature"))
890         ]
891      else
892         empty   -- Sigh.  It's really hard to give a good error message
893                 -- all the time.   One bad case is an existential pattern match
894   where
895     is_are | isSingleton frees = ptext SLIT("is")
896            | otherwise         = ptext SLIT("are")
897     pp_it | sig_tv /= tv = ptext SLIT("It unifies with") <+> quotes (ppr tv) <> comma <+> ptext SLIT("which")
898           | otherwise    = ptext SLIT("It")
899
900     vcat_first :: Int -> [SDoc] -> SDoc
901     vcat_first n []     = empty
902     vcat_first 0 (x:xs) = text "...others omitted..."
903     vcat_first n (x:xs) = x $$ vcat_first (n-1) xs
904
905 unify_msg tv thing = mk_msg tv <+> ptext SLIT("is unified with") <+> quotes thing
906 mk_msg tv          = ptext SLIT("Quantified type variable") <+> quotes (ppr tv)
907 \end{code}
908
909 These two context are used with checkSigTyVars
910     
911 \begin{code}
912 sigCtxt :: Message -> [TcTyVar] -> TcThetaType -> TcTauType
913         -> TidyEnv -> NF_TcM (TidyEnv, Message)
914 sigCtxt when sig_tyvars sig_theta sig_tau tidy_env
915   = zonkTcType sig_tau          `thenNF_Tc` \ actual_tau ->
916     let
917         (env1, tidy_sig_tyvars)  = tidyTyVars tidy_env sig_tyvars
918         (env2, tidy_sig_rho)     = tidyOpenType env1 (mkRhoTy sig_theta sig_tau)
919         (env3, tidy_actual_tau)  = tidyOpenType env2 actual_tau
920         msg = vcat [ptext SLIT("Signature type:    ") <+> pprType (mkForAllTys tidy_sig_tyvars tidy_sig_rho),
921                     ptext SLIT("Type to generalise:") <+> pprType tidy_actual_tau,
922                     when
923                    ]
924     in
925     returnNF_Tc (env3, msg)
926
927 sigPatCtxt bound_tvs bound_ids tidy_env
928   = returnNF_Tc (env1,
929                  sep [ptext SLIT("When checking a pattern that binds"),
930                       nest 4 (vcat (zipWith ppr_id show_ids tidy_tys))])
931   where
932     show_ids = filter is_interesting bound_ids
933     is_interesting id = any (`elemVarSet` idFreeTyVars id) bound_tvs
934
935     (env1, tidy_tys) = tidyOpenTypes tidy_env (map idType show_ids)
936     ppr_id id ty     = ppr id <+> dcolon <+> ppr ty
937         -- Don't zonk the types so we get the separate, un-unified versions
938 \end{code}
939
940
941 %************************************************************************
942 %*                                                                      *
943 \subsection{Errors and contexts}
944 %*                                                                      *
945 %************************************************************************
946
947 \begin{code}
948 tcsigCtxt v   = ptext SLIT("In a type signature for") <+> quotes (ppr v)
949
950 typeKindCtxt :: RenamedHsType -> Message
951 typeKindCtxt ty = sep [ptext SLIT("When checking that"),
952                        nest 2 (quotes (ppr ty)),
953                        ptext SLIT("is a type")]
954
955 appKindCtxt :: SDoc -> Message
956 appKindCtxt pp = ptext SLIT("When checking kinds in") <+> quotes pp
957
958 wrongThingErr expected thing name
959   = pp_thing thing <+> quotes (ppr name) <+> ptext SLIT("used as a") <+> text expected
960   where
961     pp_thing (AGlobal (ATyCon _)) = ptext SLIT("Type constructor")
962     pp_thing (AGlobal (AClass _)) = ptext SLIT("Class")
963     pp_thing (AGlobal (AnId   _)) = ptext SLIT("Identifier")
964     pp_thing (ATyVar _)           = ptext SLIT("Type variable")
965     pp_thing (ATcId _)            = ptext SLIT("Local identifier")
966     pp_thing (AThing _)           = ptext SLIT("Utterly bogus")
967
968 ambigErr pred ty
969   = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
970          nest 4 (ptext SLIT("for the type:") <+> ppr ty),
971          nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
972                  ptext SLIT("must be reachable from the type after the =>"))]
973
974 freeErr pred ty
975   = sep [ptext SLIT("The constraint") <+> quotes (pprPred pred) <+>
976                    ptext SLIT("does not mention any of the universally quantified type variables"),
977          nest 4 (ptext SLIT("in the type") <+> quotes (ppr ty))
978     ]
979
980 polyArgTyErr ty = ptext SLIT("Illegal polymorphic type as argument:")   <+> ppr ty
981 ubxArgTyErr  ty = ptext SLIT("Illegal unboxed tuple type as argument:") <+> ppr ty
982 \end{code}