TcHsType.lhs 27.7 KB
Newer Older
1
2
3
4
5
6
7

% (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
%
\section[TcMonoType]{Typechecking user-specified @MonoTypes@}

\begin{code}
module TcHsType (
8
	tcHsSigType, tcHsDeriv,
9
10
11
12
	UserTypeCtxt(..), 

		-- Kind checking
	kcHsTyVars, kcHsSigType, kcHsLiftedSigType, 
13
	kcCheckHsType, kcHsContext, kcHsType, 
14
15
	
		-- Typechecking kinded types
16
	tcHsKindedContext, tcHsKindedType, tcHsBangType,
17
18
	tcTyVarBndrs, dsHsType, tcLHsConResTy,
	tcDataKindSig,
19

20
21
		-- Pattern type signatures
	tcHsPatSigType, tcPatSig
22
23
24
25
   ) where

#include "HsVersions.h"

26
import HsSyn		( HsType(..), LHsType, HsTyVarBndr(..), LHsTyVarBndr, 
27
			  LHsContext, HsPred(..), LHsPred, HsExplicitForAll(..) )
28
import RnHsSyn		( extractHsTyVars )
29
import TcRnMonad
30
import TcEnv		( tcExtendTyVarEnv, tcExtendKindEnvTvs, 
31
			  tcLookup, tcLookupClass, tcLookupTyCon,
32
33
		 	  TyThing(..), getInLocalScope, getScopedTyVarBinds,
			  wrongThingErr
34
			)
35
36
37
38
import TcMType		( newKindVar, 
			  zonkTcKindToKind, 
			  tcInstBoxyTyVar, readFilledBox,
			  checkValidType
39
			)
40
import TcUnify		( boxyUnify, unifyFunKind, checkExpectedKind )
41
import TcIface		( checkWiredInTyCon )
42
43
44
45
46
import TcType		( Type, PredType(..), ThetaType, BoxySigmaType,
			  TcType, TcKind, isRigidTy,
			  UserTypeCtxt(..), pprUserTypeCtxt,
			  substTyWith, mkTyVarTys, tcEqType,
		 	  tcIsTyVarTy, mkFunTy, mkSigmaTy, mkPredTy, 
47
			  mkTyConApp, mkAppTys, typeKind )
48
49
import Kind 		( Kind, isLiftedTypeKind, liftedTypeKind, ubxTupleKind, 
			  openTypeKind, argTypeKind, splitKindFunTys )
50
import Var		( TyVar, mkTyVar, tyVarName )
51
import TyCon		( TyCon, tyConKind )
52
import Class		( Class, classTyCon )
53
54
import Name		( Name, mkInternalName )
import OccName		( mkOccName, tvName )
55
56
import NameSet
import PrelNames	( genUnitTyConName )
57
import TysWiredIn	( mkListTy, listTyCon, mkPArrTy, parrTyCon, tupleTyCon )
58
59
import BasicTypes	( Boxity(..) )
import SrcLoc		( Located(..), unLoc, noLoc, getLoc, srcSpanStart )
60
import UniqSupply	( uniqsFromSupply )
61
62
63
64
65
66
67
68
69
70
71
72
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
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
import Outputable
\end{code}


	----------------------------
		General notes
	----------------------------

Generally speaking we now type-check types in three phases

  1.  kcHsType: kind check the HsType
	*includes* performing any TH type splices;
	so it returns a translated, and kind-annotated, type

  2.  dsHsType: convert from HsType to Type:
	perform zonking
	expand type synonyms [mkGenTyApps]
	hoist the foralls [tcHsType]

  3.  checkValidType: check the validity of the resulting type

Often these steps are done one after the other (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 way
	3 check the validity of types in the now-unknotted TyCons/Classes

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 tcHsTyVars 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::*->*


Validity checking
~~~~~~~~~~~~~~~~~
Some of the validity check could in principle be done by the kind checker, 
but not all:

- During desugaring, we normalise by expanding type synonyms.  Only
  after this step can we check things like type-synonym saturation
  e.g. 	type T k = k Int
	type S a = a
  Then (T S) is ok, because T is saturated; (T S) expands to (S Int);
  and then S is saturated.  This is a GHC extension.

- Similarly, also a GHC extension, we look through synonyms before complaining
  about the form of a class or instance declaration

- Ambiguity checks involve functional dependencies, and it's easier to wait
  until knots have been resolved before poking into them

Also, in a mutually recursive group of types, we can't look at the TyCon until we've
finished building the loop.  So to keep things simple, we postpone most validity
checking until step (3).

Knot tying
~~~~~~~~~~
During step (1) we might fault in a TyCon defined in another module, and it might
(via a loop) refer back to a TyCon defined in this module. So when we tie a big
knot around type declarations with ARecThing, so that the fault-in code can get
the TyCon being defined.


%************************************************************************
%*									*
\subsection{Checking types}
%*									*
%************************************************************************

\begin{code}
148
tcHsSigType :: UserTypeCtxt -> LHsType Name -> TcM Type
149
  -- Do kind checking, and hoist for-alls to the top
150
151
152
  -- NB: it's important that the foralls that come from the top-level
  --	 HsForAllTy in hs_ty occur *first* in the returned type.
  --     See Note [Scoped] with TcSigInfo
153
tcHsSigType ctxt hs_ty 
154
  = addErrCtxt (pprHsSigCtxt ctxt hs_ty) $
155
156
157
158
    do	{ kinded_ty <- kcTypeType hs_ty
	; ty <- tcHsKindedType kinded_ty
	; checkValidType ctxt ty	
	; returnM ty }
159

160
161
162
163
-- Used for the deriving(...) items
tcHsDeriv :: LHsType Name -> TcM ([TyVar], Class, [Type])
tcHsDeriv = addLocM (tc_hs_deriv [])

164
tc_hs_deriv tv_names (HsPredTy (HsClassP cls_name hs_tys))
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
  = kcHsTyVars tv_names 		$ \ tv_names' ->
    do	{ cls_kind <- kcClass cls_name
	; (tys, res_kind) <- kcApps cls_kind (ppr cls_name) hs_tys
	; tcTyVarBndrs tv_names'	$ \ tyvars ->
    do	{ arg_tys <- dsHsTypes tys
	; cls <- tcLookupClass cls_name
	; return (tyvars, cls, arg_tys) }}

tc_hs_deriv tv_names1 (HsForAllTy _ tv_names2 (L _ []) (L _ ty))
  = 	-- Funny newtype deriving form
	-- 	forall a. C [a]
	-- where C has arity 2.  Hence can't use regular functions
    tc_hs_deriv (tv_names1 ++ tv_names2) ty

tc_hs_deriv _ other
  = failWithTc (ptext SLIT("Illegal deriving item") <+> ppr other)
181
182
183
184
185
186
187
\end{code}

	These functions are used during knot-tying in
	type and class declarations, when we have to
 	separate kind-checking, desugaring, and validity checking

\begin{code}
188
kcHsSigType, kcHsLiftedSigType :: LHsType Name -> TcM (LHsType Name)
189
190
191
192
	-- Used for type signatures
kcHsSigType ty 	     = kcTypeType ty
kcHsLiftedSigType ty = kcLiftedType ty

193
tcHsKindedType :: LHsType Name -> TcM Type
194
  -- Don't do kind checking, nor validity checking.
195
196
197
  -- 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.]
198
tcHsKindedType hs_ty = dsHsType hs_ty
199

200
201
202
203
204
tcHsBangType :: LHsType Name -> TcM Type
-- Permit a bang, but discard it
tcHsBangType (L span (HsBangTy b ty)) = tcHsKindedType ty
tcHsBangType ty 		      = tcHsKindedType ty

205
tcHsKindedContext :: LHsContext Name -> TcM ThetaType
206
207
-- Used when we are expecting a ClassContext (i.e. no implicit params)
-- Does not do validity checking, like tcHsKindedType
208
tcHsKindedContext hs_theta = addLocM (mappM dsHsLPred) hs_theta
209
210
211
212
213
214
215
216
217
218
219
220
221
\end{code}


%************************************************************************
%*									*
		The main kind checker: kcHsType
%*									*
%************************************************************************
	
	First a couple of simple wrappers for kcHsType

\begin{code}
---------------------------
222
kcLiftedType :: LHsType Name -> TcM (LHsType Name)
223
-- The type ty must be a *lifted* *type*
224
225
226
kcLiftedType ty = kcCheckHsType ty liftedTypeKind
    
---------------------------
227
kcTypeType :: LHsType Name -> TcM (LHsType Name)
228
229
230
-- The type ty must be a *type*, but it can be lifted or 
-- unlifted or an unboxed tuple.
kcTypeType ty = kcCheckHsType ty openTypeKind
231
232

---------------------------
233
kcCheckHsType :: LHsType Name -> TcKind -> TcM (LHsType Name)
234
-- Check that the type has the specified kind
235
236
237
-- Be sure to use checkExpectedKind, rather than simply unifying 
-- with OpenTypeKind, because it gives better error messages
kcCheckHsType (L span ty) exp_kind 
238
  = setSrcSpan span				$
239
    do	{ (ty', act_kind) <- add_ctxt ty (kc_hs_type ty)
240
241
242
		-- Add the context round the inner check only
		-- because checkExpectedKind already mentions
		-- 'ty' by name in any error message
243

244
	; checkExpectedKind (strip ty) act_kind exp_kind
245
	; return (L span ty') }
246
  where
247
248
249
250
	-- Wrap a context around only if we want to show that contexts.  
	-- Omit invisble ones and ones user's won't grok (HsPred p).
    add_ctxt (HsPredTy p)		    	         thing = thing
    add_ctxt (HsForAllTy Implicit tvs (L _ []) (L _ ty)) thing = add_ctxt ty thing
251
    add_ctxt other_ty thing = addErrCtxt (typeCtxt ty) thing
252
253
254
255
256
257
258
259
260

	-- We infer the kind of the type, and then complain if it's
	-- not right.  But we don't want to complain about
	--	(ty) or !(ty) or forall a. ty
	-- when the real difficulty is with the 'ty' part.
    strip (HsParTy (L _ ty))          = strip ty
    strip (HsBangTy _ (L _ ty))       = strip ty
    strip (HsForAllTy _ _ _ (L _ ty)) = strip ty
    strip ty			      = ty
261
262
263
264
265
\end{code}

	Here comes the main function

\begin{code}
266
267
kcHsType :: LHsType Name -> TcM (LHsType Name, TcKind)
kcHsType ty = wrapLocFstM kc_hs_type ty
268
269
270
271
272
273
274
275
276
277
-- kcHsType *returns* the kind of the type, rather than taking an expected
-- kind as argument as tcExpr does.  
-- Reasons: 
--	(a) the kind of (->) is
--		forall bx1 bx2. Type bx1 -> Type bx2 -> Type Boxed
--  	    so we'd need to generate huge numbers of bx variables.
--	(b) kinds are so simple that the error messages are fine
--
-- The translated type has explicitly-kinded type-variable binders

278
kc_hs_type (HsParTy ty)
279
280
281
 = kcHsType ty		`thenM` \ (ty', kind) ->
   returnM (HsParTy ty', kind)

282
kc_hs_type (HsTyVar name)
283
284
285
  = kcTyVar name	`thenM` \ kind ->
    returnM (HsTyVar name, kind)

286
kc_hs_type (HsListTy ty) 
287
288
289
  = kcLiftedType ty			`thenM` \ ty' ->
    returnM (HsListTy ty', liftedTypeKind)

290
kc_hs_type (HsPArrTy ty)
291
292
293
  = kcLiftedType ty			`thenM` \ ty' ->
    returnM (HsPArrTy ty', liftedTypeKind)

294
kc_hs_type (HsNumTy n)
295
296
   = returnM (HsNumTy n, liftedTypeKind)

297
kc_hs_type (HsKindSig ty k) 
298
299
300
  = kcCheckHsType ty k	`thenM` \ ty' ->
    returnM (HsKindSig ty' k, k)

301
kc_hs_type (HsTupleTy Boxed tys)
302
303
304
  = mappM kcLiftedType tys	`thenM` \ tys' ->
    returnM (HsTupleTy Boxed tys', liftedTypeKind)

305
kc_hs_type (HsTupleTy Unboxed tys)
306
  = mappM kcTypeType tys	`thenM` \ tys' ->
307
    returnM (HsTupleTy Unboxed tys', ubxTupleKind)
308

309
kc_hs_type (HsFunTy ty1 ty2)
310
311
  = kcCheckHsType ty1 argTypeKind	`thenM` \ ty1' ->
    kcTypeType ty2			`thenM` \ ty2' ->
312
313
    returnM (HsFunTy ty1' ty2', liftedTypeKind)

314
315
kc_hs_type ty@(HsOpTy ty1 op ty2)
  = addLocM kcTyVar op			`thenM` \ op_kind ->
316
317
318
    kcApps op_kind (ppr op) [ty1,ty2]	`thenM` \ ([ty1',ty2'], res_kind) ->
    returnM (HsOpTy ty1' op ty2', res_kind)

319
kc_hs_type ty@(HsAppTy ty1 ty2)
320
  = kcHsType fun_ty			  `thenM` \ (fun_ty', fun_kind) ->
321
322
    kcApps fun_kind (ppr fun_ty) arg_tys  `thenM` \ ((arg_ty':arg_tys'), res_kind) ->
    returnM (foldl mk_app (HsAppTy fun_ty' arg_ty') arg_tys', res_kind)
323
324
  where
    (fun_ty, arg_tys) = split ty1 [ty2]
325
326
327
328
329
330
    split (L _ (HsAppTy f a)) as = split f (a:as)
    split f       	      as = (f,as)
    mk_app fun arg = HsAppTy (noLoc fun) arg	-- Add noLocs for inner nodes of
						-- the application; they are never used
    
kc_hs_type (HsPredTy pred)
331
332
333
  = kcHsPred pred		`thenM` \ pred' ->
    returnM (HsPredTy pred', liftedTypeKind)

334
kc_hs_type (HsForAllTy exp tv_names context ty)
335
336
  = kcHsTyVars tv_names		$ \ tv_names' ->
    kcHsContext context		`thenM`	\ ctxt' ->
337
    kcLiftedType ty		`thenM` \ ty' ->
338
	-- The body of a forall is usually a type, but in principle
339
340
341
342
343
	-- there's no reason to prohibit *unlifted* types.
	-- In fact, GHC can itself construct a function with an
	-- unboxed tuple inside a for-all (via CPR analyis; see 
	-- typecheck/should_compile/tc170)
	--
344
345
346
	-- Still, that's only for internal interfaces, which aren't
	-- kind-checked, so we only allow liftedTypeKind here
    returnM (HsForAllTy exp tv_names' ctxt' ty', liftedTypeKind)
347

348
349
350
351
352
353
354
355
kc_hs_type (HsBangTy b ty)
  = do { (ty', kind) <- kcHsType ty
       ; return (HsBangTy b ty', kind) }

kc_hs_type ty@(HsSpliceTy _)
  = failWithTc (ptext SLIT("Unexpected type splice:") <+> ppr ty)


356
---------------------------
357
358
359
360
kcApps :: TcKind			-- Function kind
       -> SDoc				-- Function 
       -> [LHsType Name]		-- Arg types
       -> TcM ([LHsType Name], TcKind)	-- Kind-checked args
361
362
kcApps fun_kind ppr_fun args
  = split_fk fun_kind (length args)	`thenM` \ (arg_kinds, res_kind) ->
363
    zipWithM kc_arg args arg_kinds	`thenM` \ args' ->
364
365
366
367
368
369
370
371
372
    returnM (args', res_kind)
  where
    split_fk fk 0 = returnM ([], fk)
    split_fk fk n = unifyFunKind fk	`thenM` \ mb_fk ->
		    case mb_fk of 
			Nothing       -> failWithTc too_many_args 
			Just (ak,fk') -> split_fk fk' (n-1)	`thenM` \ (aks, rk) ->
					 returnM (ak:aks, rk)

373
    kc_arg arg arg_kind = kcCheckHsType arg arg_kind
374
375
376
377
378

    too_many_args = ptext SLIT("Kind error:") <+> quotes ppr_fun <+>
		    ptext SLIT("is applied to too many type arguments")

---------------------------
379
kcHsContext :: LHsContext Name -> TcM (LHsContext Name)
380
381
382
383
kcHsContext ctxt = wrapLocM (mappM kcHsLPred) ctxt

kcHsLPred :: LHsPred Name -> TcM (LHsPred Name)
kcHsLPred = wrapLocM kcHsPred
384

385
386
387
kcHsPred :: HsPred Name -> TcM (HsPred Name)
kcHsPred pred	-- Checks that the result is of kind liftedType
  = kc_pred pred				`thenM` \ (pred', kind) ->
388
    checkExpectedKind pred kind liftedTypeKind	`thenM_` 
389
    returnM pred'
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
    
---------------------------
kc_pred :: HsPred Name -> TcM (HsPred Name, TcKind)	
	-- Does *not* check for a saturated
	-- application (reason: used from TcDeriv)
kc_pred pred@(HsIParam name ty)
  = kcHsType ty		`thenM` \ (ty', kind) ->
    returnM (HsIParam name ty', kind)

kc_pred pred@(HsClassP cls tys)
  = kcClass cls			`thenM` \ kind ->
    kcApps kind (ppr cls) tys	`thenM` \ (tys', res_kind) ->
    returnM (HsClassP cls tys', res_kind)

---------------------------
kcTyVar :: Name -> TcM TcKind
kcTyVar name	-- Could be a tyvar or a tycon
407
408
409
  = traceTc (text "lk1" <+> ppr name) 	`thenM_`
    tcLookup name	`thenM` \ thing ->
    traceTc (text "lk2" <+> ppr name <+> ppr thing) 	`thenM_`
410
    case thing of 
411
	ATyVar _ ty	    	-> returnM (typeKind ty)
412
	AThing kind		-> returnM kind
413
	AGlobal (ATyCon tc) 	-> returnM (tyConKind tc) 
414
	other			-> wrongThingErr "type" thing name
415
416
417
418
419

kcClass :: Name -> TcM TcKind
kcClass cls	-- Must be a class
  = tcLookup cls 				`thenM` \ thing -> 
    case thing of
420
	AThing kind		-> returnM kind
421
	AGlobal (AClass cls)    -> returnM (tyConKind (classTyCon cls))
422
	other		        -> wrongThingErr "class" thing cls
423
424
425
426
427
428
429
430
431
432
433
434
435
436
\end{code}


%************************************************************************
%*									*
		Desugaring
%*									*
%************************************************************************

The type desugarer

	* Transforms from HsType to Type
	* Zonks any kinds

437
It cannot fail, and does no validity checking, except for 
438
439
440
structural matters, such as
	(a) spurious ! annotations.
	(b) a class used as a type
441
442

\begin{code}
443
444
445
dsHsType :: LHsType Name -> TcM Type
-- All HsTyVarBndrs in the intput type are kind-annotated
dsHsType ty = ds_type (unLoc ty)
446

447
ds_type ty@(HsTyVar name)
448
449
  = ds_app ty []

450
ds_type (HsParTy ty)		-- Remove the parentheses markers
451
452
  = dsHsType ty

453
454
455
ds_type ty@(HsBangTy _ _)	-- No bangs should be here
  = failWithTc (ptext SLIT("Unexpected strictness annotation:") <+> ppr ty)

456
ds_type (HsKindSig ty k)
457
458
  = dsHsType ty	-- Kind checking done already

459
ds_type (HsListTy ty)
460
461
  = dsHsType ty			`thenM` \ tau_ty ->
    checkWiredInTyCon listTyCon	`thenM_`
462
463
    returnM (mkListTy tau_ty)

464
ds_type (HsPArrTy ty)
465
466
  = dsHsType ty			`thenM` \ tau_ty ->
    checkWiredInTyCon parrTyCon	`thenM_`
467
468
    returnM (mkPArrTy tau_ty)

469
ds_type (HsTupleTy boxity tys)
470
471
472
473
474
  = dsHsTypes tys		`thenM` \ tau_tys ->
    checkWiredInTyCon tycon	`thenM_`
    returnM (mkTyConApp tycon tau_tys)
  where
    tycon = tupleTyCon boxity (length tys)
475

476
ds_type (HsFunTy ty1 ty2)
477
478
479
480
  = dsHsType ty1			`thenM` \ tau_ty1 ->
    dsHsType ty2			`thenM` \ tau_ty2 ->
    returnM (mkFunTy tau_ty1 tau_ty2)

481
482
483
ds_type (HsOpTy ty1 (L span op) ty2)
  = dsHsType ty1 		`thenM` \ tau_ty1 ->
    dsHsType ty2 		`thenM` \ tau_ty2 ->
484
    setSrcSpan span (ds_var_app op [tau_ty1,tau_ty2])
485

486
ds_type (HsNumTy n)
487
488
489
490
  = ASSERT(n==1)
    tcLookupTyCon genUnitTyConName	`thenM` \ tc ->
    returnM (mkTyConApp tc [])

491
492
ds_type ty@(HsAppTy _ _)
  = ds_app ty []
493

494
ds_type (HsPredTy pred)
495
496
497
  = dsHsPred pred	`thenM` \ pred' ->
    returnM (mkPredTy pred')

498
ds_type full_ty@(HsForAllTy exp tv_names ctxt ty)
499
  = tcTyVarBndrs tv_names		$ \ tyvars ->
500
    mappM dsHsLPred (unLoc ctxt)	`thenM` \ theta ->
501
502
503
504
505
506
507
508
509
510
    dsHsType ty				`thenM` \ tau ->
    returnM (mkSigmaTy tyvars theta tau)

dsHsTypes arg_tys = mappM dsHsType arg_tys
\end{code}

Help functions for type applications
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

\begin{code}
511
ds_app :: HsType Name -> [LHsType Name] -> TcM Type
512
ds_app (HsAppTy ty1 ty2) tys
513
  = ds_app (unLoc ty1) (ty2:tys)
514
515
516
517
518

ds_app ty tys
  = dsHsTypes tys			`thenM` \ arg_tys ->
    case ty of
	HsTyVar fun -> ds_var_app fun arg_tys
519
	other	    -> ds_type ty		`thenM` \ fun_ty ->
520
521
522
523
524
525
		       returnM (mkAppTys fun_ty arg_tys)

ds_var_app :: Name -> [Type] -> TcM Type
ds_var_app name arg_tys 
 = tcLookup name			`thenM` \ thing ->
    case thing of
526
	ATyVar _ ty 	    -> returnM (mkAppTys ty arg_tys)
527
	AGlobal (ATyCon tc) -> returnM (mkTyConApp tc arg_tys)
528
	other		    -> wrongThingErr "type" thing name
529
530
531
532
533
\end{code}


Contexts
~~~~~~~~
534

535
\begin{code}
536
537
dsHsLPred :: LHsPred Name -> TcM PredType
dsHsLPred pred = dsHsPred (unLoc pred)
538

539
dsHsPred pred@(HsClassP class_name tys)
540
541
542
543
  = dsHsTypes tys			`thenM` \ arg_tys ->
    tcLookupClass class_name		`thenM` \ clas ->
    returnM (ClassP clas arg_tys)

544
dsHsPred (HsIParam name ty)
545
546
547
548
  = dsHsType ty					`thenM` \ arg_ty ->
    returnM (IParam name arg_ty)
\end{code}

549
550
551
GADT constructor signatures

\begin{code}
552
tcLHsConResTy :: LHsType Name -> TcM (TyCon, [TcType])
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
tcLHsConResTy res_ty
  = addErrCtxt (gadtResCtxt res_ty) $
    case get_largs res_ty [] of
	   (HsTyVar tc_name, args) 
	      -> do { args' <- mapM dsHsType args
		    ; thing <- tcLookup tc_name
		    ; case thing of
		        AGlobal (ATyCon tc) -> return (tc, args')
		        other -> failWithTc (badGadtDecl res_ty) }
	   other -> failWithTc (badGadtDecl res_ty)
  where
	-- We can't call dsHsType on res_ty, and then do tcSplitTyConApp_maybe
	-- because that causes a black hole, and for good reason.  Building
	-- the type means expanding type synonyms, and we can't do that
	-- inside the "knot".  So we have to work by steam.
    get_largs (L _ ty) args = get_args ty args
    get_args (HsAppTy fun arg) 		  args = get_largs fun (arg:args)
    get_args (HsParTy ty)      		  args = get_largs ty  args
571
572
    get_args (HsOpTy ty1 (L span tc) ty2) args = (HsTyVar tc, ty1:ty2:args)
    get_args ty  	     		  args = (ty, args)
573

574
575
gadtResCtxt ty
  = hang (ptext SLIT("In the result type of a data constructor:"))
576
577
       2 (ppr ty)
badGadtDecl ty
578
  = hang (ptext SLIT("Malformed constructor result type:"))
579
       2 (ppr ty)
580
581

typeCtxt ty = ptext SLIT("In the type") <+> quotes (ppr ty)
582
\end{code}
583
584
585
586
587
588
589
590
591

%************************************************************************
%*									*
		Type-variable binders
%*									*
%************************************************************************


\begin{code}
592
593
kcHsTyVars :: [LHsTyVarBndr Name] 
	   -> ([LHsTyVarBndr Name] -> TcM r) 	-- These binders are kind-annotated
594
595
596
						-- They scope over the thing inside
	   -> TcM r
kcHsTyVars tvs thing_inside 
597
  = mappM (wrapLocM kcHsTyVar) tvs	`thenM` \ bndrs ->
598
    tcExtendKindEnvTvs bndrs (thing_inside bndrs)
599
600
601
602
603
604
605
606

kcHsTyVar :: HsTyVarBndr Name -> TcM (HsTyVarBndr Name)
	-- Return a *kind-annotated* binder, and a tyvar with a mutable kind in it	
kcHsTyVar (UserTyVar name)        = newKindVar 	`thenM` \ kind ->
				    returnM (KindedTyVar name kind)
kcHsTyVar (KindedTyVar name kind) = returnM (KindedTyVar name kind)

------------------
607
tcTyVarBndrs :: [LHsTyVarBndr Name] 	-- Kind-annotated binders, which need kind-zonking
608
609
610
611
612
	     -> ([TyVar] -> TcM r)
	     -> TcM r
-- Used when type-checking types/classes/type-decls
-- Brings into scope immutable TyVars, not mutable ones that require later zonking
tcTyVarBndrs bndrs thing_inside
613
  = mapM (zonk . unLoc) bndrs	`thenM` \ tyvars ->
614
615
    tcExtendTyVarEnv tyvars (thing_inside tyvars)
  where
616
617
    zonk (KindedTyVar name kind) = do { kind' <- zonkTcKindToKind kind
				      ; return (mkTyVar name kind') }
618
    zonk (UserTyVar name) = pprTrace "Un-kinded tyvar" (ppr name) $
619
			    return (mkTyVar name liftedTypeKind)
620
621
622

-----------------------------------
tcDataKindSig :: Maybe Kind -> TcM [TyVar]
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
623
-- GADT decls can have a (perhaps partial) kind signature
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
--	e.g.  data T :: * -> * -> * where ...
-- This function makes up suitable (kinded) type variables for 
-- the argument kinds, and checks that the result kind is indeed *
tcDataKindSig Nothing = return []
tcDataKindSig (Just kind)
  = do	{ checkTc (isLiftedTypeKind res_kind) (badKindSig kind)
	; span <- getSrcSpanM
	; us   <- newUniqueSupply 
	; let loc   = srcSpanStart span
	      uniqs = uniqsFromSupply us
	; return [ mk_tv loc uniq str kind 
		 | ((kind, str), uniq) <- arg_kinds `zip` names `zip` uniqs ] }
  where
    (arg_kinds, res_kind) = splitKindFunTys kind
    mk_tv loc uniq str kind = mkTyVar name kind
	where
	   name = mkInternalName uniq occ loc
	   occ  = mkOccName tvName str

    names :: [String]	-- a,b,c...aa,ab,ac etc
    names = [ c:cs | cs <- "" : names, c <- ['a'..'z'] ] 

badKindSig :: Kind -> SDoc
badKindSig kind 
 = hang (ptext SLIT("Kind signature on data type declaration has non-* return kind"))
	2 (ppr kind)
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
\end{code}


%************************************************************************
%*									*
		Scoped type variables
%*									*
%************************************************************************


tcAddScopedTyVars is used for scoped type variables added by pattern
type signatures
	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).

Usually we kind-infer and expand type splices, and then
tupecheck/desugar the type.  That doesn't work well for scoped type
variables, because they scope left-right in patterns.  (e.g. in the
example above, the 'a' in (y::a) is bound by the 'a' in (x::a).

The current not-very-good plan is to
  * find all the types in the patterns
  * find their free tyvars
  * do kind inference
  * bring the kinded type vars into scope
  * BUT throw away the kind-checked type
  	(we'll kind-check it again when we type-check the pattern)

This is bad because throwing away the kind checked type throws away
its splices.  But too bad for now.  [July 03]

Historical note:
    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

\begin{code}
693
694
695
696
697
698
699
700
tcHsPatSigType :: UserTypeCtxt
	       -> LHsType Name 		-- The type signature
	       -> TcM ([TyVar], 	-- Newly in-scope type variables
			Type)		-- The signature
-- Used for type-checking type signatures in
-- (a) patterns 	  e.g  f (x::Int) = e
-- (b) result signatures  e.g. g x :: Int = e
-- (c) RULE forall bndrs  e.g. forall (x::Int). f x = x
701

702
703
704
705
706
707
708
709
tcHsPatSigType ctxt hs_ty 
  = addErrCtxt (pprHsSigCtxt ctxt hs_ty) $
    do	{ 	-- Find the type variables that are mentioned in the type
		-- but not already in scope.  These are the ones that
		-- should be bound by the pattern signature
 	  in_scope <- getInLocalScope
	; let span = getLoc hs_ty
	      sig_tvs = [ L span (UserTyVar n) 
710
711
712
			| n <- nameSetToList (extractHsTyVars hs_ty),
			  not (in_scope n) ]

713
714
	-- Behave very like type-checking (HsForAllTy sig_tvs hs_ty),
	-- except that we want to keep the tvs separate
715
716
717
	; (kinded_tvs, kinded_ty) <- kcHsTyVars sig_tvs $ \ kinded_tvs -> do
				    { kinded_ty <- kcTypeType hs_ty
				    ; return (kinded_tvs, kinded_ty) }
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
	; tcTyVarBndrs kinded_tvs $ \ tyvars -> do
	{ sig_ty <- dsHsType kinded_ty
	; checkValidType ctxt sig_ty 
	; return (tyvars, sig_ty)
      } }

tcPatSig :: UserTypeCtxt
	 -> LHsType Name
	 -> BoxySigmaType
	 -> TcM (TcType,	   -- The type to use for "inside" the signature
		 [(Name,TcType)])  -- The new bit of type environment, binding
				   -- the scoped type variables
tcPatSig ctxt sig res_ty
  = do	{ (sig_tvs, sig_ty) <- tcHsPatSigType ctxt sig

	; if null sig_tvs then do {
		-- The type signature binds no type variables, 
		-- and hence is rigid, so use it to zap the res_ty
		  boxyUnify sig_ty res_ty
		; return (sig_ty, [])

	} else do {
		-- Type signature binds at least one scoped type variable
	
		-- A pattern binding cannot bind scoped type variables
		-- The renamer fails with a name-out-of-scope error 
		-- if a pattern binding tries to bind a type variable,
		-- So we just have an ASSERT here
	; let in_pat_bind = case ctxt of
				BindPatSigCtxt -> True
				other	       -> False
	; ASSERT( not in_pat_bind || null sig_tvs ) return ()

	  	-- Check that pat_ty is rigid
	; checkTc (isRigidTy res_ty) (wobblyPatSig sig_tvs)

		-- Now match the pattern signature against res_ty
		-- For convenience, and uniform-looking error messages
		-- we do the matching by allocating meta type variables, 
		-- unifying, and reading out the results.
		-- This is a strictly local operation.
	; box_tvs <- mapM tcInstBoxyTyVar sig_tvs
	; boxyUnify (substTyWith sig_tvs (mkTyVarTys box_tvs) sig_ty) res_ty
	; sig_tv_tys <- mapM readFilledBox box_tvs

		-- Check that each is bound to a distinct type variable,
		-- and one that is not already in scope
	; let tv_binds = map tyVarName sig_tvs `zip` sig_tv_tys
	; binds_in_scope <- getScopedTyVarBinds
	; check binds_in_scope tv_binds
	
		-- Phew!
	; return (res_ty, tv_binds)
	} }
772
  where
773
774
775
    check in_scope []		 = return ()
    check in_scope ((n,ty):rest) = do { check_one in_scope n ty
				      ; check ((n,ty):in_scope) rest }
776

777
778
779
    check_one in_scope n ty
	= do { checkTc (tcIsTyVarTy ty) (scopedNonVar n ty)
		-- Must bind to a type variable
780

781
782
783
	     ; checkTc (null dups) (dupInScope n (head dups) ty)
		-- Must not bind to the same type variable
		-- as some other in-scope type variable
784

785
786
787
	     ; return () }
	where
	  dups = [n' | (n',ty') <- in_scope, tcEqType ty' ty]
788
789
790
791
792
\end{code}


%************************************************************************
%*									*
793
		Scoped type variables
794
795
796
797
%*									*
%************************************************************************

\begin{code}
798
799
800
pprHsSigCtxt :: UserTypeCtxt -> LHsType Name -> SDoc
pprHsSigCtxt ctxt hs_ty = vcat [ ptext SLIT("In") <+> pprUserTypeCtxt ctxt <> colon, 
				 nest 2 (pp_sig ctxt) ]
801
  where
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
    pp_sig (FunSigCtxt n)  = pp_n_colon n
    pp_sig (ConArgCtxt n)  = pp_n_colon n
    pp_sig (ForSigCtxt n)  = pp_n_colon n
    pp_sig (RuleSigCtxt n) = pp_n_colon n
    pp_sig other	   = ppr (unLoc hs_ty)

    pp_n_colon n = ppr n <+> dcolon <+> ppr (unLoc hs_ty)


wobblyPatSig sig_tvs
  = hang (ptext SLIT("A pattern type signature cannot bind scoped type variables") 
		<+> pprQuotedList sig_tvs)
       2 (ptext SLIT("unless the pattern has a rigid type context"))
		
scopedNonVar n ty
  = vcat [sep [ptext SLIT("The scoped type variable") <+> quotes (ppr n),
	       nest 2 (ptext SLIT("is bound to the type") <+> quotes (ppr ty))],
	  nest 2 (ptext SLIT("You can only bind scoped type variables to type variables"))]

dupInScope n n' ty
  = hang (ptext SLIT("The scoped type variables") <+> quotes (ppr n) <+> ptext SLIT("and") <+> quotes (ppr n'))
       2 (vcat [ptext SLIT("are bound to the same type (variable)"),
		ptext SLIT("Distinct scoped type variables must be distinct")])
825
826
\end{code}