TcMonoType.lhs 28.9 KB
Newer Older
1
%
2
% (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
3
4
5
6
%
\section[TcMonoType]{Typechecking user-specified @MonoTypes@}

\begin{code}
7
module TcMonoType ( tcHsType, tcHsSigType, tcHsBoxedSigType, 
8
		    tcContext, tcClassContext,
9
10
11
12

			-- Kind checking
		    kcHsTyVar, kcHsTyVars, mkTyClTyVars,
		    kcHsType, kcHsSigType, kcHsBoxedSigType, kcHsContext,
13
		    kcTyVarScope, newSigTyVars, mkImmutTyVars,
14

15
		    TcSigInfo(..), tcTySig, mkTcSig, maybeSig,
16
		    checkSigTyVars, sigCtxt, sigPatCtxt
17
	          ) where
18

19
#include "HsVersions.h"
20

21
import HsSyn		( HsType(..), HsTyVarBndr(..), HsUsageAnn(..),
22
23
                          Sig(..), HsPred(..), pprParendHsType, HsTupCon(..), hsTyVarNames )
import RnHsSyn		( RenamedHsType, RenamedHsPred, RenamedContext, RenamedSig )
24
import TcHsSyn		( TcId )
25

26
import TcMonad
27
import TcEnv		( tcExtendTyVarEnv, tcLookupTy, tcGetValueEnv, tcGetInScopeTyVars,
28
                          tcExtendUVarEnv, tcLookupUVar,
29
30
			  tcGetGlobalTyVars, valueEnvIds, 
		 	  TyThing(..), tyThingKind, tcExtendKindEnv
31
			)
32
import TcType		( TcType, TcKind, TcTyVar, TcThetaType, TcTauType,
33
			  newKindVar, tcInstSigVar,
34
			  zonkKindEnv, zonkTcType, zonkTcTyVars, zonkTcTyVar
35
			)
36
37
38
import Inst		( Inst, InstOrigin(..), newMethodWithGivenTy, instToIdBndr,
			  instFunDeps, instFunDepsOfTheta )
import FunDeps		( tyVarFunDep, oclose )
39
40
import TcUnify		( unifyKind, unifyKinds, unifyOpenTypeKind )
import Type		( Type, Kind, PredType(..), ThetaType, UsageAnn(..),
41
			  mkTyVarTy, mkTyVarTys, mkFunTy, mkSynTy, mkUsgTy,
42
                          mkUsForAllTy, zipFunTys, hoistForAllTys,
43
			  mkSigmaTy, mkDictTy, mkPredTy, mkTyConApp,
44
			  mkAppTys, splitForAllTys, splitRhoTy, mkRhoTy,
45
46
			  boxedTypeKind, unboxedTypeKind, mkArrowKind,
			  mkArrowKinds, getTyVar_maybe, getTyVar, splitFunTy_maybe,
47
		  	  tidyOpenType, tidyOpenTypes, tidyTyVar, tidyTyVars,
48
49
			  tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, mkForAllTys,
			  classesOfPreds
50
			)
51
import PprType		( pprConstraint, pprType, pprPred )
52
53
import Subst		( mkTopTyVarSubst, substTy )
import Id		( mkVanillaId, idName, idType, idFreeTyVars )
54
import Var		( TyVar, mkTyVar, tyVarKind, mkNamedUVar, varName )
55
56
import VarEnv
import VarSet
57
import ErrUtils		( Message )
58
59
import TyCon		( TyCon, isSynTyCon, tyConArity, tyConKind )
import Class		( ClassContext, classArity, classTyCon )
60
import Name		( Name, OccName, isLocallyDefined )
61
import TysWiredIn	( mkListTy, mkTupleTy )
62
import UniqFM		( elemUFM, foldUFM )
63
import BasicTypes	( Boxity(..) )
64
import SrcLoc		( SrcLoc )
65
import Util		( mapAccumL, isSingleton, removeDups )
66
import Outputable
67
68
\end{code}

69

70
71
%************************************************************************
%*									*
72
\subsection{Kind checking}
73
74
75
%*									*
%************************************************************************

76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
Kind checking
~~~~~~~~~~~~~
When we come across the binding site for some type variables, we
proceed in two stages

1. Figure out what kind each tyvar has

2. Create suitably-kinded tyvars, 
   extend the envt, 
   and typecheck the body

To do step 1, we proceed thus:

1a. Bind each type variable to a kind variable
1b. Apply the kind checker
1c. Zonk the resulting kinds

The kind checker is passed to kcTyVarScope as an argument.  

For example, when we find
	(forall a m. m a -> m a)
we bind a,m to kind varibles and kind-check (m a -> m a).  This
makes a get kind *, and m get kind *->*.  Now we typecheck (m a -> m a)
in an environment that binds a and m suitably.

The kind checker passed to kcTyVarScope needs to look at enough to
establish the kind of the tyvar:
  * For a group of type and class decls, it's just the group, not
	the rest of the program
  * For a tyvar bound in a pattern type signature, its the types
	mentioned in the other type signatures in that bunch of patterns
  * For a tyvar bound in a RULE, it's the type signatures on other
	universally quantified variables in the rule

Note that this may occasionally give surprising results.  For example:

	data T a b = MkT (a b)

Here we deduce			a::*->*, b::*.
But equally valid would be
				a::(*->*)-> *, b::*->*

118
\begin{code}
119
120
121
122
123
124
125
126
kcTyVarScope :: [HsTyVarBndr Name] 
	     -> TcM s a				-- The kind checker
	     -> TcM s [(Name,Kind)]
	-- Do a kind check to find out the kinds of the type variables
	-- Then return a bunch of name-kind pairs, from which to 
	-- construct the type variables.  We don't return the tyvars
	-- themselves because sometimes we want mutable ones and 
	-- sometimes we want immutable ones.
127

128
129
130
131
132
133
134
135
136
137
138
kcTyVarScope [] kind_check = returnTc []
	-- A useful short cut for a common case!
  
kcTyVarScope tv_names kind_check 
  = kcHsTyVars tv_names 				`thenNF_Tc` \ tv_names_w_kinds ->
    tcExtendKindEnv tv_names_w_kinds kind_check		`thenTc_`
    zonkKindEnv tv_names_w_kinds
\end{code}
    

\begin{code}
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
kcHsTyVar  :: HsTyVarBndr name   -> NF_TcM s (name, TcKind)
kcHsTyVars :: [HsTyVarBndr name] -> NF_TcM s [(name, TcKind)]

kcHsTyVar (UserTyVar name)       = newKindVar	`thenNF_Tc` \ kind ->
				   returnNF_Tc (name, kind)
kcHsTyVar (IfaceTyVar name kind) = returnNF_Tc (name, kind)

kcHsTyVars tvs = mapNF_Tc kcHsTyVar tvs

---------------------------
kcBoxedType :: RenamedHsType -> TcM s ()
	-- The type ty must be a *boxed* *type*
kcBoxedType ty
  = kcHsType ty				`thenTc` \ kind ->
    tcAddErrCtxt (typeKindCtxt ty)	$
    unifyKind boxedTypeKind kind
    
---------------------------
kcTypeType :: RenamedHsType -> TcM s ()
	-- The type ty must be a *type*, but it can be boxed or unboxed.
kcTypeType ty
  = kcHsType ty				`thenTc` \ kind ->
    tcAddErrCtxt (typeKindCtxt ty)	$
    unifyOpenTypeKind kind

---------------------------
kcHsSigType, kcHsBoxedSigType :: RenamedHsType -> TcM s ()
	-- Used for type signatures
kcHsSigType  	 = kcTypeType
kcHsBoxedSigType = kcBoxedType

---------------------------
kcHsType :: RenamedHsType -> TcM s TcKind
kcHsType (HsTyVar name)	      
  = tcLookupTy name	`thenTc` \ thing ->
    case thing of
	ATyVar tv -> returnTc (tyVarKind tv)
	ATyCon tc -> returnTc (tyConKind tc)
	AThing k  -> returnTc k
	other	  -> failWithTc (wrongThingErr "type" thing name)

kcHsType (HsUsgTy _ ty)       = kcHsType ty
kcHsType (HsUsgForAllTy _ ty) = kcHsType ty

kcHsType (HsListTy ty)
  = kcBoxedType ty		`thenTc` \ tau_ty ->
    returnTc boxedTypeKind

kcHsType (HsTupleTy (HsTupCon _ Boxed) tys)
  = mapTc kcBoxedType tys	`thenTc_` 
    returnTc boxedTypeKind

kcHsType (HsTupleTy (HsTupCon _ Unboxed) tys)
  = mapTc kcTypeType tys	`thenTc_` 
    returnTc unboxedTypeKind

kcHsType (HsFunTy ty1 ty2)
  = kcTypeType ty1	`thenTc_`
    kcTypeType ty2	`thenTc_`
    returnTc boxedTypeKind

kcHsType (HsPredTy pred)
  = kcHsPred pred		`thenTc_`
    returnTc boxedTypeKind

kcHsType ty@(HsAppTy ty1 ty2)
  = kcHsType ty1		`thenTc` \ tc_kind ->
    kcHsType ty2		`thenTc` \ arg_kind ->

    tcAddErrCtxt (appKindCtxt (ppr ty))	$
    case splitFunTy_maybe tc_kind of 
	Just (arg_kind', res_kind)
		-> unifyKind arg_kind arg_kind'	`thenTc_`
		   returnTc res_kind

	Nothing -> newKindVar 						`thenNF_Tc` \ res_kind ->
		   unifyKind tc_kind (mkArrowKind arg_kind res_kind)	`thenTc_`
		   returnTc res_kind

kcHsType (HsForAllTy (Just tv_names) context ty)
  = kcHsTyVars tv_names			`thenNF_Tc` \ kind_env ->
    tcExtendKindEnv kind_env		$
    kcHsContext context		`thenTc_`
    kcHsType ty			`thenTc` \ kind ->
 
		-- Context behaves like a function type
		-- This matters.  Return-unboxed-tuple analysis can
		-- give overloaded functions like
		--	f :: forall a. Num a => (# a->a, a->a #)
		-- And we want these to get through the type checker
    returnTc (if null context then
		 kind
	      else
		  boxedTypeKind)

---------------------------
kcHsContext ctxt = mapTc_ kcHsPred ctxt

kcHsPred :: RenamedHsPred -> TcM s ()
kcHsPred pred@(HsPIParam name ty)
  = tcAddErrCtxt (appKindCtxt (ppr pred))	$
    kcBoxedType ty

kcHsPred pred@(HsPClass cls tys)
  = tcAddErrCtxt (appKindCtxt (ppr pred))	$
    tcLookupTy cls 				`thenNF_Tc` \ thing -> 
    (case thing of
	AClass cls  -> returnTc (tyConKind (classTyCon cls))
	AThing kind -> returnTc kind
	other -> failWithTc (wrongThingErr "class" thing cls))	`thenTc` \ kind ->
    mapTc kcHsType tys						`thenTc` \ arg_kinds ->
    unifyKind kind (mkArrowKinds arg_kinds boxedTypeKind)
\end{code}

253
254
255
256
257
258
%************************************************************************
%*									*
\subsection{Checking types}
%*									*
%************************************************************************

259
260
tcHsSigType and tcHsBoxedSigType
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
261

262
tcHsSigType and tcHsBoxedSigType are used for type signatures written by the programmer
263

264
  * We hoist any inner for-alls to the top
265

266
267
268
269
270
271
  * Notice that we kind-check first, because the type-check assumes
	that the kinds are already checked.
  * They are only called when there are no kind vars in the environment
  	so the kind returned is indeed a Kind not a TcKind

\begin{code}
272
273
tcHsSigType :: RenamedHsType -> TcM s TcType
tcHsSigType ty
274
275
  = kcTypeType ty	`thenTc_`
    tcHsType ty		`thenTc` \ ty' ->
276
277
    returnTc (hoistForAllTys ty')

278
279
280
281
282
tcHsBoxedSigType :: RenamedHsType -> TcM s Type
tcHsBoxedSigType ty
  = kcBoxedType ty	`thenTc_`
    tcHsType ty		`thenTc` \ ty' ->
    returnTc (hoistForAllTys ty')
283
284
\end{code}

285

286
287
tcHsType, the main work horse
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
288

289
\begin{code}
290
291
tcHsType :: RenamedHsType -> TcM s Type
tcHsType ty@(HsTyVar name)
292
  = tc_app ty []
293

294
295
296
tcHsType (HsListTy ty)
  = tcHsType ty		`thenTc` \ tau_ty ->
    returnTc (mkListTy tau_ty)
297

298
299
300
tcHsType (HsTupleTy (HsTupCon _ boxity) tys)
  = mapTc tcHsType tys	`thenTc` \ tau_tys ->
    returnTc (mkTupleTy boxity (length tys) tau_tys)
301

302
303
304
305
tcHsType (HsFunTy ty1 ty2)
  = tcHsType ty1	`thenTc` \ tau_ty1 ->
    tcHsType ty2	`thenTc` \ tau_ty2 ->
    returnTc (mkFunTy tau_ty1 tau_ty2)
306

307
tcHsType (HsAppTy ty1 ty2)
308
  = tc_app ty1 [ty2]
309

310
tcHsType (HsPredTy pred)
311
  = tcClassAssertion True pred	`thenTc` \ pred' ->
312
    returnTc (mkPredTy pred')
313

314
315
316
317
tcHsType (HsUsgTy usg ty)
  = newUsg usg			`thenTc` \ usg' ->
    tcHsType ty			`thenTc` \ tc_ty ->
    returnTc (mkUsgTy usg' tc_ty)
318
319
  where
    newUsg usg = case usg of
320
321
322
                   HsUsOnce        -> returnTc UsOnce
                   HsUsMany        -> returnTc UsMany
                   HsUsVar uv_name -> tcLookupUVar uv_name `thenTc` \ uv ->
323
                                      returnTc (UsVar uv)
324

325
tcHsType (HsUsgForAllTy uv_name ty)
326
327
328
329
  = let
        uv = mkNamedUVar uv_name
    in
    tcExtendUVarEnv uv_name uv $
330
331
    tcHsType ty                     `thenTc` \ tc_ty ->
    returnTc (mkUsForAllTy uv tc_ty)
332

333
334
335
336
337
tcHsType full_ty@(HsForAllTy (Just tv_names) ctxt ty)
  = kcTyVarScope tv_names 
		 (kcHsContext ctxt `thenTc_` kcHsType ty)  `thenTc` \ tv_kinds ->
    let
	forall_tyvars = mkImmutTyVars tv_kinds
338
339
    in
    tcExtendTyVarEnv forall_tyvars	$
340
    tcContext ctxt			`thenTc` \ theta ->
341
    tcHsType ty				`thenTc` \ tau ->
342
    let
343
344
345
346
347
348
349
350
351
352
353
354
	-- Check for ambiguity
	--   forall V. P => tau
	-- is ambiguous if P contains generic variables
	-- (i.e. one of the Vs) that are not mentioned in tau
	--
	-- However, we need to take account of functional dependencies
	-- when we speak of 'mentioned in tau'.  Example:
	--	class C a b | a -> b where ...
	-- Then the type
	--	forall x y. (C x y) => x
	-- is not ambiguous because x is mentioned and x determines y
	--
355
	-- NOTE: In addition, GHC insists that at least one type variable
356
357
358
	-- in each constraint is in V.  So we disallow a type like
	--	forall a. Eq b => b -> b
	-- even in a scope where b is in scope.
359
	-- This is the is_free test below.
360
361
362
363
364

	tau_vars	    = tyVarsOfType tau
	fds		    = instFunDepsOfTheta theta
	tvFundep	    = tyVarFunDep fds
	extended_tau_vars   = oclose tvFundep tau_vars
365
	is_ambig ct_var	    = (ct_var `elem` forall_tyvars) &&
366
			      not (ct_var `elemUFM` extended_tau_vars)
367
	is_free ct_var	    = not (ct_var `elem` forall_tyvars)
368

369
370
	check_pred pred = checkTc (not any_ambig) (ambigErr pred full_ty) `thenTc_`
			  checkTc (not all_free)  (freeErr  pred full_ty)
371
372
	      where 
		ct_vars	  = varSetElems (tyVarsOfPred pred)
373
		any_ambig = is_source_polytype && any is_ambig ct_vars
374
		all_free  = all is_free  ct_vars
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392

	-- Check ambiguity only for source-program types, not
	-- for types coming from inteface files.  The latter can
	-- legitimately have ambiguous types. Example
	--    class S a where s :: a -> (Int,Int)
	--    instance S Char where s _ = (1,1)
	--    f:: S a => [a] -> Int -> (Int,Int)
	--    f (_::[a]) x = (a*x,b)
	--	where (a,b) = s (undefined::a)
	-- Here the worker for f gets the type
	--	fw :: forall a. S a => Int -> (# Int, Int #)
	--
	-- If the list of tv_names is empty, we have a monotype,
	-- and then we don't need to check for ambiguity either,
	-- because the test can't fail (see is_ambig).
	is_source_polytype = case tv_names of
				(UserTyVar _ : _) -> True
				other		  -> False
393
    in
394
    mapTc check_pred theta		`thenTc_`
395
    returnTc (mkSigmaTy forall_tyvars theta tau)
396
\end{code}
397

398
399
Help functions for type applications
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
400

401
\begin{code}
402
tc_app (HsAppTy ty1 ty2) tys
403
  = tc_app ty1 (ty2:tys)
404

405
406
tc_app ty tys
  = tcAddErrCtxt (appKindCtxt pp_app)	$
407
408
    mapTc tcHsType tys			`thenTc` \ arg_tys ->
    tc_fun_type ty arg_tys
409
410
  where
    pp_app = ppr ty <+> sep (map pprParendHsType tys)
411

412
-- (tc_fun_type ty arg_tys) returns (mkAppTys ty arg_tys)
413
414
415
-- But not quite; for synonyms it checks the correct arity, and builds a SynTy
-- 	hence the rather strange functionality.

416
tc_fun_type (HsTyVar name) arg_tys
417
  = tcLookupTy name			`thenTc` \ thing ->
418
    case thing of
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
	ATyVar tv -> returnTc (mkAppTys (mkTyVarTy tv) arg_tys)

	ATyCon tc | isSynTyCon tc ->  checkTc arity_ok err_msg	`thenTc_`
				      returnTc (mkAppTys (mkSynTy tc (take arity arg_tys))
							 (drop arity arg_tys))

		  | otherwise	  ->  returnTc (mkTyConApp tc arg_tys)
		  where

		    arity_ok = arity <= n_args 
		    arity = tyConArity tc
			-- It's OK to have an *over-applied* type synonym
			--	data Tree a b = ...
			--	type Foo a = Tree [a]
			--	f :: Foo a b -> ...
434
		    err_msg = arityErr "Type synonym" name arity n_args
435
436
437
		    n_args  = length arg_tys

	other -> failWithTc (wrongThingErr "type constructor" thing name)
438
439

tc_fun_type ty arg_tys
440
441
  = tcHsType ty		`thenTc` \ fun_ty ->
    returnNF_Tc (mkAppTys fun_ty arg_tys)
442
443
444
\end{code}


445
446
447
Contexts
~~~~~~~~
\begin{code}
448
449
450
451
452
tcClassContext :: RenamedContext -> TcM s ClassContext
	-- Used when we are expecting a ClassContext (i.e. no implicit params)
tcClassContext context
  = tcContext context 	`thenTc` \ theta ->
    returnTc (classesOfPreds theta)
453
454

tcContext :: RenamedContext -> TcM s ThetaType
455
456
457
458
tcContext context = mapTc (tcClassAssertion False) context

tcClassAssertion ccall_ok assn@(HsPClass class_name tys)
  = tcAddErrCtxt (appKindCtxt (ppr assn))	$
459
460
    mapTc tcHsType tys				`thenTc` \ arg_tys ->
    tcLookupTy class_name			`thenTc` \ thing ->
461
    case thing of
462
463
	AClass clas -> checkTc (arity == n_tys) err				`thenTc_`
		       returnTc (Class clas arg_tys)
464
	    where
465
		arity = classArity clas
466
467
		n_tys = length tys
		err   = arityErr "Class" class_name arity n_tys
468
469

	other -> failWithTc (wrongThingErr "class" thing class_name)
470
471
472

tcClassAssertion ccall_ok assn@(HsPIParam name ty)
  = tcAddErrCtxt (appKindCtxt (ppr assn))	$
473
    tcHsType ty					`thenTc` \ arg_ty ->
474
    returnTc (IParam name arg_ty)
475
476
477
\end{code}


478
479
480
481
482
483
%************************************************************************
%*									*
\subsection{Type variables, with knot tying!}
%*									*
%************************************************************************

484
\begin{code}
485
486
487
488
489
mkImmutTyVars :: [(Name,Kind)] -> [TyVar]
newSigTyVars  :: [(Name,Kind)] -> NF_TcM s [TcTyVar]

mkImmutTyVars pairs = [mkTyVar name kind | (name, kind) <- pairs]
newSigTyVars  pairs = listNF_Tc [tcNewSigTyVar name kind | (name,kind) <- pairs]
490
491
492
493
494

mkTyClTyVars :: Kind 			-- Kind of the tycon or class
	     -> [HsTyVarBndr Name]
	     -> [TyVar]
mkTyClTyVars kind tyvar_names
495
  = mkImmutTyVars tyvars_w_kinds
496
  where
497
    (tyvars_w_kinds, _) = zipFunTys (hsTyVarNames tyvar_names) kind
498
499
\end{code}

500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516

%************************************************************************
%*									*
\subsection{Signatures}
%*									*
%************************************************************************

@tcSigs@ checks the signatures for validity, and returns a list of
{\em freshly-instantiated} signatures.  That is, the types are already
split up, and have fresh type variables installed.  All non-type-signature
"RenamedSigs" are ignored.

The @TcSigInfo@ contains @TcTypes@ because they are unified with
the variable's type, and after that checked to see whether they've
been instantiated.

\begin{code}
517
data TcSigInfo
518
519
520
  = TySigInfo	    
	Name			-- N, the Name in corresponding binding

521
	TcId			-- *Polymorphic* binder for this value...
522
523
				-- Has name = N

524
525
526
	[TcTyVar]		-- tyvars
	TcThetaType		-- theta
	TcTauType		-- tau
527

528
	TcId			-- *Monomorphic* binder for this value
529
530
531
				-- Does *not* have name = N
				-- Has type tau

532
	[Inst]			-- Empty if theta is null, or
533
534
535
536
				-- (method mono_id) otherwise

	SrcLoc			-- Of the signature

537
538
539
instance Outputable TcSigInfo where
    ppr (TySigInfo nm id tyvars theta tau _ inst loc) =
	ppr nm <+> ptext SLIT("::") <+> ppr tyvars <+> ppr theta <+> ptext SLIT("=>") <+> ppr tau
540

541
maybeSig :: [TcSigInfo] -> Name -> Maybe (TcSigInfo)
542
543
544
545
546
547
548
549
550
	-- Search for a particular signature
maybeSig [] name = Nothing
maybeSig (sig@(TySigInfo sig_name _ _ _ _ _ _ _) : sigs) name
  | name == sig_name = Just sig
  | otherwise	     = maybeSig sigs name
\end{code}


\begin{code}
551
tcTySig :: RenamedSig -> TcM s TcSigInfo
552
553

tcTySig (Sig v ty src_loc)
554
555
 = tcAddSrcLoc src_loc				$ 
   tcAddErrCtxt (tcsigCtxt v) 			$
556
   tcHsSigType ty				`thenTc` \ sigma_tc_ty ->
557
   mkTcSig (mkVanillaId v sigma_tc_ty) src_loc	`thenNF_Tc` \ sig -> 
558
559
   returnTc sig

560
mkTcSig :: TcId -> SrcLoc -> NF_TcM s TcSigInfo
561
562
563
564
565
566
567
568
569
mkTcSig poly_id src_loc
  = 	-- Instantiate this type
	-- It's important to do this even though in the error-free case
	-- we could just split the sigma_tc_ty (since the tyvars don't
	-- unified with anything).  But in the case of an error, when
	-- the tyvars *do* get unified with something, we want to carry on
	-- typechecking the rest of the program with the function bound
	-- to a pristine type, namely sigma_tc_ty
   let
570
571
572
573
574
575
576
	(tyvars, rho) = splitForAllTys (idType poly_id)
   in
   mapNF_Tc tcInstSigVar tyvars		`thenNF_Tc` \ tyvars' ->
	-- Make *signature* type variables

   let
     tyvar_tys' = mkTyVarTys tyvars'
577
578
     rho' = substTy (mkTopTyVarSubst tyvars tyvar_tys') rho
	-- mkTopTyVarSubst because the tyvars' are fresh
579
580
     (theta', tau') = splitRhoTy rho'
	-- This splitRhoTy tries hard to make sure that tau' is a type synonym
581
582
583
	-- wherever possible, which can improve interface files.
   in
   newMethodWithGivenTy SignatureOrigin 
584
		poly_id
585
586
		tyvar_tys'
		theta' tau'			`thenNF_Tc` \ inst ->
587
	-- We make a Method even if it's not overloaded; no harm
588
   instFunDeps SignatureOrigin theta'		`thenNF_Tc` \ fds ->
589
	
590
   returnNF_Tc (TySigInfo name poly_id tyvars' theta' tau' (instToIdBndr inst) (inst : fds) src_loc)
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
  where
    name = idName poly_id
\end{code}



%************************************************************************
%*									*
\subsection{Checking signature type variables}
%*									*
%************************************************************************

@checkSigTyVars@ is used after the type in a type signature has been unified with
the actual type found.  It then checks that the type variables of the type signature
are
606
	(a) Still all type variables
607
608
609
		eg matching signature [a] against inferred type [(p,q)]
		[then a will be unified to a non-type variable]

610
	(b) Still all distinct
611
612
613
		eg matching signature [(a,b)] against inferred type [(p,p)]
		[then a and b will be unified together]

614
	(c) Not mentioned in the environment
615
616
617
618
619
620
621
622
		eg the signature for f in this:

			g x = ... where
					f :: a->[a]
					f y = [x,y]

		Here, f is forced to be monorphic by the free occurence of x.

623
624
625
626
627
628
629
630
631
632
633
634
	(d) Not (unified with another type variable that is) in scope.
		eg f x :: (r->r) = (\y->y) :: forall a. a->r
	    when checking the expression type signature, we find that
	    even though there is nothing in scope whose type mentions r,
	    nevertheless the type signature for the expression isn't right.

	    Another example is in a class or instance declaration:
		class C a where
		   op :: forall b. a -> b
		   op x = x
	    Here, b gets unified with a

635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
Before doing this, the substitution is applied to the signature type variable.

We used to have the notion of a "DontBind" type variable, which would
only be bound to itself or nothing.  Then points (a) and (b) were 
self-checking.  But it gave rise to bogus consequential error messages.
For example:

   f = (*)	-- Monomorphic

   g :: Num a => a -> a
   g x = f x x

Here, we get a complaint when checking the type signature for g,
that g isn't polymorphic enough; but then we get another one when
dealing with the (Num x) context arising from f's definition;
we try to unify x with Int (to default it), but find that x has already
been unified with the DontBind variable "a" from g's signature.
This is really a problem with side-effecting unification; we'd like to
undo g's effects when its type signature fails, but unification is done
by side effect, so we can't (easily).

So we revert to ordinary type variables for signatures, and try to
give a helpful message in checkSigTyVars.

\begin{code}
660
661
662
663
checkSigTyVars :: [TcTyVar]		-- Universally-quantified type variables in the signature
	       -> TcTyVarSet		-- Tyvars that are free in the type signature
					-- These should *already* be in the global-var set, and are
					-- used here only to improve the error message
664
	       -> TcM s [TcTyVar]	-- Zonked signature type variables
665

666
checkSigTyVars [] free = returnTc []
667

668
checkSigTyVars sig_tyvars free_tyvars
669
670
  = zonkTcTyVars sig_tyvars		`thenNF_Tc` \ sig_tys ->
    tcGetGlobalTyVars			`thenNF_Tc` \ globals ->
671

672
673
674
675
676
677
678
679
680
681
682
683
684
685
    checkTcM (all_ok sig_tys globals)
	     (complain sig_tys globals)	`thenTc_`

    returnTc (map (getTyVar "checkSigTyVars") sig_tys)

  where
    all_ok []       acc = True
    all_ok (ty:tys) acc = case getTyVar_maybe ty of
			    Nothing 		          -> False	-- Point (a)
			    Just tv | tv `elemVarSet` acc -> False	-- Point (b) or (c)
				    | otherwise           -> all_ok tys (acc `extendVarSet` tv)
    

    complain sig_tys globals
686
687
688
689
690
691
692
693
694
695
696
697
698
      = -- For the in-scope ones, zonk them and construct a map
	-- from the zonked tyvar to the in-scope one
	-- If any of the in-scope tyvars zonk to a type, then ignore them;
	-- that'll be caught later when we back up to their type sig
	tcGetInScopeTyVars			`thenNF_Tc` \ in_scope_tvs ->
	zonkTcTyVars in_scope_tvs		`thenNF_Tc` \ in_scope_tys ->
	let
	    in_scope_assoc = [ (zonked_tv, in_scope_tv) 
			     | (z_ty, in_scope_tv) <- in_scope_tys `zip` in_scope_tvs,
			       Just zonked_tv <- [getTyVar_maybe z_ty]
    			     ]
	    in_scope_env = mkVarEnv in_scope_assoc
	in
699

700
701
702
703
	-- "check" checks each sig tyvar in turn
        foldlNF_Tc check
		   (env2, in_scope_env, [])
		   (tidy_tvs `zip` tidy_tys)	`thenNF_Tc` \ (env3, _, msgs) ->
704

705
706
707
708
        failWithTcM (env3, main_msg $$ nest 4 (vcat msgs))
      where
	(env1, tidy_tvs) = mapAccumL tidyTyVar emptyTidyEnv sig_tyvars
	(env2, tidy_tys) = tidyOpenTypes env1 sig_tys
709

710
	main_msg = ptext SLIT("Inferred type is less polymorphic than expected")
711

712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
	check (env, acc, msgs) (sig_tyvar,ty)
		-- sig_tyvar is from the signature;
		-- ty is what you get if you zonk sig_tyvar and then tidy it
		--
		-- acc maps a zonked type variable back to a signature type variable
	  = case getTyVar_maybe ty of {
	      Nothing ->			-- Error (a)!
			returnNF_Tc (env, acc, unify_msg sig_tyvar (ppr ty) : msgs) ;

	      Just tv ->

	    case lookupVarEnv acc tv of {
		Just sig_tyvar' -> 	-- Error (b) or (d)!
			returnNF_Tc (env, acc, unify_msg sig_tyvar (ppr sig_tyvar') : msgs) ;

		Nothing ->

	    if tv `elemVarSet` globals	-- Error (c)! Type variable escapes
					-- The least comprehensible, so put it last
731
732
733
734
	    then   tcGetValueEnv 					`thenNF_Tc` \ ve ->
        	   find_globals tv env  [] (valueEnvIds ve)		`thenNF_Tc` \ (env1, globs) ->
        	   find_frees   tv env1 [] (varSetElems free_tyvars)	`thenNF_Tc` \ (env2, frees) ->
		   returnNF_Tc (env2, acc, escape_msg sig_tyvar tv globs frees : msgs)
735
736
737
738
739
740
741
742
743

	    else 	-- All OK
	    returnNF_Tc (env, extendVarEnv acc tv sig_tyvar, msgs)
	    }}

-- find_globals looks at the value environment and finds values
-- whose types mention the offending type variable.  It has to be 
-- careful to zonk the Id's type first, so it has to be in the monad.
-- We must be careful to pass it a zonked type variable, too.
744
745
find_globals tv tidy_env acc []
  = returnNF_Tc (tidy_env, acc)
746

747
find_globals tv tidy_env acc (id:ids) 
748
749
  | not (isLocallyDefined id) ||
    isEmptyVarSet (idFreeTyVars id)
750
  = find_globals tv tidy_env acc ids
751

752
753
754
755
756
  | otherwise
  = zonkTcType (idType id)	`thenNF_Tc` \ id_ty ->
    if tv `elemVarSet` tyVarsOfType id_ty then
    	let 
    	   (tidy_env', id_ty') = tidyOpenType tidy_env id_ty
757
	   acc'		       = (idName id, id_ty') : acc
758
    	in
759
    	find_globals tv tidy_env' acc' ids
760
    else
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
    	find_globals tv tidy_env  acc  ids

find_frees tv tidy_env acc []
  = returnNF_Tc (tidy_env, acc)
find_frees tv tidy_env acc (ftv:ftvs)
  = zonkTcTyVar ftv	`thenNF_Tc` \ ty ->
    if tv `elemVarSet` tyVarsOfType ty then
	let
	    (tidy_env', ftv') = tidyTyVar tidy_env ftv
	in
	find_frees tv tidy_env' (ftv':acc) ftvs
    else
	find_frees tv tidy_env  acc        ftvs


escape_msg sig_tv tv globs frees
  = mk_msg sig_tv <+> ptext SLIT("escapes") $$
    if not (null globs) then
	vcat [pp_it <+> ptext SLIT("is mentioned in the environment"),
	      ptext SLIT("The following variables in the environment mention") <+> quotes (ppr tv),
	      nest 2 (vcat_first 10 [ppr name <+> dcolon <+> ppr ty | (name,ty) <- globs])
	]
     else if not (null frees) then
	vcat [ptext SLIT("It is reachable from the type variable(s)") <+> pprQuotedList frees,
	      nest 2 (ptext SLIT("which") <+> is_are <+> ptext SLIT("free in the signature"))
	]
     else
	empty	-- Sigh.  It's really hard to give a good error message
		-- all the time.   One bad case is an existential pattern match
790
  where
791
792
793
794
    is_are | isSingleton frees = ptext SLIT("is")
	   | otherwise         = ptext SLIT("are")
    pp_it | sig_tv /= tv = ptext SLIT("It unifies with") <+> quotes (ppr tv) <> comma <+> ptext SLIT("which")
	  | otherwise    = ptext SLIT("It")
795

sof's avatar
sof committed
796
    vcat_first :: Int -> [SDoc] -> SDoc
797
798
799
    vcat_first n []     = empty
    vcat_first 0 (x:xs) = text "...others omitted..."
    vcat_first n (x:xs) = x $$ vcat_first (n-1) xs
800
801
802
803
804
805
806
807

unify_msg tv thing = mk_msg tv <+> ptext SLIT("is unified with") <+> quotes thing
mk_msg tv          = ptext SLIT("Quantified type variable") <+> quotes (ppr tv)
\end{code}

These two context are used with checkSigTyVars
    
\begin{code}
808
sigCtxt :: Message -> [TcTyVar] -> TcThetaType -> TcTauType
809
	-> TidyEnv -> NF_TcM s (TidyEnv, Message)
810
811
812
813
814
sigCtxt when sig_tyvars sig_theta sig_tau tidy_env
  = zonkTcType sig_tau		`thenNF_Tc` \ actual_tau ->
    let
	(env1, tidy_sig_tyvars)  = tidyTyVars tidy_env sig_tyvars
	(env2, tidy_sig_rho)	 = tidyOpenType env1 (mkRhoTy sig_theta sig_tau)
815
	(env3, tidy_actual_tau)  = tidyOpenType env2 actual_tau
816
	msg = vcat [ptext SLIT("Signature type:    ") <+> pprType (mkForAllTys tidy_sig_tyvars tidy_sig_rho),
817
818
819
		    ptext SLIT("Type to generalise:") <+> pprType tidy_actual_tau,
		    when
		   ]
820
    in
821
    returnNF_Tc (env3, msg)
822

823
sigPatCtxt bound_tvs bound_ids tidy_env
824
  = returnNF_Tc (env1,
825
		 sep [ptext SLIT("When checking a pattern that binds"),
826
827
		      nest 4 (vcat (zipWith ppr_id show_ids tidy_tys))])
  where
828
829
    show_ids = filter is_interesting bound_ids
    is_interesting id = any (`elemVarSet` idFreeTyVars id) bound_tvs
830

831
832
    (env1, tidy_tys) = tidyOpenTypes tidy_env (map idType show_ids)
    ppr_id id ty     = ppr id <+> dcolon <+> ppr ty
833
834
835
836
837
838
839
840
841
842
	-- Don't zonk the types so we get the separate, un-unified versions
\end{code}


%************************************************************************
%*									*
\subsection{Errors and contexts}
%*									*
%************************************************************************

843
\begin{code}
844
845
tcsigCtxt v   = ptext SLIT("In a type signature for") <+> quotes (ppr v)

846
847
typeCtxt ty = ptext SLIT("In the type") <+> quotes (ppr ty)

848
849
850
851
852
853
854
855
typeKindCtxt :: RenamedHsType -> Message
typeKindCtxt ty = sep [ptext SLIT("When checking that"),
	  	       nest 2 (quotes (ppr ty)),
		       ptext SLIT("is a type")]

appKindCtxt :: SDoc -> Message
appKindCtxt pp = ptext SLIT("When checking kinds in") <+> quotes pp

856
857
858
859
860
861
862
wrongThingErr expected actual name
  = pp_actual actual <+> quotes (ppr name) <+> ptext SLIT("used as a") <+> text expected
  where
    pp_actual (ATyCon _) = ptext SLIT("Type constructor")
    pp_actual (AClass _) = ptext SLIT("Class")
    pp_actual (ATyVar _) = ptext SLIT("Type variable")
    pp_actual (AThing _) = ptext SLIT("Utterly bogus")
863

864
865
ambigErr pred ty
  = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
866
	 nest 4 (ptext SLIT("for the type:") <+> ppr ty),
867
	 nest 4 (ptext SLIT("Each forall'd type variable mentioned by the constraint must appear after the =>"))]
868
869
870
871
872
873

freeErr pred ty
  = sep [ptext SLIT("The constraint") <+> quotes (pprPred pred) <+>
		   ptext SLIT("does not mention any of the universally quantified type variables"),
	 nest 4 (ptext SLIT("in the type") <+> quotes (ppr ty))
    ]
874
\end{code}