TcMonoType.lhs 29.4 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
8
module TcMonoType ( tcHsSigType, tcHsType, tcIfaceType, tcHsTheta, 
		    UserTypeCtxt(..),
9
10
11

			-- Kind checking
		    kcHsTyVar, kcHsTyVars, mkTyClTyVars,
12
13
		    kcHsType, kcHsSigType, kcHsSigTypes, 
		    kcHsLiftedSigType, kcHsContext,
14
		    tcAddScopedTyVars, 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, extractHsTyVars )
25
import TcHsSyn		( TcId )
26

27
import TcMonad
28
import TcEnv		( tcExtendTyVarEnv, tcLookup, tcLookupGlobal,
29
			  tcGetGlobalTyVars, tcLEnvElts, tcInLocalScope,
30
		 	  TyThing(..), TcTyThing(..), tcExtendKindEnv
31
			)
32
import TcMType		( newKindVar, tcInstSigTyVars, 
33
			  zonkKindEnv, zonkTcType, zonkTcTyVars, zonkTcTyVar,
34
35
			  unifyKind, unifyOpenTypeKind,
			  checkValidType, UserTypeCtxt(..), pprUserTypeCtxt
36
			)
37
38
import TcType		( Type, Kind, SourceType(..), ThetaType, TyVarDetails(..),
			  TcTyVar, TcTyVarSet, TcType, TcKind, TcThetaType, TcTauType,
39
			  mkTyVarTy, mkTyVarTys, mkFunTy, mkSynTy,
40
41
42
			  tcSplitForAllTys, tcSplitRhoTy, 
		 	  hoistForAllTys, allDistinctTyVars, zipFunTys, 
			  mkSigmaTy, mkPredTy, mkTyConApp, mkAppTys, mkRhoTy,
43
			  liftedTypeKind, unliftedTypeKind, mkArrowKind,
44
			  mkArrowKinds, tcGetTyVar_maybe, tcGetTyVar, tcSplitFunTy_maybe,
45
		  	  tidyOpenType, tidyOpenTypes, tidyOpenTyVar, tidyOpenTyVars,
46
			  tyVarsOfType, mkForAllTys
47
			)
48
49
import qualified Type	( getTyVar_maybe )

50
import Inst		( Inst, InstOrigin(..), newMethodWithGivenTy, instToId )
51
import PprType		( pprType )
52
import Subst		( mkTopTyVarSubst, substTy )
53
import CoreFVs		( idFreeTyVars )
54
import Id		( mkLocalId, idName, idType )
55
import Var		( Id, Var, TyVar, mkTyVar, tyVarKind, isMutTyVar, mutTyVarDetails )
56
57
import VarEnv
import VarSet
58
import ErrUtils		( Message )
59
import TyCon		( TyCon, isSynTyCon, tyConArity, tyConKind )
60
import Class		( classTyCon )
61
62
import Name		( Name, getSrcLoc )
import NameSet
63
import TysWiredIn	( mkListTy, mkTupleTy, genUnitTyCon )
64
import BasicTypes	( Boxity(..) )
65
import SrcLoc		( SrcLoc )
sof's avatar
sof committed
66
import Util		( isSingleton, lengthIs )
67
import Outputable
68

69
70
\end{code}

71

72
73
74
75
76
77
78
79
80
81
%************************************************************************
%*									*
\subsection{Checking types}
%*									*
%************************************************************************

Generally speaking we now type-check types in three phases

	1.  Kind check the HsType [kcHsType]
	2.  Convert from HsType to Type, and hoist the foralls [tcHsType]
82
	3.  Check the validity of the resulting type [checkValidType]
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
118
119
120
121
122
123
124
125
126
127
128

Often these steps are done one after the othe (tcHsSigType).
But in mutually recursive groups of type and class decls we do
	1 kind-check the whole group
	2 build TyCons/Classes in a knot-tied wa
	3 check the validity of types in the now-unknotted TyCons/Classes

\begin{code}
tcHsSigType :: UserTypeCtxt -> RenamedHsType -> TcM Type
  -- Do kind checking, and hoist for-alls to the top
tcHsSigType ctxt ty = tcAddErrCtxt (checkTypeCtxt ctxt ty) (
			kcTypeType ty		`thenTc_`
		        tcHsType ty
		      )				`thenTc` \ ty' ->
		      checkValidType ctxt ty'	`thenTc_`
		      returnTc ty'

checkTypeCtxt ctxt ty
  = vcat [ptext SLIT("In the type:") <+> ppr ty,
	  ptext SLIT("While checking") <+> pprUserTypeCtxt ctxt ]

tcHsType    :: RenamedHsType -> TcM Type
  -- Don't do kind checking, nor validity checking, 
  -- 	but do hoist for-alls to the top
  -- This is used in type and class decls, where kinding is
  -- done in advance, and validity checking is done later
  -- [Validity checking done later because of knot-tying issues.]
tcHsType ty = tc_type ty  `thenTc` \ ty' ->  
	      returnTc (hoistForAllTys ty')

tcHsTheta :: RenamedContext -> TcM ThetaType
-- Used when we are expecting a ClassContext (i.e. no implicit params)
-- Does not do validity checking, like tcHsType
tcHsTheta hs_theta = mapTc tc_pred hs_theta

-- In interface files the type is already kinded,
-- and we definitely don't want to hoist for-alls.
-- Otherwise we'll change
--  	dmfail :: forall m:(*->*) Monad m => forall a:* => String -> m a
-- into 
-- 	dmfail :: forall m:(*->*) a:* Monad m => String -> m a
-- which definitely isn't right!
tcIfaceType ty = tc_type ty
\end{code}


129
130
%************************************************************************
%*									*
131
\subsection{Kind checking}
132
133
134
%*									*
%************************************************************************

135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
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

152
The kind checker is passed to tcHsTyVars as an argument.  
153
154
155
156
157
158
159

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.

160
The kind checker passed to tcHsTyVars needs to look at enough to
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
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::*->*

177
\begin{code}
178
179
180
181
-- tcHsTyVars is used for type variables in type signatures
--	e.g. forall a. a->a
-- They are immutable, because they scope only over the signature
-- They may or may not be explicitly-kinded
182
tcHsTyVars :: [HsTyVarBndr Name] 
183
184
185
	   -> TcM a				-- The kind checker
	   -> ([TyVar] -> TcM b)
	   -> TcM b
186
187

tcHsTyVars [] kind_check thing_inside = thing_inside []
188
189
	-- A useful short cut for a common case!
  
190
tcHsTyVars tv_names kind_check thing_inside
191
192
  = kcHsTyVars tv_names 				`thenNF_Tc` \ tv_names_w_kinds ->
    tcExtendKindEnv tv_names_w_kinds kind_check		`thenTc_`
193
194
195
196
197
198
    zonkKindEnv tv_names_w_kinds			`thenNF_Tc` \ tvs_w_kinds ->
    let
	tyvars = mkImmutTyVars tvs_w_kinds
    in
    tcExtendTyVarEnv tyvars (thing_inside tyvars)

199
200
201
202
203


tcAddScopedTyVars :: [RenamedHsType] -> TcM a -> TcM a
-- tcAddScopedTyVars is used for scoped type variables
-- added by pattern type signatures
204
205
206
--	e.g.  \ (x::a) (y::a) -> x+y
-- They never have explicit kinds (because this is source-code only)
-- They are mutable (because they can get bound to a more specific type)
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

-- Find the not-already-in-scope signature type variables,
-- kind-check them, and bring them into scope
--
-- We no longer specify that these type variables must be univerally 
-- quantified (lots of email on the subject).  If you want to put that 
-- back in, you need to
--	a) Do a checkSigTyVars after thing_inside
--	b) More insidiously, don't pass in expected_ty, else
--	   we unify with it too early and checkSigTyVars barfs
--	   Instead you have to pass in a fresh ty var, and unify
--	   it with expected_ty afterwards
tcAddScopedTyVars [] thing_inside
  = thing_inside	-- Quick get-out for the empty case

tcAddScopedTyVars sig_tys thing_inside
  = tcGetEnv					`thenNF_Tc` \ env ->
    let
	all_sig_tvs	= foldr (unionNameSets . extractHsTyVars) emptyNameSet sig_tys
	sig_tvs 	= filter not_in_scope (nameSetToList all_sig_tvs)
 	not_in_scope tv = not (tcInLocalScope env tv)
    in	      
    mapNF_Tc newNamedKindVar sig_tvs			`thenTc` \ kind_env ->
    tcExtendKindEnv kind_env (kcHsSigTypes sig_tys)	`thenTc_`
    zonkKindEnv kind_env				`thenNF_Tc` \ tvs_w_kinds ->
    listTc [ tcNewMutTyVar name kind PatSigTv
	   | (name, kind) <- tvs_w_kinds]		`thenNF_Tc` \ tyvars ->
234
    tcExtendTyVarEnv tyvars thing_inside
235
236
237
238
\end{code}
    

\begin{code}
239
240
kcHsTyVar  :: HsTyVarBndr name   -> NF_TcM (name, TcKind)
kcHsTyVars :: [HsTyVarBndr name] -> NF_TcM [(name, TcKind)]
241

242
kcHsTyVar (UserTyVar name)       = newNamedKindVar name
243
244
245
246
kcHsTyVar (IfaceTyVar name kind) = returnNF_Tc (name, kind)

kcHsTyVars tvs = mapNF_Tc kcHsTyVar tvs

247
248
249
newNamedKindVar name = newKindVar	`thenNF_Tc` \ kind ->
		       returnNF_Tc (name, kind)

250
---------------------------
251
252
253
kcLiftedType :: RenamedHsType -> TcM ()
	-- The type ty must be a *lifted* *type*
kcLiftedType ty
254
255
  = kcHsType ty				`thenTc` \ kind ->
    tcAddErrCtxt (typeKindCtxt ty)	$
256
    unifyKind liftedTypeKind kind
257
258
    
---------------------------
259
kcTypeType :: RenamedHsType -> TcM ()
260
	-- The type ty must be a *type*, but it can be lifted or unlifted.
261
262
263
264
265
266
kcTypeType ty
  = kcHsType ty				`thenTc` \ kind ->
    tcAddErrCtxt (typeKindCtxt ty)	$
    unifyOpenTypeKind kind

---------------------------
267
kcHsSigType, kcHsLiftedSigType :: RenamedHsType -> TcM ()
268
	-- Used for type signatures
269
270
kcHsSigType  	  = kcTypeType
kcHsSigTypes tys  = mapTc_ kcHsSigType tys
271
kcHsLiftedSigType = kcLiftedType
272
273

---------------------------
274
kcHsType :: RenamedHsType -> TcM TcKind
275
kcHsType (HsTyVar name)	      = kcTyVar name
276
277

kcHsType (HsListTy ty)
278
279
  = kcLiftedType ty		`thenTc` \ tau_ty ->
    returnTc liftedTypeKind
280

281
kcHsType (HsTupleTy (HsTupCon _ boxity _) tys)
282
283
  = mapTc kcTypeType tys	`thenTc_`
    returnTc (case boxity of
284
285
		  Boxed   -> liftedTypeKind
		  Unboxed -> unliftedTypeKind)
286
287
288

kcHsType (HsFunTy ty1 ty2)
  = kcTypeType ty1	`thenTc_`
289
    kcTypeType ty2	`thenTc_`
290
    returnTc liftedTypeKind
291

292
293
294
kcHsType (HsNumTy _)		-- The unit type for generics
  = returnTc liftedTypeKind

295
296
297
298
299
300
301
302
kcHsType ty@(HsOpTy ty1 op ty2)
  = kcTyVar op				`thenTc` \ op_kind ->
    kcHsType ty1			`thenTc` \ ty1_kind ->
    kcHsType ty2			`thenTc` \ ty2_kind ->
    tcAddErrCtxt (appKindCtxt (ppr ty))	$
    kcAppKind op_kind  ty1_kind		`thenTc` \ op_kind' ->
    kcAppKind op_kind' ty2_kind
   
303
304
kcHsType (HsPredTy pred)
  = kcHsPred pred		`thenTc_`
305
    returnTc liftedTypeKind
306
307

kcHsType ty@(HsAppTy ty1 ty2)
308
309
  = kcHsType ty1			`thenTc` \ tc_kind ->
    kcHsType ty2			`thenTc` \ arg_kind ->
310
    tcAddErrCtxt (appKindCtxt (ppr ty))	$
311
    kcAppKind tc_kind arg_kind
312
313

kcHsType (HsForAllTy (Just tv_names) context ty)
314
315
  = kcHsTyVars tv_names		`thenNF_Tc` \ kind_env ->
    tcExtendKindEnv kind_env	$
316
    kcHsContext context		`thenTc_`
317
    kcHsType ty			`thenTc_`
318
    returnTc liftedTypeKind
319

320
321
---------------------------
kcAppKind fun_kind arg_kind
322
  = case tcSplitFunTy_maybe fun_kind of 
323
324
325
326
327
328
329
330
	Just (arg_kind', res_kind)
		-> unifyKind arg_kind arg_kind'	`thenTc_`
		   returnTc res_kind

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

331
332
333
334

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

335
kcHsPred :: RenamedHsPred -> TcM ()
336
kcHsPred pred@(HsIParam name ty)
337
  = tcAddErrCtxt (appKindCtxt (ppr pred))	$
338
    kcLiftedType ty
339

340
kcHsPred pred@(HsClassP cls tys)
341
  = tcAddErrCtxt (appKindCtxt (ppr pred))	$
342
343
    kcClass cls					`thenTc` \ kind ->
    mapTc kcHsType tys				`thenTc` \ arg_kinds ->
344
    unifyKind kind (mkArrowKinds arg_kinds liftedTypeKind)
345

346
 ---------------------------
347
348
349
350
351
352
353
354
355
356
357
358
359
360
kcTyVar name	-- Could be a tyvar or a tycon
  = tcLookup name	`thenTc` \ thing ->
    case thing of 
	AThing kind 	    -> returnTc kind
	ATyVar tv	    -> returnTc (tyVarKind tv)
	AGlobal (ATyCon tc) -> returnTc (tyConKind tc) 
	other		    -> failWithTc (wrongThingErr "type" thing name)

kcClass cls	-- Must be a class
  = tcLookup cls 				`thenNF_Tc` \ thing -> 
    case thing of
	AThing kind	      -> returnTc kind
	AGlobal (AClass cls)  -> returnTc (tyConKind (classTyCon cls))
	other		      -> failWithTc (wrongThingErr "class" thing cls)
361
362
\end{code}

363
364
365
366
367
368
369
%************************************************************************
%*									*
\subsection{tc_type}
%*									*
%************************************************************************

tc_type, the main work horse
370
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
371

372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
	-------------------
	*** BIG WARNING ***
	-------------------

tc_type is used to typecheck the types in the RHS of data
constructors.  In the case of recursive data types, that means that
the type constructors themselves are (partly) black holes.  e.g.

	data T a = MkT a [T a]

While typechecking the [T a] on the RHS, T itself is not yet fully
defined.  That in turn places restrictions on what you can check in
tcHsType; if you poke on too much you get a black hole.  I keep
forgetting this, hence this warning!

387
388
So tc_type does no validity-checking.  Instead that's all done
by TcMType.checkValidType
389
390
391
392
393
394

	--------------------------
	*** END OF BIG WARNING ***
	--------------------------


395
\begin{code}
396
tc_type :: RenamedHsType -> TcM Type
397

398
399
tc_type ty@(HsTyVar name)
  = tc_app ty []
400

401
402
tc_type (HsListTy ty)
  = tc_type ty	`thenTc` \ tau_ty ->
403
    returnTc (mkListTy tau_ty)
404

405
tc_type (HsTupleTy (HsTupCon _ boxity arity) tys)
sof's avatar
sof committed
406
  = ASSERT( tys `lengthIs` arity )
407
    tc_types tys	`thenTc` \ tau_tys ->
408
    returnTc (mkTupleTy boxity arity tau_tys)
409
410
411
412

tc_type (HsFunTy ty1 ty2)
  = tc_type ty1			`thenTc` \ tau_ty1 ->
    tc_type ty2			`thenTc` \ tau_ty2 ->
413
    returnTc (mkFunTy tau_ty1 tau_ty2)
414

415
tc_type (HsNumTy n)
416
417
418
  = ASSERT(n== 1)
    returnTc (mkTyConApp genUnitTyCon [])

419
420
421
422
tc_type (HsOpTy ty1 op ty2)
  = tc_type ty1 `thenTc` \ tau_ty1 ->
    tc_type ty2 `thenTc` \ tau_ty2 ->
    tc_fun_type op [tau_ty1,tau_ty2]
423

424
tc_type (HsAppTy ty1 ty2) = tc_app ty1 [ty2]
425

426
427
tc_type (HsPredTy pred)
  = tc_pred pred	`thenTc` \ pred' ->
428
    returnTc (mkPredTy pred')
429

430
tc_type full_ty@(HsForAllTy (Just tv_names) ctxt ty)
431
  = let
432
	kind_check = kcHsContext ctxt `thenTc_` kcHsType ty
433
    in
434
435
436
437
    tcHsTyVars tv_names kind_check	$ \ tyvars ->
    mapTc tc_pred ctxt			`thenTc` \ theta ->
    tc_type ty				`thenTc` \ tau ->
    returnTc (mkSigmaTy tyvars theta tau)
438

439
tc_types arg_tys = mapTc tc_type arg_tys
440
\end{code}
441

442
443
Help functions for type applications
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
444

445
\begin{code}
446
447
448
tc_app :: RenamedHsType -> [RenamedHsType] -> TcM Type
tc_app (HsAppTy ty1 ty2) tys
  = tc_app ty1 (ty2:tys)
449

450
tc_app ty tys
451
  = tcAddErrCtxt (appKindCtxt pp_app)	$
452
    tc_types tys			`thenTc` \ arg_tys ->
453
454
    case ty of
	HsTyVar fun -> tc_fun_type fun arg_tys
455
	other	    -> tc_type ty		`thenTc` \ fun_ty ->
456
		       returnNF_Tc (mkAppTys fun_ty arg_tys)
457
458
  where
    pp_app = ppr ty <+> sep (map pprParendHsType tys)
459

460
-- (tc_fun_type ty arg_tys) returns (mkAppTys ty arg_tys)
461
462
463
-- But not quite; for synonyms it checks the correct arity, and builds a SynTy
-- 	hence the rather strange functionality.

464
tc_fun_type name arg_tys
465
  = tcLookup name			`thenTc` \ thing ->
466
    case thing of
467
468
	ATyVar tv -> returnTc (mkAppTys (mkTyVarTy tv) arg_tys)

469
	AGlobal (ATyCon tc)
470
		| isSynTyCon tc ->  returnTc (mkSynTy tc arg_tys)
471
		| otherwise	->  returnTc (mkTyConApp tc arg_tys)
472

473
	other -> failWithTc (wrongThingErr "type constructor" thing name)
474
475
476
\end{code}


477
478
479
Contexts
~~~~~~~~
\begin{code}
480
tc_pred assn@(HsClassP class_name tys)
481
  = tcAddErrCtxt (appKindCtxt (ppr assn))	$
482
    tc_types tys			`thenTc` \ arg_tys ->
483
    tcLookupGlobal class_name			`thenTc` \ thing ->
484
    case thing of
485
486
	AClass clas -> returnTc (ClassP clas arg_tys)
	other 	    -> failWithTc (wrongThingErr "class" (AGlobal thing) class_name)
487

488
tc_pred assn@(HsIParam name ty)
489
  = tcAddErrCtxt (appKindCtxt (ppr assn))	$
490
    tc_type ty					`thenTc` \ arg_ty ->
491
    returnTc (IParam name arg_ty)
492
493
494
\end{code}


495

496
497
498
499
500
501
%************************************************************************
%*									*
\subsection{Type variables, with knot tying!}
%*									*
%************************************************************************

502
\begin{code}
503
504
mkImmutTyVars :: [(Name,Kind)] -> [TyVar]
mkImmutTyVars pairs = [mkTyVar name kind | (name, kind) <- pairs]
505
506
507
508
509

mkTyClTyVars :: Kind 			-- Kind of the tycon or class
	     -> [HsTyVarBndr Name]
	     -> [TyVar]
mkTyClTyVars kind tyvar_names
510
  = mkImmutTyVars tyvars_w_kinds
511
  where
512
    (tyvars_w_kinds, _) = zipFunTys (hsTyVarNames tyvar_names) kind
513
514
\end{code}

515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531

%************************************************************************
%*									*
\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}
532
data TcSigInfo
533
534
535
  = TySigInfo	    
	Name			-- N, the Name in corresponding binding

536
	TcId			-- *Polymorphic* binder for this value...
537
538
				-- Has name = N

539
540
541
	[TcTyVar]		-- tyvars
	TcThetaType		-- theta
	TcTauType		-- tau
542

543
	TcId			-- *Monomorphic* binder for this value
544
545
546
				-- Does *not* have name = N
				-- Has type tau

547
	[Inst]			-- Empty if theta is null, or
548
549
550
551
				-- (method mono_id) otherwise

	SrcLoc			-- Of the signature

552
553
554
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
555

556
maybeSig :: [TcSigInfo] -> Name -> Maybe (TcSigInfo)
557
558
559
560
561
562
563
564
565
	-- 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}
566
tcTySig :: RenamedSig -> TcM TcSigInfo
567
568

tcTySig (Sig v ty src_loc)
569
 = tcAddSrcLoc src_loc				$ 
570
   tcHsSigType (FunSigCtxt v) ty		`thenTc` \ sigma_tc_ty ->
571
   mkTcSig (mkLocalId v sigma_tc_ty) src_loc	`thenNF_Tc` \ sig -> 
572
573
   returnTc sig

574
mkTcSig :: TcId -> SrcLoc -> NF_TcM TcSigInfo
575
576
577
578
579
580
581
582
583
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
584
	(tyvars, rho) = tcSplitForAllTys (idType poly_id)
585
   in
586
   tcInstSigTyVars SigTv tyvars			`thenNF_Tc` \ tyvars' ->
587
588
589
590
	-- Make *signature* type variables

   let
     tyvar_tys' = mkTyVarTys tyvars'
591
592
     rho' = substTy (mkTopTyVarSubst tyvars tyvar_tys') rho
	-- mkTopTyVarSubst because the tyvars' are fresh
593
594

     (theta', tau') = tcSplitRhoTy rho'
595
	-- This splitRhoTy tries hard to make sure that tau' is a type synonym
596
597
598
	-- wherever possible, which can improve interface files.
   in
   newMethodWithGivenTy SignatureOrigin 
599
		poly_id
600
601
		tyvar_tys'
		theta' tau'			`thenNF_Tc` \ inst ->
602
603
	-- We make a Method even if it's not overloaded; no harm
	
604
   returnNF_Tc (TySigInfo name poly_id tyvars' theta' tau' (instToId inst) [inst] src_loc)
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
  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
620
	(a) Still all type variables
621
622
623
		eg matching signature [a] against inferred type [(p,q)]
		[then a will be unified to a non-type variable]

624
	(b) Still all distinct
625
626
627
		eg matching signature [(a,b)] against inferred type [(p,p)]
		[then a and b will be unified together]

628
	(c) Not mentioned in the environment
629
630
631
632
633
634
635
636
		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.

637
638
639
640
641
642
643
644
645
646
647
648
	(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

649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
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}
674
675
checkSigTyVars :: [TcTyVar]		-- Universally-quantified type variables in the signature
	       -> TcTyVarSet		-- Tyvars that are free in the type signature
676
677
678
679
					--	Not necessarily zonked
					-- 	These should *already* be in the free-in-env set, 
					-- 	and are used here only to improve the error message
	       -> TcM [TcTyVar]		-- Zonked signature type variables
680

681
682
checkSigTyVars [] free = returnTc []
checkSigTyVars sig_tyvars free_tyvars
683
684
  = zonkTcTyVars sig_tyvars		`thenNF_Tc` \ sig_tys ->
    tcGetGlobalTyVars			`thenNF_Tc` \ globals ->
685

686
    checkTcM (allDistinctTyVars sig_tys globals)
687
688
	     (complain sig_tys globals)	`thenTc_`

689
    returnTc (map (tcGetTyVar "checkSigTyVars") sig_tys)
690
691
692

  where
    complain sig_tys globals
693
      = -- "check" checks each sig tyvar in turn
694
        foldlNF_Tc check
695
		   (env2, emptyVarEnv, [])
696
		   (tidy_tvs `zip` tidy_tys)	`thenNF_Tc` \ (env3, _, msgs) ->
697

698
        failWithTcM (env3, main_msg $$ vcat msgs)
699
      where
700
701
	(env1, tidy_tvs) = tidyOpenTyVars emptyTidyEnv sig_tyvars
	(env2, tidy_tys) = tidyOpenTypes  env1	       sig_tys
702

703
	main_msg = ptext SLIT("Inferred type is less polymorphic than expected")
704

705
	check (tidy_env, acc, msgs) (sig_tyvar,ty)
706
707
708
709
		-- 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
710
	  = case tcGetTyVar_maybe ty of {
711
	      Nothing ->			-- Error (a)!
712
			returnNF_Tc (tidy_env, acc, unify_msg sig_tyvar (quotes (ppr ty)) : msgs) ;
713
714
715
716

	      Just tv ->

	    case lookupVarEnv acc tv of {
717
		Just sig_tyvar' -> 	-- Error (b)!
718
719
720
			returnNF_Tc (tidy_env, acc, unify_msg sig_tyvar thing : msgs)
		    where
			thing = ptext SLIT("another quantified type variable") <+> quotes (ppr sig_tyvar')
721

722
	      ; Nothing ->
723

724
	    if tv `elemVarSet` globals	-- Error (c) or (d)! Type variable escapes
725
					-- The least comprehensible, so put it last
726
			-- Game plan: 
727
			--    a) get the local TcIds and TyVars from the environment,
728
729
			-- 	 and pass them to find_globals (they might have tv free)
			--    b) similarly, find any free_tyvars that mention tv
730
	    then   tcGetEnv 							`thenNF_Tc` \ ve ->
731
        	   find_globals tv tidy_env  (tcLEnvElts ve)			`thenNF_Tc` \ (tidy_env1, globs) ->
732
733
        	   find_frees   tv tidy_env1 [] (varSetElems free_tyvars)	`thenNF_Tc` \ (tidy_env2, frees) ->
		   returnNF_Tc (tidy_env2, acc, escape_msg sig_tyvar tv globs frees : msgs)
734
735

	    else 	-- All OK
736
	    returnNF_Tc (tidy_env, extendVarEnv acc tv sig_tyvar, msgs)
737
738
	    }}

739
-----------------------
740
741
742
743
-- 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
746

find_globals :: Var 
             -> TidyEnv 
747
748
             -> [TcTyThing] 
             -> NF_TcM (TidyEnv, [SDoc])
749

750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
find_globals tv tidy_env things
  = go tidy_env [] things
  where
    go tidy_env acc [] = returnNF_Tc (tidy_env, acc)
    go tidy_env acc (thing : things)
      = find_thing ignore_it tidy_env thing 	`thenNF_Tc` \ (tidy_env1, maybe_doc) ->
	case maybe_doc of
	  Just d  -> go tidy_env1 (d:acc) things
	  Nothing -> go tidy_env1 acc     things

    ignore_it ty = not (tv `elemVarSet` tyVarsOfType ty)

-----------------------
find_thing ignore_it tidy_env (ATcId id)
  = zonkTcType  (idType id)	`thenNF_Tc` \ id_ty ->
    if ignore_it id_ty then
	returnNF_Tc (tidy_env, Nothing)
    else let
	(tidy_env', tidy_ty) = tidyOpenType tidy_env id_ty
	msg = sep [ppr id <+> dcolon <+> ppr tidy_ty, 
770
771
		   nest 2 (parens (ptext SLIT("bound at") <+>
			 	   ppr (getSrcLoc id)))]
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
    in
    returnNF_Tc (tidy_env', Just msg)

find_thing ignore_it tidy_env (ATyVar tv)
  = zonkTcTyVar tv		`thenNF_Tc` \ tv_ty ->
    if ignore_it tv_ty then
	returnNF_Tc (tidy_env, Nothing)
    else let
	(tidy_env1, tv1)     = tidyOpenTyVar tidy_env  tv
	(tidy_env2, tidy_ty) = tidyOpenType  tidy_env1 tv_ty
	msg = sep [ptext SLIT("Type variable") <+> quotes (ppr tv1) <+> eq_stuff, nest 2 bound_at]

	eq_stuff | Just tv' <- Type.getTyVar_maybe tv_ty, tv == tv' = empty
		 | otherwise	  				    = equals <+> ppr tv_ty
		-- It's ok to use Type.getTyVar_maybe because ty is zonked by now
	
	bound_at | isMutTyVar tv = mut_info	-- The expected case
		 | otherwise     = empty
	
791
	mut_info = sep [ptext SLIT("is bound by the") <+> ppr (mutTyVarDetails tv),
792
793
794
	     	        ptext SLIT("at") <+> ppr (getSrcLoc tv)]
    in
    returnNF_Tc (tidy_env2, Just msg)
795

796
-----------------------
797
798
799
800
801
802
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
803
	    (tidy_env', ftv') = tidyOpenTyVar tidy_env ftv
804
805
806
807
808
809
810
811
812
	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
813
814
	vcat [pp_it <+> ptext SLIT("is mentioned in the environment:"), 
	      nest 2 (vcat globs)]
815
816
817
818
819
820
821
     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
822
  where
823
824
825
826
    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")
827

sof's avatar
sof committed
828
    vcat_first :: Int -> [SDoc] -> SDoc
829
830
831
    vcat_first n []     = empty
    vcat_first 0 (x:xs) = text "...others omitted..."
    vcat_first n (x:xs) = x $$ vcat_first (n-1) xs
832

833

834
unify_msg tv thing = mk_msg tv <+> ptext SLIT("is unified with") <+> thing
835
836
837
838
839
840
mk_msg tv          = ptext SLIT("Quantified type variable") <+> quotes (ppr tv)
\end{code}

These two context are used with checkSigTyVars
    
\begin{code}
841
sigCtxt :: Message -> [TcTyVar] -> TcThetaType -> TcTauType
842
	-> TidyEnv -> NF_TcM (TidyEnv, Message)
843
844
845
sigCtxt when sig_tyvars sig_theta sig_tau tidy_env
  = zonkTcType sig_tau		`thenNF_Tc` \ actual_tau ->
    let
846
	(env1, tidy_sig_tyvars)  = tidyOpenTyVars tidy_env sig_tyvars
847
	(env2, tidy_sig_rho)	 = tidyOpenType env1 (mkRhoTy sig_theta sig_tau)
848
	(env3, tidy_actual_tau)  = tidyOpenType env2 actual_tau
849
	msg = vcat [ptext SLIT("Signature type:    ") <+> pprType (mkForAllTys tidy_sig_tyvars tidy_sig_rho),
850
851
852
		    ptext SLIT("Type to generalise:") <+> pprType tidy_actual_tau,
		    when
		   ]
853
    in
854
    returnNF_Tc (env3, msg)
855

856
sigPatCtxt bound_tvs bound_ids tidy_env
857
  = returnNF_Tc (env1,
858
		 sep [ptext SLIT("When checking a pattern that binds"),
859
860
		      nest 4 (vcat (zipWith ppr_id show_ids tidy_tys))])
  where
861
862
    show_ids = filter is_interesting bound_ids
    is_interesting id = any (`elemVarSet` idFreeTyVars id) bound_tvs
863

864
865
    (env1, tidy_tys) = tidyOpenTypes tidy_env (map idType show_ids)
    ppr_id id ty     = ppr id <+> dcolon <+> ppr ty
866
867
868
869
870
871
872
873
874
875
	-- Don't zonk the types so we get the separate, un-unified versions
\end{code}


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

876
\begin{code}
877
878
879
880
881
882
883
884
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

885
wrongThingErr expected thing name
886
887
888
889
890
891
892
893
  = pp_thing thing <+> quotes (ppr name) <+> ptext SLIT("used as a") <+> text expected
  where
    pp_thing (AGlobal (ATyCon _)) = ptext SLIT("Type constructor")
    pp_thing (AGlobal (AClass _)) = ptext SLIT("Class")
    pp_thing (AGlobal (AnId   _)) = ptext SLIT("Identifier")
    pp_thing (ATyVar _) 	  = ptext SLIT("Type variable")
    pp_thing (ATcId _)  	  = ptext SLIT("Local identifier")
    pp_thing (AThing _) 	  = ptext SLIT("Utterly bogus")
894
\end{code}