[project @ 2001-01-25 17:54:24 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, 
8                     tcHsSigType, tcHsLiftedSigType, 
9                     tcRecClassContext, 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                           classesOfPreds, isUnboxedTupleType, isForAllTy
50                         )
51 import PprType          ( pprType, pprPred )
52 import Subst            ( mkTopTyVarSubst, substTy )
53 import CoreFVs          ( idFreeTyVars )
54 import Id               ( mkVanillaId, 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            ( ClassContext, 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@(HsPIParam name ty)
245   = tcAddErrCtxt (appKindCtxt (ppr pred))       $
246     kcLiftedType ty
247
248 kcHsPred pred@(HsPClass 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 tcHsType             ty = tc_type NonRecursive ty  `thenTc` \ ty' ->  returnTc (hoistForAllTys ty')
300 tcHsRecType wimp_out ty = tc_type wimp_out     ty  `thenTc` \ ty' ->  returnTc (hoistForAllTys ty')
301 \end{code}
302
303
304 %************************************************************************
305 %*                                                                      *
306 \subsection{tc_type}
307 %*                                                                      *
308 %************************************************************************
309
310 tc_type, the main work horse
311 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
312
313         -------------------
314         *** BIG WARNING ***
315         -------------------
316
317 tc_type is used to typecheck the types in the RHS of data
318 constructors.  In the case of recursive data types, that means that
319 the type constructors themselves are (partly) black holes.  e.g.
320
321         data T a = MkT a [T a]
322
323 While typechecking the [T a] on the RHS, T itself is not yet fully
324 defined.  That in turn places restrictions on what you can check in
325 tcHsType; if you poke on too much you get a black hole.  I keep
326 forgetting this, hence this warning!
327
328 The wimp_out argument tells when we are in a mutually-recursive
329 group of type declarations, so omit various checks else we
330 get a black hole.  They'll be done again later, in TcTyClDecls.tcGroup.
331
332         --------------------------
333         *** END OF BIG WARNING ***
334         --------------------------
335
336
337 \begin{code}
338 tc_type :: RecFlag -> RenamedHsType -> TcM Type
339
340 tc_type wimp_out ty@(HsTyVar name)
341   = tc_app wimp_out ty []
342
343 tc_type wimp_out (HsListTy ty)
344   = tc_arg_type wimp_out ty     `thenTc` \ tau_ty ->
345     returnTc (mkListTy tau_ty)
346
347 tc_type wimp_out (HsTupleTy (HsTupCon _ boxity arity) tys)
348   = ASSERT( arity == length tys )
349     mapTc tc_tup_arg tys        `thenTc` \ tau_tys ->
350     returnTc (mkTupleTy boxity arity tau_tys)
351   where
352     tc_tup_arg = case boxity of
353                    Boxed   -> tc_arg_type wimp_out
354                    Unboxed -> tc_type     wimp_out 
355         -- Unboxed tuples can have polymorphic or unboxed args.
356         -- This happens in the workers for functions returning
357         -- product types with polymorphic components
358
359 tc_type wimp_out (HsFunTy ty1 ty2)
360   = tc_type wimp_out ty1                        `thenTc` \ tau_ty1 ->
361         -- Function argument can be polymorphic, but
362         -- must not be an unboxed tuple
363     checkTc (not (isUnboxedTupleType tau_ty1))
364             (ubxArgTyErr ty1)                   `thenTc_`
365     tc_type wimp_out ty2                        `thenTc` \ tau_ty2 ->
366     returnTc (mkFunTy tau_ty1 tau_ty2)
367
368 tc_type wimp_out (HsNumTy n)
369   = ASSERT(n== 1)
370     returnTc (mkTyConApp genUnitTyCon [])
371
372 tc_type wimp_out (HsOpTy ty1 op ty2) =
373   tc_arg_type wimp_out ty1 `thenTc` \ tau_ty1 ->
374   tc_arg_type wimp_out ty2 `thenTc` \ tau_ty2 ->
375   tc_fun_type op [tau_ty1,tau_ty2]
376
377 tc_type wimp_out (HsAppTy ty1 ty2)
378   = tc_app wimp_out ty1 [ty2]
379
380 tc_type wimp_out (HsPredTy pred)
381   = tc_pred wimp_out pred       `thenTc` \ pred' ->
382     returnTc (mkPredTy pred')
383
384 tc_type wimp_out full_ty@(HsForAllTy (Just tv_names) ctxt ty)
385   = let
386         kind_check = kcHsContext ctxt `thenTc_` kcHsType ty
387     in
388     tcHsTyVars tv_names kind_check                      $ \ tyvars ->
389     tc_context wimp_out ctxt                            `thenTc` \ theta ->
390
391         -- Context behaves like a function type
392         -- This matters.  Return-unboxed-tuple analysis can
393         -- give overloaded functions like
394         --      f :: forall a. Num a => (# a->a, a->a #)
395         -- And we want these to get through the type checker
396     (if null theta then
397         tc_arg_type wimp_out ty
398      else
399         tc_type wimp_out ty
400     )                                                   `thenTc` \ tau ->
401
402     checkAmbiguity wimp_out is_source tyvars theta tau
403   where
404     is_source = case tv_names of
405                    (UserTyVar _ : _) -> True
406                    other             -> False
407
408
409   -- tc_arg_type checks that the argument of a 
410   -- type appplication isn't a for-all type or an unboxed tuple type
411   -- For example, we want to reject things like:
412   --
413   --    instance Ord a => Ord (forall s. T s a)
414   -- and
415   --    g :: T s (forall b.b)
416   --
417   -- Other unboxed types are very occasionally allowed as type
418   -- arguments depending on the kind of the type constructor
419
420 tc_arg_type wimp_out arg_ty     
421   | isRec wimp_out
422   = tc_type wimp_out arg_ty
423
424   | otherwise
425   = tc_type wimp_out arg_ty                                             `thenTc` \ arg_ty' ->
426     checkTc (not (isForAllTy arg_ty'))         (polyArgTyErr arg_ty)    `thenTc_`
427     checkTc (not (isUnboxedTupleType arg_ty')) (ubxArgTyErr arg_ty)     `thenTc_`
428     returnTc arg_ty'
429
430 tc_arg_types wimp_out arg_tys = mapTc (tc_arg_type wimp_out) arg_tys
431 \end{code}
432
433 Help functions for type applications
434 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
435
436 \begin{code}
437 tc_app :: RecFlag -> RenamedHsType -> [RenamedHsType] -> TcM Type
438 tc_app wimp_out (HsAppTy ty1 ty2) tys
439   = tc_app wimp_out ty1 (ty2:tys)
440
441 tc_app wimp_out ty tys
442   = tcAddErrCtxt (appKindCtxt pp_app)   $
443     tc_arg_types wimp_out tys           `thenTc` \ arg_tys ->
444     case ty of
445         HsTyVar fun -> tc_fun_type fun arg_tys
446         other       -> tc_type wimp_out ty              `thenTc` \ fun_ty ->
447                        returnNF_Tc (mkAppTys fun_ty arg_tys)
448   where
449     pp_app = ppr ty <+> sep (map pprParendHsType tys)
450
451 -- (tc_fun_type ty arg_tys) returns (mkAppTys ty arg_tys)
452 -- But not quite; for synonyms it checks the correct arity, and builds a SynTy
453 --      hence the rather strange functionality.
454
455 tc_fun_type name arg_tys
456   = tcLookup name                       `thenTc` \ thing ->
457     case thing of
458         ATyVar tv -> returnTc (mkAppTys (mkTyVarTy tv) arg_tys)
459
460         AGlobal (ATyCon tc)
461                 | isSynTyCon tc ->  checkTc arity_ok err_msg    `thenTc_`
462                                     returnTc (mkAppTys (mkSynTy tc (take arity arg_tys))
463                                                        (drop arity arg_tys))
464
465                 | otherwise       ->  returnTc (mkTyConApp tc arg_tys)
466                 where
467
468                     arity_ok = arity <= n_args 
469                     arity = tyConArity tc
470                         -- It's OK to have an *over-applied* type synonym
471                         --      data Tree a b = ...
472                         --      type Foo a = Tree [a]
473                         --      f :: Foo a b -> ...
474                     err_msg = arityErr "Type synonym" name arity n_args
475                     n_args  = length arg_tys
476
477         other -> failWithTc (wrongThingErr "type constructor" thing name)
478 \end{code}
479
480
481 Contexts
482 ~~~~~~~~
483 \begin{code}
484 tcRecClassContext :: RecFlag -> RenamedContext -> TcM ClassContext
485         -- Used when we are expecting a ClassContext (i.e. no implicit params)
486 tcRecClassContext wimp_out context
487   = tc_context wimp_out context         `thenTc` \ theta ->
488     returnTc (classesOfPreds theta)
489
490 tc_context :: RecFlag -> RenamedContext -> TcM ThetaType
491 tc_context wimp_out context = mapTc (tc_pred wimp_out) context
492
493 tc_pred wimp_out assn@(HsPClass class_name tys)
494   = tcAddErrCtxt (appKindCtxt (ppr assn))       $
495     tc_arg_types wimp_out tys                   `thenTc` \ arg_tys ->
496     tcLookupGlobal class_name                   `thenTc` \ thing ->
497     case thing of
498         AClass clas -> checkTc (arity == n_tys) err     `thenTc_`
499                        returnTc (Class clas arg_tys)
500             where
501                 arity = classArity clas
502                 n_tys = length tys
503                 err   = arityErr "Class" class_name arity n_tys
504
505         other -> failWithTc (wrongThingErr "class" (AGlobal thing) class_name)
506
507 tc_pred wimp_out assn@(HsPIParam name ty)
508   = tcAddErrCtxt (appKindCtxt (ppr assn))       $
509     tc_arg_type wimp_out ty                     `thenTc` \ arg_ty ->
510     returnTc (IParam name arg_ty)
511 \end{code}
512
513
514 Check for ambiguity
515 ~~~~~~~~~~~~~~~~~~~
516           forall V. P => tau
517 is ambiguous if P contains generic variables
518 (i.e. one of the Vs) that are not mentioned in tau
519
520 However, we need to take account of functional dependencies
521 when we speak of 'mentioned in tau'.  Example:
522         class C a b | a -> b where ...
523 Then the type
524         forall x y. (C x y) => x
525 is not ambiguous because x is mentioned and x determines y
526
527 NOTE: In addition, GHC insists that at least one type variable
528 in each constraint is in V.  So we disallow a type like
529         forall a. Eq b => b -> b
530 even in a scope where b is in scope.
531 This is the is_free test below.
532
533 Notes on the 'is_source_polytype' test above
534 Check ambiguity only for source-program types, not
535 for types coming from inteface files.  The latter can
536 legitimately have ambiguous types. Example
537    class S a where s :: a -> (Int,Int)
538    instance S Char where s _ = (1,1)
539    f:: S a => [a] -> Int -> (Int,Int)
540    f (_::[a]) x = (a*x,b)
541         where (a,b) = s (undefined::a)
542 Here the worker for f gets the type
543         fw :: forall a. S a => Int -> (# Int, Int #)
544
545 If the list of tv_names is empty, we have a monotype,
546 and then we don't need to check for ambiguity either,
547 because the test can't fail (see is_ambig).
548
549 \begin{code}
550 checkAmbiguity :: RecFlag -> Bool
551                -> [TyVar] -> ThetaType -> TauType
552                -> TcM SigmaType
553 checkAmbiguity wimp_out is_source_polytype forall_tyvars theta tau
554   | isRec wimp_out = returnTc sigma_ty
555   | otherwise      = mapTc_ check_pred theta    `thenTc_`
556                      returnTc sigma_ty
557   where
558     sigma_ty          = mkSigmaTy forall_tyvars theta tau
559     tau_vars          = tyVarsOfType tau
560     extended_tau_vars = grow theta tau_vars
561
562     is_ambig ct_var   = (ct_var `elem` forall_tyvars) &&
563                         not (ct_var `elemVarSet` extended_tau_vars)
564     is_free ct_var    = not (ct_var `elem` forall_tyvars)
565     
566     check_pred pred = checkTc (not any_ambig)              (ambigErr pred sigma_ty) `thenTc_`
567                       checkTc (is_ip pred || not all_free) (freeErr  pred sigma_ty)
568              where 
569                 ct_vars   = varSetElems (tyVarsOfPred pred)
570                 all_free  = all is_free ct_vars
571                 any_ambig = is_source_polytype && any is_ambig ct_vars
572                 is_ip (IParam _ _) = True
573                 is_ip _            = False
574 \end{code}
575
576 %************************************************************************
577 %*                                                                      *
578 \subsection{Type variables, with knot tying!}
579 %*                                                                      *
580 %************************************************************************
581
582 \begin{code}
583 mkImmutTyVars :: [(Name,Kind)] -> [TyVar]
584 mkImmutTyVars pairs = [mkTyVar name kind | (name, kind) <- pairs]
585
586 mkTyClTyVars :: Kind                    -- Kind of the tycon or class
587              -> [HsTyVarBndr Name]
588              -> [TyVar]
589 mkTyClTyVars kind tyvar_names
590   = mkImmutTyVars tyvars_w_kinds
591   where
592     (tyvars_w_kinds, _) = zipFunTys (hsTyVarNames tyvar_names) kind
593 \end{code}
594
595
596 %************************************************************************
597 %*                                                                      *
598 \subsection{Signatures}
599 %*                                                                      *
600 %************************************************************************
601
602 @tcSigs@ checks the signatures for validity, and returns a list of
603 {\em freshly-instantiated} signatures.  That is, the types are already
604 split up, and have fresh type variables installed.  All non-type-signature
605 "RenamedSigs" are ignored.
606
607 The @TcSigInfo@ contains @TcTypes@ because they are unified with
608 the variable's type, and after that checked to see whether they've
609 been instantiated.
610
611 \begin{code}
612 data TcSigInfo
613   = TySigInfo       
614         Name                    -- N, the Name in corresponding binding
615
616         TcId                    -- *Polymorphic* binder for this value...
617                                 -- Has name = N
618
619         [TcTyVar]               -- tyvars
620         TcThetaType             -- theta
621         TcTauType               -- tau
622
623         TcId                    -- *Monomorphic* binder for this value
624                                 -- Does *not* have name = N
625                                 -- Has type tau
626
627         [Inst]                  -- Empty if theta is null, or
628                                 -- (method mono_id) otherwise
629
630         SrcLoc                  -- Of the signature
631
632 instance Outputable TcSigInfo where
633     ppr (TySigInfo nm id tyvars theta tau _ inst loc) =
634         ppr nm <+> ptext SLIT("::") <+> ppr tyvars <+> ppr theta <+> ptext SLIT("=>") <+> ppr tau
635
636 maybeSig :: [TcSigInfo] -> Name -> Maybe (TcSigInfo)
637         -- Search for a particular signature
638 maybeSig [] name = Nothing
639 maybeSig (sig@(TySigInfo sig_name _ _ _ _ _ _ _) : sigs) name
640   | name == sig_name = Just sig
641   | otherwise        = maybeSig sigs name
642 \end{code}
643
644
645 \begin{code}
646 tcTySig :: RenamedSig -> TcM TcSigInfo
647
648 tcTySig (Sig v ty src_loc)
649  = tcAddSrcLoc src_loc                          $ 
650    tcAddErrCtxt (tcsigCtxt v)                   $
651    tcHsSigType ty                               `thenTc` \ sigma_tc_ty ->
652    mkTcSig (mkVanillaId v sigma_tc_ty) src_loc  `thenNF_Tc` \ sig -> 
653    returnTc sig
654
655 mkTcSig :: TcId -> SrcLoc -> NF_TcM TcSigInfo
656 mkTcSig poly_id src_loc
657   =     -- Instantiate this type
658         -- It's important to do this even though in the error-free case
659         -- we could just split the sigma_tc_ty (since the tyvars don't
660         -- unified with anything).  But in the case of an error, when
661         -- the tyvars *do* get unified with something, we want to carry on
662         -- typechecking the rest of the program with the function bound
663         -- to a pristine type, namely sigma_tc_ty
664    let
665         (tyvars, rho) = splitForAllTys (idType poly_id)
666    in
667    mapNF_Tc tcInstSigVar tyvars         `thenNF_Tc` \ tyvars' ->
668         -- Make *signature* type variables
669
670    let
671      tyvar_tys' = mkTyVarTys tyvars'
672      rho' = substTy (mkTopTyVarSubst tyvars tyvar_tys') rho
673         -- mkTopTyVarSubst because the tyvars' are fresh
674      (theta', tau') = splitRhoTy rho'
675         -- This splitRhoTy tries hard to make sure that tau' is a type synonym
676         -- wherever possible, which can improve interface files.
677    in
678    newMethodWithGivenTy SignatureOrigin 
679                 poly_id
680                 tyvar_tys'
681                 theta' tau'                     `thenNF_Tc` \ inst ->
682         -- We make a Method even if it's not overloaded; no harm
683         
684    returnNF_Tc (TySigInfo name poly_id tyvars' theta' tau' (instToId inst) [inst] src_loc)
685   where
686     name = idName poly_id
687 \end{code}
688
689
690
691 %************************************************************************
692 %*                                                                      *
693 \subsection{Checking signature type variables}
694 %*                                                                      *
695 %************************************************************************
696
697 @checkSigTyVars@ is used after the type in a type signature has been unified with
698 the actual type found.  It then checks that the type variables of the type signature
699 are
700         (a) Still all type variables
701                 eg matching signature [a] against inferred type [(p,q)]
702                 [then a will be unified to a non-type variable]
703
704         (b) Still all distinct
705                 eg matching signature [(a,b)] against inferred type [(p,p)]
706                 [then a and b will be unified together]
707
708         (c) Not mentioned in the environment
709                 eg the signature for f in this:
710
711                         g x = ... where
712                                         f :: a->[a]
713                                         f y = [x,y]
714
715                 Here, f is forced to be monorphic by the free occurence of x.
716
717         (d) Not (unified with another type variable that is) in scope.
718                 eg f x :: (r->r) = (\y->y) :: forall a. a->r
719             when checking the expression type signature, we find that
720             even though there is nothing in scope whose type mentions r,
721             nevertheless the type signature for the expression isn't right.
722
723             Another example is in a class or instance declaration:
724                 class C a where
725                    op :: forall b. a -> b
726                    op x = x
727             Here, b gets unified with a
728
729 Before doing this, the substitution is applied to the signature type variable.
730
731 We used to have the notion of a "DontBind" type variable, which would
732 only be bound to itself or nothing.  Then points (a) and (b) were 
733 self-checking.  But it gave rise to bogus consequential error messages.
734 For example:
735
736    f = (*)      -- Monomorphic
737
738    g :: Num a => a -> a
739    g x = f x x
740
741 Here, we get a complaint when checking the type signature for g,
742 that g isn't polymorphic enough; but then we get another one when
743 dealing with the (Num x) context arising from f's definition;
744 we try to unify x with Int (to default it), but find that x has already
745 been unified with the DontBind variable "a" from g's signature.
746 This is really a problem with side-effecting unification; we'd like to
747 undo g's effects when its type signature fails, but unification is done
748 by side effect, so we can't (easily).
749
750 So we revert to ordinary type variables for signatures, and try to
751 give a helpful message in checkSigTyVars.
752
753 \begin{code}
754 checkSigTyVars :: [TcTyVar]             -- Universally-quantified type variables in the signature
755                -> TcTyVarSet            -- Tyvars that are free in the type signature
756                                         --      Not necessarily zonked
757                                         --      These should *already* be in the free-in-env set, 
758                                         --      and are used here only to improve the error message
759                -> TcM [TcTyVar]         -- Zonked signature type variables
760
761 checkSigTyVars [] free = returnTc []
762 checkSigTyVars sig_tyvars free_tyvars
763   = zonkTcTyVars sig_tyvars             `thenNF_Tc` \ sig_tys ->
764     tcGetGlobalTyVars                   `thenNF_Tc` \ globals ->
765
766     checkTcM (allDistinctTyVars sig_tys globals)
767              (complain sig_tys globals) `thenTc_`
768
769     returnTc (map (getTyVar "checkSigTyVars") sig_tys)
770
771   where
772     complain sig_tys globals
773       = -- For the in-scope ones, zonk them and construct a map
774         -- from the zonked tyvar to the in-scope one
775         -- If any of the in-scope tyvars zonk to a type, then ignore them;
776         -- that'll be caught later when we back up to their type sig
777         tcGetEnv                                `thenNF_Tc` \ env ->
778         let
779            in_scope_tvs = tcEnvTyVars env
780         in
781         zonkTcTyVars in_scope_tvs               `thenNF_Tc` \ in_scope_tys ->
782         let
783             in_scope_assoc = [ (zonked_tv, in_scope_tv) 
784                              | (z_ty, in_scope_tv) <- in_scope_tys `zip` in_scope_tvs,
785                                Just zonked_tv <- [getTyVar_maybe z_ty]
786                              ]
787             in_scope_env = mkVarEnv in_scope_assoc
788         in
789
790         -- "check" checks each sig tyvar in turn
791         foldlNF_Tc check
792                    (env2, in_scope_env, [])
793                    (tidy_tvs `zip` tidy_tys)    `thenNF_Tc` \ (env3, _, msgs) ->
794
795         failWithTcM (env3, main_msg $$ nest 4 (vcat msgs))
796       where
797         (env1, tidy_tvs) = mapAccumL tidyTyVar emptyTidyEnv sig_tyvars
798         (env2, tidy_tys) = tidyOpenTypes env1 sig_tys
799
800         main_msg = ptext SLIT("Inferred type is less polymorphic than expected")
801
802         check (tidy_env, acc, msgs) (sig_tyvar,ty)
803                 -- sig_tyvar is from the signature;
804                 -- ty is what you get if you zonk sig_tyvar and then tidy it
805                 --
806                 -- acc maps a zonked type variable back to a signature type variable
807           = case getTyVar_maybe ty of {
808               Nothing ->                        -- Error (a)!
809                         returnNF_Tc (tidy_env, acc, unify_msg sig_tyvar (ppr ty) : msgs) ;
810
811               Just tv ->
812
813             case lookupVarEnv acc tv of {
814                 Just sig_tyvar' ->      -- Error (b) or (d)!
815                         returnNF_Tc (tidy_env, acc, unify_msg sig_tyvar (ppr sig_tyvar') : msgs) ;
816
817                 Nothing ->
818
819             if tv `elemVarSet` globals  -- Error (c)! Type variable escapes
820                                         -- The least comprehensible, so put it last
821                         -- Game plan: 
822                         --    a) get the local TcIds from the environment,
823                         --       and pass them to find_globals (they might have tv free)
824                         --    b) similarly, find any free_tyvars that mention tv
825             then   tcGetEnv                                                     `thenNF_Tc` \ ve ->
826                    find_globals tv tidy_env  [] (tcEnvTcIds ve)                 `thenNF_Tc` \ (tidy_env1, globs) ->
827                    find_frees   tv tidy_env1 [] (varSetElems free_tyvars)       `thenNF_Tc` \ (tidy_env2, frees) ->
828                    returnNF_Tc (tidy_env2, acc, escape_msg sig_tyvar tv globs frees : msgs)
829
830             else        -- All OK
831             returnNF_Tc (tidy_env, extendVarEnv acc tv sig_tyvar, msgs)
832             }}
833
834 -- find_globals looks at the value environment and finds values
835 -- whose types mention the offending type variable.  It has to be 
836 -- careful to zonk the Id's type first, so it has to be in the monad.
837 -- We must be careful to pass it a zonked type variable, too.
838
839 find_globals :: Var 
840              -> TidyEnv 
841              -> [(Name,Type)] 
842              -> [Id] 
843              -> NF_TcM (TidyEnv,[(Name,Type)])
844
845 find_globals tv tidy_env acc []
846   = returnNF_Tc (tidy_env, acc)
847
848 find_globals tv tidy_env acc (id:ids) 
849   | isEmptyVarSet (idFreeTyVars id)
850   = find_globals tv tidy_env acc ids
851
852   | otherwise
853   = zonkTcType (idType id)      `thenNF_Tc` \ id_ty ->
854     if tv `elemVarSet` tyVarsOfType id_ty then
855         let 
856            (tidy_env', id_ty') = tidyOpenType tidy_env id_ty
857            acc'                = (idName id, id_ty') : acc
858         in
859         find_globals tv tidy_env' acc' ids
860     else
861         find_globals tv tidy_env  acc  ids
862
863 find_frees tv tidy_env acc []
864   = returnNF_Tc (tidy_env, acc)
865 find_frees tv tidy_env acc (ftv:ftvs)
866   = zonkTcTyVar ftv     `thenNF_Tc` \ ty ->
867     if tv `elemVarSet` tyVarsOfType ty then
868         let
869             (tidy_env', ftv') = tidyTyVar tidy_env ftv
870         in
871         find_frees tv tidy_env' (ftv':acc) ftvs
872     else
873         find_frees tv tidy_env  acc        ftvs
874
875
876 escape_msg sig_tv tv globs frees
877   = mk_msg sig_tv <+> ptext SLIT("escapes") $$
878     if not (null globs) then
879         vcat [pp_it <+> ptext SLIT("is mentioned in the environment"),
880               ptext SLIT("The following variables in the environment mention") <+> quotes (ppr tv),
881               nest 2 (vcat_first 10 [ppr name <+> dcolon <+> ppr ty | (name,ty) <- globs])
882         ]
883      else if not (null frees) then
884         vcat [ptext SLIT("It is reachable from the type variable(s)") <+> pprQuotedList frees,
885               nest 2 (ptext SLIT("which") <+> is_are <+> ptext SLIT("free in the signature"))
886         ]
887      else
888         empty   -- Sigh.  It's really hard to give a good error message
889                 -- all the time.   One bad case is an existential pattern match
890   where
891     is_are | isSingleton frees = ptext SLIT("is")
892            | otherwise         = ptext SLIT("are")
893     pp_it | sig_tv /= tv = ptext SLIT("It unifies with") <+> quotes (ppr tv) <> comma <+> ptext SLIT("which")
894           | otherwise    = ptext SLIT("It")
895
896     vcat_first :: Int -> [SDoc] -> SDoc
897     vcat_first n []     = empty
898     vcat_first 0 (x:xs) = text "...others omitted..."
899     vcat_first n (x:xs) = x $$ vcat_first (n-1) xs
900
901 unify_msg tv thing = mk_msg tv <+> ptext SLIT("is unified with") <+> quotes thing
902 mk_msg tv          = ptext SLIT("Quantified type variable") <+> quotes (ppr tv)
903 \end{code}
904
905 These two context are used with checkSigTyVars
906     
907 \begin{code}
908 sigCtxt :: Message -> [TcTyVar] -> TcThetaType -> TcTauType
909         -> TidyEnv -> NF_TcM (TidyEnv, Message)
910 sigCtxt when sig_tyvars sig_theta sig_tau tidy_env
911   = zonkTcType sig_tau          `thenNF_Tc` \ actual_tau ->
912     let
913         (env1, tidy_sig_tyvars)  = tidyTyVars tidy_env sig_tyvars
914         (env2, tidy_sig_rho)     = tidyOpenType env1 (mkRhoTy sig_theta sig_tau)
915         (env3, tidy_actual_tau)  = tidyOpenType env2 actual_tau
916         msg = vcat [ptext SLIT("Signature type:    ") <+> pprType (mkForAllTys tidy_sig_tyvars tidy_sig_rho),
917                     ptext SLIT("Type to generalise:") <+> pprType tidy_actual_tau,
918                     when
919                    ]
920     in
921     returnNF_Tc (env3, msg)
922
923 sigPatCtxt bound_tvs bound_ids tidy_env
924   = returnNF_Tc (env1,
925                  sep [ptext SLIT("When checking a pattern that binds"),
926                       nest 4 (vcat (zipWith ppr_id show_ids tidy_tys))])
927   where
928     show_ids = filter is_interesting bound_ids
929     is_interesting id = any (`elemVarSet` idFreeTyVars id) bound_tvs
930
931     (env1, tidy_tys) = tidyOpenTypes tidy_env (map idType show_ids)
932     ppr_id id ty     = ppr id <+> dcolon <+> ppr ty
933         -- Don't zonk the types so we get the separate, un-unified versions
934 \end{code}
935
936
937 %************************************************************************
938 %*                                                                      *
939 \subsection{Errors and contexts}
940 %*                                                                      *
941 %************************************************************************
942
943 \begin{code}
944 tcsigCtxt v   = ptext SLIT("In a type signature for") <+> quotes (ppr v)
945
946 typeKindCtxt :: RenamedHsType -> Message
947 typeKindCtxt ty = sep [ptext SLIT("When checking that"),
948                        nest 2 (quotes (ppr ty)),
949                        ptext SLIT("is a type")]
950
951 appKindCtxt :: SDoc -> Message
952 appKindCtxt pp = ptext SLIT("When checking kinds in") <+> quotes pp
953
954 wrongThingErr expected thing name
955   = pp_thing thing <+> quotes (ppr name) <+> ptext SLIT("used as a") <+> text expected
956   where
957     pp_thing (AGlobal (ATyCon _)) = ptext SLIT("Type constructor")
958     pp_thing (AGlobal (AClass _)) = ptext SLIT("Class")
959     pp_thing (AGlobal (AnId   _)) = ptext SLIT("Identifier")
960     pp_thing (ATyVar _)           = ptext SLIT("Type variable")
961     pp_thing (ATcId _)            = ptext SLIT("Local identifier")
962     pp_thing (AThing _)           = ptext SLIT("Utterly bogus")
963
964 ambigErr pred ty
965   = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
966          nest 4 (ptext SLIT("for the type:") <+> ppr ty),
967          nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
968                  ptext SLIT("must be reachable from the type after the =>"))]
969
970 freeErr pred ty
971   = sep [ptext SLIT("The constraint") <+> quotes (pprPred pred) <+>
972                    ptext SLIT("does not mention any of the universally quantified type variables"),
973          nest 4 (ptext SLIT("in the type") <+> quotes (ppr ty))
974     ]
975
976 polyArgTyErr ty = ptext SLIT("Illegal polymorphic type as argument:")   <+> ppr ty
977 ubxArgTyErr  ty = ptext SLIT("Illegal unboxed tuple type as argument:") <+> ppr ty
978 \end{code}